[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(hasseDeriv k) f = sum f fun i r => ↑(monomial (i - k)) (↑(choose i k) * r)
[PROOFSTEP]
dsimp [hasseDeriv]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (sum f fun x x_1 => ↑(monomial (x - k)) (choose x k • x_1)) = sum f fun i r => ↑(monomial (i - k)) (↑(choose i k) * r)
[PROOFSTEP]
congr
[GOAL]
case e_f
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (fun x x_1 => ↑(monomial (x - k)) (choose x k • x_1)) = fun i r => ↑(monomial (i - k)) (↑(choose i k) * r)
[PROOFSTEP]
ext
[GOAL]
case e_f.h.h.a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
x✝¹ : ℕ
x✝ : R
n✝ : ℕ
⊢ coeff (↑(monomial (x✝¹ - k)) (choose x✝¹ k • x✝)) n✝ = coeff (↑(monomial (x✝¹ - k)) (↑(choose x✝¹ k) * x✝)) n✝
[PROOFSTEP]
congr
[GOAL]
case e_f.h.h.a.e_a.h.e_6.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
x✝¹ : ℕ
x✝ : R
n✝ : ℕ
⊢ choose x✝¹ k • x✝ = ↑(choose x✝¹ k) * x✝
[PROOFSTEP]
apply nsmul_eq_mul
[GOAL]
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)
[PROOFSTEP]
rw [hasseDeriv_apply, coeff_sum, sum_def, Finset.sum_eq_single (n + k), coeff_monomial]
[GOAL]
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)
[PROOFSTEP]
simp only [if_true, add_tsub_cancel_right, eq_self_iff_true]
[GOAL]
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
[PROOFSTEP]
intro i _hi hink
[GOAL]
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
[PROOFSTEP]
rw [coeff_monomial]
[GOAL]
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
[PROOFSTEP]
by_cases hik : i < k
[GOAL]
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
[PROOFSTEP]
simp only [Nat.choose_eq_zero_of_lt hik, ite_self, Nat.cast_zero, zero_mul]
[GOAL]
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
[PROOFSTEP]
push_neg at hik 
[GOAL]
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
[PROOFSTEP]
rw [if_neg]
[GOAL]
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
[PROOFSTEP]
contrapose! hink
[GOAL]
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
[PROOFSTEP]
exact (tsub_eq_iff_eq_add_of_le hik).mp hink
[GOAL]
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
[PROOFSTEP]
intro h
[GOAL]
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
[PROOFSTEP]
simp only [not_mem_support_iff.mp h, monomial_zero_right, mul_zero, coeff_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(hasseDeriv 0) f = f
[PROOFSTEP]
simp only [hasseDeriv_apply, tsub_zero, Nat.choose_zero_right, Nat.cast_one, one_mul, sum_monomial_eq]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
h : natDegree p < n
⊢ ↑(hasseDeriv n) p = 0
[PROOFSTEP]
rw [hasseDeriv_apply, sum_def]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
h : natDegree p < n
⊢ ∑ n_1 in support p, ↑(monomial (n_1 - n)) (↑(choose n_1 n) * coeff p n_1) = 0
[PROOFSTEP]
refine' Finset.sum_eq_zero fun x hx => _
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
h : natDegree p < n
x : ℕ
hx : x ∈ support p
⊢ ↑(monomial (x - n)) (↑(choose x n) * coeff p x) = 0
[PROOFSTEP]
simp [Nat.choose_eq_zero_of_lt ((le_natDegree_of_mem_supp _ hx).trans_lt h)]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(hasseDeriv 1) f = ↑derivative f
[PROOFSTEP]
simp only [hasseDeriv_apply, derivative_apply, ← C_mul_X_pow_eq_monomial, Nat.choose_one_right,
  (Nat.cast_commute _ _).eq]
[GOAL]
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)
[PROOFSTEP]
ext i
[GOAL]
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
[PROOFSTEP]
simp only [hasseDeriv_coeff, coeff_monomial]
[GOAL]
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
[PROOFSTEP]
by_cases hnik : n = i + k
[GOAL]
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
[PROOFSTEP]
rw [if_pos hnik, if_pos, ← hnik]
[GOAL]
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
[PROOFSTEP]
apply tsub_eq_of_eq_add_rev
[GOAL]
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
[PROOFSTEP]
rwa [add_comm]
[GOAL]
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
[PROOFSTEP]
rw [if_neg hnik, mul_zero]
[GOAL]
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
[PROOFSTEP]
by_cases hkn : k ≤ n
[GOAL]
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
[PROOFSTEP]
rw [← tsub_eq_iff_eq_add_of_le hkn] at hnik 
[GOAL]
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
[PROOFSTEP]
rw [if_neg hnik]
[GOAL]
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
[PROOFSTEP]
push_neg at hkn 
[GOAL]
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
[PROOFSTEP]
rw [Nat.choose_eq_zero_of_lt hkn, Nat.cast_zero, zero_mul, ite_self]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
r : R
hk : 0 < k
⊢ ↑(hasseDeriv k) (↑C r) = 0
[PROOFSTEP]
rw [← monomial_zero_left, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero, zero_mul,
  monomial_zero_right]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
