perf: increase some instance priorities

Mathlib/Algebra/Polynomial/Bivariate.lean

@@ -280,7 +280,7 @@ theorem Bivariate.swap_monomial (n : ℕ) (f : R[X]) :
 
 theorem Bivariate.swap_monomial_monomial (n m : ℕ) (r : R) :
     swap (monomial n (monomial m r)) = (monomial m (monomial n r)) := by
-  simp [← C_mul_X_pow_eq_monomial]; ac_rfl
+  simp [← C_mul_X_pow_eq_monomial, X_pow_mul_assoc]
 
 /-- Evaluating `swap p` at `x`, `y` is the same as evaluating `p` at `y` `x`. -/
 theorem Bivariate.aevalAeval_swap (x y : A) (p : R[X][Y]) :

Mathlib/Algebra/Polynomial/Coeff.lean

@@ -299,10 +299,11 @@ theorem coeff_X_add_C_pow (r : R) (n k : ℕ) :
     rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
 
 theorem coeff_X_add_one_pow (R : Type*) [Semiring R] (n k : ℕ) :
-    ((X + 1) ^ n).coeff k = (n.choose k : R) := by rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul]
+    ((X + 1 : R[X]) ^ n).coeff k = (n.choose k : R) := by
+  rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul]
 
 theorem coeff_one_add_X_pow (R : Type*) [Semiring R] (n k : ℕ) :
-    ((1 + X) ^ n).coeff k = (n.choose k : R) := by rw [add_comm _ X, coeff_X_add_one_pow]
+    ((1 + X : R[X]) ^ n).coeff k = (n.choose k : R) := by rw [add_comm _ X, coeff_X_add_one_pow]
 
 theorem one_add_X_pow_sub_X_pow {S : Type*} [CommRing S] (d : ℕ) :
     (1 + X : S[X]) ^ d - X ^ d = ∑ i ∈ range d, d.choose i • X ^ i := by

Mathlib/Algebra/Polynomial/Eval/Degree.lean

@@ -106,7 +106,7 @@ theorem coeff_comp_degree_mul_degree (hqd0 : natDegree q ≠ 0) :
 
 @[simp] lemma comp_C_mul_X_coeff {r : R} {n : ℕ} :
     (p.comp <| C r * X).coeff n = p.coeff n * r ^ n := by
