chore: deprime FiberBundle.contMDiffAt_extend' (leanprover-community#41175)

The original name was primed to avoid ambiguity with `contMDiffAt_extend`: a previous PR moved this
under the `OpenPartialHomeomorph` namespace, so this ambiguity is no longer present.

Author: grunweg

Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean

@@ -687,8 +687,7 @@ lemma exists_contMDiffOn_extend [(x : M) → Module 𝕜 (V x)] [VectorBundle 
   have : CMDiff[t.baseSet] k (fun (_x : M) ↦ w) := contMDiffOn_const
   exact this.congr (fun x hx ↦ by simp [extend, t, w, hx])
 
-lemma contMDiffAt_extend' {x : M} (σ₀ : V x) :
-    CMDiffAt k (T% (extend F σ₀)) x := by
+lemma contMDiffAt_extend {x : M} (σ₀ : V x) : CMDiffAt k (T% (extend F σ₀)) x := by
   rw [contMDiffAt_section]
   set t := trivializationAt F V x
   let w : F := (t ⟨x, σ₀⟩).2
@@ -700,6 +699,8 @@ lemma contMDiffAt_extend' {x : M} (σ₀ : V x) :
     simp [extend, t, hx, w]
   · exact FiberBundle.mem_baseSet_trivializationAt' x
 
+@[deprecated (since := "2026-06-30")] alias contMDiffAt_extend' := contMDiffAt_extend
+
 lemma exists_mdifferentiableOn_extend [∀ x, Module 𝕜 (V x)] [VectorBundle 𝕜 F V]
     [ContMDiffVectorBundle 1 F V I] {x₀ : M} (σ₀ : V x₀) :
     ∃ s ∈ 𝓝 x₀, MDiff[s] (T% (extend F σ₀)) := by
@@ -708,7 +709,7 @@ lemma exists_mdifferentiableOn_extend [∀ x, Module 𝕜 (V x)] [VectorBundle 
 
 lemma mdifferentiableAt_extend {x : M} (σ₀ : V x) :
     MDiffAt (T% (extend F σ₀)) x :=
-  (contMDiffAt_extend' (k := 1) I F σ₀).mdifferentiableAt one_ne_zero
+  (contMDiffAt_extend (k := 1) I F σ₀).mdifferentiableAt one_ne_zero
 
 variable (V) in
 lemma _root_.VectorBundle.injective_eval_mdifferentiableAt_sec [∀ x, Module 𝕜 (V x)]
@@ -728,7 +729,7 @@ lemma _root_.VectorBundle.injective_eval_contMDiffAt_sec {n : WithTop ℕ∞} [
         fun (Z : Π x, V x) (_ : CMDiffAt n (T% Z) x) ↦ A (Z x)) := by
   intro X X' h
   ext σ₀
-  simpa using congr($h (extend F σ₀) (contMDiffAt_extend' ..))
+  simpa using congr($h (extend F σ₀) (contMDiffAt_extend ..))
 
 end FiberBundle
 end extend