From f66a5ddbc2f86eba8ea2149aaf2ed0e503ab7fc4 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 21 Feb 2022 11:38:06 +0000
Subject: [PATCH] chore(data/set/basic): add a few lemmas and a `@[simp]`
 attribute (#12176)

* rename `set.exists_eq_singleton_iff_nonempty_unique_mem` to `set.exists_eq_singleton_iff_nonempty_subsingleton`, use `set.subsingleton` in the statement;
* add `@[simp]` to `set.subset_compl_singleton_iff`;
* add `set.diff_diff_right_self`.
---
 src/data/set/basic.lean             | 24 +++++++++++++-----------
 src/group_theory/complement.lean    |  4 ++--
 src/topology/separation.lean        |  2 +-
 src/topology/subset_properties.lean |  2 +-
 4 files changed, 17 insertions(+), 15 deletions(-)

diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index fcafe14a9c095..2621a66ee78fd 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -773,16 +773,6 @@ subset.antisymm_iff.trans $ and.comm.trans $ and_congr_left' singleton_subset_if
 lemma eq_singleton_iff_nonempty_unique_mem : s = {a} ↔ s.nonempty ∧ ∀ x ∈ s, x = a :=
 eq_singleton_iff_unique_mem.trans $ and_congr_left $ λ H, ⟨λ h', ⟨_, h'⟩, λ ⟨x, h⟩, H x h ▸ h⟩
 
-lemma exists_eq_singleton_iff_nonempty_unique_mem :
-  (∃ a : α, s = {a}) ↔ (s.nonempty ∧ ∀ a b ∈ s, a = b) :=
-begin
-  refine ⟨_, λ h, _⟩,
-  { rintros ⟨a, rfl⟩,
-    refine ⟨set.singleton_nonempty a, λ b hb c hc, hb.trans hc.symm⟩ },
-  { obtain ⟨a, ha⟩ := h.1,
-    refine ⟨a, set.eq_singleton_iff_unique_mem.mpr ⟨ha, λ b hb, (h.2 b hb a ha)⟩⟩ },
-end
-
 -- while `simp` is capable of proving this, it is not capable of turning the LHS into the RHS.
 @[simp] lemma default_coe_singleton (x : α) : (default : ({x} : set α)) = ⟨x, rfl⟩ := rfl
 
@@ -921,7 +911,7 @@ forall_congr $ λ a, imp_not_comm
 theorem subset_compl_iff_disjoint {s t : set α} : s ⊆ tᶜ ↔ s ∩ t = ∅ :=
 iff.trans (forall_congr $ λ a, and_imp.symm) subset_empty_iff
 
-lemma subset_compl_singleton_iff {a : α} {s : set α} : s ⊆ {a}ᶜ ↔ a ∉ s :=
+@[simp] lemma subset_compl_singleton_iff {a : α} {s : set α} : s ⊆ {a}ᶜ ↔ a ∉ s :=
 subset_compl_comm.trans singleton_subset_iff
 
 theorem inter_subset (a b c : set α) : a ∩ b ⊆ c ↔ a ⊆ bᶜ ∪ c :=
@@ -1109,6 +1099,8 @@ by simp [insert_eq, union_diff_self, -union_singleton, -singleton_union]
 
 @[simp] lemma diff_self {s : set α} : s \ s = ∅ := sdiff_self
 
+lemma diff_diff_right_self (s t : set α)  : s \ (s \ t) = s ∩ t := sdiff_sdiff_right_self
+
 lemma diff_diff_cancel_left {s t : set α} (h : s ⊆ t) : t \ (t \ s) = s :=
 sdiff_sdiff_eq_self h
 
@@ -1637,6 +1629,16 @@ lemma subsingleton_is_top (α : Type*) [partial_order α] : set.subsingleton {x
 lemma subsingleton_is_bot (α : Type*) [partial_order α] : set.subsingleton {x : α | is_bot x} :=
 λ x hx y hy, hx.is_min.eq_of_ge (hy x)
 
+lemma exists_eq_singleton_iff_nonempty_subsingleton :
+  (∃ a : α, s = {a}) ↔ s.nonempty ∧ s.subsingleton :=
+begin
+  refine ⟨_, λ h, _⟩,
+  { rintros ⟨a, rfl⟩,
+    exact ⟨singleton_nonempty a, subsingleton_singleton⟩ },
+  { obtain ⟨a, ha⟩ := h.1,
+    exact ⟨a, eq_singleton_iff_unique_mem.mpr ⟨ha, λ b hb, h.2 hb ha⟩⟩ },
+end
+
 /-- `s`, coerced to a type, is a subsingleton type if and only if `s`
 is a subsingleton set. -/
 @[simp, norm_cast] lemma subsingleton_coe (s : set α) : subsingleton s ↔ s.subsingleton :=
diff --git a/src/group_theory/complement.lean b/src/group_theory/complement.lean
index e8554aca64a67..1e151b8633257 100644
--- a/src/group_theory/complement.lean
+++ b/src/group_theory/complement.lean
@@ -100,7 +100,7 @@ end
 
 @[to_additive] lemma is_complement_top_left : is_complement ⊤ S ↔ ∃ g : G, S = {g} :=
 begin
-  refine ⟨λ h, set.exists_eq_singleton_iff_nonempty_unique_mem.mpr ⟨_, λ a ha b hb, _⟩, _⟩,
+  refine ⟨λ h, set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨_, λ a ha b hb, _⟩, _⟩,
   { obtain ⟨a, ha⟩ := h.2 1,
     exact ⟨a.2.1, a.2.2⟩ },
   { have : (⟨⟨_, mem_top a⁻¹⟩, ⟨a, ha⟩⟩ : (⊤ : set G) × S) = ⟨⟨_, mem_top b⁻¹⟩, ⟨b, hb⟩⟩ :=
@@ -112,7 +112,7 @@ end
 
 @[to_additive] lemma is_complement_top_right : is_complement S ⊤ ↔ ∃ g : G, S = {g} :=
 begin
-  refine ⟨λ h, set.exists_eq_singleton_iff_nonempty_unique_mem.mpr ⟨_, λ a ha b hb, _⟩, _⟩,
+  refine ⟨λ h, set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨_, λ a ha b hb, _⟩, _⟩,
   { obtain ⟨a, ha⟩ := h.2 1,
     exact ⟨a.1.1, a.1.2⟩ },
   { have : (⟨⟨a, ha⟩, ⟨_, mem_top a⁻¹⟩⟩ : S × (⊤ : set G)) = ⟨⟨b, hb⟩, ⟨_, mem_top b⁻¹⟩⟩ :=
diff --git a/src/topology/separation.lean b/src/topology/separation.lean
index e8a9fc06b617e..c60f1ec5703be 100644
--- a/src/topology/separation.lean
+++ b/src/topology/separation.lean
@@ -1169,7 +1169,7 @@ lemma is_irreducible_iff_singleton [t2_space α] (S : set α) :
 begin
   split,
   { intro h,
-    rw exists_eq_singleton_iff_nonempty_unique_mem,
+    rw exists_eq_singleton_iff_nonempty_subsingleton,
     use h.1,
     intros a ha b hb,
     injection @@subsingleton.elim ((is_preirreducible_iff_subsingleton _).mp h.2) ⟨_, ha⟩ ⟨_, hb⟩ },
diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean
index 997fa53d48f29..b7299a43cb677 100644
--- a/src/topology/subset_properties.lean
+++ b/src/topology/subset_properties.lean
@@ -1405,7 +1405,7 @@ lemma is_preirreducible_of_subsingleton (s : set α) [hs : subsingleton s] : is_
 begin
   cases s.eq_empty_or_nonempty,
   { exact h.symm ▸ is_preirreducible_empty },
-  { obtain ⟨x, e⟩ := exists_eq_singleton_iff_nonempty_unique_mem.mpr
+  { obtain ⟨x, e⟩ := exists_eq_singleton_iff_nonempty_subsingleton.mpr
       ⟨h, λ _ ha _ hb, by injection @@subsingleton.elim hs ⟨_, ha⟩ ⟨_, hb⟩⟩,
     exact e.symm ▸ is_irreducible_singleton.2 }
 end