-  simp_rw [comp, eval₂_eq_sum_range, (commute_X _).symm.mul_pow,
+  simp_rw [comp, eval₂_eq_sum_range, (commute_X (R := R) _).symm.mul_pow,
     ← C_pow, finsetSum_coeff, coeff_C_mul, coeff_X_pow]
   rw [Finset.sum_eq_single n _ fun h ↦ ?_, if_pos rfl, mul_one]
   · intro b _ h; simp_rw [if_neg h.symm, mul_zero]

Mathlib/Algebra/Quaternion.lean

@@ -1217,6 +1217,7 @@ theorem normSq_div : normSq (a / b) = normSq a / normSq b :=
 theorem normSq_zpow (z : ℤ) : normSq (a ^ z) = normSq a ^ z :=
   map_zpow₀ normSq a z
 
+omit [LinearOrder R] [IsStrictOrderedRing R] in
 @[norm_cast]
 theorem normSq_ratCast (q : ℚ) : normSq (q : ℍ[R]) = (q : ℍ[R]) ^ 2 := by
   rw [← coe_ratCast, normSq_coe, coe_pow]

Mathlib/Algebra/Ring/Defs.lean

@@ -145,6 +145,8 @@ class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α,
 /-- A `Ring` is a `Semiring` with negation making it an additive group. -/
 class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
 
+attribute [instance 1100] Ring.toSemiring
+
 /-!
 ### Semirings
 -/
@@ -221,6 +223,8 @@ class NonAssocCommSemiring (α : Type u)
 /-- A commutative semiring is a semiring with commutative multiplication. -/
 class CommSemiring (R : Type u) extends Semiring R, CommMonoid R
 
+attribute [instance 1100] CommSemiring.toSemiring
+
 attribute [instance 100] NonAssocCommSemiring.toNonAssocSemiring
 attribute [instance 100] NonAssocCommSemiring.toNonUnitalNonAssocCommSemiring
 
@@ -405,6 +409,8 @@ instance (priority := 100) NonUnitalCommRing.toNonUnitalCommSemiring [s : NonUni
 /-- A commutative ring is a ring with commutative multiplication. -/
 class CommRing (α : Type u) extends Ring α, CommMonoid α
 
+attribute [instance 1100] CommRing.toRing
+
 instance (priority := 100) CommRing.toNonAssocCommRing [CommRing α] : NonAssocCommRing α where
 
 instance (priority := 100) CommRing.toCommSemiring [s : CommRing α] : CommSemiring α :=

Mathlib/Analysis/Calculus/FDeriv/Add.lean

@@ -133,7 +133,7 @@ lemma differentiableAt_smul_iff (c : R) [Invertible c] :
 `c` must be invertible, i.e. if `R` is a field. -/
 theorem fderiv_const_smul_of_invertible (c : R) [Invertible c] :
     fderiv 𝕜 (c • f) x = c • fderiv 𝕜 f x := by
-  simp [← fderivWithin_univ, fderivWithin_const_smul_of_invertible c uniqueDiffWithinAt_univ]
+  simpa [← fderivWithin_univ] using fderivWithin_const_smul_of_invertible c uniqueDiffWithinAt_univ
 
 end ConstSMul
 
@@ -178,7 +178,9 @@ typeclass. -/
 lemma fderiv_const_smul_field (c : R) : fderiv 𝕜 (c • f) = c • fderiv 𝕜 f := by
   simp_rw [← fderivWithin_univ]
   ext x
-  simp [fderivWithin_const_smul_field c uniqueDiffWithinAt_univ]
+  simp only [Pi.smul_apply, coe_smul']
+  rw [fderivWithin_const_smul_field c uniqueDiffWithinAt_univ]
+  exact smul_apply c (fderivWithin 𝕜 f Set.univ x) _
 
 @[deprecated (since := "2026-01-11")] alias fderiv_const_smul_of_field := fderiv_const_smul_field
 
@@ -595,7 +597,8 @@ theorem fderivWithin_neg (hxs : UniqueDiffWithinAt 𝕜 s x) :
 
 @[simp]
 theorem fderiv_fun_neg : fderiv 𝕜 (fun y => -f y) x = -fderiv 𝕜 f x := by
-  simp only [← fderivWithin_univ, fderivWithin_fun_neg uniqueDiffWithinAt_univ]
+  simp only [← fderivWithin_univ]
+  rw [fderivWithin_fun_neg uniqueDiffWithinAt_univ]
 
 /-- Version of `fderiv_neg` where the function is written `-f` instead of `fun y ↦ - f y`. -/
 theorem fderiv_neg : fderiv 𝕜 (-f) x = -fderiv 𝕜 f x :=
@@ -842,7 +845,8 @@ theorem fderivWithin_const_sub (hxs : UniqueDiffWithinAt 𝕜 s x) (c : F) :
   simp only [sub_eq_add_neg, fderivWithin_const_add, fderivWithin_fun_neg, hxs]
 
 theorem fderiv_const_sub (c : F) : fderiv 𝕜 (fun y => c - f y) x = -fderiv 𝕜 f x := by
-  simp only [← fderivWithin_univ, fderivWithin_const_sub uniqueDiffWithinAt_univ]
+  simp only [← fderivWithin_univ]
+  rw [fderivWithin_const_sub uniqueDiffWithinAt_univ]
 
 end Sub
 

Mathlib/Data/Nat/Choose/Vandermonde.lean

@@ -31,8 +31,8 @@ namespace Nat
 theorem add_choose_eq (m n k : ℕ) :
     (m + n).choose k = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 := by
   calc
-    (m + n).choose k = ((X + 1) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, cast_id]
-    _ = ((X + 1) ^ m * (X + 1) ^ n).coeff k := by rw [pow_add]
+    (m + n).choose k = ((X + 1 : ℕ[X]) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, cast_id]
+    _ = ((X + 1) ^ m * (X + 1 : ℕ[X]) ^ n).coeff k := by rw [pow_add]
     _ = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 := by
       rw [coeff_mul, Finset.sum_congr rfl]
       simp only [coeff_X_add_one_pow, cast_id, imp_true_iff]

Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean

@@ -124,7 +124,8 @@ theorem map_polynomial_aeval_of_nonempty [IsAlgClosed 𝕜] (a : A) (p : 𝕜[X]
 
 /-- A specialization of `spectrum.subset_polynomial_aeval` to monic monomials for convenience. -/
 theorem pow_image_subset (a : A) (n : ℕ) : (fun x => x ^ n) '' σ a ⊆ σ (a ^ n) := by
-  simpa only [eval_X_pow, aeval_X_pow] using subset_polynomial_aeval a (X ^ n : 𝕜[X])
+  have := subset_polynomial_aeval a (X ^ n : 𝕜[X])
+  simpa only [eval_X_pow, aeval_X_pow] using this
 
 theorem pow_mem_pow (a : A) (n : ℕ) {k : 𝕜} (hk : k ∈ σ a) : k ^ n ∈ σ (a ^ n) :=
   pow_image_subset a n ⟨k, ⟨hk, rfl⟩⟩
@@ -133,14 +134,15 @@ theorem pow_mem_pow (a : A) (n : ℕ) {k : 𝕜} (hk : k ∈ σ a) : k ^ n ∈ 
 convenience. -/
 theorem map_pow_of_pos [IsAlgClosed 𝕜] (a : A) {n : ℕ} (hn : 0 < n) :
     σ (a ^ n) = (· ^ n) '' σ a := by
-  simpa only [aeval_X_pow, eval_X_pow]
-    using map_polynomial_aeval_of_degree_pos a (X ^ n : 𝕜[X]) (by rwa [degree_X_pow, Nat.cast_pos])
+  have := map_polynomial_aeval_of_degree_pos a (X ^ n : 𝕜[X]) (by rwa [degree_X_pow, Nat.cast_pos])
+  simpa only [aeval_X_pow, eval_X_pow] using this
 
 /-- A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for
 convenience. -/
 theorem map_pow_of_nonempty [IsAlgClosed 𝕜] {a : A} (ha : (σ a).Nonempty) (n : ℕ) :
     σ (a ^ n) = (· ^ n) '' σ a := by
-  simpa only [aeval_X_pow, eval_X_pow] using map_polynomial_aeval_of_nonempty a (X ^ n) ha
+  have := map_polynomial_aeval_of_nonempty a (X ^ n) ha
+  simpa only [aeval_X_pow, eval_X_pow] using this
 
 variable (𝕜)
 

Mathlib/FieldTheory/SeparableClosure.lean

@@ -398,6 +398,7 @@ lemma exists_finset_maximalFor_isTranscendenceBasis_separableClosure
     · convert hs.isAlgebraic_field <;> simp [s]
   have : Module.Finite ((separableClosure (adjoin F (s : Set E)) E).restrictScalars F) E :=
     inferInstanceAs <| Module.Finite (separableClosure (adjoin F (s : Set E)) E) E
+  stop
   exact d.not_lt_argminOn _ ht (by apply finrank_lt_of_gt H)
 
 @[deprecated (since := "2025-12-08")]

Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean

@@ -101,6 +101,8 @@ lemma tensorCotangentSpace_tmul (t : T) (x : P.CotangentSpace) :
   simp [tensorCotangentSpace_tmul_tmul, CotangentSpace.map_tmul_eq_tmul_map,
     smul_tmul', Algebra.smul_def, RingHom.algebraMap_toAlgebra]
 
+-- #defeq_abuse in
+set_option backward.isDefEq.respectTransparency false in
 /-- If `T` is flat over `R`, there is a `T`-linear isomorphism
 `T ⊗[R] P.Cotangent ≃ₗ[T] (P.baseChange).Cotangent`. -/
 noncomputable def tensorCotangentOfFlat [Module.Flat R T] :
@@ -118,7 +120,7 @@ lemma tensorCotangentOfFlat_tmul [Module.Flat R T] (t : T) (x : P.Cotangent) :
   simp only [tensorCotangentOfFlat, LinearEquiv.trans_apply, AlgebraTensorModule.congr_tmul,
     LinearEquiv.refl_apply, LinearEquiv.restrictScalars_apply, cotangentEquivCotangentKer_apply,
     Cotangent.val_mk, Ideal.tensorCotangentEquiv_tmul, map_smul, Cotangent.map_mk,
-    Hom.toAlgHom_apply, Ideal.Cotangent.equivOfEq_toCotangent]
+    Hom.toAlgHom_apply] --, Ideal.Cotangent.equivOfEq_toCotangent]
   rfl
 
 /-- The canonical map `T ⊗[R] P.H1Cotangent →ₗ[T] (P.baseChange).H1Cotangent`. -/

Mathlib/RingTheory/Finiteness/Basic.lean

@@ -343,8 +343,9 @@ instance bot : Module.Finite R (⊥ : Submodule R M) := .of_fg fg_bot
 instance top [Module.Finite R M] : Module.Finite R (⊤ : Submodule R M) := .of_fg fg_top
 
 instance top_left [Module.Finite R M] : Module.Finite (⊤ : Subsemiring R) M :=
-  have : RingHomSurjective (Subsemiring.topEquiv (R := R)).symm.toRingHom :=
-    RingHomSurjective.instToRingHomRingEquiv Subsemiring.topEquiv.symm
+  have : RingHomSurjective (Subsemiring.topEquiv (R := R)).symm.toRingHom := {
+    is_surjective := Function.RightInverse.surjective (congrFun rfl)
+  }    -- RingHomSurjective.instToRingHomRingEquiv Subsemiring.topEquiv.symm
   of_surjective (σ := (Subsemiring.topEquiv (R := R)).symm.toRingHom)
       ⟨⟨id, fun _ _ ↦ rfl⟩, fun _ _ ↦ rfl⟩ Function.surjective_id
 

Mathlib/RingTheory/Polynomial/IsIntegral.lean

@@ -215,7 +215,9 @@ theorem MvPolynomial.isIntegral_iff_isIntegral_coeff.{w} {σ : Type w} {f : MvPo
         convert H.map ((rename Subtype.val).comp
           (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective)).toRingHom
         · exact RingHom.ext (by simp [MvPolynomial.killCompl_map])
-        · nth_rw 1 12 [← hg]; simp)) n (.of_fintype _)
+        · conv_lhs => rw [← hg]
+          conv_rhs => enter [2]; rw [← hg]
+          simp)) n (.of_fintype _)
     · rw [← hg, coeff_rename_eq_zero _ _ _ (by grind)]
       exact isIntegral_zero
   revert f n

Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean

@@ -272,6 +272,9 @@ private lemma induction_structure (n : ℕ)
         Ideal.Quotient.mk_singleton_self, ne_eq, not_true_eq_false, false_or] at h_eq
       exact hi h_eq
 
+attribute [local instance 1000] Ring.toSemiring
+attribute [local instance 1000] CommSemiring.toSemiring
+
 -- TODO: fix non-terminal simp (large simp set)
 set_option linter.flexible false in
 open IsLocalization in

Mathlib/Topology/Algebra/Polynomial.lean

@@ -151,7 +151,8 @@ theorem isClosedMap_eval [ProperSpace R] (p : R[X]) : IsClosedMap p.eval := by
 
 variable (R) in
 theorem _root_.isClosedMap_pow [ProperSpace R] (n : ℕ) : IsClosedMap fun x : R ↦ x ^ n := by
-  simpa [eval_X_pow] using (X ^ n).isClosedMap_eval
+  have := (X ^ n : R[X]).isClosedMap_eval
+  simpa [eval_X_pow] using this
 
 section Roots