-- Mathlib/Geometry/Manifold/VectorField.lean
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version within a set at a point. -/
protected lemma _root_.MDifferentiableWithinAt.mpullbackWithin_vectorField_inter
    (hV : MDifferentiableWithinAt I' I'.tangent
      (fun (y : M') ↦ (V y : TangentBundle I' M')) t (f x₀))
    (hf : ContMDiffWithinAt I I' n f s x₀) (hf' : (mfderivWithin I I' f s x₀).IsInvertible)
    (hx₀ : x₀ ∈ s) (hs : UniqueMDiffOn I s) (hmn : 2 ≤ n) :
    MDifferentiableWithinAt I I.tangent
      (fun (y : M) ↦ (mpullbackWithin I I' f V s y : TangentBundle I M)) (s ∩ f ⁻¹' t) x₀

Proof state:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
n : WithTop ℕ∞
t : Set M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I' I'.tangent (fun y => { proj := y, snd := V y }) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderivWithin I I' f s x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : 2 ≤ n
b₁ : M → M' := f
b₂ : M → M := _root_.id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x => (mfderivWithin I I' f s x).inverse
hv : MDifferentiableWithinAt I I'.tangent (fun x => { proj := f x, snd := v x }) (s ∩ f ⁻¹' t) x₀
⊢ MDifferentiableWithinAt I I.tangent (fun y => { proj := y, snd := mpullbackWithin I I' f V s y }) (s ∩ f ⁻¹' t) x₀

Tactic:
suffices hϕ : MDifferentiableWithinAt I 𝓘(𝕜, E' →L[𝕜] E)
    (fun (x : M) ↦ ContinuousLinearMap.inCoordinates
      E' (TangentSpace I' (M := M')) E (TangentSpace I (M := M))
      (b₁ x₀) (b₁ x) (b₂ x₀) (b₂ x) (ϕ x)) s x₀ from
  MDifferentiableWithinAt.clm_apply_of_inCoordinates (hϕ.mono inter_subset_left)
    hv mdifferentiableWithinAt_id

Result:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
n : WithTop ℕ∞
t : Set M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I' I'.tangent (fun y => { proj := y, snd := V y }) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderivWithin I I' f s x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : 2 ≤ n
b₁ : M → M' := f
b₂ : M → M := _root_.id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x => (mfderivWithin I I' f s x).inverse
hv : MDifferentiableWithinAt I I'.tangent (fun x => { proj := f x, snd := v x }) (s ∩ f ⁻¹' t) x₀
⊢ MDifferentiableWithinAt I 𝓘(𝕜, E' →L[𝕜] E)
    (fun x => inCoordinates E' (TangentSpace I') E (TangentSpace I) (b₁ x₀) (b₁ x) (b₂ x₀) (b₂ x) (ϕ x)) s x₀

Proof state:
case a.he
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
n : WithTop ℕ∞
t : Set M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I' I'.tangent (fun y => { proj := y, snd := V y }) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderivWithin I I' f s x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : 2 ≤ n
b₁ : M → M' := f
b₂ : M → M := _root_.id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x => (mfderivWithin I I' f s x).inverse
hv : MDifferentiableWithinAt I I'.tangent (fun x => { proj := f x, snd := v x }) (s ∩ f ⁻¹' t) x₀
this :
  MDifferentiableWithinAt I 𝓘(𝕜, E →L[𝕜] E')
    (fun x => inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x)) s x₀
⊢ (inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x₀ (f x₀) (f x₀) (mfderivWithin I I' f s x₀)).IsInvertible

Tactic:
rw [inCoordinates_eq (FiberBundle.mem_baseSet_trivializationAt' x₀)
  (FiberBundle.mem_baseSet_trivializationAt' (f x₀))]

Result:
case a.he
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
n : WithTop ℕ∞
t : Set M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I' I'.tangent (fun y => { proj := y, snd := V y }) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderivWithin I I' f s x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : 2 ≤ n
b₁ : M → M' := f
b₂ : M → M := _root_.id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x => (mfderivWithin I I' f s x).inverse
hv : MDifferentiableWithinAt I I'.tangent (fun x => { proj := f x, snd := v x }) (s ∩ f ⁻¹' t) x₀
this :
  MDifferentiableWithinAt I 𝓘(𝕜, E →L[𝕜] E')
    (fun x => inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderivWithin I I' f s x)) s x₀
⊢ ((↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (f x₀)) (f x₀) ⋯)).comp
      ((mfderivWithin I I' f s x₀).comp
        ↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x₀ ⋯).symm)).IsInvertible