feat(translate): automatically infer the (reorder := ...) argument (#31902)

This PR adds the feature to `to_additive` and `to_dual` that if the translation already exists (i.e. when using `existing` or `self`) the attribute will try to guess how to reorder the arguments correctly. If you then provide the same `reorder` argument manually, the linter will tell you that you can remove it.

Author: JovanGerb

Mathlib/Algebra/Group/ULift.lean

@@ -69,11 +69,11 @@ instance smul [SMul α β] : SMul α (ULift β) :=
 theorem smul_down [SMul α β] (a : α) (b : ULift.{w} β) : (a • b).down = a • b.down :=
   rfl
 
-@[to_additive existing (reorder := 1 2) smul]
+@[to_additive existing smul]
 instance pow [Pow α β] : Pow (ULift α) β :=
   ⟨fun x n => up (x.down ^ n)⟩
 
-@[to_additive existing (attr := simp) (reorder := 1 2, 4 5) smul_down]
+@[to_additive existing (attr := simp) smul_down]
 theorem pow_down [Pow α β] (a : ULift.{w} α) (b : β) : (a ^ b).down = a.down ^ b :=
   rfl
 

Mathlib/Algebra/Notation/Defs.lean

@@ -78,7 +78,7 @@ attribute [to_additive existing (reorder := 1 2, 5 6) hSMul] HPow.hPow
 attribute [to_additive existing (reorder := 1 2, 4 5) smul] Pow.pow
 
 attribute [to_additive (attr := default_instance)] instHSMul
-attribute [to_additive existing (reorder := 1 2)] instHPow
+attribute [to_additive existing] instHPow
 
 variable {G : Type*}
 

Mathlib/Algebra/Notation/Prod.lean

@@ -158,19 +158,19 @@ variable {E α β : Type*} [Pow α E] [Pow β E]
 @[to_additive existing instSMul]
 instance instPow : Pow (α × β) E where pow p c := (p.1 ^ c, p.2 ^ c)
 
-@[to_additive existing (attr := simp) (reorder := 6 7) smul_fst]
+@[to_additive existing (attr := simp) smul_fst]
 lemma pow_fst (p : α × β) (c : E) : (p ^ c).fst = p.fst ^ c := rfl
 
-@[to_additive existing (attr := simp) (reorder := 6 7) smul_snd]
+@[to_additive existing (attr := simp) smul_snd]
 lemma pow_snd (p : α × β) (c : E) : (p ^ c).snd = p.snd ^ c := rfl
 
-@[to_additive existing (attr := simp) (reorder := 6 7 8) smul_mk]
+@[to_additive existing (attr := simp) smul_mk]
 lemma pow_mk (a : α) (b : β) (c : E) : Prod.mk a b ^ c = Prod.mk (a ^ c) (b ^ c) := rfl
 
-@[to_additive existing (reorder := 6 7) smul_def]
+@[to_additive existing smul_def]
 lemma pow_def (p : α × β) (c : E) : p ^ c = (p.1 ^ c, p.2 ^ c) := rfl
 
-@[to_additive existing (attr := simp) (reorder := 6 7) smul_swap]
+@[to_additive existing (attr := simp) smul_swap]
 lemma pow_swap (p : α × β) (c : E) : (p ^ c).swap = p.swap ^ c := rfl
 
 end Pow

Mathlib/Combinatorics/Quiver/Basic.lean

@@ -61,17 +61,16 @@ 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)]
+@[to_dual self]
 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)]
+@[to_dual self]
 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, to_dual self (reorder := 3 4)]
-def Hom.opEquiv {V} [Quiver V] {X Y : V} :
-    (X ⟶ Y) ≃ (Opposite.op Y ⟶ Opposite.op X) where
+@[simps, to_dual self]
+def Hom.opEquiv {V} [Quiver V] {X Y : V} : (X ⟶ Y) ≃ (Opposite.op Y ⟶ Opposite.op X) where
   toFun := Opposite.op
   invFun := Opposite.unop
 
@@ -80,7 +79,7 @@ def Empty (V : Type u) : Type u := V
 
 instance emptyQuiver (V : Type u) : Quiver.{u} (Empty V) := ⟨fun _ _ => PEmpty⟩
 
