chore(Order/Defs/LinearOrder): use @[to_dual] (#31709)

This PR tags the content of `Mathlib.Order.Defs.LinearOrder` with `@[to_dual]`. For this to work, we also tag some lemmas used by `grind` with the `@[to_dual]` tag.

Author: JovanGerb

Mathlib/Order/Basic.lean

@@ -372,15 +372,6 @@ lemma gt_or_lt (h : a < b) (c : α) : a < c ∨ c < b := (le_or_gt b c).imp h.tr
 
 end LT.lt
 
--- Variant of `min_def` with the branches reversed.
-theorem min_def' (a b : α) : min a b = if b ≤ a then b else a := by
-  grind
-
--- Variant of `min_def` with the branches reversed.
--- This is sometimes useful as it used to be the default.
-theorem max_def' (a b : α) : max a b = if b ≤ a then a else b := by
-  grind
-
 @[deprecated (since := "2025-05-11")] alias lt_of_not_le := lt_of_not_ge
 @[deprecated (since := "2025-05-11")] alias lt_iff_not_le := lt_iff_not_ge
 

Mathlib/Order/Defs/LinearOrder.lean

@@ -75,12 +75,20 @@ class LinearOrder (α : Type*) extends PartialOrder α, Min α, Max α, Ord α w
   compare_eq_compareOfLessAndEq : ∀ a b, compare a b = compareOfLessAndEq a b := by
     compareOfLessAndEq_rfl
 
+attribute [to_dual existing] LinearOrder.toMax
+
 variable [LinearOrder α] {a b c : α}
 
 attribute [instance 900] LinearOrder.toDecidableLT
 attribute [instance 900] LinearOrder.toDecidableLE
 attribute [instance 900] LinearOrder.toDecidableEq
 
+@[to_dual existing toDecidableLT, inherit_doc toDecidableLT]
+def LinearOrder.toDecidableLT' : DecidableLT' α := fun a b => toDecidableLT b a
+
+@[to_dual existing toDecidableLE, inherit_doc toDecidableLE]
+def LinearOrder.toDecidableLE' : DecidableLE' α := fun a b => toDecidableLE b a
+
 instance : Std.IsLinearOrder α where
   le_total := LinearOrder.le_total
 
@@ -91,6 +99,7 @@ lemma lt_of_not_ge (h : ¬b ≤ a) : a < b := lt_of_le_not_ge (le_of_not_ge h) h
 
 @[deprecated (since := "2025-05-11")] alias le_of_not_le := le_of_not_ge
 
+@[to_dual gt_trichotomy]
 lemma lt_trichotomy (a b : α) : a < b ∨ a = b ∨ b < a := by grind
 
 lemma le_of_not_gt (h : ¬b < a) : a ≤ b :=
@@ -110,21 +119,27 @@ lemma le_or_gt (a b : α) : a ≤ b ∨ b < a := (lt_or_ge b a).symm
 
 @[deprecated (since := "2025-05-11")] alias le_or_lt := le_or_gt
 
+@[to_dual gt_or_lt_of_ne]
 lemma lt_or_gt_of_ne (h : a ≠ b) : a < b ∨ b < a := by grind
 
+@[to_dual ne_iff_gt_or_lt]
 lemma ne_iff_lt_or_gt : a ≠ b ↔ a < b ∨ b < a := ⟨lt_or_gt_of_ne, (Or.elim · ne_of_lt ne_of_gt)⟩
 
 lemma lt_iff_not_ge : a < b ↔ ¬b ≤ a := ⟨not_le_of_gt, lt_of_not_ge⟩
 
 @[simp, push] lemma not_lt : ¬a < b ↔ b ≤ a := ⟨le_of_not_gt, not_lt_of_ge⟩
 @[simp, push] lemma not_le : ¬a ≤ b ↔ b < a := lt_iff_not_ge.symm
 
+attribute [to_dual self (reorder := a b)]
+  le_total le_of_not_ge lt_of_not_ge le_of_not_gt lt_or_ge le_or_gt lt_iff_not_ge not_lt not_le
+
+@[to_dual eq_or_lt_of_not_gt]
 lemma eq_or_gt_of_not_lt (h : ¬a < b) : a = b ∨ b < a :=
   if h₁ : a = b then Or.inl h₁ else Or.inr (lt_of_not_ge fun hge => h (lt_of_le_of_ne hge h₁))
 
-@[deprecated (since := "2025-07-27")] alias eq_or_lt_of_not_gt := eq_or_gt_of_not_lt
 @[deprecated (since := "2025-05-11")] alias eq_or_lt_of_not_lt := eq_or_gt_of_not_lt
 
+@[to_dual self (reorder := a b, c d)]
 theorem le_imp_le_of_lt_imp_lt {α β} [Preorder α] [LinearOrder β] {a b : α} {c d : β}
     (H : d < c → b < a) (h : a ≤ b) : c ≤ d :=
   le_of_not_gt fun h' => not_le_of_gt (H h') h
@@ -134,62 +149,50 @@ lemma min_def (a b : α) : min a b = if a ≤ b then a else b := LinearOrder.min
 @[grind =]
 lemma max_def (a b : α) : max a b = if a ≤ b then b else a := LinearOrder.max_def a b
 
+@[to_dual existing max_def]
+theorem min_def' (a b : α) : min a b = if b ≤ a then b else a := by grind
+
+@[to_dual existing min_def]
+theorem max_def' (a b : α) : max a b = if b ≤ a then a else b := by grind
+
+@[to_dual le_max_left]
 lemma min_le_left (a b : α) : min a b ≤ a := by grind
 
