no goals
α : Type u_1
β : Type ?u.64088
γ : Type ?u.64091
δ : Type ?u.64094
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
⊢ ofSet univ (_ : IsOpen univ) = LocalHomeomorph.refl α
ext <;> simp