hk : 0 < k
⊢ ↑(hasseDeriv k) 1 = 0
[PROOFSTEP]
rw [← C_1, hasseDeriv_C k _ hk]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
hk : 1 < k
⊢ ↑(hasseDeriv k) X = 0
[PROOFSTEP]
rw [← monomial_one_one_eq_X, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero, zero_mul,
  monomial_zero_right]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(Nat.zero ! • hasseDeriv Nat.zero) = (↑derivative)^[Nat.zero]
[PROOFSTEP]
rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]
[GOAL]
case succ
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
⊢ ↑((succ k)! • hasseDeriv (succ k)) = (↑derivative)^[succ k]
[PROOFSTEP]
ext f n : 2
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ coeff (↑((succ k)! • hasseDeriv (succ k)) f) n = coeff ((↑derivative)^[succ k] f) n
[PROOFSTEP]
rw [iterate_succ_apply', ← ih]
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ coeff (↑((succ k)! • hasseDeriv (succ k)) f) n = coeff (↑derivative (↑(k ! • hasseDeriv k) f)) n
[PROOFSTEP]
simp only [LinearMap.smul_apply, coeff_smul, LinearMap.map_smul_of_tower, coeff_derivative, hasseDeriv_coeff, ←
  @choose_symm_add _ k]
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ (succ k)! • (↑(choose (n + succ k) (succ k)) * coeff f (n + succ k)) =
    k ! • (↑(choose (n + 1 + k) (n + 1)) * coeff f (n + 1 + k) * (↑n + 1))
[PROOFSTEP]
simp only [nsmul_eq_mul, factorial_succ, mul_assoc, succ_eq_add_one, ← add_assoc, add_right_comm n 1 k, ← cast_succ]
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑(choose (n + k + 1) (k + 1)) * coeff f (n + k + 1)) =
    ↑k ! * (↑(choose (n + k + 1) (n + 1)) * (coeff f (n + k + 1) * ↑(n + 1)))
[PROOFSTEP]
rw [← (cast_commute (n + 1) (f.coeff (n + k + 1))).eq]
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑(choose (n + k + 1) (k + 1)) * coeff f (n + k + 1)) =
    ↑k ! * (↑(choose (n + k + 1) (n + 1)) * (↑(n + 1) * coeff f (n + k + 1)))
[PROOFSTEP]
simp only [← mul_assoc]
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * ↑(choose (n + k + 1) (k + 1)) * coeff f (n + k + 1) =
    ↑k ! * ↑(choose (n + k + 1) (n + 1)) * ↑(n + 1) * coeff f (n + k + 1)
[PROOFSTEP]
norm_cast
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k ! * choose (n + k + 1) (k + 1)) * coeff f (n + k + 1) =
    ↑(k ! * choose (n + k + 1) (n + 1) * (n + 1)) * coeff f (n + k + 1)
