-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem hasseDeriv_monomial (n : ℕ) (r : R) :
    hasseDeriv k (monomial n r) = monomial (n - k) (↑(n.choose k) * r)

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
by_cases hnik : n = i + k

Result:
case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0

case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
rw [if_neg hnik, mul_zero]

Result:
case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Proof state:
case pos.hc.h
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ n = k + i

Tactic:
rwa [add_comm]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
by_cases hkn : k ≤ n

Result:
case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : ¬k ≤ n
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n - k = i
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
rw [if_neg hnik]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
rw [Nat.choose_eq_zero_of_lt hkn, Nat.cast_zero, zero_mul, ite_self]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
⊢ (hasseDeriv k) ((monomial n) r) = (monomial (n - k)) (↑(n.choose k) * r)

Tactic:
ext i

Result:
case a
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
⊢ ((hasseDeriv k) ((monomial n) r)).coeff i = ((monomial (n - k)) (↑(n.choose k) * r)).coeff i

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : ¬k ≤ n
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
push_neg at hkn

Result:
case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
rw [if_pos hnik, if_pos, ← hnik]

Result:
case pos.hc
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ n - k = i

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
rw [← tsub_eq_iff_eq_add_of_le hkn] at hnik

Result:
case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n - k = i
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Proof state:
case pos.hc
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ n - k = i

Tactic:
apply tsub_eq_of_eq_add_rev

Result:
case pos.hc.h
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ n = k + i

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
⊢ ((hasseDeriv k) ((monomial n) r)).coeff i = ((monomial (n - k)) (↑(n.choose k) * r)).coeff i

Tactic:
simp only [hasseDeriv_coeff, coeff_monomial]

Result:
case a
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0