feat(data/set/basic): add lemmata (#2353)

* feat(data/set/basic): add lemmata

* switch to term mode proof

* removing dupe

* make linter happy

* Update src/data/set/basic.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* change proof

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 3 people

src/data/set/basic.lean

@@ -703,6 +703,9 @@ by rw [←compl_empty_iff, compl_compl]
 lemma nonempty_compl {s : set α} : (-s : set α).nonempty ↔ s ≠ univ :=
 ne_empty_iff_nonempty.symm.trans $ not_congr $ compl_empty_iff
 
+lemma mem_compl_singleton_iff {a x : α} : x ∈ -({a} : set α) ↔ x ≠ a :=
+not_iff_not_of_iff mem_singleton_iff
+
 theorem union_eq_compl_compl_inter_compl (s t : set α) : s ∪ t = -(-s ∩ -t) :=
 by simp [compl_inter, compl_compl]
 
@@ -735,9 +738,12 @@ 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} : set α) ↔ a ∉ s :=
+by { rw subset_compl_comm, simp }
+
 theorem inter_subset (a b c : set α) : a ∩ b ⊆ c ↔ a ⊆ -b ∪ c :=
 begin
-  haveI := classical.prop_decidable,
+  classical,
   split,
   { intros h x xa, by_cases h' : x ∈ b, simp [h ⟨xa, h'⟩], simp [h'] },
   intros h x, rintro ⟨xa, xb⟩, cases h xa, contradiction, assumption
@@ -1290,6 +1296,10 @@ theorem forall_range_iff {p : α → Prop} : (∀ a ∈ range f, p a) ↔ (∀ i
 theorem exists_range_iff {p : α → Prop} : (∃ a ∈ range f, p a) ↔ (∃ i, p (f i)) :=
 ⟨assume ⟨a, ⟨i, eq⟩, h⟩, ⟨i, eq.symm ▸ h⟩, assume ⟨i, h⟩, ⟨f i, mem_range_self _, h⟩⟩
 
+lemma exists_range_iff' {p : α → Prop} :
+  (∃ a, a ∈ range f ∧ p a) ↔ ∃ i, p (f i) :=
+by simpa only [exists_prop] using exists_range_iff
+
 theorem range_iff_surjective : range f = univ ↔ surjective f :=
 eq_univ_iff_forall
 
@@ -1648,6 +1658,8 @@ end
 
 end prod
 
+/-! ### Lemmas about set-indexed products of sets -/
+
 section pi
 variables {α : Type*} {π : α → Type*}
 
@@ -1678,6 +1690,8 @@ end
 
 end pi
 
+/-! ### Lemmas about `inclusion`, the injection of subtypes induced by `⊆` -/
+
 section inclusion
 variable {α : Type*}