no goals
α : Type u_2
β : Type u_1
γ : Type ?u.71931
δ : Type ?u.71934
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set β
hs : IsOpen s
⊢ LocalHomeomorph.trans e (ofSet s hs) = LocalHomeomorph.restr e (e.source ∩ ↑e ⁻¹' s)
rw [trans_ofSet, restr_source_inter]