fix

astrainfinita · astrainfinita · commit 958c4a56410c · 2023-10-21T22:07:26.000+08:00
diff --git a/Mathlib/Algebra/Order/Field/Canonical/Defs.lean b/Mathlib/Algebra/Order/Field/Canonical/Defs.lean
@@ -16,8 +16,7 @@ import Mathlib.Algebra.Order.WithZero
 
 variable {α : Type _} [LinearOrderedSemifield α] [CanonicallyOrderedAdd α]
 
--- See note [lower instance priority]
-instance (priority := 100) CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero :
+abbrev CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero :
     LinearOrderedCommGroupWithZero α :=
   { ‹LinearOrderedSemifield α› with
     mul_le_mul_left := fun a b h c ↦ mul_le_mul_of_nonneg_left h <| zero_le _ }
diff --git a/Mathlib/Algebra/Order/Ring/Canonical.lean b/Mathlib/Algebra/Order/Ring/Canonical.lean
@@ -82,8 +82,7 @@ instance (priority := 100) toOrderedCommMonoid
   mul_le_mul_left _ _ := mul_le_mul_left'
 #align canonically_ordered_comm_semiring.to_ordered_comm_monoid CanonicallyOrderedAdd.toOrderedCommMonoid
 
--- see Note [lower instance priority]
-instance (priority := 100) toOrderedCommSemiring
+abbrev toOrderedCommSemiring
     [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α]
     [CovariantClass α α (· + ·) (· ≤ ·)] :
     OrderedCommSemiring α where
@@ -93,7 +92,7 @@ instance (priority := 100) toOrderedCommSemiring
   mul_le_mul_of_nonneg_left := fun _ _ _ h _ => mul_le_mul_left' h _
   mul_le_mul_of_nonneg_right := fun _ _ _ h _ => mul_le_mul_right' h _
 #align canonically_ordered_comm_semiring.to_ordered_comm_semiring CanonicallyOrderedAdd.toOrderedCommSemiring
---[OrderedSemiring α] [CanonicallyOrderedAdd α]
+
 @[simp]
 theorem mul_pos [NonUnitalNonAssocSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α]
     [NoZeroDivisors α] {a b : α} :
diff --git a/Mathlib/Data/DFinsupp/Lex.lean b/Mathlib/Data/DFinsupp/Lex.lean
@@ -194,7 +194,8 @@ section OrderedAddMonoid
 
 variable [LinearOrder ι]
 
-instance Lex.orderBot [∀ i, CanonicallyOrderedAddCommMonoid (α i)] :
+instance Lex.orderBot [∀ i, AddZeroClass (α i)] [∀ i, PartialOrder (α i)]
+    [∀ i, CanonicallyOrderedAdd (α i)] :
     OrderBot (Lex (Π₀ i, α i)) where
   bot := 0
   bot_le _ := DFinsupp.toLex_monotone bot_le
diff --git a/Mathlib/RingTheory/MvPolynomial/Symmetric.lean b/Mathlib/RingTheory/MvPolynomial/Symmetric.lean
@@ -303,7 +303,7 @@ theorem psum_one : psum σ R 1 = ∑ i, X i := by
 
 @[simp]
 theorem rename_psum (n : ℕ) (e : σ ≃ τ) : rename e (psum σ R n) = psum τ R n := by
-  simp_rw [psum, map_sum, map_pow, rename_X, e.sum_comp (X · ^ n)]
+  simp_rw [psum, map_sum, map_pow, rename_X, e.sum_comp (fun i ↦ (X i ^ n : MvPolynomial τ R))]
 
 theorem psum_isSymmetric (n : ℕ) : IsSymmetric (psum σ R n) := rename_psum _ _ n
 
