awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ (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])
    (∑ 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]
-- 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)
⊢ ∑ 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) +
      ∑ 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) =
    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)
have rw : ∑ 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)) =
  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)
Tactic: rw [add_comm, add_assoc]
-- 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)
rw :
  ∑ 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)) =
    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)
⊢ ∑ 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) +
      ∑ 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) =
    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)
have rw₁ : ∑ 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)) =
  ∑ 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))
Tactic: rw [add_comm, add_assoc]
-- 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)
⊢ 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 + 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)
Tactic: simp_rw [Nat.choose_succ_succ, Nat.succ_sub_succ, add_smul, sum_add_distrib]
-- 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)
⊢ 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 + 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]
-- 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)
⊢ ∑ 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) =
    ∑ k ∈ range n.succ.succ,
      n.succ.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n.succ - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
have rw : ∑ 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) =
  ∑ k ∈ range n.succ,
      n.succ.choose (k + 1) •
        ((⇑derivative : (a : R[X]) → R[X])^[n.succ - (k + 1)] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q) +
    n.succ.choose 0 • ((⇑derivative : (a : R[X]) → R[X])^[n.succ - 0] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)
Tactic: rw [sum_range_succ' _ n.succ, Nat.choose_zero_right, tsub_zero]
-- 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)
rw :
  ∑ 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) =
    ∑ k ∈ range n.succ,
        n.succ.choose (k + 1) •
          ((⇑derivative : (a : R[X]) → R[X])^[n.succ - (k + 1)] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q) +
      n.succ.choose 0 • ((⇑derivative : (a : R[X]) → R[X])^[n.succ - 0] 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) =
    ∑ k ∈ range n.succ.succ,
      n.succ.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n.succ - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
have rw₁ : ∑ 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) =
  ∑ k ∈ range n.succ,
      n.succ.choose (k + 1) •
        ((⇑derivative : (a : R[X]) → R[X])^[n.succ - (k + 1)] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q) +
    HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n.succ - 0] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)
Tactic: rw [sum_range_succ' _ n.succ, Nat.choose_zero_right, tsub_zero]
-- 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)
rw :
  ∑ 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) =
    ∑ k ∈ range n.succ,
        n.succ.choose (k + 1) •
          ((⇑derivative : (a : R[X]) → R[X])^[n.succ - (k + 1)] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q) +
      n.succ.choose 0 • ((⇑derivative : (a : R[X]) → R[X])^[n.succ - 0] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)
rw₁ :
  ∑ 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) =
    ∑ k ∈ range n.succ,
        n.succ.choose (k + 1) •
          ((⇑derivative : (a : R[X]) → R[X])^[n.succ - (k + 1)] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q) +
      HSMul.hSMul (α := ℕ) 1
        ((⇑derivative : (a : R[X]) → R[X])^[n.succ - 0] 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) =
    ∑ k ∈ range n.succ.succ,
      n.succ.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n.succ - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
have rw₂ : ∑ 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) =
  ∑ k ∈ range n.succ,
      n.succ.choose (k + 1) •
        ((⇑derivative : (a : R[X]) → R[X])^[n.succ - (k + 1)] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q) +
    HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n.succ] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)
Tactic: rw [sum_range_succ' _ n.succ, Nat.choose_zero_right, tsub_zero]
-- 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)
⊢ (⇑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)
have succ : 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)) =
  ∑ 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) +
    ∑ 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: 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]
-- 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)
⊢ 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)) =
    ∑ 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) +
      ∑ 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 succ : ∑ 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.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)
Tactic: congr
-- 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)
⊢ ∑ 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.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)
have succ : Eq.{u + 1} (α := R[X])
  (∑ k ∈ range n,
    n.choose (k + 1) •
      ((⇑derivative : (a : R[X]) → R[X])^[n - (k + 1) + 1] 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))
Tactic: refine (sum_range_succ' _ _).trans (congr_arg₂ (· + ·) ?_ ?_)