diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean
index c4b71d71..2abc9f9d 100644
--- a/SphereEversion/Global/Immersion.lean
+++ b/SphereEversion/Global/Immersion.lean
@@ -72,8 +72,8 @@ theorem immersionRel_open [FiniteDimensional ℝ E] : IsOpen (immersionRel I M I
 
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 @[simp]
-theorem immersionRel_slice_eq {m : M} {m' : M'} {p : DualPair <| TangentSpace I m}
-    {φ : TangentSpace I m →L[ℝ] TangentSpace I' m'} (hφ : Injective φ) :
+theorem immersionRel_slice_eq {m : M} {m' : M'} {p : DualPair <| TangentSpace% m}
+    {φ : TangentSpace% m →L[ℝ] TangentSpace% m'} (hφ : Injective φ) :
     (immersionRel I M I' M').slice ⟨(m, m'), φ⟩ p =
       (((p.π.ker).map (φ : TM m →ₛₗ[.id ℝ] TM' m')): Set <| TM' m')ᶜ :=
   Set.ext_iff.mpr fun _ ↦ p.injective_update_iff hφ
@@ -83,9 +83,9 @@ variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ E']
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 theorem immersionRel_ample (h : finrank ℝ E < finrank ℝ E') : (immersionRel I M I' M').Ample := by
   rw [RelMfld.ample_iff]
-  rintro ⟨⟨m, m'⟩, φ : TangentSpace I m →L[ℝ] TangentSpace I' m'⟩ (p : DualPair (TangentSpace I m))
+  rintro ⟨⟨m, m'⟩, φ : TangentSpace% m →L[ℝ] TangentSpace% m'⟩ (p : DualPair (TangentSpace% m))
     (hφ : Injective φ)
-  haveI : FiniteDimensional ℝ (TangentSpace I m) := (by infer_instance : FiniteDimensional ℝ E)
+  haveI : FiniteDimensional ℝ (TangentSpace% m) := (by infer_instance : FiniteDimensional ℝ E)
   have hcodim := one_lt_rank_of_rank_lt_rank p.ker_pi_ne_top h φ.toLinearMap
   rw [immersionRel_slice_eq I I' hφ]
   exact AmpleSet.of_one_lt_codim hcodim
diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean
index 7b505202..80eabca1 100644
--- a/SphereEversion/Global/OneJetBundle.lean
+++ b/SphereEversion/Global/OneJetBundle.lean
@@ -109,7 +109,7 @@ local notation "FJ¹MM'" => (OneJetSpace I I' : M × M' → Type _)
 
 variable (I I')
 
-instance (p : M × M') : FunLike (OneJetSpace I I' p) (TangentSpace I p.1) (TangentSpace I' p.2)
+instance (p : M × M') : FunLike (OneJetSpace I I' p) (TangentSpace% p.1) (TangentSpace% p.2)
 where
   coe := fun φ ↦ φ.toFun
   coe_injective := fun _ _ h ↦ ContinuousLinearMap.ext (congrFun h)
@@ -480,7 +480,7 @@ variable (I' J')
 
 /-- A useful definition to define maps between two `OneJetBundle`s. -/
 protected def OneJetBundle.map (f : M → N) (g : M' → N')
-    (Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] TangentSpace I x) :
+    (Dfinv : ∀ x : M, TangentSpace% (f x) →L[𝕜] TangentSpace% x) :
     OneJetBundle I M I' M' → OneJetBundle J N J' N' := fun p ↦
   OneJetBundle.mk (f p.1.1) (g p.1.2) ((mfderiv% g p.1.2 ∘L p.2) ∘L Dfinv p.1.1)
 
@@ -491,9 +491,9 @@ omit [IsManifold I ∞ M] [IsManifold I' ∞ M']
   [IsManifold I₂ ∞ M₂] [IsManifold I₃ ∞ M₃]
   [IsManifold J' ∞ N'] [IsManifold J ∞ N] in
 theorem OneJetBundle.map_map {f₂ : N → M₂} {f : M → N} {g₂ : N' → M₃} {g : M' → N'}
-    {Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] TangentSpace I x}
-    {Df₂inv : ∀ x : N, TangentSpace I₂ (f₂ x) →L[𝕜] TangentSpace J x} {x : J¹MM'}
-    (hg₂ : MDifferentiableAt J' I₃ g₂ (g x.1.2)) (hg : MDifferentiableAt I' J' g x.1.2) :
+    {Dfinv : ∀ x : M, TangentSpace% (f x) →L[𝕜] TangentSpace% x}
+    {Df₂inv : ∀ x : N, TangentSpace% (f₂ x) →L[𝕜] TangentSpace% x} {x : J¹MM'}
+    (hg₂ : MDiffAt g₂ (g x.1.2)) (hg : MDiffAt g x.1.2) :
     OneJetBundle.map J' I₃ f₂ g₂ Df₂inv (OneJetBundle.map I' J' f g Dfinv x) =
       OneJetBundle.map I' I₃ (f₂ ∘ f) (g₂ ∘ g) (fun x ↦ Dfinv x ∘L Df₂inv (f x)) x := by
   ext
@@ -517,7 +517,7 @@ theorem OneJetBundle.map_id (x : J¹MM') :
   erw [ContinuousLinearMap.id_comp]
 
 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'}
+    {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))
     (hDfinv :
@@ -539,7 +539,7 @@ theorem ContMDiffAt.oneJetBundle_map {f : M'' → M → N} {g : M'' → M' → N
 
 
 /-- A useful definition to define maps between two `OneJetBundle`s. -/
-def mapLeft (f : M → N) (Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] TangentSpace I x) :
+def mapLeft (f : M → N) (Dfinv : ∀ x : M, TangentSpace% (f x) →L[𝕜] TangentSpace% x) :
     J¹MM' → OneJetBundle J N I' M' := fun p ↦ OneJetBundle.mk (f p.1.1) p.1.2 (p.2 ∘L Dfinv p.1.1)
 
 set_option backward.isDefEq.respectTransparency false in
@@ -547,13 +547,13 @@ set_option linter.style.multiGoal false in
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M']
   [IsManifold I₂ ∞ M₂] [IsManifold I₃ ∞ M₃]
   [IsManifold J' ∞ N'] [IsManifold J ∞ N] in
-theorem mapLeft_eq_map (f : M → N) (Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] TangentSpace I x) :
+theorem mapLeft_eq_map (f : M → N) (Dfinv : ∀ x : M, TangentSpace% (f x) →L[𝕜] TangentSpace% x) :
     mapLeft f Dfinv = OneJetBundle.map I' I' f (id : M' → M') Dfinv := by
   ext x; rfl; rfl; dsimp only [OneJetBundle.map, mapLeft, oneJetBundle_mk_snd]
   simp_rw [mfderiv_id, ContinuousLinearMap.id_comp]
 
 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'}
+    {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))
     (hDfinv :
       ContMDiffAt J' 𝓘(𝕜, F →L[𝕜] E) ∞
diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean
index 6b8fd28b..6e73c25e 100644
--- a/SphereEversion/Global/OneJetSec.lean
+++ b/SphereEversion/Global/OneJetSec.lean
@@ -47,7 +47,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 /-- A section of a 1-jet bundle seen as a bundle over the source manifold. -/
 @[ext] structure OneJetSec where
   bs : M → M'
-  ϕ : ∀ x : M, TangentSpace I x →L[𝕜] TangentSpace I' (bs x)
+  ϕ : ∀ x : M, TangentSpace% x →L[𝕜] TangentSpace% (bs x)
   contMDiff' : ContMDiff I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞
     fun x ↦ OneJetBundle.mk x (bs x) (ϕ x)
 
@@ -176,7 +176,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [Top
   in such a way that the function is smooth as a function of all arguments. -/
 @[ext] structure FamilyOneJetSec where
   bs : N → M → M'
-  ϕ : ∀ (n : N) (m : M), TangentSpace I m →L[ℝ] TangentSpace I' (bs n m)
+  ϕ : ∀ (n : N) (m : M), TangentSpace% m →L[ℝ] TangentSpace% (bs n m)
   contMDiff' :
     ContMDiff (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ∞ fun p : N × M ↦
       OneJetBundle.mk p.2 (bs p.1 p.2) (ϕ p.1 p.2)
diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean
index 8dcd0291..d125dff7 100644
--- a/SphereEversion/Global/ParametricityForFree.lean
+++ b/SphereEversion/Global/ParametricityForFree.lean
@@ -50,22 +50,22 @@ Porting note: the next statement has huge elaboration issue because of defEq abu
 We force our way using hard type ascription, ie. using `id`.
 The following commented out variables and check show the issue.
 variable {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
-    {p : DualPair <| TangentSpace (IP.prod I) σ.1.1}(q : DualPair <| TangentSpace I σ.1.1.2)
+    {p : DualPair <| TangentSpace% σ.1.1}(q : DualPair <| TangentSpace% σ.1.1.2)
 
 #check  p.v
-#check (p.v - (id ((0 : EP), (q.v : E)) : TangentSpace (IP.prod I) σ.proj.1))
+#check (p.v - (id ((0 : EP), (q.v : E)) : TangentSpace% σ.proj.1))
 #check (R.relativize IP P).slice σ p
-#check (R.slice (bundleSnd σ) q : Set <| TangentSpace I' σ.proj.2) -/
+#check (R.slice (bundleSnd σ) q : Set <| TangentSpace% σ.proj.2) -/
 
 set_option backward.isDefEq.respectTransparency false in
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] [IsManifold IP ∞ P] in
 theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
-    {p : DualPair <| TangentSpace (IP.prod I) σ.1.1} (q : DualPair <| TangentSpace I σ.1.1.2)
+    {p : DualPair <| TangentSpace% σ.1.1} (q : DualPair <| TangentSpace% σ.1.1.2)
     (hpq : p.π.comp (ContinuousLinearMap.inr ℝ EP E) = q.π) :
     (R.relativize IP P).slice σ p =
-      σ.2 (p.v - (id (0, (q.v : E)) : TangentSpace (IP.prod I) σ.proj.1)) +ᵥ
-      (id (R.slice (bundleSnd σ) q) : Set <| TangentSpace I' σ.proj.2) := by
-  set z := (p.v - (id (0, (q.v : E)) : TangentSpace (IP.prod I) σ.proj.1))
+      σ.2 (p.v - (id (0, (q.v : E)) : TangentSpace% σ.proj.1)) +ᵥ
+      (id (R.slice (bundleSnd σ) q) : Set <| TangentSpace% σ.proj.2) := by
+  set z := (p.v - (id (0, (q.v : E)) : TangentSpace% σ.proj.1))
   have h2pq : ∀ x : E, p.π ((0 : EP), x) = q.π x := fun x ↦
     congr_arg (fun f : E →L[ℝ] ℝ ↦ f x) hpq
   ext1 w
@@ -76,7 +76,7 @@ theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
     erw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply,
          ← ContinuousLinearMap.map_neg, neg_sub]
     obtain ⟨u, hu, t, rfl⟩ := q.decomp x
-    have hv : (id (0, (q.v : E)) : TangentSpace (IP.prod I) σ.proj.1) - p.v ∈ p.π.ker := by
+    have hv : (id (0, (q.v : E)) : TangentSpace% σ.proj.1) - p.v ∈ p.π.ker := by
       simp [LinearMap.mem_ker, map_sub, p.pairing, h2pq, q.pairing, sub_self]
     have hup : ((0 : EP), u) ∈ p.π.ker := (h2pq u).trans hu
     erw [q.update_apply _ hu, ← Prod.zero_mk_add_zero_mk, map_add, p.update_ker_pi _ _ hup, ←
@@ -89,7 +89,7 @@ theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
 
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] [IsManifold IP ∞ P] in
 theorem relativize_slice_eq_univ {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
-    {p : DualPair <| TangentSpace (IP.prod I) σ.1.1}
+    {p : DualPair <| TangentSpace% σ.1.1}
     (hp : p.π.comp (ContinuousLinearMap.inr ℝ EP E) = 0) :
     ((R.relativize IP P).slice σ p).Nonempty ↔ (R.relativize IP P).slice σ p = univ := by
   rcases σ with ⟨⟨⟨q, m⟩,m'⟩, φ⟩
@@ -123,7 +123,7 @@ theorem RelMfld.Ample.relativize (hR : R.Ample) : (R.relativize IP P).Ample := b
       PreconnectedSpace.connectedComponent_eq_univ, convexHull_univ]
   obtain ⟨u', hu'⟩ := ContinuousLinearMap.exists_ne_zero h
   let u := (p2 u')⁻¹ • u'
-  let q : DualPair (TangentSpace I σ.1.1.2) :=
+  let q : DualPair (TangentSpace% σ.1.1.2) :=
     ⟨p2, u, by erw [p2.map_smul, smul_eq_mul, inv_mul_cancel₀ hu']⟩
   rw [relativize_slice q rfl]
   exact (hR q).vadd
diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean
index 5c97d5e3..1438ed24 100644
--- a/SphereEversion/Global/Relation.lean
+++ b/SphereEversion/Global/Relation.lean
@@ -488,8 +488,8 @@ theorem OpenSmoothEmbedding.range_transfer :
   · rintro ⟨σ, rfl⟩; exact mk_mem_prod (mem_range_self _) (mem_range_self _)
   · rcases σ with ⟨⟨x, y⟩, τ⟩
     rintro ⟨⟨x, rfl⟩ : x ∈ range φ, ⟨y, rfl⟩ : y ∈ range ψ⟩
-    refine ⟨⟨(x, y), ((ψ.fderiv y).symm : TangentSpace IN (ψ y) →L[ℝ] TangentSpace IY y) ∘L
-      τ ∘L (φ.fderiv x : TangentSpace IX x →L[ℝ] TangentSpace IM (φ x))⟩, ?_⟩
+    refine ⟨⟨(x, y), ((ψ.fderiv y).symm : TangentSpace% (ψ y) →L[ℝ] TangentSpace% y) ∘L
+      τ ∘L (φ.fderiv x : TangentSpace% x →L[ℝ] TangentSpace% (φ x))⟩, ?_⟩
     refine congr_arg (Bundle.TotalSpace.mk _) (ContinuousLinearMap.ext fun v ↦ ?_)
     /- Porting note: Lean 3 version was
     simp_rw [continuous_linear_map.comp_apply, ← ψ.fderiv_coe, continuous_linear_equiv.coe_coe,
diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean
index ba2618c0..1bdbb8a8 100644
--- a/SphereEversion/Global/SmoothEmbedding.lean
+++ b/SphereEversion/Global/SmoothEmbedding.lean
@@ -86,12 +86,12 @@ 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 I x ≃L[𝕜] TangentSpace I' (f x) :=
-  have h₁ : MDifferentiableAt I' I f.invFun (f x) :=
+def fderiv (x : M) : TangentSpace% x ≃L[𝕜] TangentSpace% (f x) :=
+  have h₁ : MDiffAt f.invFun (f x) :=
     ((f.contMDiffOn_inv (f x)
     (mem_range_self x)).mdifferentiableWithinAt (by simp)).mdifferentiableAt
     (f.isOpenMap.range_mem_nhds x)
-  have h₂ : MDifferentiableAt I I' f x := f.contMDiff_to.mdifferentiableAt (by simp)
+  have h₂ : MDiffAt f x := f.contMDiff_to.mdifferentiableAt (by simp)
   ContinuousLinearEquiv.equivOfInverse (mfderiv% f x) (mfderiv% f.invFun (f x))
     (by
       intro v
@@ -110,19 +110,19 @@ def fderiv (x : M) : TangentSpace I x ≃L[𝕜] TangentSpace I' (f x) :=
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 @[simp]
 theorem fderiv_coe (x : M) :
-    (f.fderiv x : TangentSpace I x →L[𝕜] TangentSpace I' (f x)) = mfderiv% f x := by ext; rfl
+    (f.fderiv x : TangentSpace% x →L[𝕜] TangentSpace% (f x)) = mfderiv% f x := by ext; rfl
 
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 @[simp]
 theorem fderiv_symm_coe (x : M) :
-    ((f.fderiv x).symm : TangentSpace I' (f x) →L[𝕜] TangentSpace I x) =
+    ((f.fderiv x).symm : TangentSpace% (f x) →L[𝕜] TangentSpace% x) =
       mfderiv% f.invFun (f x) := by ext; rfl
 
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 theorem fderiv_symm_coe' {x : M'} (hx : x ∈ range f) :
     ((f.fderiv (f.invFun x)).symm :
-        TangentSpace I' (f (f.invFun x)) →L[𝕜] TangentSpace I (f.invFun x)) =
-      (mfderiv% f.invFun x : TangentSpace I' x →L[𝕜] TangentSpace I (f.invFun x)) :=
+        TangentSpace% (f (f.invFun x)) →L[𝕜] TangentSpace% (f.invFun x)) =
+      (mfderiv% f.invFun x : TangentSpace% x →L[𝕜] TangentSpace% (f.invFun x)) :=
   by rw [fderiv_symm_coe, f.right_inv hx]
 
 end
diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean
index efe62c8b..6a82186c 100644
--- a/SphereEversion/Global/TwistOneJetSec.lean
+++ b/SphereEversion/Global/TwistOneJetSec.lean
@@ -106,8 +106,8 @@ end Sections
 
 section proj
 
-instance piBugInstanceRestatement (x : M) : TopologicalSpace
-    (TangentSpace I x →L[𝕜] Trivial M V x) := by
+instance piBugInstanceRestatement (x : M) :
+    TopologicalSpace (TangentSpace% x →L[𝕜] Trivial M V x) := by
   infer_instance
 
 instance piBugInstanceRestatement2 (x : M × V) : TopologicalSpace (OneJetSpace I 𝓘(𝕜, V) x) := by
diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean
index 130666f7..83799bce 100644
--- a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean
+++ b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean
@@ -188,9 +188,9 @@ protected nonrec def ContMDiffAt {x : M} (φ : Germ (𝓝 x) F) (n : WithTop ℕ
 
 -- currently unused
 nonrec def mfderiv {x : M} (φ : Germ (𝓝 x) N) :
-    TangentSpace I x →L[ℝ] TangentSpace IG φ.value :=
+    TangentSpace% x →L[ℝ] TangentSpace% φ.value :=
   @Quotient.hrecOn _ (germSetoid (𝓝 x) N)
-    (fun φ : Germ (𝓝 x) N ↦ TangentSpace I x →L[ℝ] TangentSpace IG φ.value) φ
+    (fun φ : Germ (𝓝 x) N ↦ TangentSpace% x →L[ℝ] TangentSpace% φ.value) φ
     (fun f ↦ mfderiv% f x) fun _f _g hfg ↦ heq_of_eq (EventuallyEq.mfderiv_eq hfg : _)
 
 variable {I}
diff --git a/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean b/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean
index 9f1a86b1..74a3522a 100644
--- a/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean
+++ b/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean
@@ -337,7 +337,7 @@ attribute [mfld_simps] mem_insert_iff
 --   sorry
 -- end
 theorem contMDiffAt_tangentBundle_trivializationAt_continuousLinearMap (x₀ : TangentBundle I M) :
-    ContMDiffAt I.tangent 𝓘(𝕜, E) m
+    CMDiffAt m
       (fun x : TangentBundle I M ↦
         (trivializationAt E (TangentSpace I) x₀.proj).continuousLinearMapAt 𝕜 x.proj x.2)
       x₀ := by
@@ -374,7 +374,8 @@ theorem ContMDiffAt.contMDiffAt_tangentMap (x₀ : TangentBundle I M)
     (FiberBundle.continuous_proj E (TangentSpace I)).continuousAt.preimage_mem_nhds
       (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt _ _ _)
   have h2 :=
-    (hf.continuousAt.comp (FiberBundle.continuous_proj E (TangentSpace I)).continuousAt).preimage_mem_nhds
+    (hf.continuousAt.comp
+      (FiberBundle.continuous_proj E (TangentSpace I)).continuousAt).preimage_mem_nhds
       (e'.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt _ _ _)
   sorry /-filter_upwards [h1, h2] with x hx h2x
   dsimp only [inTangentCoordinates, in_coordinates, id_def]