∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (toEquiv toEquiv_1 : X ≃ Y)
  (e_toEquiv : toEquiv = toEquiv_1) (continuous_toFun : Continuous toEquiv.toFun)
  (continuous_invFun : Continuous toEquiv.invFun),
  { toEquiv := toEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
    { toEquiv := toEquiv_1, continuous_toFun := ⋯, continuous_invFun := ⋯ }