-- Mathlib/Analysis/Calculus/VectorField.lean
lemma DifferentiableWithinAt.pullbackWithin {f : E → F} {V : F → F} {s : Set E} {t : Set F} {x : E}
    (hV : DifferentiableWithinAt 𝕜 V t (f x))
    (hf : ContDiffWithinAt 𝕜 2 f s x) (hf' : (fderivWithin 𝕜 f s x).IsInvertible)
    (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hst : MapsTo f s t) :
    DifferentiableWithinAt 𝕜 (pullbackWithin 𝕜 f V s) s x

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y => ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
⊢ DifferentiableWithinAt 𝕜 (VectorField.pullbackWithin 𝕜 f V s) s x

Tactic:
simp only [pullbackWithin_eq]

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y => ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
⊢ DifferentiableWithinAt 𝕜 (fun x => (fderivWithin 𝕜 f s x).inverse (V (f x))) s x

Proof state:
case intro.intro.intro.intro.h₁
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y => ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (fun y => ↑(M y).symm (V (f y))) s x
⊢ (fun x => (fderivWithin 𝕜 f s x).inverse (V (f x))) =ᶠ[𝓝[s] x] fun y => ↑(M y).symm (V (f y))

Tactic:
filter_upwards [hM] with y hy using by simp [← hy]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y => ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
⊢ DifferentiableWithinAt 𝕜 (fun y => ↑(M y).symm (V (f y))) s x

Tactic:
apply DifferentiableWithinAt.clm_apply

Result:
case hc
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y => ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
⊢ DifferentiableWithinAt 𝕜 (fun y => ↑(M y).symm) s x

case hu
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y => ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
⊢ DifferentiableWithinAt 𝕜 (fun y => V (f y)) s x

Proof state:
case intro.intro.intro.intro.hx
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y => ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (fun y => ↑(M y).symm (V (f y))) s x
⊢ (fderivWithin 𝕜 f s x).inverse (V (f x)) = ↑(M x).symm (V (f x))

Tactic:
have hMx : M x = fderivWithin 𝕜 f s x := by apply mem_of_mem_nhdsWithin hx hM

Result:
case intro.intro.intro.intro.hx
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y => ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (fun y => ↑(M y).symm (V (f y))) s x
hMx : ↑(M x) = fderivWithin 𝕜 f s x
⊢ (fderivWithin 𝕜 f s x).inverse (V (f x)) = ↑(M x).symm (V (f x))

Proof state:
case hu
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y => ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
⊢ DifferentiableWithinAt 𝕜 (fun y => V (f y)) s x

Tactic:
exact hV.comp _ (hf.differentiableWithinAt one_le_two) hst

Result:
no goals