chore: bump mathlib

SphereEversion.lean

@@ -57,5 +57,4 @@ import SphereEversion.ToMathlib.Topology.Algebra.Module
 import SphereEversion.ToMathlib.Topology.Misc
 import SphereEversion.ToMathlib.Topology.Paracompact
 import SphereEversion.ToMathlib.Topology.Path
-import SphereEversion.ToMathlib.Topology.Separation.Hausdorff
 import SphereEversion.ToMathlib.Unused.Fin

SphereEversion/Global/Immersion.lean

@@ -72,7 +72,8 @@ omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 @[simp]
 theorem immersionRel_slice_eq {m : M} {m' : M'} {p : DualPair <| TangentSpace I m}
     {φ : TangentSpace I m →L[ℝ] TangentSpace I' m'} (hφ : Injective φ) :
-    (immersionRel I M I' M').slice ⟨(m, m'), φ⟩ p = ((ker p.π).map φ : Set <| TM' m')ᶜ :=
+    (immersionRel I M I' M').slice ⟨(m, m'), φ⟩ p =
+      (((p.π.ker).map (φ : TM m →ₛₗ[.id ℝ] TM' m')): Set <| TM' m')ᶜ :=
   Set.ext_iff.mpr fun _ ↦ p.injective_update_iff hφ
 
 variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ E']

SphereEversion/Global/OneJetSec.lean

@@ -264,18 +264,18 @@ theorem uncurry_ϕ' (S : FamilyOneJetSec I M I' M' IP P) (p : P × M) :
   congr 1
   convert
     mfderiv_comp p ((S.contMDiff_bs.comp (contMDiff_id.prodMk contMDiff_const)).mdifferentiable
-      (by simp) p.1) (contMDiff_fst.mdifferentiable le_top p)
+      (by simp) p.1) (contMDiff_fst.mdifferentiable one_ne_zero p)
   simp_rw [mfderiv_fst]
   rfl
 
 theorem isHolonomicAt_uncurry (S : FamilyOneJetSec I M I' M' IP P) {p : P × M} :
     S.uncurry.IsHolonomicAt p ↔ (S p.1).IsHolonomicAt p.2 := by
   simp_rw [OneJetSec.IsHolonomicAt, OneJetSec.snd_eq, S.uncurry_ϕ]
   rw [show S.uncurry.bs = fun x ↦ S.uncurry.bs x from rfl, funext S.uncurry_bs]
-  simp_rw [mfderiv_prod_eq_add (S.contMDiff_bs.mdifferentiableAt (mod_cast le_top)),
+  simp_rw [mfderiv_prod_eq_add (S.contMDiff_bs.mdifferentiableAt (by simp)),
     mfderiv_snd, add_right_inj]
-  erw [mfderiv_comp p (S.contMDiff_coe_bs.mdifferentiableAt (mod_cast le_top))
-    (contMDiff_snd.mdifferentiableAt le_top), mfderiv_snd]
+  erw [mfderiv_comp p (S.contMDiff_coe_bs.mdifferentiableAt (by simp))
+    (contMDiff_snd.mdifferentiableAt one_ne_zero), mfderiv_snd]
   exact (show Surjective (ContinuousLinearMap.snd ℝ EP E) from
     Prod.snd_surjective).clm_comp_injective.eq_iff
 

SphereEversion/Global/ParametricityForFree.lean

@@ -82,9 +82,9 @@ theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
     erw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply,
          ← ContinuousLinearMap.map_neg, neg_sub]
     obtain ⟨u, hu, t, rfl⟩ := q.decomp x
-    have hv : (id (0, (q.v : E)) : TangentSpace (IP.prod I) σ.proj.1) - p.v ∈ ker p.π := by
+    have hv : (id (0, (q.v : E)) : TangentSpace (IP.prod I) σ.proj.1) - p.v ∈ p.π.ker := by
       simp [LinearMap.mem_ker, map_sub, p.pairing, h2pq, q.pairing, sub_self]
-    have hup : ((0 : EP), u) ∈ ker p.π := (h2pq u).trans hu
+    have hup : ((0 : EP), u) ∈ p.π.ker := (h2pq u).trans hu
     erw [q.update_apply _ hu, ← Prod.zero_mk_add_zero_mk, map_add, p.update_ker_pi _ _ hup, ←
       Prod.smul_zero_mk, map_smul]
     conv_lhs => rw [← sub_add_cancel (0, q.v) p.v]
@@ -203,7 +203,7 @@ theorem FamilyOneJetSec.curry_ϕ' (S : FamilyOneJetSec (IP.prod I) (P × M) I' M
     (x : M) : (S.curry p).ϕ x = (S p.1).ϕ (p.2, x) ∘L ContinuousLinearMap.inr ℝ EP E := by
   rw [S.curry_ϕ]
   congr 1
-  refine (mdifferentiableAt_const.mfderiv_prod (contMDiff_id.mdifferentiableAt le_top)).trans ?_
+  refine (mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_id).trans ?_
   rw [mfderiv_id, mfderiv_const]
   rfl
 
@@ -216,9 +216,8 @@ theorem FamilyOneJetSec.isHolonomicAt_curry (S : FamilyOneJetSec (IP.prod I) (P
     (S.curry (t, s)).IsHolonomicAt x := by
   simp_rw [OneJetSec.IsHolonomicAt, (S.curry _).snd_eq, S.curry_ϕ] at hS ⊢
   rw [show (S.curry (t, s)).bs = fun x ↦ (S.curry (t, s)).bs x from rfl, funext (S.curry_bs _)]
-  refine (mfderiv_comp x ((S t).contMDiff_bs.mdifferentiableAt (mod_cast le_top))
-    (mdifferentiableAt_const.prodMk (contMDiff_id.mdifferentiableAt le_top))).trans
-    ?_
+  refine (mfderiv_comp x ((S t).contMDiff_bs.mdifferentiableAt (by simp))
+    (mdifferentiableAt_const.prodMk mdifferentiableAt_id)).trans ?_
   rw [id, hS]
   rfl
 

SphereEversion/Global/Relation.lean

@@ -613,7 +613,7 @@ def OneJetBundle.embedding : OpenSmoothEmbedding IXY J¹XY IMN J¹MN where
   left_inv' {σ} := by
     rw [OpenSmoothEmbedding.transfer, OneJetBundle.map_map]; rotate_left
     · exact (ψ.contMDiffAt_inv'.mdifferentiableAt (by simp))
-    · exact ψ.contMDiff_to.contMDiffAt.mdifferentiableAt (mod_cast le_top)
+    · exact ψ.contMDiff_to.contMDiffAt.mdifferentiableAt (by simp)
     conv_rhs => rw [← OneJetBundle.map_id σ]
     congr 1
     · rw [OpenSmoothEmbedding.invFun_comp_coe]

SphereEversion/Global/SmoothEmbedding.lean

@@ -89,9 +89,9 @@ variable [IsManifold I ∞ M] [IsManifold I' ∞ M']
 def fderiv (x : M) : TangentSpace I x ≃L[𝕜] TangentSpace I' (f x) :=
   have h₁ : MDifferentiableAt I' I f.invFun (f x) :=
     ((f.contMDiffOn_inv (f x)
-    (mem_range_self x)).mdifferentiableWithinAt (mod_cast le_top)).mdifferentiableAt
+    (mem_range_self x)).mdifferentiableWithinAt (by simp)).mdifferentiableAt
     (f.isOpenMap.range_mem_nhds x)
-  have h₂ : MDifferentiableAt I I' f x := f.contMDiff_to.mdifferentiableAt (mod_cast le_top)
+  have h₂ : MDifferentiableAt I I' f x := f.contMDiff_to.mdifferentiableAt (by simp)
   ContinuousLinearEquiv.equivOfInverse (mfderiv% f x) (mfderiv% f.invFun (f x))
     (by
       intro v

SphereEversion/InductiveConstructions.lean

@@ -326,7 +326,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ
       rcases eq_or_lt_of_le ht with (rfl | ht)
       · apply Quotient.sound
         replace hpast_F' : ↿F' =ᶠ[𝓝 (0, x)] fun q : ℝ × X ↦ F (T i.toNat, q.2) := by
-          have : 𝓝 (0 : ℝ) ≤ 𝓝ˢ (Iic 0) := nhds_le_nhdsSet right_mem_Iic
+          have : 𝓝 (0 : ℝ) ≤ 𝓝ˢ (Iic 0) := nhds_le_nhdsSet self_mem_Iic
           apply mem_of_superset (prod_mem_nhds (hpast_F'.filter_mono this) univ_mem)
           rintro ⟨t', x'⟩ ⟨ht', -⟩
           exact (congr_fun ht' x' : _)

SphereEversion/Local/Corrugation.lean

@@ -167,7 +167,7 @@ theorem corrugation.fderiv_eq {N : ℝ} (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ)
   have key := (hasFDerivAt_parametric_primitive_of_contDiff' diff (hπ_diff.const_smul N) x₀ 0).2
   erw [fderiv_const_smul key.differentiableAt, key.fderiv, smul_add, add_comm]
   congr 1
-  rw [fderiv_fun_const_smul (hπ_diff.differentiable le_rfl).differentiableAt N, π.fderiv]
+  rw [fderiv_fun_const_smul (hπ_diff.differentiable (by simp)).differentiableAt N, π.fderiv]
   simp only [smul_smul, inv_mul_cancel₀ hN, one_div, smul_eq_mul, one_smul,
     ContinuousLinearMap.comp_smul]
 
@@ -181,8 +181,8 @@ theorem fderiv_corrugated_map (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ) {f : E 
     D (f + corrugation p.π N γ) x =
       p.update (D f x) (γ x (N * p.π x)) + corrugation.remainder p.π N γ x := by
   ext v
-  erw [fderiv_add (hf.differentiable le_rfl).differentiableAt
-      ((corrugation.contDiff _ N hγ_diff).differentiable le_rfl).differentiableAt]
+  erw [fderiv_add (hf.differentiable (by simp)).differentiableAt
+      ((corrugation.contDiff _ N hγ_diff).differentiable (by simp)).differentiableAt]
   simp_rw [ContinuousLinearMap.add_apply, corrugation.fderiv_apply _ N hN hγ_diff, hfγ,
     DualPair.update, ContinuousLinearMap.add_apply, p.π.comp_toSpanSingleton_apply, add_assoc]
 

SphereEversion/Local/DualPair.lean

@@ -65,7 +65,7 @@ attribute [local simp] ContinuousLinearMap.toSpanSingleton_apply
 theorem pi_ne_zero (p : DualPair E) : p.π ≠ 0 := fun H ↦ by
   simpa [H] using p.pairing
 
-theorem ker_pi_ne_top (p : DualPair E) : ker p.π ≠ ⊤ := fun H ↦ by
+theorem ker_pi_ne_top (p : DualPair E) : p.π.ker ≠ ⊤ := fun H ↦ by
   have : p.π.toLinearMap p.v = 1 := p.pairing
   simpa [LinearMap.ker_eq_top.mp H]
 
@@ -84,10 +84,10 @@ def update (p : DualPair E) (φ : E →L[ℝ] F) (w : F) : E →L[ℝ] F :=
   φ + (w - φ p.v) ⬝ p.π
 
 @[simp]
-theorem update_ker_pi (p : DualPair E) (φ : E →L[ℝ] F) (w : F) {u} (hu : u ∈ ker p.π) :
+theorem update_ker_pi (p : DualPair E) (φ : E →L[ℝ] F) (w : F) {u} (hu : u ∈ p.π.ker) :
     p.update φ w u = φ u := by
   rw [LinearMap.mem_ker] at hu
-  simp [update, hu]
+  simpa [update] using Or.inl hu
 
 @[simp]
 theorem update_v (p : DualPair E) (φ : E →L[ℝ] F) (w : F) : p.update φ w p.v = w := by
@@ -105,29 +105,29 @@ theorem update_update (p : DualPair E) (φ : E →L[ℝ] F) (w w' : F) :
     add_sub_cancel, add_assoc, ← ContinuousLinearMap.add_comp, ← toSpanSingleton_add,
     sub_add_eq_add_sub, add_sub_cancel]
 
-theorem inf_eq_bot (p : DualPair E) : ker p.π ⊓ p.spanV = ⊥ := bot_unique <| fun x hx ↦ by
+theorem inf_eq_bot (p : DualPair E) : p.π.ker ⊓ p.spanV = ⊥ := bot_unique <| fun x hx ↦ by
   have : p.π x = 0 ∧ ∃ a : ℝ, a • p.v = x := by
     simpa [DualPair.spanV, Submodule.mem_span_singleton] using hx
   rcases this with ⟨H, t, rfl⟩
   rw [p.π.map_smul, p.pairing, smul_eq_mul, mul_one] at H
   simp [H]
 
-theorem sup_eq_top (p : DualPair E) : ker p.π ⊔ p.spanV = ⊤ := by
+theorem sup_eq_top (p : DualPair E) : p.π.ker ⊔ p.spanV = ⊤ := by
   rw [Submodule.sup_eq_top_iff]
   intro x
   refine ⟨x - p.π x • p.v, ?_, p.π x • p.v, ?_, ?_⟩ <;>
     simp [DualPair.spanV, Submodule.mem_span_singleton, p.pairing]
 
-theorem decomp (p : DualPair E) (e : E) : ∃ u ∈ ker p.π, ∃ t : ℝ, e = u + t • p.v := by
-  have : e ∈ ker p.π ⊔ p.spanV := by
+theorem decomp (p : DualPair E) (e : E) : ∃ u ∈ p.π.ker, ∃ t : ℝ, e = u + t • p.v := by
+  have : e ∈ p.π.ker ⊔ p.spanV := by
     rw [p.sup_eq_top]
     exact Submodule.mem_top
   simp_rw [Submodule.mem_sup, DualPair.mem_spanV] at this
   rcases this with ⟨u, hu, -, ⟨t, rfl⟩, rfl⟩
   exact ⟨u, hu, t, rfl⟩
 
 -- useful with `DualPair.decomp`
-theorem update_apply (p : DualPair E) (φ : E →L[ℝ] F) {w : F} {t : ℝ} {u} (hu : u ∈ ker p.π) :
+theorem update_apply (p : DualPair E) (φ : E →L[ℝ] F) {w : F} {t : ℝ} {u} (hu : u ∈ p.π.ker) :
     p.update φ w (u + t • p.v) = φ u + t • w := by
   rw [map_add, map_smul, p.update_v, p.update_ker_pi _ _ hu]
 
@@ -152,23 +152,20 @@ theorem map_update_comp_right (p : DualPair E) (ψ' : E →L[ℝ] F) (φ : E ≃
 
 @[simp]
 theorem injective_update_iff (p : DualPair E) {φ : E →L[ℝ] F} (hφ : Injective φ) {w : F} :
-    Injective (p.update φ w) ↔ w ∉ (ker p.π).map φ := by
+    Injective (p.update φ w) ↔ w ∉ (p.π.ker).map (φ : E →ₛₗ[.id ℝ] F) := by
   constructor
   · rintro h ⟨u, hu, rfl⟩
     have : p.update φ (φ u) p.v = φ u := p.update_v φ (φ u)
-    conv_rhs at this => rw [← p.update_ker_pi φ (φ u) hu]
-    rw [← h this] at hu
-    simp only [SetLike.mem_coe, LinearMap.mem_ker] at hu
-    rw [p.pairing] at hu
-    linarith
+    nth_rw 2 [← p.update_ker_pi φ (φ u) hu] at this
+    simp [← h this, p.pairing] at hu
   · intro hw
     refine (injective_iff_map_eq_zero (p.update φ w)).mpr fun x hx ↦ ?_
     rcases p.decomp x with ⟨u, hu, t, rfl⟩
     rw [map_add, map_smul, update_v, p.update_ker_pi _ _ hu] at hx
     obtain rfl : t = 0 := by
       by_contra ht
       apply hw
-      refine ⟨-t⁻¹ • u, (ker p.π).smul_mem _ hu, ?_⟩
+      refine ⟨-t⁻¹ • u, (p.π.ker).smul_mem _ hu, ?_⟩
       rw [map_smul]
       have : -t⁻¹ • (φ u + t • w) + w = -t⁻¹ • (0 : F) + w := congr_arg (-t⁻¹ • · + w) hx
       rwa [smul_add, neg_smul, neg_smul, inv_smul_smul₀ ht, smul_zero, zero_add,

SphereEversion/Local/HPrinciple.lean

@@ -89,7 +89,7 @@ together with a dual pair `p` and a subspace `E'` of the corresponding hyperplan
 structure StepLandscape extends Landscape E where
   E' : Submodule ℝ E
   p : DualPair E
-  hEp : E' ≤ ker p.π
+  hEp : E' ≤ p.π.ker
 
 variable {E}
 
@@ -510,7 +510,7 @@ theorem RelLoc.FormalSol.improve (𝓕 : FormalSol R) (h_hol : ∀ᶠ x near L.C
     · apply (H.comp_le_0 _ _).mono
       · intro t ht
         rw [ht]
-        exact hH₀.self_of_nhdsSet 0 right_mem_Iic
+        exact hH₀.self_of_nhdsSet 0 self_mem_Iic
     -- t = 0
     · apply (H.comp_ge_1 _ _).mono
       · intro t ht

SphereEversion/Local/OneJet.lean

@@ -304,7 +304,7 @@ theorem HtpyJetSec.comp_le_0 (𝓕 𝓖 : HtpyJetSec E F) (h) :
 -- unused
 -- @[simp] can prove this
 theorem HtpyJetSec.comp_0 (𝓕 𝓖 : HtpyJetSec E F) (h) : 𝓕.comp 𝓖 h 0 = 𝓕 0 :=
-  (𝓕.comp_le_0 𝓖 h).self_of_nhdsSet 0 right_mem_Iic
+  (𝓕.comp_le_0 𝓖 h).self_of_nhdsSet 0 self_mem_Iic
 
 @[simp]
 theorem HtpyJetSec.comp_of_not_le (𝓕 𝓖 : HtpyJetSec E F) (h) {t : ℝ} (ht : ¬t ≤ 1 / 2) :
@@ -325,6 +325,6 @@ theorem HtpyJetSec.comp_ge_1 (𝓕 𝓖 : HtpyJetSec E F) (h) : ∀ᶠ t near Ic
 
 @[simp]
 theorem HtpyJetSec.comp_1 (𝓕 𝓖 : HtpyJetSec E F) (h) : 𝓕.comp 𝓖 h 1 = 𝓖 1 :=
-  (𝓕.comp_ge_1 𝓖 h).self_of_nhdsSet 1 left_mem_Ici
+  (𝓕.comp_ge_1 𝓖 h).self_of_nhdsSet 1 self_mem_Iic
 
 end HtpyJetSec

SphereEversion/Local/ParametricHPrinciple.lean

@@ -78,9 +78,9 @@ theorem relativize_slice_loc {σ : OneJet (P × E) F} {p : DualPair (P × E)} (q
     simp_rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply]
     rw [← ContinuousLinearMap.map_neg, neg_sub]
     obtain ⟨u, hu, t, rfl⟩ := q.decomp x
-    have hv : (0, q.v) - p.v ∈ ker p.π := by
-      rw [LinearMap.mem_ker, map_sub, p.pairing, h2pq, q.pairing, sub_self]
-    have hup : ((0 : P), u) ∈ ker p.π := (h2pq u).trans hu
+    have hv : (0, q.v) - p.v ∈ p.π.ker := by
+      simp [map_sub, p.pairing, h2pq, q.pairing, sub_self]
+    have hup : ((0 : P), u) ∈ p.π.ker := (h2pq u).trans hu
     rw [q.update_apply _ hu, ← Prod.zero_mk_add_zero_mk, map_add, p.update_ker_pi _ _ hup, ←
       Prod.smul_zero_mk, map_smul, vadd_eq_add]
     conv_lhs => { rw [← sub_add_cancel (0, q.v) p.v] }
@@ -140,7 +140,7 @@ theorem FamilyJetSec.uncurry_φ' (S : FamilyJetSec E F P) (p : P × E) :
         S.φ p.1 p.2 ∘L ContinuousLinearMap.snd ℝ P E := by
   simp_rw [S.uncurry_φ, fderiv_snd, add_left_inj]
   refine (fderiv_comp p ((S.f_diff.comp (contDiff_id.prodMk contDiff_const)).differentiable
-    (mod_cast le_top) p.1) differentiableAt_fst).trans ?_
+    (by simp) p.1) differentiableAt_fst).trans ?_
   rw [fderiv_fst]
   rfl
 
@@ -163,10 +163,9 @@ theorem FamilyJetSec.isHolonomicAt_uncurry (S : FamilyJetSec E F P) {p : P × E}
   simp_rw [JetSec.IsHolonomicAt, S.uncurry_φ]
   rw [show S.uncurry.f = fun x ↦ S.uncurry.f x from rfl, funext S.uncurry_f,
     show (fun x : P × E ↦ S.f x.1 x.2) = ↿S.f from rfl]
-  rw [fderiv_prod_eq_add (S.f_diff.differentiable (mod_cast le_top) _), fderiv_snd]
+  rw [fderiv_prod_eq_add (S.f_diff.differentiable (by simp) _), fderiv_snd]
   refine (add_right_inj _).trans ?_
-  have := fderiv_comp p ((S p.1).f_diff.contDiffAt.differentiableAt (mod_cast le_top))
-    differentiableAt_snd
+  have := fderiv_comp p ((S p.1).f_diff.contDiffAt.differentiableAt (by simp)) differentiableAt_snd
   rw [show D (fun z : P × E ↦ (↿S.f) (p.fst, z.snd)) p = _ from this, fderiv_snd,
     (show Surjective (ContinuousLinearMap.snd ℝ P E) from
           Prod.snd_surjective).clm_comp_injective.eq_iff]
@@ -217,7 +216,7 @@ theorem FamilyJetSec.isHolonomicAt_curry (S : FamilyJetSec (P × E) F G) {t : G}
     (hS : (S t).IsHolonomicAt (s, x)) : (S.curry (t, s)).IsHolonomicAt x := by
   simp_rw [JetSec.IsHolonomicAt, S.curry_φ] at hS ⊢
   rw [show (S.curry (t, s)).f = fun x ↦ (S.curry (t, s)).f x from rfl, funext (S.curry_f _)]
-  refine (fderiv_comp x ((S t).f_diff.contDiffAt.differentiableAt (mod_cast le_top))
+  refine (fderiv_comp x ((S t).f_diff.contDiffAt.differentiableAt (by simp))
     ((differentiableAt_const _).prodMk differentiableAt_id)).trans ?_
   rw [_root_.id, hS]
   rfl
@@ -287,7 +286,7 @@ theorem RelLoc.FamilyFormalSol.improve_htpy {ε : ℝ} (ε_pos : 0 < ε) (C : Se
   obtain ⟨𝓕, h₁, -, h₂, -, h₄, h₅⟩ :=
     𝓕₀.uncurry.improve_htpy' (R.isOpen_relativize h_op) (h_ample.relativize P) parametric_landscape
       ε_pos (h_hol.mono fun p hp ↦ 𝓕₀.isHolonomicAt_uncurry.mpr hp)
-  have h₁ : ∀ p, 𝓕 0 p = 𝓕₀.uncurry p := by intro p; rw [h₁.self_of_nhdsSet 0 right_mem_Iic]; rfl
+  have h₁ : ∀ p, 𝓕 0 p = 𝓕₀.uncurry p := by intro p; rw [h₁.self_of_nhdsSet 0 self_mem_Iic]; rfl
   refine ⟨𝓕.curry, ?_, ?_, ?_, ?_⟩
   · intro s x; exact curry_eq_iff_eq_uncurry_loc (h₁ (s, x))
   · refine h₂.mono ?_; rintro ⟨s, x⟩ hp t; exact curry_eq_iff_eq_uncurry_loc (hp t)