chore(Algebra/Order/SuccPred/TypeTags): fix defeq abuse with Additive…

… and Multiplicative (#19379) these simp lemmas now don't use defeq abuse between `A` and `Multiplicative A`.
leanprover-community · Nov 22, 2024 · 9e7e427 · 9e7e427
1 parent dd74f01
commit 9e7e427
Showing 1 changed file with 8 additions and 4 deletions.
diff --git a/Mathlib/Algebra/Order/SuccPred/TypeTags.lean b/Mathlib/Algebra/Order/SuccPred/TypeTags.lean
@@ -36,15 +36,19 @@ namespace Order
 open Additive Multiplicative
 
 @[simp] lemma succ_ofMul [Preorder X] [SuccOrder X] (x : X) : succ (ofMul x) = ofMul (succ x) := rfl
-@[simp] lemma succ_toMul [Preorder X] [SuccOrder X] (x : X) : succ (toMul x) = toMul (succ x) := rfl
+@[simp] lemma succ_toMul [Preorder X] [SuccOrder X] (x : Additive X) :
+  succ (toMul x) = toMul (succ x) := rfl
 
 @[simp] lemma succ_ofAdd [Preorder X] [SuccOrder X] (x : X) : succ (ofAdd x) = ofAdd (succ x) := rfl
-@[simp] lemma succ_toAdd [Preorder X] [SuccOrder X] (x : X) : succ (toAdd x) = toAdd (succ x) := rfl
+@[simp] lemma succ_toAdd [Preorder X] [SuccOrder X] (x : Multiplicative X) :
+  succ (toAdd x) = toAdd (succ x) := rfl
 
 @[simp] lemma pred_ofMul [Preorder X] [PredOrder X] (x : X) : pred (ofMul x) = ofMul (pred x) := rfl
-@[simp] lemma pred_toMul [Preorder X] [PredOrder X] (x : X) : pred (toMul x) = toMul (pred x) := rfl
+@[simp] lemma pred_toMul [Preorder X] [PredOrder X] (x : Additive X) :
+  pred (toMul x) = toMul (pred x) := rfl
 
 @[simp] lemma pred_ofAdd [Preorder X] [PredOrder X] (x : X) : pred (ofAdd x) = ofAdd (pred x) := rfl
-@[simp] lemma pred_toAdd [Preorder X] [PredOrder X] (x : X) : pred (toAdd x) = toAdd (pred x) := rfl
+@[simp] lemma pred_toAdd [Preorder X] [PredOrder X] (x : Multiplicative X) :
+  pred (toAdd x) = toAdd (pred x) := rfl
 
 end Order