-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
lemma extChartAt_target_subset_closure_interior {x : M} :
    (extChartAt I x).target ⊆ closure (interior (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
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
⊢ (t ∩ interior (extChartAt I x).target).Nonempty

Tactic:
have B : y ∈ closure (interior (range I)) := by
  apply I.range_subset_closure_interior (extChartAt_target_subset_range x hy)

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
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
B : y ∈ closure (interior (range ↑I))
⊢ (t ∩ 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
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
⊢ y ∈ closure (interior (range ↑I))

Tactic:
apply I.range_subset_closure_interior (extChartAt_target_subset_range x hy)

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
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
B : y ∈ closure (interior (range ↑I))
z : E
hz : z ∈ interior (range ↑I)
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range ↑I)ᶜ
h''z : z ∈ (extChartAt I x).target
⊢ z ∈ interior (extChartAt I x).target

Tactic:
exact (extChartAt_target_eventuallyEq_of_mem h''z).symm.mem_interior hz

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
inst✝ : ChartedSpace H M
x : M
⊢ (extChartAt I x).target ⊆ closure (interior (extChartAt I x).target)

Tactic:
intro y hy

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
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ y ∈ closure (interior (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
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
B : y ∈ closure (interior (range ↑I))
⊢ (t ∩ interior (extChartAt I x).target).Nonempty

Tactic:
obtain ⟨z, ⟨tz, h'z⟩, hz⟩ :
    (t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∩ interior (range I)).Nonempty :=
  mem_closure_iff_nhds.1 B _ A

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
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
B : y ∈ closure (interior (range ↑I))
z : E
hz : z ∈ interior (range ↑I)
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range ↑I)ᶜ
⊢ (t ∩ interior (extChartAt I x).target).Nonempty

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
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
B : y ∈ closure (interior (range ↑I))
z : E
hz : z ∈ interior (range ↑I)
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range ↑I)ᶜ
⊢ z ∈ interior (extChartAt I x).target

Tactic:
have h''z : z ∈ (extChartAt I x).target := by simpa [interior_subset hz] using h'z

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
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
B : y ∈ closure (interior (range ↑I))
z : E
hz : z ∈ interior (range ↑I)
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range ↑I)ᶜ
h''z : z ∈ (extChartAt I x).target
⊢ z ∈ interior (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
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ y ∈ closure (interior (extChartAt I x).target)

Tactic:
rw [mem_closure_iff_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
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ ∀ t ∈ 𝓝 y, (t ∩ 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
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
⊢ (t ∩ interior (extChartAt I x).target).Nonempty

Tactic:
have A : t ∩ ((extChartAt I x).target ∪ (range I)ᶜ) ∈ 𝓝 y :=
  inter_mem ht (extChartAt_target_union_compl_range_mem_nhds_of_mem hy)

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
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
⊢ (t ∩ interior (extChartAt I x).target).Nonempty