Replace mono by gcongr where possible; one golf using gcongr.

leanprover-community · Jul 7, 2024 · 406babb · 406babb
1 parent f469c7a
commit 406babb
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 5 deletions.
diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean
@@ -111,7 +111,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple' (hRample : R.Ample) (hRopen : IsOpen
       φ.openEmbedding.toInducing.isCompact_preimage' K₁_cpct K₁φ
     have K₀K₁' : φ ⁻¹' K₀ ⊆ interior (φ ⁻¹' K₁) := by
       rw [← φ.isOpenMap.preimage_interior_eq_interior_preimage φ.continuous]
-      mono
+      gcongr
     simp only [P₀, forall_and] at P₀f
     rcases P₀f with ⟨hf_sec, hf_sol, hf_smooth, hf_A, hf_dist⟩
     rw [forall_restrictGermPredicate_iff] at hf_A

diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean
@@ -294,6 +294,8 @@ lemma ContMDiffMap.snd_apply (x : M) (x' : M') :
 
 end
 
+attribute [gcongr] preimage_mono Set.prod_mono
+
 /-- In `J¹(M, M')`, the target of a chart has a nice formula -/
 theorem oneJetBundle_chart_target (x₀ : J¹MM') :
     (chartAt HJ x₀).target = Prod.fst ⁻¹' (chartAt (ModelProd H H') x₀.proj).target := by

diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean
@@ -8,6 +8,8 @@ import SphereEversion.Notations
 
 -- set_option trace.filter_inst_type true
 
+attribute [gcongr] nhdsSet_mono
+
 open Set Filter Function
 
 open scoped Topology unitInterval
@@ -239,8 +241,7 @@ theorem relative_inductive_construction_of_loc {X Y : Type*} [EMetricSpace X]
     refine ⟨f, fun x ↦ ⟨h₀f x, restrictGermPredicate_congr (hf₁ x).2 ?_⟩, ?_, ?_⟩
     · exact h'f.filter_mono (nhdsSet_mono <| subset_union_of_subset_right hKU₂' K₁')
     · rwa [hK₁'K₂'] at hf
-    · apply h'f.filter_mono (nhdsSet_mono <| ?_)
-      exact union_subset_union hK₁K₁' <| compl_subset_compl_of_subset hU₂'U₂
+    · apply h'f.filter_mono; gcongr
   rcases inductive_construction_of_loc P₀ P₀' P₁ hf₀ loc ind' with ⟨f, hf⟩
   simp only [forall_and, forall_restrictGermPredicate_iff] at hf ⊢
   exact ⟨f, ⟨hf.1, hf.2.2⟩, hf.2.1⟩
@@ -473,7 +474,7 @@ theorem inductive_htpy_construction' {X Y : Type*}
     with ⟨F, hF₀, hF₁, hF₂, hFK₁, ht⟩
   refine ⟨F, hF₀, ?_, hF₂, ?_, ht⟩
   apply hF₁.filter_mono
-  mono
+  gcongr
   rw [bUnion_le]
   exact fun t x hx ↦ hFK₁ t x (not_mem_subset K₁W hx)
 end Htpy
diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean
@@ -132,7 +132,7 @@ theorem ContDiff.periodize {f : ℝ → E} {n : ℕ∞} (h : ContDiff ℝ n f) (
     intro i hi
     rw [mem_setOf_eq, ← nonempty_iff_ne_empty]
     apply Nonempty.mono _ hi
-    mono
+    gcongr
     · rw [show (e i : ℝ → ℝ) = VAdd.vadd i by ext x; exact add_comm x i]
       exact image_subset _ Ioo_subset_Icc_self
     exact subset_tsupport f