store

SphereEversion/Global/Localisation.lean

@@ -93,19 +93,19 @@ def HtpyJetSec.unloc (𝓕 : HtpyJetSec E E') : HtpyOneJetSec 𝓘(ℝ, E) E 
   ϕ t x := (𝓕 t x).2
   smooth' := by
     intro a
-    refine contMDiffAt_oneJetBundle.mpr ⟨contMDiffAt_snd,
-      sorry, -- TODO-MR: fix proof, was: (𝓕.f_diff.contMDiff (a.fst, a.snd)).comp a (contMDiffAt_fst.prod_mk_space contMDiffAt_snd),
-      ?_⟩
-    -- TODO: Investigate why we need so many different tactics before the exact
-    unfold inTangentCoordinates
-    dsimp [inCoordinates, chartAt]
-    simp  [range_id, fderivWithin_univ, fderiv_id, TangentBundle.symmL_model_space,
-      TangentBundle.continuousLinearMapAt_model_space, ContinuousLinearMap.one_def,
-      ContinuousLinearMap.comp_id]
-    dsimp only [TangentSpace]
-    simp_rw [ContinuousLinearMap.id_comp]
-    sorry -- TODO-MR: fix proof, was:
-    -- exact (𝓕.φ_diff.contMDiff (a.fst, a.snd)).comp a (contMDiffAt_fst.prod_mk_space contMDiffAt_snd)
+    refine contMDiffAt_oneJetBundle.mpr ⟨contMDiffAt_snd, ?_, ?_⟩
+    · apply (𝓕.f_diff.contMDiff (a.fst, a.snd)).comp a
+        (contMDiffAt_fst.prod_mk_space contMDiffAt_snd)
+    · -- TODO: Investigate why we need so many different tactics before the apply
+      unfold inTangentCoordinates
+      dsimp [inCoordinates, chartAt]
+      simp only [TangentBundle.trivializationAt_baseSet, PartialHomeomorph.refl_partialEquiv,
+        PartialEquiv.refl_source, PartialHomeomorph.singletonChartedSpace_chartAt_eq, mem_univ,
+        VectorBundleCore.trivializationAt_continuousLinearMapAt, tangentBundleCore_indexAt,
+        TangentBundle.coordChange_model_space, one_def, VectorBundleCore.trivializationAt_symmL,
+        comp_id]
+      apply (𝓕.φ_diff.contMDiff (a.fst, a.snd)).comp a
+        (contMDiffAt_fst.prod_mk_space contMDiffAt_snd)
 
 end Unloc
 

SphereEversion/Global/OneJetSec.lean

@@ -257,21 +257,21 @@ theorem uncurry_ϕ' (S : FamilyOneJetSec I M I' M' IP P) (p : P × M) :
         S.ϕ p.1 p.2 ∘L ContinuousLinearMap.snd ℝ EP E := by
   simp_rw [S.uncurry_ϕ, mfderiv_snd]
   congr 1
-  sorry /-- TODO-MR
   convert
-    mfderiv_comp p ((S.smooth_bs.comp (contMDiff_id.prod_mk contMDiff_const)).mdifferentiable (by simp) p.1)
-      (contMDiff_fst.mdifferentiable (sorry) p)
+    mfderiv_comp p ((S.smooth_bs.comp (contMDiff_id.prod_mk contMDiff_const)).mdifferentiable
+      (by simp) p.1) (contMDiff_fst.mdifferentiable le_top p)
   simp_rw [mfderiv_fst]
-  rfl -/
+  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]
-  sorry /- TODO-MR simp_rw [mfderiv_prod_eq_add (S.smooth_bs.mdifferentiable _), mfderiv_snd, add_right_inj]
-  erw [mfderiv_comp p S.smooth_coe_bs.mdifferentiableAt contMDiff_snd.mdifferentiableAt, mfderiv_snd]
+  simp_rw [mfderiv_prod_eq_add (S.smooth_bs.mdifferentiableAt le_top), mfderiv_snd, add_right_inj]
+  erw [mfderiv_comp p (S.smooth_coe_bs.mdifferentiableAt le_top)
+    (contMDiff_snd.mdifferentiableAt le_top), mfderiv_snd]
   exact (show Surjective (ContinuousLinearMap.snd ℝ EP E) from
-    Prod.snd_surjective).clm_comp_injective.eq_iff -/
+    Prod.snd_surjective).clm_comp_injective.eq_iff
 
 end FamilyOneJetSec
 

