case a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
⊢ coeff (↑(hasseDeriv k) (↑(monomial n) r)) i = coeff (↑(monomial (n - k)) (↑(choose n k) * r)) i
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
⊢ ↑(hasseDeriv k) (↑(monomial n) r) = ↑(monomial (n - k)) (↑(choose n k) * r)
ext i
case a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
⊢ (↑(choose (i + k) k) * if n = i + k then r else 0) = if n - k = i then ↑(choose n k) * r else 0
case a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
⊢ coeff (↑(hasseDeriv k) (↑(monomial n) r)) i = coeff (↑(monomial (n - k)) (↑(choose n k) * r)) i
simp only [hasseDeriv_coeff, coeff_monomial]
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ (↑(choose (i + k) k) * if n = i + k then r else 0) = if n - k = i then ↑(choose n k) * r else 0

case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ (↑(choose (i + k) k) * if n = i + k then r else 0) = if n - k = i then ↑(choose n k) * r else 0
case a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
⊢ (↑(choose (i + k) k) * if n = i + k then r else 0) = if n - k = i then ↑(choose n k) * r else 0
by_cases hnik : n = i + k
case pos.hc
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ n - k = i
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ (↑(choose (i + k) k) * if n = i + k then r else 0) = if n - k = i then ↑(choose n k) * r else 0
rw [if_pos hnik, if_pos, ← hnik]
case pos.hc.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ n = k + i
case pos.hc
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ n - k = i
apply tsub_eq_of_eq_add_rev
no goals
case pos.hc.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ n = k + i
rwa [add_comm]
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ (↑(choose (i + k) k) * if n = i + k then r else 0) = if n - k = i then ↑(choose n k) * r else 0
rw [if_neg hnik, MulZeroClass.mul_zero]
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0

case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : ¬k ≤ n
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
by_cases hkn : k ≤ n
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n - k = i
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
rw [← tsub_eq_iff_eq_add_of_le hkn] at hnik
no goals
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n - k = i
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
rw [if_neg hnik]
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : ¬k ≤ n
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
push_neg  at hkn
no goals
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
rw [Nat.choose_eq_zero_of_lt hkn, Nat.cast_zero, MulZeroClass.zero_mul, ite_self]