chore(data/set/basic): reuse some proofs about boolean_algebra (#5728)

API changes:

* merge `set.compl_compl` with `compl_compl'`;
* add `is_compl.compl_eq_iff`, `compl_eq_top`, and `compl_eq_bot`;
* add `simp` attribute to `compl_le_compl_iff_le`;
* fix misleading name in `compl_le_iff_compl_le`, add a missing
  variant;
* add `simp` attribute to `compl_empty_iff` and `compl_univ_iff`;
* add `set.subset.eventually_le`.

src/algebraic_geometry/prime_spectrum.lean

@@ -324,7 +324,7 @@ by simp only [@eq_comm _ Uᶜ]; refl
 
 lemma is_closed_iff_zero_locus (Z : set (prime_spectrum R)) :
   is_closed Z ↔ ∃ s, Z = zero_locus s :=
-by rw [is_closed, is_open_iff, set.compl_compl]
+by rw [is_closed, is_open_iff, compl_compl]
 
 lemma is_closed_zero_locus (s : set R) :
   is_closed (zero_locus s) :=

src/data/set/basic.lean

@@ -802,40 +802,27 @@ theorem not_mem_of_mem_compl {s : set α} {x : α} (h : x ∈ sᶜ) : x ∉ s :=
 
 theorem mem_compl_iff (s : set α) (x : α) : x ∈ sᶜ ↔ x ∉ s := iff.rfl
 
-@[simp] theorem inter_compl_self (s : set α) : s ∩ sᶜ = ∅ :=
-by finish [ext_iff]
-
-@[simp] theorem compl_inter_self (s : set α) : sᶜ ∩ s = ∅ :=
-by finish [ext_iff]
+@[simp] theorem inter_compl_self (s : set α) : s ∩ sᶜ = ∅ := inf_compl_eq_bot
 
-@[simp] theorem compl_empty : (∅ : set α)ᶜ = univ :=
-by finish [ext_iff]
+@[simp] theorem compl_inter_self (s : set α) : sᶜ ∩ s = ∅ := compl_inf_eq_bot
 
-@[simp] theorem compl_union (s t : set α) : (s ∪ t)ᶜ = sᶜ ∩ tᶜ :=
-by finish [ext_iff]
+@[simp] theorem compl_empty : (∅ : set α)ᶜ = univ := compl_bot
 
-local attribute [simp] -- Will be generalized to lattices in `compl_compl'`
-theorem compl_compl (s : set α) : sᶜᶜ = s :=
-by finish [ext_iff]
+@[simp] theorem compl_union (s t : set α) : (s ∪ t)ᶜ = sᶜ ∩ tᶜ := compl_sup
 
--- ditto
-theorem compl_inter (s t : set α) : (s ∩ t)ᶜ = sᶜ ∪ tᶜ :=
-by finish [ext_iff]
+theorem compl_inter (s t : set α) : (s ∩ t)ᶜ = sᶜ ∪ tᶜ := compl_inf
 
-@[simp] theorem compl_univ : (univ : set α)ᶜ = ∅ :=
-by finish [ext_iff]
+@[simp] theorem compl_univ : (univ : set α)ᶜ = ∅ := compl_top
 
-lemma compl_empty_iff {s : set α} : sᶜ = ∅ ↔ s = univ :=
-by { split, intro h, rw [←compl_compl s, h, compl_empty], intro h, rw [h, compl_univ] }
+@[simp] lemma compl_empty_iff {s : set α} : sᶜ = ∅ ↔ s = univ := compl_eq_bot
 
-lemma compl_univ_iff {s : set α} : sᶜ = univ ↔ s = ∅ :=
-by rw [←compl_empty_iff, compl_compl]
+@[simp] lemma compl_univ_iff {s : set α} : sᶜ = univ ↔ s = ∅ := compl_eq_top
 
 lemma nonempty_compl {s : set α} : sᶜ.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
+not_congr mem_singleton_iff
 
 lemma compl_singleton_eq (a : α) : ({a} : set α)ᶜ = {x | x ≠ a} :=
 ext $ λ x, mem_compl_singleton_iff
@@ -856,11 +843,10 @@ theorem compl_comp_compl : compl ∘ compl = @id (set α) :=
 funext compl_compl
 
 theorem compl_subset_comm {s t : set α} : sᶜ ⊆ t ↔ tᶜ ⊆ s :=
-by haveI := classical.prop_decidable; exact
-forall_congr (λ a, not_imp_comm)
+@compl_le_iff_compl_le _ s t _
 
 lemma compl_subset_compl {s t : set α} : sᶜ ⊆ tᶜ ↔ t ⊆ s :=
-by rw [compl_subset_comm, compl_compl]
+@compl_le_compl_iff_le _ t s _
 
 theorem compl_subset_iff_union {s t : set α} : sᶜ ⊆ t ↔ s ∪ t = univ :=
 iff.symm $ eq_univ_iff_forall.trans $ forall_congr $ λ a,

src/measure_theory/measurable_space.lean

@@ -98,7 +98,7 @@ lemma is_measurable.compl : is_measurable s → is_measurable sᶜ :=
 ‹measurable_space α›.is_measurable_compl s
 
 lemma is_measurable.of_compl (h : is_measurable sᶜ) : is_measurable s :=
-s.compl_compl ▸ h.compl
+compl_compl s ▸ h.compl
 
 @[simp] lemma is_measurable.compl_iff : is_measurable sᶜ ↔ is_measurable s :=
 ⟨is_measurable.of_compl, is_measurable.compl⟩

src/order/boolean_algebra.lean

@@ -64,15 +64,24 @@ is_compl_top_bot.compl_eq
 @[simp] theorem compl_bot : ⊥ᶜ = (⊤:α) :=
 is_compl_bot_top.compl_eq
 
-@[simp] theorem compl_compl' : xᶜᶜ = x :=
+@[simp] theorem compl_compl (x : α) : xᶜᶜ = x :=
 is_compl_compl.symm.compl_eq
 
 theorem compl_injective : function.injective (compl : α → α) :=
-function.involutive.injective $ λ x, compl_compl'
+function.involutive.injective compl_compl
 
 @[simp] theorem compl_inj_iff : xᶜ = yᶜ ↔ x = y :=
 compl_injective.eq_iff
 
+theorem is_compl.compl_eq_iff (h : is_compl x y) : zᶜ = y ↔ z = x :=
+h.compl_eq ▸ compl_inj_iff
+
+@[simp] theorem compl_eq_top : xᶜ = ⊤ ↔ x = ⊥ :=
+is_compl_bot_top.compl_eq_iff
+
+@[simp] theorem compl_eq_bot : xᶜ = ⊥ ↔ x = ⊤ :=
+is_compl_top_bot.compl_eq_iff
+
 @[simp] theorem compl_inf : (x ⊓ y)ᶜ = xᶜ ⊔ yᶜ :=
 (is_compl_compl.inf_sup is_compl_compl).compl_eq
 
@@ -82,19 +91,22 @@ compl_injective.eq_iff
 theorem compl_le_compl (h : y ≤ x) : xᶜ ≤ yᶜ :=
 is_compl_compl.antimono is_compl_compl h
 
-theorem compl_le_compl_iff_le : yᶜ ≤ xᶜ ↔ x ≤ y :=
+@[simp] theorem compl_le_compl_iff_le : yᶜ ≤ xᶜ ↔ x ≤ y :=
 ⟨assume h, by have h := compl_le_compl h; simp at h; assumption,
   compl_le_compl⟩
 
 theorem le_compl_of_le_compl (h : y ≤ xᶜ) : x ≤ yᶜ :=
-by simpa only [compl_compl'] using compl_le_compl h
+by simpa only [compl_compl] using compl_le_compl h
 
 theorem compl_le_of_compl_le (h : yᶜ ≤ x) : xᶜ ≤ y :=
-by simpa only [compl_compl'] using compl_le_compl h
+by simpa only [compl_compl] using compl_le_compl h
 
-theorem compl_le_iff_compl_le : y ≤ xᶜ ↔ x ≤ yᶜ :=
+theorem le_compl_iff_le_compl : y ≤ xᶜ ↔ x ≤ yᶜ :=
 ⟨le_compl_of_le_compl, le_compl_of_le_compl⟩
 
+theorem compl_le_iff_compl_le : xᶜ ≤ y ↔ yᶜ ≤ x :=
+⟨compl_le_of_compl_le, compl_le_of_compl_le⟩
+
 theorem sup_sdiff_same : x ⊔ (y \ x) = x ⊔ y :=
 by simp [sdiff_eq, sup_inf_left]
 

src/order/filter/basic.lean

@@ -2403,3 +2403,6 @@ lemma set.eq_on.eventually_eq_of_mem {α β} {s : set α} {l : filter α} {f g :
   (h : eq_on f g s) (hl : s ∈ l) :
   f =ᶠ[l] g :=
 h.eventually_eq.filter_mono $ filter.le_principal_iff.2 hl
+
+lemma set.subset.eventually_le {α} {l : filter α} {s t : set α} (h : s ⊆ t) : s ≤ᶠ[l] t :=
+filter.eventually_of_forall h

src/order/filter/ultrafilter.lean

@@ -283,7 +283,7 @@ alias compl_mem_hyperfilter_of_finite ← set.finite.compl_mem_hyperfilter
 
 theorem mem_hyperfilter_of_finite_compl {s : set α} (hf : set.finite sᶜ) :
   s ∈ hyperfilter α :=
-s.compl_compl ▸ hf.compl_mem_hyperfilter
+compl_compl s ▸ hf.compl_mem_hyperfilter
 
 end hyperfilter
 

src/topology/separation.lean

@@ -722,7 +722,7 @@ begin
     (λ Z : {Z : set α // is_clopen Z ∧ x ∈ Z}, Z) (λ Z, Z.2.1.2)),
   rw [←not_imp_not, not_forall, not_nonempty_iff_eq_empty, inter_comm] at H1,
   have huv_union := subset.trans hab (union_subset_union hau hbv),
-  rw [←set.compl_compl (u ∪ v), subset_compl_iff_disjoint] at huv_union,
+  rw [← compl_compl (u ∪ v), subset_compl_iff_disjoint] at huv_union,
   cases H1 huv_union with Zi H2,
   refine ⟨(⋂ (U ∈ Zi), subtype.val U), _, _, _⟩,
   { exact is_clopen_bInter (λ Z hZ, Z.2.1) },