chore(order/bounded_order): Golf disjoint API (#14194)

Reorder lemmas and golf.

Lemma additions:
* `disjoint.eq_bot_of_ge`
* `is_compl.of_dual`
* `is_compl_to_dual_iff`
* `is_compl_of_dual_iff`

Lemma deletions:
* `eq_bot_of_disjoint_absorbs`: This is an unhelpful combination of `disjoint.eq_bot_of_ge` and `sup_eq_left`
* `inf_eq_bot_iff_le_compl`: This is a worse version of `is_compl.disjoint_left_iff`

Lemma renames:
* `is_compl.to_order_dual` → `is_compl.dual`

src/order/bounded_order.lean

@@ -40,14 +40,16 @@ We didn't prove things about `[distrib_lattice α] [order_top α]` because the d
 `disjoint` isn't really used anywhere.
 -/
 
-/-! ### Top, bottom element -/
+open order_dual
 
 set_option old_structure_cmd true
 
 universes u v
 
 variables {α : Type u} {β : Type v}
 
+/-! ### Top, bottom element -/
+
 /-- Typeclass for the `⊤` (`\top`) notation -/
 @[notation_class] class has_top (α : Type u) := (top : α)
 /-- Typeclass for the `⊥` (`\bot`) notation -/
@@ -1130,110 +1132,95 @@ instance [has_le α] [has_le β] [bounded_order α] [bounded_order β] : bounded
 
 end prod
 
+section linear_order
+variables [linear_order α]
+
+-- `simp` can prove these, so they shouldn't be simp-lemmas.
+lemma min_bot_left [order_bot α] (a : α) : min ⊥ a = ⊥ := bot_inf_eq
+lemma max_top_left [order_top α] (a : α) : max ⊤ a = ⊤ := top_sup_eq
+lemma min_top_left [order_top α] (a : α) : min ⊤ a = a := top_inf_eq
+lemma max_bot_left [order_bot α] (a : α) : max ⊥ a = a := bot_sup_eq
+lemma min_top_right [order_top α] (a : α) : min a ⊤ = a := inf_top_eq
+lemma max_bot_right [order_bot α] (a : α) : max a ⊥ = a := sup_bot_eq
+lemma min_bot_right [order_bot α] (a : α) : min a ⊥ = ⊥ := inf_bot_eq
+lemma max_top_right [order_top α] (a : α) : max a ⊤ = ⊤ := sup_top_eq
+
+@[simp] lemma min_eq_bot [order_bot α] {a b : α} : min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥ :=
+by simp only [←inf_eq_min, ←le_bot_iff, inf_le_iff]
+
+@[simp] lemma max_eq_top [order_top α] {a b : α} : max a b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
+@min_eq_bot αᵒᵈ _ _ a b
+
+@[simp] lemma max_eq_bot [order_bot α] {a b : α} : max a b = ⊥ ↔ a = ⊥ ∧ b = ⊥ := sup_eq_bot_iff
+@[simp] lemma min_eq_top [order_top α] {a b : α} : min a b = ⊤ ↔ a = ⊤ ∧ b = ⊤ := inf_eq_top_iff
+
+end linear_order
+
 /-! ### Disjointness and complements -/
 
 section disjoint
 section semilattice_inf_bot
-variables [semilattice_inf α] [order_bot α]
+variables [semilattice_inf α] [order_bot α] {a b c d : α}
 
 /-- Two elements of a lattice are disjoint if their inf is the bottom element.
   (This generalizes disjoint sets, viewed as members of the subset lattice.) -/
 def disjoint (a b : α) : Prop := a ⊓ b ≤ ⊥
 
-theorem disjoint.eq_bot {a b : α} (h : disjoint a b) : a ⊓ b = ⊥ :=
-eq_bot_iff.2 h
-
-theorem disjoint_iff {a b : α} : disjoint a b ↔ a ⊓ b = ⊥ :=
-eq_bot_iff.symm
+lemma disjoint_iff : disjoint a b ↔ a ⊓ b = ⊥ := le_bot_iff
+lemma disjoint.eq_bot : disjoint a b → a ⊓ b = ⊥ := bot_unique
+lemma disjoint.comm : disjoint a b ↔ disjoint b a := by rw [disjoint, disjoint, inf_comm]
+@[symm] lemma disjoint.symm ⦃a b : α⦄ : disjoint a b → disjoint b a := disjoint.comm.1
+lemma symmetric_disjoint : symmetric (disjoint : α → α → Prop) := disjoint.symm
+lemma disjoint_assoc : disjoint (a ⊓ b) c ↔ disjoint a (b ⊓ c) :=
+by rw [disjoint, disjoint, inf_assoc]
 
-theorem disjoint.comm {a b : α} : disjoint a b ↔ disjoint b a :=
-by rw [disjoint, disjoint, inf_comm]
+@[simp] lemma disjoint_bot_left : disjoint ⊥ a := inf_le_left
+@[simp] lemma disjoint_bot_right : disjoint a ⊥ := inf_le_right
 
-@[symm] theorem disjoint.symm ⦃a b : α⦄ : disjoint a b → disjoint b a :=
-disjoint.comm.1
+lemma disjoint.mono (h₁ : a ≤ b) (h₂ : c ≤ d) : disjoint b d → disjoint a c :=
+le_trans $ inf_le_inf h₁ h₂
 
-lemma symmetric_disjoint : symmetric (disjoint : α → α → Prop) := disjoint.symm
+lemma disjoint.mono_left (h : a ≤ b) : disjoint b c → disjoint a c := disjoint.mono h le_rfl
+lemma disjoint.mono_right : b ≤ c → disjoint a c → disjoint a b := disjoint.mono le_rfl
 
-@[simp] theorem disjoint_bot_left {a : α} : disjoint ⊥ a := inf_le_left
-@[simp] theorem disjoint_bot_right {a : α} : disjoint a ⊥ := inf_le_right
+variables (c)
 
-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₂)
+lemma disjoint.inf_left (h : disjoint a b) : disjoint (a ⊓ c) b := h.mono_left inf_le_left
+lemma disjoint.inf_left' (h : disjoint a b) : disjoint (c ⊓ a) b := h.mono_left inf_le_right
+lemma disjoint.inf_right (h : disjoint a b) : disjoint a (b ⊓ c) := h.mono_right inf_le_left
+lemma disjoint.inf_right' (h : disjoint a b) : disjoint a (c ⊓ b) := h.mono_right inf_le_right
 
