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
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ natDegree (↑(hasseDeriv n) p) ≤ natDegree p - n
rw [hasseDeriv_apply, sum_def]
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
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
refine' (natDegree_sum_le _ _).trans _
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
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
simp_rw [Function.comp, natDegree_monomial]
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

case h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ max 0 (max 0 0) = max 0 0
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
rw [Finset.fold_ite, Finset.fold_const]
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
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
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]
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
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
intro x hx hx'
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
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
have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
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
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
have hxn : n ≤ x := by
  contrapose! hx'
  simp [Nat.choose_eq_zero_of_lt hx']
no goals
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
rwa [tsub_add_cancel_of_le (hxn.trans hxp)]
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
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
contrapose! hx'
no goals
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
simp [Nat.choose_eq_zero_of_lt hx']
no goals
case h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ max 0 (max 0 0) = max 0 0
simp