[PROOFSTEP]
congr 2
[GOAL]
case succ.h.a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * k ! * choose (n + k + 1) (k + 1) = k ! * choose (n + k + 1) (n + 1) * (n + 1)
[PROOFSTEP]
rw [mul_comm (k + 1) _, mul_assoc, mul_assoc]
[GOAL]
case succ.h.a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ k ! * ((k + 1) * choose (n + k + 1) (k + 1)) = k ! * (choose (n + k + 1) (n + 1) * (n + 1))
[PROOFSTEP]
congr 1
[GOAL]
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * choose (n + k + 1) (k + 1) = choose (n + k + 1) (n + 1) * (n + 1)
[PROOFSTEP]
have : n + k + 1 = n + (k + 1) := by apply add_assoc
[GOAL]
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ n + k + 1 = n + (k + 1)
[PROOFSTEP]
apply add_assoc
[GOAL]
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (k + 1) * choose (n + k + 1) (k + 1) = choose (n + k + 1) (n + 1) * (n + 1)
[PROOFSTEP]
rw [← choose_symm_of_eq_add this, choose_succ_right_eq, mul_comm]
[GOAL]
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ choose (n + k + 1) n * (k + 1) = choose (n + k + 1) n * (n + k + 1 - n)
[PROOFSTEP]
congr
[GOAL]
case succ.h.a.e_a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ k + 1 = n + k + 1 - n
[PROOFSTEP]
rw [add_assoc, add_tsub_cancel_left]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l : ℕ
⊢ LinearMap.comp (hasseDeriv k) (hasseDeriv l) = choose (k + l) k • hasseDeriv (k + l)
[PROOFSTEP]
ext i : 2
[GOAL]
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(LinearMap.comp (LinearMap.comp (hasseDeriv k) (hasseDeriv l)) (monomial i)) 1 =
    ↑(LinearMap.comp (choose (k + l) k • hasseDeriv (k + l)) (monomial i)) 1
[PROOFSTEP]
simp only [LinearMap.smul_apply, comp_apply, LinearMap.coe_comp, smul_monomial, hasseDeriv_apply, mul_one,
  monomial_eq_zero_iff, sum_monomial_index, mul_zero, ← tsub_add_eq_tsub_tsub, add_comm l k]
[GOAL]
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(monomial (i - (k + l))) (↑(choose (i - l) k) * ↑(choose i l)) =
    ↑(monomial (i - (k + l))) (choose (k + l) k • ↑(choose i (k + l)))
[PROOFSTEP]
rw_mod_cast [nsmul_eq_mul]
[GOAL]
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(monomial (i - (k + l))) ↑(choose (i - l) k * choose i l) =
    ↑(monomial (i - (k + l))) (↑(choose (k + l) k) * ↑(choose i (k + l)))
[PROOFSTEP]
rw [← Nat.cast_mul]
[GOAL]
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(monomial (i - (k + l))) ↑(choose (i - l) k * choose i l) =
    ↑(monomial (i - (k + l))) ↑(choose (k + l) k * choose i (k + l))
