chore(topology/separation): golf some proofs (#14279)

* extract `minimal_nonempty_closed_eq_singleton` out of the proof of
  `is_closed.exists_closed_singleton`;

* replace `exists_open_singleton_of_open_finset` with
  `exists_open_singleton_of_open_finite`, extract
  `minimal_nonempty_open_eq_singleton` out of its proof.

* add `exists_is_open_xor_mem`, an alias for `t0_space.t0`.

src/topology/separation.lean

@@ -158,6 +158,10 @@ end separated
 class t0_space (α : Type u) [topological_space α] : Prop :=
 (t0 : ∀ x y, x ≠ y → ∃ U:set α, is_open U ∧ (xor (x ∈ U) (y ∈ U)))
 
+lemma exists_is_open_xor_mem [t0_space α] {x y : α} (h : x ≠ y) :
+  ∃ U:set α, is_open U ∧ xor (x ∈ U) (y ∈ U) :=
+t0_space.t0 x y h
+
 lemma t0_space_def (α : Type u) [topological_space α] :
   t0_space α ↔ ∀ x y, x ≠ y → ∃ U:set α, is_open U ∧ (xor (x ∈ U) (y ∈ U)) :=
 by { split, apply @t0_space.t0, apply t0_space.mk }
@@ -206,71 +210,62 @@ lemma subtype_indistinguishable_iff {α : Type u} [topological_space α] {U : se
   indistinguishable x y ↔ indistinguishable (x : α) y :=
 by { simp_rw [indistinguishable_iff_closure, closure_subtype, image_singleton] }
 
+theorem minimal_nonempty_closed_eq_singleton [t0_space α] {s : set α} (hs : is_closed s)
+  (hne : s.nonempty) (hmin : ∀ t ⊆ s, t.nonempty → is_closed t → t = s) :
+  ∃ x, s = {x} :=
+begin
+  suffices : s.subsingleton, from exists_eq_singleton_iff_nonempty_subsingleton.2 ⟨hne, this⟩,
+  refine λ x hx y hy, of_not_not (λ hxy, _),
+  rcases exists_is_open_xor_mem hxy with ⟨U, hUo, hU⟩,
+  wlog h : x ∈ U ∧ y ∉ U := hU using [x y, y x], cases h with hxU hyU,
+  have : s \ U = s := hmin (s \ U) (diff_subset _ _) ⟨y, hy, hyU⟩ (hs.sdiff hUo),
+  exact (this.symm.subset hx).2 hxU
+end
+
 /-- Given a closed set `S` in a compact T₀ space,
 there is some `x ∈ S` such that `{x}` is closed. -/
 theorem is_closed.exists_closed_singleton {α : Type*} [topological_space α]
   [t0_space α] [compact_space α] {S : set α} (hS : is_closed S) (hne : S.nonempty) :
   ∃ (x : α), x ∈ S ∧ is_closed ({x} : set α) :=
 begin
   obtain ⟨V, Vsub, Vne, Vcls, hV⟩ := hS.exists_minimal_nonempty_closed_subset hne,
-  by_cases hnt : ∃ (x y : α) (hx : x ∈ V) (hy : y ∈ V), x ≠ y,
-  { exfalso,
-    obtain ⟨x, y, hx, hy, hne⟩ := hnt,
-    obtain ⟨U, hU, hsep⟩ := t0_space.t0 _ _ hne,
-    have : ∀ (z w : α) (hz : z ∈ V) (hw : w ∈ V) (hz' : z ∈ U) (hw' : ¬ w ∈ U), false,
-    { intros z w hz hw hz' hw',
-      have uvne : (V ∩ Uᶜ).nonempty,
-      { use w, simp only [hw, hw', set.mem_inter_eq, not_false_iff, and_self, set.mem_compl_eq], },
-      specialize hV (V ∩ Uᶜ) (set.inter_subset_left _ _) uvne
-        (is_closed.inter Vcls (is_closed_compl_iff.mpr hU)),
-      have : V ⊆ Uᶜ,
-      { rw ←hV, exact set.inter_subset_right _ _ },
-      exact this hz hz', },
-    cases hsep,
-    { exact this x y hx hy hsep.1 hsep.2 },
-    { exact this y x hy hx hsep.1 hsep.2 } },
-  { push_neg at hnt,
-    obtain ⟨z, hz⟩ := Vne,
-    refine ⟨z, Vsub hz, _⟩,
-    convert Vcls,
-    ext,
-    simp only [set.mem_singleton_iff, set.mem_compl_eq],
-    split,
-    { rintro rfl, exact hz, },
-    { exact λ hx, hnt x z hx hz, }, },
+  rcases minimal_nonempty_closed_eq_singleton Vcls Vne hV with ⟨x, rfl⟩,
+  exact ⟨x, Vsub (mem_singleton x), Vcls⟩
 end
 
-/-- Given an open `finset` `S` in a T₀ space, there is some `x ∈ S` such that `{x}` is open. -/
-theorem exists_open_singleton_of_open_finset [t0_space α] (s : finset α) (sne : s.nonempty)
-  (hso : is_open (s : set α)) :
+theorem minimal_nonempty_open_eq_singleton [t0_space α] {s : set α} (hs : is_open s)
+  (hne : s.nonempty) (hmin : ∀ t ⊆ s, t.nonempty → is_open t → t = s) :
+  ∃ x, s = {x} :=
+begin
+  suffices : s.subsingleton, from exists_eq_singleton_iff_nonempty_subsingleton.2 ⟨hne, this⟩,
+  refine λ x hx y hy, of_not_not (λ hxy, _),
+  rcases exists_is_open_xor_mem hxy with ⟨U, hUo, hU⟩,
+  wlog h : x ∈ U ∧ y ∉ U := hU using [x y, y x], cases h with hxU hyU,
+  have : s ∩ U = s := hmin (s ∩ U) (inter_subset_left _ _) ⟨x, hx, hxU⟩ (hs.inter hUo),
+  exact hyU (this.symm.subset hy).2
+end
+
+/-- Given an open finite set `S` in a T₀ space, there is some `x ∈ S` such that `{x}` is open. -/
+theorem exists_open_singleton_of_open_finite [t0_space α] {s : set α} (hfin : s.finite)
+  (hne : s.nonempty) (ho : is_open s) :
   ∃ x ∈ s, is_open ({x} : set α):=
 begin
+  lift s to finset α using hfin,
   induction s using finset.strong_induction_on with s ihs,
-  by_cases hs : set.subsingleton (s : set α),
-  { rcases sne with ⟨x, hx⟩,
-    refine ⟨x, hx, _⟩,
-    have : (s : set α) = {x}, from hs.eq_singleton_of_mem hx,
-    rwa this at hso },
-  { dunfold set.subsingleton at hs,
-    push_neg at hs,
-    rcases hs with ⟨x, hx, y, hy, hxy⟩,
-    rcases t0_space.t0 x y hxy with ⟨U, hU, hxyU⟩,
-    wlog H : x ∈ U ∧ y ∉ U := hxyU using [x y, y x],
-    obtain ⟨z, hzs, hz⟩ : ∃ z ∈ s.filter (λ z, z ∈ U), is_open ({z} : set α),
-    { refine ihs _ (finset.filter_ssubset.2 ⟨y, hy, H.2⟩) ⟨x, finset.mem_filter.2 ⟨hx, H.1⟩⟩ _,
-      rw [finset.coe_filter],
-      exact is_open.inter hso hU },
-    exact ⟨z, (finset.mem_filter.1 hzs).1, hz⟩ }
+  rcases em (∃ t ⊂ s, t.nonempty ∧ is_open (t : set α)) with ⟨t, hts, htne, hto⟩|ht,
+  { rcases ihs t hts htne hto with ⟨x, hxt, hxo⟩,
+    exact ⟨x, hts.1 hxt, hxo⟩ },
+  { rcases minimal_nonempty_open_eq_singleton ho hne _ with ⟨x, hx⟩,
+    { exact ⟨x, hx.symm ▸ rfl, hx ▸ ho⟩ },
+    refine λ t hts htne hto, of_not_not (λ hts', ht _),
+    lift t to finset α using s.finite_to_set.subset hts,
+    exact ⟨t, ssubset_iff_subset_ne.2 ⟨hts, mt finset.coe_inj.2 hts'⟩, htne, hto⟩ }
 end
 
-theorem exists_open_singleton_of_fintype [t0_space α] [f : fintype α] [ha : nonempty α] :
+theorem exists_open_singleton_of_fintype [t0_space α] [fintype α] [nonempty α] :
   ∃ x:α, is_open ({x}:set α) :=
-begin
-  refine ha.elim (λ x, _),
-  have : is_open ((finset.univ : finset α) : set α), { simp },
-  rcases exists_open_singleton_of_open_finset _ ⟨x, finset.mem_univ x⟩ this with ⟨x, _, hx⟩,
-  exact ⟨x, hx⟩
-end
+let ⟨x, _, h⟩ := exists_open_singleton_of_open_finite (finite.of_fintype _) univ_nonempty
+  is_open_univ in ⟨x, h⟩
 
 lemma t0_space_of_injective_of_continuous [topological_space β] {f : α → β}
   (hf : function.injective f) (hf' : continuous f) [t0_space β] : t0_space α :=