feat(order/atoms): add lemmas (#14162)

src/algebra/associated.lean

@@ -904,7 +904,7 @@ end
 lemma associates.is_atom_iff [cancel_comm_monoid_with_zero α] {p : associates α} (h₁ : p ≠ 0) :
   is_atom p ↔ irreducible p :=
 ⟨λ hp, ⟨by simpa only [associates.is_unit_iff_eq_one] using hp.1,
-        λ a b h, (eq_bot_or_eq_of_le_atom hp ⟨_, h⟩).cases_on
+        λ a b h, (hp.le_iff.mp ⟨_, h⟩).cases_on
           (λ ha, or.inl (a.is_unit_iff_eq_one.mpr ha))
           (λ ha, or.inr (show is_unit b, by {rw ha at h, apply is_unit_of_associated_mul
           (show associated (p * b) p, by conv_rhs {rw h}) h₁ }))⟩,

src/order/atoms.lean

@@ -56,50 +56,78 @@ section atoms
 
 section is_atom
 
-/-- An atom of an `order_bot` is an element with no other element between it and `⊥`,
-  which is not `⊥`. -/
-def is_atom [preorder α] [order_bot α] (a : α) : Prop := a ≠ ⊥ ∧ (∀ b, b < a → b = ⊥)
+section preorder
 
-variables [partial_order α] [order_bot α] {a b x : α}
+variables [preorder α] [order_bot α] {a b x : α}
 
-lemma eq_bot_or_eq_of_le_atom (ha : is_atom a) (hab : b ≤ a) : b = ⊥ ∨ b = a :=
-hab.lt_or_eq.imp_left (ha.2 b)
+/-- An atom of an `order_bot` is an element with no other element between it and `⊥`,
+  which is not `⊥`. -/
+def is_atom (a : α) : Prop := a ≠ ⊥ ∧ (∀ b, b < a → b = ⊥)
 
 lemma is_atom.Iic (ha : is_atom a) (hax : a ≤ x) : is_atom (⟨a, hax⟩ : set.Iic x) :=
 ⟨λ con, ha.1 (subtype.mk_eq_mk.1 con), λ ⟨b, hb⟩ hba, subtype.mk_eq_mk.2 (ha.2 b hba)⟩
 
 lemma is_atom.of_is_atom_coe_Iic {a : set.Iic x} (ha : is_atom a) : is_atom (a : α) :=
 ⟨λ con, ha.1 (subtype.ext con), λ b hba, subtype.mk_eq_mk.1 (ha.2 ⟨b, hba.le.trans a.prop⟩ hba)⟩
 
+end preorder
+
+variables [partial_order α] [order_bot α] {a b x : α}
+
+lemma is_atom.lt_iff (h : is_atom a) : x < a ↔ x = ⊥ := ⟨h.2 x, λ hx, hx.symm ▸ h.1.bot_lt⟩
+
+lemma is_atom.le_iff (h : is_atom a) : x ≤ a ↔ x = ⊥ ∨ x = a :=
+by rw [le_iff_lt_or_eq, h.lt_iff]
+
+lemma is_atom.Iic_eq (h : is_atom a) : set.Iic a = {⊥, a} := set.ext $ λ x, h.le_iff
+
 @[simp] lemma bot_covby_iff : ⊥ ⋖ a ↔ is_atom a :=
-⟨λ h, ⟨h.lt.ne', λ b hba, not_not.1 $ λ hb, h.2 (ne.bot_lt hb) hba⟩,
-  λ h, ⟨h.1.bot_lt, λ b hb hba, hb.ne' $ h.2 _ hba⟩⟩
+by simp only [covby, bot_lt_iff_ne_bot, is_atom, not_imp_not]
 
 alias bot_covby_iff ↔ covby.is_atom is_atom.bot_covby
 
 end is_atom
 
 section is_coatom
 
+section preorder
+
+variables [preorder α]
+
 /-- A coatom of an `order_top` is an element with no other element between it and `⊤`,
   which is not `⊤`. -/
-def is_coatom [preorder α] [order_top α] (a : α) : Prop := a ≠ ⊤ ∧ (∀ b, a < b → b = ⊤)
+def is_coatom [order_top α] (a : α) : Prop := a ≠ ⊤ ∧ (∀ b, a < b → b = ⊤)
 
-variables [partial_order α] [order_top α] {a b x : α}
+@[simp] lemma is_coatom_dual_iff_is_atom [order_bot α] {a : α}:
+  is_coatom (order_dual.to_dual a) ↔ is_atom a :=
+iff.rfl
 
-lemma eq_top_or_eq_of_coatom_le (ha : is_coatom a) (hab : a ≤ b) : b = ⊤ ∨ b = a :=
-hab.lt_or_eq.imp (ha.2 b) eq_comm.2
+@[simp] lemma is_atom_dual_iff_is_coatom [order_top α] {a : α} :
+  is_atom (order_dual.to_dual a) ↔ is_coatom a :=
+iff.rfl
+
+alias is_coatom_dual_iff_is_atom ↔ _ is_atom.dual
+alias is_atom_dual_iff_is_coatom ↔ _ is_coatom.dual
+
+variables [order_top α] {a x : α}
 
 lemma is_coatom.Ici (ha : is_coatom a) (hax : x ≤ a) : is_coatom (⟨a, hax⟩ : set.Ici x) :=
-⟨λ con, ha.1 (subtype.mk_eq_mk.1 con), λ ⟨b, hb⟩ hba, subtype.mk_eq_mk.2 (ha.2 b hba)⟩
+ha.dual.Iic hax
 
 lemma is_coatom.of_is_coatom_coe_Ici {a : set.Ici x} (ha : is_coatom a) :
   is_coatom (a : α) :=
-⟨λ con, ha.1 (subtype.ext con), λ b hba, subtype.mk_eq_mk.1 (ha.2 ⟨b, le_trans a.prop hba.le⟩ hba)⟩
+@is_atom.of_is_atom_coe_Iic αᵒᵈ _ _ x a ha
+
+end preorder
+
+variables [partial_order α] [order_top α] {a b x : α}
+
+lemma is_coatom.lt_iff (h : is_coatom a) : a < x ↔ x = ⊤ := h.dual.lt_iff
+lemma is_coatom.le_iff (h : is_coatom a) : a ≤ x ↔ x = ⊤ ∨ x = a := h.dual.le_iff
+lemma is_coatom.Ici_eq (h : is_coatom a) : set.Ici a = {⊤, a} := h.dual.Iic_eq
 
 @[simp] lemma covby_top_iff : a ⋖ ⊤ ↔ is_coatom a :=
-⟨λ h, ⟨h.ne, λ b hab, not_not.1 $ λ hb, h.2 hab $ ne.lt_top hb⟩,
-  λ h, ⟨h.1.lt_top, λ b hab hb, hb.ne $ h.2 _ hab⟩⟩
+to_dual_covby_to_dual_iff.symm.trans bot_covby_iff
 
 alias covby_top_iff ↔ covby.is_coatom is_coatom.covby_top
 
@@ -109,34 +137,18 @@ section pairwise
 
 lemma is_atom.inf_eq_bot_of_ne [semilattice_inf α] [order_bot α] {a b : α}
   (ha : is_atom a) (hb : is_atom b) (hab : a ≠ b) : a ⊓ b = ⊥ :=
-or.elim (eq_bot_or_eq_of_le_atom ha inf_le_left) id
-  (λ h1, or.elim (eq_bot_or_eq_of_le_atom hb inf_le_right) id
-  (λ h2, false.rec _ (hab (le_antisymm (inf_eq_left.mp h1) (inf_eq_right.mp h2)))))
+hab.not_le_or_not_le.elim (ha.lt_iff.1 ∘ inf_lt_left.2) (hb.lt_iff.1 ∘ inf_lt_right.2)
 
 lemma is_atom.disjoint_of_ne [semilattice_inf α] [order_bot α] {a b : α}
   (ha : is_atom a) (hb : is_atom b) (hab : a ≠ b) : disjoint a b :=
 disjoint_iff.mpr (is_atom.inf_eq_bot_of_ne ha hb hab)
 
 lemma is_coatom.sup_eq_top_of_ne [semilattice_sup α] [order_top α] {a b : α}
   (ha : is_coatom a) (hb : is_coatom b) (hab : a ≠ b) : a ⊔ b = ⊤ :=
-or.elim (eq_top_or_eq_of_coatom_le ha le_sup_left) id
-  (λ h1, or.elim (eq_top_or_eq_of_coatom_le hb le_sup_right) id
-  (λ h2, false.rec _ (hab (le_antisymm (sup_eq_right.mp h2) (sup_eq_left.mp h1)))))
+ha.dual.inf_eq_bot_of_ne hb.dual hab
 
 end pairwise
 
-variables [preorder α] {a : α}
-
-@[simp]
-lemma is_coatom_dual_iff_is_atom [order_bot α] :
-  is_coatom (order_dual.to_dual a) ↔ is_atom a :=
-iff.rfl
-
-@[simp]
-lemma is_atom_dual_iff_is_coatom [order_top α] :
-  is_atom (order_dual.to_dual a) ↔ is_coatom a :=
-iff.rfl
-
 end atoms
 
 section atomic

src/order/compactly_generated.lean

@@ -415,7 +415,7 @@ theorem is_complemented_of_Sup_atoms_eq_top (h : Sup {a : α | is_atom a} = ⊤)
     rw [← h, Sup_le_iff],
     intros a ha,
     rw ← inf_eq_left,
-    refine (eq_bot_or_eq_of_le_atom ha inf_le_left).resolve_left (λ con, ha.1 _),
+    refine (ha.le_iff.mp inf_le_left).resolve_left (λ con, ha.1 _),
     rw [eq_bot_iff, ← con],
     refine le_inf (le_refl a) ((le_Sup _).trans le_sup_right),
     rw ← disjoint_iff at *,

src/order/partition/finpartition.lean

@@ -153,7 +153,7 @@ def _root_.is_atom.unique_finpartition (ha : is_atom a) : unique (finpartition a
 { default := indiscrete ha.1,
   uniq := λ P, begin
     have h : ∀ b ∈ P.parts, b = a,
-    { exact λ b hb, (eq_bot_or_eq_of_le_atom ha $ P.le hb).resolve_left (P.ne_bot hb) },
+    { exact λ b hb, (ha.le_iff.mp $ P.le hb).resolve_left (P.ne_bot hb) },
     ext b,
     refine iff.trans ⟨h b, _⟩ mem_singleton.symm,
     rintro rfl,