-@[simp, to_dual self (reorder := 2 3)]
+@[simp, to_dual self]
 theorem empty_arrow {V : Type u} (a b : Empty V) : (a ⟶ b) = PEmpty := rfl
 
 /-- A quiver is thin if it has no parallel arrows. -/
@@ -95,54 +94,54 @@ 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. -/
-@[to_dual self (reorder := 3 4, 5 6, 8 9)]
+@[to_dual self (reorder := X Y, X' Y', hX hY)]
 def homOfEq (f : X ⟶ Y) (hX : X = X') (hY : Y = Y') : X' ⟶ Y' := by
   subst hX hY
   exact f
 
-@[simp, to_dual self (reorder := 3 4, 5 6, 8 9, 10 11, 12 13)]
+@[simp, to_dual self]
 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
 
-@[to_dual self (reorder := 3 4, 5 6, 7 8)]
+@[to_dual self]
 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, to_dual self (reorder := 3 4)]
+@[simp, to_dual self]
 lemma homOfEq_rfl (f : X ⟶ Y) : Quiver.homOfEq f rfl rfl = f := rfl
 
-@[to_dual self (reorder := 3 4, 5 6, 7 8)]
+@[to_dual self]
 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]
 
-@[to_dual self (reorder := 3 4, 5 6, 9 10)]
+@[to_dual self]
 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
 
-@[to_dual self (reorder := 3 4, 5 6, 9 10)]
+@[to_dual self]
 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
 
-@[to_dual self (reorder := 3 4, 5 6, 7 8)]
+@[to_dual self]
 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
 
-@[to_dual self (reorder := 3 4, 5 6, 9 10)]
+@[to_dual self]
 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
 
-@[to_dual self (reorder := 3 4, 5 6, 9 10)]
+@[to_dual self]
 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/Order/Basic.lean

@@ -122,12 +122,12 @@ section Preorder
 
 variable [Preorder α] {a b c d : α}
 
-@[to_dual self (reorder := a b)]
+@[to_dual self]
 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)]
+@[to_dual self]
 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]
 
