no goals
α : Type u_1
β : Type u_2
γ : Type ?u.72442
δ : Type ?u.72445
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
⊢ (LocalHomeomorph.trans (ofSet s hs) e).toLocalEquiv.source = (LocalHomeomorph.restr e s).toLocalEquiv.source
simp [hs.interior_eq, inter_comm]