-- 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 :
  HAdd.hAdd (α := 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 + 1] q))
        (∑ k ∈ range n.succ,
          n.choose k.succ •
            ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q)) +
      HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q) =
    ∑ x ∈ range n.succ,
        (n.choose x + n.choose x.succ) •
          ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - (x + 1)] p * (⇑derivative : (a : R[X]) → R[X])^[x + 1] q) +
      HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)
simp_rw₁ :
  HAdd.hAdd (α := 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 + 1] q))
        (∑ k ∈ range n.succ,
          n.choose k.succ •
            ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q)) +
      HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q) =
    ∑ x ∈ range n.succ,
        (n.choose x + n.choose x.succ) •
          ((⇑derivative : (a : R[X]) → R[X])^[n - x] p * (⇑derivative : (a : R[X]) → R[X])^[x + 1] q) +
      HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)
⊢ HAdd.hAdd (α := 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 + 1] q))
        (∑ k ∈ range n.succ,
          n.choose k.succ •
            ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q)) +
      HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q) =
    ∑ i ∈ range n.succ,
        (n + 1).choose (i + 1) •
          ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - (i + 1)] p * (⇑derivative : (a : R[X]) → R[X])^[i + 1] q) +
      HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)
have simp_rw₂ : HAdd.hAdd (α := 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 + 1] q))
      (∑ k ∈ range n.succ,
        n.choose k.succ • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q)) +
    HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q) =
  ∑ x ∈ range n.succ,
      (n.choose x • ((⇑derivative : (a : R[X]) → R[X])^[n - x] p * (⇑derivative : (a : R[X]) → R[X])^[x + 1] q) +
        n.choose x.succ • ((⇑derivative : (a : R[X]) → R[X])^[n - x] p * (⇑derivative : (a : R[X]) → R[X])^[x + 1] q)) +
    HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)
Tactic: simp_rw [Nat.choose_succ_succ, Nat.succ_sub_succ, add_smul, sum_add_distrib]