-theorem disjoint.mono_left {a b c : α} (h : a ≤ b) : disjoint b c → disjoint a c :=
-disjoint.mono h le_rfl
+variables {c}
 
-theorem disjoint.mono_right {a b c : α} (h : b ≤ c) : disjoint a c → disjoint a b :=
-disjoint.mono le_rfl h
+@[simp] lemma disjoint_self : disjoint a a ↔ a = ⊥ := by simp [disjoint]
 
-@[simp] lemma disjoint_self {a : α} : disjoint a a ↔ a = ⊥ :=
-by simp [disjoint]
+/- TODO: Rename `disjoint.eq_bot` to `disjoint.inf_eq` and `disjoint.eq_bot_of_self` to
+`disjoint.eq_bot` -/
+alias disjoint_self ↔ disjoint.eq_bot_of_self _
 
-lemma disjoint.ne {a b : α} (ha : a ≠ ⊥) (hab : disjoint a b) : a ≠ b :=
-by { intro h, rw [←h, disjoint_self] at hab, exact ha hab }
+lemma disjoint.ne (ha : a ≠ ⊥) (hab : disjoint a b) : a ≠ b :=
+λ h, ha $ disjoint_self.1 $ by rwa ←h at hab
 
-lemma disjoint.eq_bot_of_le {a b : α} (hab : disjoint a b) (h : a ≤ b) : a = ⊥ :=
+lemma disjoint.eq_bot_of_le (hab : disjoint a b) (h : a ≤ b) : a = ⊥ :=
 eq_bot_iff.2 (by rwa ←inf_eq_left.2 h)
 
