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