final fixes

leanprover-community · Dec 15, 2024 · d76594b · d76594b
1 parent 77a5035
commit d76594b
Show file tree

Hide file tree

Showing 8 changed files with 97 additions and 84 deletions.
diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean
@@ -16,6 +16,8 @@ open Set Filter ModelWithCorners Metric
 
 open scoped Topology Manifold
 
+local notation "∞" => (⊤ : ℕ∞)
+
 variable {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] [FiniteDimensional ℝ EM]
   {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} [Boundaryless IM]
   {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] [SmoothManifoldWithCorners IM M]
@@ -85,7 +87,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple' (hRample : R.Ample) (hRopen : IsOpen
       exact τ_pos x
   have hP₂' : ∀ (t : ℝ) (x : M) (f : M → J¹), P₀ x f → P₂ (t, x) fun p : ℝ × M ↦ f p.2 := by
     intro t x f hf
-    exact SmoothAt.comp (t, x) hf.2.2.1 contMDiffAt_snd
+    exact ContMDiffAt.comp (t, x) hf.2.2.1 contMDiffAt_snd
   have ind : ∀ m : M,
     ∃ V ∈ 𝓝 m, ∀ K₁ ⊆ V, ∀ K₀ ⊆ interior K₁, IsCompact K₀ → IsCompact K₁ → ∀ (C : Set M) (f : M → J¹),
       IsClosed C → (∀ x, P₀ x f) → (∀ᶠ x in 𝓝ˢ C, P₁ x f) →

diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean
@@ -13,6 +13,8 @@ open Metric Module Set Function LinearMap Filter ContinuousLinearMap
 
 open scoped Manifold Topology
 
+local notation "∞" => (⊤ : ℕ∞)
+
 section General
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
@@ -161,7 +163,7 @@ variable (ω : Orientation ℝ E (Fin 3))
 
 -- this result holds mutatis mutandis in `ℝ^n`
 theorem smooth_bs :
-    Smooth (𝓘(ℝ, ℝ).prod (𝓡 2)) 𝓘(ℝ, E)
+    ContMDiff (𝓘(ℝ, ℝ).prod (𝓡 2)) 𝓘(ℝ, E) ∞
       fun p : ℝ × (sphere (0 : E) 1) ↦ (1 - p.1) • (p.2 : E) + p.1 • -(p.2: E) := by
   refine (ContMDiff.smul ?_ ?_).add (contMDiff_fst.smul ?_)
   · exact (contDiff_const.sub contDiff_id).contMDiff.comp contMDiff_fst
@@ -174,11 +176,11 @@ def formalEversionAux : FamilyOneJetSec (𝓡 2) 𝕊² 𝓘(ℝ, E) E 𝓘(ℝ,
       (fun p : ℝ × 𝕊² ↦ ω.rot (p.1, p.2))
       (by
         intro p
-        have : SmoothAt 𝓘(ℝ, ℝ × E) 𝓘(ℝ, E →L[ℝ] E) ω.rot (p.1, p.2) := by
-          refine (ω.contDiff_rot ?_).contMDiffAt
+        have : ContMDiffAt 𝓘(ℝ, ℝ × E) 𝓘(ℝ, E →L[ℝ] E) ∞ ω.rot (p.1, p.2) := by
+          refine ((ω.contDiff_rot ?_).of_le le_top).contMDiffAt
           exact ne_zero_of_mem_unit_sphere p.2
-        refine this.comp p (Smooth.smoothAt ?_)
-        exact smooth_fst.prod_mk_space (contMDiff_coe_sphere.comp smooth_snd))
+        apply this.comp p (f := fun (p : ℝ × sphere 0 1) ↦ (p.1, (p.2 : E)))
+        apply contMDiff_fst.prod_mk_space (contMDiff_coe_sphere.comp contMDiff_snd))
 
 /-- A formal eversion of a two-sphere into its ambient Euclidean space. -/
 def formalEversionAux2 : HtpyFormalSol 𝓡_imm :=
@@ -285,21 +287,21 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {P : Type*} [TopologicalSpace P] [ChartedSpace HP P]
 
 -- move to Mathlib.Geometry.Manifold.ContMDiff.Product
