-- 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:
case a
𝕜 : 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)
⊢ ↑(extChartAt I x₀) y ∈ (extChartAt I x₀).target

Tactic:
exact (extChartAt I x₀).map_source hy

Result:
no goals

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
⊢ (↑(extChartAt I x₀) ⁻¹' o ∩ (extChartAt I x₀).source ∩ interior s).Nonempty

Tactic:
have : (extChartAt I x₀) ⁻¹' o ∈ 𝓝 x := by
  apply (continuousAt_extChartAt' h'x).preimage_mem_nhds (o_open.mem_nhds ho)

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₀) ⁻¹' o ∩ (extChartAt I x₀).source ∩ interior s).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
this : ↑(extChartAt I x₀) ⁻¹' o ∈ 𝓝 x
⊢ (extChartAt I x₀).source ∈ 𝓝 x

Tactic:
apply (isOpen_extChartAt_source x₀).mem_nhds h'x

Result:
no goals

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
⊢ s ∈ 𝓝 (↑(extChartAt I x₀).symm (↑(extChartAt I x₀) y))

Tactic:
simp only [hy, PartialEquiv.left_inv]

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 ∈ 𝓝 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
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)
⊢ ↑(extChartAt I x₀) y ∈ closure (interior (extChartAt I x₀).target)

Tactic:
apply extChartAt_target_subset_closure_interior (x := x₀)

Result:
case a
𝕜 : 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)
⊢ ↑(extChartAt I x₀) y ∈ (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
⊢ (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty

Tactic:
obtain ⟨y, ⟨yo, hy⟩, ys⟩ :
    ((extChartAt I x₀) ⁻¹' o ∩ (extChartAt I x₀).source ∩ interior s).Nonempty := by
  have : (extChartAt I x₀) ⁻¹' o ∈ 𝓝 x := by
    apply (continuousAt_extChartAt' h'x).preimage_mem_nhds (o_open.mem_nhds ho)
  refine (mem_closure_iff_nhds.1 hx) _ (inter_mem this ?_)
  apply (isOpen_extChartAt_source x₀).mem_nhds h'x

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
⊢ (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
⊢ ↑(extChartAt I x₀) ⁻¹' o ∈ 𝓝 x

Tactic:
apply (continuousAt_extChartAt' h'x).preimage_mem_nhds (o_open.mem_nhds ho)

Result:
no goals