+@[to_dual le_max_right]
 lemma min_le_right (a b : α) : min a b ≤ b := by grind
 
+@[to_dual max_le]
 lemma le_min (h₁ : c ≤ a) (h₂ : c ≤ b) : c ≤ min a b := by grind
 
-lemma le_max_left (a b : α) : a ≤ max a b := by grind
-
-lemma le_max_right (a b : α) : b ≤ max a b := by grind
-
-lemma max_le (h₁ : a ≤ c) (h₂ : b ≤ c) : max a b ≤ c := by grind
-
+@[to_dual]
 lemma eq_min (h₁ : c ≤ a) (h₂ : c ≤ b) (h₃ : ∀ {d}, d ≤ a → d ≤ b → d ≤ c) : c = min a b :=
   le_antisymm (le_min h₁ h₂) (h₃ (min_le_left a b) (min_le_right a b))
 
+@[to_dual]
 lemma min_comm (a b : α) : min a b = min b a :=
   eq_min (min_le_right a b) (min_le_left a b) fun h₁ h₂ => le_min h₂ h₁
 
+@[to_dual]
 lemma min_assoc (a b c : α) : min (min a b) c = min a (min b c) := by grind
 
+@[to_dual]
 lemma min_left_comm (a b c : α) : min a (min b c) = min b (min a c) := by grind
 
-@[simp] lemma min_self (a : α) : min a a = a := by grind
+@[to_dual (attr := simp)] lemma min_self (a : α) : min a a = a := by grind
 
+@[to_dual]
 lemma min_eq_left (h : a ≤ b) : min a b = a := by grind
 
+@[to_dual]
 lemma min_eq_right (h : b ≤ a) : min a b = b := min_comm b a ▸ min_eq_left h
 
-lemma eq_max (h₁ : a ≤ c) (h₂ : b ≤ c) (h₃ : ∀ {d}, a ≤ d → b ≤ d → c ≤ d) :
-    c = max a b :=
-  le_antisymm (h₃ (le_max_left a b) (le_max_right a b)) (max_le h₁ h₂)
-
-lemma max_comm (a b : α) : max a b = max b a :=
-  eq_max (le_max_right a b) (le_max_left a b) fun h₁ h₂ => max_le h₂ h₁
-
-lemma max_assoc (a b c : α) : max (max a b) c = max a (max b c) := by grind
-
-lemma max_left_comm (a b c : α) : max a (max b c) = max b (max a c) := by grind
-
-@[simp] lemma max_self (a : α) : max a a = a := by grind
-
-lemma max_eq_left (h : b ≤ a) : max a b = a := by grind
-
-lemma max_eq_right (h : a ≤ b) : max a b = b := max_comm b a ▸ max_eq_left h
-
-lemma min_eq_left_of_lt (h : a < b) : min a b = a := min_eq_left (le_of_lt h)
-lemma min_eq_right_of_lt (h : b < a) : min a b = b := min_eq_right (le_of_lt h)
-lemma max_eq_left_of_lt (h : b < a) : max a b = a := max_eq_left (le_of_lt h)
-lemma max_eq_right_of_lt (h : a < b) : max a b = b := max_eq_right (le_of_lt h)
+@[to_dual] lemma min_eq_left_of_lt (h : a < b) : min a b = a := min_eq_left (le_of_lt h)
+@[to_dual] lemma min_eq_right_of_lt (h : b < a) : min a b = b := min_eq_right (le_of_lt h)
 
+@[to_dual max_lt]
 lemma lt_min (h₁ : a < b) (h₂ : a < c) : a < min b c := by
   cases le_total b c <;> simp [min_eq_left, min_eq_right, *]
 
-lemma max_lt (h₁ : a < c) (h₂ : b < c) : max a b < c := by
-  cases le_total a b <;> simp [max_eq_left, max_eq_right, *]
-
 section Ord
 
 lemma compare_lt_iff_lt : compare a b = .lt ↔ a < b := by

Mathlib/Tactic/ToDual.lean

@@ -41,3 +41,24 @@ attribute [to_dual lt_of_eq_of_lt''] lt_of_eq_of_lt
 attribute [to_dual lt_of_lt_of_eq''] lt_of_lt_of_eq
 
 attribute [to_dual] Max
+
+-- We need to tag the lemmas used by `grind` in order to translate `grind` proofs.
+namespace Lean.Grind.Order
+
+attribute [to_dual existing le_of_eq_1] le_of_eq_2
+attribute [to_dual self (reorder := a b)] le_of_not_le lt_of_not_le le_of_not_lt
+attribute [to_dual self (reorder := 6 7)] eq_of_le_of_le
+attribute [to_dual self (reorder := a c, h₁ h₂)] le_trans lt_trans
+attribute [to_dual existing (reorder := a c, h₁ h₂) le_lt_trans] lt_le_trans
+attribute [to_dual self (reorder := a b)]
+  le_eq_true_of_lt le_eq_false_of_lt lt_eq_false_of_lt lt_eq_false_of_le
+
+/- For now, we don't tag any `grind` lemmas involving offsets, but this may be done in the future.
+These offset lemmas are:
+
+le_of_eq_1_k, le_of_eq_2_k, le_of_not_lt_k, lt_of_not_le_k, le_trans_k, lt_trans_k, le_lt_trans_k,
+lt_le_trans_k, le_unsat_k, lt_unsat_k, le_eq_true_of_le_k, le_eq_true_of_lt_k, lt_eq_true_of_lt_k,
+lt_eq_true_of_le_k, le_eq_false_of_le_k, lt_eq_false_of_le_k, lt_eq_false_of_lt_k,
+le_eq_false_of_lt_k -/
+
+end Lean.Grind.Order