Theorem: PartialHomeomorph.extend_image_mem_nhds_symm (Sard/ManifoldAux.lean)

State before:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
⊢ ↑(e.extend I).symm '' n ∈ 𝓝 (↑(e.extend I).symm x)
Tactic:
rcases mem_nhds_iff.mp hn with ⟨t', ht's', ht'open, hxt'⟩
State after:
case intro.intro.intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ ↑(e.extend I).symm '' n ∈ 𝓝 (↑(e.extend I).symm x)

State before:
case intro.intro.intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ ↑(e.extend I).symm '' n ∈ 𝓝 (↑(e.extend I).symm x)
Tactic:
rw [mem_nhds_iff]
State after:
case intro.intro.intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ ∃ t ⊆ ↑(e.extend I).symm '' n, IsOpen t ∧ ↑(e.extend I).symm x ∈ t

State before:
case intro.intro.intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ ∃ t ⊆ ↑(e.extend I).symm '' n, IsOpen t ∧ ↑(e.extend I).symm x ∈ t
Tactic:
refine ⟨(e.extend I).symm '' t', image_subset _ ht's', ?_, ?_⟩
State after:
case intro.intro.intro.refine_1
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ IsOpen (↑(e.extend I).symm '' t')

case intro.intro.intro.refine_2
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ ↑(e.extend I).symm x ∈ ↑(e.extend I).symm '' t'

State before:
case intro.intro.intro.refine_1
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ IsOpen (↑(e.extend I).symm '' t')
Tactic:
apply e.extend_symm_isOpenMapOn_target _ ht'open (Subset.trans ht's' hn')
State after:
no goals

State before:
case intro.intro.intro.refine_2
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ ↑(e.extend I).symm x ∈ ↑(e.extend I).symm '' t'
Tactic:
exact mem_image_of_mem (e.extend I).symm hxt'
State after:
no goals