-- 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:
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)

Tactic:
simp only [mfld_simps] at 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 ∈ (chartAt H x).source
⊢ y ∈ ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)

Proof state:
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 ∈ (chartAt H x).source
⊢ y ∈ ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)

Tactic:
simp [hy, h'y]

Result:
no goals