-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
lemma extChartAt_mem_closure_interior {x₀ x : M}
    (hx : x ∈ closure (interior s)) (h'x : x ∈ (extChartAt I x₀).source) :
    extChartAt I x₀ x ∈
      closure (interior ((extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target))

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen o
ho : ↑(extChartAt I x₀) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ ↑(extChartAt I x₀) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∈ 𝓝 (↑(extChartAt I x₀) y)

Tactic:
simp only [interior_mem_nhds]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen o
ho : ↑(extChartAt I x₀) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ ↑(extChartAt I x₀) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ ↑(extChartAt I x₀).symm ⁻¹' s ∈ 𝓝 (↑(extChartAt I x₀) y)

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen o
ho : ↑(extChartAt I x₀) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ ↑(extChartAt I x₀) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty

Tactic:
have A : interior (↑(extChartAt I x₀).symm ⁻¹' s) ∈ 𝓝 (extChartAt I x₀ y) := by
  simp only [interior_mem_nhds]
  apply (continuousAt_extChartAt_symm' hy).preimage_mem_nhds
  simp only [hy, PartialEquiv.left_inv]
  exact mem_interior_iff_mem_nhds.mp ys

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen o
ho : ↑(extChartAt I x₀) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ ↑(extChartAt I x₀) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
A : interior (↑(extChartAt I x₀).symm ⁻¹' s) ∈ 𝓝 (↑(extChartAt I x₀) y)
⊢ (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen o
ho : ↑(extChartAt I x₀) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ ↑(extChartAt I x₀) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ ↑(extChartAt I x₀).symm ⁻¹' s ∈ 𝓝 (↑(extChartAt I x₀) y)

Tactic:
apply (continuousAt_extChartAt_symm' hy).preimage_mem_nhds

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen o
ho : ↑(extChartAt I x₀) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ ↑(extChartAt I x₀) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ s ∈ 𝓝 (↑(extChartAt I x₀).symm (↑(extChartAt I x₀) y))

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen o
ho : ↑(extChartAt I x₀) x ∈ o
this : ↑(extChartAt I x₀) ⁻¹' o ∈ 𝓝 x
⊢ (↑(extChartAt I x₀) ⁻¹' o ∩ (extChartAt I x₀).source ∩ interior s).Nonempty

Tactic:
refine (mem_closure_iff_nhds.1 hx) _ (inter_mem this ?_)

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen o
ho : ↑(extChartAt I x₀) x ∈ o
this : ↑(extChartAt I x₀) ⁻¹' o ∈ 𝓝 x
⊢ (extChartAt I x₀).source ∈ 𝓝 x

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen o
ho : ↑(extChartAt I x₀) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ ↑(extChartAt I x₀) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
A : interior (↑(extChartAt I x₀).symm ⁻¹' s) ∈ 𝓝 (↑(extChartAt I x₀) y)
B : ↑(extChartAt I x₀) y ∈ closure (interior (extChartAt I x₀).target)
⊢ (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty

Tactic:
exact mem_closure_iff_nhds.1 B _ (inter_mem (o_open.mem_nhds yo) A)

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen o
ho : ↑(extChartAt I x₀) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ ↑(extChartAt I x₀) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
A : interior (↑(extChartAt I x₀).symm ⁻¹' s) ∈ 𝓝 (↑(extChartAt I x₀) y)
⊢ (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty

Tactic:
have B : (extChartAt I x₀) y ∈ closure (interior (extChartAt I x₀).target) := by
  apply extChartAt_target_subset_closure_interior (x := x₀)
  exact (extChartAt I x₀).map_source hy

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen o
ho : ↑(extChartAt I x₀) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ ↑(extChartAt I x₀) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
A : interior (↑(extChartAt I x₀).symm ⁻¹' s) ∈ 𝓝 (↑(extChartAt I x₀) y)
B : ↑(extChartAt I x₀) y ∈ closure (interior (extChartAt I x₀).target)
⊢ (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty