-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
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))
⊢ (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))
have 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]))
Tactic: simp_rw [derivative_sum, derivative_smul, derivative_mul, Function.iterate_succ_apply',
          smul_add, sum_add_distrib]