Restore old proof using mono.

leanprover-community · Oct 7, 2024 · 5e6aeb0 · 5e6aeb0
1 parent 3d99d1b
commit 5e6aeb0
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean
@@ -13,6 +13,7 @@ import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
 import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc
 import Mathlib.Geometry.Manifold.VectorBundle.Hom
 import Mathlib.Geometry.Manifold.VectorBundle.Pullback
+import Mathlib.Tactic.Monotonicity.Lemmas
 
 /-!
 # 1-jet bundles
@@ -314,8 +315,7 @@ theorem oneJetBundle_chart_target (x₀ : J¹MM') :
       (Prod.map (chartAt H m).symm (chartAt H' m').symm) ∘ Prod.fst := by
     ext x <;> rfl
   rw [this, preimage_comp, preimage_prod_map_prod]
-  simp only [Prod.range_fst, subset_univ, preimage_subset_preimage_iff]
-  gcongr
+  mono
   · exact (chartAt H m).target_subset_preimage_source
   · exact (chartAt H' m').target_subset_preimage_source