-lemma Smooth.inr (x : M) :
-    Smooth I' (I.prod I') fun p : M' ↦ (⟨x, p⟩ : M × M') := by
-  rw [smooth_prod_iff]
-  exact ⟨smooth_const, smooth_id⟩
+lemma ContMDiff.inr {n : ℕ∞} (x : M) :
+    ContMDiff I' (I.prod I') n fun p : M' ↦ (⟨x, p⟩ : M × M') := by
+  rw [contMDiff_prod_iff]
+  exact ⟨contMDiff_const, contMDiff_id⟩
 
 -- xxx: is one better than the other?
-alias Smooth.prod_left := Smooth.inr
+alias ContMDiff.prod_left := ContMDiff.inr
 
 -- move to Mathlib.Geometry.Manifold.ContMDiff.Product
-theorem Smooth.uncurry_left
-    {f : M → M' → P} (hf : Smooth (I.prod I') IP ↿f) (x : M) :
-    Smooth I' IP (f x) := by
+theorem ContMDiff.uncurry_left {n : ℕ∞}
+    {f : M → M' → P} (hf : ContMDiff (I.prod I') IP n ↿f) (x : M) :
+    ContMDiff I' IP n (f x) := by
   have : f x = (uncurry f) ∘ fun p : M' ↦ ⟨x, p⟩ := by ext; simp
