feat(topology/separation): generalize&rename a lemma (#16503)

* rename `tot_sep_of_zero_dim` to `totally_separated_space_of_t1_of_basis_clopen`;
* generalize it from a `t2_space` to a `t1_space`.

src/data/set/basic.lean

@@ -159,8 +159,7 @@ end set_coe
 lemma subtype.mem {α : Type*} {s : set α} (p : s) : (p : α) ∈ s := p.prop
 
 /-- Duplicate of `eq.subset'`, which currently has elaboration problems. -/
-lemma eq.subset {α} {s t : set α} : s = t → s ⊆ t :=
-by { rintro rfl x hx, exact hx }
+lemma eq.subset {α} {s t : set α} : s = t → s ⊆ t := eq.subset'
 
 namespace set
 

src/topology/separation.lean

@@ -58,7 +58,8 @@ This file defines the predicate `separated`, and common separation axioms
 * `is_compact.is_closed`: All compact sets are closed.
 * `locally_compact_of_compact_nhds`: If every point has a compact neighbourhood,
   then the space is locally compact.
-* `tot_sep_of_zero_dim`: If `α` has a clopen basis, it is a `totally_separated_space`.
+* `totally_separated_space_of_t1_of_basis_clopen`: If `α` has a clopen basis, then
+  it is a `totally_separated_space`.
 * `loc_compact_t2_tot_disc_iff_tot_sep`: A locally compact T₂ space is totally disconnected iff
   it is totally separated.
 
@@ -1544,22 +1545,19 @@ end
 
 section profinite
 
-variables [t2_space α]
-
-/-- A Hausdorff space with a clopen basis is totally separated. -/
-lemma tot_sep_of_zero_dim (h : is_topological_basis {s : set α | is_clopen s}) :
+/-- A T1 space with a clopen basis is totally separated. -/
+lemma totally_separated_space_of_t1_of_basis_clopen [t1_space α]
+  (h : is_topological_basis {s : set α | is_clopen s}) :
   totally_separated_space α :=
 begin
   constructor,
   rintros x - y - hxy,
-  obtain ⟨u, v, hu, hv, xu, yv, disj⟩ := t2_separation hxy,
-  obtain ⟨w, hw : is_clopen w, xw, wu⟩ := (is_topological_basis.mem_nhds_iff h).1
-    (is_open.mem_nhds hu xu),
-  refine ⟨w, wᶜ, hw.1, hw.compl.1, xw, λ h, disj ⟨wu h, yv⟩, _, disjoint_compl_right⟩,
-  rw set.union_compl_self,
+  rcases h.mem_nhds_iff.mp (is_open_ne.mem_nhds hxy) with ⟨U, hU, hxU, hyU⟩,
+  exact ⟨U, Uᶜ, hU.is_open, hU.compl.is_open, hxU, λ h, hyU h rfl,
+    (union_compl_self U).superset, disjoint_compl_right⟩
 end
 
-variables [compact_space α]
+variables [t2_space α] [compact_space α]
 
 /-- A compact Hausdorff space is totally disconnected if and only if it is totally separated, this
   is also true for locally compact spaces. -/
@@ -1678,7 +1676,7 @@ theorem loc_compact_t2_tot_disc_iff_tot_sep :
 begin
   split,
   { introI h,
-    exact tot_sep_of_zero_dim loc_compact_Haus_tot_disc_of_zero_dim, },
+    exact totally_separated_space_of_t1_of_basis_clopen loc_compact_Haus_tot_disc_of_zero_dim },
   apply totally_separated_space.totally_disconnected_space,
 end