no goals
α : Type u_2
β : Type u_1
γ : Type ?u.70901
δ : Type ?u.70904
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set β
hs : IsOpen s
⊢ (LocalHomeomorph.trans e (ofSet s hs)).toLocalEquiv.source = (LocalHomeomorph.restr e (↑e ⁻¹' s)).toLocalEquiv.source
rw [trans_source, restr_source, ofSet_source, ← preimage_interior, hs.interior_eq]