-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem hasseDeriv_coeff (n : ℕ) :
    (hasseDeriv k f).coeff n = (n + k).choose k * f.coeff (n + k)

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : ¬i < k
⊢ (if i - k = n then ↑(i.choose k) * f.coeff i else 0) = 0

Tactic:
push_neg at hik

Result:
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : k ≤ i
⊢ (if i - k = n then ↑(i.choose k) * f.coeff i else 0) = 0

Proof state:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : k ≤ i
⊢ ¬i - k = n

Tactic:
contrapose! hink

Result:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hik : k ≤ i
hink : i - k = n
⊢ i = n + k

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : i < k
⊢ (if i - k = n then ↑(i.choose k) * f.coeff i else 0) = 0

Tactic:
simp only [Nat.choose_eq_zero_of_lt hik, ite_self, Nat.cast_zero, zero_mul]

Result:
no goals

Proof state:
case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ n + k ∉ f.support → ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0

Tactic:
intro h

Result:
case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
h : n + k ∉ f.support
⊢ ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0

Proof state:
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ∀ b ∈ f.support, b ≠ n + k → ((monomial (b - k)) (↑(b.choose k) * f.coeff b)).coeff n = 0

Tactic:
intro i _hi hink

Result:
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
⊢ ((monomial (i - k)) (↑(i.choose k) * f.coeff i)).coeff n = 0

Proof state:
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
⊢ ((monomial (i - k)) (↑(i.choose k) * f.coeff i)).coeff n = 0

Tactic:
rw [coeff_monomial]

Result:
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
⊢ (if i - k = n then ↑(i.choose k) * f.coeff i else 0) = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : k ≤ i
⊢ (if i - k = n then ↑(i.choose k) * f.coeff i else 0) = 0

Tactic:
rw [if_neg]

Result:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : k ≤ i
⊢ ¬i - k = n

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ (if n + k - k = n then ↑((n + k).choose k) * f.coeff (n + k) else 0) = ↑((n + k).choose k) * f.coeff (n + k)

Tactic:
simp only [if_true, add_tsub_cancel_right, eq_self_iff_true]

Result:
no goals

Proof state:
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
⊢ (if i - k = n then ↑(i.choose k) * f.coeff i else 0) = 0

Tactic:
by_cases hik : i < k

Result:
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : i < k
⊢ (if i - k = n then ↑(i.choose k) * f.coeff i else 0) = 0

case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : ¬i < k
⊢ (if i - k = n then ↑(i.choose k) * f.coeff i else 0) = 0

Proof state:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hik : k ≤ i
hink : i - k = n
⊢ i = n + k

Tactic:
exact (tsub_eq_iff_eq_add_of_le hik).mp hink

Result:
no goals

Proof state:
case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
h : n + k ∉ f.support
⊢ ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0

Tactic:
simp only [not_mem_support_iff.mp h, monomial_zero_right, mul_zero, coeff_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ((hasseDeriv k) f).coeff n = ↑((n + k).choose k) * f.coeff (n + k)

Tactic:
rw [hasseDeriv_apply, coeff_sum, sum_def, Finset.sum_eq_single (n + k), coeff_monomial]

Result:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ (if n + k - k = n then ↑((n + k).choose k) * f.coeff (n + k) else 0) = ↑((n + k).choose k) * f.coeff (n + k)

case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ∀ b ∈ f.support, b ≠ n + k → ((monomial (b - k)) (↑(b.choose k) * f.coeff b)).coeff n = 0

case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ n + k ∉ f.support → ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0