𝕜 : Type u_3
E : Type u_1
M : Type u_2
H : Type u_4
E' : Type ?u.166336
M' : Type ?u.166339
H' : Type ?u.166342
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
⊢ ↑(ModelWithCorners.symm I) ⁻¹' f.target ∩ ↑(LocalEquiv.symm (extend f I)) ⁻¹' f'.source ∩ range ↑I =
    ↑(ModelWithCorners.symm I) ⁻¹' (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source ∩ range ↑I
𝕜 : Type u_3
E : Type u_1
M : Type u_2
H : Type u_4
E' : Type ?u.166336
M' : Type ?u.166339
H' : Type ?u.166342
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
⊢ (LocalEquiv.symm (extend f I) ≫ extend f' I).source = ↑I '' (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source
simp_rw [LocalEquiv.trans_source, I.image_eq, extend_source, LocalEquiv.symm_source,
  extend_target, inter_right_comm _ (range I)]
no goals
𝕜 : Type u_3
E : Type u_1
M : Type u_2
H : Type u_4
E' : Type ?u.166336
M' : Type ?u.166339
H' : Type ?u.166342
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
⊢ ↑(ModelWithCorners.symm I) ⁻¹' f.target ∩ ↑(LocalEquiv.symm (extend f I)) ⁻¹' f'.source ∩ range ↑I =
    ↑(ModelWithCorners.symm I) ⁻¹' (LocalHomeomorph.symm f ≫ₕ f').toLocalEquiv.source ∩ range ↑I
rfl