-lemma disjoint_assoc {a b c : α} : disjoint (a ⊓ b) c ↔ disjoint a (b ⊓ c) :=
-by rw [disjoint, disjoint, inf_assoc]
+lemma disjoint.eq_bot_of_ge (hab : disjoint a b) : b ≤ a → b = ⊥ := hab.symm.eq_bot_of_le
 
-lemma disjoint.of_disjoint_inf_of_le {a b c : α} (h : disjoint (a ⊓ b) c) (hle : a ≤ c) :
-  disjoint a b := by rw [disjoint_iff, h.eq_bot_of_le (inf_le_left.trans hle)]
+lemma disjoint.of_disjoint_inf_of_le (h : disjoint (a ⊓ b) c) (hle : a ≤ c) : disjoint a b :=
+disjoint_iff.2 $ h.eq_bot_of_le $ inf_le_of_left_le hle
 
-lemma disjoint.of_disjoint_inf_of_le' {a b c : α} (h : disjoint (a ⊓ b) c) (hle : b ≤ c) :
-  disjoint a b := by rw [disjoint_iff, h.eq_bot_of_le (inf_le_right.trans hle)]
+lemma disjoint.of_disjoint_inf_of_le' (h : disjoint (a ⊓ b) c) (hle : b ≤ c) : disjoint a b :=
+disjoint_iff.2 $ h.eq_bot_of_le $ inf_le_of_right_le hle
 
 end semilattice_inf_bot
 
