-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem coeff_iterate_derivative {k} (p : R[X]) (m : ℕ) :
    (derivative^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ ((⇑derivative)^[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]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
k : ℕ
p : R[X]
m : ℕ
⊢ ((⇑derivative)^[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]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ (m + k).succ.descFactorial k • p.coeff (m + k.succ) * (↑m + 1) =
    ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)

Tactic:
rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ) =
    (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ)

Tactic:
rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ ((⇑derivative)^[k + 1] p).coeff m = (m + k).succ.descFactorial k • p.coeff (m + k.succ) * (↑m + 1)

Tactic:
rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ (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]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
m : ℕ
⊢ ((⇑derivative)^[0] p).coeff m = (m + 0).descFactorial 0 • p.coeff (m + 0)

Tactic:
simp

Result:
no goals