From 912bbcfd0e4096bcad7541b7ffa289294e5ffdf1 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Mon, 18 Mar 2024 12:29:37 +0100
Subject: [PATCH] Rename Immersion.differentiable to contMDiff.

---
 SphereEversion/Global/Immersion.lean                      | 6 +++---
 SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean
index d8e9c505..f6e33ec4 100644
--- a/SphereEversion/Global/Immersion.lean
+++ b/SphereEversion/Global/Immersion.lean
@@ -122,13 +122,13 @@ variable {n : ℕ} (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E]
 /-- The inclusion of `𝕊^n` into `ℝ^{n+1}` is an immersion. -/
 theorem immersion_inclusion_sphere : Immersion (𝓡 n) 𝓘(ℝ, E)
     (fun x : sphere (0 : E) 1 ↦ (x : E)) ⊤ where
-  differentiable := contMDiff_coe_sphere
+  contMDiff := contMDiff_coe_sphere
   diff_injective := mfderiv_coe_sphere_injective
 
 /-- The antipodal map on `𝕊^n ⊆ ℝ^{n+1}` is an immersion. -/
 theorem immersion_antipodal_sphere : Immersion (𝓡 n) 𝓘(ℝ, E)
     (fun x : sphere (0 : E) 1 ↦ -(x : E)) ⊤ where
-  differentiable :=
+  contMDiff :=
     -- Write this as the composition of `coe_sphere` and the antipodal map on `E`.
     -- The other direction elaborates much worse.
     (contDiff_neg.contMDiff).comp contMDiff_coe_sphere
@@ -334,7 +334,7 @@ theorem sphere_eversion :
     rw [this (1, x) (by simp)]
     convert formalEversion_one E ω x
   · exact fun t ↦ {
-      differentiable := Smooth.uncurry_left 𝓘(ℝ, ℝ) (𝓡 2) 𝓘(ℝ, E) h₁ t
+      contMDiff := Smooth.uncurry_left 𝓘(ℝ, ℝ) (𝓡 2) 𝓘(ℝ, E) h₁ t
       diff_injective := h₅ t
     }
 
diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean
index 5903f531..b7b4d8b2 100644
--- a/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean
+++ b/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean
@@ -53,7 +53,7 @@ section Definition
 
 /-- A `C^n` immersion `f : M → M` is a `C^n` map whose differential is injective at every point. -/
 structure Immersion (f : M → M') (n : ℕ∞) : Prop :=
-  differentiable : ContMDiff I I' n f
+  contMDiff : ContMDiff I I' n f
   diff_injective : ∀ p, Injective (mfderiv I I' f p)
 
 /-- An injective `C^n` immersion -/