-  -- or just `apply hf.comp (Smooth.inr I I' x)`
-  rw [this]; exact hf.comp (Smooth.inr I I' x)
+  -- or just `apply hf.comp (ContMDiff.inr I I' x)`
+  rw [this]; exact hf.comp (ContMDiff.inr I I' x)
 
 end helper
 
@@ -335,7 +337,7 @@ theorem sphere_eversion :
     rw [this (1, x) (by simp)]
     convert formalEversion_one E ω x
   · exact fun t ↦ {
-      contMDiff := Smooth.uncurry_left 𝓘(ℝ, ℝ) (𝓡 2) 𝓘(ℝ, E) h₁ t
+      contMDiff := ContMDiff.uncurry_left 𝓘(ℝ, ℝ) (𝓡 2) 𝓘(ℝ, E) h₁ t
       diff_injective := h₅ t
     }
 

diff --git a/SphereEversion/Local/HPrinciple.lean b/SphereEversion/Local/HPrinciple.lean
@@ -148,7 +148,7 @@ theorem smooth_b (L : StepLandscape E) (𝓕 : JetSec E F) : 𝒞 ∞ (L.b 𝓕)
   (ContinuousLinearMap.apply ℝ F L.v).contDiff.comp 𝓕.φ_diff
 
 theorem smooth_g (L : StepLandscape E) (𝓕 : JetSec E F) : 𝒞 ∞ (L.g 𝓕) :=
-  (ContinuousLinearMap.apply ℝ F L.v).contDiff.comp (contDiff_top_iff_fderiv.mp 𝓕.f_diff).2
+  (ContinuousLinearMap.apply ℝ F L.v).contDiff.comp (contDiff_infty_iff_fderiv.mp 𝓕.f_diff).2
 
 theorem Accepts.rel {L : StepLandscape E} {𝓕 : JetSec E F} (h : L.Accepts R 𝓕) :
     ∀ᶠ x : E near L.K, (L.g 𝓕) x = (L.b 𝓕) x := by
@@ -187,7 +187,7 @@ theorem loop_smooth' (L : StepLandscape E) {𝓕 : FormalSol R} (h : L.Accepts R
 
 theorem loop_C1 (L : StepLandscape E) {𝓕 : FormalSol R} (h : L.Accepts R 𝓕) :
     ∀ t, 𝒞 1 ↿(L.loop h t) := fun _ ↦
-  (L.loop_smooth' h contDiff_const contDiff_snd contDiff_fst).of_le le_top
+  (L.loop_smooth' h contDiff_const contDiff_snd contDiff_fst).of_le (mod_cast le_top)
 
 variable (L : StepLandscape E)
 
@@ -228,15 +228,15 @@ def improveStep {𝓕 : FormalSol R} (h : L.Accepts R 𝓕) (N : ℝ) : HtpyJetS
       (smoothStep t * L.ρ x) • corrugation.remainder L.p.π N (L.loop h 1) x
   φ_diff := by
     apply ContDiff.add
-    apply L.p.smooth_update
-    apply 𝓕.φ_diff.snd'
-    apply L.loop_smooth'
-    exact smoothStep.smooth.fst'.mul L.ρ_smooth.snd'
-    apply contDiff_const.mul L.π.contDiff.snd'
-    exact contDiff_snd
-    apply ContDiff.smul
-    exact smoothStep.smooth.fst'.mul L.ρ_smooth.snd'
-    exact Remainder.smooth _ _ (L.loop_smooth h) contDiff_snd contDiff_const
+    · apply L.p.smooth_update
+      · exact 𝓕.φ_diff.snd'
+      apply L.loop_smooth'
+      · exact smoothStep.smooth.fst'.mul L.ρ_smooth.snd'
+      · apply contDiff_const.mul L.π.contDiff.snd'
+      · exact contDiff_snd
+    · apply ContDiff.smul
+      · exact smoothStep.smooth.fst'.mul L.ρ_smooth.snd'
+      · exact Remainder.smooth _ _ (L.loop_smooth h) contDiff_snd contDiff_const
 
 variable {L}
 variable {𝓕 : FormalSol R} (h : L.Accepts R 𝓕) (N : ℝ)
@@ -325,22 +325,24 @@ theorem improveStep_c0_close {ε : ℝ} (ε_pos : 0 < ε) :
     ∀ᶠ N in atTop, ∀ x t, ‖(L.improveStep h N t).f x - 𝓕.f x‖ ≤ ε := by
   set γ := L.loop h
   have γ_cont : Continuous ↿fun t x ↦ γ t x := (L.nice h).smooth.continuous
-  have γ_C1 : 𝒞 1 ↿(γ 1) := ((L.nice h).smooth.comp (contDiff_prod_mk_right 1)).of_le le_top
+  have γ_C1 : 𝒞 1 ↿(γ 1) := ((L.nice h).smooth.comp (contDiff_prod_mk_right 1)).of_le
+    (mod_cast le_top)
   apply
     ((corrugation.c0_small_on _ L.hK₁ (L.nice h).t_le_zero (L.nice h).t_ge_one γ_cont ε_pos).and <|
         remainder_c0_small_on L.π L.hK₁ γ_C1 ε_pos).mono
-  rintro N ⟨H, _⟩ x t
-  by_cases hx : x ∈ L.K₁
-  · rw [improveStep_apply_f h]
-    suffices ‖(smoothStep t * L.ρ x) • corrugation L.π N (L.loop h t) x‖ ≤ ε by simpa
-    exact (bu_lt _ _ <| H _ hx t).le
-  · rw [show (L.improveStep h N t).f x = 𝓕.f x from
-        congr_arg Prod.fst (improveStep_rel_compl_K₁ h N hx t)]
-    simp [ε_pos.le]
+  · rintro N ⟨H, _⟩ x t
+    by_cases hx : x ∈ L.K₁
+    · rw [improveStep_apply_f h]
+      suffices ‖(smoothStep t * L.ρ x) • corrugation L.π N (L.loop h t) x‖ ≤ ε by simpa
+      exact (bu_lt _ _ <| H _ hx t).le
+    · rw [show (L.improveStep h N t).f x = 𝓕.f x from
+          congr_arg Prod.fst (improveStep_rel_compl_K₁ h N hx t)]
+      simp [ε_pos.le]
 
 theorem improveStep_part_hol {N : ℝ} (hN : N ≠ 0) :
     ∀ᶠ x near L.K₀, (L.improveStep h N 1).IsPartHolonomicAt (L.p.spanV ⊔ L.E') x := by
-  have γ_C1 : 𝒞 1 ↿(L.loop h 1) := ((L.nice h).smooth.comp (contDiff_prod_mk_right 1)).of_le le_top
+  have γ_C1 : 𝒞 1 ↿(L.loop h 1) := ((L.nice h).smooth.comp (contDiff_prod_mk_right 1)).of_le
+    (mod_cast le_top)
   let 𝓕' : JetSec E F :=
     { f := fun x ↦ 𝓕.f x + corrugation L.π N (L.loop h 1) x
       f_diff := 𝓕.f_diff.add (corrugation.contDiff' _ _ (L.loop_smooth h) contDiff_id contDiff_const)
@@ -361,7 +363,7 @@ theorem improveStep_part_hol {N : ℝ} (hN : N ≠ 0) :
     intro x hx
     simp [𝓕', improveStep_apply h, hx]
   have fderiv_𝓕' := fun x ↦
-    fderiv_corrugated_map N hN γ_C1 (𝓕.f_diff.of_le le_top) L.p ((L.nice h).avg x)
+    fderiv_corrugated_map N hN γ_C1 (𝓕.f_diff.of_le (mod_cast le_top)) L.p ((L.nice h).avg x)
   rw [eventually_congr (H.isPartHolonomicAt_congr (L.p.spanV ⊔ L.E'))]
   apply h.hK₀.mono
   intro x hx
@@ -370,20 +372,21 @@ theorem improveStep_part_hol {N : ℝ} (hN : N ≠ 0) :
     rcases Submodule.mem_span_singleton.mp hu with ⟨l, rfl⟩
     rw [(D 𝓕'.f x).map_smul, (𝓕'.φ x).map_smul]
     apply congr_arg
-    unfold_let 𝓕'
+    unfold 𝓕'
     erw [fderiv_𝓕', ContinuousLinearMap.add_apply, L.p.update_v, ContinuousLinearMap.add_apply,
          L.p.update_v]
     rfl
   · intro u hu
     have hu_ker := L.hEp hu
-    unfold_let 𝓕'
+    unfold 𝓕'
     erw [fderiv_𝓕', ContinuousLinearMap.add_apply, L.p.update_ker_pi _ _ hu_ker,
       ContinuousLinearMap.add_apply, L.p.update_ker_pi _ _ hu_ker, hx u hu]
 
 theorem improveStep_formalSol : ∀ᶠ N in atTop, ∀ t, (L.improveStep h N t).IsFormalSol R := by
   set γ := L.loop h
   have γ_cont : Continuous ↿fun t x ↦ γ t x := (L.nice h).smooth.continuous
-  have γ_C1 : 𝒞 1 ↿(γ 1) := ((L.nice h).smooth.comp (contDiff_prod_mk_right 1)).of_le le_top
+  have γ_C1 : 𝒞 1 ↿(γ 1) := ((L.nice h).smooth.comp (contDiff_prod_mk_right 1)).of_le
+    (mod_cast le_top)
   set K :=
     (fun p : E × ℝ × ℝ ↦ (p.1, 𝓕.f p.1, L.p.update (𝓕.φ p.1) (L.loop h p.2.1 p.1 p.2.2))) ''
       L.K₁ ×ˢ I ×ˢ I
@@ -401,25 +404,25 @@ theorem improveStep_formalSol : ∀ᶠ N in atTop, ∀ t, (L.improveStep h N t).
   apply
     ((corrugation.c0_small_on _ L.hK₁ (L.nice h).t_le_zero (L.nice h).t_ge_one γ_cont ε_pos).and <|
         remainder_c0_small_on L.π L.hK₁ γ_C1 ε_pos).mono
-  rintro N ⟨H, H'⟩ t x
-  by_cases hxK₁ : x ∈ L.K₁
-  · apply hε
-    rw [Metric.mem_thickening_iff]
-    refine ⟨(x, 𝓕.f x, L.p.update (𝓕.φ x) <| L.loop h (smoothStep t * L.ρ x) x <| N * L.π x), ?_, ?_⟩
-    · exact ⟨⟨x, smoothStep t * L.ρ x, Int.fract (N * L.π x)⟩,
-        ⟨hxK₁, unitInterval.mul_mem (smoothStep.mem t) (L.ρ_mem x), unitInterval.fract_mem _⟩,
-         by simp only [Loop.fract_eq]⟩
-    · simp only [h, improveStep_apply_f, FormalSol.toJetSec_eq_coe, improveStep_apply_φ]
-      rw [Prod.dist_eq, max_lt_iff, Prod.dist_eq, max_lt_iff]
-      refine ⟨by simpa using ε_pos, ?_, ?_⟩ <;> dsimp only <;> rw [dist_self_add_left]
-      · exact bu_lt _ _ <| H _ hxK₁ _
-      -- adaptation note(2024-03-28): `exact` used to work; started failing after mathlib bump
-      · apply bu_lt _ _ <| H' _ hxK₁
-  · rw [show ((L.improveStep h N) t).f x = 𝓕.f x from
-        congr_arg Prod.fst <| improveStep_rel_compl_K₁ h N hxK₁ t,
-      show ((L.improveStep h N) t).φ x = 𝓕.φ x from
-        congr_arg Prod.snd <| improveStep_rel_compl_K₁ h N hxK₁ t]
-    exact 𝓕.is_sol _
+  · rintro N ⟨H, H'⟩ t x
+    by_cases hxK₁ : x ∈ L.K₁
+    · apply hε
+      rw [Metric.mem_thickening_iff]
+      refine ⟨(x, 𝓕.f x, L.p.update (𝓕.φ x) <| L.loop h (smoothStep t * L.ρ x) x <| N * L.π x), ?_, ?_⟩
+      · exact ⟨⟨x, smoothStep t * L.ρ x, Int.fract (N * L.π x)⟩,
+          ⟨hxK₁, unitInterval.mul_mem (smoothStep.mem t) (L.ρ_mem x), unitInterval.fract_mem _⟩,
+          by simp only [Loop.fract_eq]⟩
+      · simp only [h, improveStep_apply_f, FormalSol.toJetSec_eq_coe, improveStep_apply_φ]
+        rw [Prod.dist_eq, max_lt_iff, Prod.dist_eq, max_lt_iff]
+        refine ⟨by simpa using ε_pos, ?_, ?_⟩ <;> dsimp only <;> rw [dist_self_add_left]
+        · exact bu_lt _ _ <| H _ hxK₁ _
+        -- adaptation note(2024-03-28): `exact` used to work; started failing after mathlib bump
+        · apply bu_lt _ _ <| H' _ hxK₁
+    · rw [show ((L.improveStep h N) t).f x = 𝓕.f x from
+          congr_arg Prod.fst <| improveStep_rel_compl_K₁ h N hxK₁ t,
+        show ((L.improveStep h N) t).φ x = 𝓕.φ x from
+          congr_arg Prod.snd <| improveStep_rel_compl_K₁ h N hxK₁ t]
+      exact 𝓕.is_sol _
 
 end StepLandscape
 
@@ -506,13 +509,13 @@ theorem RelLoc.FormalSol.improve (𝓕 : FormalSol R) (h_hol : ∀ᶠ x near L.C
       rfl
     refine ⟨H.comp (S.improveStep acc N) glue, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
     · apply (H.comp_le_0 _ _).mono
-      intro t ht
-      rw [ht]
-      exact hH₀.self_of_nhdsSet 0 right_mem_Iic
+      · intro t ht
+        rw [ht]
+        exact hH₀.self_of_nhdsSet 0 right_mem_Iic
     -- t = 0
     · apply (H.comp_ge_1 _ _).mono
-      intro t ht
-      rw [ht, H.comp_1]
+      · intro t ht
+        rw [ht, H.comp_1]
     · -- rel C
       apply (hHC.and <| hH₁_rel_C.and <| improveStep_rel_C acc N).mono
       rintro x ⟨hx, hx', hx''⟩ t

diff --git a/SphereEversion/Local/ParametricHPrinciple.lean b/SphereEversion/Local/ParametricHPrinciple.lean
@@ -132,7 +132,7 @@ def FamilyJetSec.uncurry (S : FamilyJetSec E F P) : JetSec (P × E) F where
   φ p := fderiv ℝ (fun z : P × E ↦ S.f z.1 p.2) p + S.φ p.1 p.2 ∘L fderiv ℝ Prod.snd p
   f_diff := S.f_diff
   φ_diff := by
-    refine (ContDiff.fderiv ?_ contDiff_id le_top).add (S.φ_diff.clm_comp ?_)
+    refine (ContDiff.fderiv ?_ contDiff_id (m := ∞) le_rfl).add (S.φ_diff.clm_comp ?_)
     · exact S.f_diff.comp (contDiff_snd.fst.prod contDiff_fst.snd)
     · exact ContDiff.fderiv contDiff_snd.snd contDiff_id le_top
 
@@ -141,8 +141,8 @@ theorem FamilyJetSec.uncurry_φ' (S : FamilyJetSec E F P) (p : P × E) :
       fderiv ℝ (fun z ↦ S.f z p.2) p.1 ∘L ContinuousLinearMap.fst ℝ 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.prod contDiff_const)).differentiable le_top p.1)
-    differentiableAt_fst).trans ?_
+  refine (fderiv_comp p ((S.f_diff.comp (contDiff_id.prod contDiff_const)).differentiable
+    (mod_cast le_top) p.1) differentiableAt_fst).trans ?_
   rw [fderiv_fst]
   rfl
 
@@ -165,9 +165,10 @@ 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]
-  simp_rw [fderiv_prod_eq_add (S.f_diff.differentiable le_top _), fderiv_snd]
+  rw [fderiv_prod_eq_add (S.f_diff.differentiable (mod_cast le_top) _), fderiv_snd]
   refine (add_right_inj _).trans ?_
-  have := fderiv.comp p ((S p.1).f_diff.contDiffAt.differentiableAt le_top) differentiableAt_snd
+  have := fderiv_comp p ((S p.1).f_diff.contDiffAt.differentiableAt (mod_cast le_top))
+    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]
@@ -191,9 +192,10 @@ theorem RelLoc.FamilyFormalSol.uncurry_φ' (S : R.FamilyFormalSol P) (p : P × E
 def FamilyJetSec.curry (S : FamilyJetSec (P × E) F G) : FamilyJetSec E F (G × P) where
   f p x := (S p.1).f (p.2, x)
   φ p x := (S p.1).φ (p.2, x) ∘L fderiv ℝ (fun x ↦ (p.2, x)) x
-  f_diff := S.f_diff.comp (contDiff_prodAssoc : ContDiff ℝ ⊤ (Equiv.prodAssoc G P E))
+  f_diff := S.f_diff.comp ((contDiff_prodAssoc : ContDiff ℝ ⊤ (Equiv.prodAssoc G P E)).of_le le_top)
   φ_diff := by
-    refine (S.φ_diff.comp (contDiff_prodAssoc : ContDiff ℝ ⊤ (Equiv.prodAssoc G P E))).clm_comp ?_
+    refine (S.φ_diff.comp
+      ((contDiff_prodAssoc : ContDiff ℝ ⊤ (Equiv.prodAssoc G P E)).of_le le_top)).clm_comp ?_
     refine ContDiff.fderiv ?_ contDiff_snd le_top
     exact contDiff_fst.fst.snd.prod contDiff_snd
 
@@ -217,7 +219,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 le_top)
+  refine (fderiv_comp x ((S t).f_diff.contDiffAt.differentiableAt (mod_cast le_top))
     ((differentiableAt_const _).prod differentiableAt_id)).trans ?_
   rw [_root_.id, hS]
   rfl

diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean
@@ -146,7 +146,7 @@ theorem loc_immersion_rel_open : IsOpen (immersionSphereRel E F) := by
     have : ∀ᶠ p : OneJet E F in 𝓝 (x₀, y₀, φ₀), P (f p) := loc_immersion_rel_open_aux hx₀ H
     apply this.mono; clear this
     rintro ⟨x, y, φ⟩ ⟨hxx₀ : ⟪x₀, x⟫ ≠ 0, Hφ⟩ _
-    unfold_let P f at Hφ
+    unfold P f at Hφ
     change InjOn φ (ℝ ∙ x)ᗮ
     have : range (subtypeL (ℝ ∙ x)ᗮ ∘ pr[x]ᗮ ∘ j₀) = (ℝ ∙ x)ᗮ := by
       rw [Function.Surjective.range_comp]
@@ -262,8 +262,9 @@ local notation "∞" => (⊤ : ℕ∞)
 
 variable [Fact (dim E = 3)] [FiniteDimensional ℝ E] (ω : Orientation ℝ E (Fin 3))
 
-theorem smooth_at_locFormalEversionAuxφ {p : ℝ × E} (hx : p.2 ≠ 0) :
-    ContDiffAt ℝ ∞ (uncurry (locFormalEversionAuxφ ω)) p := by
+theorem smooth_at_locFormalEversionAuxφ {p : ℝ × E} (hx : p.2 ≠ 0) {n : WithTop ℕ∞} :
+    ContDiffAt ℝ n (uncurry (locFormalEversionAuxφ ω)) p := by
+  apply ContDiffAt.of_le _ le_top
   refine (ω.contDiff_rot hx).sub ?_
   refine ContDiffAt.smul (contDiffAt_const.mul contDiffAt_fst) ?_
   exact (contDiffAt_orthogonalProjection_singleton hx).comp p contDiffAt_snd
@@ -434,7 +435,7 @@ theorem sphere_eversion_of_loc [Fact (dim E = 3)] :
 -- Stating the full statement with all type-class arguments and no uncommon notation.
 example (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] :
     ∃ f : ℝ → E → E,
-      ContDiff ℝ ⊤ (uncurry f) ∧
+      ContDiff ℝ ∞ (uncurry f) ∧
         (∀ x ∈ sphere (0 : E) 1, f 0 x = x) ∧
           (∀ x ∈ sphere (0 : E) 1, f 1 x = -x) ∧ ∀ t ∈ unitInterval, SphereImmersion (f t) :=
   sphere_eversion_of_loc