From ad2add5823c39e03d314cbb940bd1799f40ea6c5 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Mon, 1 Jun 2026 15:39:43 +0200
Subject: [PATCH 1/3] chore: use elaborators more

---
 SphereEversion/Global/OneJetBundle.lean    | 37 ++++++++++------------
 SphereEversion/Global/OneJetSec.lean       |  8 ++---
 SphereEversion/Global/SmoothEmbedding.lean |  6 ++--
 3 files changed, 23 insertions(+), 28 deletions(-)

diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean
index 80eabca1..51f911cd 100644
--- a/SphereEversion/Global/OneJetBundle.lean
+++ b/SphereEversion/Global/OneJetBundle.lean
@@ -337,12 +337,12 @@ theorem contMDiff_oneJetBundle_proj :
 
 theorem ContMDiff.oneJetBundle_proj {f : N → J¹MM'}
     (hf : ContMDiff J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ f) :
-    ContMDiff J (I.prod I') ∞ fun x ↦ (f x).1 :=
+    CMDiff ∞ fun x ↦ (f x).1 :=
   contMDiff_oneJetBundle_proj.comp hf
 
 theorem ContMDiffAt.oneJetBundle_proj {f : N → J¹MM'} {x₀ : N}
     (hf : ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ f x₀) :
-    ContMDiffAt J (I.prod I') ∞ (fun x ↦ (f x).1) x₀ :=
+    CMDiffAt ∞ (fun x ↦ (f x).1) x₀ :=
   (contMDiff_oneJetBundle_proj _).comp x₀ hf
 
 /-- The constructor of `OneJetBundle`, in case `Sigma.mk` will not give the right type. -/
@@ -365,11 +365,10 @@ theorem oneJetBundle_mk_snd {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} :
 set_option backward.isDefEq.respectTransparency false in
 theorem contMDiffAt_oneJetBundle {f : N → J¹MM'} {x₀ : N} :
     ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ f x₀ ↔
-      CMDiffAt ∞ (fun x ↦ (f x).1.1) x₀ ∧
-        CMDiffAt ∞ (fun x ↦ (f x).1.2) x₀ ∧
-          ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') ∞
-            (inTangentCoordinates I I' (fun x ↦ (f x).1.1) (fun x ↦ (f x).1.2) (fun x ↦ (f x).2)
-              x₀) x₀ := by
+      CMDiffAt ∞ (fun x ↦ (f x).1.1) x₀ ∧ CMDiffAt ∞ (fun x ↦ (f x).1.2) x₀ ∧
+        CMDiffAt ∞
+          (inTangentCoordinates I I' (fun x ↦ (f x).1.1) (fun x ↦ (f x).1.2) (fun x ↦ (f x).2) x₀)
+          x₀ := by
   simp_rw [Bundle.contMDiffAt_totalSpace, contMDiffAt_prod_iff, and_assoc,
     oneJetBundle_trivializationAt]
   rfl
@@ -383,7 +382,7 @@ theorem contMDiffAt_oneJetBundle_mk {f : N → M} {g : N → M'} {ϕ : N → E 
 
 theorem ContMDiffAt.oneJetBundle_mk {f : N → M} {g : N → M'} {ϕ : N → E →L[𝕜] E'} {x₀ : N}
     (hf : CMDiffAt ∞ f x₀) (hg : CMDiffAt ∞ g x₀)
-    (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') ∞ (inTangentCoordinates I I' f g ϕ x₀) x₀) :
+    (hϕ : CMDiffAt ∞ (inTangentCoordinates I I' f g ϕ x₀) x₀) :
     ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞
       (fun x ↦ OneJetBundle.mk (f x) (g x) (ϕ x) : N → J¹MM') x₀ :=
   contMDiffAt_oneJetBundle.mpr ⟨hf, hg, hϕ⟩
@@ -421,9 +420,9 @@ theorem ContinuousAt.inTangentCoordinates_comp {f : N → M} {g : N → M'} {h :
 
 theorem ContMDiffAt.clm_comp_inTangentCoordinates {f : N → M} {g : N → M'} {h : N → N'}
     {ϕ' : N → E' →L[𝕜] F'} {ϕ : N → E →L[𝕜] E'} {n : N} (hg : ContinuousAt g n)
-    (hϕ' : ContMDiffAt J 𝓘(𝕜, E' →L[𝕜] F') ∞ (inTangentCoordinates I' J' g h ϕ' n) n)
-    (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') ∞ (inTangentCoordinates I I' f g ϕ n) n) :
-    ContMDiffAt J 𝓘(𝕜, E →L[𝕜] F') ∞ (inTangentCoordinates I J' f h (fun n ↦ ϕ' n ∘L ϕ n) n) n :=
+    (hϕ' : CMDiffAt ∞ (inTangentCoordinates I' J' g h ϕ' n) n)
+    (hϕ : CMDiffAt ∞ (inTangentCoordinates I I' f g ϕ n) n) :
+    CMDiffAt ∞ (inTangentCoordinates I J' f h (fun n ↦ ϕ' n ∘L ϕ n) n) n :=
   (hϕ'.clm_comp hϕ).congr_of_eventuallyEq hg.inTangentCoordinates_comp
 
 variable (I')
@@ -518,13 +517,11 @@ theorem OneJetBundle.map_id (x : J¹MM') :
 
 theorem ContMDiffAt.oneJetBundle_map {f : M'' → M → N} {g : M'' → M' → N'} {x₀ : M''}
     {Dfinv : ∀ (z : M'') (x : M), TangentSpace% (f z x) →L[𝕜] TangentSpace% x} {k : M'' → J¹MM'}
-    (hf : ContMDiffAt (I''.prod I) J ∞ f.uncurry (x₀, (k x₀).1.1))
-    (hg : ContMDiffAt (I''.prod I') J' ∞ g.uncurry (x₀, (k x₀).1.2))
+    (hf : CMDiffAt ∞ f.uncurry (x₀, (k x₀).1.1))
+    (hg : CMDiffAt ∞ g.uncurry (x₀, (k x₀).1.2))
     (hDfinv :
-      ContMDiffAt I'' 𝓘(𝕜, F →L[𝕜] E) ∞
-        (inTangentCoordinates J I (fun x ↦ f x (k x).1.1) (fun x ↦ (k x).1.1)
-          (fun x ↦ Dfinv x (k x).1.1) x₀)
-        x₀)
+      CMDiffAt ∞ (inTangentCoordinates J I (fun x ↦ f x (k x).1.1) (fun x ↦ (k x).1.1)
+        (fun x ↦ Dfinv x (k x).1.1) x₀) x₀)
     (hk : ContMDiffAt I'' ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ k x₀) :
     ContMDiffAt I'' ((J.prod J').prod 𝓘(𝕜, F →L[𝕜] F')) ∞
       (fun z ↦ OneJetBundle.map I' J' (f z) (g z) (Dfinv z) (k z)) x₀ := by
@@ -532,7 +529,7 @@ theorem ContMDiffAt.oneJetBundle_map {f : M'' → M → N} {g : M'' → M' → N
   refine ContMDiffAt.oneJet_comp _ _ ?_ ?_
   · refine ContMDiffAt.oneJet_comp _ _ ?_ ?_
     · refine hk.2.1.oneJetBundle_mk (hg.comp x₀ (contMDiffAt_id.prodMk hk.2.1)) ?_
-      exact ContMDiffAt.mfderiv g (fun x ↦ (k x).1.2) hg hk.2.1 le_rfl
+      exact hg.mfderiv g (fun x ↦ (k x).1.2) hk.2.1 le_rfl
     · exact hk.1.oneJetBundle_mk hk.2.1 hk.2.2
   apply (hf.comp x₀ (contMDiffAt_id.prodMk hk.1)).oneJetBundle_mk hk.1
   apply hDfinv
@@ -554,9 +551,9 @@ theorem mapLeft_eq_map (f : M → N) (Dfinv : ∀ x : M, TangentSpace% (f x) →
 
 theorem ContMDiffAt.mapLeft {f : N' → M → N} {x₀ : N'}
     {Dfinv : ∀ (z : N') (x : M), TangentSpace% (f z x) →L[𝕜] TangentSpace% x} {g : N' → J¹MM'}
-    (hf : ContMDiffAt (J'.prod I) J ∞ f.uncurry (x₀, (g x₀).1.1))
+    (hf : CMDiffAt ∞ f.uncurry (x₀, (g x₀).1.1))
     (hDfinv :
-      ContMDiffAt J' 𝓘(𝕜, F →L[𝕜] E) ∞
+      CMDiffAt ∞
         (inTangentCoordinates J I (fun x ↦ f x (g x).1.1) (fun x ↦ (g x).1.1)
           (fun x ↦ Dfinv x (g x).1.1) x₀)
         x₀)
diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean
index 6e73c25e..892d0fae 100644
--- a/SphereEversion/Global/OneJetSec.lean
+++ b/SphereEversion/Global/OneJetSec.lean
@@ -224,7 +224,7 @@ protected theorem contMDiff (S : FamilyOneJetSec I M I' M' J N) :
   S.contMDiff'
 
 theorem contMDiff_bs (S : FamilyOneJetSec I M I' M' J N) :
-    ContMDiff (J.prod I) I' ∞ fun p : N × M ↦ S.bs p.1 p.2 :=
+    CMDiff ∞ fun p : N × M ↦ S.bs p.1 p.2 :=
   contMDiff_oneJetBundle_proj.snd.comp S.contMDiff
 
 theorem contMDiff_coe_bs (S : FamilyOneJetSec I M I' M' J N) {p : N} : CMDiff ∞ (S.bs p) :=
@@ -244,14 +244,12 @@ def reindex (S : FamilyOneJetSec I M I' M' J' N') (f : C^∞⟮J, N; J', N'⟯)
 def uncurry (S : FamilyOneJetSec I M I' M' IP P) : OneJetSec (IP.prod I) (P × M) I' M' where
   bs p := S.bs p.1 p.2
   ϕ p :=
-    (mfderiv (IP.prod I) I' (fun z : P × M ↦ S.bs z.1 p.2) p) +
-      S.ϕ p.1 p.2 ∘L mfderiv (IP.prod I) I Prod.snd p
+    (mfderiv% (fun z : P × M ↦ S.bs z.1 p.2) p) + S.ϕ p.1 p.2 ∘L mfderiv (IP.prod I) I Prod.snd p
   contMDiff' := by
     refine ContMDiff.oneJet_add ?_ ?_
     · intro y
       refine contMDiffAt_id.oneJetBundle_mk (S.contMDiff_bs y) ?_
-      have : ContMDiffAt ((IP.prod I).prod (IP.prod I)) I' ∞
-          (Function.uncurry fun x z : P × M ↦ S.bs z.1 x.2) (y, y) :=
+      have : CMDiffAt ∞ (Function.uncurry fun x z : P × M ↦ S.bs z.1 x.2) (y, y) :=
         S.contMDiff_bs.comp (contMDiff_snd.fst.prodMk contMDiff_fst.snd) (y, y)
       apply ContMDiffAt.mfderiv (fun x z : P × M ↦ S.bs z.1 x.2) id this contMDiffAt_id
         (mod_cast le_top)
diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean
index 1bdbb8a8..8062257f 100644
--- a/SphereEversion/Global/SmoothEmbedding.lean
+++ b/SphereEversion/Global/SmoothEmbedding.lean
@@ -86,7 +86,7 @@ variable [IsManifold I ∞ M] [IsManifold I' ∞ M']
 
 /- Note that we are slightly abusing the fact that `TangentSpace I x` and
 `TangentSpace I (f.invFun (f x))` are both definitionally `E` below. -/
-def fderiv (x : M) : TangentSpace% x ≃L[𝕜] TangentSpace% (f x) :=
+def fderiv (x : M) : TangentSpace I x ≃L[𝕜] TangentSpace I' (f x) :=
   have h₁ : MDiffAt f.invFun (f x) :=
     ((f.contMDiffOn_inv (f x)
     (mem_range_self x)).mdifferentiableWithinAt (by simp)).mdifferentiableAt
@@ -419,8 +419,8 @@ open Function
 
 /-- This is lemma `lem:smooth_updating` in the blueprint. -/
 theorem contMDiff_update (f : M' → M → N) (g : M' → X → Y) {k : M' → M} {K : Set X}
-    (hK : IsClosed (φ '' K)) (hf : ContMDiff (IM'.prod IM) IN ∞ (uncurry f))
-    (hg : ContMDiff (IM'.prod IX) IY ∞ (uncurry g)) (hk : CMDiff ∞ k)
+    (hK : IsClosed (φ '' K)) (hf : CMDiff ∞ (uncurry f))
+    (hg : CMDiff ∞ (uncurry g)) (hk : CMDiff ∞ k)
     (hg' : ∀ y x, x ∉ K → f y (φ x) = ψ (g y x)) :
     CMDiff ∞ fun x ↦ update φ ψ (f x) (g x) (k x) := by
   have hK' : ∀ x, k x ∉ φ '' K → update φ ψ (f x) (g x) (k x) = f x (k x) := fun x hx ↦

From 0150d4a53a999d24574ecf90730a232a8e44e000 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Sun, 26 Oct 2025 21:53:29 +0100
Subject: [PATCH 2/3] ExistsOfConvex: remove last use of local notation The new
 elaborators are similarly short

---
 SphereEversion/ToMathlib/ExistsOfConvex.lean | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean
index eeb90b53..9113be1b 100644
--- a/SphereEversion/ToMathlib/ExistsOfConvex.lean
+++ b/SphereEversion/ToMathlib/ExistsOfConvex.lean
@@ -110,10 +110,6 @@ variable {H₁ M₁ H₂ M₂ : Type*}
   [TopologicalSpace H₂] (I₂ : ModelWithCorners ℝ E₂ H₂)
   [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [IsManifold I₂ ∞ M₂]
 
-@[inherit_doc] local notation "𝓒" => ContMDiff (I₁.prod I₂) 𝓘(ℝ, F)
-
-@[inherit_doc] local notation "𝓒_on" => ContMDiffOn (I₁.prod I₂) 𝓘(ℝ, F)
-
 omit [FiniteDimensional ℝ E₁] [FiniteDimensional ℝ E₂]
   [IsManifold I₁ ∞ M₁] [IsManifold I₂ ∞ M₂] in
 theorem reallyConvex_contMDiffAtProd {x : M₁} (n : ℕ∞) :
@@ -134,8 +130,8 @@ omit [FiniteDimensional ℝ E₂] [IsManifold I₂ ∞ M₂] in
 theorem exists_contMDiff_of_convex₂ {P : M₁ → (M₂ → F) → Prop} [SigmaCompactSpace M₁] [T2Space M₁]
     (hP : ∀ x, Convex ℝ {f | P x f}) {n : ℕ∞}
     (hP' : ∀ x : M₁, ∃ U ∈ 𝓝 x, ∃ f : M₁ → M₂ → F,
-      𝓒_on n (uncurry f) (U ×ˢ (univ : Set M₂)) ∧ ∀ y ∈ U, P y (f y)) :
-    ∃ f : M₁ → M₂ → F, 𝓒 n (uncurry f) ∧ ∀ x, P x (f x) := by
+      CMDiff[U ×ˢ (univ : Set M₂)] n (uncurry f) ∧ ∀ y ∈ U, P y (f y)) :
+    ∃ f : M₁ → M₂ → F, CMDiff n (uncurry f) ∧ ∀ x, P x (f x) := by
   let PP : (Σ x : M₁, Germ (𝓝 x) (M₂ → F)) → Prop := fun p ↦
     p.2.ContMDiffAtProd I₁ I₂ n ∧ P p.1 p.2.value
   have hPP : ∀ x : M₁, ReallyConvex (smoothGerm I₁ x) {φ | PP ⟨x, φ⟩} := fun x ↦ by

From 07940fe500b39833bb9e174227c430e3b579c47a Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Mon, 1 Jun 2026 15:55:55 +0200
Subject: [PATCH 3/3] Use more

---
 SphereEversion/Global/Gromov.lean             |  5 ++--
 SphereEversion/Global/Immersion.lean          | 24 +++++++++----------
 SphereEversion/Global/OneJetBundle.lean       |  3 +--
 .../Global/ParametricityForFree.lean          | 10 ++++----
 SphereEversion/Global/Relation.lean           |  4 ++--
 SphereEversion/Global/TwistOneJetSec.lean     | 15 ++++++------
 6 files changed, 28 insertions(+), 33 deletions(-)

diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean
index beeeaf67..67910282 100644
--- a/SphereEversion/Global/Gromov.lean
+++ b/SphereEversion/Global/Gromov.lean
@@ -68,9 +68,8 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R
     change ContMDiffAt _ _ _ (f ∘ fun p : ℝ × M ↦ (a * p.1 + b, p.2)) (t, x)
     change ContMDiffAt _ _ _ f ((fun p : ℝ × M ↦ (a * p.1 + b, p.2)) (t, x)) at h
     have :
-      ContMDiffAt (𝓘(ℝ, ℝ).prod IM) (𝓘(ℝ, ℝ).prod IM) ∞ (fun p : ℝ × M ↦ (a * p.1 + b, p.2))
-        (t, x) :=
-      haveI h₁ : ContMDiffAt 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) ∞ (fun t ↦ a * t + b) t :=
+      CMDiffAt ∞ (fun p : ℝ × M ↦ (a * p.1 + b, p.2)) (t, x) :=
+      haveI h₁ : CMDiffAt ∞ (fun t ↦ a * t + b) t :=
         contMDiffAt_iff_contDiffAt.mpr
           (((contDiffAt_id : ContDiffAt ℝ ∞ id t).const_smul a).add contDiffAt_const)
       h₁.prodMap contMDiffAt_id
diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean
index 2abc9f9d..29dbb9be 100644
--- a/SphereEversion/Global/Immersion.lean
+++ b/SphereEversion/Global/Immersion.lean
@@ -142,7 +142,7 @@ theorem immersion_antipodal_sphere : Immersion (𝓡 n) 𝓘(ℝ, E)
     -- The other direction elaborates much worse.
     (contDiff_neg.contMDiff).comp (contMDiff_coe_sphere.of_le le_top)
   diff_injective x := by
-    change Injective (mfderiv (𝓡 n) 𝓘(ℝ, E) (-fun x : sphere (0 : E) 1 ↦ (x : E)) x)
+    change Injective (mfderiv% (-fun x : sphere (0 : E) 1 ↦ (x : E)) x)
     rw [mfderiv_neg]
     exact neg_injective.comp (mfderiv_coe_sphere_injective x)
 
@@ -168,8 +168,7 @@ variable (ω : Orientation ℝ E (Fin 3))
 
 -- this result holds mutatis mutandis in `ℝ^n`
 theorem smooth_bs :
-    ContMDiff (𝓘(ℝ, ℝ).prod (𝓡 2)) 𝓘(ℝ, E) ∞
-      fun p : ℝ × (sphere (0 : E) 1) ↦ (1 - p.1) • (p.2 : E) + p.1 • -(p.2: E) := by
+    CMDiff ∞ fun p : ℝ × (sphere (0 : E) 1) ↦ (1 - p.1) • (p.2 : E) + p.1 • -(p.2: E) := by
   refine (ContMDiff.smul (I := 𝓘(ℝ)) ?_ ?_).add (contMDiff_fst.smul ?_)
   · exact (contDiff_const.sub contDiff_id).contMDiff.comp contMDiff_fst
   · exact (contMDiff_coe_sphere.of_le le_top).comp contMDiff_snd
@@ -181,6 +180,8 @@ def formalEversionAux : FamilyOneJetSec (𝓡 2) 𝕊² 𝓘(ℝ, E) E 𝓘(ℝ,
       (fun p : ℝ × 𝕊² ↦ ω.rot (p.1, p.2))
       (by
         intro p
+        -- Note: elaborators would infer another model on the domain, namely `𝓘(ℝ, ℝ).prod 𝓘(ℝ, E)`
+        -- In any case, this should not work, as we have a product of normed spaces?
         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
@@ -209,9 +210,9 @@ theorem formalEversionHolAtZero {t : ℝ} (ht : t < 1 / 4) :
     (formalEversion E ω t).toOneJetSec.IsHolonomic := by
   intro x
   change
-    mfderiv (𝓡 2) 𝓘(ℝ, E) (fun y : 𝕊² ↦ ((1 : ℝ) - smoothStep t) • (y : E) +
+    mfderiv% (fun y : 𝕊² ↦ ((1 : ℝ) - smoothStep t) • (y : E) +
       smoothStep t • -(y : E)) x =
-      (ω.rot (smoothStep t, x)).comp (mfderiv (𝓡 2) 𝓘(ℝ, E) (fun y : 𝕊² ↦ (y : E)) x)
+      (ω.rot (smoothStep t, x)).comp (mfderiv% (fun y : 𝕊² ↦ (y : E)) x)
   simp_rw [smoothStep.of_lt ht, ω.rot_zero, ContinuousLinearMap.id_comp]
   congr with y
   simp [smoothStep.of_lt ht]
@@ -221,10 +222,10 @@ theorem formalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) :
     (formalEversion E ω t).toOneJetSec.IsHolonomic := by
   intro x
   change
-    mfderiv (𝓡 2) 𝓘(ℝ, E) (fun y : 𝕊² ↦ ((1 : ℝ) - smoothStep t) • (y : E) +
+    mfderiv% (fun y : 𝕊² ↦ ((1 : ℝ) - smoothStep t) • (y : E) +
       smoothStep t • -(y : E)) x =
-      (ω.rot (smoothStep t, x)).comp (mfderiv (𝓡 2) 𝓘(ℝ, E) (fun y : 𝕊² ↦ (y : E)) x)
-  trans mfderiv (𝓡 2) 𝓘(ℝ, E) (-fun y : 𝕊² ↦ (y : E)) x
+      (ω.rot (smoothStep t, x)).comp (mfderiv% (fun y : 𝕊² ↦ (y : E)) x)
+  trans mfderiv% (-fun y : 𝕊² ↦ (y : E)) x
   · congr 2 with y
     simp [smoothStep.of_gt ht]
   ext v
@@ -285,13 +286,13 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 
 -- move to Mathlib.Geometry.Manifold.ContMDiff.Product
 lemma ContMDiff.prod_left {n : ℕ∞} (x : M) :
-    ContMDiff I' (I.prod I') n fun p : M' ↦ (⟨x, p⟩ : M × M') := by
+    CMDiff n fun p : M' ↦ (⟨x, p⟩ : M × M') := by
   rw [contMDiff_prod_iff]
   exact ⟨contMDiff_const, contMDiff_id⟩
 
 -- move to Mathlib.Geometry.Manifold.ContMDiff.Product
 theorem ContMDiff.uncurry_left {n : ℕ∞} {f : M → M' → P}
-    (hf : ContMDiff (I.prod I') IP n ↿f) (x : M) : CMDiff n (f x) := by
+    (hf : CMDiff n ↿f) (x : M) : CMDiff n (f x) := by
   have : f x = (uncurry f) ∘ fun p : M' ↦ ⟨x, p⟩ := by ext; simp
   -- or just `apply hf.comp (ContMDiff.prod_left I I' x)`
   rw [this]; exact hf.comp (ContMDiff.prod_left I I' x)
@@ -300,8 +301,7 @@ end helper
 
 theorem sphere_eversion :
     ∃ f : ℝ → 𝕊² → E,
-      ContMDiff (𝓘(ℝ, ℝ).prod (𝓡 2)) 𝓘(ℝ, E) ∞ ↿f ∧
-        (f 0 = fun x : 𝕊² ↦ (x : E)) ∧ (f 1 = fun x : 𝕊² ↦ -(x : E)) ∧
+      CMDiff ∞ ↿f ∧ (f 0 = fun x : 𝕊² ↦ (x : E)) ∧ (f 1 = fun x : 𝕊² ↦ -(x : E)) ∧
         ∀ t, Immersion (𝓡 2) 𝓘(ℝ, E) (f t) ∞ := by
   classical
   let ω : Orientation ℝ E (Fin 3) :=
diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean
index 51f911cd..651331d0 100644
--- a/SphereEversion/Global/OneJetBundle.lean
+++ b/SphereEversion/Global/OneJetBundle.lean
@@ -376,8 +376,7 @@ theorem contMDiffAt_oneJetBundle {f : N → J¹MM'} {x₀ : N} :
 theorem contMDiffAt_oneJetBundle_mk {f : N → M} {g : N → M'} {ϕ : N → E →L[𝕜] E'} {x₀ : N} :
     ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞
         (fun x ↦ OneJetBundle.mk (f x) (g x) (ϕ x) : N → J¹MM') x₀ ↔
-      CMDiffAt ∞ f x₀ ∧ CMDiffAt ∞ g x₀ ∧
-        ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') ∞ (inTangentCoordinates I I' f g ϕ x₀) x₀ :=
+      CMDiffAt ∞ f x₀ ∧ CMDiffAt ∞ g x₀ ∧ CMDiffAt ∞ (inTangentCoordinates I I' f g ϕ x₀) x₀ :=
   contMDiffAt_oneJetBundle
 
 theorem ContMDiffAt.oneJetBundle_mk {f : N → M} {g : N → M'} {ϕ : N → E →L[𝕜] E'} {x₀ : N}
diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean
index d125dff7..65fa455d 100644
--- a/SphereEversion/Global/ParametricityForFree.lean
+++ b/SphereEversion/Global/ParametricityForFree.lean
@@ -156,7 +156,7 @@ def FamilyFormalSol.uncurry (S : FamilyFormalSol IP P R) : FormalSol (R.relativi
 
 theorem FamilyFormalSol.uncurry_ϕ' (S : FamilyFormalSol IP P R) (p : P × M) :
     S.uncurry.ϕ p =
-      mfderiv IP I' (fun z ↦ S.bs z p.2) p.1 ∘L ContinuousLinearMap.fst ℝ EP E +
+      mfderiv% (fun z ↦ S.bs z p.2) p.1 ∘L ContinuousLinearMap.fst ℝ EP E +
         S.ϕ p.1 p.2 ∘L ContinuousLinearMap.snd ℝ EP E :=
   S.toFamilyOneJetSec.uncurry_ϕ' p
 
@@ -169,17 +169,15 @@ def FamilyOneJetSec.curry (S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N) :
     rintro ⟨⟨t, s⟩, x⟩
     refine contMDiffAt_snd.oneJetBundle_mk (S.contMDiff_bs.comp contMDiff_prod_assoc _) ?_
     have h1 :
-      ContMDiffAt ((J.prod IP).prod I) 𝓘(ℝ, EP × E →L[ℝ] E') ∞
-        (inTangentCoordinates (IP.prod I) I' (fun p : (N × P) × M ↦ (p.1.2, p.2))
+      CMDiffAt ∞ (inTangentCoordinates (IP.prod I) I' (fun p : (N × P) × M ↦ (p.1.2, p.2))
           (fun p : (N × P) × M ↦ (S p.1.1).bs (p.1.2, p.2))
           (fun p : (N × P) × M ↦ (S p.1.1).ϕ (p.1.2, p.2)) ((t, s), x))
         ((t, s), x) := by
       apply (contMDiffAt_oneJetBundle.mp <|
         (S.contMDiff (t, (s, x))).comp ((t, s), x) (contMDiff_prod_assoc ((t, s), x))).2.2
     have h2 :
-      ContMDiffAt ((J.prod IP).prod I) 𝓘(ℝ, E →L[ℝ] EP × E) ∞
-        (inTangentCoordinates I (IP.prod I) Prod.snd (fun p : (N × P) × M ↦ (p.1.2, p.2))
-          (fun p : (N × P) × M ↦ mfderiv I (IP.prod I) (fun x : M ↦ (p.1.2, x)) p.2) ((t, s), x))
+      CMDiffAt ∞ (inTangentCoordinates I (IP.prod I) Prod.snd (fun p : (N × P) × M ↦ (p.1.2, p.2))
+          (fun p : (N × P) × M ↦ mfderiv% (fun x : M ↦ (p.1.2, x)) p.2) ((t, s), x))
         ((t, s), x) := by
       apply
         ContMDiffAt.mfderiv (fun (p : (N × P) × M) (x : M) ↦ (p.1.2, x)) Prod.snd
diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean
index 1438ed24..1b68ffe7 100644
--- a/SphereEversion/Global/Relation.lean
+++ b/SphereEversion/Global/Relation.lean
@@ -385,13 +385,13 @@ theorem RelMfld.SatisfiesHPrincipleWith.bs {R : RelMfld I M IX X} {C : Set (P ×
     (h : R.SatisfiesHPrincipleWith IP C ε) (𝓕₀ : FamilyFormalSol IP P R)
     (h2 : ∀ᶠ p : P × M near C, (𝓕₀ p.1).toOneJetSec.IsHolonomicAt p.2) :
     ∃ f : P → M → X,
-      (ContMDiff (IP.prod I) IX ∞ <| uncurry f) ∧
+      (CMDiff ∞ (uncurry f)) ∧
         (∀ᶠ p : P × M near C, f p.1 p.2 = 𝓕₀.bs p.1 p.2) ∧
           (∀ p m, dist (f p m) ((𝓕₀ p).bs m) ≤ ε m) ∧ ∀ p m, oneJetExt I IX (f p) m ∈ R := by
   rcases h 𝓕₀ h2 with ⟨𝓕, _, h₂, h₃, h₄⟩
   refine ⟨fun s ↦ (𝓕 (1, s)).bs, ?_, ?_, ?_, ?_⟩
   · let j : C^∞⟮IP, P; 𝓘(ℝ, ℝ).prod IP, ℝ × P⟯ :=
-      ⟨fun p ↦ (1, p), ContMDiff.prodMk contMDiff_const contMDiff_id⟩
+      ⟨fun p ↦ (1, p), contMDiff_const.prodMk contMDiff_id⟩
     rw [show
         (uncurry fun s ↦ (𝓕 (1, s)).bs) =
           Prod.snd ∘ π _ (OneJetSpace I IX) ∘ fun p : P × M ↦ 𝓕.reindex j p.1 p.2
diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean
index 6a82186c..542e9ea7 100644
--- a/SphereEversion/Global/TwistOneJetSec.lean
+++ b/SphereEversion/Global/TwistOneJetSec.lean
@@ -33,7 +33,7 @@ variable {f : N → J¹[𝕜, E, I, M, V]}
 -- todo: remove or use to prove `contMDiff_one_jet_eucl_bundle`
 theorem contMDiffAt_one_jet_eucl_bundle' {x₀ : N} :
     ContMDiffAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞ f x₀ ↔ CMDiffAt ∞ (fun x  ↦ (f x).1) x₀ ∧
-    ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ∞ (fun x  ↦ show E →L[𝕜] V from
+    CMDiffAt ∞ (fun x  ↦ show E →L[𝕜] V from
       (f x).2 ∘L (trivializationAt E (TangentSpace I : M → _) (f x₀).1).symmL 𝕜 (f x).1) x₀ := by
   simp_rw [contMDiffAt_hom_bundle, inCoordinates, Trivial.trivializationAt,
     Trivial.trivialization_continuousLinearMapAt]
@@ -43,7 +43,7 @@ theorem contMDiffAt_one_jet_eucl_bundle' {x₀ : N} :
 theorem contMDiffAt_one_jet_eucl_bundle {x₀ : N} :
     ContMDiffAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞ f x₀ ↔
       CMDiffAt ∞ (fun x  ↦ (f x).1) x₀ ∧
-        ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ∞ (fun x  ↦ show E →L[𝕜] V from
+        CMDiffAt ∞ (fun x  ↦ show E →L[𝕜] V from
           (f x).2 ∘L (trivializationAt E (TangentSpace I) (f x₀).proj).symmL 𝕜 (f x).proj) x₀ := by
   rw [contMDiffAt_hom_bundle, and_congr_right_iff]
   intro hf
@@ -60,7 +60,7 @@ theorem contMDiffAt_one_jet_eucl_bundle {x₀ : N} :
 
 theorem ContMDiffAt.one_jet_eucl_bundle_mk' {f : N → M} {ϕ : N → E →L[𝕜] V} {x₀ : N}
     (hf : CMDiffAt ∞ f x₀)
-    (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ∞ (fun x ↦ show E →L[𝕜] V from
+    (hϕ : CMDiffAt ∞ (fun x ↦ show E →L[𝕜] V from
             ϕ x ∘L (trivializationAt E (TangentSpace I : M → _) (f x₀)).symmL 𝕜 (f x)) x₀) :
     ContMDiffAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞
       (fun x ↦ Bundle.TotalSpace.mk (f x) (ϕ x) : N → J¹[𝕜, E, I, M, V]) x₀ :=
@@ -68,7 +68,7 @@ theorem ContMDiffAt.one_jet_eucl_bundle_mk' {f : N → M} {ϕ : N → E →L[
 
 theorem ContMDiffAt.one_jet_eucl_bundle_mk {f : N → M} {ϕ : N → E →L[𝕜] V} {x₀ : N}
     (hf : CMDiffAt ∞ f x₀)
-    (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ∞ (fun x ↦ show E →L[𝕜] V from
+    (hϕ : CMDiffAt ∞ (fun x ↦ show E →L[𝕜] V from
       ϕ x ∘L (trivializationAt E (TangentSpace I) (f x₀)).symmL 𝕜 (f x)) x₀) :
     ContMDiffAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞
       (fun x ↦ Bundle.TotalSpace.mk (f x) (ϕ x) : N → J¹[𝕜, E, I, M, V]) x₀ :=
@@ -208,7 +208,7 @@ theorem FamilyOneJetEuclSec.contMDiff (s : FamilyOneJetEuclSec I M V J N) :
 
 variable {V'}
 
-def familyJoin {f : N × M → V} (hf : ContMDiff (J.prod I) 𝓘(ℝ, V) ∞ f)
+def familyJoin {f : N × M → V} (hf : CMDiff ∞ f)
     (s : FamilyOneJetEuclSec I M V J N) : FamilyOneJetSec I M 𝓘(ℝ, V) V J N
     where
   bs n m := (incl I M V (s (n, m), f (n, m))).1.2
@@ -219,9 +219,8 @@ def familyJoin {f : N × M → V} (hf : ContMDiff (J.prod I) 𝓘(ℝ, V) ∞ f)
 
 set_option backward.isDefEq.respectTransparency false in
 def familyTwist (s : OneJetEuclSec I M V) (i : N × M → V →L[ℝ] V')
-    (hi : ∀ x₀ : N × M, ContMDiffAt (J.prod I) 𝓘(ℝ, V →L[ℝ] V') ∞ i x₀) :
-    FamilyOneJetEuclSec I M V' J N
-    where
+    (hi : ∀ x₀ : N × M, CMDiffAt ∞ i x₀) :
+    FamilyOneJetEuclSec I M V' J N where
   toFun p := ⟨p.2, (i p).comp (s p.2).2⟩
   is_sec' p := rfl
   contMDiff' := by