awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k_1 k : ℕ
ih :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) k ! (hasseDeriv k)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k]
f : R[X]
n : ℕ
⊢ k ! * ((k + 1) * (n + k + 1).choose (k + 1)) = k ! * ((n + k + 1).choose (n + 1) * (n + 1))
have succ : (k + 1) * (n + k + 1).choose (k + 1) = (n + k + 1).choose (n + 1) * (n + 1)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
k_1 k : ℕ
ih :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) k ! (hasseDeriv k)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * (n + k + 1).choose (k + 1) = (n + k + 1).choose (n + 1) * (n + 1)
have this : n + k + 1 = n + (k + 1)
Tactic: have : n + k + 1 = n + (k + 1) := by apply add_assoc
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k_1 k : ℕ
ih :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) k ! (hasseDeriv k)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (k + 1) * (n + k + 1).choose (k + 1) = (n + k + 1).choose (n + 1) * (n + 1)
have succ : (n + k + 1).choose n * (k + 1) = (n + k + 1).choose n * (n + k + 1 - n)
Tactic: rw [← choose_symm_of_eq_add this, choose_succ_right_eq, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k_1 k : ℕ
ih :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) k ! (hasseDeriv k)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (n + k + 1).choose n * (k + 1) = (n + k + 1).choose n * (n + k + 1 - n)
have succ : k + 1 = n + k + 1 - n
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k_1 k : ℕ
ih :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) k ! (hasseDeriv k)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ k + 1 = n + k + 1 - n
have succ : k + 1 = n + (k + 1) - n
Tactic: rw [add_assoc, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k_1 k : ℕ
ih :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) k ! (hasseDeriv k)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
succ : k + 1 = n + (k + 1) - n
⊢ k + 1 = n + k + 1 - n
have succ₁ : k + 1 = k + 1
Tactic: rw [add_assoc, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l : ℕ
⊢ hasseDeriv k ∘ₗ hasseDeriv l = HSMul.hSMul (β := R[X] →ₗ[R] R[X]) ((k + l).choose k) (hasseDeriv (k + l))
have h : ∀ (i : ℕ),
  Eq (α := R[X]) (((hasseDeriv k ∘ₗ hasseDeriv l) ∘ₗ monomial i : (a : R) → R[X]) 1)
    ((HSMul.hSMul (β := R[X] →ₗ[R] R[X]) ((k + l).choose k) (hasseDeriv (k + l)) ∘ₗ monomial i : (a : R) → R[X]) 1)
Tactic: ext i : 2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
⊢ Eq (α := R[X]) (((hasseDeriv k ∘ₗ hasseDeriv l) ∘ₗ monomial i : (a : R) → R[X]) 1)
    ((HSMul.hSMul (β := R[X] →ₗ[R] R[X]) ((k + l).choose k) (hasseDeriv (k + l)) ∘ₗ monomial i : (a : R) → R[X]) 1)
have h : Eq (α := R[X])
  ((monomial (i - (k + l)) : (a : R) → R[X]) (HMul.hMul (α := R) (↑((i - l).choose k) : R) (↑(i.choose l) : R)) : R[X])
  ((monomial (i - (k + l)) : (a : R) → R[X]) (HSMul.hSMul (β := R) ((k + l).choose k) (↑(i.choose (k + l)) : R)) : R[X])
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
⊢ Eq (α := R[X])
    ((monomial (i - (k + l)) : (a : R) → R[X]) (HMul.hMul (α := R) (↑((i - l).choose k) : R) (↑(i.choose l) : R)) :
      R[X])
    ((monomial (i - (k + l)) : (a : R) → R[X]) (HSMul.hSMul (β := R) ((k + l).choose k) (↑(i.choose (k + l)) : R)) :
      R[X])
have h : Eq (α := R[X]) ((monomial (i - (k + l)) : (a : R) → R[X]) (↑((i - l).choose k * i.choose l) : R) : R[X])
  ((monomial (i - (k + l)) : (a : R) → R[X]) (HMul.hMul (α := R) (↑((k + l).choose k) : R) (↑(i.choose (k + l)) : R)) :
    R[X])
Tactic: rw_mod_cast [nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
⊢ Eq (α := R[X]) ((monomial (i - (k + l)) : (a : R) → R[X]) (↑((i - l).choose k * i.choose l) : R) : R[X])
    ((monomial (i - (k + l)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑((k + l).choose k) : R) (↑(i.choose (k + l)) : R)) :
      R[X])
have h : Eq.{u_1 + 1} (α := R[X]) ((monomial (i - (k + l)) : (a : R) → R[X]) (↑((i - l).choose k * i.choose l) : R))
  ((monomial (i - (k + l)) : (a : R) → R[X]) (↑((k + l).choose k * i.choose (k + l)) : R))
Tactic: rw [← Nat.cast_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
⊢ Eq.{u_1 + 1} (α := R[X]) ((monomial (i - (k + l)) : (a : R) → R[X]) (↑((i - l).choose k * i.choose l) : R))
    ((monomial (i - (k + l)) : (a : R) → R[X]) (↑((k + l).choose k * i.choose (k + l)) : R))
have h : (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)
have pos : ∀ (hikl : i < k + l), (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)
Tactic: by_cases! hikl : i < k + l
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
pos : ∀ (hikl : i < k + l), (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)
have neg : ∀ (hikl : k + l ≤ i), (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)
Tactic: by_cases! hikl : i < k + l
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)
have pos : (i - l).choose k * i.choose l = 0
Tactic: rw [choose_eq_zero_of_lt hikl, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = 0
have pos : ∀ (hil : i < l), (i - l).choose k * i.choose l = 0
Tactic: by_cases! hil : i < l
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : i < k + l
pos : ∀ (hil : i < l), (i - l).choose k * i.choose l = 0
⊢ (i - l).choose k * i.choose l = 0
have neg : ∀ (hil : l ≤ i), (i - l).choose k * i.choose l = 0
Tactic: by_cases! hil : i < l
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : i < k + l
hil : i < l
⊢ (i - l).choose k * i.choose l = 0
have pos : (i - l).choose k * 0 = 0
Tactic: rw [choose_eq_zero_of_lt hil, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : i < k + l
hil : i < l
pos : (i - l).choose k * 0 = 0
⊢ (i - l).choose k * i.choose l = 0
have pos₁ : Eq (α := ℕ) 0 0
Tactic: rw [choose_eq_zero_of_lt hil, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : i < k + l
hil : l ≤ i
⊢ (i - l).choose k * i.choose l = 0
have hikl₁ : i - l < k
Tactic: rw [← tsub_lt_iff_right hil] at hikl
Cleared hypotheses: hikl, hil
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
⊢ (i - l).choose k * i.choose l = 0
have neg : 0 * i.choose l = 0
Tactic: rw [choose_eq_zero_of_lt hikl, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
neg : 0 * i.choose l = 0
⊢ (i - l).choose k * i.choose l = 0
have neg₁ : Eq (α := ℕ) 0 0
Tactic: rw [choose_eq_zero_of_lt hikl, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : k + l ≤ i
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)
have neg : Eq (α := ℚ) (↑((i - l).choose k * i.choose l) : ℚ) (↑((k + l).choose k * i.choose (k + l)) : ℚ)
Tactic: apply @cast_injective ℚ
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : k + l ≤ i
⊢ Eq (α := ℚ) (↑((i - l).choose k * i.choose l) : ℚ) (↑((k + l).choose k * i.choose (k + l)) : ℚ)
have h1 : l ≤ i
Tactic: have h1 : l ≤ i := le_of_add_le_right hikl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
⊢ Eq (α := ℚ) (↑((i - l).choose k * i.choose l) : ℚ) (↑((k + l).choose k * i.choose (k + l)) : ℚ)
have h2 : k ≤ i - l
Tactic: have h2 : k ≤ i - l := le_tsub_of_add_le_right hikl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
⊢ Eq (α := ℚ) (↑((i - l).choose k * i.choose l) : ℚ) (↑((k + l).choose k * i.choose (k + l)) : ℚ)
have h3 : k ≤ k + l
Tactic: have h3 : k ≤ k + l := le_self_add
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ Eq (α := ℚ) (↑((i - l).choose k * i.choose l) : ℚ) (↑((k + l).choose k * i.choose (k + l)) : ℚ)
have neg : HMul.hMul (α := ℚ) (↑((i - l).choose k) : ℚ) (↑(i.choose l) : ℚ) =
  HMul.hMul (α := ℚ) (↑((k + l).choose k) : ℚ) (↑(i.choose (k + l)) : ℚ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ HMul.hMul (α := ℚ) (↑((i - l).choose k) : ℚ) (↑(i.choose l) : ℚ) =
    HMul.hMul (α := ℚ) (↑((k + l).choose k) : ℚ) (↑(i.choose (k + l)) : ℚ)
have neg : (↑(i - l)! : ℚ) / HMul.hMul (α := ℚ) (↑k ! : ℚ) (↑(i - l - k)! : ℚ) *
    ((↑i ! : ℚ) / HMul.hMul (α := ℚ) (↑l ! : ℚ) (↑(i - l)! : ℚ)) =
  (↑(k + l)! : ℚ) / HMul.hMul (α := ℚ) (↑k ! : ℚ) (↑(k + l - k)! : ℚ) *
    ((↑i ! : ℚ) / HMul.hMul (α := ℚ) (↑(k + l)! : ℚ) (↑(i - (k + l))! : ℚ))
Tactic: rw [cast_choose ℚ h1, cast_choose ℚ h2, cast_choose ℚ h3, cast_choose ℚ hikl]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (k + l) = i - l - k
have rw : i - (l + k) = i - l - k
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ (↑(i - l)! : ℚ) / HMul.hMul (α := ℚ) (↑k ! : ℚ) (↑(i - l - k)! : ℚ) *
      ((↑i ! : ℚ) / HMul.hMul (α := ℚ) (↑l ! : ℚ) (↑(i - l)! : ℚ)) =
    (↑(k + l)! : ℚ) / HMul.hMul (α := ℚ) (↑k ! : ℚ) (↑(k + l - k)! : ℚ) *
      ((↑i ! : ℚ) / HMul.hMul (α := ℚ) (↑(k + l)! : ℚ) (↑(i - (k + l))! : ℚ))
have neg : (↑(i - l)! : ℚ) / HMul.hMul (α := ℚ) (↑k ! : ℚ) (↑(i - l - k)! : ℚ) *
    ((↑i ! : ℚ) / HMul.hMul (α := ℚ) (↑l ! : ℚ) (↑(i - l)! : ℚ)) =
  (↑(k + l)! : ℚ) / HMul.hMul (α := ℚ) (↑k ! : ℚ) (↑(k + l - k)! : ℚ) *
    ((↑i ! : ℚ) / HMul.hMul (α := ℚ) (↑(k + l)! : ℚ) (↑(i - l - k)! : ℚ))
Tactic: rw [show i - (k + l) = i - l - k by rw [add_comm]; apply tsub_add_eq_tsub_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ (↑(i - l)! : ℚ) / HMul.hMul (α := ℚ) (↑k ! : ℚ) (↑(i - l - k)! : ℚ) *
      ((↑i ! : ℚ) / HMul.hMul (α := ℚ) (↑l ! : ℚ) (↑(i - l)! : ℚ)) =
    (↑(k + l)! : ℚ) / HMul.hMul (α := ℚ) (↑k ! : ℚ) (↑(k + l - k)! : ℚ) *
      ((↑i ! : ℚ) / HMul.hMul (α := ℚ) (↑(k + l)! : ℚ) (↑(i - l - k)! : ℚ))
have neg : (↑(i - l)! : ℚ) / HMul.hMul (α := ℚ) (↑k ! : ℚ) (↑(i - l - k)! : ℚ) *
    ((↑i ! : ℚ) / HMul.hMul (α := ℚ) (↑l ! : ℚ) (↑(i - l)! : ℚ)) =
  (↑(k + l)! : ℚ) / HMul.hMul (α := ℚ) (↑k ! : ℚ) (↑l ! : ℚ) *
    ((↑i ! : ℚ) / HMul.hMul (α := ℚ) (↑(k + l)! : ℚ) (↑(i - l - k)! : ℚ))
Tactic: simp only [add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) p) ≤ p.natDegree - n
have rw : natDegree.{u_1} (R := R)
    (∑ n_1 ∈ p.support, (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1)) ≤
  p.natDegree - n
Tactic: rw [hasseDeriv_apply, sum_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ natDegree.{u_1} (R := R)
      (∑ n_1 ∈ p.support, (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1)) ≤
    p.natDegree - n
have refine : Finset.fold max 0
    (Function.comp.{1, u_1 + 1, 1} (β := R[X]) natDegree fun (n_1 : ℕ) ↦
      (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1))
    p.support ≤
  p.natDegree - n
Tactic: refine (natDegree_sum_le _ _).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ Finset.fold max 0
      (Function.comp.{1, u_1 + 1, 1} (β := R[X]) natDegree fun (n_1 : ℕ) ↦
        (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1))
      p.support ≤
    p.natDegree - n
have simp_rw : Finset.fold max 0 (fun (x : ℕ) ↦ if (↑(x.choose n) : R) * p.coeff x = 0 then 0 else x - n) p.support ≤ p.natDegree - n
Tactic: simp_rw [Function.comp, natDegree_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ Finset.fold max 0 (fun (x : ℕ) ↦ if (↑(x.choose n) : R) * p.coeff x = 0 then 0 else x - n) p.support ≤ p.natDegree - n
have rw : max (if {x ∈ p.support | (↑(x.choose n) : R) * p.coeff x = 0} = ∅ then 0 else max 0 0)
    (Finset.fold max 0 (fun (x : ℕ) ↦ x - n) ({i ∈ p.support | ¬(↑(i.choose n) : R) * p.coeff i = 0})) ≤
  p.natDegree - n
Tactic: rw [Finset.fold_ite, Finset.fold_const]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
rw :
  max (if {x ∈ p.support | (↑(x.choose n) : R) * p.coeff x = 0} = ∅ then 0 else max 0 0)
      (Finset.fold max 0 (fun (x : ℕ) ↦ x - n) ({i ∈ p.support | ¬(↑(i.choose n) : R) * p.coeff i = 0})) ≤
    p.natDegree - n
⊢ Finset.fold max 0 (fun (x : ℕ) ↦ if (↑(x.choose n) : R) * p.coeff x = 0 then 0 else x - n) p.support ≤ p.natDegree - n
have h : Eq (α := ℕ) (max 0 (max 0 0)) (max 0 0)
Tactic: rw [Finset.fold_ite, Finset.fold_const]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ max (if {x ∈ p.support | (↑(x.choose n) : R) * p.coeff x = 0} = ∅ then 0 else max 0 0)
      (Finset.fold max 0 (fun (x : ℕ) ↦ x - n) ({i ∈ p.support | ¬(↑(i.choose n) : R) * p.coeff i = 0})) ≤
    p.natDegree - n
have simp : ∀ (x : ℕ), ¬p.coeff x = 0 → ¬(↑(x.choose n) : R) * p.coeff x = 0 → x ≤ p.natDegree - n + 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n x : ℕ
hx : ¬p.coeff x = 0
hx' : ¬(↑(x.choose n) : R) * p.coeff x = 0
⊢ x ≤ p.natDegree - n + n
have hxp : x ≤ p.natDegree
Tactic: have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) p) ≤ p.natDegree - n
have rw : natDegree (R := R) (p.sum fun (i : ℕ) (r : R) ↦ (monomial (i - n) : (a : R) → R[X]) ((↑(i.choose n) : R) * r)) ≤
  p.natDegree - n
Tactic: 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, and_imp,
        tsub_le_iff_right, mem_support_iff, Ne, Finset.mem_filter]
      intro x hx hx'
      have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
      grind
    · simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
rw :
  natDegree (R := R) (p.sum fun (i : ℕ) (r : R) ↦ (monomial (i - n) : (a : R) → R[X]) ((↑(i.choose n) : R) * r)) ≤
    p.natDegree - n
⊢ natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) p) ≤ p.natDegree - n
have rw₁ : natDegree.{u_1} (R := R)
    (∑ n_1 ∈ p.support, (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1)) ≤
  p.natDegree - n
Tactic: 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, and_imp,
        tsub_le_iff_right, mem_support_iff, Ne, Finset.mem_filter]
      intro x hx hx'
      have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
      grind
    · simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
rw :
  natDegree (R := R) (p.sum fun (i : ℕ) (r : R) ↦ (monomial (i - n) : (a : R) → R[X]) ((↑(i.choose n) : R) * r)) ≤
    p.natDegree - n
rw₁ rw₂ rw₃ :
  natDegree.{u_1} (R := R)
      (∑ n_1 ∈ p.support, (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1)) ≤
    p.natDegree - n
⊢ natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) p) ≤ p.natDegree - n
have rw₄ : Finset.fold max 0
    (Function.comp.{1, u_1 + 1, 1} (β := R[X]) natDegree fun (n_1 : ℕ) ↦
      (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1))
    p.support ≤
  p.natDegree - n
Tactic: 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, and_imp,
        tsub_le_iff_right, mem_support_iff, Ne, Finset.mem_filter]
      intro x hx hx'
      have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
      grind
    · simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