@@ -143,10 +143,10 @@ lemma lt_self_iff_false (x : α) : x < x ↔ False := ⟨lt_irrefl x, False.elim
 @[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
 
-@[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
+@[to_dual self] alias LE.le.lt_of_not_ge := lt_of_le_not_ge
+@[to_dual self] alias LT.lt.le := le_of_lt
+@[to_dual self] alias LT.lt.asymm := lt_asymm
+@[to_dual self] alias LT.lt.not_gt := lt_asymm
 
 @[to_dual ne'] alias LT.lt.ne := ne_of_lt
 @[to_dual ge] alias Eq.le := le_of_eq
@@ -161,11 +161,11 @@ lemma lt_self_iff_false (x : α) : x < x ↔ False := ⟨lt_irrefl x, False.elim
 @[to_dual ne_of_not_ge]
 theorem ne_of_not_le (h : ¬a ≤ b) : a ≠ b := fun hab ↦ h (le_of_eq hab)
 
-@[simp, to_dual self (reorder := a b)]
+@[simp, to_dual self]
 lemma le_of_subsingleton [Subsingleton α] : a ≤ b := (Subsingleton.elim a b).le
 
 -- Making this a @[simp] lemma causes confluence problems downstream.
-@[nontriviality, to_dual self (reorder := a b)]
+@[nontriviality, to_dual self]
 lemma not_lt_of_subsingleton [Subsingleton α] : ¬a < b := (Subsingleton.elim a b).not_lt
 
 @[to_dual le_of_forall_ge]

Mathlib/Order/Defs/LinearOrder.lean

@@ -92,16 +92,17 @@ def LinearOrder.toDecidableLE' : DecidableLE' α := fun a b => toDecidableLE b a
 instance : Std.IsLinearOrder α where
   le_total := LinearOrder.le_total
 
-lemma le_total : ∀ a b : α, a ≤ b ∨ b ≤ a := LinearOrder.le_total
+@[to_dual self] lemma le_total : ∀ a b : α, a ≤ b ∨ b ≤ a := LinearOrder.le_total
 
-lemma le_of_not_ge : ¬a ≤ b → b ≤ a := (le_total a b).resolve_left
-lemma lt_of_not_ge (h : ¬b ≤ a) : a < b := lt_of_le_not_ge (le_of_not_ge h) h
+@[to_dual self] lemma le_of_not_ge : ¬a ≤ b → b ≤ a := (le_total a b).resolve_left
+@[to_dual self] 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
 
+@[to_dual self]
 lemma le_of_not_gt (h : ¬b < a) : a ≤ b :=
   match lt_trichotomy a b with
   | Or.inl hlt => le_of_lt hlt
@@ -110,12 +111,12 @@ lemma le_of_not_gt (h : ¬b < a) : a ≤ b :=
 
 @[deprecated (since := "2025-05-11")] alias le_of_not_lt := le_of_not_gt
 
-lemma lt_or_ge (a b : α) : a < b ∨ b ≤ a :=
+@[to_dual self] lemma lt_or_ge (a b : α) : a < b ∨ b ≤ a :=
   if hba : b ≤ a then Or.inr hba else Or.inl <| lt_of_not_ge hba
 
 @[deprecated (since := "2025-05-11")] alias lt_or_le := lt_or_ge
 
-lemma le_or_gt (a b : α) : a ≤ b ∨ b < a := (lt_or_ge b a).symm
+@[to_dual self] 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
 
@@ -125,21 +126,18 @@ 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⟩
+@[to_dual self] 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
+@[simp, push, to_dual self] lemma not_lt : ¬a < b ↔ b ≤ a := ⟨le_of_not_gt, not_lt_of_ge⟩
+@[simp, push, to_dual self] lemma not_le : ¬a ≤ b ↔ b < a := lt_iff_not_ge.symm
 
 @[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-05-11")] alias eq_or_lt_of_not_lt := eq_or_gt_of_not_lt
 
-@[to_dual self (reorder := a b, c d)]
+@[to_dual self]
 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

Mathlib/Order/Defs/PartialOrder.lean

@@ -48,8 +48,8 @@ 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
+attribute [to_dual self (reorder := a c, 6 7)] Preorder.le_trans
+attribute [to_dual self] Preorder.lt_iff_le_not_ge
 
 instance [Preorder α] : Std.LawfulOrderLT α where
   lt_iff := Preorder.lt_iff_le_not_ge
@@ -71,30 +71,26 @@ lemma le_rfl : a ≤ a := le_refl a
 /-- The relation `≤` on a preorder is transitive. -/
 @[to_dual ge_trans] lemma le_trans : a ≤ b → b ≤ c → a ≤ c := Preorder.le_trans _ _ _
 
-@[to_dual self (reorder := 3 4)]
+@[to_dual self]
 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)]
+@[to_dual self]
 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
+@[to_dual ge_of_eq] lemma le_of_eq (hab : a = b) : a ≤ b := by rw [hab]
+@[to_dual self] lemma le_of_lt (hab : a < b) : a ≤ b := (lt_iff_le_not_ge.1 hab).1
+@[to_dual self] lemma not_le_of_gt (hab : a < b) : ¬ b ≤ a := (lt_iff_le_not_ge.1 hab).2
+@[to_dual self] 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
 
-@[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
+@[to_dual self] alias LT.lt.not_ge := not_le_of_gt
+@[to_dual self] 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
@@ -119,11 +115,11 @@ lemma lt_trans : a < b → b < c → a < c := fun h₁ h₂ => lt_of_lt_of_le h
 
 @[to_dual ne_of_gt]
 lemma ne_of_lt (h : a < b) : a ≠ b := fun he => absurd h (he ▸ lt_irrefl a)
-@[to_dual self (reorder := 3 4)]
+@[to_dual self]
 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
+@[to_dual self] 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']

Mathlib/Tactic/ToDual.lean

@@ -33,7 +33,7 @@ attribute [to_dual DecidableLE' /-- `DecidableLE'` is equivalent to `DecidableLE
 It is used by `@[to_dual]` in order to deal with `DecidableLE`. -/] DecidableLE
 
 set_option linter.existingAttributeWarning false in
-attribute [to_dual self (reorder := 3 4)] ge_iff_le gt_iff_lt
+attribute [to_dual self] ge_iff_le gt_iff_lt
 
 attribute [to_dual le_of_eq_of_le''] le_of_eq_of_le
 attribute [to_dual le_of_le_of_eq''] le_of_le_of_eq
@@ -46,12 +46,11 @@ attribute [to_dual] Max
 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] 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
+attribute [to_dual self] 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: