𝕜 : Type u_3
E : Type u_4
M : Type u_2
H : Type u_1
E' : Type ?u.178926
M' : Type ?u.178929
H' : Type ?u.178932
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
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I M
hf' : f' ∈ maximalAtlas I 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_3
E : Type u_4
M : Type u_2
H : Type u_1
E' : Type ?u.178926
M' : Type ?u.178929
H' : Type ?u.178932
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
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I M
hf' : f' ∈ maximalAtlas I M
x : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ContDiffWithinAt 𝕜 ⊤ (↑(extend f I) ∘ ↑(LocalEquiv.symm (extend f' I))) (range ↑I) (↑(extend f' I) x)
refine' contDiffWithinAt_extend_coord_change I hf hf' _
𝕜 : Type u_3
E : Type u_4
M : Type u_2
H : Type u_1
E' : Type ?u.178926
M' : Type ?u.178929
H' : Type ?u.178932
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
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I M
hf' : f' ∈ maximalAtlas I M
x : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ↑(extend f' I) x ∈ ↑(extend f' I) '' (f'.source ∩ f.source)
𝕜 : Type u_3
E : Type u_4
M : Type u_2
H : Type u_1
E' : Type ?u.178926
M' : Type ?u.178929
H' : Type ?u.178932
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
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I M
hf' : f' ∈ maximalAtlas I 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
𝕜 : Type u_3
E : Type u_4
M : Type u_2
H : Type u_1
E' : Type ?u.178926
M' : Type ?u.178929
H' : Type ?u.178932
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
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I M
hf' : f' ∈ maximalAtlas I 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⟩