-- Mathlib/Geometry/Manifold/VectorField.lean
lemma eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm
    {V : Π (x : M), TangentSpace I x}
    (hV : ContMDiffWithinAt I I.tangent m (fun x ↦ (V x : TangentBundle I M)) s x)
    (hs : UniqueMDiffOn I s) (hx : x ∈ s) (hmn : m + 1 ≤ n) (hm : m ≠ ∞) :
    ∀ᶠ y in 𝓝[s] x, ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
    (fun z ↦ (mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm V (range I) z :
      TangentBundle 𝓘(𝕜, E) E))
    ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x 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
s : Set M
x : M
m n : WithTop ℕ∞
inst✝² : IsManifold I n M
inst✝¹ : CompleteSpace E
inst✝ : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV : ContMDiffWithinAt I I.tangent m (fun x => { proj := x, snd := V x }) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
T :
  {x_1 |
      (fun x' =>
          ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
            (fun y => { proj := y, snd := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) y })
            ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x')
        x_1} ∈
    𝓝[(extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s] ↑(extChartAt I x) x
A :
  ↑(extChartAt I x) ⁻¹'
      {x_1 |
        (fun x' =>
            ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
              (fun y => { proj := y, snd := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) y })
              ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x')
          x_1} ∈
    𝓝[↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)] x
⊢ ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) ∈ 𝓝[s] x

Tactic:
filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds (extChartAt_source_mem_nhds (I := I) x)]
  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
s : Set M
x : M
m n : WithTop ℕ∞
inst✝² : IsManifold I n M
inst✝¹ : CompleteSpace E
inst✝ : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV : ContMDiffWithinAt I I.tangent m (fun x => { proj := x, snd := V x }) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
T :
  {x_1 |
      (fun x' =>
          ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
            (fun y => { proj := y, snd := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) y })
            ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x')
        x_1} ∈
    𝓝[(extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s] ↑(extChartAt I x) x
A :
  ↑(extChartAt I x) ⁻¹'
      {x_1 |
        (fun x' =>
            ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
              (fun y => { proj := y, snd := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) y })
              ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x')
          x_1} ∈
    𝓝[↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)] x
y : M
hy : y ∈ s
h'y : y ∈ (extChartAt I x).source
⊢ y ∈ ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)

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
m n : WithTop ℕ∞
inst✝² : IsManifold I n M
inst✝¹ : CompleteSpace E
inst✝ : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV : ContMDiffWithinAt I I.tangent m (fun x => { proj := x, snd := V x }) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
⊢ ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
      (fun z => { proj := z, snd := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) z })
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)

Tactic:
have T := nhdsWithin_mono _ (subset_insert _ _)
  ((contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin hm).1
    (contMDiffWithinAt_mpullbackWithin_extChartAt_symm hV hs hx 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
s : Set M
x : M
m n : WithTop ℕ∞
inst✝² : IsManifold I n M
inst✝¹ : CompleteSpace E
inst✝ : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV : ContMDiffWithinAt I I.tangent m (fun x => { proj := x, snd := V x }) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
T :
  {x_1 |
      (fun x' =>
          ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
            (fun y => { proj := y, snd := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) y })
            ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x')
        x_1} ∈
    𝓝[(extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s] ↑(extChartAt I x) x
⊢ ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
      (fun z => { proj := z, snd := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) z })
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)