refactor(order/directed): use (≥) instead of swap (≤) (#14474)

Author: urkud

src/analysis/convex/quasiconvex.lean

@@ -78,7 +78,7 @@ lemma quasiconvex_on.convex [is_directed β (≤)] (hf : quasiconvex_on 𝕜 s f
 λ x y hx hy a b ha hb hab,
   let ⟨z, hxz, hyz⟩ := exists_ge_ge (f x) (f y) in (hf _ ⟨hx, hxz⟩ ⟨hy, hyz⟩ ha hb hab).1
 
-lemma quasiconcave_on.convex [is_directed β (swap (≤))] (hf : quasiconcave_on 𝕜 s f) : convex 𝕜 s :=
+lemma quasiconcave_on.convex [is_directed β (≥)] (hf : quasiconcave_on 𝕜 s f) : convex 𝕜 s :=
 hf.dual.convex
 
 end ordered_add_comm_monoid

src/category_theory/filtered.lean

@@ -481,14 +481,14 @@ instance is_cofiltered_of_semilattice_inf_nonempty
 
 @[priority 100]
 instance is_cofiltered_or_empty_of_directed_ge (α : Type u) [preorder α]
-  [is_directed α (swap (≤))] :
+  [is_directed α (≥)] :
   is_cofiltered_or_empty α :=
 { cocone_objs := λ X Y, let ⟨Z, hX, hY⟩ := exists_le_le X Y in
     ⟨Z, hom_of_le hX, hom_of_le hY, trivial⟩,
   cocone_maps := λ X Y f g, ⟨X, 𝟙 _, by simp⟩ }
 
 @[priority 100]
-instance is_cofiltered_of_directed_ge_nonempty  (α : Type u) [preorder α] [is_directed α (swap (≤))]
+instance is_cofiltered_of_directed_ge_nonempty  (α : Type u) [preorder α] [is_directed α (≥)]
   [nonempty α] :
   is_cofiltered α := {}
 

src/order/directed.lean

@@ -119,38 +119,38 @@ lemma is_directed_mono [is_directed α r] (h : ∀ ⦃a b⦄, r a b → s a b) :
 lemma exists_ge_ge [has_le α] [is_directed α (≤)] (a b : α) : ∃ c, a ≤ c ∧ b ≤ c :=
 directed_of (≤) a b
 
-lemma exists_le_le [has_le α] [is_directed α (swap (≤))] (a b : α) : ∃ c, c ≤ a ∧ c ≤ b :=
-directed_of (swap (≤)) a b
+lemma exists_le_le [has_le α] [is_directed α (≥)] (a b : α) : ∃ c, c ≤ a ∧ c ≤ b :=
+directed_of (≥) a b
 
-instance order_dual.is_directed_ge [has_le α] [is_directed α (≤)] : is_directed αᵒᵈ (swap (≤)) :=
+instance order_dual.is_directed_ge [has_le α] [is_directed α (≤)] : is_directed αᵒᵈ (≥) :=
 by assumption
 
-instance order_dual.is_directed_le [has_le α] [is_directed α (swap (≤))] : is_directed αᵒᵈ (≤) :=
+instance order_dual.is_directed_le [has_le α] [is_directed α (≥)] : is_directed αᵒᵈ (≤) :=
 by assumption
 
 section preorder
 variables [preorder α] {a : α}
 
-protected lemma is_min.is_bot [is_directed α (swap (≤))] (h : is_min a) : is_bot a :=
+protected lemma is_min.is_bot [is_directed α (≥)] (h : is_min a) : is_bot a :=
 λ b, let ⟨c, hca, hcb⟩ := exists_le_le a b in (h hca).trans hcb
 
 protected lemma is_max.is_top [is_directed α (≤)] (h : is_max a) : is_top a :=
-λ b, let ⟨c, hac, hbc⟩ := exists_ge_ge a b in hbc.trans $ h hac
+h.to_dual.is_bot
 
 lemma is_top_or_exists_gt [is_directed α (≤)] (a : α) : is_top a ∨ (∃ b, a < b) :=
 (em (is_max a)).imp is_max.is_top not_is_max_iff.mp
 
-lemma is_bot_or_exists_lt [is_directed α (swap (≤))] (a : α) : is_bot a ∨ (∃ b, b < a) :=
+lemma is_bot_or_exists_lt [is_directed α (≥)] (a : α) : is_bot a ∨ (∃ b, b < a) :=
 @is_top_or_exists_gt αᵒᵈ _ _ a
 
-lemma is_bot_iff_is_min [is_directed α (swap (≤))] : is_bot a ↔ is_min a :=
+lemma is_bot_iff_is_min [is_directed α (≥)] : is_bot a ↔ is_min a :=
 ⟨is_bot.is_min, is_min.is_bot⟩
 
 lemma is_top_iff_is_max [is_directed α (≤)] : is_top a ↔ is_max a := ⟨is_top.is_max, is_max.is_top⟩
 
 variables (β) [partial_order β]
 
-theorem exists_lt_of_directed_ge [is_directed β (swap (≤))] [nontrivial β] : ∃ a b : β, a < b :=
+theorem exists_lt_of_directed_ge [is_directed β (≥)] [nontrivial β] : ∃ a b : β, a < b :=
 begin
   rcases exists_pair_ne β with ⟨a, b, hne⟩,
   rcases is_bot_or_exists_lt a with ha|⟨c, hc⟩,
@@ -167,13 +167,13 @@ instance semilattice_sup.to_is_directed_le [semilattice_sup α] : is_directed α
 ⟨λ a b, ⟨a ⊔ b, le_sup_left, le_sup_right⟩⟩
 
 @[priority 100]  -- see Note [lower instance priority]
-instance semilattice_inf.to_is_directed_ge [semilattice_inf α] : is_directed α (swap (≤)) :=
+instance semilattice_inf.to_is_directed_ge [semilattice_inf α] : is_directed α (≥) :=
 ⟨λ 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 (≤)) :=
+instance order_bot.to_is_directed_ge [has_le α] [order_bot α] : is_directed α (≥) :=
 ⟨λ a b, ⟨⊥, bot_le, bot_le⟩⟩

src/order/ideal.lean

@@ -124,11 +124,11 @@ and nonempty. -/
 @[mk_iff] class is_maximal (I : ideal P) extends is_proper I : Prop :=
 (maximal_proper : ∀ ⦃J : ideal P⦄, I < J → (J : set P) = univ)
 
-lemma inter_nonempty [is_directed P (swap (≤))] (I J : ideal P) : (I ∩ J : set P).nonempty :=
+lemma inter_nonempty [is_directed P (≥)] (I J : ideal P) : (I ∩ J : set P).nonempty :=
 begin
   obtain ⟨a, ha⟩ := I.nonempty,
   obtain ⟨b, hb⟩ := J.nonempty,
-  obtain ⟨c, hac, hbc⟩ := directed_of (swap (≤)) a b,
+  obtain ⟨c, hac, hbc⟩ := exists_le_le a b,
   exact ⟨c, I.lower hac ha, J.lower hbc hb⟩,
 end
 
@@ -237,7 +237,7 @@ let ⟨z, hz, hx, hy⟩ := s.directed x hx y hy in s.lower (sup_le hx hy) hz
 end semilattice_sup
 
 section semilattice_sup_directed
-variables [semilattice_sup P] [is_directed P (swap (≤))] {x : P} {I J K s t : ideal P}
+variables [semilattice_sup P] [is_directed P (≥)] {x : P} {I J K s t : ideal P}
 
 /-- The infimum of two ideals of a co-directed order is their intersection. -/
 instance : has_inf (ideal P) :=