[PROOFSTEP]
congr 2
[GOAL]
case h.h.h.e_6.h.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
[PROOFSTEP]
by_cases hikl : i < k + l
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
[PROOFSTEP]
rw [choose_eq_zero_of_lt hikl, mul_zero]
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
⊢ choose (i - l) k * choose i l = 0
[PROOFSTEP]
by_cases hil : i < l
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
hil : i < l
⊢ choose (i - l) k * choose i l = 0
[PROOFSTEP]
rw [choose_eq_zero_of_lt hil, mul_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
hil : ¬i < l
⊢ choose (i - l) k * choose i l = 0
[PROOFSTEP]
push_neg at hil 
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
hil : l ≤ i
⊢ choose (i - l) k * choose i l = 0
[PROOFSTEP]
rw [← tsub_lt_iff_right hil] at hikl 
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
⊢ choose (i - l) k * choose i l = 0
[PROOFSTEP]
rw [choose_eq_zero_of_lt hikl, zero_mul]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : ¬i < k + l
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
[PROOFSTEP]
push_neg at hikl 
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
[PROOFSTEP]
apply @cast_injective ℚ
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
[PROOFSTEP]
have h1 : l ≤ i := le_of_add_le_right hikl
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
[PROOFSTEP]
have h2 : k ≤ i - l := le_tsub_of_add_le_right hikl
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
[PROOFSTEP]
have h3 : k ≤ k + l := le_self_add
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
[PROOFSTEP]
push_cast
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(choose (i - l) k) * ↑(choose i l) = ↑(choose (k + l) k) * ↑(choose i (k + l))
[PROOFSTEP]
rw [cast_choose ℚ h1, cast_choose ℚ h2, cast_choose ℚ h3, cast_choose ℚ hikl]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑(k + l - k)!) * (↑i ! / (↑(k + l)! * ↑(i - (k + l))!))
[PROOFSTEP]
rw [show i - (k + l) = i - l - k by rw [add_comm]; apply tsub_add_eq_tsub_tsub]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (k + l) = i - l - k
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (l + k) = i - l - k
[PROOFSTEP]
apply tsub_add_eq_tsub_tsub
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑(k + l - k)!) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))
[PROOFSTEP]
simp only [add_tsub_cancel_left]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑l !) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))
[PROOFSTEP]
have H : ∀ n : ℕ, (n ! : ℚ) ≠ 0 := by exact_mod_cast factorial_ne_zero
[GOAL]
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ∀ (n : ℕ), ↑n ! ≠ 0
[PROOFSTEP]
exact_mod_cast factorial_ne_zero
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
H : ∀ (n : ℕ), ↑n ! ≠ 0
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑l !) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))
[PROOFSTEP]
field_simp [H]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
H : ∀ (n : ℕ), ↑n ! ≠ 0
⊢ ↑(i - l)! * ↑i ! * (↑k ! * ↑l ! * (↑(k + l)! * ↑(i - l - k)!)) =
    ↑(k + l)! * ↑i ! * (↑k ! * ↑(i - l - k)! * (↑l ! * ↑(i - l)!))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ natDegree (↑(hasseDeriv n) p) ≤ natDegree p - n
