chore(Order/Basic): use @[to_dual] for Preorder/PartialOrder (#31852)

This PR tags some part of `Mathlib.Order.Basic` with `@[to_dual]`. This PR adds a lot of new declarations in cases where there used to not be a dual declaration (and even a new simp lemma `ne_iff_gt_iff_ge`).

The sections for pure `LE`/`LT`, and `LinearOrder` in this file are left to be tagged for future PRs.

Author: JovanGerb

Mathlib/Order/Basic.lean

@@ -53,7 +53,6 @@ provide many aliases to dot notation-less lemmas. For example, `le_trans` is ali
 ## TODO
 
 - expand module docs
-- automatic construction of dual definitions / theorems
 
 ## Tags
 
@@ -123,76 +122,71 @@ section Preorder
 
 variable [Preorder α] {a b c d : α}
 
+@[to_dual self (reorder := a b)]
 theorem not_lt_iff_not_le_or_ge : ¬a < b ↔ ¬a ≤ b ∨ b ≤ a := by
   rw [lt_iff_le_not_ge, Classical.not_and_iff_not_or_not, Classical.not_not]
 
 -- Unnecessary brackets are here for readability
+@[to_dual self (reorder := a b)]
 lemma not_lt_iff_le_imp_ge : ¬ a < b ↔ (a ≤ b → b ≤ a) := by
   simp [not_lt_iff_not_le_or_ge, or_iff_not_imp_left]
 
 @[deprecated (since := "2025-05-11")] alias not_lt_iff_le_imp_le := not_lt_iff_le_imp_ge
 
-@[simp] lemma lt_self_iff_false (x : α) : x < x ↔ False := ⟨lt_irrefl x, False.elim⟩
-
-alias le_trans' := ge_trans
-alias lt_trans' := gt_trans
-alias LE.le.trans := le_trans
-alias LE.le.trans' := le_trans'
-alias LT.lt.trans := lt_trans
-alias LT.lt.trans' := lt_trans'
-alias LE.le.trans_lt := lt_of_le_of_lt
-alias LE.le.trans_lt' := lt_of_le_of_lt'
-alias LT.lt.trans_le := lt_of_lt_of_le
-alias LT.lt.trans_le' := lt_of_lt_of_le'
-alias LE.le.lt_of_not_ge := lt_of_le_not_ge
-alias LT.lt.le := le_of_lt
-alias LT.lt.ne := ne_of_lt
-alias Eq.le := le_of_eq
-alias Eq.ge := ge_of_eq
-alias LT.lt.asymm := lt_asymm
-alias LT.lt.not_gt := lt_asymm
+@[simp, to_dual self]
+lemma lt_self_iff_false (x : α) : x < x ↔ False := ⟨lt_irrefl x, False.elim⟩
 
-@[deprecated (since := "2025-05-11")] alias LE.le.lt_of_not_le := LE.le.lt_of_not_ge
-@[deprecated (since := "2025-06-07")] alias LT.lt.not_lt := LT.lt.not_gt
+@[to_dual ge_trans'] alias le_trans' := ge_trans
+@[to_dual gt_trans'] alias lt_trans' := gt_trans
+@[to_dual trans'] alias LE.le.trans := le_trans
+@[to_dual trans'] alias LT.lt.trans := lt_trans
+@[to_dual trans_lt'] alias LE.le.trans_lt := lt_of_le_of_lt
+@[to_dual trans_le'] alias LT.lt.trans_le := lt_of_lt_of_le
 
-theorem ne_of_not_le (h : ¬a ≤ b) : a ≠ b := fun hab ↦ h (le_of_eq hab)
+@[to_dual self (reorder := a b)] alias LE.le.lt_of_not_ge := lt_of_le_not_ge
+@[to_dual self (reorder := a b)] alias LT.lt.le := le_of_lt
+@[to_dual self (reorder := a b)] alias LT.lt.asymm := lt_asymm
+@[to_dual self (reorder := a b)] alias LT.lt.not_gt := lt_asymm
 
-protected lemma Eq.not_lt (hab : a = b) : ¬a < b := fun h' ↦ h'.ne hab
-protected lemma Eq.not_gt (hab : a = b) : ¬b < a := hab.symm.not_lt
+@[to_dual ne'] alias LT.lt.ne := ne_of_lt
+@[to_dual ge] alias Eq.le := le_of_eq
 
-@[simp] lemma le_of_subsingleton [Subsingleton α] : a ≤ b := (Subsingleton.elim a b).le
+@[to_dual self] protected lemma LT.lt.false : a < a → False := lt_irrefl a
 
--- Making this a @[simp] lemma causes confluence problems downstream.
-@[nontriviality]
-lemma not_lt_of_subsingleton [Subsingleton α] : ¬a < b := (Subsingleton.elim a b).not_lt
+@[to_dual not_gt] protected lemma Eq.not_lt (hab : a = b) : ¬a < b := fun h' ↦ h'.ne hab
 
-namespace LT.lt
+@[deprecated (since := "2025-05-11")] alias LE.le.lt_of_not_le := LE.le.lt_of_not_ge
+@[deprecated (since := "2025-06-07")] alias LT.lt.not_lt := LT.lt.not_gt
 
-protected theorem false : a < a → False := lt_irrefl a
+@[to_dual ne_of_not_ge]
+theorem ne_of_not_le (h : ¬a ≤ b) : a ≠ b := fun hab ↦ h (le_of_eq hab)
 
-theorem ne' (h : a < b) : b ≠ a := h.ne.symm
+@[simp, to_dual self (reorder := a b)]
+lemma le_of_subsingleton [Subsingleton α] : a ≤ b := (Subsingleton.elim a b).le
 
-end LT.lt
+-- Making this a @[simp] lemma causes confluence problems downstream.
+@[nontriviality, to_dual self (reorder := a b)]
+lemma not_lt_of_subsingleton [Subsingleton α] : ¬a < b := (Subsingleton.elim a b).not_lt
 
+@[to_dual le_of_forall_ge]
 theorem le_of_forall_le (H : ∀ c, c ≤ a → c ≤ b) : a ≤ b := H _ le_rfl
-theorem le_of_forall_ge (H : ∀ c, a ≤ c → b ≤ c) : b ≤ a := H _ le_rfl
 
+@[to_dual forall_ge_iff_le]
 theorem forall_le_iff_le : (∀ ⦃c⦄, c ≤ a → c ≤ b) ↔ a ≤ b :=
   ⟨le_of_forall_le, fun h _ hca ↦ le_trans hca h⟩
 
-theorem forall_ge_iff_le : (∀ ⦃c⦄, a ≤ c → b ≤ c) ↔ b ≤ a :=
-  ⟨le_of_forall_ge, fun h _ hca ↦ le_trans h hca⟩
-
 @[deprecated (since := "2025-07-27")] alias forall_le_iff_ge := forall_ge_iff_le
 
 /-- monotonicity of `≤` with respect to `→` -/
-@[gcongr] theorem le_imp_le_of_le_of_le (h₁ : c ≤ a) (h₂ : b ≤ d) : a ≤ b → c ≤ d :=
+@[gcongr, to_dual self (reorder := a b, c d, h₁ h₂)]
+theorem le_imp_le_of_le_of_le (h₁ : c ≤ a) (h₂ : b ≤ d) : a ≤ b → c ≤ d :=
   fun hab ↦ (h₁.trans hab).trans h₂
 
 @[deprecated (since := "2025-07-31")] alias le_implies_le_of_le_of_le := le_imp_le_of_le_of_le
 
 /-- monotonicity of `<` with respect to `→` -/
-@[gcongr] theorem lt_imp_lt_of_le_of_le (h₁ : c ≤ a) (h₂ : b ≤ d) : a < b → c < d :=
+@[gcongr, to_dual self (reorder := a b, c d, h₁ h₂)]
+theorem lt_imp_lt_of_le_of_le (h₁ : c ≤ a) (h₂ : b ≤ d) : a < b → c < d :=
   fun hab ↦ (h₁.trans_lt hab).trans_le h₂
 
 namespace Mathlib.Tactic.GCongr
@@ -211,63 +205,45 @@ section PartialOrder
 
 variable [PartialOrder α] {a b : α}
 
+@[to_dual lt_of_le'] -- TODO: should be called `gt_of_ge`
 theorem Ne.lt_of_le : a ≠ b → a ≤ b → a < b :=
   flip lt_of_le_of_ne
 
-theorem Ne.lt_of_le' : b ≠ a → a ≤ b → a < b :=
-  flip lt_of_le_of_ne'
-
-alias LE.le.antisymm := le_antisymm
-alias LE.le.antisymm' := ge_antisymm
-alias LE.le.lt_of_ne := lt_of_le_of_ne
-alias LE.le.lt_of_ne' := lt_of_le_of_ne'
-
--- Unnecessary brackets are here for readability
-lemma le_imp_eq_iff_le_imp_ge' : (a ≤ b → b = a) ↔ (a ≤ b → b ≤ a) where
-  mp h hab := (h hab).le
-  mpr h hab := (h hab).antisymm hab
-
-@[deprecated (since := "2025-05-11")] alias le_imp_eq_iff_le_imp_le := le_imp_eq_iff_le_imp_ge'
-
--- Unnecessary brackets are here for readability
-lemma le_imp_eq_iff_le_imp_ge : (a ≤ b → a = b) ↔ (a ≤ b → b ≤ a) where
-  mp h hab := (h hab).ge
-  mpr h hab := hab.antisymm (h hab)
-
-@[deprecated (since := "2025-05-11")] alias ge_imp_eq_iff_le_imp_le := le_imp_eq_iff_le_imp_ge
-
 namespace LE.le
 
-theorem lt_iff_ne (h : a ≤ b) : a < b ↔ a ≠ b :=
-  ⟨fun h ↦ h.ne, h.lt_of_ne⟩
-
-theorem lt_iff_ne' (h : a ≤ b) : a < b ↔ b ≠ a :=
-  ⟨fun h ↦ h.ne.symm, h.lt_of_ne'⟩
+@[to_dual antisymm'] alias antisymm := le_antisymm
+@[to_dual lt_of_ne'] alias lt_of_ne := lt_of_le_of_ne
 
-theorem not_lt_iff_eq (h : a ≤ b) : ¬a < b ↔ a = b :=
-  h.lt_iff_ne.not_left
+@[to_dual lt_iff_ne']
+theorem lt_iff_ne (h : a ≤ b) : a < b ↔ a ≠ b := ⟨ne_of_lt, h.lt_of_ne⟩
 
-theorem not_lt_iff_eq' (h : a ≤ b) : ¬a < b ↔ b = a :=
-  h.lt_iff_ne'.not_left
+@[to_dual not_lt_iff_eq']
+theorem not_lt_iff_eq (h : a ≤ b) : ¬a < b ↔ a = b := h.lt_iff_ne.not_left
 
-theorem ge_iff_eq (h : a ≤ b) : b ≤ a ↔ a = b :=
-  ⟨h.antisymm, Eq.ge⟩
-
-theorem ge_iff_eq' (h : a ≤ b) : b ≤ a ↔ b = a :=
-  ⟨fun h' ↦ h'.antisymm h, Eq.le⟩
+@[to_dual ge_iff_eq']
+theorem ge_iff_eq (h : a ≤ b) : b ≤ a ↔ a = b := ⟨h.antisymm, Eq.ge⟩
 
 @[deprecated (since := "2025-06-08")] alias gt_iff_ne := lt_iff_ne'
 @[deprecated (since := "2025-06-08")] alias le_iff_eq := ge_iff_eq'
 @[deprecated (since := "2025-06-08")] alias not_gt_iff_eq := not_lt_iff_eq'
 
 end LE.le
 
+-- Unnecessary brackets are here for readability
+@[to_dual le_imp_eq_iff_le_imp_ge']
+lemma le_imp_eq_iff_le_imp_ge : (a ≤ b → a = b) ↔ (a ≤ b → b ≤ a) where
+  mp h hab := (h hab).ge
+  mpr h hab := hab.antisymm (h hab)
+
 -- See Note [decidable namespace]
+@[to_dual le_iff_eq_or_lt']
 protected theorem Decidable.le_iff_eq_or_lt [DecidableLE α] : a ≤ b ↔ a = b ∨ a < b :=
   Decidable.le_iff_lt_or_eq.trans or_comm
 
+@[to_dual le_iff_eq_or_lt']
 theorem le_iff_eq_or_lt : a ≤ b ↔ a = b ∨ a < b := le_iff_lt_or_eq.trans or_comm
 
+@[to_dual lt_iff_le_and_ne']
 theorem lt_iff_le_and_ne : a < b ↔ a ≤ b ∧ a ≠ b :=
   ⟨fun h ↦ ⟨le_of_lt h, ne_of_lt h⟩, fun ⟨h1, h2⟩ ↦ h1.lt_of_ne h2⟩
 
@@ -277,62 +253,62 @@ lemma eq_iff_not_lt_of_le (hab : a ≤ b) : a = b ↔ ¬ a < b := hab.not_lt_iff
 @[deprecated (since := "2025-06-08")] alias LE.le.eq_iff_not_lt := eq_iff_not_lt_of_le
 
 -- See Note [decidable namespace]
+@[to_dual eq_iff_ge_not_gt]
 protected theorem Decidable.eq_iff_le_not_lt [DecidableLE α] : a = b ↔ a ≤ b ∧ ¬a < b :=
   ⟨fun h ↦ ⟨h.le, h ▸ lt_irrefl _⟩, fun ⟨h₁, h₂⟩ ↦
     h₁.antisymm <| Decidable.byContradiction fun h₃ ↦ h₂ (h₁.lt_of_not_ge h₃)⟩
 
+@[to_dual eq_iff_ge_not_gt]
 theorem eq_iff_le_not_lt : a = b ↔ a ≤ b ∧ ¬a < b := open scoped Classical in
   Decidable.eq_iff_le_not_lt
 
 -- See Note [decidable namespace]
+@[to_dual eq_or_lt_of_le']
 protected theorem Decidable.eq_or_lt_of_le [DecidableLE α] (h : a ≤ b) : a = b ∨ a < b :=
   (Decidable.lt_or_eq_of_le h).symm
 
+@[to_dual eq_or_lt_of_le']
 theorem eq_or_lt_of_le (h : a ≤ b) : a = b ∨ a < b := (lt_or_eq_of_le h).symm
-theorem eq_or_lt_of_le' (h : a ≤ b) : b = a ∨ a < b := (eq_or_lt_of_le h).imp Eq.symm id
 
-alias LE.le.lt_or_eq_dec := Decidable.lt_or_eq_of_le
-alias LE.le.eq_or_lt_dec := Decidable.eq_or_lt_of_le
-alias LE.le.lt_or_eq := lt_or_eq_of_le
-alias LE.le.eq_or_lt := eq_or_lt_of_le
-alias LE.le.eq_or_lt' := eq_or_lt_of_le'
-alias LE.le.lt_or_eq' := lt_or_eq_of_le'
+@[to_dual lt_or_eq_dec'] alias LE.le.lt_or_eq_dec := Decidable.lt_or_eq_of_le
+@[to_dual eq_or_lt_dec'] alias LE.le.eq_or_lt_dec := Decidable.eq_or_lt_of_le
+@[to_dual lt_or_eq'] alias LE.le.lt_or_eq := lt_or_eq_of_le
+@[to_dual eq_or_lt'] alias LE.le.eq_or_lt := eq_or_lt_of_le
 
 @[deprecated (since := "2025-06-08")] alias eq_or_gt_of_le := eq_or_lt_of_le'
 @[deprecated (since := "2025-06-08")] alias gt_or_eq_of_le := lt_or_eq_of_le'
 @[deprecated (since := "2025-06-08")] alias LE.le.eq_or_gt := LE.le.eq_or_lt'
 @[deprecated (since := "2025-06-08")] alias LE.le.gt_or_eq := LE.le.lt_or_eq'
 
+@[to_dual eq_of_le_of_not_lt']
 theorem eq_of_le_of_not_lt (h₁ : a ≤ b) (h₂ : ¬a < b) : a = b := h₁.eq_or_lt.resolve_right h₂
-theorem eq_of_le_of_not_lt' (h₁ : a ≤ b) (h₂ : ¬a < b) : b = a := (eq_of_le_of_not_lt h₁ h₂).symm
 
-alias LE.le.eq_of_not_lt := eq_of_le_of_not_lt
-alias LE.le.eq_of_not_lt' := eq_of_le_of_not_lt'
+@[to_dual eq_of_not_lt'] alias LE.le.eq_of_not_lt := eq_of_le_of_not_lt
 
 @[deprecated (since := "2025-06-08")] alias eq_of_ge_of_not_gt := eq_of_le_of_not_lt'
 @[deprecated (since := "2025-06-08")] alias LE.le.eq_of_not_gt := LE.le.eq_of_not_lt'
 
+@[to_dual ge_iff_gt]
 theorem Ne.le_iff_lt (h : a ≠ b) : a ≤ b ↔ a < b := ⟨fun h' ↦ lt_of_le_of_ne h' h, fun h ↦ h.le⟩
 
+@[to_dual not_ge_or_not_le]
 theorem Ne.not_le_or_not_ge (h : a ≠ b) : ¬a ≤ b ∨ ¬b ≤ a := not_and_or.1 <| le_antisymm_iff.not.1 h
 
 @[deprecated (since := "2025-06-07")] alias Ne.not_le_or_not_le := Ne.not_le_or_not_ge
 
 -- See Note [decidable namespace]
+@[to_dual ne_iff_gt_iff_ge]
 protected theorem Decidable.ne_iff_lt_iff_le [DecidableEq α] : (a ≠ b ↔ a < b) ↔ a ≤ b :=
   ⟨fun h ↦ Decidable.byCases le_of_eq (le_of_lt ∘ h.mp), fun h ↦ ⟨lt_of_le_of_ne h, ne_of_lt⟩⟩
 
-@[simp]
-theorem ne_iff_lt_iff_le : (a ≠ b ↔ a < b) ↔ a ≤ b :=
-  haveI := Classical.dec
+@[to_dual (attr := simp) ne_iff_gt_iff_ge]
+theorem ne_iff_lt_iff_le : (a ≠ b ↔ a < b) ↔ a ≤ b := open scoped Classical in
   Decidable.ne_iff_lt_iff_le
 
+@[to_dual eq_of_forall_ge_iff]
 lemma eq_of_forall_le_iff (H : ∀ c, c ≤ a ↔ c ≤ b) : a = b :=
   ((H _).1 le_rfl).antisymm ((H _).2 le_rfl)
 
-lemma eq_of_forall_ge_iff (H : ∀ c, a ≤ c ↔ b ≤ c) : a = b :=
-  ((H _).2 le_rfl).antisymm ((H _).1 le_rfl)
-
 /-- To prove commutativity of a binary operation `○`, we only to check `a ○ b ≤ b ○ a` for all `a`,
 `b`. -/
 lemma commutative_of_le {f : β → β → α} (comm : ∀ a b, f a b ≤ f b a) : ∀ a b, f a b = f b a :=