-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_mul {n} (p q : R[X]) :
    derivative^[n] (p * q) =
      ∑ k ∈ range n.succ, (n.choose k • (derivative^[n - k] p * derivative^[k] q))

Proof state:
case zero
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (⇑derivative)^[0] (p * q) = ∑ k ∈ range (Nat.succ 0), Nat.choose 0 k • ((⇑derivative)^[0 - k] p * (⇑derivative)^[k] q)

Tactic:
simp [Finset.range]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ 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) =
    ∑ 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)

Tactic:
congr

Result:
case succ.e_a
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k + 1] p * (⇑derivative)^[k] 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)

Proof state:
case succ.e_a.refine_1.e_a.e_a.e_a
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
k : ℕ
hk : k < n
⊢ n - (k + 1) + 1 = n - k

Tactic:
omega

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] 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) +
      ∑ 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)

Tactic:
rw [add_comm, add_assoc]

Result:
no goals

Proof state:
case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n, n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    ∑ x ∈ range n, n.choose x.succ • ((⇑derivative)^[n - x] p * (⇑derivative)^[x + 1] q)

Tactic:
refine sum_congr rfl fun k hk => ?_

Result:
case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
k : ℕ
hk : k ∈ range n
⊢ n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)

Proof state:
case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n, n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)

Tactic:
rw [sum_range_succ, Nat.choose_succ_self, zero_smul, add_zero]

Result:
case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n, n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    ∑ x ∈ range n, n.choose x.succ • ((⇑derivative)^[n - x] p * (⇑derivative)^[x + 1] q)

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ (⇑derivative)^[n + 1] (p * q) =
    ∑ k ∈ range (n + 1).succ, (n + 1).choose k • ((⇑derivative)^[n + 1 - k] p * (⇑derivative)^[k] 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]

Result:
case succ
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ 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) =
    ∑ 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)

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ 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) =
    ∑ k ∈ range n.succ.succ, n.succ.choose k • ((⇑derivative)^[n.succ - k] p * (⇑derivative)^[k] q)

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

Result:
no goals

Proof state:
case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
k : ℕ
hk : k < n
⊢ n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)

Tactic:
congr

Result:
case succ.e_a.refine_1.e_a.e_a.e_a
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
k : ℕ
hk : k < n
⊢ n - (k + 1) + 1 = n - k