case hx
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.173038
M' : Type ?u.173041
H' : Type ?u.173044
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 : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ↑(extend f I) x ∈ (LocalEquiv.symm (extend f I) ≫ extend f' I).source
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.173038
M' : Type ?u.173041
H' : Type ?u.173044
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 : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ (LocalEquiv.symm (extend f I) ≫ extend f' I).source ∈ 𝓝[range ↑I] ↑(extend f I) x
apply extend_coord_change_source_mem_nhdsWithin
case hx
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.173038
M' : Type ?u.173041
H' : Type ?u.173044
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 : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ↑(extend f I) x ∈ ↑(extend f I) '' (f.source ∩ f'.source)
case hx
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.173038
M' : Type ?u.173041
H' : Type ?u.173044
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 : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ↑(extend f I) x ∈ (LocalEquiv.symm (extend f I) ≫ extend f' I).source
rw [← extend_image_source_inter]
no goals
case hx
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.173038
M' : Type ?u.173041
H' : Type ?u.173044
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 : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ↑(extend f I) x ∈ ↑(extend f I) '' (f.source ∩ f'.source)
exact mem_image_of_mem _ ⟨hxf, hxf'⟩