rw :
  natDegree (R := R) (p.sum fun (i : ℕ) (r : R) ↦ (monomial (i - n) : (a : R) → R[X]) ((↑(i.choose n) : R) * r)) ≤
    p.natDegree - n
rw₁ rw₂ rw₃ :
  natDegree.{u_1} (R := R)
      (∑ n_1 ∈ p.support, (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1)) ≤
    p.natDegree - n
rw₄ :
  Finset.fold max 0
      (Function.comp.{1, u_1 + 1, 1} (β := R[X]) natDegree fun (n_1 : ℕ) ↦
        (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1))
      p.support ≤
    p.natDegree - n
⊢ natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) p) ≤ p.natDegree - n
have rw₅ : Finset.fold max 0 (fun (x : ℕ) ↦ if (↑(x.choose n) : R) * p.coeff x = 0 then 0 else x - n) p.support ≤ p.natDegree - n
Tactic: 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, and_imp,
        tsub_le_iff_right, mem_support_iff, Ne, Finset.mem_filter]
      intro x hx hx'
      have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
      grind
    · simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
rw :
  natDegree (R := R) (p.sum fun (i : ℕ) (r : R) ↦ (monomial (i - n) : (a : R) → R[X]) ((↑(i.choose n) : R) * r)) ≤
    p.natDegree - n
