feat(Topology/UniformSpace/OfCompactT2): generalize theorem (#30917)

This PR continues the work from #24103.

Original PR: #24103

Author: plp127

Mathlib/Topology/Separation/Regular.lean

@@ -267,6 +267,17 @@ lemma IsClosed.HasSeparatingCover {s t : Set X} [LindelofSpace X] [RegularSpace
     u u_open (fun a ainh ↦ mem_iUnion.mpr ⟨a, u_nhds a ainh⟩)
   exact ⟨u ∘ f, f_cov, fun n ↦ ⟨u_open (f n), u_dis (f n)⟩⟩
 
+/-- Given two separable points `x` and `y`, we can find neighbourhoods
+`x ∈ V₁ ⊆ U₁` and `y ∈ V₂ ⊆ U₂`, with the `Vₖ` closed and the `Uₖ` open,
+such that the `Uₖ` are disjoint. -/
+theorem disjoint_nested_nhds_of_not_inseparable [RegularSpace X] {x y : X} (h : ¬Inseparable x y) :
+    ∃ U₁ ∈ 𝓝 x, ∃ V₁ ∈ 𝓝 x, ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y,
+      IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂ := by
+  rcases r1_separation h with ⟨U₁, U₂, U₁_op, U₂_op, x_in, y_in, H⟩
+  rcases exists_mem_nhds_isClosed_subset (U₁_op.mem_nhds x_in) with ⟨V₁, V₁_in, V₁_closed, h₁⟩
+  rcases exists_mem_nhds_isClosed_subset (U₂_op.mem_nhds y_in) with ⟨V₂, V₂_in, V₂_closed, h₂⟩
+  exact ⟨U₁, mem_of_superset V₁_in h₁, V₁, V₁_in, U₂, mem_of_superset V₂_in h₂, V₂, V₂_in,
+    V₁_closed, V₂_closed, U₁_op, U₂_op, h₁, h₂, H⟩
 
 end RegularSpace
 
@@ -389,12 +400,8 @@ instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i,
 with the `Vₖ` closed and the `Uₖ` open, such that the `Uₖ` are disjoint. -/
 theorem disjoint_nested_nhds [T3Space X] {x y : X} (h : x ≠ y) :
     ∃ U₁ ∈ 𝓝 x, ∃ V₁ ∈ 𝓝 x, ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y,
-      IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂ := by
-  rcases t2_separation h with ⟨U₁, U₂, U₁_op, U₂_op, x_in, y_in, H⟩
-  rcases exists_mem_nhds_isClosed_subset (U₁_op.mem_nhds x_in) with ⟨V₁, V₁_in, V₁_closed, h₁⟩
-  rcases exists_mem_nhds_isClosed_subset (U₂_op.mem_nhds y_in) with ⟨V₂, V₂_in, V₂_closed, h₂⟩
-  exact ⟨U₁, mem_of_superset V₁_in h₁, V₁, V₁_in, U₂, mem_of_superset V₂_in h₂, V₂, V₂_in,
-    V₁_closed, V₂_closed, U₁_op, U₂_op, h₁, h₂, H⟩
+      IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂ :=
+  disjoint_nested_nhds_of_not_inseparable (mt Inseparable.eq h)
 
 open SeparationQuotient
 

Mathlib/Topology/UniformSpace/OfCompactT2.lean

@@ -5,18 +5,19 @@ Authors: Patrick Massot, Yury Kudryashov
 -/
 import Mathlib.Topology.Separation.Regular
 import Mathlib.Topology.UniformSpace.Defs
+import Mathlib.Tactic.TautoSet
 
 /-!
 # Compact separated uniform spaces
 
 ## Main statement
 
-* `uniformSpace_of_compact_t2`: every compact T2 topological structure is induced by a uniform
+* `uniformSpaceOfCompactR1`: every compact R1 topological structure is induced by a uniform
   structure. This uniform structure is described by `compactSpace_uniformity`.
 
 ## Implementation notes
 
-The construction `uniformSpace_of_compact_t2` is not declared as an instance, as it would badly
+The construction `uniformSpaceOfCompactR1` is not declared as an instance, as it would badly
 loop.
 
 ## Tags
@@ -35,7 +36,7 @@ variable {γ : Type*}
 
 
 /-- The unique uniform structure inducing a given compact topological structure. -/
-def uniformSpaceOfCompactT2 [TopologicalSpace γ] [CompactSpace γ] [T2Space γ] : UniformSpace γ where
+def uniformSpaceOfCompactR1 [TopologicalSpace γ] [CompactSpace γ] [R1Space γ] : UniformSpace γ where
   uniformity := 𝓝ˢ (diagonal γ)
   symm := continuous_swap.tendsto_nhdsSet fun _ => Eq.symm
   comp := by
@@ -55,55 +56,53 @@ def uniformSpaceOfCompactT2 [TopologicalSpace γ] [CompactSpace γ] [T2Space γ]
     -- Hence compactness would give us a cluster point (x, y) for F ⊓ 𝓟 Vᶜ
     obtain ⟨⟨x, y⟩, hxy⟩ : ∃ p : γ × γ, ClusterPt p (F ⊓ 𝓟 Vᶜ) := exists_clusterPt_of_compactSpace _
     -- In particular (x, y) is a cluster point of 𝓟 Vᶜ, hence is not in the interior of V,
-    -- and a fortiori not in Δ, so x ≠ y
+    -- so x and y are inseparable
     have clV : ClusterPt (x, y) (𝓟 <| Vᶜ) := hxy.of_inf_right
-    have : (x, y) ∉ interior V := by
-      have : (x, y) ∈ closure Vᶜ := by rwa [mem_closure_iff_clusterPt]
-      rwa [closure_compl] at this
-    have diag_subset : diagonal γ ⊆ interior V := subset_interior_iff_mem_nhdsSet.2 V_in
-    have x_ne_y : x ≠ y := mt (@diag_subset (x, y)) this
+    have ninsep_xy : ¬Inseparable x y := by
+      intro h
+      rw [← mem_closure_iff_clusterPt, (h.prod .rfl).mem_closed_iff isClosed_closure,
+        closure_compl] at clV
+      apply clV
+      rw [mem_interior_iff_mem_nhds]
+      exact nhds_le_nhdsSet (mem_diagonal y) V_in
     -- Since γ is compact and Hausdorff, it is T₄, hence T₃.
     -- So there are closed neighborhoods V₁ and V₂ of x and y contained in
     -- disjoint open neighborhoods U₁ and U₂.
     obtain
-      ⟨U₁, _, V₁, V₁_in, U₂, _, V₂, V₂_in, V₁_cl, V₂_cl, U₁_op, U₂_op, VU₁, VU₂, hU₁₂⟩ :=
-      disjoint_nested_nhds x_ne_y
+      ⟨U₁, -, V₁, V₁_in, U₂, -, V₂, V₂_in, V₁_cl, V₂_cl, U₁_op, U₂_op, VU₁, VU₂, hU₁₂⟩ :=
+      disjoint_nested_nhds_of_not_inseparable ninsep_xy
     -- We set U₃ := (V₁ ∪ V₂)ᶜ so that W := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃ is an open
     -- neighborhood of Δ.
     let U₃ := (V₁ ∪ V₂)ᶜ
     have U₃_op : IsOpen U₃ := (V₁_cl.union V₂_cl).isOpen_compl
     let W := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
     have W_in : W ∈ 𝓝Δ := by
       rw [mem_nhdsSet_iff_forall]
-      rintro ⟨z, z'⟩ (rfl : z = z')
+      rintro ⟨z, z'⟩ hzz'
       refine IsOpen.mem_nhds ?_ ?_
       · apply_rules [IsOpen.union, IsOpen.prod]
-      · simp only [W, mem_union, mem_prod, and_self_iff]
-        exact (_root_.em _).imp_left fun h => union_subset_union VU₁ VU₂ h
+      · cases hzz'
+        simp only [W, U₃, mem_union, mem_prod]
+        tauto_set
     -- So W ○ W ∈ F by definition of F
-    have : W ○ W ∈ F := by simpa only using mem_lift' W_in
+    have : W ○ W ∈ F := mem_lift' W_in
     -- And V₁ ×ˢ V₂ ∈ 𝓝 (x, y)
     have hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y) := prod_mem_nhds V₁_in V₂_in
     -- But (x, y) is also a cluster point of F so (V₁ ×ˢ V₂) ∩ (W ○ W) ≠ ∅
