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

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

case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ¬n + k ∈ support f → coeff (↑(monomial (n + k - k)) (↑(choose (n + k) k) * coeff f (n + k))) n = 0
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ coeff (↑(hasseDeriv k) f) n = ↑(choose (n + k) k) * coeff f (n + k)
rw [hasseDeriv_apply, coeff_sum, sum_def, Finset.sum_eq_single (n + k), coeff_monomial]
no goals
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ (if n + k - k = n then ↑(choose (n + k) k) * coeff f (n + k) else 0) = ↑(choose (n + k) k) * coeff f (n + k)
simp only [if_true, add_tsub_cancel_right, eq_self_iff_true]
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
⊢ coeff (↑(monomial (i - k)) (↑(choose i k) * coeff f i)) n = 0
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ∀ (b : ℕ), b ∈ support f → b ≠ n + k → coeff (↑(monomial (b - k)) (↑(choose b k) * coeff f b)) n = 0
intro i _hi hink
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
⊢ (if i - k = n then ↑(choose i k) * coeff f i else 0) = 0
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
⊢ coeff (↑(monomial (i - k)) (↑(choose i k) * coeff f i)) n = 0
rw [coeff_monomial]
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
hik : i < k
⊢ (if i - k = n then ↑(choose i k) * coeff f i else 0) = 0

case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
hik : ¬i < k
⊢ (if i - k = n then ↑(choose i k) * coeff f i else 0) = 0
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
⊢ (if i - k = n then ↑(choose i k) * coeff f i else 0) = 0
by_cases hik : i < k
no goals
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
hik : i < k
⊢ (if i - k = n then ↑(choose i k) * coeff f i else 0) = 0
simp only [Nat.choose_eq_zero_of_lt hik, ite_self, Nat.cast_zero, MulZeroClass.zero_mul]
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
hik : k ≤ i
⊢ (if i - k = n then ↑(choose i k) * coeff f i else 0) = 0
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
hik : ¬i < k
⊢ (if i - k = n then ↑(choose i k) * coeff f i else 0) = 0
push_neg at hik
case neg.hnc
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
hik : k ≤ i
⊢ ¬i - k = n
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
hik : k ≤ i
⊢ (if i - k = n then ↑(choose i k) * coeff f i else 0) = 0
rw [if_neg]
case neg.hnc
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hik : k ≤ i
hink : i - k = n
⊢ i = n + k
case neg.hnc
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
hik : k ≤ i
⊢ ¬i - k = n
contrapose! hink
no goals
case neg.hnc
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hik : k ≤ i
hink : i - k = n
⊢ i = n + k
exact (tsub_eq_iff_eq_add_of_le hik).mp hink
case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
h : ¬n + k ∈ support f
⊢ coeff (↑(monomial (n + k - k)) (↑(choose (n + k) k) * coeff f (n + k))) n = 0
case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ¬n + k ∈ support f → coeff (↑(monomial (n + k - k)) (↑(choose (n + k) k) * coeff f (n + k))) n = 0
intro h
no goals
case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
h : ¬n + k ∈ support f
⊢ coeff (↑(monomial (n + k - k)) (↑(choose (n + k) k) * coeff f (n + k))) n = 0
simp only [not_mem_support_iff.mp h, monomial_zero_right, MulZeroClass.mul_zero, coeff_zero]