chore: rephrase t2Space_iff_of_continuous_surjective_open

SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean

@@ -92,10 +92,12 @@ theorem image_proj𝕊₁_Ico : proj𝕊₁ '' Ico 0 1 = univ := by
 theorem image_proj𝕊₁_Icc : proj𝕊₁ '' Icc 0 1 = univ :=
   eq_univ_of_subset (image_mono Ico_subset_Icc_self) image_proj𝕊₁_Ico
 
+theorem isOpenQuotientMap_proj𝕊₁ : IsOpenQuotientMap proj𝕊₁ := QuotientAddGroup.isOpenQuotientMap_mk
+
 @[continuity, fun_prop]
-theorem continuous_proj𝕊₁ : Continuous proj𝕊₁ := continuous_quotient_mk'
+theorem continuous_proj𝕊₁ : Continuous proj𝕊₁ := isOpenQuotientMap_proj𝕊₁.continuous
 
-theorem isOpenMap_proj𝕊₁ : IsOpenMap proj𝕊₁ := QuotientAddGroup.isOpenMap_coe
+theorem isOpenMap_proj𝕊₁ : IsOpenMap proj𝕊₁ := isOpenQuotientMap_proj𝕊₁.isOpenMap
 
 theorem quotientMap_id_proj𝕊₁ {X : Type*} [TopologicalSpace X] :
     Topology.IsQuotientMap fun p : X × ℝ ↦ (p.1, proj𝕊₁ p.2) :=
@@ -117,8 +119,7 @@ theorem isClosed_int : IsClosed (range ((↑) : ℤ → ℝ)) :=
   Int.isClosedEmbedding_coe_real.isClosed_range
 
 instance : T2Space 𝕊₁ := by
-  have πcont : Continuous π := continuous_quotient_mk'
-  rw [t2Space_iff_of_continuous_surjective_open πcont Quotient.mk''_surjective isOpenMap_proj𝕊₁]
+  rw [t2Space_iff_of_isOpenQuotientMap isOpenQuotientMap_proj𝕊₁]
   have : {q : ℝ × ℝ | π q.fst = π q.snd} = {q : ℝ × ℝ | ∃ k : ℤ, q.2 = q.1 + k} := by
     ext ⟨a, b⟩
     exact Quotient.eq''.trans transOne_rel_iff

SphereEversion/ToMathlib/Topology/Separation/Hausdorff.lean

@@ -1,18 +1,12 @@
 import Mathlib.Topology.Separation.Hausdorff
-open Set Function
 
-variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
-
-/-
-TODO? State a specialized version for quotient maps? Note the open map assumption is still
-a separate assumption there, because there is no `QuotientMap.prod_map`.
--/
-theorem t2Space_iff_of_continuous_surjective_open {α β : Type*} [TopologicalSpace α]
-    [TopologicalSpace β] {π : α → β} (hcont : Continuous π) (hsurj : Surjective π)
-    (hop : IsOpenMap π) : T2Space β ↔ IsClosed {q : α × α | π q.1 = π q.2} := by
+theorem t2Space_iff_of_isOpenQuotientMap {α β : Type*} [TopologicalSpace α]
+    [TopologicalSpace β] {π : α → β} (h : IsOpenQuotientMap π) :
+    T2Space β ↔ IsClosed {q : α × α | π q.1 = π q.2} := by
   rw [t2_iff_isClosed_diagonal]
+  replace h := IsOpenQuotientMap.prodMap h h
   constructor <;> intro H
-  · exact H.preimage (hcont.prodMap hcont)
+  · exact H.preimage h.continuous
   · simp_rw [← isOpen_compl_iff] at H ⊢
-    convert hop.prodMap hop _ H
-    exact ((hsurj.prodMap hsurj).image_preimage _).symm
+    convert h.isOpenMap _ H
+    exact (h.surjective.image_preimage _).symm