[PROOFSTEP]
classical
rw [hasseDeriv_apply, sum_def]
refine' (natDegree_sum_le _ _).trans _
simp_rw [Function.comp, natDegree_monomial]
rw [Finset.fold_ite, Finset.fold_const]
· simp only [ite_self, max_eq_right, zero_le', Finset.fold_max_le, true_and_iff, and_imp, tsub_le_iff_right,
    mem_support_iff, Ne.def, Finset.mem_filter]
  intro x hx hx'
  have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
  have hxn : n ≤ x := by
    contrapose! hx'
    simp [Nat.choose_eq_zero_of_lt hx']
  rwa [tsub_add_cancel_of_le (hxn.trans hxp)]
· simp
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ natDegree (↑(hasseDeriv n) p) ≤ natDegree p - n
[PROOFSTEP]
rw [hasseDeriv_apply, sum_def]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ natDegree (∑ n_1 in support p, ↑(monomial (n_1 - n)) (↑(choose n_1 n) * coeff p n_1)) ≤ natDegree p - n
[PROOFSTEP]
refine' (natDegree_sum_le _ _).trans _
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ Finset.fold max 0 (natDegree ∘ fun n_1 => ↑(monomial (n_1 - n)) (↑(choose n_1 n) * coeff p n_1)) (support p) ≤
    natDegree p - n
[PROOFSTEP]
simp_rw [Function.comp, natDegree_monomial]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ Finset.fold max 0 (fun x => if ↑(choose x n) * coeff p x = 0 then 0 else x - n) (support p) ≤ natDegree p - n
[PROOFSTEP]
rw [Finset.fold_ite, Finset.fold_const]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ max (if Finset.filter (fun x => ↑(choose x n) * coeff p x = 0) (support p) = ∅ then 0 else max 0 0)
      (Finset.fold max 0 (fun x => x - n) (Finset.filter (fun i => ¬↑(choose i n) * coeff p i = 0) (support p))) ≤
    natDegree p - n
[PROOFSTEP]
simp only [ite_self, max_eq_right, zero_le', Finset.fold_max_le, true_and_iff, and_imp, tsub_le_iff_right,
  mem_support_iff, Ne.def, Finset.mem_filter]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ ∀ (x : ℕ), ¬coeff p x = 0 → ¬↑(choose x n) * coeff p x = 0 → x ≤ natDegree p - n + n
[PROOFSTEP]
intro x hx hx'
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n x : ℕ
hx : ¬coeff p x = 0
hx' : ¬↑(choose x n) * coeff p x = 0
⊢ x ≤ natDegree p - n + n
[PROOFSTEP]
have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n x : ℕ
hx : ¬coeff p x = 0
hx' : ¬↑(choose x n) * coeff p x = 0
hxp : x ≤ natDegree p
⊢ x ≤ natDegree p - n + n
[PROOFSTEP]
have hxn : n ≤ x := by
  contrapose! hx'
  simp [Nat.choose_eq_zero_of_lt hx']
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n x : ℕ
hx : ¬coeff p x = 0
hx' : ¬↑(choose x n) * coeff p x = 0
hxp : x ≤ natDegree p
⊢ n ≤ x
[PROOFSTEP]
contrapose! hx'
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n x : ℕ
hx : ¬coeff p x = 0
hxp : x ≤ natDegree p
hx' : x < n
⊢ ↑(choose x n) * coeff p x = 0
[PROOFSTEP]
simp [Nat.choose_eq_zero_of_lt hx']
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n x : ℕ
hx : ¬coeff p x = 0
hx' : ¬↑(choose x n) * coeff p x = 0
hxp : x ≤ natDegree p
hxn : n ≤ x
⊢ x ≤ natDegree p - n + n
[PROOFSTEP]
rwa [tsub_add_cancel_of_le (hxn.trans hxp)]
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ max 0 (max 0 0) = max 0 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
⊢ natDegree (↑(hasseDeriv n) p) = natDegree p - n
[PROOFSTEP]
cases' lt_or_le p.natDegree n with hn hn
[GOAL]
case inl
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : natDegree p < n
⊢ natDegree (↑(hasseDeriv n) p) = natDegree p - n
[PROOFSTEP]
simpa [hasseDeriv_eq_zero_of_lt_natDegree, hn] using (tsub_eq_zero_of_le hn.le).symm
[GOAL]
case inr
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ natDegree (↑(hasseDeriv n) p) = natDegree p - n
[PROOFSTEP]
refine' map_natDegree_eq_sub _ _
[GOAL]
case inr.refine'_1
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (f : R[X]), natDegree f < n → ↑(hasseDeriv n) f = 0
[PROOFSTEP]
exact fun h => hasseDeriv_eq_zero_of_lt_natDegree _ _
[GOAL]
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (n_1 : ℕ) (c : R), c ≠ 0 → natDegree (↑(hasseDeriv n) (↑(monomial n_1) c)) = n_1 - n
[PROOFSTEP]
classical
simp only [ite_eq_right_iff, Ne.def, natDegree_monomial, hasseDeriv_monomial]
intro k c c0 hh
rw [← nsmul_eq_mul, smul_eq_zero, Nat.choose_eq_zero_iff] at hh 
exact (tsub_eq_zero_of_le (Or.resolve_right hh c0).le).symm
[GOAL]
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (n_1 : ℕ) (c : R), c ≠ 0 → natDegree (↑(hasseDeriv n) (↑(monomial n_1) c)) = n_1 - n
[PROOFSTEP]
simp only [ite_eq_right_iff, Ne.def, natDegree_monomial, hasseDeriv_monomial]
[GOAL]
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (n_1 : ℕ) (c : R), ¬c = 0 → ↑(choose n_1 n) * c = 0 → 0 = n_1 - n
[PROOFSTEP]
intro k c c0 hh
[GOAL]
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k✝ : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
k : ℕ
c : R
c0 : ¬c = 0
hh : ↑(choose k n) * c = 0
⊢ 0 = k - n
[PROOFSTEP]
rw [← nsmul_eq_mul, smul_eq_zero, Nat.choose_eq_zero_iff] at hh 
[GOAL]
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k✝ : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
k : ℕ
c : R
c0 : ¬c = 0
hh : k < n ∨ c = 0
⊢ 0 = k - n
[PROOFSTEP]
exact (tsub_eq_zero_of_le (Or.resolve_right hh c0).le).symm
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f✝ f g : R[X]
⊢ ↑(hasseDeriv k) (f * g) = ∑ ij in antidiagonal k, ↑(hasseDeriv ij.fst) f * ↑(hasseDeriv ij.snd) g
[PROOFSTEP]
let D k := (@hasseDeriv R _ k).toAddMonoidHom
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f✝ f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
⊢ ↑(hasseDeriv k) (f * g) = ∑ ij in antidiagonal k, ↑(hasseDeriv ij.fst) f * ↑(hasseDeriv ij.snd) g
[PROOFSTEP]
let Φ := @AddMonoidHom.mul R[X] _
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f✝ f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ ↑(hasseDeriv k) (f * g) = ∑ ij in antidiagonal k, ↑(hasseDeriv ij.fst) f * ↑(hasseDeriv ij.snd) g
[PROOFSTEP]
show
  (compHom (D k)).comp Φ f g = ∑ ij : ℕ × ℕ in antidiagonal k, ((compHom.comp ((compHom Φ) (D ij.1))).flip (D ij.2) f) g
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f✝ f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ ↑(↑(AddMonoidHom.comp (↑compHom (D k)) Φ) f) g =
    ∑ ij in antidiagonal k,
      ↑(↑(↑(AddMonoidHom.flip (AddMonoidHom.comp compHom (↑(↑compHom Φ) (D ij.fst)))) (D ij.snd)) f) g
[PROOFSTEP]
simp only [← finset_sum_apply]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f✝ f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ ↑(↑(AddMonoidHom.comp (↑compHom (LinearMap.toAddMonoidHom (hasseDeriv k))) mul) f) g =
    ↑(↑(∑ x in antidiagonal k,
              ↑(AddMonoidHom.flip
                    (AddMonoidHom.comp compHom (↑(↑compHom mul) (LinearMap.toAddMonoidHom (hasseDeriv x.fst)))))
                (LinearMap.toAddMonoidHom (hasseDeriv x.snd)))
          f)
      g
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f✝ f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ AddMonoidHom.comp (↑compHom (LinearMap.toAddMonoidHom (hasseDeriv k))) mul =
    ∑ x in antidiagonal k,
      ↑(AddMonoidHom.flip (AddMonoidHom.comp compHom (↑(↑compHom mul) (LinearMap.toAddMonoidHom (hasseDeriv x.fst)))))
        (LinearMap.toAddMonoidHom (hasseDeriv x.snd))
[PROOFSTEP]
clear f g
[GOAL]
case e_a.e_a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ AddMonoidHom.comp (↑compHom (LinearMap.toAddMonoidHom (hasseDeriv k))) mul =
    ∑ x in antidiagonal k,
      ↑(AddMonoidHom.flip (AddMonoidHom.comp compHom (↑(↑compHom mul) (LinearMap.toAddMonoidHom (hasseDeriv x.fst)))))
        (LinearMap.toAddMonoidHom (hasseDeriv x.snd))
[PROOFSTEP]
ext m r n s : 4
[GOAL]
case e_a.e_a.h.h.h.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
⊢ ↑(AddMonoidHom.comp
          (↑(AddMonoidHom.comp (AddMonoidHom.comp (↑compHom (LinearMap.toAddMonoidHom (hasseDeriv k))) mul)
                (LinearMap.toAddMonoidHom (monomial m)))
            r)
          (LinearMap.toAddMonoidHom (monomial n)))
      s =
    ↑(AddMonoidHom.comp
          (↑(AddMonoidHom.comp
                (∑ x in antidiagonal k,
                  ↑(AddMonoidHom.flip
                        (AddMonoidHom.comp compHom (↑(↑compHom mul) (LinearMap.toAddMonoidHom (hasseDeriv x.fst)))))
                    (LinearMap.toAddMonoidHom (hasseDeriv x.snd)))
                (LinearMap.toAddMonoidHom (monomial m)))
            r)
          (LinearMap.toAddMonoidHom (monomial n)))
      s
[PROOFSTEP]
simp only [finset_sum_apply, coe_mulLeft, coe_comp, flip_apply, Function.comp_apply, hasseDeriv_monomial,
  LinearMap.toAddMonoidHom_coe, compHom_apply_apply, coe_mul, monomial_mul_monomial]
[GOAL]
case e_a.e_a.h.h.h.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
⊢ ↑(monomial (m + n - k)) (↑(choose (m + n) k) * (r * s)) =
    ∑ x in antidiagonal k, ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s))
[PROOFSTEP]
have aux :
  ∀ x : ℕ × ℕ,
    x ∈ antidiagonal k →
      monomial (m - x.1 + (n - x.2)) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
        monomial (m + n - k) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s)) :=
  by
  intro x hx
  rw [Finset.Nat.mem_antidiagonal] at hx 
  subst hx
  by_cases hm : m < x.1
  · simp only [Nat.choose_eq_zero_of_lt hm, Nat.cast_zero, zero_mul, monomial_zero_right]
  by_cases hn : n < x.2
  · simp only [Nat.choose_eq_zero_of_lt hn, Nat.cast_zero, zero_mul, mul_zero, monomial_zero_right]
  push_neg at hm hn 
  rw [tsub_add_eq_add_tsub hm, ← add_tsub_assoc_of_le hn, ← tsub_add_eq_tsub_tsub, add_comm x.2 x.1, mul_assoc, ←
    mul_assoc r, ← (Nat.cast_commute _ r).eq, mul_assoc, mul_assoc]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
