-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
zero :
  (⇑derivative : (a : R[X]) → R[X])^[0] (p * q) =
    ∑ k ∈ range (Nat.succ 0),
      Nat.choose 0 k • ((⇑derivative : (a : R[X]) → R[X])^[0 - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
succ :
  ∀ (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)),
    (⇑derivative : (a : R[X]) → R[X])^[n + 1] (p * q) =
      ∑ k ∈ range (n + 1).succ,
        (n + 1).choose k • ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
⊢ (⇑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)

Tactic:
induction n with
  | zero =>
    simp [Finset.range]
  | succ n IH =>
    calc
      derivative^[n + 1] (p * q) =
          derivative (∑ k ∈ range n.succ,
              n.choose k • (derivative^[n - k] p * derivative^[k] q)) := by
        rw [Function.iterate_succ_apply', IH]
      _ = (∑ k ∈ range n.succ,
            n.choose k • (derivative^[n - k + 1] p * derivative^[k] q)) +
          ∑ k ∈ range n.succ,
            n.choose k • (derivative^[n - k] p * derivative^[k + 1] q) := by
        simp_rw [derivative_sum, derivative_smul, derivative_mul, Function.iterate_succ_apply',
          smul_add, sum_add_distrib]
      _ = (∑ k ∈ range n.succ,
                n.choose k.succ • (derivative^[n - k] p * derivative^[k + 1] q)) +
              1 • (derivative^[n + 1] p * derivative^[0] q) +
            ∑ k ∈ range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k + 1] q) :=
        ?_
      _ = ((∑ k ∈ range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k + 1] q)) +
              ∑ k ∈ range n.succ,
                n.choose k.succ • (derivative^[n - k] p * derivative^[k + 1] q)) +
            1 • (derivative^[n + 1] p * derivative^[0] q) := by
        rw [add_comm, add_assoc]
      _ = (∑ i ∈ range n.succ,
              (n + 1).choose (i + 1) • (derivative^[n + 1 - (i + 1)] p * derivative^[i + 1] q)) +
            1 • (derivative^[n + 1] p * derivative^[0] q) := by
        simp_rw [Nat.choose_succ_succ, Nat.succ_sub_succ, add_smul, sum_add_distrib]
      _ = ∑ k ∈ range n.succ.succ,
            n.succ.choose k • (derivative^[n.succ - k] p * derivative^[k] q) := by
        rw [sum_range_succ' _ n.succ, Nat.choose_zero_right, tsub_zero]
    congr
    refine (sum_range_succ' _ _).trans (congr_arg₂ (· + ·) ?_ ?_)
    · rw [sum_range_succ, Nat.choose_succ_self, zero_smul, add_zero]
      refine sum_congr rfl fun k hk => ?_
      rw [mem_range] at hk
      congr
      lia
    · rw [Nat.choose_zero_right, tsub_zero]

Premises used: Polynomial.derivative, Nat.choose, HMul.hMul, HSub.hSub, Finset.mem_range, Nat.iterate, tsub_zero, Finset.range, zero_smul, HAdd.hAdd, HSMul.hSMul, add_zero, OfNat.ofNat, Nat.choose_succ_self, Nat.succ, DFunLike.coe, Finset.sum_range_succ', Finset.sum_range_succ, Finset.sum_congr, Finset.sum, Nat.choose_zero_right, rfl, Eq.trans, congr_arg₂