From a9a99c531cf7f63aa41a5d76f4d6246626168915 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Mon, 16 Feb 2026 05:40:55 +0100
Subject: [PATCH 1/3] split out code from different branch

---
 .../Manifold/IsManifold/ExtChartAt.lean       | 55 +++++++++++++++++++
 1 file changed, 55 insertions(+)

diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
index cc31a4c1053e2d..39075d78ecd526 100644
--- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
+++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
@@ -370,6 +370,61 @@ theorem contDiffWithinAt_extend_coord_change' [ChartedSpace H M] (hf : f ∈ max
 
 end OpenPartialHomeomorph
 
+namespace ModelWithCorners
+
+/-- The change of charts from `e` to `e'` in the model vector space `E`. -/
+@[simps!]
+def extCoordChange (e e' : OpenPartialHomeomorph M H) : PartialEquiv E E :=
+  (e.extend I).symm.trans (e'.extend I)
+
+variable {e e' : OpenPartialHomeomorph M H}
+
+lemma extCoordChange_symm : (I.extCoordChange e e').symm = I.extCoordChange e' e := by
+  rfl
+
+lemma uniqueDiffOn_extCoordChange_source : UniqueDiffOn 𝕜 (I.extCoordChange e e').source := by
+  rw [extCoordChange_source, inter_assoc, inter_comm, preimage_comp, ← preimage_inter]
+  exact I.uniqueDiffOn_preimage <| e.isOpen_inter_preimage_symm e'.open_source
+
+lemma uniqueDiffOn_extCoordChange_target : UniqueDiffOn 𝕜 (I.extCoordChange e e').target := by
+  rw [← extCoordChange_symm, PartialEquiv.symm_target]
+  exact uniqueDiffOn_extCoordChange_source
+
+variable [ChartedSpace H M] {n : WithTop ℕ∞}
+
+lemma contDiffOn_extCoordChange (he : e ∈ IsManifold.maximalAtlas I n M)
+    (he' : e' ∈ IsManifold.maximalAtlas I n M) :
+    ContDiffOn 𝕜 n (I.extCoordChange e e') (I.extCoordChange e e').source :=
+  e'.contDiffOn_extend_coord_change he' he
+
+lemma contDiffOn_extCoordChange_symm (he : e ∈ IsManifold.maximalAtlas I n M)
+    (he' : e' ∈ IsManifold.maximalAtlas I n M) :
+    ContDiffOn 𝕜 n (I.extCoordChange e e').symm (I.extCoordChange e e').target :=
+  e.contDiffOn_extend_coord_change he he'
+
+lemma isInvertible_fderivWithin_extCoordChange (hn : n ≠ 0) (he : e ∈ IsManifold.maximalAtlas I n M)
+    (he' : e' ∈ IsManifold.maximalAtlas I n M) {x : E} (hx : x ∈ (I.extCoordChange e e').source) :
+    (fderivWithin 𝕜 (I.extCoordChange e e') (I.extCoordChange e e').source x).IsInvertible := by
+  set φ := I.extCoordChange e e'
+  have hφ : ContDiffOn 𝕜 n φ φ.source := I.contDiffOn_extCoordChange he he'
+  have hφ' : ContDiffOn 𝕜 n φ.symm φ.target := I.contDiffOn_extCoordChange_symm he he'
+  refine .of_inverse (g := (fderivWithin 𝕜 φ.symm φ.target (φ x))) ?_ ?_
+  · rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp,
+      fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx), fderivWithin_id]
+    · exact I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx)
+    · exact (φ.left_inv hx ▸ ((hφ _ hx).differentiableWithinAt hn):)
+    · exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn
+    · exact φ.symm_mapsTo
+    · exact I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx)
+  · rw [← fderivWithin_comp, fderivWithin_congr' φ.leftInvOn.eqOn hx, fderivWithin_id]
+    · exact I.uniqueDiffOn_extCoordChange_source _ hx
+    · exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn
+    · exact (hφ _ hx).differentiableWithinAt hn
+    · exact φ.mapsTo
+    · exact I.uniqueDiffOn_extCoordChange_source _ hx
+
+end ModelWithCorners
+
 open OpenPartialHomeomorph
 
 variable [ChartedSpace H M] [ChartedSpace H' M']

From 9002926742b01088c1eb23f7350221f19418170e Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Mon, 16 Feb 2026 05:42:41 +0100
Subject: [PATCH 2/3] rename `extCoordChange` to `extendCoordChange`

---
 .../Manifold/IsManifold/ExtChartAt.lean       | 44 ++++++++++---------
 1 file changed, 23 insertions(+), 21 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
index 39075d78ecd526..3226de17b2bda5 100644
--- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
+++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
@@ -374,54 +374,56 @@ namespace ModelWithCorners
 
 /-- The change of charts from `e` to `e'` in the model vector space `E`. -/
 @[simps!]
-def extCoordChange (e e' : OpenPartialHomeomorph M H) : PartialEquiv E E :=
+def extendCoordChange (e e' : OpenPartialHomeomorph M H) : PartialEquiv E E :=
   (e.extend I).symm.trans (e'.extend I)
 
 variable {e e' : OpenPartialHomeomorph M H}
 
-lemma extCoordChange_symm : (I.extCoordChange e e').symm = I.extCoordChange e' e := by
+lemma extendCoordChange_symm : (I.extendCoordChange e e').symm = I.extendCoordChange e' e := by
   rfl
 
-lemma uniqueDiffOn_extCoordChange_source : UniqueDiffOn 𝕜 (I.extCoordChange e e').source := by
-  rw [extCoordChange_source, inter_assoc, inter_comm, preimage_comp, ← preimage_inter]
+lemma uniqueDiffOn_extendCoordChange_source : UniqueDiffOn 𝕜 (I.extendCoordChange e e').source := by
+  rw [extendCoordChange_source, inter_assoc, inter_comm, preimage_comp, ← preimage_inter]
   exact I.uniqueDiffOn_preimage <| e.isOpen_inter_preimage_symm e'.open_source
 
-lemma uniqueDiffOn_extCoordChange_target : UniqueDiffOn 𝕜 (I.extCoordChange e e').target := by
-  rw [← extCoordChange_symm, PartialEquiv.symm_target]
-  exact uniqueDiffOn_extCoordChange_source
+lemma uniqueDiffOn_extendCoordChange_target : UniqueDiffOn 𝕜 (I.extendCoordChange e e').target := by
+  rw [← extendCoordChange_symm, PartialEquiv.symm_target]
+  exact uniqueDiffOn_extendCoordChange_source
 
 variable [ChartedSpace H M] {n : WithTop ℕ∞}
 
-lemma contDiffOn_extCoordChange (he : e ∈ IsManifold.maximalAtlas I n M)
+lemma contDiffOn_extendCoordChange (he : e ∈ IsManifold.maximalAtlas I n M)
     (he' : e' ∈ IsManifold.maximalAtlas I n M) :
-    ContDiffOn 𝕜 n (I.extCoordChange e e') (I.extCoordChange e e').source :=
+    ContDiffOn 𝕜 n (I.extendCoordChange e e') (I.extendCoordChange e e').source :=
   e'.contDiffOn_extend_coord_change he' he
 
-lemma contDiffOn_extCoordChange_symm (he : e ∈ IsManifold.maximalAtlas I n M)
+lemma contDiffOn_extendCoordChange_symm (he : e ∈ IsManifold.maximalAtlas I n M)
     (he' : e' ∈ IsManifold.maximalAtlas I n M) :
-    ContDiffOn 𝕜 n (I.extCoordChange e e').symm (I.extCoordChange e e').target :=
+    ContDiffOn 𝕜 n (I.extendCoordChange e e').symm (I.extendCoordChange e e').target :=
   e.contDiffOn_extend_coord_change he he'
 
-lemma isInvertible_fderivWithin_extCoordChange (hn : n ≠ 0) (he : e ∈ IsManifold.maximalAtlas I n M)
-    (he' : e' ∈ IsManifold.maximalAtlas I n M) {x : E} (hx : x ∈ (I.extCoordChange e e').source) :
-    (fderivWithin 𝕜 (I.extCoordChange e e') (I.extCoordChange e e').source x).IsInvertible := by
-  set φ := I.extCoordChange e e'
-  have hφ : ContDiffOn 𝕜 n φ φ.source := I.contDiffOn_extCoordChange he he'
-  have hφ' : ContDiffOn 𝕜 n φ.symm φ.target := I.contDiffOn_extCoordChange_symm he he'
+lemma isInvertible_fderivWithin_extendCoordChange (hn : n ≠ 0)
+    (he : e ∈ IsManifold.maximalAtlas I n M) (he' : e' ∈ IsManifold.maximalAtlas I n M)
+    {x : E} (hx : x ∈ (I.extendCoordChange e e').source) :
+    ContinuousLinearMap.IsInvertible <|
+      fderivWithin 𝕜 (I.extendCoordChange e e') (I.extendCoordChange e e').source x := by
+  set φ := I.extendCoordChange e e'
+  have hφ : ContDiffOn 𝕜 n φ φ.source := I.contDiffOn_extendCoordChange he he'
+  have hφ' : ContDiffOn 𝕜 n φ.symm φ.target := I.contDiffOn_extendCoordChange_symm he he'
   refine .of_inverse (g := (fderivWithin 𝕜 φ.symm φ.target (φ x))) ?_ ?_
   · rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp,
       fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx), fderivWithin_id]
-    · exact I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx)
+    · exact I.uniqueDiffOn_extendCoordChange_source _ (φ.map_source hx)
     · exact (φ.left_inv hx ▸ ((hφ _ hx).differentiableWithinAt hn):)
     · exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn
     · exact φ.symm_mapsTo
-    · exact I.uniqueDiffOn_extCoordChange_source _ (φ.map_source hx)
+    · exact I.uniqueDiffOn_extendCoordChange_source _ (φ.map_source hx)
   · rw [← fderivWithin_comp, fderivWithin_congr' φ.leftInvOn.eqOn hx, fderivWithin_id]
-    · exact I.uniqueDiffOn_extCoordChange_source _ hx
+    · exact I.uniqueDiffOn_extendCoordChange_source _ hx
     · exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn
     · exact (hφ _ hx).differentiableWithinAt hn
     · exact φ.mapsTo
-    · exact I.uniqueDiffOn_extCoordChange_source _ hx
+    · exact I.uniqueDiffOn_extendCoordChange_source _ hx
 
 end ModelWithCorners
 

From c9d9f727e4add9f0fe1f4bb738b1ca0f959871e3 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Mon, 16 Feb 2026 07:52:17 +0100
Subject: [PATCH 3/3] merge with original `extend_coord_change` API

---
 .../Manifold/IsManifold/ExtChartAt.lean       | 161 ++++++++++--------
 .../Manifold/VectorBundle/Tangent.lean        |  18 +-
 scripts/nolints_prime_decls.txt               |   2 +
 3 files changed, 102 insertions(+), 79 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
index 3226de17b2bda5..f59e2650d12ba9 100644
--- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
+++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
@@ -23,11 +23,12 @@ in general, but we can still register them as `PartialEquiv`s.
 * `extChartAt I x`: the extended chart at `x`, obtained by composing the `chartAt H x` with `I`.
   Since the target is in general not open, this is not an open partial homeomorphism in general, but
   we register them as `PartialEquiv`s.
+* `I.extendCoordChange e e'`: the change of extended charts `(e.extend I).symm ≫ e'.extend I`.
 
 ## Main results
 
-* `contDiffOn_extend_coord_change`: if `f` and `f'` lie in the maximal atlas on `M`,
-  `f.extend I ∘ (f'.extend I).symm` is continuous on its source
+* `ModelWithCorners.contDiffOn_extendCoordChange`: if `f` and `f'` lie in the maximal atlas on `M`,
+  `I.extendCoordChange f f'` is Cⁿ on its source
 
 * `contDiffOn_ext_coord_change`: for `x x' : M`, the coordinate change
   `(extChartAt I x').symm ≫ extChartAt I x` is continuous on its source
@@ -315,95 +316,91 @@ theorem extend_symm_preimage_inter_range_eventuallyEq {s : Set M} {x : M} (hs :
 lemma extend_prod (f' : OpenPartialHomeomorph M' H') :
     (f.prod f').extend (I.prod I') = (f.extend I).prod (f'.extend I') := by simp
 
-/-! We use the name `extend_coord_change` for `(f'.extend I).symm ≫ f.extend I`. -/
-
-theorem extend_coord_change_source :
-    ((f.extend I).symm ≫ f'.extend I).source = I '' (f.symm ≫ₕ f').source := by
-  simp_rw [PartialEquiv.trans_source, I.image_eq, extend_source, PartialEquiv.symm_source,
-    extend_target, inter_right_comm _ (range I)]
-  rfl
-
-theorem extend_image_source_inter :
-    f.extend I '' (f.source ∩ f'.source) = ((f.extend I).symm ≫ f'.extend I).source := by
-  simp_rw [f.extend_coord_change_source, f.extend_coe, image_comp I f, trans_source'', symm_symm,
-    symm_target]
-
-theorem extend_coord_change_source_mem_nhdsWithin {x : E}
-    (hx : x ∈ ((f.extend I).symm ≫ f'.extend I).source) :
-    ((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range I] x := by
-  rw [f.extend_coord_change_source] at hx ⊢
-  obtain ⟨x, hx, rfl⟩ := hx
-  refine I.image_mem_nhdsWithin ?_
-  exact (OpenPartialHomeomorph.open_source _).mem_nhds hx
-
-theorem extend_coord_change_source_mem_nhdsWithin' {x : M} (hxf : x ∈ f.source)
-    (hxf' : x ∈ f'.source) :
-    ((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range I] f.extend I x := by
-  apply extend_coord_change_source_mem_nhdsWithin
-  rw [← extend_image_source_inter]
-  exact mem_image_of_mem _ ⟨hxf, hxf'⟩
-
-variable {f f'}
-
-open IsManifold
-
-theorem contDiffOn_extend_coord_change [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
-    (hf' : f' ∈ maximalAtlas I n M) :
-    ContDiffOn 𝕜 n (f.extend I ∘ (f'.extend I).symm) ((f'.extend I).symm ≫ f.extend I).source := by
-  rw [extend_coord_change_source, I.image_eq]
-  exact (StructureGroupoid.compatible_of_mem_maximalAtlas hf' hf).1
-
-theorem contDiffWithinAt_extend_coord_change [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
-    (hf' : f' ∈ maximalAtlas I n M) {x : E} (hx : x ∈ ((f'.extend I).symm ≫ f.extend I).source) :
-    ContDiffWithinAt 𝕜 n (f.extend I ∘ (f'.extend I).symm) (range I) x := by
-  apply (contDiffOn_extend_coord_change hf hf' x hx).mono_of_mem_nhdsWithin
-  rw [extend_coord_change_source] at hx ⊢
-  obtain ⟨z, hz, rfl⟩ := hx
-  exact I.image_mem_nhdsWithin ((OpenPartialHomeomorph.open_source _).mem_nhds hz)
-
-theorem contDiffWithinAt_extend_coord_change' [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
-    (hf' : f' ∈ maximalAtlas I n M) {x : M} (hxf : x ∈ f.source) (hxf' : x ∈ f'.source) :
-    ContDiffWithinAt 𝕜 n (f.extend I ∘ (f'.extend I).symm) (range I) (f'.extend I x) := by
-  refine contDiffWithinAt_extend_coord_change hf hf' ?_
-  rw [← extend_image_source_inter]
-  exact mem_image_of_mem _ ⟨hxf', hxf⟩
-
 end OpenPartialHomeomorph
 
 namespace ModelWithCorners
 
 /-- The change of charts from `e` to `e'` in the model vector space `E`. -/
-@[simps!]
+@[simps! apply symm_apply]
 def extendCoordChange (e e' : OpenPartialHomeomorph M H) : PartialEquiv E E :=
-  (e.extend I).symm.trans (e'.extend I)
+  (e.extend I).symm ≫ e'.extend I
 
 variable {e e' : OpenPartialHomeomorph M H}
 
 lemma extendCoordChange_symm : (I.extendCoordChange e e').symm = I.extendCoordChange e' e := by
   rfl
 
+lemma extendCoordChange_source :
+    (I.extendCoordChange e e').source = I '' (e.symm ≫ₕ e').source := by
+  simp_rw [extendCoordChange, PartialEquiv.trans_source, I.image_eq, e'.extend_source,
+    PartialEquiv.symm_source, e.extend_target, inter_right_comm _ (range I)]
+  rfl
+
+lemma extendCoordChange_target :
+    (I.extendCoordChange e e').target = I '' (e.symm ≫ₕ e').target := by
+  rw [← PartialEquiv.symm_source, ← OpenPartialHomeomorph.symm_source]
+  exact I.extendCoordChange_source
+
+lemma _root_.OpenPartialHomeomorph.extend_image_source_inter :
+    f.extend I '' (f.source ∩ f'.source) = (I.extendCoordChange f f').source := by
+  simp_rw [I.extendCoordChange_source, f.extend_coe, image_comp I f,
+    OpenPartialHomeomorph.trans_source'', OpenPartialHomeomorph.symm_symm,
+    OpenPartialHomeomorph.symm_target]
+
+lemma extendCoordChange_source_mem_nhdsWithin {x : E}
+    (hx : x ∈ (I.extendCoordChange e e').source) :
+    (I.extendCoordChange e e').source ∈ 𝓝[range I] x := by
+  rw [I.extendCoordChange_source] at hx ⊢
+  obtain ⟨x, hx, rfl⟩ := hx
+  refine I.image_mem_nhdsWithin ?_
+  exact (OpenPartialHomeomorph.open_source _).mem_nhds hx
+
+lemma extendCoordChange_source_mem_nhdsWithin' {x : M} (hxe : x ∈ e.source)
+    (hxe' : x ∈ e'.source) :
+    (I.extendCoordChange e e').source ∈ 𝓝[range I] e.extend I x := by
+  apply extendCoordChange_source_mem_nhdsWithin
+  rw [← OpenPartialHomeomorph.extend_image_source_inter]
+  exact mem_image_of_mem _ ⟨hxe, hxe'⟩
+
 lemma uniqueDiffOn_extendCoordChange_source : UniqueDiffOn 𝕜 (I.extendCoordChange e e').source := by
-  rw [extendCoordChange_source, inter_assoc, inter_comm, preimage_comp, ← preimage_inter]
+  rw [extendCoordChange_source, I.image_eq]
   exact I.uniqueDiffOn_preimage <| e.isOpen_inter_preimage_symm e'.open_source
 
 lemma uniqueDiffOn_extendCoordChange_target : UniqueDiffOn 𝕜 (I.extendCoordChange e e').target := by
   rw [← extendCoordChange_symm, PartialEquiv.symm_target]
   exact uniqueDiffOn_extendCoordChange_source
 
-variable [ChartedSpace H M] {n : WithTop ℕ∞}
+open IsManifold
+
+variable [ChartedSpace H M]
 
-lemma contDiffOn_extendCoordChange (he : e ∈ IsManifold.maximalAtlas I n M)
-    (he' : e' ∈ IsManifold.maximalAtlas I n M) :
-    ContDiffOn 𝕜 n (I.extendCoordChange e e') (I.extendCoordChange e e').source :=
-  e'.contDiffOn_extend_coord_change he' he
+lemma contDiffOn_extendCoordChange (he : e ∈ maximalAtlas I n M) (he' : e' ∈ maximalAtlas I n M) :
+    ContDiffOn 𝕜 n (I.extendCoordChange e e') (I.extendCoordChange e e').source := by
+  rw [I.extendCoordChange_source, I.image_eq]
+  exact (StructureGroupoid.compatible_of_mem_maximalAtlas he he').1
 
-lemma contDiffOn_extendCoordChange_symm (he : e ∈ IsManifold.maximalAtlas I n M)
-    (he' : e' ∈ IsManifold.maximalAtlas I n M) :
+lemma contDiffWithinAt_extendCoordChange (he : e ∈ maximalAtlas I n M)
+    (he' : e' ∈ maximalAtlas I n M) {x : E} (hx : x ∈ (I.extendCoordChange e e').source) :
+    ContDiffWithinAt 𝕜 n (I.extendCoordChange e e') (range I) x := by
+  apply (I.contDiffOn_extendCoordChange he he' x hx).mono_of_mem_nhdsWithin
+  rw [I.extendCoordChange_source] at hx ⊢
+  obtain ⟨z, hz, rfl⟩ := hx
+  exact I.image_mem_nhdsWithin ((OpenPartialHomeomorph.open_source _).mem_nhds hz)
+
+lemma contDiffWithinAt_extendCoordChange' (he : e ∈ maximalAtlas I n M)
+    (he' : e' ∈ maximalAtlas I n M) {x : M} (hxe : x ∈ e.source) (hxe' : x ∈ e'.source) :
+    ContDiffWithinAt 𝕜 n (I.extendCoordChange e e') (range I) (e.extend I x) := by
+  refine I.contDiffWithinAt_extendCoordChange he he' ?_
+  rw [← OpenPartialHomeomorph.extend_image_source_inter]
+  exact mem_image_of_mem _ ⟨hxe, hxe'⟩
+
+lemma contDiffOn_extendCoordChange_symm (he : e ∈ maximalAtlas I n M)
+    (he' : e' ∈ maximalAtlas I n M) :
     ContDiffOn 𝕜 n (I.extendCoordChange e e').symm (I.extendCoordChange e e').target :=
-  e.contDiffOn_extend_coord_change he he'
+  I.contDiffOn_extendCoordChange he' he
 
 lemma isInvertible_fderivWithin_extendCoordChange (hn : n ≠ 0)
-    (he : e ∈ IsManifold.maximalAtlas I n M) (he' : e' ∈ IsManifold.maximalAtlas I n M)
+    (he : e ∈ maximalAtlas I n M) (he' : e' ∈ maximalAtlas I n M)
     {x : E} (hx : x ∈ (I.extendCoordChange e e').source) :
     ContinuousLinearMap.IsInvertible <|
       fderivWithin 𝕜 (I.extendCoordChange e e') (I.extendCoordChange e e').source x := by
@@ -427,6 +424,30 @@ lemma isInvertible_fderivWithin_extendCoordChange (hn : n ≠ 0)
 
 end ModelWithCorners
 
+namespace OpenPartialHomeomorph
+
+@[deprecated (since := "2026-02-16")]
+alias extend_coord_change_source := ModelWithCorners.extendCoordChange_source
+
+@[deprecated (since := "2026-02-16")]
+alias extend_coord_change_source_mem_nhdsWithin :=
+  ModelWithCorners.extendCoordChange_source_mem_nhdsWithin
+
+@[deprecated (since := "2026-02-16")]
+alias extend_coord_change_source_mem_nhdsWithin' :=
+  ModelWithCorners.extendCoordChange_source_mem_nhdsWithin'
+
+@[deprecated (since := "2026-02-16")]
+alias contDiffOn_extend_coord_change := ModelWithCorners.contDiffOn_extendCoordChange
+
+@[deprecated (since := "2026-02-16")]
+alias contDiffWithinAt_extend_coord_change := ModelWithCorners.contDiffWithinAt_extendCoordChange
+
+@[deprecated (since := "2026-02-16")]
+alias contDiffWithinAt_extend_coord_change' := ModelWithCorners.contDiffWithinAt_extendCoordChange'
+
+end OpenPartialHomeomorph
+
 open OpenPartialHomeomorph
 
 variable [ChartedSpace H M] [ChartedSpace H' M']
@@ -764,19 +785,19 @@ theorem ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq
 theorem ext_coord_change_source (x x' : M) :
     ((extChartAt I x').symm ≫ extChartAt I x).source =
       I '' ((chartAt H x').symm ≫ₕ chartAt H x).source :=
-  extend_coord_change_source _ _
+  I.extendCoordChange_source
 
 open IsManifold
 
 theorem contDiffOn_ext_coord_change [IsManifold I n M] (x x' : M) :
     ContDiffOn 𝕜 n (extChartAt I x ∘ (extChartAt I x').symm)
       ((extChartAt I x').symm ≫ extChartAt I x).source :=
-  contDiffOn_extend_coord_change (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas x')
+  I.contDiffOn_extendCoordChange (chart_mem_maximalAtlas x') (chart_mem_maximalAtlas x)
 
 theorem contDiffWithinAt_ext_coord_change [IsManifold I n M] (x x' : M) {y : E}
     (hy : y ∈ ((extChartAt I x').symm ≫ extChartAt I x).source) :
     ContDiffWithinAt 𝕜 n (extChartAt I x ∘ (extChartAt I x').symm) (range I) y :=
-  contDiffWithinAt_extend_coord_change (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas x') hy
+  I.contDiffWithinAt_extendCoordChange (chart_mem_maximalAtlas x') (chart_mem_maximalAtlas x) hy
 
 variable (I I') in
 /-- Conjugating a function to write it in the preferred charts around `x`.
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
index a29cd44c5a3336..777183a3a51bd4 100644
--- a/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
+++ b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
@@ -60,13 +60,13 @@ theorem contDiffOn_fderiv_coord_change [IsManifold I (n + 1) M]
     ContDiffOn 𝕜 n (fderivWithin 𝕜 (j.1.extend I ∘ (i.1.extend I).symm) (range I))
       ((i.1.extend I).symm ≫ j.1.extend I).source := by
   have h : ((i.1.extend I).symm ≫ j.1.extend I).source ⊆ range I := by
-    rw [i.1.extend_coord_change_source]; apply image_subset_range
+    refine I.extendCoordChange_source.trans_subset ?_; apply image_subset_range
   intro x hx
   refine (ContDiffWithinAt.fderivWithin_right ?_ I.uniqueDiffOn le_rfl
     <| h hx).mono h
-  refine (OpenPartialHomeomorph.contDiffOn_extend_coord_change (subset_maximalAtlas j.2)
-    (subset_maximalAtlas i.2) x hx).mono_of_mem_nhdsWithin ?_
-  exact i.1.extend_coord_change_source_mem_nhdsWithin j.1 hx
+  refine (I.contDiffOn_extendCoordChange (subset_maximalAtlas i.2)
+    (subset_maximalAtlas j.2) x hx).mono_of_mem_nhdsWithin ?_
+  exact I.extendCoordChange_source_mem_nhdsWithin hx
 
 open IsManifold
 
@@ -101,7 +101,7 @@ def tangentBundleCore : VectorBundleCore 𝕜 M E (atlas H M) where
     refine (contDiffOn_fderiv_coord_change (n := 0) i j).continuousOn.comp
       (i.1.continuousOn_extend.mono ?_) ?_
     · rw [i.1.extend_source]; exact inter_subset_left
-    simp_rw [← i.1.extend_image_source_inter, mapsTo_image]
+    exact mapsTo_iff_image_subset.2 (i.1.extend_image_source_inter j.1).subset
   coordChange_comp := by
     have : IsManifold I (0 + 1) M := by simpa
     rintro i j k x ⟨⟨hxi, hxj⟩, hxk⟩ v
@@ -110,10 +110,10 @@ def tangentBundleCore : VectorBundleCore 𝕜 M E (atlas H M) where
       filter_upwards [nhdsWithin_le_nhds this] with y hy
       simp_rw [Function.comp_apply, (j.1.extend I).left_inv hy]
     · simp_rw [Function.comp_apply, i.1.extend_left_inv hxi, j.1.extend_left_inv hxj]
-    · exact (contDiffWithinAt_extend_coord_change' (subset_maximalAtlas k.2)
-        (subset_maximalAtlas j.2) hxk hxj).differentiableWithinAt one_ne_zero
-    · exact (contDiffWithinAt_extend_coord_change' (subset_maximalAtlas j.2)
-        (subset_maximalAtlas i.2) hxj hxi).differentiableWithinAt one_ne_zero
+    · exact (I.contDiffWithinAt_extendCoordChange' (subset_maximalAtlas j.2)
+        (subset_maximalAtlas k.2) hxj hxk).differentiableWithinAt one_ne_zero
+    · exact (I.contDiffWithinAt_extendCoordChange' (subset_maximalAtlas i.2)
+        (subset_maximalAtlas j.2) hxi hxj).differentiableWithinAt one_ne_zero
     · intro x _; exact mem_range_self _
     · exact I.uniqueDiffWithinAt_image
     · rw [Function.comp_apply, i.1.extend_left_inv hxi]
diff --git a/scripts/nolints_prime_decls.txt b/scripts/nolints_prime_decls.txt
index 66e6d86a092535..867080b969beee 100644
--- a/scripts/nolints_prime_decls.txt
+++ b/scripts/nolints_prime_decls.txt
@@ -3028,6 +3028,8 @@ Miu.le_pow2_and_pow2_eq_mod3'
 mk_eq_mk_of_basis'
 Mod_.comp_hom'
 Mod_.id_hom'
+ModelWithCorners.contDiffWithinAt_extendCoordChange'
+ModelWithCorners.extendCoordChange_source_mem_nhdsWithin'
 ModularCyclotomicCharacter.toFun_spec'
 ModularCyclotomicCharacter.toFun_spec''
 ModularCyclotomicCharacter.toFun_unique'