𝕜 : Type u_3
E : Type u_4
M : Type u_2
H : Type u_1
E' : Type ?u.174952
M' : Type ?u.174955
H' : Type ?u.174958
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
⊢ ContDiffOn 𝕜 ⊤ (↑(extend f I) ∘ ↑(LocalEquiv.symm (extend f' I)))
    (↑(ModelWithCorners.symm I) ⁻¹' (LocalHomeomorph.symm f' ≫ₕ f).toLocalEquiv.source ∩ range ↑I)
𝕜 : Type u_3
E : Type u_4
M : Type u_2
H : Type u_1
E' : Type ?u.174952
M' : Type ?u.174955
H' : Type ?u.174958
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
⊢ ContDiffOn 𝕜 ⊤ (↑(extend f I) ∘ ↑(LocalEquiv.symm (extend f' I))) (LocalEquiv.symm (extend f' I) ≫ extend f I).source
rw [extend_coord_change_source, I.image_eq]
no goals
𝕜 : Type u_3
E : Type u_4
M : Type u_2
H : Type u_1
E' : Type ?u.174952
M' : Type ?u.174955
H' : Type ?u.174958
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
⊢ ContDiffOn 𝕜 ⊤ (↑(extend f I) ∘ ↑(LocalEquiv.symm (extend f' I)))
    (↑(ModelWithCorners.symm I) ⁻¹' (LocalHomeomorph.symm f' ≫ₕ f).toLocalEquiv.source ∩ range ↑I)
exact (StructureGroupoid.compatible_of_mem_maximalAtlas hf' hf).1