-- Mathlib/Geometry/Manifold/VectorField.lean
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version within a set at a point, with a set used for the pullback possibly larger. -/
protected lemma _root_.ContMDiffWithinAt.mpullbackWithin_vectorField' {u : Set M}
    (hV : ContMDiffWithinAt I' I'.tangent m
      (fun (y : M') ↦ (V y : TangentBundle I' M')) t (f x₀))
    (hf : ContMDiffWithinAt I I' n f u x₀) (hf' : (mfderivWithin I I' f u x₀).IsInvertible)
    (hx₀ : x₀ ∈ s) (hs : UniqueMDiffOn I s) (hmn : m + 1 ≤ n)
    (hst : f ⁻¹' t ∈ 𝓝[s] x₀) (hu : s ⊆ u) :
    ContMDiffWithinAt I I.tangent m
      (fun (y : M) ↦ (mpullbackWithin I I' f V u y : TangentBundle I M)) s 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
m n : WithTop ℕ∞
t : Set M'
inst✝⁴ : IsManifold I n M
inst✝³ : IsManifold I' n M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
u : Set M
hV : ContMDiffWithinAt I' I'.tangent m (fun y => { proj := y, snd := V y }) t (f x₀)
hf : ContMDiffWithinAt I I' n f u x₀
hf' : (mfderivWithin I I' f u x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : ↑1 ≤ n
hh : (mfderivWithin I I' f s x₀).IsInvertible
Y : ∀ᶠ (x' : M) in 𝓝[u] x₀, ContMDiffWithinAt I I' (↑1) f u x'
⊢ (fun y => { proj := y, snd := mpullbackWithin I I' f V u y }) =ᶠ[𝓝[s] x₀] fun y =>
    { proj := y, snd := mpullbackWithin I I' f V s y }

Tactic:
filter_upwards [self_mem_nhdsWithin, nhdsWithin_mono _ hu Y] with y hy h'y

Result:
case h
𝕜 : 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
m n : WithTop ℕ∞
t : Set M'
inst✝⁴ : IsManifold I n M
inst✝³ : IsManifold I' n M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
u : Set M
hV : ContMDiffWithinAt I' I'.tangent m (fun y => { proj := y, snd := V y }) t (f x₀)
hf : ContMDiffWithinAt I I' n f u x₀
hf' : (mfderivWithin I I' f u x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : ↑1 ≤ n
hh : (mfderivWithin I I' f s x₀).IsInvertible
Y : ∀ᶠ (x' : M) in 𝓝[u] x₀, ContMDiffWithinAt I I' (↑1) f u x'
y : M
hy : y ∈ s
h'y : ContMDiffWithinAt I I' (↑1) f u y
⊢ { proj := y, snd := mpullbackWithin I I' f V u y } = { proj := y, snd := mpullbackWithin I I' f V s y }

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
m n : WithTop ℕ∞
t : Set M'
inst✝⁴ : IsManifold I n M
inst✝³ : IsManifold I' n M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
u : Set M
hV : ContMDiffWithinAt I' I'.tangent m (fun y => { proj := y, snd := V y }) t (f x₀)
hf : ContMDiffWithinAt I I' n f u x₀
hf' : (mfderivWithin I I' f u x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : ↑1 ≤ n
hh : (mfderivWithin I I' f s x₀).IsInvertible
⊢ ContMDiffWithinAt I I.tangent m (fun y => { proj := y, snd := mpullbackWithin I I' f V u y }) s x₀

Tactic:
apply (hV.mpullbackWithin_vectorField_of_mem (hf.mono hu) hh hx₀ hs hmn
  hst).congr_of_eventuallyEq_of_mem _ hx₀

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
m n : WithTop ℕ∞
t : Set M'
inst✝⁴ : IsManifold I n M
inst✝³ : IsManifold I' n M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
u : Set M
hV : ContMDiffWithinAt I' I'.tangent m (fun y => { proj := y, snd := V y }) t (f x₀)
hf : ContMDiffWithinAt I I' n f u x₀
hf' : (mfderivWithin I I' f u x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : ↑1 ≤ n
hh : (mfderivWithin I I' f s x₀).IsInvertible
⊢ (fun y => { proj := y, snd := mpullbackWithin I I' f V u y }) =ᶠ[𝓝[s] x₀] fun y =>
    { proj := y, snd := mpullbackWithin I I' f V s y }

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
m n : WithTop ℕ∞
t : Set M'
inst✝⁴ : IsManifold I n M
inst✝³ : IsManifold I' n M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
u : Set M
hV : ContMDiffWithinAt I' I'.tangent m (fun y => { proj := y, snd := V y }) t (f x₀)
hf : ContMDiffWithinAt I I' n f u x₀
hf' : (mfderivWithin I I' f u x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
⊢ ContMDiffWithinAt I I.tangent m (fun y => { proj := y, snd := mpullbackWithin I I' f V u y }) s x₀

Tactic:
have hn : (1 : ℕ) ≤ n := le_trans le_add_self hmn

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
m n : WithTop ℕ∞
t : Set M'
inst✝⁴ : IsManifold I n M
inst✝³ : IsManifold I' n M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
u : Set M
hV : ContMDiffWithinAt I' I'.tangent m (fun y => { proj := y, snd := V y }) t (f x₀)
hf : ContMDiffWithinAt I I' n f u x₀
hf' : (mfderivWithin I I' f u x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiffOn I s
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : ↑1 ≤ n
⊢ ContMDiffWithinAt I I.tangent m (fun y => { proj := y, snd := mpullbackWithin I I' f V u y }) s x₀