From 7138640ce946069270bf5f63cf37d18ffd9987e9 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Tue, 8 Oct 2024 06:00:36 +0000
Subject: [PATCH] feat: strengthen
 `instTotallyDisconnectedSpaceOfIsUltrametricDist` to `TotallySeparatedSpace`
 (#17427)

Rename the file it's in to `TotallySeparated`. Also add two lemmas `isClopen_of_disjoint_cover_open` and `totallySeparatedSpace_iff_exists_isClopen`.
---
 Mathlib.lean                                  |  2 +-
 Mathlib/Topology/Clopen.lean                  |  4 +++
 .../Connected/TotallyDisconnected.lean        | 21 ++++++++------
 .../Ultra/TotallyDisconnected.lean            | 25 -----------------
 .../MetricSpace/Ultra/TotallySeparated.lean   | 28 +++++++++++++++++++
 5 files changed, 45 insertions(+), 35 deletions(-)
 delete mode 100644 Mathlib/Topology/MetricSpace/Ultra/TotallyDisconnected.lean
 create mode 100644 Mathlib/Topology/MetricSpace/Ultra/TotallySeparated.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 6917161a2ee67..4304ebaaafbdb 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4744,7 +4744,7 @@ import Mathlib.Topology.MetricSpace.ThickenedIndicator
 import Mathlib.Topology.MetricSpace.Thickening
 import Mathlib.Topology.MetricSpace.Ultra.Basic
 import Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps
-import Mathlib.Topology.MetricSpace.Ultra.TotallyDisconnected
+import Mathlib.Topology.MetricSpace.Ultra.TotallySeparated
 import Mathlib.Topology.Metrizable.Basic
 import Mathlib.Topology.Metrizable.ContinuousMap
 import Mathlib.Topology.Metrizable.Uniformity
diff --git a/Mathlib/Topology/Clopen.lean b/Mathlib/Topology/Clopen.lean
index c560e10009cd9..ff10a04698b33 100644
--- a/Mathlib/Topology/Clopen.lean
+++ b/Mathlib/Topology/Clopen.lean
@@ -102,6 +102,10 @@ theorem isClopen_inter_of_disjoint_cover_clopen {s a b : Set X} (h : IsClopen s)
   rintro x ⟨hx₁, hx₂⟩
   exact ⟨hx₁, by simpa [not_mem_of_mem_compl hx₂] using cover hx₁⟩
 
+theorem isClopen_of_disjoint_cover_open {a b : Set X} (cover : univ ⊆ a ∪ b)
+    (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) : IsClopen a :=
+  univ_inter a ▸ isClopen_inter_of_disjoint_cover_clopen isClopen_univ cover ha hb hab
+
 @[simp]
 theorem isClopen_discrete [DiscreteTopology X] (s : Set X) : IsClopen s :=
   ⟨isClosed_discrete _, isOpen_discrete _⟩
diff --git a/Mathlib/Topology/Connected/TotallyDisconnected.lean b/Mathlib/Topology/Connected/TotallyDisconnected.lean
index 0da1004c037f4..b7f1ff02b4fb4 100644
--- a/Mathlib/Topology/Connected/TotallyDisconnected.lean
+++ b/Mathlib/Topology/Connected/TotallyDisconnected.lean
@@ -195,7 +195,7 @@ alias IsTotallySeparated.isTotallyDisconnected := isTotallyDisconnected_of_isTot
 
 /-- A space is totally separated if any two points can be separated by two disjoint open sets
 covering the whole space. -/
-class TotallySeparatedSpace (α : Type u) [TopologicalSpace α] : Prop where
+@[mk_iff] class TotallySeparatedSpace (α : Type u) [TopologicalSpace α] : Prop where
   /-- The universal set `Set.univ` in a totally separated space is totally separated. -/
   isTotallySeparated_univ : IsTotallySeparated (univ : Set α)
 
@@ -210,15 +210,19 @@ instance (priority := 100) TotallySeparatedSpace.of_discrete (α : Type*) [Topol
   ⟨fun _ _ b _ h => ⟨{b}ᶜ, {b}, isOpen_discrete _, isOpen_discrete _, h, rfl,
     (compl_union_self _).symm.subset, disjoint_compl_left⟩⟩
 
+theorem totallySeparatedSpace_iff_exists_isClopen {α : Type*} [TopologicalSpace α] :
+    TotallySeparatedSpace α ↔ ∀ x y : α, x ≠ y → ∃ U : Set α, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ := by
+  simp only [totallySeparatedSpace_iff, IsTotallySeparated, Set.Pairwise, mem_univ, true_implies]
+  refine forall₃_congr fun x y _ ↦
+    ⟨fun ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ ↦ ?_, fun ⟨U, hU, Ux, Ucy⟩ ↦ ?_⟩
+  · exact ⟨U, isClopen_of_disjoint_cover_open f hU hV disj,
+      Ux, fun Uy ↦ Set.disjoint_iff.mp disj ⟨Uy, Vy⟩⟩
+  · exact ⟨U, Uᶜ, hU.2, hU.compl.2, Ux, Ucy, (Set.union_compl_self U).ge, disjoint_compl_right⟩
+
 theorem exists_isClopen_of_totally_separated {α : Type*} [TopologicalSpace α]
     [TotallySeparatedSpace α] {x y : α} (hxy : x ≠ y) :
-    ∃ U : Set α, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ := by
-  obtain ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ :=
-    TotallySeparatedSpace.isTotallySeparated_univ (Set.mem_univ x) (Set.mem_univ y) hxy
-  have hU := isClopen_inter_of_disjoint_cover_clopen isClopen_univ f hU hV disj
-  rw [univ_inter _] at hU
-  rw [← Set.subset_compl_iff_disjoint_right, subset_compl_comm] at disj
-  exact ⟨U, hU, Ux, disj Vy⟩
+    ∃ U : Set α, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ :=
+  totallySeparatedSpace_iff_exists_isClopen.mp ‹_› _ _ hxy
 
 end TotallySeparated
 
@@ -260,7 +264,6 @@ theorem Continuous.connectedComponentsLift_unique (h : Continuous f) (g : Connec
     (hg : g ∘ (↑) = f) : g = h.connectedComponentsLift :=
   connectedComponents_lift_unique' <| hg.trans h.connectedComponentsLift_comp_coe.symm
 
-
 instance ConnectedComponents.totallyDisconnectedSpace :
     TotallyDisconnectedSpace (ConnectedComponents α) := by
   rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]
diff --git a/Mathlib/Topology/MetricSpace/Ultra/TotallyDisconnected.lean b/Mathlib/Topology/MetricSpace/Ultra/TotallyDisconnected.lean
deleted file mode 100644
index 161f861120e27..0000000000000
--- a/Mathlib/Topology/MetricSpace/Ultra/TotallyDisconnected.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-/-
-Copyright (c) 2024 Yakov Pechersky. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yakov Pechersky, David Loeffler
--/
-import Mathlib.Topology.MetricSpace.Defs
-import Mathlib.Topology.MetricSpace.Ultra.Basic
-
-/-!
-# Ultrametric spaces are totally disconnected
-
-In a metric space with an ultrametric, the space is totally disconnected.
-
-## Tags
-
-ultrametric, nonarchimedean, totally disconnected
--/
-open Metric IsUltrametricDist
-
-instance {X : Type*} [MetricSpace X] [IsUltrametricDist X] : TotallyDisconnectedSpace X := by
-  refine (totallyDisconnectedSpace_iff X).mpr (isTotallyDisconnected_of_isClopen_set fun x y h ↦ ?_)
-  obtain ⟨r, hr, hr'⟩ := exists_between (dist_pos.mpr h)
-  refine ⟨_, IsUltrametricDist.isClopen_ball x r, ?_, ?_⟩
-  · simp only [mem_ball, dist_self, hr]
-  · simp only [mem_ball, dist_comm, not_lt, hr'.le]
diff --git a/Mathlib/Topology/MetricSpace/Ultra/TotallySeparated.lean b/Mathlib/Topology/MetricSpace/Ultra/TotallySeparated.lean
new file mode 100644
index 0000000000000..09edc0330ec3e
--- /dev/null
+++ b/Mathlib/Topology/MetricSpace/Ultra/TotallySeparated.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2024 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky, David Loeffler
+-/
+import Mathlib.Topology.MetricSpace.Defs
+import Mathlib.Topology.MetricSpace.Ultra.Basic
+
+/-!
+# Ultrametric spaces are totally separated
+
+In a metric space with an ultrametric, the space is totally separated, hence totally disconnected.
+
+## Tags
+
+ultrametric, nonarchimedean, totally separated, totally disconnected
+-/
+open Metric IsUltrametricDist
+
+instance {X : Type*} [MetricSpace X] [IsUltrametricDist X] : TotallySeparatedSpace X :=
+  totallySeparatedSpace_iff_exists_isClopen.mpr fun x y h ↦ by
+    obtain ⟨r, hr, hr'⟩ := exists_between (dist_pos.mpr h)
+    refine ⟨_, IsUltrametricDist.isClopen_ball x r, ?_, ?_⟩
+    · simp only [mem_ball, dist_self, hr]
+    · simp only [Set.mem_compl, mem_ball, dist_comm, not_lt, hr'.le]
+
+example {X : Type*} [MetricSpace X] [IsUltrametricDist X] : TotallyDisconnectedSpace X :=
+  inferInstance