refactor(order/ideal): Generalize definition and lemmas (#11421)

* Generalize the `order_top` instance to `[nonempty P] [is_directed P (≤)]`.
* Delete `order.ideal.ideal_inter_nonempty` in favor of the equivalent condition `is_directed P (swap (≤))`.
* Delete `order.ideal.sup`/`order.ideal.inf` in favor of a direct instance declaration.
* Generalize defs/lemmas from `preorder` to `has_le` or `partial_order` to `preorder`.
* Two more `is_directed` lemmas and instances for `order_bot` and `order_top`.

src/order/atoms.lean

@@ -54,11 +54,11 @@ section atoms
 
 section is_atom
 
-variables [partial_order α] [order_bot α] {a b x : α}
-
 /-- 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 = ⊥)
+def is_atom [preorder α] [order_bot α] (a : α) : Prop := a ≠ ⊥ ∧ (∀ b, b < a → b = ⊥)
+
+variables [partial_order α] [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)
@@ -79,11 +79,11 @@ end is_atom
 
 section is_coatom
 
-variables [partial_order α] [order_top α] {a b x : α}
-
 /-- A coatom of an `order_top` is an element with no other element between it and `⊤`,
   which is not `⊤`. -/
-def is_coatom (a : α) : Prop := a ≠ ⊤ ∧ (∀ b, a < b → b = ⊤)
+def is_coatom [preorder α] [order_top α] (a : α) : Prop := a ≠ ⊤ ∧ (∀ b, a < b → b = ⊤)
+
+variables [partial_order α] [order_top α] {a b x : α}
 
 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

src/order/directed.lean

@@ -3,7 +3,6 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import order.lattice
 import data.set.basic
 
 /-!
@@ -100,7 +99,13 @@ lemma directed_of (r : α → α → Prop) [is_directed α r] (a b : α) : ∃ c
 is_directed.directed _ _
 
 lemma directed_id [is_directed α r] : directed r id := by convert directed_of r
-lemma directed_id_iff_is_directed : directed r id ↔ is_directed α r := ⟨λ h, ⟨h⟩, @directed_id _ _⟩
+lemma directed_id_iff : directed r id ↔ is_directed α r := ⟨λ h, ⟨h⟩, @directed_id _ _⟩
+
+lemma directed_on_univ [is_directed α r] : directed_on r set.univ :=
+λ a _ b _, let ⟨c, hc⟩ := directed_of r a b in ⟨c, trivial, hc⟩
+
+lemma directed_on_univ_iff : directed_on r set.univ ↔ is_directed α r :=
+⟨λ h, ⟨λ a b, let ⟨c, _, hc⟩ := h a trivial b trivial in ⟨c, hc⟩⟩, @directed_on_univ _ _⟩
 
 @[priority 100]  -- see Note [lower instance priority]
 instance is_total.to_is_directed [is_total α r] : is_directed α r :=
@@ -130,3 +135,11 @@ instance semilattice_sup.to_is_directed_le [semilattice_sup α] : is_directed α
 @[priority 100]  -- see Note [lower instance priority]
 instance semilattice_inf.to_is_directed_ge [semilattice_inf α] : is_directed α (swap (≤)) :=
 ⟨λ a b, ⟨a ⊓ b, inf_le_left, inf_le_right⟩⟩
+
+@[priority 100]  -- see Note [lower instance priority]
+instance order_top.to_is_directed_le [has_le α] [order_top α] : is_directed α (≤) :=
+⟨λ a b, ⟨⊤, le_top, le_top⟩⟩
+
+@[priority 100]  -- see Note [lower instance priority]
+instance order_bot.to_is_directed_ge [has_le α] [order_bot α] : is_directed α (swap (≤)) :=
+⟨λ a b, ⟨⊥, bot_le, bot_le⟩⟩