∀ {R : Type u} [inst : Ring R] (toTopologicalSpace : TopologicalSpace R) (toIsTopologicalRing : IsTopologicalRing R)
  (toTopologicalSpace_1 : TopologicalSpace R) (toIsTopologicalRing_1 : IsTopologicalRing R),
  ({ toTopologicalSpace := toTopologicalSpace, toIsTopologicalRing := toIsTopologicalRing } =
      { toTopologicalSpace := toTopologicalSpace_1, toIsTopologicalRing := toIsTopologicalRing_1 }) =
    (toTopologicalSpace = toTopologicalSpace_1)