∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Mul G] [inst_3 : Mul H]
  (e : G ≃* H) (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s),
  e.toContinuousMulEquiv he =
    { toFun := ⇑e, invFun := ⇑e.symm, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }