case zero
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(Nat.zero ! • hasseDeriv Nat.zero) = ↑derivative^[Nat.zero]

case succ
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
⊢ ↑((succ k)! • hasseDeriv (succ k)) = ↑derivative^[succ k]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(k ! • hasseDeriv k) = ↑derivative^[k]
induction' k with k ih
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ coeff (↑((succ k)! • hasseDeriv (succ k)) f) n = coeff ((↑derivative^[succ k]) f) n
case succ
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
⊢ ↑((succ k)! • hasseDeriv (succ k)) = ↑derivative^[succ k]
ext (f n) : 2
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ coeff (↑((succ k)! • hasseDeriv (succ k)) f) n = coeff (↑derivative (↑(k ! • hasseDeriv k) f)) n
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ coeff (↑((succ k)! • hasseDeriv (succ k)) f) n = coeff ((↑derivative^[succ k]) f) n
rw [iterate_succ_apply', ← ih]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ (succ k)! • (↑(choose (n + succ k) (succ k)) * coeff f (n + succ k)) =
    k ! • (↑(choose (n + 1 + k) (n + 1)) * coeff f (n + 1 + k) * (↑n + 1))
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ coeff (↑((succ k)! • hasseDeriv (succ k)) f) n = coeff (↑derivative (↑(k ! • hasseDeriv k) f)) n
simp only [LinearMap.smul_apply, coeff_smul, LinearMap.map_smul_of_tower, coeff_derivative,
  hasseDeriv_coeff, ← @choose_symm_add _ k]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑(choose (n + k + 1) (k + 1)) * coeff f (n + k + 1)) =
    ↑k ! * (↑(choose (n + k + 1) (n + 1)) * (coeff f (n + k + 1) * ↑(n + 1)))
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ (succ k)! • (↑(choose (n + succ k) (succ k)) * coeff f (n + succ k)) =
    k ! • (↑(choose (n + 1 + k) (n + 1)) * coeff f (n + 1 + k) * (↑n + 1))
simp only [nsmul_eq_mul, factorial_succ, mul_assoc, succ_eq_add_one, ← add_assoc,
  add_right_comm n 1 k, ← cast_succ]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑(choose (n + k + 1) (k + 1)) * coeff f (n + k + 1)) =
    ↑k ! * (↑(choose (n + k + 1) (n + 1)) * (↑(n + 1) * coeff f (n + k + 1)))
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑(choose (n + k + 1) (k + 1)) * coeff f (n + k + 1)) =
    ↑k ! * (↑(choose (n + k + 1) (n + 1)) * (coeff f (n + k + 1) * ↑(n + 1)))
rw [← (cast_commute (n + 1) (f.coeff (n + k + 1))).eq]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * ↑(choose (n + k + 1) (k + 1)) * coeff f (n + k + 1) =
    ↑k ! * ↑(choose (n + k + 1) (n + 1)) * ↑(n + 1) * coeff f (n + k + 1)
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑(choose (n + k + 1) (k + 1)) * coeff f (n + k + 1)) =
    ↑k ! * (↑(choose (n + k + 1) (n + 1)) * (↑(n + 1) * coeff f (n + k + 1)))
simp only [← mul_assoc]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k ! * choose (n + k + 1) (k + 1)) * coeff f (n + k + 1) =
    ↑(k ! * choose (n + k + 1) (n + 1) * (n + 1)) * coeff f (n + k + 1)
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * ↑(choose (n + k + 1) (k + 1)) * coeff f (n + k + 1) =
    ↑k ! * ↑(choose (n + k + 1) (n + 1)) * ↑(n + 1) * coeff f (n + k + 1)
norm_cast
case succ.h.a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * k ! * choose (n + k + 1) (k + 1) = k ! * choose (n + k + 1) (n + 1) * (n + 1)
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k ! * choose (n + k + 1) (k + 1)) * coeff f (n + k + 1) =
    ↑(k ! * choose (n + k + 1) (n + 1) * (n + 1)) * coeff f (n + k + 1)
congr 2
case succ.h.a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ k ! * ((k + 1) * choose (n + k + 1) (k + 1)) = k ! * (choose (n + k + 1) (n + 1) * (n + 1))
case succ.h.a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * k ! * choose (n + k + 1) (k + 1) = k ! * choose (n + k + 1) (n + 1) * (n + 1)
rw [mul_comm (k+1) _, mul_assoc, mul_assoc]
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * choose (n + k + 1) (k + 1) = choose (n + k + 1) (n + 1) * (n + 1)
case succ.h.a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ k ! * ((k + 1) * choose (n + k + 1) (k + 1)) = k ! * (choose (n + k + 1) (n + 1) * (n + 1))
congr 1
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (k + 1) * choose (n + k + 1) (k + 1) = choose (n + k + 1) (n + 1) * (n + 1)
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * choose (n + k + 1) (k + 1) = choose (n + k + 1) (n + 1) * (n + 1)
have : n + k + 1 = n + (k + 1) := by apply add_assoc
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ choose (n + k + 1) n * (k + 1) = choose (n + k + 1) n * (n + k + 1 - n)
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (k + 1) * choose (n + k + 1) (k + 1) = choose (n + k + 1) (n + 1) * (n + 1)
rw [←choose_symm_of_eq_add this, choose_succ_right_eq, mul_comm]
case succ.h.a.e_a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ k + 1 = n + k + 1 - n
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ choose (n + k + 1) n * (k + 1) = choose (n + k + 1) n * (n + k + 1 - n)
congr
no goals
case succ.h.a.e_a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ k + 1 = n + k + 1 - n
rw [add_assoc, add_tsub_cancel_left]
no goals
case zero
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(Nat.zero ! • hasseDeriv Nat.zero) = ↑derivative^[Nat.zero]
rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]
no goals
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = ↑derivative^[k]
f : R[X]
n : ℕ
⊢ n + k + 1 = n + (k + 1)
apply add_assoc