𝕜 : Type u_3
E : Type u_1
M : Type u_2
H : Type u_4
E' : Type ?u.171224
M' : Type ?u.171227
H' : Type ?u.171230
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x✝ : M
s t : Set M
x : E
hx : x ∈ ↑I '' (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source
⊢ ↑I '' (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source ∈ 𝓝[range ↑I] x
𝕜 : Type u_3
E : Type u_1
M : Type u_2
H : Type u_4
E' : Type ?u.171224
M' : Type ?u.171227
H' : Type ?u.171230
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x✝ : M
s t : Set M
x : E
hx : x ∈ (LocalEquiv.symm (extend f I) ≫ extend f' I).source
⊢ (LocalEquiv.symm (extend f I) ≫ extend f' I).source ∈ 𝓝[range ↑I] x
rw [f.extend_coord_change_source] at hx ⊢
case intro.intro
𝕜 : Type u_3
E : Type u_1
M : Type u_2
H : Type u_4
E' : Type ?u.171224
M' : Type ?u.171227
H' : Type ?u.171230
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x✝ : M
s t : Set M
x : H
hx : x ∈ (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source
⊢ ↑I '' (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source ∈ 𝓝[range ↑I] ↑I x
𝕜 : Type u_3
E : Type u_1
M : Type u_2
H : Type u_4
E' : Type ?u.171224
M' : Type ?u.171227
H' : Type ?u.171230
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x✝ : M
s t : Set M
x : E
hx : x ∈ ↑I '' (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source
⊢ ↑I '' (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source ∈ 𝓝[range ↑I] x
obtain ⟨x, hx, rfl⟩ := hx
case intro.intro
𝕜 : Type u_3
E : Type u_1
M : Type u_2
H : Type u_4
E' : Type ?u.171224
M' : Type ?u.171227
H' : Type ?u.171230
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x✝ : M
s t : Set M
x : H
hx : x ∈ (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source
⊢ (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source ∈ 𝓝 x
case intro.intro
𝕜 : Type u_3
E : Type u_1
M : Type u_2
H : Type u_4
E' : Type ?u.171224
M' : Type ?u.171227
H' : Type ?u.171230
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x✝ : M
s t : Set M
x : H
hx : x ∈ (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source
⊢ ↑I '' (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source ∈ 𝓝[range ↑I] ↑I x
refine' I.image_mem_nhdsWithin _
no goals
case intro.intro
𝕜 : Type u_3
E : Type u_1
M : Type u_2
H : Type u_4
E' : Type ?u.171224
M' : Type ?u.171227
H' : Type ?u.171230
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x✝ : M
s t : Set M
x : H
hx : x ∈ (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source
⊢ (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source ∈ 𝓝 x
refine' (LocalHomeomorph.open_source _).mem_nhds hx