SphereEversion/Global/Relation.lean

@@ -618,31 +618,29 @@ def OneJetBundle.embedding : OpenSmoothEmbedding IXY J¹XY IMN J¹MN where
     OneJetBundle.map IN IY φ.invFun ψ.invFun fun x ↦
       (φ.fderiv <| φ.invFun x : TX (φ.invFun x) →L[ℝ] TM (φ <| φ.invFun x))
   left_inv' {σ} := by
-    sorry /- TODO-MR: fix proof, was:
-    rw [OpenSmoothEmbedding.transfer,
-      OneJetBundle.map_map (ψ.contMDiffAt_inv'.mdifferentiableAt (by simp))
-        ψ.contMDiff_to.contMDiffAt.mdifferentiableAt (le_top)]
+    rw [OpenSmoothEmbedding.transfer, OneJetBundle.map_map]; rotate_left
+    · exact (ψ.contMDiffAt_inv'.mdifferentiableAt (by simp))
+    · exact ψ.contMDiff_to.contMDiffAt.mdifferentiableAt (le_top)
     conv_rhs => rw [← OneJetBundle.map_id σ]
     congr 1
     · rw [OpenSmoothEmbedding.invFun_comp_coe]
     · rw [OpenSmoothEmbedding.invFun_comp_coe]
     · ext x v; simp_rw [ContinuousLinearMap.comp_apply]
       convert (φ.fderiv x).symm_apply_apply v
-      erw [φ.left_inv]; rfl -/
+      erw [φ.left_inv]; rfl
   isOpen_range := φ.isOpen_range_transfer ψ
   contMDiff_to := φ.smooth_transfer ψ
   contMDiffOn_inv := by
     rintro _ ⟨x, rfl⟩
-    sorry /- TODO-MR: fix proof, was
-    refine (ContMDiffAt.oneJetBundle_map ?_ ?_ ?_ contMDiffAt_id).smoothWithinAt
-    · refine (φ.smoothAt_inv ?_).comp (φ.transfer ψ x, (φ.transfer ψ x).proj.1) smoothAt_snd
+    refine (ContMDiffAt.oneJetBundle_map ?_ ?_ ?_ contMDiffAt_id).contMDiffWithinAt
+    · refine (φ.contMDiffAt_inv ?_).comp (φ.transfer ψ x, (φ.transfer ψ x).proj.1) contMDiffAt_snd
       exact mem_range_self _
-    · refine (ψ.smoothAt_inv ?_).comp (φ.transfer ψ x, (φ.transfer ψ x).proj.2) smoothAt_snd
+    · refine (ψ.contMDiffAt_inv ?_).comp (φ.transfer ψ x, (φ.transfer ψ x).proj.2) contMDiffAt_snd
       exact mem_range_self _
     have' :=
       ContMDiffAt.mfderiv (fun _ ↦ φ) (fun x : OneJetBundle IM M IN N ↦ φ.invFun x.1.1)
-        (φ.contMDiff_to.smoothAt.comp _ smoothAt_snd)
-        ((φ.contMDiffAt_to_inv _).comp _ (smooth_oneJetBundle_proj.fst (φ.transfer ψ x))) le_top
+        (φ.contMDiff_to.contMDiffAt.comp _ contMDiffAt_snd)
+        ((φ.contMDiffAt_inv _).comp _ (contMDiff_oneJetBundle_proj.fst (φ.transfer ψ x))) le_top
     · dsimp only [id]
       refine this.congr_of_eventuallyEq ?_
       refine Filter.eventually_of_mem ((φ.isOpen_range_transfer ψ).mem_nhds (mem_range_self _)) ?_
@@ -652,7 +650,7 @@ def OneJetBundle.embedding : OpenSmoothEmbedding IXY J¹XY IMN J¹MN where
       simp_rw [φ.transfer_proj_fst, φ.left_inv]
       congr 1
       simp_rw [φ.left_inv]
-    exact mem_range_self _ -/
+    exact mem_range_self _
 
 
 /-! ## Updating 1-jet sections and formal solutions -/

SphereEversion/Local/Corrugation.lean

@@ -186,20 +186,20 @@ theorem fderiv_corrugated_map (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ) {f : E 
   simp_rw [ContinuousLinearMap.add_apply, corrugation.fderiv_apply _ N hN hγ_diff, hfγ,
     DualPair.update, ContinuousLinearMap.add_apply, p.π.comp_toSpanSingleton_apply, add_assoc]
 
-local notation "∞" => (⊤ : ℕ∞)
+open scoped ContDiff
 
 theorem Remainder.smooth {γ : G → E → Loop F} (hγ_diff : 𝒞 ∞ ↿γ) {x : H → E} (hx : 𝒞 ∞ x)
-    {g : H → G} (hg : 𝒞 ⊤ g) : 𝒞 ∞ fun h ↦ R N (γ <| g h) <| x h := by
+    {g : H → G} (hg : 𝒞 ∞ g) : 𝒞 ∞ fun h ↦ R N (γ <| g h) <| x h := by
   apply ContDiff.const_smul
   apply contDiff_parametric_primitive_of_contDiff
   · let ψ : E → H × ℝ → F := fun x q ↦ (γ (g q.1) x).normalize q.2
     change  𝒞 ∞ fun q : H × ℝ ↦ ∂₁ ψ (x q.1) (q.1, q.2)
     refine (ContDiff.contDiff_top_partial_fst ?_).comp₂ hx.fst' (contDiff_fst.prod contDiff_snd)
     dsimp [Loop.normalize]
     apply ContDiff.sub
-    · sorry -- TODO-MR fix, was: apply hγ_diff.comp₃ hg.fst'.snd' contDiff_fst contDiff_snd.snd
-    · sorry -- TODO-MR fix, was: apply contDiff_average
-      -- exact hγ_diff.comp₃ hg.fst'.snd'.fst' contDiff_fst.fst' contDiff_snd
+    · apply hγ_diff.comp₃ hg.fst'.snd' contDiff_fst contDiff_snd.snd
+    · apply contDiff_average
+      exact hγ_diff.comp₃ hg.fst'.snd'.fst' contDiff_fst.fst' contDiff_snd
   · exact contDiff_const.mul (π.contDiff.comp hx)
 
 set_option linter.style.multiGoal false in

SphereEversion/Loops/Reparametrization.lean

@@ -48,7 +48,7 @@ existence of delta mollifiers, partitions of unity, and the inverse function the
 noncomputable section
 
 open Set Function MeasureTheory Module intervalIntegral Filter
-open scoped Topology Manifold
+open scoped Topology Manifold ContDiff
 
 variable {E F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 
@@ -89,9 +89,9 @@ variable [NormedAddCommGroup E] [NormedSpace ℝ E]
 /-- Given a smooth function `g : E → F` between normed vector spaces, a smooth surrounding family
 is a smooth family of loops `E → loop F`, `x ↦ γₓ` such that `γₓ` surrounds `g x` for all `x`. -/
 structure SmoothSurroundingFamily (g : E → F) where
-  smooth_surrounded : 𝒞 ⊤ g
+  smooth_surrounded : 𝒞 ∞ g
   toFun : E → Loop F
-  smooth : 𝒞 ⊤ ↿toFun
+  smooth : 𝒞 ∞ ↿toFun
   Surrounds : ∀ x, (toFun x).Surrounds <| g x
 
 namespace SmoothSurroundingFamily
@@ -132,12 +132,12 @@ def approxSurroundingPointsAt (n : ℕ) (i : ι) : F :=
 
 variable [FiniteDimensional ℝ E] [CompleteSpace F] in
 theorem approxSurroundingPointsAt_smooth (n : ℕ) :
-    𝒞 ⊤ fun y ↦ γ.approxSurroundingPointsAt x y n := by
+    𝒞 ∞ fun y ↦ γ.approxSurroundingPointsAt x y n := by
   refine contDiff_pi.mpr fun i ↦ ?_
-  suffices 𝒞 ⊤ fun y ↦ ∫ s in (0 : ℝ)..1, deltaMollifier n (γ.surroundingParametersAt x i) s • γ y s by simpa [approxSurroundingPointsAt, Loop.mollify]
-  sorry /- TODO-MR: fix proof, was:
+  suffices 𝒞 ∞ fun y ↦ ∫ s in (0 : ℝ)..1, deltaMollifier n (γ.surroundingParametersAt x i) s • γ y s
+    by simpa [approxSurroundingPointsAt, Loop.mollify]
   apply contDiff_parametric_integral_of_contDiff
-  exact ContDiff.smul deltaMollifier_smooth.snd' γ.smooth -/
+  exact ContDiff.smul deltaMollifier_smooth.snd' (γ.smooth.of_le le_top)
 
 variable [FiniteDimensional ℝ F]
 
@@ -264,19 +264,19 @@ theorem localCenteringDensity_smooth_on :
     let z : E → F × (ι → F) :=
       (Prod.map g fun y ↦ γ.approxSurroundingPointsAt x y (γ.localCenteringDensityMp x)) ∘
         fun x ↦ (x, x)
-    change ContDiffOn ℝ ⊤ ((w ∘ z) ∘ Prod.fst) (γ.localCenteringDensityNhd x ×ˢ (univ : Set ℝ))
+    change ContDiffOn ℝ ∞ ((w ∘ z) ∘ Prod.fst) (γ.localCenteringDensityNhd x ×ˢ (univ : Set ℝ))
     rw [prod_univ]
     refine ContDiffOn.comp ?_ contDiff_fst.contDiffOn Subset.rfl
-    have h₁ := smooth_barycentric ι ℝ F (Fintype.card_fin _)
-    have h₂ : 𝒞 ⊤ (eval i : (ι → ℝ) → ℝ) := contDiff_apply _ _ i
+    have h₁ := smooth_barycentric ι ℝ F (Fintype.card_fin _) (n := ∞)
+    have h₂ : 𝒞 ∞ (eval i : (ι → ℝ) → ℝ) := contDiff_apply _ _ i
     refine (h₂.comp_contDiffOn h₁).comp ?_ ?_
     · have h₃ := (diag_preimage_prod_self (γ.localCenteringDensityNhd x)).symm.subset
       refine ContDiffOn.comp ?_ (contDiff_id.prod contDiff_id).contDiffOn h₃
       refine γ.smooth_surrounded.contDiffOn.prod_map (ContDiff.contDiffOn ?_)
       exact γ.approxSurroundingPointsAt_smooth x _
     · intro y hy
       simp [z, γ.approxSurroundingPointsAt_mem_affineBases x y hy]
-  · sorry -- TODO-MR: fix proof, was: exact deltaMollifier_smooth.comp contDiff_snd
+  · exact deltaMollifier_smooth.comp contDiff_snd
 
 variable [FiniteDimensional ℝ E] in
 theorem localCenteringDensity_continuous (hy : y ∈ γ.localCenteringDensityNhd x) :
@@ -386,7 +386,7 @@ def centeringDensity : E → ℝ → ℝ :=
   Classical.choose
     (exists_contDiff_of_convex₂ γ.isCenteringDensity_convex γ.exists_smooth_isCenteringDensity)
 
-theorem centeringDensity_smooth : 𝒞 ⊤ <| uncurry fun x t ↦ γ.centeringDensity x t :=
+theorem centeringDensity_smooth : 𝒞 ∞ <| uncurry fun x t ↦ γ.centeringDensity x t :=
   (Classical.choose_spec <|
       exists_contDiff_of_convex₂ γ.isCenteringDensity_convex γ.exists_smooth_isCenteringDensity).1
 
@@ -466,12 +466,11 @@ theorem hasDerivAt_reparametrize_symm (s : ℝ) :
     (γ.centeringDensity_continuous x).continuousAt
 
 -- 𝒞 ∞ ↿γ.reparametrize
-theorem reparametrize_smooth : 𝒞 ⊤ <| uncurry fun (x : E) (t : ℝ) ↦ γ.reparametrize x t := by
+theorem reparametrize_smooth : 𝒞 ∞ <| uncurry fun (x : E) (t : ℝ) ↦ γ.reparametrize x t := by
   let f : E → ℝ → ℝ := fun x t ↦ ∫ s in (0)..t, γ.centeringDensity x s
-  change 𝒞 ⊤ fun p : E × ℝ ↦ (StrictMono.orderIsoOfSurjective (f p.1) _ _).symm p.2
+  change 𝒞 ∞ fun p : E × ℝ ↦ (StrictMono.orderIsoOfSurjective (f p.1) _ _).symm p.2
   apply contDiff_parametric_symm_of_deriv_pos
-  · sorry -- TODO-MR: fix, was (mismatch about ∞ vs ⊤)
-    -- exact contDiff_parametric_primitive_of_contDiff'' γ.centeringDensity_smooth 0
+  · exact contDiff_parametric_primitive_of_contDiff'' γ.centeringDensity_smooth 0
   · exact fun x ↦ deriv_integral_centeringDensity_pos γ x
   · exact fun x ↦ surjective_integral_centeringDensity γ x
 

SphereEversion/Loops/Surrounding.lean

@@ -208,7 +208,7 @@ theorem smooth_surrounding [FiniteDimensional ℝ F] {x : F} {p : ι → F} {w :
   have hι : Fintype.card ι = d + 1 := Fintype.card_fin _
   have hp : p ∈ affineBases ι ℝ F := h.mem_affineBases
   have hV : IsOpen V := isOpen_set_pi finite_univ fun _ _ ↦ isOpen_Ioi
-  have hW' : ContinuousOn W' A := (smooth_barycentric ι ℝ F hι).continuousOn
+  have hW' : ContinuousOn W' A := (smooth_barycentric ι ℝ F hι (n := 0)).continuousOn
   have hxp : W' (x, p) ∈ V := by simp [W', V, hp, h.coord_eq_w, h.w_pos]
   have hA : IsOpen A := by
     simp only [A, affineBases_findim ι ℝ F hι]
@@ -221,7 +221,7 @@ theorem smooth_surrounding [FiniteDimensional ℝ F] {x : F} {p : ι → F} {w :
   have hq : q ∈ affineBases ι ℝ F := by simpa [A] using inter_subset_left hyq
   have hyq' : (y, q) ∈ W' ⁻¹' V := inter_subset_right hyq
   refine ⟨⟨U, mem_nhds_iff.mpr ⟨U, le_refl U, hU₂, hyq⟩,
-    (smooth_barycentric ι ℝ F hι).mono inter_subset_left⟩, ?_, ?_, ?_⟩
+    ((smooth_barycentric ι ℝ F hι).mono inter_subset_left).of_le le_top⟩, ?_, ?_, ?_⟩
   · simpa [V] using hyq'
   · simp [hq]
   · simp [hq]; exact AffineBasis.linear_combination_coord_eq_self _ y
@@ -280,7 +280,7 @@ theorem eventually_surroundingPts_of_tendsto_of_tendsto {l : Filter X} {m : Filt
     simp only [A, affineBases_findim ι ℝ F hι]
     exact isOpen_univ.prod (isOpen_affineIndependent ℝ F)
   have hW' : ContinuousAt W' (q, v) :=
-    (smooth_barycentric ι ℝ F hι).continuousOn.continuousAt
+    (smooth_barycentric ι ℝ F hι (n := 0)).continuousOn.continuousAt
       (mem_nhds_iff.mpr ⟨A, Subset.rfl, hA, hqv⟩)
   have hS : S ∈ 𝓝 (q, v) := hW'.preimage_mem_nhds hV'
   obtain ⟨n₁, hn₁, n₂, hn₂, hS'⟩ := mem_nhds_prod_iff.mp hS
@@ -640,7 +640,6 @@ theorem local_loops [FiniteDimensional ℝ F] {x₀ : E} (hΩ_op : ∃ U ∈ 
     (hg : ContinuousAt g x₀) (hb : Continuous b)
     (hconv : g x₀ ∈ convexHull ℝ (connectedComponentIn (Prod.mk x₀ ⁻¹' Ω) <| b x₀)) :
     ∃ γ : E → ℝ → Loop F, ∃ U ∈ 𝓝 x₀, SurroundingFamilyIn g b γ U Ω := by
-  sorry /- TODO-MR fix proof, "stuck at solving universe constraint
   have hbx₀ : ContinuousAt b x₀ := hb.continuousAt
   have hΩ_op_x₀ : IsOpen (connectedComponentIn (Prod.mk x₀ ⁻¹' Ω) <| b x₀) :=
     (isOpen_slice_of_isOpen_over hΩ_op).connectedComponentIn
@@ -653,7 +652,7 @@ theorem local_loops [FiniteDimensional ℝ F] {x₀ : E} (hΩ_op : ∃ U ∈ 
   rcases surrounding_loop_of_convexHull hΩ_op_x₀ hΩ_conn hconv hb_in with
     ⟨γ, h1γ, h2γ, h3γ, h4γ, h5γ, h6γ⟩
   have h5γ : ∀ t s : ℝ, γ t s ∈ mk x₀ ⁻¹' Ω := fun t s ↦ connectedComponentIn_subset _ _ (h5γ t s)
-  let δ : E → ℝ → Loop F := fun x t ↦ b x - b x₀ +ᵥ γ t
+  let δ : E → ℝ → Loop F := fun x t ↦ (b x - b x₀) +ᵥ γ t
   have hδ : Continuous ↿δ := by
     dsimp only [δ, HasUncurry.uncurry, Loop.vadd_apply]
     exact (hb.fst'.sub continuous_const).add h1γ.snd'
@@ -688,7 +687,7 @@ theorem local_loops [FiniteDimensional ℝ F] {x₀ : E} (hΩ_op : ∃ U ∈ 
     filter_upwards [hc.tendsto.eventually hW]
     rintro x ⟨_, hx⟩
     exact ⟨_, _, hx⟩
-  exact ⟨δ, _, hδΩ.and hδsurr, ⟨⟨hδs0, hδt0, hδt1, fun x ↦ And.right, hδ⟩, fun x ↦ And.left⟩⟩ -/
+  exact ⟨δ, _, hδΩ.and hδsurr, ⟨⟨hδs0, hδt0, hδt1, fun x ↦ And.right, hδ⟩, fun x ↦ And.left⟩⟩
 
 /-- A tiny reformulation of `local_loops` where the existing `U` is open. -/
 theorem local_loops_open [FiniteDimensional ℝ F] {x₀ : E}

SphereEversion/Notations.lean

@@ -8,7 +8,7 @@ notation "hull" => convexHull ℝ
 
 notation "D" => fderiv ℝ
 
-notation "smooth_on" => ContDiffOn ℝ ⊤
+notation "smooth_on" => ContDiffOn ℝ (⊤ : ℕ∞)
 
 -- `∀ᶠ x near s, p x` means property `p` holds at every point in a neighborhood of the set `s`.
 notation3 (prettyPrint := false)

SphereEversion/ToMathlib/Analysis/ContDiff.lean

@@ -218,7 +218,7 @@ section
 variable (𝕜 : Type*) [NontriviallyNormedField 𝕜]
 
 theorem contDiff_toSpanSingleton (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
-    ContDiff 𝕜 ∞ (ContinuousLinearMap.toSpanSingleton 𝕜 : E → 𝕜 →L[𝕜] E) :=
+    ContDiff 𝕜 ω (ContinuousLinearMap.toSpanSingleton 𝕜 : E → 𝕜 →L[𝕜] E) :=
   (ContinuousLinearMap.lsmul 𝕜 𝕜 : 𝕜 →L[𝕜] E →L[𝕜] E).flip.contDiff
 
 end
@@ -244,10 +244,10 @@ section
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
 
 /-- The orthogonal projection onto a vector in a real inner product space `E`, considered as a map
-from `E` to `E →L[ℝ] E`, is smooth away from 0. -/
+from `E` to `E →L[ℝ] E`, is analytic away from 0. -/
 theorem contDiffAt_orthogonalProjection_singleton {v₀ : E} (hv₀ : v₀ ≠ 0) :
-    ContDiffAt ℝ ∞ (fun v : E ↦ (ℝ ∙ v).subtypeL.comp (orthogonalProjection (ℝ ∙ v))) v₀ := by
-  suffices ContDiffAt ℝ ∞
+    ContDiffAt ℝ ω (fun v : E ↦ (ℝ ∙ v).subtypeL.comp (orthogonalProjection (ℝ ∙ v))) v₀ := by
+  suffices ContDiffAt ℝ ω
     (fun v : E ↦ (1 / ‖v‖ ^ 2) • .toSpanSingleton ℝ v ∘L InnerProductSpace.toDual ℝ E v) v₀ by
     refine this.congr_of_eventuallyEq ?_
     filter_upwards with v

SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean

@@ -55,12 +55,11 @@ theorem rot_eq_aux : ω.rot = ω.rotAux := by
 /-- The map `rot` is smooth on `ℝ × (E \ {0})`. -/
 theorem contDiff_rot {p : ℝ × E} (hp : p.2 ≠ 0) : ContDiffAt ℝ ⊤ ω.rot p := by
   simp only [rot_eq_aux]
-  sorry /- TODO-MR: fix proof
   refine (contDiffAt_fst.mul_const.cos.smul contDiffAt_const).add ?_
   refine ((contDiffAt_const.sub contDiffAt_fst.mul_const.cos).smul ?_).add
     (contDiffAt_fst.mul_const.sin.smul ?_)
   · exact (contDiffAt_orthogonalProjection_singleton hp).comp _ contDiffAt_snd
-  · exact ω.crossProduct'.contDiff.contDiffAt.comp _ contDiffAt_snd -/
+  · exact ω.crossProduct'.contDiff.contDiffAt.comp _ contDiffAt_snd
 
 /-- The map `rot` sends `{0} × E` to the identity. -/
 theorem rot_zero (v : E) : ω.rot (0, v) = ContinuousLinearMap.id ℝ E := by