case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ ∀ (m : ℕ), coeff ((↑derivative^[Nat.zero]) p) m = (∏ i in range Nat.zero, (m + Nat.zero - i)) • coeff p (m + Nat.zero)

case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
⊢ ∀ (m : ℕ),
    coeff ((↑derivative^[Nat.succ k]) p) m =
      (∏ i in range (Nat.succ k), (m + Nat.succ k - i)) • coeff p (m + Nat.succ k)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
k : ℕ
p : R[X]
⊢ ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
induction' k with k ih
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
m : ℕ
⊢ coeff ((↑derivative^[Nat.succ k]) p) m = (∏ i in range (Nat.succ k), (m + Nat.succ k - i)) • coeff p (m + Nat.succ k)
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
⊢ ∀ (m : ℕ),
    coeff ((↑derivative^[Nat.succ k]) p) m =
      (∏ i in range (Nat.succ k), (m + Nat.succ k - i)) • coeff p (m + Nat.succ k)
intro m
no goals
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
m : ℕ
⊢ coeff ((↑derivative^[Nat.succ k]) p) m = (∏ i in range (Nat.succ k), (m + Nat.succ k - i)) • coeff p (m + Nat.succ k)
calc
  ((derivative^[k + 1]) p).coeff m =
      (∏ i in range k, (m + k.succ - i)) • p.coeff (m + k.succ) * (m + 1) :=
    by rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
  _ = ((∏ i in range k, (m + k.succ - i)) * (m + 1)) • p.coeff (m + k.succ) := by
    rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul, mul_comm]
  _ = (∏ i in range k.succ, (m + k.succ - i)) • p.coeff (m + k.succ) := by
    rw [prod_range_succ, add_tsub_assoc_of_le k.le_succ, Nat.succ_sub le_rfl, tsub_self]
no goals
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ ∀ (m : ℕ), coeff ((↑derivative^[Nat.zero]) p) m = (∏ i in range Nat.zero, (m + Nat.zero - i)) • coeff p (m + Nat.zero)
simp
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
m : ℕ
⊢ coeff ((↑derivative^[k + 1]) p) m = (∏ i in range k, (m + Nat.succ k - i)) • coeff p (m + Nat.succ k) * (↑m + 1)
rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
m : ℕ
⊢ (∏ i in range k, (m + Nat.succ k - i)) • coeff p (m + Nat.succ k) * (↑m + 1) =
    ((∏ i in range k, (m + Nat.succ k - i)) * (m + 1)) • coeff p (m + Nat.succ k)
rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul, mul_comm]
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
m : ℕ
⊢ ((∏ i in range k, (m + Nat.succ k - i)) * (m + 1)) • coeff p (m + Nat.succ k) =
    (∏ i in range (Nat.succ k), (m + Nat.succ k - i)) • coeff p (m + Nat.succ k)
rw [prod_range_succ, add_tsub_assoc_of_le k.le_succ, Nat.succ_sub le_rfl, tsub_self]