-section order_bot
-
-variables [lattice α] [order_bot α]
-
-lemma eq_bot_of_disjoint_absorbs
-  {a b : α} (w : disjoint a b) (h : a ⊔ b = a) : b = ⊥ :=
-begin
-  rw disjoint_iff at w,
-  rw [←w, right_eq_inf],
-  rwa sup_eq_left at h,
-end
-
-end order_bot
-
-section bounded_order
-
+section lattice
 variables [lattice α] [bounded_order α] {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_order
-
-section linear_order
-
-variables [linear_order α]
-
-lemma min_top_left [order_top α] (a : α) : min (⊤ : α) a = a := min_eq_right le_top
-lemma min_top_right [order_top α] (a : α) : min a ⊤ = a := min_eq_left le_top
-lemma max_bot_left [order_bot α] (a : α) : max (⊥ : α) a = a := max_eq_right bot_le
-lemma max_bot_right [order_bot α] (a : α) : max a ⊥ = a := max_eq_left bot_le
-
--- `simp` can prove these, so they shouldn't be simp-lemmas.
-lemma min_bot_left [order_bot α] (a : α) : min ⊥ a = ⊥ := min_eq_left bot_le
-lemma min_bot_right [order_bot α] (a : α) : min a ⊥ = ⊥ := min_eq_right bot_le
-lemma max_top_left [order_top α] (a : α) : max ⊤ a = ⊤ := max_eq_left le_top
-lemma max_top_right [order_top α] (a : α) : max a ⊤ = ⊤ := max_eq_right le_top
-
-@[simp] lemma min_eq_bot [order_bot α] {a b : α} : min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥ :=
-by { symmetry, cases le_total a b; simpa [*, min_eq_left, min_eq_right] using eq_bot_mono h }
-
-@[simp] lemma max_eq_top [order_top α] {a b : α} : max a b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
-@min_eq_bot αᵒᵈ _ _ a b
-
-@[simp] lemma max_eq_bot [order_bot α] {a b : α} : max a b = ⊥ ↔ a = ⊥ ∧ b = ⊥ := sup_eq_bot_iff
-@[simp] lemma min_eq_top [order_top α] {a b : α} : min a b = ⊤ ↔ a = ⊤ ∧ b = ⊤ := inf_eq_top_iff
-
-end linear_order
+end lattice
 
 section distrib_lattice_bot
 variables [distrib_lattice α] [order_bot α] {a b c : α}
@@ -1250,46 +1237,15 @@ disjoint_sup_left.2 ⟨ha, hb⟩
 lemma disjoint.sup_right (hb : disjoint a b) (hc : disjoint a c) : disjoint a (b ⊔ c) :=
 disjoint_sup_right.2 ⟨hb, hc⟩
 
-lemma disjoint.left_le_of_le_sup_right {a b c : α} (h : a ≤ b ⊔ c) (hd : disjoint a c) : a ≤ b :=
-(λ x, le_of_inf_le_sup_le x (sup_le h le_sup_right)) ((disjoint_iff.mp hd).symm ▸ bot_le)
+lemma disjoint.left_le_of_le_sup_right (h : a ≤ b ⊔ c) (hd : disjoint a c) : a ≤ b :=
+le_of_inf_le_sup_le (le_trans hd bot_le) $ sup_le h le_sup_right
 
-lemma disjoint.left_le_of_le_sup_left {a b c : α} (h : a ≤ c ⊔ b) (hd : disjoint a c) : a ≤ b :=
-@le_of_inf_le_sup_le _ _ a b c ((disjoint_iff.mp hd).symm ▸ bot_le)
-  ((@sup_comm _ _ c b) ▸ (sup_le h le_sup_left))
+lemma disjoint.left_le_of_le_sup_left (h : a ≤ c ⊔ b) (hd : disjoint a c) : a ≤ b :=
+hd.left_le_of_le_sup_right $ by rwa sup_comm
 
 end distrib_lattice_bot
-
-section semilattice_inf_bot
-
-variables [semilattice_inf α] [order_bot α] {a b : α} (c : α)
-
-lemma disjoint.inf_left (h : disjoint a b) : disjoint (a ⊓ c) b :=
-h.mono_left inf_le_left
-
-lemma disjoint.inf_left' (h : disjoint a b) : disjoint (c ⊓ a) b :=
-h.mono_left inf_le_right
-
-lemma disjoint.inf_right (h : disjoint a b) : disjoint a (b ⊓ c) :=
-h.mono_right inf_le_left
-
-lemma disjoint.inf_right' (h : disjoint a b) : disjoint a (c ⊓ b) :=
-h.mono_right inf_le_right
-
-end semilattice_inf_bot
-
 end disjoint
 
-lemma inf_eq_bot_iff_le_compl [distrib_lattice α] [bounded_order α] {a b c : α}
-  (h₁ : b ⊔ c = ⊤) (h₂ : b ⊓ c = ⊥) : a ⊓ b = ⊥ ↔ a ≤ c :=
-⟨λ h,
-  calc a ≤ a ⊓ (b ⊔ c) : by simp [h₁]
-    ... = (a ⊓ b) ⊔ (a ⊓ c) : by simp [inf_sup_left]
-    ... ≤ c : by simp [h, inf_le_right],
-  λ h,
-  bot_unique $
-    calc a ⊓ b ≤ b ⊓ c : by { rw inf_comm, exact inf_le_inf_left _ h }
-      ... = ⊥ : h₂⟩
-
 section is_compl
 
 /-- Two elements `x` and `y` are complements of each other if `x ⊔ y = ⊤` and `x ⊓ y = ⊥`. -/
@@ -1308,16 +1264,14 @@ protected lemma disjoint (h : is_compl x y) : disjoint x y := h.1
 @[symm] protected lemma symm (h : is_compl x y) : is_compl y x :=
 ⟨by { rw inf_comm, exact h.1 }, by { rw sup_comm, exact h.2 }⟩
 
-lemma of_eq (h₁ : x ⊓ y = ⊥) (h₂ : x ⊔ y = ⊤) : is_compl x y :=
-⟨le_of_eq h₁, le_of_eq h₂.symm⟩
+lemma of_eq (h₁ : x ⊓ y = ⊥) (h₂ : x ⊔ y = ⊤) : is_compl x y := ⟨h₁.le, h₂.ge⟩
 
 lemma inf_eq_bot (h : is_compl x y) : x ⊓ y = ⊥ := h.disjoint.eq_bot
 
 lemma sup_eq_top (h : is_compl x y) : x ⊔ y = ⊤ := top_unique h.top_le_sup
 
-open order_dual (to_dual)
-
-lemma to_order_dual (h : is_compl x y) : is_compl (to_dual x) (to_dual y) := ⟨h.2, h.1⟩
+lemma dual (h : is_compl x y) : is_compl (to_dual x) (to_dual y) := ⟨h.2, h.1⟩
+lemma of_dual {a b : αᵒᵈ} (h : is_compl a b) : is_compl (of_dual a) (of_dual b) := ⟨h.2, h.1⟩
 
 end bounded_order
 
@@ -1330,7 +1284,7 @@ calc a ⊓ x ≤ (b ⊔ y) ⊓ x : inf_le_inf hle le_rfl
 ... ≤ b : inf_le_left
 
 lemma le_sup_right_iff_inf_left_le {a b} (h : is_compl x y) : a ≤ b ⊔ y ↔ a ⊓ x ≤ b :=
-⟨h.inf_left_le_of_le_sup_right, h.symm.to_order_dual.inf_left_le_of_le_sup_right⟩
+⟨h.inf_left_le_of_le_sup_right, h.symm.dual.inf_left_le_of_le_sup_right⟩
 
 lemma inf_left_eq_bot_iff (h : is_compl y z) : x ⊓ y = ⊥ ↔ x ≤ z :=
 by rw [← le_bot_iff, ← h.le_sup_right_iff_inf_left_le, bot_sup_eq]
@@ -1350,8 +1304,7 @@ h.disjoint_right_iff.symm
 lemma le_right_iff (h : is_compl x y) : z ≤ y ↔ disjoint z x :=
 h.symm.le_left_iff
 
-lemma left_le_iff (h : is_compl x y) : x ≤ z ↔ ⊤ ≤ z ⊔ y :=
-h.to_order_dual.le_left_iff
+lemma left_le_iff (h : is_compl x y) : x ≤ z ↔ ⊤ ≤ z ⊔ y := h.dual.le_left_iff
 
 lemma right_le_iff (h : is_compl x y) : y ≤ z ↔ ⊤ ≤ z ⊔ x :=
 h.symm.left_le_iff
@@ -1382,26 +1335,22 @@ lemma inf_sup {x' y'} (h : is_compl x y) (h' : is_compl x' y') :
 
 end is_compl
 
-lemma is_compl_bot_top [lattice α] [bounded_order α] : is_compl (⊥ : α) ⊤ :=
-is_compl.of_eq bot_inf_eq sup_top_eq
-
-lemma is_compl_top_bot [lattice α] [bounded_order α] : is_compl (⊤ : α) ⊥ :=
-is_compl.of_eq inf_bot_eq top_sup_eq
-
 section
-variables [lattice α] [bounded_order α] {x : α}
+variables [lattice α] [bounded_order α] {a b x : α}
 
-lemma eq_top_of_is_compl_bot (h : is_compl x ⊥) : x = ⊤ :=
-sup_bot_eq.symm.trans h.sup_eq_top
+@[simp] lemma is_compl_to_dual_iff : is_compl (to_dual a) (to_dual b) ↔ is_compl a b :=
+⟨is_compl.of_dual, is_compl.dual⟩
 
-lemma eq_top_of_bot_is_compl (h : is_compl ⊥ x) : x = ⊤ :=
-eq_top_of_is_compl_bot h.symm
+@[simp] lemma is_compl_of_dual_iff {a b : αᵒᵈ} : is_compl (of_dual a) (of_dual b) ↔ is_compl a b :=
+⟨is_compl.dual, is_compl.of_dual⟩
 
-lemma eq_bot_of_is_compl_top (h : is_compl x ⊤) : x = ⊥ :=
-eq_top_of_is_compl_bot h.to_order_dual
+lemma is_compl_bot_top : is_compl (⊥ : α) ⊤ := is_compl.of_eq bot_inf_eq sup_top_eq
+lemma is_compl_top_bot : is_compl (⊤ : α) ⊥ := is_compl.of_eq inf_bot_eq top_sup_eq
 
-lemma eq_bot_of_top_is_compl (h : is_compl ⊤ x) : x = ⊥ :=
-eq_top_of_bot_is_compl h.to_order_dual
+lemma eq_top_of_is_compl_bot (h : is_compl x ⊥) : x = ⊤ := sup_bot_eq.symm.trans h.sup_eq_top
+lemma eq_top_of_bot_is_compl (h : is_compl ⊥ x) : x = ⊤ := eq_top_of_is_compl_bot h.symm
+lemma eq_bot_of_is_compl_top (h : is_compl x ⊤) : x = ⊥ := eq_top_of_is_compl_bot h.dual
+lemma eq_bot_of_top_is_compl (h : is_compl ⊤ x) : x = ⊥ := eq_top_of_bot_is_compl h.dual
 
 end
 
@@ -1416,7 +1365,7 @@ namespace is_complemented
 variables [lattice α] [bounded_order α] [is_complemented α]
 
 instance : is_complemented αᵒᵈ :=
-⟨λ a, let ⟨b, hb⟩ := exists_is_compl (show α, from a) in ⟨b, hb.to_order_dual⟩⟩
+⟨λ a, let ⟨b, hb⟩ := exists_is_compl (show α, from a) in ⟨b, hb.dual⟩⟩
 
 end is_complemented
 
@@ -1434,22 +1383,16 @@ lemma bot_lt_top : (⊥ : α) < ⊤ := lt_top_iff_ne_top.2 bot_ne_top
 
 end nontrivial
 
-namespace bool
+section bool
+open bool
 
--- TODO: is this comment relevant now that `bounded_order` is factored out?
--- Could be generalised to `bounded_distrib_lattice` and `is_complemented`
 instance : bounded_order bool :=
 { top := tt,
   le_top := λ x, le_tt,
   bot := ff,
   bot_le := λ x, ff_le }
 
-end bool
-
-section bool
-
 @[simp] lemma top_eq_tt : ⊤ = tt := rfl
-
 @[simp] lemma bot_eq_ff : ⊥ = ff := rfl
 
 end bool

src/ring_theory/artinian.lean

@@ -275,8 +275,8 @@ begin
       exact nat.succ_le_succ_iff.mp p }, },
 
   obtain ⟨n, w⟩ := monotone_stabilizes_iff_artinian.mpr I (partial_sups (order_dual.to_dual ∘ f)),
-  exact ⟨n, (λ m p, eq_bot_of_disjoint_absorbs (h m)
-    ((eq.symm (w (m + 1) (le_add_right p))).trans (w m p)))⟩
+  exact ⟨n, λ m p, (h m).eq_bot_of_ge $ sup_eq_left.1 $ (w (m + 1) $ le_add_right p).symm.trans $
+    w m p⟩
 end
 
 universe w

src/ring_theory/noetherian.lean

@@ -637,8 +637,8 @@ begin
       exact nat.succ_le_succ_iff.mp p }, },
 
   obtain ⟨n, w⟩ := monotone_stabilizes_iff_noetherian.mpr I (partial_sups f),
-  exact ⟨n, (λ m p,
-    eq_bot_of_disjoint_absorbs (h m) ((eq.symm (w (m + 1) (le_add_right p))).trans (w m p)))⟩
+  exact ⟨n, λ m p, (h m).eq_bot_of_ge $ sup_eq_left.1 $ (w (m + 1) $ le_add_right p).symm.trans $
+    w m p⟩
 end
 
 /--