rw₁ rw₂ rw₃ :
  natDegree.{u_1} (R := R)
      (∑ n_1 ∈ p.support, (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1)) ≤
    p.natDegree - n
rw₄ :
  Finset.fold max 0
      (Function.comp.{1, u_1 + 1, 1} (β := R[X]) natDegree fun (n_1 : ℕ) ↦
        (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1))
      p.support ≤
    p.natDegree - n
rw₅ :
  Finset.fold max 0 (fun (x : ℕ) ↦ if (↑(x.choose n) : R) * p.coeff x = 0 then 0 else x - n) p.support ≤ p.natDegree - n
⊢ natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) p) ≤ p.natDegree - n
have rw₆ : max (if {x ∈ p.support | (↑(x.choose n) : R) * p.coeff x = 0} = ∅ then 0 else max 0 0)
    (Finset.fold max 0 (fun (x : ℕ) ↦ x - n) ({i ∈ p.support | ¬(↑(i.choose n) : R) * p.coeff i = 0})) ≤
  p.natDegree - n
Tactic: 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, and_imp,
        tsub_le_iff_right, mem_support_iff, Ne, Finset.mem_filter]
      intro x hx hx'
      have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
      grind
    · simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
rw :
  natDegree (R := R) (p.sum fun (i : ℕ) (r : R) ↦ (monomial (i - n) : (a : R) → R[X]) ((↑(i.choose n) : R) * r)) ≤
    p.natDegree - n
