no goals
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ ↑(pderiv i) (f * g) = ↑(pderiv i) f * g + f * ↑(pderiv i) g
simp only [(pderiv i).leibniz f g, smul_eq_mul, mul_comm, add_comm]