-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
IH :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * q) =
    ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
simp_rw :
  ∑ b ∈ range n.succ,
      (derivative : (a : R[X]) → R[X])
        (n.choose b • ((⇑derivative : (a : R[X]) → R[X])^[n - b] p * (⇑derivative : (a : R[X]) → R[X])^[b] q)) =
    HAdd.hAdd (α := R[X])
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q))
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
simp_rw₁ :
  ∑ x ∈ range n.succ,
      HSMul.hSMul (β := R[X]) (n.choose x)
        ((derivative : (a : R[X]) → R[X])
            ((⇑derivative : (a : R[X]) → R[X])^[n - x] p * (⇑derivative : (a : R[X]) → R[X])^[x] q) :
          R[X]) =
    HAdd.hAdd (α := R[X])
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q))
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
simp_rw₂ :
  ∑ x ∈ range n.succ,
      n.choose x •
        (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - x] p) : R[X])
            ((⇑derivative : (a : R[X]) → R[X])^[x] q) +
          HMul.hMul (β := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - x] p)
            ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[x] q) : R[X])) =
    HAdd.hAdd (α := R[X])
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q))
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
simp_rw₃ :
  ∑ x ∈ range n.succ,
      n.choose x •
        (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - x] p) : R[X])
            ((⇑derivative : (a : R[X]) → R[X])^[x] q) +
          HMul.hMul (β := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - x] p)
            ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[x] q) : R[X])) =
    HAdd.hAdd (α := R[X])
      (∑ x ∈ range n.succ,
        n.choose x •
          HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - x] p) : R[X])
            ((⇑derivative : (a : R[X]) → R[X])^[x] q))
      (∑ x ∈ range n.succ,
        n.choose x •
          HMul.hMul (β := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - x] p)
            ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[x] q) : R[X]))
simp_rw₄ :
  ∑ x ∈ range n.succ,
      (n.choose x •
          HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - x] p) : R[X])
            ((⇑derivative : (a : R[X]) → R[X])^[x] q) +
        n.choose x •
          HMul.hMul (β := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - x] p)
            ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[x] q) : R[X])) =
    HAdd.hAdd (α := R[X])
      (∑ x ∈ range n.succ,
        n.choose x •
          HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - x] p) : R[X])
            ((⇑derivative : (a : R[X]) → R[X])^[x] q))
      (∑ x ∈ range n.succ,
        n.choose x •
          HMul.hMul (β := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - x] p)
            ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[x] q) : R[X]))
⊢ (derivative : (a : R[X]) → R[X])
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)) =
    HAdd.hAdd (α := R[X])
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q))
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))

Tactic:
simp_rw [derivative_sum, derivative_smul, derivative_mul, Function.iterate_succ_apply',
          smul_add, sum_add_distrib]

Premises used: Function.iterate_succ_apply', Polynomial.derivative_mul, Polynomial.derivative_sum, Polynomial.derivative_smul, Finset.sum_add_distrib, smul_add