diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean
index f0b3af6e..d7dc7d77 100644
--- a/SphereEversion/Global/Gromov.lean
+++ b/SphereEversion/Global/Gromov.lean
@@ -67,10 +67,8 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R
     rintro a b ⟨t, x⟩ f h
     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 :=
+    have : 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 30c4c3ee..266501b0 100644
--- a/SphereEversion/Global/Immersion.lean
+++ b/SphereEversion/Global/Immersion.lean
@@ -286,14 +286,13 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {P : Type*} [TopologicalSpace P] [ChartedSpace HP P]
 
 -- 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
+lemma ContMDiff.prod_left {n : ℕ∞} (x : M) : 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)
diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean
index 5c9bda64..aa86ff70 100644
--- a/SphereEversion/Global/OneJetBundle.lean
+++ b/SphereEversion/Global/OneJetBundle.lean
@@ -331,12 +331,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. -/
@@ -360,9 +360,8 @@ 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 ∞ (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
@@ -370,13 +369,12 @@ 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}
     (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ϕ⟩
@@ -414,9 +412,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')
@@ -509,13 +507,10 @@ 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 J (f z x) →L[𝕜] TangentSpace I 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))
-    (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₀)
+    (hf : CMDiffAt ∞ f.uncurry (x₀, (k x₀).1.1))
+    (hg : CMDiffAt ∞ g.uncurry (x₀, (k x₀).1.2))
+    (hDfinv : 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
@@ -544,12 +539,9 @@ theorem mapLeft_eq_map (f : M → N) (Dfinv : ∀ x : M, TangentSpace J (f x) 
 
 theorem ContMDiffAt.mapLeft {f : N' → M → N} {x₀ : N'}
     {Dfinv : ∀ (z : N') (x : M), TangentSpace J (f z x) →L[𝕜] TangentSpace I x} {g : N' → J¹MM'}
-    (hf : ContMDiffAt (J'.prod I) J ∞ f.uncurry (x₀, (g x₀).1.1))
-    (hDfinv :
-      ContMDiffAt J' 𝓘(𝕜, F →L[𝕜] E) ∞
-        (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₀)
+    (hf : CMDiffAt ∞ f.uncurry (x₀, (g x₀).1.1))
+    (hDfinv : 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₀)
     (hg : ContMDiffAt J' ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ g x₀) :
     ContMDiffAt J' ((J.prod I').prod 𝓘(𝕜, F →L[𝕜] E')) ∞
       (fun z ↦ mapLeft (f z) (Dfinv z) (g z)) x₀ := by
diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean
index 66c9876e..2b098313 100644
--- a/SphereEversion/Global/OneJetSec.lean
+++ b/SphereEversion/Global/OneJetSec.lean
@@ -222,7 +222,7 @@ protected theorem smooth (S : FamilyOneJetSec I M I' M' J N) :
   S.smooth'
 
 theorem smooth_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.smooth
 
 theorem smooth_coe_bs (S : FamilyOneJetSec I M I' M' J N) {p : N} : CMDiff ∞ (S.bs p) :=
diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean
index 66513de0..e9c4e727 100644
--- a/SphereEversion/Global/ParametricityForFree.lean
+++ b/SphereEversion/Global/ParametricityForFree.lean
@@ -171,16 +171,13 @@ def FamilyOneJetSec.curry (S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N) :
   smooth' := by
     rintro ⟨⟨t, s⟩, x⟩
     refine contMDiffAt_snd.oneJetBundle_mk (S.smooth_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))
+    have h1 : 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 <|
         ContMDiffAt.comp ((t, s), x) (S.smooth (t, (s, x))) (contMDiff_prod_assoc ((t, s), x))).2.2
-    have h2 :
-      ContMDiffAt ((J.prod IP).prod I) 𝓘(ℝ, E →L[ℝ] EP × E) ∞
+    have h2 : CMDiffAt ∞
         (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))
         ((t, s), x) := by
diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean
index 3e8b9d66..77803387 100644
--- a/SphereEversion/Global/Relation.lean
+++ b/SphereEversion/Global/Relation.lean
@@ -383,10 +383,9 @@ family of formal solutions. -/
 theorem RelMfld.SatisfiesHPrincipleWith.bs {R : RelMfld I M IX X} {C : Set (P × M)} {ε : M → ℝ}
     (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) ∧
-        (∀ᶠ 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
+    ∃ f : P → M → X, (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⟯ :=
diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean
index d455f2bb..73f73f53 100644
--- a/SphereEversion/Global/SmoothEmbedding.lean
+++ b/SphereEversion/Global/SmoothEmbedding.lean
@@ -424,8 +424,8 @@ open Function
 
 /-- This is lemma `lem:smooth_updating` in the blueprint. -/
 theorem smooth_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 ↦
diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean
index f67ea804..02d53c36 100644
--- a/SphereEversion/Global/TwistOneJetSec.lean
+++ b/SphereEversion/Global/TwistOneJetSec.lean
@@ -35,7 +35,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]
@@ -45,7 +45,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
@@ -62,7 +62,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₀ :=
@@ -70,7 +70,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₀ :=
@@ -218,9 +218,8 @@ def familyJoin {f : N × M → V} (hf : ContMDiff (J.prod I) 𝓘(ℝ, V) ∞ f)
     ext : 1 <;> simp
 
 def familyTwist (s : OneJetEuclSec I M V) (i : N × M → V →L[ℝ] V')
-    (i_smooth : ∀ x₀ : N × M, ContMDiffAt (J.prod I) 𝓘(ℝ, V →L[ℝ] V') ∞ i x₀) :
-    FamilyOneJetEuclSec I M V' J N
-    where
+    (i_smooth : ∀ 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
   smooth' := by
diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean
index 810df115..a1468f22 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 : ℕ∞) :
@@ -135,8 +131,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
diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/MiscManifold.lean b/SphereEversion/ToMathlib/Geometry/Manifold/MiscManifold.lean
index 9f35ccee..ad44a3ae 100644
--- a/SphereEversion/ToMathlib/Geometry/Manifold/MiscManifold.lean
+++ b/SphereEversion/ToMathlib/Geometry/Manifold/MiscManifold.lean
@@ -31,23 +31,19 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {e : OpenPartialHomeomorph M H} {f : M → M'} {m n : WithTop ℕ∞} {s : Set M} {x x' : M}
 
 theorem contMDiff_prod {f : M → M' × N'} :
-    ContMDiff I (I'.prod J') n f ↔
-      (CMDiff n fun x ↦ (f x).1) ∧ CMDiff n fun x ↦ (f x).2 :=
+    CMDiff n f ↔ (CMDiff n fun x ↦ (f x).1) ∧ CMDiff n fun x ↦ (f x).2 :=
   ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩
 
 theorem contMDiffAt_prod {f : M → M' × N'} {x : M} :
-    ContMDiffAt I (I'.prod J') n f x ↔
-      CMDiffAt n (fun x ↦ (f x).1) x ∧ CMDiffAt n (fun x ↦ (f x).2) x :=
+    CMDiffAt n f x ↔ CMDiffAt n (fun x ↦ (f x).1) x ∧ CMDiffAt n (fun x ↦ (f x).2) x :=
   ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩
 
 theorem smooth_prod {f : M → M' × N'} :
-    ContMDiff I (I'.prod J') ∞ f ↔
-      (CMDiff ∞ fun x ↦ (f x).1) ∧ CMDiff ∞ fun x ↦ (f x).2 :=
+    CMDiff ∞ f ↔ (CMDiff ∞ fun x ↦ (f x).1) ∧ CMDiff ∞ fun x ↦ (f x).2 :=
   contMDiff_prod
 
 theorem smoothAt_prod {f : M → M' × N'} {x : M} :
-    ContMDiffAt I (I'.prod J') ∞ f x ↔
-      CMDiffAt ∞ (fun x ↦ (f x).1) x ∧ CMDiffAt ∞ (fun x ↦ (f x).2) x :=
+    CMDiffAt ∞ f x ↔ CMDiffAt ∞ (fun x ↦ (f x).1) x ∧ CMDiffAt ∞ (fun x ↦ (f x).2) x :=
   contMDiffAt_prod
 
 end IsManifold
diff --git a/lake-manifest.json b/lake-manifest.json
index 8d0aa48c..632cc44c 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -11,21 +11,21 @@
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
+  {"url": "https://github.com/grunweg/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "7c64d37d340c4fad44f930c9da90d2dae284bb8b",
+   "scope": "",
+   "rev": "d4a0bdb55c93112e3bdea8e86864379701317dbd",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "diffgeo-use-custom-elaborators",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b949552f6ca8e223f424b3e3b33f74185bbf1179",
+   "rev": "8864a73bf79aad549e34eff972c606343935106d",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d768126816be17600904726ca7976b185786e6b9",
+   "rev": "451499ea6e97cee4c8979b507a9af5581a849161",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "556caed0eadb7901e068131d1be208dd907d07a2",
+   "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.74",
+   "inputRev": "v0.0.77",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
+   "rev": "1fa48c6a63b4c4cda28be61e1037192776e77ac0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2676cb5599c12c434daac781e2cea44e8105fc41",
+   "rev": "95c2f8afe09d9e49d3cacca667261da04f7f93f7",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
+   "rev": "c44068fa1b40041e6df42bd67639b690eb2764ca",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
+   "rev": "72ae7004d9f0ddb422aec5378204fdd7828c5672",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.25.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "SphereEversion",
diff --git a/lakefile.toml b/lakefile.toml
index ba83c495..c289967f 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -9,7 +9,8 @@ linter.mathlibStandardSet = true
 
 [[require]]
 name = "mathlib"
-scope = "leanprover-community"
+git = "https://github.com/grunweg/mathlib4.git"
+rev = "diffgeo-use-custom-elaborators"
 
 [[require]]
 name = "checkdecls"
diff --git a/lean-toolchain b/lean-toolchain
index 58ae2451..137937a3 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.24.0
\ No newline at end of file
+leanprover/lean4:v4.25.0-rc2
\ No newline at end of file