⊢ ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal k →
      ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
        ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
rw [Finset.Nat.mem_antidiagonal] at hx 
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hx : x.fst + x.snd = k
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
subst hx
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - (x.fst + x.snd))) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
by_cases hm : m < x.1
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : m < x.fst
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - (x.fst + x.snd))) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
simp only [Nat.choose_eq_zero_of_lt hm, Nat.cast_zero, zero_mul, monomial_zero_right]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : ¬m < x.fst
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - (x.fst + x.snd))) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
by_cases hn : n < x.2
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : ¬m < x.fst
hn : n < x.snd
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - (x.fst + x.snd))) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
simp only [Nat.choose_eq_zero_of_lt hn, Nat.cast_zero, zero_mul, mul_zero, monomial_zero_right]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : ¬m < x.fst
hn : ¬n < x.snd
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - (x.fst + x.snd))) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
push_neg at hm hn 
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.fst ≤ m
hn : x.snd ≤ n
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - (x.fst + x.snd))) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
rw [tsub_add_eq_add_tsub hm, ← add_tsub_assoc_of_le hn, ← tsub_add_eq_tsub_tsub, add_comm x.2 x.1, mul_assoc, ←
  mul_assoc r, ← (Nat.cast_commute _ r).eq, mul_assoc, mul_assoc]
[GOAL]
case e_a.e_a.h.h.h.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal k →
      ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
        ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
⊢ ↑(monomial (m + n - k)) (↑(choose (m + n) k) * (r * s)) =
    ∑ x in antidiagonal k, ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s))
[PROOFSTEP]
rw [Finset.sum_congr rfl aux]
[GOAL]
case e_a.e_a.h.h.h.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal k →
      ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
        ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
⊢ ↑(monomial (m + n - k)) (↑(choose (m + n) k) * (r * s)) =
    ∑ x in antidiagonal k, ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
rw [← LinearMap.map_sum, ← Finset.sum_mul]
[GOAL]
case e_a.e_a.h.h.h.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal k →
      ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
        ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
⊢ ↑(monomial (m + n - k)) (↑(choose (m + n) k) * (r * s)) =
    ↑(monomial (m + n - k)) ((∑ x in antidiagonal k, ↑(choose m x.fst) * ↑(choose n x.snd)) * (r * s))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a.h.h.h.h.h.e_6.h.e_a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal k →
      ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
        ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
⊢ ↑(choose (m + n) k) = ∑ x in antidiagonal k, ↑(choose m x.fst) * ↑(choose n x.snd)
[PROOFSTEP]
rw_mod_cast [← Nat.add_choose_eq]
