chore(MvPolynomial/PDeriv): remove superfluous use of DecidableEq (#1…

…7504) Found by the linter in #10235.
leanprover-community · Oct 7, 2024 · 04198c1 · 04198c1
1 parent 3cd9755
commit 04198c1
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/Mathlib/Algebra/MvPolynomial/PDeriv.lean b/Mathlib/Algebra/MvPolynomial/PDeriv.lean
@@ -115,13 +115,14 @@ theorem pderiv_map {S} [CommSemiring S] {φ : R →+* S} {f : MvPolynomial σ R}
   · simp [eq]
   · simp [eq, h]
 
-lemma pderiv_rename {τ : Type*} [DecidableEq τ] [DecidableEq σ] {f : σ → τ}
+lemma pderiv_rename {τ : Type*} [DecidableEq τ] {f : σ → τ}
     (hf : Function.Injective f) (x : σ) (p : MvPolynomial σ R) :
     pderiv (f x) (rename f p) = rename f (pderiv x p) := by
   induction' p using MvPolynomial.induction_on with a p q hp hq p a h
   · simp
   · simp [hp, hq]
-  · simp only [map_mul, MvPolynomial.rename_X, Derivation.leibniz, MvPolynomial.pderiv_X,
+  · classical
+    simp only [map_mul, MvPolynomial.rename_X, Derivation.leibniz, MvPolynomial.pderiv_X,
       Pi.single_apply, hf.eq_iff, smul_eq_mul, mul_ite, mul_one, mul_zero, h, map_add, add_left_inj]
     split_ifs <;> simp