-- Mathlib/Geometry/Manifold/VectorField.lean
lemma _root_.MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField
    (hV : MDifferentiableWithinAt I I.tangent (fun x ↦ (V x : TangentBundle I M)) s x) :
    DifferentiableWithinAt 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm V (range I))
    ((extChartAt I x).symm ⁻¹' s ∩ range I) (extChartAt I x x)

Proof state:
case a
𝕜 : 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
s : Set M
x : M
V : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) s x
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
have := MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq hV
  (contMDiffWithinAt_extChartAt_symm_range x (mem_extChartAt_target x))
  (isInvertible_mfderivWithin_extChartAt_symm (mem_extChartAt_target x)) (mem_range_self _)
  I.uniqueMDiffOn le_rfl (extChartAt_to_inv x).symm

Result:
case a
𝕜 : 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
s : Set M
x : M
V : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) s x
this :
  MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent
    (fun y => { proj := y, snd := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) y })
    (range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Proof state:
case a
𝕜 : 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
s : Set M
x : M
V : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) s x
this :
  MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent
    (fun y => { proj := y, snd := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) y })
    (range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
rw [inter_comm]

Result:
case a
𝕜 : 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
s : Set M
x : M
V : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) s x
this :
  MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent
    (fun y => { proj := y, snd := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) y })
    (range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) 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
s : Set M
x : M
V : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) s x
⊢ DifferentiableWithinAt 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
apply MDifferentiableWithinAt.differentiableWithinAt

Result:
case a
𝕜 : 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
s : Set M
x : M
V : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) s x
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Proof state:
case a
𝕜 : 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
s : Set M
x : M
V : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) s x
this :
  MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent
    (fun y => { proj := y, snd := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) y })
    (range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)

Tactic:
exact ((contMDiff_snd_tangentBundle_modelSpace E 𝓘(𝕜, E)).contMDiffAt.mdifferentiableAt
  le_rfl).comp_mdifferentiableWithinAt _ this

Result:
no goals