-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem natDegree_hasseDeriv_le (p : R[X]) (n : ℕ) :
    natDegree (hasseDeriv n p) ≤ natDegree p - n

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n x : ℕ
hx : ¬p.coeff x = 0
hxp : x ≤ p.natDegree
hx' : x < n
⊢ ↑(x.choose n) * p.coeff x = 0

Tactic:
simp [Nat.choose_eq_zero_of_lt hx']

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ 0 ⊔ (0 ⊔ 0) = 0 ⊔ 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n x : ℕ
hx : ¬p.coeff x = 0
hx' : ¬↑(x.choose n) * p.coeff x = 0
hxp : x ≤ p.natDegree
hxn : n ≤ x
⊢ x ≤ p.natDegree - n + n

Tactic:
rwa [tsub_add_cancel_of_le (hxn.trans hxp)]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n x : ℕ
hx : ¬p.coeff x = 0
hx' : ¬↑(x.choose n) * p.coeff x = 0
⊢ x ≤ p.natDegree - n + n

Tactic:
have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n x : ℕ
hx : ¬p.coeff x = 0
hx' : ¬↑(x.choose n) * p.coeff x = 0
hxp : x ≤ p.natDegree
⊢ x ≤ p.natDegree - n + n

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (∑ n_1 ∈ p.support, (monomial (n_1 - n)) (↑(n_1.choose n) * p.coeff n_1)).natDegree ≤ p.natDegree - n

Tactic:
refine (natDegree_sum_le _ _).trans ?_

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ Finset.fold max 0 (natDegree ∘ fun n_1 => (monomial (n_1 - n)) (↑(n_1.choose n) * p.coeff n_1)) p.support ≤
    p.natDegree - n

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n x : ℕ
hx : ¬p.coeff x = 0
hx' : ¬↑(x.choose n) * p.coeff x = 0
hxp : x ≤ p.natDegree
⊢ n ≤ x

Tactic:
contrapose! hx'

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n x : ℕ
hx : ¬p.coeff x = 0
hxp : x ≤ p.natDegree
hx' : x < n
⊢ ↑(x.choose n) * p.coeff x = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (if Finset.filter (fun x => ↑(x.choose n) * p.coeff x = 0) p.support = ∅ then 0 else 0 ⊔ 0) ⊔
      Finset.fold max 0 (fun x => x - n) (Finset.filter (fun i => ¬↑(i.choose n) * p.coeff i = 0) p.support) ≤
    p.natDegree - n

Tactic:
simp only [ite_self, max_eq_right, zero_le', Finset.fold_max_le, true_and, and_imp,
  tsub_le_iff_right, mem_support_iff, Ne, Finset.mem_filter]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ∀ (x : ℕ), ¬p.coeff x = 0 → ¬↑(x.choose n) * p.coeff x = 0 → x ≤ p.natDegree - n + n

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ∀ (x : ℕ), ¬p.coeff x = 0 → ¬↑(x.choose n) * p.coeff x = 0 → x ≤ p.natDegree - n + n

Tactic:
intro x hx hx'

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n x : ℕ
hx : ¬p.coeff x = 0
hx' : ¬↑(x.choose n) * p.coeff x = 0
⊢ x ≤ p.natDegree - n + n

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ Finset.fold max 0 (natDegree ∘ fun n_1 => (monomial (n_1 - n)) (↑(n_1.choose n) * p.coeff n_1)) p.support ≤
    p.natDegree - n

Tactic:
simp_rw [Function.comp, natDegree_monomial]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ Finset.fold max 0 (fun x => if ↑(x.choose n) * p.coeff x = 0 then 0 else x - n) p.support ≤ p.natDegree - n

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n x : ℕ
hx : ¬p.coeff x = 0
hx' : ¬↑(x.choose n) * p.coeff x = 0
hxp : x ≤ p.natDegree
⊢ x ≤ p.natDegree - n + n

Tactic:
have hxn : n ≤ x := by
  contrapose! hx'
  simp [Nat.choose_eq_zero_of_lt hx']

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n x : ℕ
hx : ¬p.coeff x = 0
hx' : ¬↑(x.choose n) * p.coeff x = 0
hxp : x ≤ p.natDegree
hxn : n ≤ x
⊢ x ≤ p.natDegree - n + n

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ Finset.fold max 0 (fun x => if ↑(x.choose n) * p.coeff x = 0 then 0 else x - n) p.support ≤ p.natDegree - n

Tactic:
rw [Finset.fold_ite, Finset.fold_const]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (if Finset.filter (fun x => ↑(x.choose n) * p.coeff x = 0) p.support = ∅ then 0 else 0 ⊔ 0) ⊔
      Finset.fold max 0 (fun x => x - n) (Finset.filter (fun i => ¬↑(i.choose n) * p.coeff i = 0) p.support) ≤
    p.natDegree - n

case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ 0 ⊔ (0 ⊔ 0) = 0 ⊔ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ((hasseDeriv n) p).natDegree ≤ p.natDegree - n

Tactic:
rw [hasseDeriv_apply, sum_def]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (∑ n_1 ∈ p.support, (monomial (n_1 - n)) (↑(n_1.choose n) * p.coeff n_1)).natDegree ≤ p.natDegree - n