rw₁ rw₂ rw₃ :
  natDegree.{u_1} (R := R)
      (∑ n_1 ∈ p.support, (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1)) ≤
    p.natDegree - n
rw₄ :
  Finset.fold max 0
      (Function.comp.{1, u_1 + 1, 1} (β := R[X]) natDegree fun (n_1 : ℕ) ↦
        (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1))
      p.support ≤
    p.natDegree - n
rw₅ :
  Finset.fold max 0 (fun (x : ℕ) ↦ if (↑(x.choose n) : R) * p.coeff x = 0 then 0 else x - n) p.support ≤ p.natDegree - n
rw₆ :
  max (if {x ∈ p.support | (↑(x.choose n) : R) * p.coeff x = 0} = ∅ then 0 else max 0 0)
      (Finset.fold max 0 (fun (x : ℕ) ↦ x - n) ({i ∈ p.support | ¬(↑(i.choose n) : R) * p.coeff i = 0})) ≤
    p.natDegree - n
⊢ natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) p) ≤ p.natDegree - n
have h : Eq (α := ℕ) (max 0 (max 0 0)) (max 0 0)
Tactic: 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, and_imp,
        tsub_le_iff_right, mem_support_iff, Ne, Finset.mem_filter]
      intro x hx hx'
      have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
      grind
    · simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ Eq (α := R[X]) ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
have this : natDegree.{u_1} (R := R) ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f) ≤ 0
Tactic: have : _ ≤ 0 := Nat.sub_self f.natDegree ▸ natDegree_hasseDeriv_le ..