awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
f : MvPolynomial σ R
n : ℕ
rw :
  n •
      HSMul.hSMul (β := MvPolynomial σ R) (f ^ (n - 1))
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
rw₁ :
  (↑n : MvPolynomial σ R) *
      HSMul.hSMul (β := MvPolynomial σ R) (f ^ (n - 1))
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
rw₂ :
  (↑n : MvPolynomial σ R) *
      HMul.hMul (β := MvPolynomial σ R) (f ^ (n - 1))
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
rw₃ rw₄ :
  (↑n : MvPolynomial σ R) *
      HMul.hMul (β := MvPolynomial σ R) (f ^ (n - 1))
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
    (↑n : MvPolynomial σ R) *
      HMul.hMul (β := MvPolynomial σ R) (f ^ (n - 1))
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (f ^ n) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
rw [(pderiv i).leibniz_pow f n, nsmul_eq_mul, smul_eq_mul, mul_assoc]

Premises used: mul_assoc, MvPolynomial.pderiv, Derivation.leibniz_pow, nsmul_eq_mul, smul_eq_mul
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
a : R
inst : CommSemiring R
f : MvPolynomial σ R
i : σ
rw :
  (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (a • f) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
rw₁ :
  HSMul.hSMul (β := MvPolynomial σ R) a ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
rw₂ rw₃ :
  HSMul.hSMul (β := MvPolynomial σ R) a ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
    HSMul.hSMul (β := MvPolynomial σ R) a ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
rw [C_mul', Derivation.map_smul, C_mul']

Premises used: MvPolynomial.C_mul', Derivation.map_smul
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
S : Type u_1
inst_1 : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
r : R
⊢ Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) ((C : (a : R) → MvPolynomial σ R) r)) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r)) :
      MvPolynomial σ S)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
S : Type u_1
inst_1 : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p q : MvPolynomial σ R
hp :
  Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S) ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial σ S)
hq :
  Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S) ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) q) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) q) :
      MvPolynomial σ S)
⊢ Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) (p + q)) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q)) :
      MvPolynomial σ S)

Tactic:
simp [hp, hq]
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
S : Type u_1
inst_1 : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
apply :
  ∀ (p : MvPolynomial σ R) (j : σ)
    (eq :
      Eq (α := MvPolynomial σ S)
        ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S)
            ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
          MvPolynomial σ S)
        ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
            ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial σ S)),
    Eq (α := MvPolynomial σ S)
      ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S)
          ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) (p * X j)) :
        MvPolynomial σ S)
      ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X j)) :
        MvPolynomial σ S)
⊢ Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S) ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) f) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ S)

Tactic:
apply induction_on f (fun r ↦ by simp) (fun p q hp hq ↦ by simp [hp, hq]) fun p j eq ↦ ?_

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
S : Type u_1
inst_1 : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p : MvPolynomial σ R
j : σ
eq :
  Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S) ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial σ S)
inl :
  ∀
    (eq :
      Eq (α := MvPolynomial σ S)
        ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
            ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
          MvPolynomial σ S)
        ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
            ((pderiv j : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial σ S)),
    Eq (α := MvPolynomial σ S)
      ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
          ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) (p * X j)) :
        MvPolynomial σ S)
      ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
          ((pderiv j : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X j)) :
        MvPolynomial σ S)
inr :
  ∀ (h : j ≠ i),
    Eq (α := MvPolynomial σ S)
      ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S)
          ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) (p * X j)) :
        MvPolynomial σ S)
      ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X j)) :
        MvPolynomial σ S)
⊢ Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) (p * X j)) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X j)) :
      MvPolynomial σ S)

Tactic:
obtain rfl | h := eq_or_ne j i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
S : Type u_1
inst_1 : CommSemiring S
φ : R →+* S
f p : MvPolynomial σ R
j : σ
eq :
  Eq (α := MvPolynomial σ S)
    ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S) ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) ((pderiv j : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial σ S)
⊢ Eq (α := MvPolynomial σ S)
    ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) (p * X j)) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((pderiv j : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X j)) :
      MvPolynomial σ S)

Tactic:
simp [eq]
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
S : Type u_1
inst_1 : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p : MvPolynomial σ R
j : σ
eq :
  Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S) ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial σ S)
h : j ≠ i
⊢ Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) (p * X j)) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X j)) :
      MvPolynomial σ S)

Tactic:
simp [eq, h]
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
a : R
⊢ Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial τ R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p q : MvPolynomial σ R
hp :
  Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
hq :
  Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) q) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q) :
      MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q)) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q)) :
      MvPolynomial τ R)

Tactic:
simp [hp, hq]
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h :
  Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
mul_X :
  HAdd.hAdd (α := MvPolynomial τ R)
      (if a = x then (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p else 0 : MvPolynomial τ R)
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R)) =
    HAdd.hAdd (α := MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (if a = x then p else 0) : MvPolynomial τ R)
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R))
⊢ Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p * X a)) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X a)) :
      MvPolynomial τ R)

Tactic:
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]

Premises used: Pi.single_apply, Function.Injective.eq_iff, mul_ite, MvPolynomial.pderiv_X, map_add, MulZeroClass.mul_zero, Derivation.leibniz, map_mul, MvPolynomial.rename_X, smul_eq_mul, mul_one
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h :
  Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
pos :
  a = x →
    HAdd.hAdd (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
        (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
              ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
            MvPolynomial τ R)) =
      HAdd.hAdd (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
        (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
              ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
            MvPolynomial τ R))
neg :
  ¬a = x →
    0 +
        HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
              ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
            MvPolynomial τ R) =
      (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) 0 +
        HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
              ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
            MvPolynomial τ R)
⊢ HAdd.hAdd (α := MvPolynomial τ R)
      (if a = x then (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p else 0 : MvPolynomial τ R)
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R)) =
    HAdd.hAdd (α := MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (if a = x then p else 0) : MvPolynomial τ R)
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R))

Tactic:
split_ifs
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h :
  Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
h_1 : a = x
⊢ HAdd.hAdd (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R)) =
    HAdd.hAdd (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h :
  Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
h_1 : ¬a = x
⊢ 0 +
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R) =
    (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) 0 +
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
S : Type u_1
τ : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
f : τ → S
j : σ
a : R
⊢ Eq (α := MvPolynomial σ S)
    ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
        ((pderiv (Sum.inl j) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial (σ ⊕ τ) R)
          ((C : (a : R) → MvPolynomial (σ ⊕ τ) R) a)) :
      MvPolynomial σ S)
    ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
          ((C : (a : R) → MvPolynomial (σ ⊕ τ) R) a)) :
      MvPolynomial σ S)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
S : Type u_1
τ : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
f : τ → S
j : σ
p q : MvPolynomial (σ ⊕ τ) R
hp :
  Eq (α := MvPolynomial σ S)
    ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
        ((pderiv (Sum.inl j) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial (σ ⊕ τ) R) p) :
      MvPolynomial σ S)
    ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
          p) :
      MvPolynomial σ S)
hq :
  Eq (α := MvPolynomial σ S)
    ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
        ((pderiv (Sum.inl j) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial (σ ⊕ τ) R) q) :
      MvPolynomial σ S)
    ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
          q) :
      MvPolynomial σ S)
⊢ Eq (α := MvPolynomial σ S)
    ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
        ((pderiv (Sum.inl j) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial (σ ⊕ τ) R) (p + q)) :
      MvPolynomial σ S)
    ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
          (p + q)) :
      MvPolynomial σ S)

Tactic:
simp [hp, hq]