∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y)
  (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s), (e.toHomeomorph he).symm = e.symm.toHomeomorph ⋯