diff --git a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
index e6ab158996ea6c..fe370981f4d96c 100644
--- a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
+++ b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
@@ -274,18 +274,18 @@ variable [Is : IsManifold I 1 M] [I's : IsManifold I' 1 M']
 is `C^m` when `m+1 ≤ n`. -/
 theorem ContMDiffOn.contMDiffOn_tangentMapWithin
     (hf : CMDiff[s] n f) (hmn : m + 1 ≤ n) (hs : UniqueMDiffOn I s) :
-    CMDiff[(π E (TangentSpace I) ⁻¹' s)] m (tangentMapWithin I I' f s) := by
+    CMDiff[(π E (TangentSpace I) ⁻¹' s)] m (tangentMap[s] f) := by
   intro x₀ hx₀
   let s' : Set (TangentBundle I M) := (π E (TangentSpace I) ⁻¹' s)
   let b₁ : TangentBundle I M → M := fun p ↦ p.1
-  let v : Π (y : TangentBundle I M), TangentSpace I (b₁ y) := fun y ↦ y.2
+  let v : Π (y : TangentBundle I M), TangentSpace% (b₁ y) := fun y ↦ y.2
   have hv : ContMDiffWithinAt I.tangent I.tangent m (fun y ↦ (v y : TangentBundle I M)) s' x₀ :=
     contMDiffWithinAt_id
   let b₂ : TangentBundle I M → M' := f ∘ b₁
   have hb₂ : CMDiffAt[s'] m b₂ x₀ :=
     ((hf (b₁ x₀) hx₀).of_le (le_self_add.trans hmn)).comp _
       (contMDiffWithinAt_proj (TangentSpace I)) (fun x h ↦ h)
-  let ϕ : Π (y : TangentBundle I M), TangentSpace I (b₁ y) →L[𝕜] TangentSpace I' (b₂ y) :=
+  let ϕ : Π (y : TangentBundle I M), TangentSpace% (b₁ y) →L[𝕜] TangentSpace% (b₂ y) :=
     fun y ↦ mfderiv[s] f (b₁ y)
   have hϕ : CMDiffAt[s'] m (fun y ↦ ContinuousLinearMap.inCoordinates E (TangentSpace I (M := M)) E'
       (TangentSpace I' (M := M')) (b₁ x₀) (b₁ y) (b₂ x₀) (b₂ y) (ϕ y)) x₀ := by
@@ -299,21 +299,21 @@ theorem ContMDiffOn.contMDiffOn_tangentMapWithin
 derivative is continuous there. -/
 theorem ContMDiffOn.continuousOn_tangentMapWithin (hf : CMDiff[s] n f) (hmn : 1 ≤ n)
     (hs : UniqueMDiffOn I s) :
-    ContinuousOn (tangentMapWithin I I' f s) (π E (TangentSpace I) ⁻¹' s) := by
-  have : CMDiff[π E (TangentSpace I) ⁻¹' s] 0 (tangentMapWithin I I' f s) :=
+    ContinuousOn (tangentMap[s] f) (π E (TangentSpace I) ⁻¹' s) := by
+  have : CMDiff[π E (TangentSpace I) ⁻¹' s] 0 (tangentMap[s] f) :=
     hf.contMDiffOn_tangentMapWithin hmn hs
   exact this.continuousOn
 
 /-- If a function is `C^n`, then its bundled derivative is `C^m` when `m+1 ≤ n`. -/
 theorem ContMDiff.contMDiff_tangentMap (hf : CMDiff n f) (hmn : m + 1 ≤ n) :
-    CMDiff m (tangentMap I I' f) := by
+    CMDiff m (tangentMap% f) := by
   rw [← contMDiffOn_univ] at hf ⊢
   convert! hf.contMDiffOn_tangentMapWithin hmn uniqueMDiffOn_univ
   rw [tangentMapWithin_univ]
 
 /-- If a function is `C^n`, with `1 ≤ n`, then its bundled derivative is continuous. -/
 theorem ContMDiff.continuous_tangentMap (hf : CMDiff n f) (hmn : 1 ≤ n) :
-    Continuous (tangentMap I I' f) := by
+    Continuous (tangentMap% f) := by
   rw [← contMDiffOn_univ] at hf
   rw [← continuousOn_univ]
   convert! hf.continuousOn_tangentMapWithin hmn uniqueMDiffOn_univ
@@ -342,7 +342,7 @@ may seem.
 TODO define splittings of vector bundles; state this result invariantly. -/
 theorem tangentMap_tangentBundle_pure [Is : IsManifold I 1 M]
     (p : TangentBundle I M) :
-    tangentMap I I.tangent (zeroSection E (TangentSpace I)) p = ⟨⟨p.proj, 0⟩, ⟨p.2, 0⟩⟩ := by
+    tangentMap% (zeroSection (B := M) E (TangentSpace I)) p = ⟨⟨p.proj, 0⟩, ⟨p.2, 0⟩⟩ := by
   rcases p with ⟨x, v⟩
   have N : I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (I ((chartAt H x) x)) := by
     apply IsOpen.mem_nhds
@@ -404,7 +404,7 @@ bundles. -/
 
 lemma equivTangentBundleProd_eq_tangentMap_prod_tangentMap :
     equivTangentBundleProd I M I' M' = fun (p : TangentBundle (I.prod I') (M × M')) ↦
-      (tangentMap (I.prod I') I Prod.fst p, tangentMap (I.prod I') I' Prod.snd p) := by
+      (tangentMap% (@Prod.fst M M') p, tangentMap% (@Prod.snd M M') p) := by
   simp only [tangentMap_prodFst, tangentMap_prodSnd]; rfl
 
 variable [IsManifold I 1 M] [IsManifold I' 1 M']
diff --git a/Mathlib/Geometry/Manifold/GroupLieAlgebra.lean b/Mathlib/Geometry/Manifold/GroupLieAlgebra.lean
index 010d41d7d763a8..0a011da1035f3d 100644
--- a/Mathlib/Geometry/Manifold/GroupLieAlgebra.lean
+++ b/Mathlib/Geometry/Manifold/GroupLieAlgebra.lean
@@ -53,13 +53,13 @@ variable (I G) in
 `GroupLieAlgebra` instead of `LieAlgebra` as the latter is taken as a generic class. -/
 @[to_additive /-- The Lie algebra of an additive Lie group, i.e., its tangent space at zero. We use
 the word `AddGroupLieAlgebra` instead of `LieAlgebra` as the latter is taken as a generic class. -/]
-abbrev GroupLieAlgebra : Type _ := TangentSpace I (1 : G)
+abbrev GroupLieAlgebra : Type _ := TangentSpace% (1 : G)
 
 /-- The invariant vector field associated to a vector `v` in the Lie algebra. At a point `g`, it
 is given by the image of `v` under left-multiplication by `g`. -/
 @[to_additive /-- The invariant vector field associated to a vector `v` in the Lie algebra. At a
 point `g`, it is given by the image of `v` under left-addition by `g`. -/]
-noncomputable def mulInvariantVectorField (v : GroupLieAlgebra I G) (g : G) : TangentSpace I g :=
+noncomputable def mulInvariantVectorField (v : GroupLieAlgebra I G) (g : G) : TangentSpace% g :=
   mfderiv% (g * ·) (1 : G) v
 
 set_option backward.isDefEq.respectTransparency false in
@@ -134,7 +134,7 @@ lemma mpullback_mulInvariantVectorField (g : G) (v : GroupLieAlgebra I G) :
 
 set_option backward.isDefEq.respectTransparency false in
 @[to_additive]
-lemma mulInvariantVectorField_eq_mpullback (g : G) (V : Π (g : G), TangentSpace I g) :
+lemma mulInvariantVectorField_eq_mpullback (g : G) (V : Π (g : G), TangentSpace% g) :
     mulInvariantVectorField (V 1) g = mpullback I I (g⁻¹ * ·) V g := by
   have A : 1 = g⁻¹ * g := by simp
   simp only [mulInvariantVectorField, mpullback, inverse_mfderiv_mul_left]
@@ -171,7 +171,7 @@ theorem contMDiff_mulInvariantVectorField (v : GroupLieAlgebra I G) :
     (equivTangentBundleProd I G I G).symm
   have S₂ : CMDiff (minSmoothness 𝕜 2) F₂ := contMDiff_equivTangentBundleProd_symm
   let F₃ : TangentBundle (I.prod I) (G × G) → TangentBundle I G :=
-    tangentMap (I.prod I) I (fun (p : G × G) ↦ p.1 * p.2)
+    tangentMap% (fun (p : G × G) ↦ p.1 * p.2)
   have S₃ : CMDiff (minSmoothness 𝕜 2) F₃ := by
     apply ContMDiff.contMDiff_tangentMap _ (m := minSmoothness 𝕜 2) le_rfl
     rw [A]
diff --git a/Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean b/Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
index 39836315da45e3..be0efc65d54a50 100644
--- a/Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
+++ b/Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
@@ -6,6 +6,7 @@ Authors: Winston Yin
 module
 
 public import Mathlib.Geometry.Manifold.MFDeriv.Tangent
+public import Mathlib.Geometry.Manifold.Notation
 
 /-!
 # Integral curves of vector fields on a manifold
@@ -62,21 +63,21 @@ variable
 /-- If `γ : ℝ → M` is $C^1$ on `s : Set ℝ` and `v` is a vector field on `M`,
 `IsMIntegralCurveOn γ v s` means `γ t` is tangent to `v (γ t)` for all `t ∈ s`. The value of `γ`
 outside of `s` is irrelevant and considered junk. -/
-def IsMIntegralCurveOn (γ : ℝ → M) (v : (x : M) → TangentSpace I x) (s : Set ℝ) : Prop :=
+def IsMIntegralCurveOn (γ : ℝ → M) (v : (x : M) → TangentSpace% x) (s : Set ℝ) : Prop :=
   ∀ t ∈ s, HasMFDerivAt[s] γ t ((1 : ℝ →L[ℝ] ℝ).smulRight <| v (γ t))
 
 /-- If `v` is a vector field on `M` and `t₀ : ℝ`, `IsMIntegralCurveAt γ v t₀` means `γ : ℝ → M` is a
 local integral curve of `v` in a neighbourhood containing `t₀`. The value of `γ` outside of this
 interval is irrelevant and considered junk. -/
-def IsMIntegralCurveAt (γ : ℝ → M) (v : (x : M) → TangentSpace I x) (t₀ : ℝ) : Prop :=
+def IsMIntegralCurveAt (γ : ℝ → M) (v : (x : M) → TangentSpace% x) (t₀ : ℝ) : Prop :=
   ∀ᶠ t in 𝓝 t₀, HasMFDerivAt% γ t ((1 : ℝ →L[ℝ] ℝ).smulRight <| v (γ t))
 
 /-- If `v : M → TM` is a vector field on `M`, `IsMIntegralCurve γ v` means `γ : ℝ → M` is a global
 integral curve of `v`. That is, `γ t` is tangent to `v (γ t)` for all `t : ℝ`. -/
-def IsMIntegralCurve (γ : ℝ → M) (v : (x : M) → TangentSpace I x) : Prop :=
+def IsMIntegralCurve (γ : ℝ → M) (v : (x : M) → TangentSpace% x) : Prop :=
   ∀ t : ℝ, HasMFDerivAt% γ t ((1 : ℝ →L[ℝ] ℝ).smulRight (v (γ t)))
 
-variable {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {s s' : Set ℝ} {t₀ : ℝ}
+variable {γ γ' : ℝ → M} {v : (x : M) → TangentSpace% x} {s s' : Set ℝ} {t₀ : ℝ}
 
 lemma IsMIntegralCurve.isMIntegralCurveOn (h : IsMIntegralCurve γ v) (s : Set ℝ) :
     IsMIntegralCurveOn γ v s := fun t _ ↦ (h t).hasMFDerivWithinAt
diff --git a/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean b/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
index 45c0236b5d06fe..0cc8f598e3708b 100644
--- a/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
+++ b/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
@@ -276,15 +276,15 @@ This lemma phrases the formula using the equiv `NormedSpace.fromTangentSpace`, w
 canonical identification. (It would also be possible to phrase the formula without this equiv,
 instead using casting and definitional abuse.) -/
 private lemma HasMFDerivAt.smul
-    {f' : TangentSpace I x →L[𝕜] 𝕜}
+    {f' : TangentSpace% x →L[𝕜] 𝕜}
     (hs : HasMFDerivAt% f x ((fromTangentSpace (f x)).symm.toContinuousLinearMap ∘L f'))
-    {g' : TangentSpace I x →L[𝕜] V}
+    {g' : TangentSpace% x →L[𝕜] V}
     (hg : HasMFDerivAt% g x ((fromTangentSpace (g x)).symm.toContinuousLinearMap ∘L g')) :
     -- canonically identify `g'` with a linear map into the tangent space at `(f • g) x`
-    letI g'_ : TangentSpace I x →L[𝕜] TangentSpace 𝓘(𝕜, V) ((f • g) x) :=
+    letI g'_ : TangentSpace% x →L[𝕜] TangentSpace 𝓘(𝕜, V) ((f • g) x) :=
       (fromTangentSpace _).symm.toContinuousLinearMap ∘L g'
     -- canonically identify `g x` with a linear map into a tangent space at `(f • g) x`
-    letI gx : 𝕜 →L[𝕜] TangentSpace 𝓘(𝕜, V) ((f • g) x) :=
+    letI gx : 𝕜 →L[𝕜] TangentSpace% ((f • g) x) :=
       toSpanSingleton 𝕜 ((fromTangentSpace _).symm (g x))
     -- now the main statement typechecks
     HasMFDerivAt% (f • g) x (f x • g'_ + gx ∘L f') := by
@@ -382,7 +382,7 @@ typecheck we need a phrasing involving the canonical identification `NormedSpace
 between the vector space `V` and the tangent space to this vector space at any point. This is
 because two different tangent spaces (at `(f • g) x` and `g x`) appear in the equation. -/
 private lemma fromTangentSpace_mfderiv_smul_apply (hf : MDiffAt f x) (hg : MDiffAt g x)
-    (v : TangentSpace I x) :
+    (v : TangentSpace% x) :
     fromTangentSpace _ (mfderiv% (f • g) x v)
     = f x • fromTangentSpace _ (mfderiv% g x v) + fromTangentSpace _ (mfderiv% f x v) • g x := by
   simpa using congr($(fromTangentSpace_mfderiv_smul hf hg) v)
@@ -400,7 +400,7 @@ because two different tangent spaces (at `(f • g) x` and `g x`) appear in the
 This is a defeq variant of the main lemma `fromTangentSpace_mfderiv_smul_apply`, in which we work in
 the tangent space at `f x • g x` (the simp-normal form) rather than at `(f • g) x`. -/
 private lemma fromTangentSpace_mfderiv_smul_apply' (hf : MDiffAt f x) (hg : MDiffAt g x)
-    (v : TangentSpace I x) :
+    (v : TangentSpace% x) :
     fromTangentSpace (f x • g x) (mfderiv% (f • g) x v)
     = f x • fromTangentSpace _ (mfderiv% g x v) + fromTangentSpace _ (mfderiv% f x v) • g x :=
   fromTangentSpace_mfderiv_smul_apply hf hg v
@@ -428,7 +428,7 @@ Future: this could be generalised to functions into additive torsors over abelia
 -/
 @[expose]
 noncomputable def mvfderiv (g : M → F) :
-    Π x : M, TangentSpace I x →L[𝕜] F :=
+    Π x : M, TangentSpace% x →L[𝕜] F :=
   fun x ↦ (NormedSpace.fromTangentSpace <| g x).toContinuousLinearMap ∘L (mfderiv% g x)
 @[deprecated (since := "2026-05-17")] alias extDerivFun := mvfderiv
 
diff --git a/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean b/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
index 28254093a16323..60b917645a0878 100644
--- a/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
+++ b/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Analysis.Calculus.FDeriv.Mul
 public import Mathlib.Geometry.Manifold.MFDeriv.FDeriv
-import Mathlib.Geometry.Manifold.Notation
+public import Mathlib.Geometry.Manifold.Notation
 
 /-!
 # Differentiability of specific functions
@@ -126,7 +126,7 @@ section id
 /-! #### Identity -/
 
 theorem hasMFDerivAt_id (x : M) :
-    HasMFDerivAt% (@id M) x (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) := by
+    HasMFDerivAt% (@id M) x (ContinuousLinearMap.id 𝕜 (TangentSpace% x)) := by
   refine ⟨continuousAt_id, ?_⟩
   have : ∀ᶠ y in 𝓝[range I] (extChartAt I x) x, (extChartAt I x ∘ (extChartAt I x).symm) y = y := by
     apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin x)
@@ -135,7 +135,7 @@ theorem hasMFDerivAt_id (x : M) :
   simp only [mfld_simps]
 
 theorem hasMFDerivWithinAt_id (s : Set M) (x : M) :
-    HasMFDerivAt[s] (@id M) x (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) :=
+    HasMFDerivAt[s] (@id M) x (ContinuousLinearMap.id 𝕜 (TangentSpace% x)) :=
   (hasMFDerivAt_id x).hasMFDerivWithinAt
 
 theorem mdifferentiableAt_id : MDiffAt (@id M) x :=
@@ -150,20 +150,20 @@ theorem mdifferentiableOn_id : MDiff[s] (@id M) :=
   mdifferentiable_id.mdifferentiableOn
 
 @[simp, mfld_simps]
-theorem mfderiv_id : mfderiv% (@id M) x = ContinuousLinearMap.id 𝕜 (TangentSpace I x) :=
+theorem mfderiv_id : mfderiv% (@id M) x = ContinuousLinearMap.id 𝕜 (TangentSpace% x) :=
   (hasMFDerivAt_id x).mfderiv
 
 theorem mfderivWithin_id (hxs : UniqueMDiffWithinAt I s x) :
-    mfderiv[s] (@id M) x = ContinuousLinearMap.id 𝕜 (TangentSpace I x) := by
+    mfderiv[s] (@id M) x = ContinuousLinearMap.id 𝕜 (TangentSpace% x) := by
   rw [MDifferentiable.mfderivWithin mdifferentiableAt_id hxs]
   exact mfderiv_id
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp, mfld_simps]
-theorem tangentMap_id : tangentMap I I (id : M → M) = id := by ext1 ⟨x, v⟩; simp [tangentMap]
+theorem tangentMap_id : tangentMap% (@id M) = id := by ext1 ⟨x, v⟩; simp [tangentMap]
 
 theorem tangentMapWithin_id {p : TangentBundle I M} (hs : UniqueMDiffWithinAt I s p.proj) :
-    tangentMapWithin I I (id : M → M) s p = p := by
+    tangentMap[s] (id : M → M) p = p := by
   simp only [tangentMapWithin, id]
   rw [mfderivWithin_id]
   · rcases p with ⟨⟩; rfl
@@ -180,11 +180,11 @@ variable {c : M'}
 
 set_option backward.isDefEq.respectTransparency false in
 theorem hasMFDerivAt_const (c : M') (x : M) :
-    HasMFDerivAt% (fun _ : M ↦ c) x (0 : TangentSpace I x →L[𝕜] TangentSpace I' c) :=
+    HasMFDerivAt% (fun _ : M ↦ c) x (0 : TangentSpace% x →L[𝕜] TangentSpace% c) :=
   ⟨by fun_prop, by simp [Function.comp_def, hasFDerivWithinAt_const]⟩
 
 theorem hasMFDerivWithinAt_const (c : M') (s : Set M) (x : M) :
-    HasMFDerivAt[s] (fun _ : M ↦ c) x (0 : TangentSpace I x →L[𝕜] TangentSpace I' c) :=
+    HasMFDerivAt[s] (fun _ : M ↦ c) x (0 : TangentSpace% x →L[𝕜] TangentSpace% c) :=
   (hasMFDerivAt_const c x).hasMFDerivWithinAt
 
 theorem mdifferentiableAt_const : MDiffAt (fun _ : M ↦ c) x :=
@@ -200,11 +200,11 @@ theorem mdifferentiableOn_const : MDiff[s] (fun _ : M ↦ c) :=
 
 @[simp, mfld_simps]
 theorem mfderiv_const :
-    mfderiv% (fun _ : M ↦ c) x = (0 : TangentSpace I x →L[𝕜] TangentSpace I' c) :=
+    mfderiv% (fun _ : M ↦ c) x = (0 : TangentSpace% x →L[𝕜] TangentSpace% c) :=
   (hasMFDerivAt_const c x).mfderiv
 
 theorem mfderivWithin_const :
-    mfderiv[s] (fun _ : M ↦ c) x = (0 : TangentSpace I x →L[𝕜] TangentSpace I' c) :=
+    mfderiv[s] (fun _ : M ↦ c) x = (0 : TangentSpace% x →L[𝕜] TangentSpace% c) :=
   (hasMFDerivWithinAt_const _ _ _).mfderivWithin_eq_zero
 
 end Const
@@ -221,8 +221,8 @@ theorem MDifferentiableWithinAt.prodMk {f : M → M'} {g : M → M''}
 /-- If `f` and `g` have derivatives `df` and `dg` within `s` at `x`, respectively,
 then `x ↦ (f x, g x)` has derivative `df.prod dg` within `s`. -/
 theorem HasMFDerivWithinAt.prodMk {f : M → M'} {g : M → M''}
-    {df : TangentSpace I x →L[𝕜] TangentSpace I' (f x)} (hf : HasMFDerivAt[s] f x df)
-    {dg : TangentSpace I x →L[𝕜] TangentSpace I'' (g x)} (hg : HasMFDerivAt[s] g x dg) :
+    {df : TangentSpace% x →L[𝕜] TangentSpace% (f x)} (hf : HasMFDerivAt[s] f x df)
+    {dg : TangentSpace% x →L[𝕜] TangentSpace% (g x)} (hg : HasMFDerivAt[s] g x dg) :
     HasMFDerivAt[s] (fun y ↦ (f y, g y)) x (df.prod dg) :=
   ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩
 
@@ -244,8 +244,8 @@ theorem MDifferentiableAt.prodMk {f : M → M'} {g : M → M''} (hf : MDiffAt f
 /-- If `f` and `g` have derivatives `df` and `dg` at `x`, respectively,
 then `x ↦ (f x, g x)` has derivative `df.prod dg`. -/
 theorem HasMFDerivAt.prodMk {f : M → M'} {g : M → M''}
-    {df : TangentSpace I x →L[𝕜] TangentSpace I' (f x)} (hf : HasMFDerivAt% f x df)
-    {dg : TangentSpace I x →L[𝕜] TangentSpace I'' (g x)} (hg : HasMFDerivAt% g x dg) :
+    {df : TangentSpace% x →L[𝕜] TangentSpace% (f x)} (hf : HasMFDerivAt% f x df)
+    {dg : TangentSpace% x →L[𝕜] TangentSpace% (g x)} (hg : HasMFDerivAt% g x dg) :
     HasMFDerivAt% (fun y ↦ (f y, g y)) x (df.prod dg) :=
   ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩
 
@@ -276,7 +276,7 @@ fun x ↦ (hf x).prodMk_space (hg x)
 
 theorem hasMFDerivAt_fst (x : M × M') :
     HasMFDerivAt% (@Prod.fst M M') x
-      (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) := by
+      (ContinuousLinearMap.fst 𝕜 (TangentSpace% x.1) (TangentSpace% x.2)) := by
   refine ⟨continuous_fst.continuousAt, ?_⟩
   have :
     ∀ᶠ y in 𝓝[range (I.prod I')] extChartAt (I.prod I') x x,
@@ -294,7 +294,7 @@ theorem hasMFDerivAt_fst (x : M × M') :
 
 theorem hasMFDerivWithinAt_fst (s : Set (M × M')) (x : M × M') :
     HasMFDerivAt[s] (@Prod.fst M M') x
-      (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) :=
+      (ContinuousLinearMap.fst 𝕜 (TangentSpace% x.1) (TangentSpace% x.2)) :=
   (hasMFDerivAt_fst x).hasMFDerivWithinAt
 
 theorem mdifferentiableAt_fst {x : M × M'} : MDiffAt (@Prod.fst M M') x :=
@@ -312,23 +312,23 @@ theorem mdifferentiableOn_fst {s : Set (M × M')} : MDiff[s] (@Prod.fst M M') :=
 @[simp, mfld_simps]
 theorem mfderiv_fst {x : M × M'} :
     mfderiv% (@Prod.fst M M') x =
-      ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2) :=
+      ContinuousLinearMap.fst 𝕜 (TangentSpace% x.1) (TangentSpace% x.2) :=
   (hasMFDerivAt_fst x).mfderiv
 
 theorem mfderivWithin_fst {s : Set (M × M')} {x : M × M'}
     (hxs : UniqueMDiffWithinAt (I.prod I') s x) :
     mfderiv[s] (@Prod.fst M M') x =
-      ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2) := by
+      ContinuousLinearMap.fst 𝕜 (TangentSpace% x.1) (TangentSpace% x.2) := by
   rw [MDifferentiable.mfderivWithin mdifferentiableAt_fst hxs]; exact mfderiv_fst
 
 @[simp, mfld_simps]
 theorem tangentMap_prodFst {p : TangentBundle (I.prod I') (M × M')} :
-    tangentMap (I.prod I') I Prod.fst p = ⟨p.proj.1, p.2.1⟩ := by
+    tangentMap% (@Prod.fst M M') p = ⟨p.proj.1, p.2.1⟩ := by
   simp [tangentMap]; rfl
 
 theorem tangentMapWithin_prodFst {s : Set (M × M')} {p : TangentBundle (I.prod I') (M × M')}
     (hs : UniqueMDiffWithinAt (I.prod I') s p.proj) :
-    tangentMapWithin (I.prod I') I Prod.fst s p = ⟨p.proj.1, p.2.1⟩ := by
+    tangentMap[s] (@Prod.fst M M') p = ⟨p.proj.1, p.2.1⟩ := by
   simp only [tangentMapWithin]
   rw [mfderivWithin_fst]
   · rcases p with ⟨⟩; rfl
@@ -336,7 +336,7 @@ theorem tangentMapWithin_prodFst {s : Set (M × M')} {p : TangentBundle (I.prod
 
 theorem hasMFDerivAt_snd (x : M × M') :
     HasMFDerivAt% (@Prod.snd M M') x
-      (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) := by
+      (ContinuousLinearMap.snd 𝕜 (TangentSpace% x.1) (TangentSpace% x.2)) := by
   refine ⟨continuous_snd.continuousAt, ?_⟩
   have :
     ∀ᶠ y in 𝓝[range (I.prod I')] extChartAt (I.prod I') x x,
@@ -354,7 +354,7 @@ theorem hasMFDerivAt_snd (x : M × M') :
 
 theorem hasMFDerivWithinAt_snd (s : Set (M × M')) (x : M × M') :
     HasMFDerivAt[s] (@Prod.snd M M') x
-      (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) :=
+      (ContinuousLinearMap.snd 𝕜 (TangentSpace% x.1) (TangentSpace% x.2)) :=
   (hasMFDerivAt_snd x).hasMFDerivWithinAt
 
 theorem mdifferentiableAt_snd {x : M × M'} : MDiffAt (@Prod.snd M M') x :=
@@ -371,13 +371,13 @@ theorem mdifferentiableOn_snd {s : Set (M × M')} : MDiff[s] (@Prod.snd M M') :=
 @[simp, mfld_simps]
 theorem mfderiv_snd {x : M × M'} :
     mfderiv% (@Prod.snd M M') x =
-      ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2) :=
+      ContinuousLinearMap.snd 𝕜 (TangentSpace% x.1) (TangentSpace% x.2) :=
   (hasMFDerivAt_snd x).mfderiv
 
 theorem mfderivWithin_snd {s : Set (M × M')} {x : M × M'}
     (hxs : UniqueMDiffWithinAt (I.prod I') s x) :
     mfderiv[s] (@Prod.snd M M') x =
-      ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2) := by
+      ContinuousLinearMap.snd 𝕜 (TangentSpace% x.1) (TangentSpace% x.2) := by
   rw [MDifferentiable.mfderivWithin mdifferentiableAt_snd hxs]; exact mfderiv_snd
 
 theorem MDifferentiableWithinAt.fst {f : N → M × M'} {s : Set N} {x : N}
@@ -481,9 +481,9 @@ theorem MDifferentiable.prodMap (hf : MDiff f) (hg : MDiff g) : MDiff (Prod.map
 
 set_option backward.isDefEq.respectTransparency false in
 lemma HasMFDerivWithinAt.prodMap {s : Set <| M × M'} {p : M × M'} {f : M → N} {g : M' → N'}
-    {df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)}
+    {df : TangentSpace% p.1 →L[𝕜] TangentSpace% (f p.1)}
     (hf : HasMFDerivAt[Prod.fst '' s] f p.1 df)
-    {dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)}
+    {dg : TangentSpace% p.2 →L[𝕜] TangentSpace% (g p.2)}
     (hg : HasMFDerivAt[Prod.snd '' s] g p.2 dg) :
     HasMFDerivAt[s] (Prod.map f g) p (df.prodMap dg) := by
   refine ⟨hf.1.prodMap hg.1 |>.mono (by grind), ?_⟩
@@ -501,8 +501,8 @@ lemma HasMFDerivWithinAt.prodMap {s : Set <| M × M'} {p : M × M'} {f : M → N
 
 set_option backward.isDefEq.respectTransparency false in
 lemma HasMFDerivAt.prodMap {p : M × M'} {f : M → N} {g : M' → N'}
-    {df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)} (hf : HasMFDerivAt% f p.1 df)
-    {dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)} (hg : HasMFDerivAt% g p.2 dg) :
+    {df : TangentSpace% p.1 →L[𝕜] TangentSpace% (f p.1)} (hf : HasMFDerivAt% f p.1 df)
+    {dg : TangentSpace% p.2 →L[𝕜] TangentSpace% (g p.2)} (hg : HasMFDerivAt% g p.2 dg) :
     HasMFDerivAt% (Prod.map f g) p
       ((mfderiv% f p.1).prodMap (mfderiv% g p.2)) := by
   simp_rw [← hasMFDerivWithinAt_univ, ← mfderivWithin_univ, ← univ_prod_univ]
@@ -535,12 +535,12 @@ end prodMap
 
 @[simp, mfld_simps]
 theorem tangentMap_prodSnd {p : TangentBundle (I.prod I') (M × M')} :
-    tangentMap (I.prod I') I' Prod.snd p = ⟨p.proj.2, p.2.2⟩ := by
+    tangentMap% (@Prod.snd M M') p = ⟨p.proj.2, p.2.2⟩ := by
   simp [tangentMap]; rfl
 
 theorem tangentMapWithin_prodSnd {s : Set (M × M')} {p : TangentBundle (I.prod I') (M × M')}
     (hs : UniqueMDiffWithinAt (I.prod I') s p.proj) :
-    tangentMapWithin (I.prod I') I' Prod.snd s p = ⟨p.proj.2, p.2.2⟩ := by
+    tangentMap[s] (@Prod.snd M M') p = ⟨p.proj.2, p.2.2⟩ := by
   simp only [tangentMapWithin]
   rw [mfderivWithin_snd hs]
   rcases p with ⟨⟩; rfl
@@ -551,24 +551,25 @@ alias MDifferentiableAt.mfderiv_prod := mfderiv_prodMk
 set_option backward.isDefEq.respectTransparency false in
 theorem mfderiv_prod_left {x₀ : M} {y₀ : M'} :
     mfderiv% (fun (x : M) ↦ (x, y₀)) x₀ =
-      ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) := by
+      ContinuousLinearMap.inl 𝕜 (TangentSpace% x₀) (TangentSpace% y₀) := by
   refine (mdifferentiableAt_id.mfderiv_prod mdifferentiableAt_const).trans ?_
   rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inl]
 
+-- TODO: better error when the type of x is left open
 theorem tangentMap_prod_left {p : TangentBundle I M} {y₀ : M'} :
-    tangentMap I (I.prod I') (fun x ↦ (x, y₀)) p = ⟨(p.1, y₀), (p.2, 0)⟩ := by
+    tangentMap% (fun (x : M) ↦ (x, y₀)) p = ⟨(p.1, y₀), (p.2, 0)⟩ := by
   simp only [tangentMap, mfderiv_prod_left, TotalSpace.mk_inj]
   rfl
 
 set_option backward.isDefEq.respectTransparency false in
 theorem mfderiv_prod_right {x₀ : M} {y₀ : M'} :
     mfderiv% (fun (y : M') ↦ (x₀, y)) y₀ =
-      ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) := by
+      ContinuousLinearMap.inr 𝕜 (TangentSpace% x₀) (TangentSpace% y₀) := by
   refine (mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_id).trans ?_
   rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inr]
 
 theorem tangentMap_prod_right {p : TangentBundle I' M'} {x₀ : M} :
-    tangentMap I' (I.prod I') (fun y ↦ (x₀, y)) p = ⟨(x₀, p.1), (0, p.2)⟩ := by
+    tangentMap% (fun (y : M') ↦ (x₀, y)) p = ⟨(x₀, p.1), (0, p.2)⟩ := by
   simp only [tangentMap, mfderiv_prod_right, TotalSpace.mk_inj]
   rfl
 
@@ -596,9 +597,9 @@ theorem mfderiv_prod_eq_add {f : M × M' → M''} {p : M × M'}
 theorem mfderiv_prod_eq_add_comp {f : M × M' → M''} {p : M × M'} (hf : MDiffAt f p) :
     mfderiv% f p =
         (mfderiv% (fun z : M ↦ f (z, p.2)) p.1) ∘L (id (ContinuousLinearMap.fst 𝕜 E E') :
-          (TangentSpace (I.prod I') p) →L[𝕜] (TangentSpace I p.1)) +
+          (TangentSpace% p) →L[𝕜] (TangentSpace% p.1)) +
         (mfderiv% (fun z : M' ↦ f (p.1, z)) p.2) ∘L (id (ContinuousLinearMap.snd 𝕜 E E') :
-          (TangentSpace (I.prod I') p) →L[𝕜] (TangentSpace I' p.2)) := by
+          (TangentSpace% p) →L[𝕜] (TangentSpace% p.2)) := by
   rw [mfderiv_prod_eq_add hf]
   congr
   · have : (fun z : M × M' ↦ f (z.1, p.2)) = (fun z : M ↦ f (z, p.2)) ∘ Prod.fst := rfl
@@ -617,7 +618,7 @@ theorem mfderiv_prod_eq_add_comp {f : M × M' → M''} {p : M × M'} (hf : MDiff
 /-- The total derivative of a function in two variables is the sum of the partial derivatives.
   Note that to state this (without casts) we need to be able to see through the definition of
   `TangentSpace`. Version in terms of the one-variable derivatives. -/
-theorem mfderiv_prod_eq_add_apply {f : M × M' → M''} {p : M × M'} {v : TangentSpace (I.prod I') p}
+theorem mfderiv_prod_eq_add_apply {f : M × M' → M''} {p : M × M'} {v : TangentSpace% p}
     (hf : MDiffAt f p) :
     mfderiv% f p v =
       mfderiv% (fun z : M ↦ f (z, p.2)) p.1 v.1 + mfderiv% (fun z : M' ↦ f (p.1, z)) p.2 v.2 := by
@@ -662,7 +663,7 @@ lemma writtenInExtChartAt_sumSwap_eventuallyEq_id :
       exact (chartAt H x).open_target.mem_nhds (by simp)
 
 theorem hasMFDerivAt_sumSwap :
-    HasMFDerivAt% (@Sum.swap M M') p (ContinuousLinearMap.id 𝕜 (TangentSpace I p)) := by
+    HasMFDerivAt% (@Sum.swap M M') p (ContinuousLinearMap.id 𝕜 (TangentSpace% p)) := by
   refine ⟨by fun_prop, ?_⟩
   apply (hasFDerivWithinAt_id _ (range I)).congr_of_eventuallyEq
   · exact writtenInExtChartAt_sumSwap_eventuallyEq_id
@@ -671,12 +672,12 @@ theorem hasMFDerivAt_sumSwap :
 
 @[simp]
 theorem mfderivWithin_sumSwap {s : Set (M ⊕ M')} (hs : UniqueMDiffWithinAt I s p) :
-    mfderiv[s] (@Sum.swap M M') p = ContinuousLinearMap.id 𝕜 (TangentSpace I p) :=
+    mfderiv[s] (@Sum.swap M M') p = ContinuousLinearMap.id 𝕜 (TangentSpace% p) :=
   hasMFDerivAt_sumSwap.hasMFDerivWithinAt.mfderivWithin hs
 
 @[simp]
 theorem mfderiv_sumSwap :
-    mfderiv% (@Sum.swap M M') p = ContinuousLinearMap.id 𝕜 (TangentSpace I p) := by
+    mfderiv% (@Sum.swap M M') p = ContinuousLinearMap.id 𝕜 (TangentSpace% p) := by
   simpa [mfderivWithin_univ] using (mfderivWithin_sumSwap (uniqueMDiffWithinAt_univ I))
 
 variable {f : M → N} (g : M' → N') {q : M} {q' : M'}
@@ -706,7 +707,7 @@ lemma writtenInExtChartAt_sumInr_eventuallyEq_id :
     (chartAt H q').right_inv (by simpa [Set.mem_preimage, I.left_inv] using hyT)]
 
 theorem hasMFDerivWithinAt_inl :
-    HasMFDerivAt[s] (@Sum.inl M M') q (ContinuousLinearMap.id 𝕜 (TangentSpace I q)) := by
+    HasMFDerivAt[s] (@Sum.inl M M') q (ContinuousLinearMap.id 𝕜 (TangentSpace% q)) := by
   refine ⟨by fun_prop, ?_⟩
   have : (writtenInExtChartAt I I q (@Sum.inl M M'))
       =ᶠ[𝓝[(extChartAt I q).symm ⁻¹' s ∩ Set.range I] (extChartAt I q q)] id :=
@@ -715,11 +716,11 @@ theorem hasMFDerivWithinAt_inl :
     (by simp [writtenInExtChartAt, extChartAt])
 
 theorem hasMFDerivAt_inl :
-    HasMFDerivAt% (@Sum.inl M M') q (ContinuousLinearMap.id 𝕜 (TangentSpace I p)) := by
+    HasMFDerivAt% (@Sum.inl M M') q (ContinuousLinearMap.id 𝕜 (TangentSpace% p)) := by
   simpa [HasMFDerivAt, hasMFDerivWithinAt_univ] using! hasMFDerivWithinAt_inl (s := Set.univ)
 
 theorem hasMFDerivWithinAt_inr {t : Set M'} :
-    HasMFDerivAt[t] (@Sum.inr M M') q' (ContinuousLinearMap.id 𝕜 (TangentSpace I q')) := by
+    HasMFDerivAt[t] (@Sum.inr M M') q' (ContinuousLinearMap.id 𝕜 (TangentSpace% q')) := by
   refine ⟨by fun_prop, ?_⟩
   have : (writtenInExtChartAt I I q' (@Sum.inr M M'))
       =ᶠ[𝓝[(extChartAt I q').symm ⁻¹' t ∩ Set.range I] (extChartAt I q' q')] id :=
@@ -728,23 +729,23 @@ theorem hasMFDerivWithinAt_inr {t : Set M'} :
     (by simp [writtenInExtChartAt, extChartAt])
 
 theorem hasMFDerivAt_inr :
-    HasMFDerivAt% (@Sum.inr M M') q' (ContinuousLinearMap.id 𝕜 (TangentSpace I p)) := by
+    HasMFDerivAt% (@Sum.inr M M') q' (ContinuousLinearMap.id 𝕜 (TangentSpace% p)) := by
   simpa [HasMFDerivAt, hasMFDerivWithinAt_univ] using! hasMFDerivWithinAt_inr (t := Set.univ)
 
 theorem mfderivWithin_sumInl (hU : UniqueMDiffWithinAt I s q) :
-    mfderiv[s] (@Sum.inl M M') q = ContinuousLinearMap.id 𝕜 (TangentSpace I p) :=
+    mfderiv[s] (@Sum.inl M M') q = ContinuousLinearMap.id 𝕜 (TangentSpace% p) :=
   hasMFDerivWithinAt_inl.mfderivWithin hU
 
 theorem mfderiv_sumInl :
-    mfderiv% (@Sum.inl M M') q = ContinuousLinearMap.id 𝕜 (TangentSpace I p) := by
+    mfderiv% (@Sum.inl M M') q = ContinuousLinearMap.id 𝕜 (TangentSpace% p) := by
   simpa [mfderivWithin_univ] using (mfderivWithin_sumInl (uniqueMDiffWithinAt_univ I))
 
 theorem mfderivWithin_sumInr {t : Set M'} (hU : UniqueMDiffWithinAt I t q') :
-    mfderiv[t] (@Sum.inr M M') q' = ContinuousLinearMap.id 𝕜 (TangentSpace I q') :=
+    mfderiv[t] (@Sum.inr M M') q' = ContinuousLinearMap.id 𝕜 (TangentSpace% q') :=
   hasMFDerivWithinAt_inr.mfderivWithin hU
 
 theorem mfderiv_sumInr :
-    mfderiv% (@Sum.inr M M') q' = ContinuousLinearMap.id 𝕜 (TangentSpace I q') := by
+    mfderiv% (@Sum.inr M M') q' = ContinuousLinearMap.id 𝕜 (TangentSpace% q') := by
   simpa [mfderivWithin_univ] using (mfderivWithin_sumInr (uniqueMDiffWithinAt_univ I))
 
 end disjointUnion
@@ -760,7 +761,7 @@ canonical, but in this case (the tangent space of a vector space) it is canonica
 
 section Group
 
-variable {z : M} {f g : M → E'} {f' g' : TangentSpace I z →L[𝕜] E'}
+variable {z : M} {f g : M → E'} {f' g' : TangentSpace% z →L[𝕜] E'}
 
 theorem HasMFDerivWithinAt.add {s : Set M}
     (hf : HasMFDerivAt[s] f z f') (hg : HasMFDerivAt[s] g z g') :
@@ -788,18 +789,18 @@ theorem MDifferentiable.add (hf : MDiff f) (hg : MDiff g) : MDiff (f + g) :=
 -- Deprecate all these lemmas in favour of a version using `mvfderiv(Within)`
 -- Porting note: forcing types using `by exact`
 theorem mfderiv_add (hf : MDiffAt f z) (hg : MDiffAt g z) :
-    (mfderiv% (f + g) z : TangentSpace I z →L[𝕜] E') =
+    (mfderiv% (f + g) z : TangentSpace% z →L[𝕜] E') =
       (by exact mfderiv% f z) + (by exact mfderiv% g z) :=
   (hf.hasMFDerivAt.add hg.hasMFDerivAt).mfderiv
 
 theorem mfderivWithin_add (hf : MDiffAt[s] f z) (hg : MDiffAt[s] g z)
     (hs : UniqueMDiffWithinAt I s z) :
-    (mfderiv[s] (f + g) z : TangentSpace I z →L[𝕜] E') =
+    (mfderiv[s] (f + g) z : TangentSpace% z →L[𝕜] E') =
       (by exact mfderiv[s] f z) + (by exact mfderiv[s] g z) :=
   (hf.hasMFDerivWithinAt.add hg.hasMFDerivWithinAt).mfderivWithin hs
 
 section sum
-variable {ι : Type} {t : Finset ι} {f : ι → M → E'} {f' : ι → TangentSpace I z →L[𝕜] E'}
+variable {ι : Type} {t : Finset ι} {f : ι → M → E'} {f' : ι → TangentSpace% z →L[𝕜] E'}
 
 lemma HasMFDerivWithinAt.sum (hf : ∀ i ∈ t, HasMFDerivAt[s] (f i) z (f' i)) :
     HasMFDerivAt[s] (∑ i ∈ t, f i) z (∑ i ∈ t, f' i) := by
@@ -914,12 +915,12 @@ theorem MDifferentiable.sub (hf : MDiff f) (hg : MDiff g) : MDiff (f - g) :=
 
 theorem mfderivWithin_sub (hf : MDiffAt[s] f z) (hg : MDiffAt[s] g z)
     (hs : UniqueMDiffWithinAt I s z) :
-    (mfderiv[s] (f - g) z : TangentSpace I z →L[𝕜] E') =
+    (mfderiv[s] (f - g) z : TangentSpace% z →L[𝕜] E') =
       (by exact mfderiv[s] f z) - (by exact mfderiv[s] g z) :=
   (hf.hasMFDerivWithinAt.sub hg.hasMFDerivWithinAt).mfderivWithin hs
 
 theorem mfderiv_sub (hf : MDiffAt f z) (hg : MDiffAt g z) :
-    (mfderiv% (f - g) z : TangentSpace I z →L[𝕜] E') =
+    (mfderiv% (f - g) z : TangentSpace% z →L[𝕜] E') =
       (by exact mfderiv% f z) - (by exact mfderiv% g z) :=
   (hf.hasMFDerivAt.sub hg.hasMFDerivAt).mfderiv
 
@@ -929,7 +930,7 @@ section AlgebraOverRing
 open scoped RightActions
 
 variable {z : M} {F' : Type*} [NormedRing F'] [NormedAlgebra 𝕜 F'] {p q : M → F'}
-  {p' q' : TangentSpace I z →L[𝕜] F'}
+  {p' q' : TangentSpace% z →L[𝕜] F'}
 
 theorem HasMFDerivWithinAt.mul' (hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p')
     (hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q') :
@@ -979,7 +980,7 @@ end AlgebraOverRing
 section AlgebraOverCommRing
 
 variable {z : M} {F' : Type*} [NormedCommRing F'] [NormedAlgebra 𝕜 F'] {p q : M → F'}
-  {p' q' : TangentSpace I z →L[𝕜] F'}
+  {p' q' : TangentSpace% z →L[𝕜] F'}
 
 set_option backward.isDefEq.respectTransparency false in
 theorem HasMFDerivWithinAt.mul (hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p')
@@ -993,7 +994,7 @@ theorem HasMFDerivAt.mul (hp : HasMFDerivAt I 𝓘(𝕜, F') p z p')
   hasMFDerivWithinAt_univ.mp <| hp.hasMFDerivWithinAt.mul hq.hasMFDerivWithinAt
 
 section prod
-variable {ι : Type} {t : Finset ι} {f : ι → M → F'} {f' : ι → TangentSpace I z →L[𝕜] F'}
+variable {ι : Type} {t : Finset ι} {f : ι → M → F'} {f' : ι → TangentSpace% z →L[𝕜] F'}
 
 set_option backward.isDefEq.respectTransparency false in
 lemma HasMFDerivWithinAt.prod [DecidableEq ι]
@@ -1046,7 +1047,7 @@ section DivisionRing
 open scoped RightActions
 
 variable {z : M} {F' : Type*} [NormedDivisionRing F'] [NormedAlgebra 𝕜 F'] {p q : M → F'}
-  {p' q' : TangentSpace I z →L[𝕜] F'}
+  {p' q' : TangentSpace% z →L[𝕜] F'}
 
 lemma HasMFDerivWithinAt.inv' (hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p') (hp_ne : p z ≠ 0) :
     HasMFDerivWithinAt I 𝓘(𝕜, F') (p⁻¹) s z (-((p z)⁻¹ •> p' <• (p z)⁻¹) : E →L[𝕜] F') :=
@@ -1097,7 +1098,7 @@ end DivisionRing
 section Field
 
 variable {z : M} {F' : Type*} [NormedField F'] [NormedAlgebra 𝕜 F'] {p q : M → F'}
-  {p' q' : TangentSpace I z →L[𝕜] F'}
+  {p' q' : TangentSpace% z →L[𝕜] F'}
 
 lemma HasMFDerivWithinAt.inv (hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p') (hp_ne : p z ≠ 0) :
     HasMFDerivWithinAt I 𝓘(𝕜, F') (p⁻¹) s z (-(p z ^ 2)⁻¹ • p' : E →L[𝕜] F') := by
diff --git a/Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean b/Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean
index bbde671e83da07..ea2f7fa9b139b9 100644
--- a/Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean
+++ b/Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean
@@ -35,7 +35,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 /-- The derivative of the chart at a base point is the chart of the tangent bundle, composed with
 the identification between the tangent bundle of the model space and the product space. -/
 theorem tangentMap_chart {p q : TangentBundle I M} (h : q.1 ∈ (chartAt H p.1).source) :
-    tangentMap I I (chartAt H p.1) q =
+    tangentMap% (chartAt H p.1) q =
       (TotalSpace.toProd _ _).symm
         ((chartAt (ModelProd H E) p : TangentBundle I M → ModelProd H E) q) := by
   dsimp [tangentMap]
@@ -48,7 +48,7 @@ tangent bundle, composed with the identification between the tangent bundle of t
 the product space. -/
 theorem tangentMap_chart_symm {p : TangentBundle I M} {q : TangentBundle I H}
     (h : q.1 ∈ (chartAt H p.1).target) :
-    tangentMap I I (chartAt H p.1).symm q =
+    tangentMap% (chartAt H p.1).symm q =
       (chartAt (ModelProd H E) p).symm (TotalSpace.toProd H E q) := by
   dsimp only [tangentMap]
   rw [MDifferentiableAt.mfderiv (mdifferentiableAt_atlas_symm (chart_mem_atlas _ _) h)]
@@ -74,7 +74,7 @@ postcomposing it with derivatives of extended charts.
 Concrete version of `inTangentCoordinates_eq`. -/
 lemma inTangentCoordinates_eq_mfderiv_comp
     {N : Type*} {f : N → M} {g : N → M'}
-    {ϕ : Π x : N, TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)} {x₀ : N} {x : N}
+    {ϕ : Π x : N, TangentSpace% (f x) →L[𝕜] TangentSpace% (g x)} {x₀ : N} {x : N}
     (hx : f x ∈ (chartAt H (f x₀)).source) (hy : g x ∈ (chartAt H' (g x₀)).source) :
     inTangentCoordinates I I' f g ϕ x₀ x =
     (mfderiv% (extChartAt I' (g x₀)) (g x)) ∘L (ϕ x) ∘L
diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean
index cc7ede9c610b4d..24e6737558c2c5 100644
--- a/Mathlib/Geometry/Manifold/Notation.lean
+++ b/Mathlib/Geometry/Manifold/Notation.lean
@@ -37,6 +37,9 @@ including inference of the model with corners.
 | `mfderiv% f x`           | `mfderiv I J f x`                   |
 | `HasMFDerivAt[s] f x f'` | `HasMFDerivWithinAt I J f s x f'`   |
 | `HasMFDerivAt% f x f'`   | `HasMFDerivAt I J f x f'`           |
+| `TangentSpace% x`        | `TangentSpace I x`                  |
+| `tangentMap[s] f`        | `tangentMapWithin I J f s`          |
+| `tangentMap% f`          | `tangentMap I J f`                  |
 
 In each of these cases, the models with corners are inferred from the domain and codomain of `f`.
 The search for models with corners uses the local context and is (almost) only based on expression
@@ -941,6 +944,29 @@ scoped elab:max "HasMFDerivAt%" ppSpace
   let (srcI, tgtI) ← findModels ef none
   mkAppM ``HasMFDerivAt #[srcI, tgtI, ef, ex, ef']
 
+/-- `TangentSpace% x` elaborates to `TangentSpace I x`,
+trying to determine `I` from the local context. -/
+scoped elab:max "TangentSpace%" ppSpace x:term:arg : term => do
+  let ex ← Term.elabTerm x none
+  let extype ← instantiateMVars <| ← inferType ex
+  let src ← findModel extype
+  mkAppM ``TangentSpace #[src, ex]
+
+/-- `tangentMap[s] f` elaborates to `tangentMapWithin I J f s`,
+trying to determine `I` and `J` from the local context. -/
+scoped elab:max "tangentMap[" s:term "]" ppSpace f:term:arg : term => do
+  let es ← Term.elabTerm s none
+  let ef ← ensureIsFunction <|← Term.elabTerm f none
+  let (srcI, tgtI) ← findModels ef none
+  mkAppM ``tangentMapWithin #[srcI, tgtI, ef, es]
+
+/-- `tangentMap% f` elaborates to `tangentMap I J f`,
+trying to determine `I` and `J` from the local context. -/
+scoped elab:max "tangentMap%" ppSpace f:term:arg : term => do
+  let ef ← ensureIsFunction <|← Term.elabTerm f none
+  let (srcI, tgtI) ← findModels ef none
+  mkAppM ``tangentMap #[srcI, tgtI, ef]
+
 end Manifold
 
 section trace
diff --git a/Mathlib/Geometry/Manifold/Riemannian/Basic.lean b/Mathlib/Geometry/Manifold/Riemannian/Basic.lean
index aac89e42f29fcd..7ddda591cfd451 100644
--- a/Mathlib/Geometry/Manifold/Riemannian/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Riemannian/Basic.lean
@@ -66,7 +66,7 @@ variable
 section
 
 variable [PseudoEMetricSpace M] [ChartedSpace H M]
-  [RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
+  [RiemannianBundle (fun (x : M) ↦ TangentSpace% x)]
 
 variable (I M) in
 /-- Consider a manifold in which the tangent spaces are already endowed with an inner product, and
@@ -101,7 +101,7 @@ variable (F) in
 /-- The standard Riemannian metric on a vector space with an inner product, given by this inner
 product on each tangent space. -/
 noncomputable def riemannianMetricVectorSpace :
-    ContMDiffRiemannianMetric 𝓘(ℝ, F) ω F (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x) where
+    ContMDiffRiemannianMetric 𝓘(ℝ, F) ω F (fun (x : F) ↦ TangentSpace% x) where
   inner x := (innerSL ℝ (E := F) : F →L[ℝ] F →L[ℝ] ℝ)
   symm x v w := real_inner_comm _ _
   pos x v hv := real_inner_self_pos.2 hv
@@ -123,19 +123,19 @@ noncomputable def riemannianMetricVectorSpace :
     ext v w
     simp [hom_trivializationAt_apply, ContinuousLinearMap.inCoordinates, TangentSpace]
 
-noncomputable instance : RiemannianBundle (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x) :=
+noncomputable instance : RiemannianBundle (fun (x : F) ↦ TangentSpace% x) :=
   ⟨(riemannianMetricVectorSpace F).toRiemannianMetric⟩
 
 set_option backward.isDefEq.respectTransparency false in
-lemma norm_tangentSpace_vectorSpace {x : F} {v : TangentSpace 𝓘(ℝ, F) x} :
+lemma norm_tangentSpace_vectorSpace {x : F} {v : TangentSpace% x} :
     ‖v‖ = ‖letI V : F := v; V‖ := by
   rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner]
 
-lemma nnnorm_tangentSpace_vectorSpace {x : F} {v : TangentSpace 𝓘(ℝ, F) x} :
+lemma nnnorm_tangentSpace_vectorSpace {x : F} {v : TangentSpace% x} :
     ‖v‖₊ = ‖letI V : F := v; V‖₊ := by
   simp [nnnorm, norm_tangentSpace_vectorSpace]
 
-lemma enorm_tangentSpace_vectorSpace {x : F} {v : TangentSpace 𝓘(ℝ, F) x} :
+lemma enorm_tangentSpace_vectorSpace {x : F} {v : TangentSpace% x} :
     ‖v‖ₑ = ‖letI V : F := v; V‖ₑ := by
   simp [enorm, nnnorm_tangentSpace_vectorSpace]
 
@@ -210,8 +210,8 @@ the image of the neighborhood in the extended chart.
 open Manifold Metric
 open scoped NNReal
 
-variable [RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
-  [IsManifold I 1 M] [IsContinuousRiemannianBundle E (fun (x : M) ↦ TangentSpace I x)]
+variable [RiemannianBundle (fun (x : M) ↦ TangentSpace% x)]
+  [IsManifold I 1 M] [IsContinuousRiemannianBundle E (fun (x : M) ↦ TangentSpace% x)]
 
 /-- Register on the tangent space to a normed vector space the same `NormedAddCommGroup` structure
 as in the vector space.
@@ -220,7 +220,7 @@ Should not be a global instance, as it does not coincide definitionally with the
 structure for inner product spaces, but can be activated locally. -/
 @[instance_reducible]
 def normedAddCommGroupTangentSpaceVectorSpace (x : E) :
-    NormedAddCommGroup (TangentSpace 𝓘(ℝ, E) x) :=
+    NormedAddCommGroup (TangentSpace% x) :=
   inferInstanceAs (NormedAddCommGroup E)
 
 attribute [local instance] normedAddCommGroupTangentSpaceVectorSpace
@@ -231,7 +231,7 @@ as in the vector space.
 Should not be a global instance, as it does not coincide definitionally with the Riemannian
 structure for inner product spaces, but can be activated locally. -/
 @[instance_reducible]
-def normedSpaceTangentSpaceVectorSpace (x : E) : NormedSpace ℝ (TangentSpace 𝓘(ℝ, E) x) :=
+def normedSpaceTangentSpaceVectorSpace (x : E) : NormedSpace ℝ (TangentSpace% x) :=
   inferInstanceAs (NormedSpace ℝ E)
 
 attribute [local instance] normedSpaceTangentSpaceVectorSpace
@@ -241,7 +241,7 @@ variable (I)
 set_option backward.isDefEq.respectTransparency false in
 lemma eventually_norm_mfderiv_extChartAt_lt (x : M) :
     ∃ C > 0, ∀ᶠ y in 𝓝 x, ‖mfderiv% (extChartAt I x) y‖ < C := by
-  rcases eventually_norm_trivializationAt_lt E (fun (x : M) ↦ TangentSpace I x) x
+  rcases eventually_norm_trivializationAt_lt E (fun (x : M) ↦ TangentSpace% x) x
     with ⟨C, C_pos, hC⟩
   refine ⟨C, C_pos, ?_⟩
   have hx : (chartAt H x).source ∈ 𝓝 x := chart_source_mem_nhds H x
@@ -262,7 +262,7 @@ lemma eventually_enorm_mfderiv_extChartAt_lt (x : M) :
 set_option backward.isDefEq.respectTransparency false in
 lemma eventually_norm_mfderivWithin_symm_extChartAt_comp_lt (x : M) :
     ∃ C > 0, ∀ᶠ y in 𝓝 x, ‖mfderiv[range I] (extChartAt I x).symm (extChartAt I x y)‖ < C := by
-  rcases eventually_norm_symmL_trivializationAt_lt E (fun (x : M) ↦ TangentSpace I x) x
+  rcases eventually_norm_symmL_trivializationAt_lt E (fun (x : M) ↦ TangentSpace% x) x
     with ⟨C, C_pos, hC⟩
   refine ⟨C, C_pos, ?_⟩
   have hx : (chartAt H x).source ∈ 𝓝 x := chart_source_mem_nhds H x
diff --git a/Mathlib/Geometry/Manifold/Riemannian/PathELength.lean b/Mathlib/Geometry/Manifold/Riemannian/PathELength.lean
index bc1507a2f8fa13..f41e39caaafe9b 100644
--- a/Mathlib/Geometry/Manifold/Riemannian/PathELength.lean
+++ b/Mathlib/Geometry/Manifold/Riemannian/PathELength.lean
@@ -50,7 +50,7 @@ variable
 
 namespace Manifold
 
-variable [∀ (x : M), ENorm (TangentSpace I x)] {a b c a' b' : ℝ} {γ γ' : ℝ → M}
+variable [∀ (x : M), ENorm (TangentSpace% x)] {a b c a' b' : ℝ} {γ γ' : ℝ → M}
 
 variable (I) in
 /-- The length on `Icc a b` of a path into a manifold, where the path is defined on the whole real
@@ -131,7 +131,7 @@ lemma lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc {a b : ℝ}
 
 open MeasureTheory
 
-variable [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)]
+variable [∀ (x : M), ENormSMulClass ℝ (TangentSpace% x)]
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The length of a path in a manifold is invariant under a monotone reparametrization. -/
@@ -158,7 +158,7 @@ lemma pathELength_comp_of_monotoneOn {f : ℝ → ℝ} (h : a ≤ b) (hf : Monot
       exact uniqueDiffOn_Icc h _ ht
   rw [this]
   simp only [Function.comp_apply, ContinuousLinearMap.comp_apply]
-  have : mfderiv[Icc a b] f t 1 = derivWithin f (Icc a b) t • (1 : TangentSpace 𝓘(ℝ) (f t)) := by
+  have : mfderiv[Icc a b] f t 1 = derivWithin f (Icc a b) t • (1 : TangentSpace% (f t)) := by
     simp only [mfderivWithin_eq_fderivWithin, ← fderivWithin_derivWithin, smul_eq_mul, mul_one]
     rfl
   rw [this]
@@ -191,7 +191,7 @@ lemma pathELength_comp_of_antitoneOn {f : ℝ → ℝ} (h : a ≤ b) (hf : Antit
   rw [this]
   simp only [Function.comp_apply, ContinuousLinearMap.comp_apply]
   have : mfderiv[Icc a b] f t 1
-      = derivWithin f (Icc a b) t • (1 : TangentSpace 𝓘(ℝ) (f t)) := by
+      = derivWithin f (Icc a b) t • (1 : TangentSpace% (f t)) := by
     simp only [mfderivWithin_eq_fderivWithin, ← fderivWithin_derivWithin, smul_eq_mul, mul_one]
     rfl
   rw [this]
@@ -242,7 +242,7 @@ lemma riemannianEDist_le_pathELength {γ : ℝ → M} (hγ : CMDiff[Icc a b] 1 
   · simpa [η, ContinuousAffineMap.coe_lineMap_eq] using hγ.mdifferentiableOn one_ne_zero
   · apply (AffineMap.lineMap_mono hab).monotoneOn
 
-omit [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] in
+omit [∀ (x : M), ENormSMulClass ℝ (TangentSpace% x)] in
 /-- If some `r` is strictly larger than the Riemannian edistance between two points, there exists
 a path between these two points of length `< r`. Here, we get such a path on `[0, 1]`.
 For a more precise version giving locally constant paths around the endpoints, see
diff --git a/Mathlib/Topology/FiberBundle/Constructions.lean b/Mathlib/Topology/FiberBundle/Constructions.lean
index d3dca3611b0892..0e44b40be93d8c 100644
--- a/Mathlib/Topology/FiberBundle/Constructions.lean
+++ b/Mathlib/Topology/FiberBundle/Constructions.lean
@@ -308,7 +308,7 @@ variable [∀ _b, Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass
 noncomputable def Bundle.Trivialization.pullback (e : Trivialization F (π F E)) (f : K) :
     Trivialization F (π F ((f : B' → B) *ᵖ E)) where
   toFun z := (z.proj, (e (Pullback.lift f z)).2)
-  invFun y := @TotalSpace.mk _ F (f *ᵖ E) y.1 (e.symm (f y.1) y.2)
+  invFun y := TotalSpace.mk' F y.1 (e.symm (f y.1) y.2)
   source := Pullback.lift f ⁻¹' e.source
   baseSet := f ⁻¹' e.baseSet
   target := (f ⁻¹' e.baseSet) ×ˢ univ
diff --git a/MathlibTest/DifferentialGeometry/Notation/Basic.lean b/MathlibTest/DifferentialGeometry/Notation/Basic.lean
index 2976d90b7c9fc8..862e96f248d2da 100644
--- a/MathlibTest/DifferentialGeometry/Notation/Basic.lean
+++ b/MathlibTest/DifferentialGeometry/Notation/Basic.lean
@@ -931,7 +931,7 @@ info: ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜
 
 end smoothness
 
--- Inferring the type of `x` for all ContMDiff/MDifferentiable{Within}At elaborators.
+/-! Inferring the type of `x` for all ContMDiff/MDifferentiable{Within}At elaborators. -/
 section
 
 variable {EM' : Type*} [NormedAddCommGroup EM']
@@ -970,6 +970,33 @@ open ContDiff in -- for the ∞ notation
 
 end
 
+/-! Tests for the elaborators for `tangentMap(Within)` and `TangentSpace` -/
+section
+
+variable {f : M → M} {s : Set M} {x : M} {X : TangentSpace% x}
+
+/-- info: TangentSpace I x : Type u_2 -/
+#guard_msgs in
+#check TangentSpace% x
+
+/-- info: tangentMap I I f : TangentBundle I M → TangentBundle I M -/
+#guard_msgs in
+#check tangentMap% f
+
+/-- info: tangentMapWithin I I f s : TangentBundle I M → TangentBundle I M -/
+#guard_msgs in
+#check tangentMap[s] f
+
+/-- info: tangentMap I I f { proj := x, snd := X } : TangentBundle I M -/
+#guard_msgs in
+#check tangentMap% f X
+
+/-- info: tangentMapWithin I I f s { proj := x, snd := X } : TangentBundle I M -/
+#guard_msgs in
+#check tangentMap[s] f X
+
+end
+
 /-! Products of models with corners: TODO, add lots of further tests -/
 section