chore(*): move/add lemmas about disjoint (#5277)

* `set.disjoint_compl_left` and `set.disjoint_compl_right`:
  - generalize to any `boolean_algebra`,
  - move to `order/boolean_algebra`,
  - drop `set.` prefix,
  - make the argument implicit to follow the style of other lemmas in `order/boolean_algebra`
* add `set.disjoint_empty` and `set.empty_disjoint`
* add `disjoint_top` and `top_disjoint`, use in `set.disjoint_univ`and `set.univ_disjoint`.

Author: urkud

src/data/set/lattice.lean

@@ -1116,15 +1116,15 @@ disjoint_sup_right
 theorem disjoint_diff {a b : set α} : disjoint a (b \ a) :=
 disjoint_iff.2 (inter_diff_self _ _)
 
-theorem disjoint_compl_left (s : set α) : disjoint sᶜ s := assume a ⟨h₁, h₂⟩, h₁ h₂
+@[simp] theorem disjoint_empty (s : set α) : disjoint s ∅ := disjoint_bot_right
 
-theorem disjoint_compl_right (s : set α) : disjoint s sᶜ := assume a ⟨h₁, h₂⟩, h₂ h₁
+@[simp] theorem empty_disjoint (s : set α) : disjoint ∅ s := disjoint_bot_left
 
 @[simp] lemma univ_disjoint {s : set α}: disjoint univ s ↔ s = ∅ :=
-by simp [set.disjoint_iff_inter_eq_empty]
+top_disjoint
 
 @[simp] lemma disjoint_univ {s : set α} : disjoint s univ ↔ s = ∅ :=
-by simp [set.disjoint_iff_inter_eq_empty]
+disjoint_top
 
 @[simp] theorem disjoint_singleton_left {a : α} {s : set α} : disjoint {a} s ↔ a ∉ s :=
 by simp [set.disjoint_iff, subset_def]; exact iff.rfl

src/linear_algebra/basic.lean

@@ -2517,8 +2517,8 @@ lemma disjoint_std_basis_std_basis (I J : set ι) (h : disjoint I J) :
   disjoint (⨆i∈I, range (std_basis R φ i)) (⨆i∈J, range (std_basis R φ i)) :=
 begin
   refine disjoint.mono
-    (supr_range_std_basis_le_infi_ker_proj _ _ _ _ $ set.disjoint_compl_right I)
-    (supr_range_std_basis_le_infi_ker_proj _ _ _ _ $ set.disjoint_compl_right J) _,
+    (supr_range_std_basis_le_infi_ker_proj _ _ _ _ $ disjoint_compl_right)
+    (supr_range_std_basis_le_infi_ker_proj _ _ _ _ $ disjoint_compl_right) _,
   simp only [disjoint, submodule.le_def', mem_infi, mem_inf, mem_ker, mem_bot, proj_apply,
     funext_iff],
   rintros b ⟨hI, hJ⟩ i,

src/linear_algebra/finsupp.lean

@@ -131,8 +131,8 @@ lemma disjoint_lsingle_lsingle (s t : set α) (hs : disjoint s t) :
   disjoint (⨆a∈s, (lsingle a : M →ₗ[R] (α →₀ M)).range) (⨆a∈t, (lsingle a).range) :=
 begin
   refine disjoint.mono
-    (lsingle_range_le_ker_lapply _ _ $ disjoint_compl_right s)
-    (lsingle_range_le_ker_lapply _ _ $ disjoint_compl_right t)
+    (lsingle_range_le_ker_lapply _ _ $ disjoint_compl_right)
+    (lsingle_range_le_ker_lapply _ _ $ disjoint_compl_right)
     (le_trans (le_infi $ assume i, _) infi_ker_lapply_le_bot),
   classical,
   by_cases his : i ∈ s,

src/linear_algebra/matrix.lean

@@ -621,7 +621,7 @@ begin
   simp only [comap_infi, (ker_comp _ _).symm, proj_diagonal, ker_smul'],
   have : univ ⊆ {i : m | w i = 0} ∪ {i : m | w i = 0}ᶜ, { rw set.union_compl_self },
   exact (supr_range_std_basis_eq_infi_ker_proj K (λi:m, K)
-    (disjoint_compl_right {i | w i = 0}) this (finite.of_fintype _)).symm
+    disjoint_compl_right this (finite.of_fintype _)).symm
 end
 
 lemma range_diagonal [decidable_eq m] (w : m → K) :
@@ -637,7 +637,7 @@ lemma rank_diagonal [decidable_eq m] [decidable_eq K] (w : m → K) :
   rank (diagonal w).to_lin' = fintype.card { i // w i ≠ 0 } :=
 begin
   have hu : univ ⊆ {i : m | w i = 0}ᶜ ∪ {i : m | w i = 0}, { rw set.compl_union_self },
-  have hd : disjoint {i : m | w i ≠ 0} {i : m | w i = 0} := (disjoint_compl_right {i | w i = 0}).symm,
+  have hd : disjoint {i : m | w i ≠ 0} {i : m | w i = 0} := disjoint_compl_left,
   have h₁ := supr_range_std_basis_eq_infi_ker_proj K (λi:m, K) hd hu (finite.of_fintype _),
   have h₂ := @infi_ker_proj_equiv K _ _ (λi:m, K) _ _ _ _ (by simp; apply_instance) hd hu,
   rw [rank, range_diagonal, h₁, ←@dim_fun' K],

src/measure_theory/measure_space.lean

@@ -824,7 +824,7 @@ end
 
 @[simp] lemma restrict_add_restrict_compl {s : set α} (hs : is_measurable s) :
   μ.restrict s + μ.restrict sᶜ = μ :=
-by rw [← restrict_union (disjoint_compl_right _) hs hs.compl, union_compl_self, restrict_univ]
+by rw [← restrict_union disjoint_compl_right hs hs.compl, union_compl_self, restrict_univ]
 
 @[simp] lemma restrict_compl_add_restrict {s : set α} (hs : is_measurable s) :
   μ.restrict sᶜ + μ.restrict s = μ :=

src/measure_theory/set_integral.lean

@@ -331,7 +331,7 @@ lemma integral_univ : ∫ x in univ, f x ∂μ = ∫ x, f x ∂μ := by rw [meas
 
 lemma integral_add_compl (hs : is_measurable s) (hfi : integrable f μ) :
   ∫ x in s, f x ∂μ + ∫ x in sᶜ, f x ∂μ = ∫ x, f x ∂μ :=
-by rw [← integral_union (disjoint_compl_right s) hs hs.compl hfi.integrable_on hfi.integrable_on,
+by rw [← integral_union disjoint_compl_right hs hs.compl hfi.integrable_on hfi.integrable_on,
   union_compl_self, integral_univ]
 
 /-- For a measurable function `f` and a measurable set `s`, the integral of `indicator s f`

src/order/boolean_algebra.lean

@@ -49,6 +49,9 @@ is_compl.of_eq inf_compl_eq_bot sup_compl_eq_top
 theorem is_compl.compl_eq (h : is_compl x y) : xᶜ = y :=
 (h.right_unique is_compl_compl).symm
 
+theorem disjoint_compl_right : disjoint x xᶜ := is_compl_compl.disjoint
+theorem disjoint_compl_left : disjoint xᶜ x := disjoint_compl_right.symm
+
 theorem sdiff_eq : x \ y = x ⊓ yᶜ :=
 boolean_algebra.sdiff_eq x y
 

src/order/bounded_lattice.lean

@@ -954,8 +954,8 @@ by rw [disjoint, disjoint, inf_comm]
 @[symm] theorem disjoint.symm ⦃a b : α⦄ : disjoint a b → disjoint b a :=
 disjoint.comm.1
 
-@[simp] theorem disjoint_bot_left {a : α} : disjoint ⊥ a := disjoint_iff.2 bot_inf_eq
-@[simp] theorem disjoint_bot_right {a : α} : disjoint a ⊥ := disjoint_iff.2 inf_bot_eq
+@[simp] theorem disjoint_bot_left {a : α} : disjoint ⊥ a := inf_le_left
+@[simp] theorem disjoint_bot_right {a : α} : disjoint a ⊥ := inf_le_right
 
 theorem disjoint.mono {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
   disjoint b d → disjoint a c := le_trans (inf_le_inf h₁ h₂)
@@ -974,6 +974,15 @@ by { intro h, rw [←h, disjoint_self] at hab, exact ha hab }
 
 end semilattice_inf_bot
 
+section bounded_lattice
+
+variables [bounded_lattice α] {a : α}
+
+@[simp] theorem disjoint_top : disjoint a ⊤ ↔ a = ⊥ := by simp [disjoint_iff]
+@[simp] theorem top_disjoint : disjoint ⊤ a ↔ a = ⊥ := by simp [disjoint_iff]
+
+end bounded_lattice
+
 section bounded_distrib_lattice
 
 variables [bounded_distrib_lattice α] {a b c : α}

src/ring_theory/localization.lean

@@ -1173,7 +1173,7 @@ begin
   ext x,
   split; simp only [local_ring.mem_maximal_ideal, mem_nonunits_iff]; intro hx,
   { exact λ h, (localization_map.is_prime_of_is_prime_disjoint f P hP
-      (set.disjoint_compl_left P.carrier)).1 (ideal.eq_top_of_is_unit_mem _ hx h) },
+      disjoint_compl_left).1 (ideal.eq_top_of_is_unit_mem _ hx h) },
   { obtain ⟨⟨a, b⟩, hab⟩ := localization_map.surj f x,
     contrapose! hx,
     rw is_unit_iff_exists_inv,