feat: to_dual attribute (#27887)

This PR defines the `to_dual` attribute for translating lemmas to their dual. This is useful in order theory and in category theory. It is built on top of the `to_additive` machinery.

This PR only adds `@[to_dual]` tags in files that directly need to import `ToDual`, namely `Order/Defs/PartialOrder`, `Order/Notation` and `Combinatorics/Quiver/Basic`. Further tagging is left for (many) future PRs.

This PR continues the work from #21719

Related (mathlib3) issues: 
- leanprover-community/mathlib3#13461
- leanprover-community/mathlib3#7691

Co-authored-by: @bryangingechen
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Author: JovanGerb

Mathlib.lean

@@ -6508,6 +6508,9 @@ import Mathlib.Tactic.TermCongr
 import Mathlib.Tactic.ToAdditive
 import Mathlib.Tactic.ToAdditive.Frontend
 import Mathlib.Tactic.ToAdditive.GuessName
+import Mathlib.Tactic.ToAdditive.ToAdditive
+import Mathlib.Tactic.ToAdditive.ToDual
+import Mathlib.Tactic.ToDual
 import Mathlib.Tactic.ToExpr
 import Mathlib.Tactic.ToLevel
 import Mathlib.Tactic.Trace

Mathlib/Algebra/Order/Group/Defs.lean

@@ -59,7 +59,7 @@ but we still use the namespaces.
 
 TODO: everything in these namespaces should be renamed; even if these typeclasses still existed,
 it's unconventional to put theorems in namespaces named after them. -/
-run_meta ToAdditive.insertTranslation `LinearOrderedCommGroup `LinearOrderedAddCommGroup
+insert_to_additive_translation LinearOrderedCommGroup LinearOrderedAddCommGroup
 
 section LinearOrderedCommGroup
 

Mathlib/Combinatorics/Quiver/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Wärn, Kim Morrison
 -/
 import Mathlib.Data.Opposite
+import Mathlib.Tactic.ToDual
 
 /-!
 # Quivers
@@ -41,6 +42,8 @@ class Quiver (V : Type u) where
   /-- The type of edges/arrows/morphisms between a given source and target. -/
   Hom : V → V → Sort v
 
+attribute [to_dual self (reorder := 3 4)] Quiver.Hom
+
 /--
 Notation for the type of edges/arrows/morphisms between a given source and target
 in a quiver or category.
@@ -54,13 +57,15 @@ instance opposite {V} [Quiver V] : Quiver Vᵒᵖ :=
   ⟨fun a b => (unop b ⟶ unop a)ᵒᵖ⟩
 
 /-- The opposite of an arrow in `V`. -/
+@[to_dual self (reorder := 3 4)]
 def Hom.op {V} [Quiver V] {X Y : V} (f : X ⟶ Y) : op Y ⟶ op X := ⟨f⟩
 
 /-- Given an arrow in `Vᵒᵖ`, we can take the "unopposite" back in `V`. -/
+@[to_dual self (reorder := 3 4)]
 def Hom.unop {V} [Quiver V] {X Y : Vᵒᵖ} (f : X ⟶ Y) : unop Y ⟶ unop X := Opposite.unop f
 
 /-- The bijection `(X ⟶ Y) ≃ (op Y ⟶ op X)`. -/
-@[simps]
+@[simps, to_dual self (reorder := 3 4)]
 def Hom.opEquiv {V} [Quiver V] {X Y : V} :
     (X ⟶ Y) ≃ (Opposite.op Y ⟶ Opposite.op X) where
   toFun := Opposite.op
@@ -71,64 +76,70 @@ def Empty (V : Type u) : Type u := V
 
 instance emptyQuiver (V : Type u) : Quiver.{u} (Empty V) := ⟨fun _ _ => PEmpty⟩
 
-@[simp]
+@[simp, to_dual self (reorder := 2 3)]
 theorem empty_arrow {V : Type u} (a b : Empty V) : (a ⟶ b) = PEmpty := rfl
 
 /-- A quiver is thin if it has no parallel arrows. -/
+@[to_dual IsThin' /-- `isThin'` is equivalent to `IsThin`.
+It is used by `@[to_dual]` to be able to translate `IsThin`. -/]
 abbrev IsThin (V : Type u) [Quiver V] : Prop := ∀ a b : V, Subsingleton (a ⟶ b)
 
 
 section
 
-variable {V : Type*} [Quiver V]
+variable {V : Type*} [Quiver V] {X Y X' Y' : V}
 
 /-- An arrow in a quiver can be transported across equalities between the source and target
 objects. -/
-def homOfEq {X Y : V} (f : X ⟶ Y) {X' Y' : V} (hX : X = X') (hY : Y = Y') : X' ⟶ Y' := by
+@[to_dual self (reorder := 3 4, 5 6, 8 9)]
+def homOfEq (f : X ⟶ Y) (hX : X = X') (hY : Y = Y') : X' ⟶ Y' := by
   subst hX hY
   exact f
 
-@[simp]
-lemma homOfEq_trans {X Y : V} (f : X ⟶ Y) {X' Y' : V} (hX : X = X') (hY : Y = Y')
+@[simp, to_dual self (reorder := 3 4, 5 6, 8 9, 10 11, 12 13)]
+lemma homOfEq_trans (f : X ⟶ Y) (hX : X = X') (hY : Y = Y')
     {X'' Y'' : V} (hX' : X' = X'') (hY' : Y' = Y'') :
     homOfEq (homOfEq f hX hY) hX' hY' = homOfEq f (hX.trans hX') (hY.trans hY') := by
   subst hX hY hX' hY'
   rfl
 
-lemma homOfEq_injective {X X' Y Y' : V} (hX : X = X') (hY : Y = Y')
+@[to_dual self (reorder := 3 4, 5 6, 7 8)]
+lemma homOfEq_injective (hX : X = X') (hY : Y = Y')
     {f g : X ⟶ Y} (h : Quiver.homOfEq f hX hY = Quiver.homOfEq g hX hY) : f = g := by
   subst hX hY
   exact h
 
-@[simp]
-lemma homOfEq_rfl {X Y : V} (f : X ⟶ Y) : Quiver.homOfEq f rfl rfl = f := rfl
+@[simp, to_dual self (reorder := 3 4)]
+lemma homOfEq_rfl (f : X ⟶ Y) : Quiver.homOfEq f rfl rfl = f := rfl
 
-lemma heq_of_homOfEq_ext {X Y X' Y' : V} (hX : X = X') (hY : Y = Y') {f : X ⟶ Y} {f' : X' ⟶ Y'}
+@[to_dual self (reorder := 3 4, 5 6, 7 8)]
+lemma heq_of_homOfEq_ext (hX : X = X') (hY : Y = Y') {f : X ⟶ Y} {f' : X' ⟶ Y'}
     (e : Quiver.homOfEq f hX hY = f') : f ≍ f' := by
   subst hX hY
   rw [Quiver.homOfEq_rfl] at e
   rw [e]
 
-lemma homOfEq_eq_iff {X X' Y Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y')
-    (hX : X = X') (hY : Y = Y') :
+@[to_dual self (reorder := 3 4, 5 6, 9 10)]
+lemma homOfEq_eq_iff (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X = X') (hY : Y = Y') :
     Quiver.homOfEq f hX hY = g ↔ f = Quiver.homOfEq g hX.symm hY.symm := by
   subst hX hY; simp
 
-lemma eq_homOfEq_iff {X X' Y Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y')
-    (hX : X' = X) (hY : Y' = Y) :
+@[to_dual self (reorder := 3 4, 5 6, 9 10)]
+lemma eq_homOfEq_iff (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X' = X) (hY : Y' = Y) :
     f = Quiver.homOfEq g hX hY ↔ Quiver.homOfEq f hX.symm hY.symm = g := by
   subst hX hY; simp
 
-lemma homOfEq_heq {X Y X' Y' : V} (hX : X = X') (hY : Y = Y') (f : X ⟶ Y) :
-    homOfEq f hX hY ≍ f := (heq_of_homOfEq_ext hX hY rfl).symm
+@[to_dual self (reorder := 3 4, 5 6, 7 8)]
+lemma homOfEq_heq (hX : X = X') (hY : Y = Y') (f : X ⟶ Y) : homOfEq f hX hY ≍ f :=
+  (heq_of_homOfEq_ext hX hY rfl).symm
 
-lemma homOfEq_heq_left_iff {X Y X' Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y')
-    (hX : X = X') (hY : Y = Y') :
+@[to_dual self (reorder := 3 4, 5 6, 9 10)]
+lemma homOfEq_heq_left_iff (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X = X') (hY : Y = Y') :
     homOfEq f hX hY ≍ g ↔ f ≍ g := by
   cases hX; cases hY; rfl
 
-lemma homOfEq_heq_right_iff {X Y X' Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y')
-    (hX : X' = X) (hY : Y' = Y) :
+@[to_dual self (reorder := 3 4, 5 6, 9 10)]
+lemma homOfEq_heq_right_iff (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X' = X) (hY : Y' = Y) :
     f ≍ homOfEq g hX hY ↔ f ≍ g := by
   cases hX; cases hY; rfl
 

Mathlib/GroupTheory/Coset/Defs.lean

@@ -46,7 +46,7 @@ open scoped Pointwise
 variable {α : Type*}
 
 /- Ensure that `@[to_additive]` uses the right namespace. -/
-run_meta ToAdditive.insertTranslation `QuotientGroup `QuotientAddGroup
+insert_to_additive_translation QuotientGroup QuotientAddGroup
 
 namespace QuotientGroup
 

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -58,7 +58,7 @@ variable {α : Type u}
 attribute [local simp] List.append_eq_has_append
 
 /- Ensure that `@[to_additive]` uses the right namespace before the definition of `FreeGroup`. -/
-run_meta ToAdditive.insertTranslation `FreeGroup `FreeAddGroup
+insert_to_additive_translation FreeGroup FreeAddGroup
 
 /-- Reduction step for the additive free group relation: `w + x + (-x) + v ~> w + v` -/
 inductive FreeAddGroup.Red.Step : List (α × Bool) → List (α × Bool) → Prop

Mathlib/GroupTheory/MonoidLocalization/Basic.lean

@@ -115,7 +115,7 @@ end Submonoid
 namespace Localization
 
 /- Ensure that `@[to_additive]` uses the right namespace before the definition of `Localization`. -/
-run_meta ToAdditive.insertTranslation `Localization `AddLocalization
+insert_to_additive_translation Localization AddLocalization
 
 /-- The congruence relation on `M × S`, `M` a `CommMonoid` and `S` a submonoid of `M`, whose
 quotient is the localization of `M` at `S`, defined as the unique congruence relation on

Mathlib/Order/Basic.lean

@@ -128,8 +128,6 @@ lemma not_lt_iff_le_imp_ge : ¬ a < b ↔ (a ≤ b → b ≤ a) := by
 
 @[deprecated (since := "2025-05-11")] alias not_lt_iff_le_imp_le := not_lt_iff_le_imp_ge
 
-lemma ge_of_eq (h : a = b) : b ≤ a := le_of_eq h.symm
-
 @[simp] lemma lt_self_iff_false (x : α) : x < x ↔ False := ⟨lt_irrefl x, False.elim⟩
 
 alias le_trans' := ge_trans
@@ -209,11 +207,6 @@ section PartialOrder
 
 variable [PartialOrder α] {a b : α}
 
-theorem ge_antisymm : a ≤ b → b ≤ a → b = a :=
-  flip le_antisymm
-
-theorem lt_of_le_of_ne' : a ≤ b → b ≠ a → a < b := fun h₁ h₂ ↦ lt_of_le_of_ne h₁ h₂.symm
-
 theorem Ne.lt_of_le : a ≠ b → a ≤ b → a < b :=
   flip lt_of_le_of_ne
 
@@ -293,7 +286,6 @@ protected theorem Decidable.eq_or_lt_of_le [DecidableLE α] (h : a ≤ b) : a =
 
 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
-theorem lt_or_eq_of_le' (h : a ≤ b) : a < b ∨ b = a := (eq_or_lt_of_le' h).symm
 
 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

Mathlib/Order/Defs/PartialOrder.lean

@@ -9,6 +9,7 @@ import Mathlib.Tactic.ExtendDoc
 import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.SplitIfs
 import Mathlib.Tactic.TypeStar
+import Mathlib.Tactic.ToDual
 
 /-!
 # Orders
@@ -43,6 +44,9 @@ class Preorder (α : Type*) extends LE α, LT α where
   lt := fun a b => a ≤ b ∧ ¬b ≤ a
   lt_iff_le_not_ge : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
 
+attribute [to_dual self (reorder := 3 5, 6 7)] Preorder.le_trans
+attribute [to_dual self (reorder := 3 4)] Preorder.lt_iff_le_not_ge
+
 instance [Preorder α] : Std.LawfulOrderLT α where
   lt_iff := Preorder.lt_iff_le_not_ge
 
@@ -61,79 +65,92 @@ variable [Preorder α] {a b c : α}
 lemma le_rfl : a ≤ a := le_refl a
 
 /-- The relation `≤` on a preorder is transitive. -/
-lemma le_trans : a ≤ b → b ≤ c → a ≤ c := Preorder.le_trans _ _ _
+@[to_dual ge_trans] lemma le_trans : a ≤ b → b ≤ c → a ≤ c := Preorder.le_trans _ _ _
 
+@[to_dual self (reorder := 3 4)]
 lemma lt_iff_le_not_ge : a < b ↔ a ≤ b ∧ ¬b ≤ a := Preorder.lt_iff_le_not_ge _ _
 
 @[deprecated (since := "2025-05-11")] alias lt_iff_le_not_le := lt_iff_le_not_ge
 
+@[to_dual self (reorder := 3 4)]
 lemma lt_of_le_not_ge (hab : a ≤ b) (hba : ¬ b ≤ a) : a < b := lt_iff_le_not_ge.2 ⟨hab, hba⟩
 
 @[deprecated (since := "2025-05-11")] alias lt_of_le_not_le := lt_of_le_not_ge
 
+@[to_dual ge_of_eq]
 lemma le_of_eq (hab : a = b) : a ≤ b := by rw [hab]
+@[to_dual self (reorder := 3 4)]
 lemma le_of_lt (hab : a < b) : a ≤ b := (lt_iff_le_not_ge.1 hab).1
+@[to_dual self (reorder := 3 4)]
 lemma not_le_of_gt (hab : a < b) : ¬ b ≤ a := (lt_iff_le_not_ge.1 hab).2
+@[to_dual self (reorder := 3 4)]
 lemma not_lt_of_ge (hab : a ≤ b) : ¬ b < a := imp_not_comm.1 not_le_of_gt hab
 
 @[deprecated (since := "2025-05-11")] alias not_le_of_lt := not_le_of_gt
 @[deprecated (since := "2025-05-11")] alias not_lt_of_le := not_lt_of_ge
 
-alias LT.lt.not_ge := not_le_of_gt
-alias LE.le.not_gt := not_lt_of_ge
+@[to_dual self (reorder := 3 4)] alias LT.lt.not_ge := not_le_of_gt
+@[to_dual self (reorder := 3 4)] alias LE.le.not_gt := not_lt_of_ge
 
 @[deprecated (since := "2025-06-07")] alias LT.lt.not_le := LT.lt.not_ge
 @[deprecated (since := "2025-06-07")] alias LE.le.not_lt := LE.le.not_gt
 
-
-lemma ge_trans : b ≤ a → c ≤ b → c ≤ a := fun h₁ h₂ => le_trans h₂ h₁
-
-lemma lt_irrefl (a : α) : ¬a < a := fun h ↦ not_le_of_gt h le_rfl
+@[to_dual self] lemma lt_irrefl (a : α) : ¬a < a := fun h ↦ not_le_of_gt h le_rfl
 
 @[deprecated (since := "2025-06-07")] alias gt_irrefl := lt_irrefl
 
+@[to_dual lt_of_lt_of_le']
 lemma lt_of_lt_of_le (hab : a < b) (hbc : b ≤ c) : a < c :=
   lt_of_le_not_ge (le_trans (le_of_lt hab) hbc) fun hca ↦ not_le_of_gt hab (le_trans hbc hca)
 
+@[to_dual lt_of_le_of_lt']
 lemma lt_of_le_of_lt (hab : a ≤ b) (hbc : b < c) : a < c :=
   lt_of_le_not_ge (le_trans hab (le_of_lt hbc)) fun hca ↦ not_le_of_gt hbc (le_trans hca hab)
 
-lemma lt_of_lt_of_le' : b < a → c ≤ b → c < a := flip lt_of_le_of_lt
-lemma lt_of_le_of_lt' : b ≤ a → c < b → c < a := flip lt_of_lt_of_le
-
 @[deprecated (since := "2025-06-07")] alias gt_of_gt_of_ge := lt_of_lt_of_le'
 @[deprecated (since := "2025-06-07")] alias gt_of_ge_of_gt := lt_of_le_of_lt'
 
+@[to_dual gt_trans]
 lemma lt_trans : a < b → b < c → a < c := fun h₁ h₂ => lt_of_lt_of_le h₁ (le_of_lt h₂)
-lemma gt_trans : b < a → c < b → c < a := flip lt_trans
 
+@[to_dual ne_of_gt]
 lemma ne_of_lt (h : a < b) : a ≠ b := fun he => absurd h (he ▸ lt_irrefl a)
-lemma ne_of_gt (h : b < a) : a ≠ b := fun he => absurd h (he ▸ lt_irrefl a)
+@[to_dual self (reorder := 3 4)]
 lemma lt_asymm (h : a < b) : ¬b < a := fun h1 : b < a => lt_irrefl a (lt_trans h h1)
 
+@[to_dual self (reorder := 3 4)]
 alias not_lt_of_gt := lt_asymm
-
 @[deprecated (since := "2025-05-11")] alias not_lt_of_lt := not_lt_of_gt
 
+@[to_dual le_of_lt_or_eq']
 lemma le_of_lt_or_eq (h : a < b ∨ a = b) : a ≤ b := h.elim le_of_lt le_of_eq
+@[to_dual le_of_eq_or_lt']
 lemma le_of_eq_or_lt (h : a = b ∨ a < b) : a ≤ b := h.elim le_of_eq le_of_lt
 
-instance : @Trans α α α LE.le LE.le LE.le := ⟨le_trans⟩
-instance : @Trans α α α LT.lt LT.lt LT.lt := ⟨lt_trans⟩
-instance : @Trans α α α LT.lt LE.le LT.lt := ⟨lt_of_lt_of_le⟩
-instance : @Trans α α α LE.le LT.lt LT.lt := ⟨lt_of_le_of_lt⟩
-instance : @Trans α α α GE.ge GE.ge GE.ge := ⟨ge_trans⟩
-instance : @Trans α α α GT.gt GT.gt GT.gt := ⟨gt_trans⟩
-instance : @Trans α α α GT.gt GE.ge GT.gt := ⟨lt_of_lt_of_le'⟩
-instance : @Trans α α α GE.ge GT.gt GT.gt := ⟨lt_of_le_of_lt'⟩
+instance instTransLE : @Trans α α α LE.le LE.le LE.le := ⟨le_trans⟩
+instance instTransLT : @Trans α α α LT.lt LT.lt LT.lt := ⟨lt_trans⟩
+instance instTransLTLE : @Trans α α α LT.lt LE.le LT.lt := ⟨lt_of_lt_of_le⟩
+instance instTransLELT : @Trans α α α LE.le LT.lt LT.lt := ⟨lt_of_le_of_lt⟩
+-- we have to express the following 4 instances in terms of `≥` instead of flipping the arguments
+-- to `≤`, because otherwise `calc` gets confused.
+@[to_dual existing instTransLE]
+instance instTransGE : @Trans α α α GE.ge GE.ge GE.ge := ⟨ge_trans⟩
+@[to_dual existing instTransLT]
+instance instTransGT : @Trans α α α GT.gt GT.gt GT.gt := ⟨gt_trans⟩
+@[to_dual existing instTransLTLE]
+instance instTransGTGE : @Trans α α α GT.gt GE.ge GT.gt := ⟨lt_of_lt_of_le'⟩
+@[to_dual existing instTransLELT]
+instance instTransGEGT : @Trans α α α GE.ge GT.gt GT.gt := ⟨lt_of_le_of_lt'⟩
 
 /-- `<` is decidable if `≤` is. -/
+@[to_dual decidableGTOfDecidableGE /-- `<` is decidable if `≤` is. -/]
 def decidableLTOfDecidableLE [DecidableLE α] : DecidableLT α :=
   fun _ _ => decidable_of_iff _ lt_iff_le_not_ge.symm
 
 /-- `WCovBy a b` means that `a = b` or `b` covers `a`.
 This means that `a ≤ b` and there is no element in between. This is denoted `a ⩿ b`.
 -/
+@[to_dual self (reorder := 3 4)]
 def WCovBy (a b : α) : Prop :=
   a ≤ b ∧ ∀ ⦃c⦄, a < c → ¬c < b
 
@@ -142,6 +159,7 @@ infixl:50 " ⩿ " => WCovBy
 
 /-- `CovBy a b` means that `b` covers `a`. This means that `a < b` and there is no element in
 between. This is denoted `a ⋖ b`. -/
+@[to_dual self (reorder := 3 4)]
 def CovBy {α : Type*} [LT α] (a b : α) : Prop :=
   a < b ∧ ∀ ⦃c⦄, a < c → ¬c < b
 
@@ -160,38 +178,49 @@ section PartialOrder
 class PartialOrder (α : Type*) extends Preorder α where
   le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
 
+attribute [to_dual self (reorder := 5 6)] PartialOrder.le_antisymm
+
 instance [PartialOrder α] : Std.IsPartialOrder α where
   le_antisymm := PartialOrder.le_antisymm
 
 variable [PartialOrder α] {a b : α}
 
+@[to_dual ge_antisymm]
 lemma le_antisymm : a ≤ b → b ≤ a → a = b := PartialOrder.le_antisymm _ _
 
+@[to_dual eq_of_ge_of_le]
 alias eq_of_le_of_ge := le_antisymm
 
 @[deprecated (since := "2025-06-07")] alias eq_of_le_of_le := eq_of_le_of_ge
 
+@[to_dual ge_antisymm_iff]
 lemma le_antisymm_iff : a = b ↔ a ≤ b ∧ b ≤ a :=
   ⟨fun e => ⟨le_of_eq e, le_of_eq e.symm⟩, fun ⟨h1, h2⟩ => le_antisymm h1 h2⟩
 
+@[to_dual lt_of_le_of_ne']
 lemma lt_of_le_of_ne : a ≤ b → a ≠ b → a < b := fun h₁ h₂ =>
   lt_of_le_not_ge h₁ <| mt (le_antisymm h₁) h₂
 
 /-- Equality is decidable if `≤` is. -/
+@[to_dual decidableEqofDecidableGE /-- Equality is decidable if `≤` is. -/]
 def decidableEqOfDecidableLE [DecidableLE α] : DecidableEq α
   | a, b =>
     if hab : a ≤ b then
       if hba : b ≤ a then isTrue (le_antisymm hab hba) else isFalse fun heq => hba (heq ▸ le_refl _)
     else isFalse fun heq => hab (heq ▸ le_refl _)
 
 -- See Note [decidable namespace]
+@[to_dual Decidable.lt_or_eq_of_le']
 protected lemma Decidable.lt_or_eq_of_le [DecidableLE α] (hab : a ≤ b) : a < b ∨ a = b :=
   if hba : b ≤ a then Or.inr (le_antisymm hab hba) else Or.inl (lt_of_le_not_ge hab hba)
 
+@[to_dual Decidable.le_iff_lt_or_eq']
 protected lemma Decidable.le_iff_lt_or_eq [DecidableLE α] : a ≤ b ↔ a < b ∨ a = b :=
   ⟨Decidable.lt_or_eq_of_le, le_of_lt_or_eq⟩
 
+@[to_dual lt_or_eq_of_le']
 lemma lt_or_eq_of_le : a ≤ b → a < b ∨ a = b := open scoped Classical in Decidable.lt_or_eq_of_le
+@[to_dual le_iff_lt_or_eq']
 lemma le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b := open scoped Classical in Decidable.le_iff_lt_or_eq
 
 end PartialOrder