awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
rw rw₁ :
  (m + k.succ).descFactorial k.succ • p.coeff (m + k.succ) = (m + k.succ).descFactorial k.succ • p.coeff (m + k.succ)
⊢ (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ) = (m + k.succ).descFactorial k.succ • p.coeff (m + k.succ)

Tactic:
rw [Nat.succ_add_eq_add_succ]

Premises used: Nat.succ_add_eq_add_succ
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
_ :
  ((⇑derivative : (a : R[X]) → R[X])^[k + 1] p).coeff m =
    (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
_₁ :
  (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1 =
    ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)
_₂ :
  ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ) =
    (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ)
_₃ : (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ) = (m + k.succ).descFactorial k.succ • p.coeff (m + k.succ)
⊢ ((⇑derivative : (a : R[X]) → R[X])^[k + 1] p).coeff m = (m + (k + 1)).descFactorial (k + 1) • p.coeff (m + (k + 1))

Tactic:
calc
        (derivative^[k + 1] p).coeff m
        _ = Nat.descFactorial (Nat.succ (m + k)) k • p.coeff (m + k.succ) * (m + 1) := by
          rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
        _ = ((m + 1) * Nat.descFactorial (Nat.succ (m + k)) k) • p.coeff (m + k.succ) := by
          rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]
        _ = Nat.descFactorial (m.succ + k) k.succ • p.coeff (m + k.succ) := by
          rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
        _ = Nat.descFactorial (m + k.succ) k.succ • p.coeff (m + k.succ) := by
          rw [Nat.succ_add_eq_add_succ]

Premises used: Polynomial.derivative, HMul.hMul, Nat.iterate, Polynomial.coeff, HAdd.hAdd, OfNat.ofNat, Nat.succ, DFunLike.coe, Nat.descFactorial
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
k : ℕ
p : R[X]
m : ℕ
zero : ∀ (m : ℕ), ((⇑derivative : (a : R[X]) → R[X])^[0] p).coeff m = (m + 0).descFactorial 0 • p.coeff (m + 0)
succ :
  ∀ (k : ℕ)
    (ih : ∀ (m : ℕ), ((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k))
    (m : ℕ),
    ((⇑derivative : (a : R[X]) → R[X])^[k + 1] p).coeff m = (m + (k + 1)).descFactorial (k + 1) • p.coeff (m + (k + 1))
⊢ ((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)

Tactic:
induction k generalizing m with
  | zero => simp
  | succ k ih =>
      calc
        (derivative^[k + 1] p).coeff m
        _ = Nat.descFactorial (Nat.succ (m + k)) k • p.coeff (m + k.succ) * (m + 1) := by
          rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
        _ = ((m + 1) * Nat.descFactorial (Nat.succ (m + k)) k) • p.coeff (m + k.succ) := by
          rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]
        _ = Nat.descFactorial (m.succ + k) k.succ • p.coeff (m + k.succ) := by
          rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
        _ = Nat.descFactorial (m + k.succ) k.succ • p.coeff (m + k.succ) := by
          rw [Nat.succ_add_eq_add_succ]

Premises used: Polynomial.derivative, HMul.hMul, Nat.iterate, Polynomial.coeff, HAdd.hAdd, OfNat.ofNat, Nat.succ, DFunLike.coe, Nat.descFactorial
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
rw :
  ∑ i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff i) : R[X])
      (HPow.hPow (α := R[X]) X i)
| (⇑derivative : (a : R[X]) → R[X])^[k] p

Tactic:
rw [(derivative^[k] p).as_sum_support_C_mul_X_pow]

Premises used: Polynomial.derivative, Polynomial.as_sum_support_C_mul_X_pow, Nat.iterate, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
conv_lhs :
  Eq.{u + 1} (α := R[X])
    (∑ i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff i) : R[X])
        (HPow.hPow (α := R[X]) X i))
    (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x))
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] p =
    ∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x)

Tactic:
conv_lhs => rw [(derivative^[k] p).as_sum_support_C_mul_X_pow]

Premises used: Polynomial.derivative, Polynomial.as_sum_support_C_mul_X_pow, Nat.iterate, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
⊢ Eq.{u + 1} (α := R[X])
    (∑ i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff i) : R[X])
        (HPow.hPow (α := R[X]) X i))
    (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x))

