-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem factorial_smul_hasseDeriv : ⇑(k ! • @hasseDeriv R _ k) = (@derivative R _)^[k]

Proof state:
case succ.h.a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * k ! * (n + k + 1).choose (k + 1) = k ! * (n + k + 1).choose (n + 1) * (n + 1)

Tactic:
rw [mul_comm (k+1) _, mul_assoc, mul_assoc]

Result:
case succ.h.a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ k ! * ((k + 1) * (n + k + 1).choose (k + 1)) = k ! * ((n + k + 1).choose (n + 1) * (n + 1))

Proof state:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (((k + 1)! • hasseDeriv (k + 1)) f).coeff n = ((⇑derivative)^[k + 1] f).coeff n

Tactic:
rw [iterate_succ_apply', ← ih]

Result:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (((k + 1)! • hasseDeriv (k + 1)) f).coeff n = (derivative ((k ! • hasseDeriv k) f)).coeff n

Proof state:
case succ.h.a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ k ! * ((k + 1) * (n + k + 1).choose (k + 1)) = k ! * ((n + k + 1).choose (n + 1) * (n + 1))

Tactic:
congr 1

Result:
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * (n + k + 1).choose (k + 1) = (n + k + 1).choose (n + 1) * (n + 1)

Proof state:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1)) =
    ↑k ! * (↑((n + k + 1).choose (n + 1)) * (f.coeff (n + k + 1) * ↑(n + 1)))

Tactic:
rw [← (cast_commute (n + 1) (f.coeff (n + k + 1))).eq]

Result:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1)) =
    ↑k ! * (↑((n + k + 1).choose (n + 1)) * (↑(n + 1) * f.coeff (n + k + 1)))

Proof state:
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (k + 1) * (n + k + 1).choose (k + 1) = (n + k + 1).choose (n + 1) * (n + 1)

Tactic:
rw [← choose_symm_of_eq_add this, choose_succ_right_eq, mul_comm]

Result:
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (n + k + 1).choose n * (k + 1) = (n + k + 1).choose n * (n + k + 1 - n)

Proof state:
case succ.h.a.e_a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ k + 1 = n + k + 1 - n

Tactic:
rw [add_assoc, add_tsub_cancel_left]

Result:
no goals

Proof state:
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (n + k + 1).choose n * (k + 1) = (n + k + 1).choose n * (n + k + 1 - n)

Tactic:
congr

Result:
case succ.h.a.e_a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ k + 1 = n + k + 1 - n

Proof state:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1)) =
    ↑k ! * (↑((n + k + 1).choose (n + 1)) * (↑(n + 1) * f.coeff (n + k + 1)))

Tactic:
simp only [← mul_assoc]

Result:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * ↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1) =
    ↑k ! * ↑((n + k + 1).choose (n + 1)) * ↑(n + 1) * f.coeff (n + k + 1)

Proof state:
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * (n + k + 1).choose (k + 1) = (n + k + 1).choose (n + 1) * (n + 1)

Tactic:
have : n + k + 1 = n + (k + 1) := by apply add_assoc

Result:
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (k + 1) * (n + k + 1).choose (k + 1) = (n + k + 1).choose (n + 1) * (n + 1)

Proof state:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * ↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1) =
    ↑k ! * ↑((n + k + 1).choose (n + 1)) * ↑(n + 1) * f.coeff (n + k + 1)

Tactic:
norm_cast

Result:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k ! * (n + k + 1).choose (k + 1)) * f.coeff (n + k + 1) =
    ↑(k ! * (n + k + 1).choose (n + 1) * (n + 1)) * f.coeff (n + k + 1)

Proof state:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1)! • (↑((n + (k + 1)).choose (k + 1)) * f.coeff (n + (k + 1))) =
    k ! • (↑((n + 1 + k).choose (n + 1)) * f.coeff (n + 1 + k) * (↑n + 1))

Tactic:
simp only [nsmul_eq_mul, factorial_succ, mul_assoc, succ_eq_add_one, ← add_assoc,
  add_right_comm n 1 k, ← cast_succ]

Result:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1)) =
    ↑k ! * (↑((n + k + 1).choose (n + 1)) * (f.coeff (n + k + 1) * ↑(n + 1)))

Proof state:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k ! * (n + k + 1).choose (k + 1)) * f.coeff (n + k + 1) =
    ↑(k ! * (n + k + 1).choose (n + 1) * (n + 1)) * f.coeff (n + k + 1)

Tactic:
congr 2

Result:
case succ.h.a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * k ! * (n + k + 1).choose (k + 1) = k ! * (n + k + 1).choose (n + 1) * (n + 1)

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
⊢ ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]

Tactic:
induction' k with k ih

Result:
case zero
R : Type u_1
inst✝ : Semiring R
k : ℕ
⊢ ⇑(0! • hasseDeriv 0) = (⇑derivative)^[0]

case succ
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
⊢ ⇑((k + 1)! • hasseDeriv (k + 1)) = (⇑derivative)^[k + 1]

Proof state:
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ n + k + 1 = n + (k + 1)

Tactic:
apply add_assoc

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : Semiring R
k : ℕ
⊢ ⇑(0! • hasseDeriv 0) = (⇑derivative)^[0]

Tactic:
rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
⊢ ⇑((k + 1)! • hasseDeriv (k + 1)) = (⇑derivative)^[k + 1]

Tactic:
ext f n : 2

Result:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (((k + 1)! • hasseDeriv (k + 1)) f).coeff n = ((⇑derivative)^[k + 1] f).coeff n