∀ (α : Type u) [isCommRing : CommRing α] [isTopologicalSpace : TopologicalSpace α]
  [isTopologicalRing : IsTopologicalRing α] (α_1 : Type u) (isCommRing_1 : CommRing α_1)
  (isTopologicalSpace_1 : TopologicalSpace α_1) (isTopologicalRing_1 : IsTopologicalRing α_1),
  ({ α := α, isCommRing := isCommRing, isTopologicalSpace := isTopologicalSpace,
        isTopologicalRing := isTopologicalRing } =
      { α := α_1, isCommRing := isCommRing_1, isTopologicalSpace := isTopologicalSpace_1,
        isTopologicalRing := isTopologicalRing_1 }) =
    (α = α_1 ∧ isCommRing ≍ isCommRing_1 ∧ isTopologicalSpace ≍ isTopologicalSpace_1)