-    -- However the construction of W implies (V₁ ×ˢ V₂) ∩ (W ○ W) = ∅.
-    -- Indeed assume for contradiction there is some (u, v) in the intersection.
     obtain ⟨⟨u, v⟩, ⟨u_in, v_in⟩, w, huw, hwv⟩ :=
       clusterPt_iff_nonempty.mp hxy.of_inf_left hV₁₂ this
-    -- So u ∈ V₁, v ∈ V₂, and there exists some w such that (u, w) ∈ W and (w, v) ∈ W.
-    -- Because u is in V₁ which is disjoint from U₂ and U₃, (u, w) ∈ W forces (u, w) ∈ U₁ ×ˢ U₁.
-    have uw_in : (u, w) ∈ U₁ ×ˢ U₁ :=
-      (huw.resolve_right fun h => h.1 <| Or.inl u_in).resolve_right fun h =>
-        hU₁₂.le_bot ⟨VU₁ u_in, h.1⟩
-    -- Similarly, because v ∈ V₂, (w, v) ∈ W forces (w, v) ∈ U₂ ×ˢ U₂.
-    have wv_in : (w, v) ∈ U₂ ×ˢ U₂ :=
-      (hwv.resolve_right fun h => h.2 <| Or.inr v_in).resolve_left fun h =>
-        hU₁₂.le_bot ⟨h.2, VU₂ v_in⟩
-    -- Hence w ∈ U₁ ∩ U₂ which is empty.
-    -- So we have a contradiction
-    exact hU₁₂.le_bot ⟨uw_in.2, wv_in.1⟩
+    -- However the construction of W implies (V₁ ×ˢ V₂) ∩ (W ○ W) = ∅.
+    simp only [W, U₃, mem_union, mem_prod] at huw hwv
+    tauto_set
   nhds_eq_comap_uniformity x := by
     simp_rw [nhdsSet_diagonal, comap_iSup, nhds_prod_eq, comap_prod, Function.comp_def, comap_id']
-    rw [iSup_split_single _ x, comap_const_of_mem fun V => mem_of_mem_nhds]
-    suffices ∀ y ≠ x, comap (fun _ : γ ↦ x) (𝓝 y) ⊓ 𝓝 y ≤ 𝓝 x by simpa
-    intro y hxy
-    simp [comap_const_of_notMem (compl_singleton_mem_nhds hxy) (not_not_intro rfl)]
+    rw [iSup_split _ (Inseparable x)]
+    conv_rhs =>
+      congr
+      · enter [1, i, 1, hi]
+        rw [← hi.nhds_eq, comap_const_of_mem fun V => mem_of_mem_nhds]
+      · enter [1, i, 1, hi]
+        rw [(not_specializes_iff_exists_open.1 (mt Specializes.inseparable hi)).elim
+          fun S hS => comap_const_of_notMem (hS.1.mem_nhds hS.2.1) hS.2.2]
+    rw [iSup_subtype', @iSup_const _ _ _ _ ⟨⟨x, .rfl⟩⟩]
+    simp

scripts/noshake.json

@@ -204,6 +204,7 @@
   "Mathlib.Init"],
  "ignore":
  {"Mathlib.Util.Notation3": ["Lean.Elab.AuxDef", "Lean.Elab.BuiltinCommand"],
+  "Mathlib.Topology.UniformSpace.OfCompactT2": ["Mathlib.Tactic.TautoSet"],
   "Mathlib.Topology.UniformSpace.Defs": ["Mathlib.Tactic.Monotonicity.Basic"],
   "Mathlib.Topology.Sober": ["Mathlib.Algebra.HierarchyDesign"],
   "Mathlib.Topology.Sheaves.Forget": ["Mathlib.Algebra.Category.Ring.Limits"],
@@ -427,9 +428,7 @@
   "Mathlib.Geometry.Manifold.Notation":
   ["Mathlib.Geometry.Manifold.ContMDiff.Defs",
    "Mathlib.Geometry.Manifold.MFDeriv.Defs"],
-  "Mathlib.FieldTheory.Normal.Defs": ["Mathlib.FieldTheory.Galois.Notation"],
   "Mathlib.FieldTheory.Galois.Notation": ["Mathlib.Algebra.Algebra.Equiv"],
-  "Mathlib.FieldTheory.Finite.Basic": ["Mathlib.FieldTheory.Galois.Notation"],
   "Mathlib.Deprecated.NatLemmas": ["Batteries.Data.Nat.Lemmas", "Batteries.WF"],
   "Mathlib.Deprecated.MinMax": ["Mathlib.Order.MinMax"],
   "Mathlib.Deprecated.LazyList": ["Mathlib.Lean.Thunk"],