Tactic:
sum_congr rfl fun i _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
refine :
  ∀ i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff i) : R[X])
        (HPow.hPow (α := R[X]) X i) =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
        (HPow.hPow (α := R[X]) X i)
⊢ Eq.{u + 1} (α := R[X])
    (∑ i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff i) : R[X])
        (HPow.hPow (α := R[X]) X i))
    (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x))

Tactic:
refine sum_congr rfl fun i _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k i : ℕ
h : i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i)
rw₁ rw₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((k ! * (i + k).choose k) • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((k ! * (i + k).choose k) • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i)
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff i) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i)

Tactic:
rw [coeff_iterate_derivative, Nat.descFactorial_eq_factorial_mul_choose]

Premises used: Polynomial.coeff_iterate_derivative, Nat.descFactorial_eq_factorial_mul_choose
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
rw :
  ∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
      (HPow.hPow (α := R[X]) X x)
| (⇑derivative : (a : R[X]) → R[X])^[k] p

Tactic:
rw [iterate_derivative_eq_sum]

Premises used: Polynomial.iterate_derivative_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
conv_lhs :
  ∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x) =
    HSMul.hSMul (β := R[X]) k !
      (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).choose k • p.coeff (x + k)) : R[X])
          (HPow.hPow (α := R[X]) X x))
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] p =
    HSMul.hSMul (β := R[X]) k !
      (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).choose k • p.coeff (x + k)) : R[X])
          (HPow.hPow (α := R[X]) X x))

Tactic:
conv_lhs => rw [iterate_derivative_eq_sum]

Premises used: Polynomial.iterate_derivative_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
rw :
  Eq.{u + 1} (α := R[X])
    (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x))
    (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      k ! •
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).choose k • p.coeff (x + k)) : R[X])
          (HPow.hPow (α := R[X]) X x))
⊢ ∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x) =
    HSMul.hSMul (β := R[X]) k !
      (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).choose k • p.coeff (x + k)) : R[X])
          (HPow.hPow (α := R[X]) X x))

Tactic:
rw [smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
⊢ Eq.{u + 1} (α := R[X])
    (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x))
    (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      k ! •
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).choose k • p.coeff (x + k)) : R[X])
          (HPow.hPow (α := R[X]) X x))

Tactic:
sum_congr rfl fun i _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
refine :
  ∀ i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
        (HPow.hPow (α := R[X]) X i) =
      k ! •
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X])
          (HPow.hPow (α := R[X]) X i)
⊢ Eq.{u + 1} (α := R[X])
    (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x))
    (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      k ! •
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).choose k • p.coeff (x + k)) : R[X])
          (HPow.hPow (α := R[X]) X x))

Tactic:
refine sum_congr rfl fun i _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k i : ℕ
h : i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HSMul.hSMul (β := R[X]) k ! ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X]) *
      HPow.hPow (α := R[X]) X i
rw₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (k ! • (i + k).choose k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i)
rw₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((k ! * (i + k).choose k) • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i)
rw₃ rw₄ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((k ! * (i + k).choose k) • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((k ! * (i + k).choose k) • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i)
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    k ! •
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X])
        (HPow.hPow (α := R[X]) X i)

Tactic:
rw [← smul_mul_assoc, smul_C, smul_smul, Nat.descFactorial_eq_factorial_mul_choose]

Premises used: smul_smul, smul_mul_assoc, Polynomial.smul_C, Nat.descFactorial_eq_factorial_mul_choose
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ (⇑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)

Tactic:
simp [Finset.range]

Premises used: Finset.range
-- 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)
rw :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n] (p * 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)) :
      R[X])
rw₁ rw₂ :
  Eq.{u + 1} (α := 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)))
    ((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)))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1] (p * 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))

Tactic:
rw [Function.iterate_succ_apply', IH]

Premises used: Function.iterate_succ_apply'
-- 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)
⊢ 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:
?_
-- 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)
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)
rw₁ 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))
⊢ ∑ 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)

Tactic:
rw [add_comm, add_assoc]

Premises used: add_assoc, add_comm
-- 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)
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)
rw₂ 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)
⊢ ∑ 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)

Tactic:
rw [sum_range_succ' _ n.succ, Nat.choose_zero_right, tsub_zero]

Premises used: tsub_zero, Nat.succ, Finset.sum_range_succ', Nat.choose_zero_right