awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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 : ℕ
succ :
  (k + 1)! • ((↑((n + (k + 1)).choose (k + 1)) : R) * f.coeff (n + (k + 1))) =
    k ! • ((↑((n + 1 + k).choose (n + 1)) : R) * f.coeff (n + 1 + k) * HAdd.hAdd (α := R) (↑n : R) 1)
⊢ Eq.{u_1 + 1} (α := R)
    (coeff ((HSMul.hSMul (β := R[X] →ₗ[R] R[X]) (k + 1)! (hasseDeriv (k + 1)) : (a : R[X]) → R[X]) f) n)
    (coeff
      ((derivative : (a : R[X]) → R[X]) ((HSMul.hSMul (β := R[X] →ₗ[R] R[X]) k ! (hasseDeriv k) : (a : R[X]) → R[X]) f))
      n)

Tactic:
simp only [LinearMap.smul_apply, coeff_smul, LinearMap.map_smul_of_tower, coeff_derivative,
    hasseDeriv_coeff, ← @choose_symm_add _ k]

Premises used: Polynomial.coeff_derivative, LinearMap.smul_apply, Polynomial.hasseDeriv_coeff, Nat.choose_symm_add, Polynomial.coeff_smul, LinearMap.map_smul_of_tower
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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 : ℕ
succ :
  (↑((k + 1) * k !) : R) * ((↑((n + k + 1).choose (k + 1)) : R) * f.coeff (n + k + 1)) =
    (↑k ! : R) * ((↑((n + k + 1).choose (n + 1)) : R) * (f.coeff (n + k + 1) * (↑(n + 1) : R)))
⊢ (k + 1)! • ((↑((n + (k + 1)).choose (k + 1)) : R) * f.coeff (n + (k + 1))) =
    k ! • ((↑((n + 1 + k).choose (n + 1)) : R) * f.coeff (n + 1 + k) * HAdd.hAdd (α := R) (↑n : R) 1)

Tactic:
simp only [nsmul_eq_mul, factorial_succ, mul_assoc, succ_eq_add_one, ← add_assoc,
    add_right_comm n 1 k, ← cast_succ]

Premises used: Nat.cast_succ, Nat.succ_eq_add_one, Nat.factorial_succ, add_assoc, mul_assoc, add_right_comm, nsmul_eq_mul, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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 : ℕ
succ :
  (↑((k + 1) * k !) : R) * ((↑((n + k + 1).choose (k + 1)) : R) * f.coeff (n + k + 1)) =
    (↑k ! : R) * ((↑((n + k + 1).choose (n + 1)) : R) * ((↑(n + 1) : R) * f.coeff (n + k + 1)))
⊢ (↑((k + 1) * k !) : R) * ((↑((n + k + 1).choose (k + 1)) : R) * f.coeff (n + k + 1)) =
    (↑k ! : R) * ((↑((n + k + 1).choose (n + 1)) : R) * (f.coeff (n + k + 1) * (↑(n + 1) : R)))

Tactic:
rw [← (cast_commute (n + 1) (f.coeff (n + k + 1))).eq]

Premises used: Polynomial.coeff, HAdd.hAdd, OfNat.ofNat, Commute.eq, Nat.cast_commute
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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 : ℕ
succ :
  HMul.hMul (α := R) (↑((k + 1) * k !) : R) (↑((n + k + 1).choose (k + 1)) : R) * f.coeff (n + k + 1) =
    HMul.hMul (α := R) (↑k ! : R) (↑((n + k + 1).choose (n + 1)) : R) * (↑(n + 1) : R) * f.coeff (n + k + 1)
⊢ (↑((k + 1) * k !) : R) * ((↑((n + k + 1).choose (k + 1)) : R) * f.coeff (n + k + 1)) =
    (↑k ! : R) * ((↑((n + k + 1).choose (n + 1)) : R) * ((↑(n + 1) : R) * f.coeff (n + k + 1)))

Tactic:
simp only [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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 : ℕ
succ :
  (↑((k + 1) * k ! * (n + k + 1).choose (k + 1)) : R) * f.coeff (n + k + 1) =
    (↑(k ! * (n + k + 1).choose (n + 1) * (n + 1)) : R) * f.coeff (n + k + 1)
⊢ HMul.hMul (α := R) (↑((k + 1) * k !) : R) (↑((n + k + 1).choose (k + 1)) : R) * f.coeff (n + k + 1) =
    HMul.hMul (α := R) (↑k ! : R) (↑((n + k + 1).choose (n + 1)) : R) * (↑(n + 1) : R) * f.coeff (n + k + 1)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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 : ℕ
succ : (k + 1) * k ! * (n + k + 1).choose (k + 1) = k ! * (n + k + 1).choose (n + 1) * (n + 1)
⊢ (↑((k + 1) * k ! * (n + k + 1).choose (k + 1)) : R) * f.coeff (n + k + 1) =
    (↑(k ! * (n + k + 1).choose (n + 1) * (n + 1)) : R) * f.coeff (n + k + 1)

Tactic:
congr 2
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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 : ℕ
succ : k ! * ((k + 1) * (n + k + 1).choose (k + 1)) = k ! * ((n + k + 1).choose (n + 1) * (n + 1))
⊢ (k + 1) * k ! * (n + k + 1).choose (k + 1) = k ! * (n + k + 1).choose (n + 1) * (n + 1)

Tactic:
rw [mul_comm (k + 1) _, mul_assoc, mul_assoc]

Premises used: mul_assoc, HAdd.hAdd, mul_comm, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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 : ℕ
succ : (k + 1) * (n + k + 1).choose (k + 1) = (n + k + 1).choose (n + 1) * (n + 1)
⊢ k ! * ((k + 1) * (n + k + 1).choose (k + 1)) = k ! * ((n + k + 1).choose (n + 1) * (n + 1))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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 : ℕ
⊢ n + k + 1 = n + (k + 1)

Tactic:
apply add_assoc

Premises used: add_assoc
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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 : ℕ
⊢ n + k + 1 = n + (k + 1)

Tactic:
have : n + k + 1 = n + (k + 1) := by apply add_assoc
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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 : (n + k + 1).choose n * (k + 1) = (n + k + 1).choose n * (n + k + 1 - n)
⊢ (k + 1) * (n + k + 1).choose (k + 1) = (n + k + 1).choose (n + 1) * (n + 1)

Tactic:
rw [← choose_symm_of_eq_add this, choose_succ_right_eq, mul_comm]

Premises used: Nat.choose_succ_right_eq, mul_comm, Nat.choose_symm_of_eq_add
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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
⊢ (n + k + 1).choose n * (k + 1) = (n + k + 1).choose n * (n + k + 1 - n)

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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
succ₁ succ₂ : k + 1 = k + 1
⊢ k + 1 = n + k + 1 - n

Tactic:
rw [add_assoc, add_tsub_cancel_left]

Premises used: add_assoc, add_tsub_cancel_left
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k l : ℕ
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)
⊢ hasseDeriv k ∘ₗ hasseDeriv l = HSMul.hSMul (β := R[X] →ₗ[R] R[X]) ((k + l).choose k) (hasseDeriv (k + l))

Tactic:
ext i : 2
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
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])
⊢ 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:
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]

Premises used: LinearMap.smul_apply, Polynomial.smul_monomial, Polynomial.monomial_eq_zero_iff, Polynomial.sum_monomial_index, add_comm, MulZeroClass.mul_zero, LinearMap.coe_comp, Polynomial.hasseDeriv_apply, Function.comp_apply, tsub_add_eq_tsub_tsub, mul_one
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
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])
⊢ 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:
rw_mod_cast [nsmul_eq_mul]

Premises used: nsmul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
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))
⊢ 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 [← Nat.cast_mul]

Premises used: Nat.cast_mul
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
h : (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)
⊢ 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:
congr 2
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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)
neg : ∀ (hikl : k + l ≤ i), (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)

Tactic:
by_cases! hikl : i < k + l
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : i < k + l
pos : (i - l).choose k * i.choose l = 0
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

Tactic:
rw [choose_eq_zero_of_lt hikl, mul_zero]

Premises used: MulZeroClass.mul_zero, Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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
neg : ∀ (hil : l ≤ i), (i - l).choose k * i.choose l = 0
⊢ (i - l).choose k * i.choose l = 0

Tactic:
by_cases! hil : i < l
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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
pos₁ pos₂ : Eq (α := ℕ) 0 0
⊢ (i - l).choose k * i.choose l = 0

Tactic:
rw [choose_eq_zero_of_lt hil, mul_zero]

Premises used: MulZeroClass.mul_zero, Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : i < k + l
hil : l ≤ i
⊢ i - l < k

Tactic:
rw [← tsub_lt_iff_right hil] at hikl

Premises used: tsub_lt_iff_right
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : i < k + l
hil : l ≤ i
hikl₁ : i - l < k
⊢ l ≤ i

Tactic:
rw [← tsub_lt_iff_right hil] at hikl

Premises used: tsub_lt_iff_right
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
neg : 0 * i.choose l = 0
neg₁ neg₂ : Eq (α := ℕ) 0 0
⊢ (i - l).choose k * i.choose l = 0

Tactic:
rw [choose_eq_zero_of_lt hikl, zero_mul]

Premises used: MulZeroClass.zero_mul, Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : k + l ≤ i
neg : Eq (α := ℚ) (↑((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)

Tactic:
apply @cast_injective ℚ

Premises used: Nat.cast_injective
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : k + l ≤ i
⊢ l ≤ i

Tactic:
have h1 : l ≤ i := le_of_add_le_right hikl
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
⊢ k ≤ i - l

Tactic:
have h2 : k ≤ i - l := le_tsub_of_add_le_right hikl
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
⊢ k ≤ k + l

Tactic:
have h3 : k ≤ k + l := le_self_add
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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
neg :
  HMul.hMul (α := ℚ) (↑((i - l).choose k) : ℚ) (↑(i.choose l) : ℚ) =
    HMul.hMul (α := ℚ) (↑((k + l).choose k) : ℚ) (↑(i.choose (k + l)) : ℚ)
⊢ Eq (α := ℚ) (↑((i - l).choose k * i.choose l) : ℚ) (↑((k + l).choose k * i.choose (k + l)) : ℚ)

Tactic:
push_cast
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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
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))! : ℚ))
⊢ HMul.hMul (α := ℚ) (↑((i - l).choose k) : ℚ) (↑(i.choose l) : ℚ) =
    HMul.hMul (α := ℚ) (↑((k + l).choose k) : ℚ) (↑(i.choose (k + l)) : ℚ)

Tactic:
rw [cast_choose ℚ h1, cast_choose ℚ h2, cast_choose ℚ h3, cast_choose ℚ hikl]

Premises used: Rat, Nat.cast_choose
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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
rw : i - (l + k) = i - l - k
⊢ i - (k + l) = i - l - k

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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 + k) = i - l - k

Tactic:
apply tsub_add_eq_tsub_tsub

Premises used: tsub_add_eq_tsub_tsub
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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
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)! : ℚ))
⊢ (↑(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 [show i - (k + l) = i - l - k by rw [add_comm]; apply tsub_add_eq_tsub_tsub]
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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
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)! : ℚ))
⊢ (↑(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:
simp only [add_tsub_cancel_left]

Premises used: add_tsub_cancel_left
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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 ! : ℚ) (↑l ! : ℚ) *
      ((↑i ! : ℚ) / HMul.hMul (α := ℚ) (↑(k + l)! : ℚ) (↑(i - l - k)! : ℚ))

Tactic:
field
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
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

Tactic:
rw [hasseDeriv_apply, sum_def]

Premises used: Polynomial.sum_def, Polynomial.hasseDeriv_apply
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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

Tactic:
(natDegree_sum_le _ _).trans ?_

Premises used: Polynomial.natDegree_sum_le, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
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
⊢ 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:
refine (natDegree_sum_le _ _).trans ?_

Premises used: Polynomial.natDegree_sum_le, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
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
⊢ 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:
simp_rw [Function.comp, natDegree_monomial]

Premises used: Function.comp, Polynomial.natDegree_monomial
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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
h : Eq (α := ℕ) (max 0 (max 0 0)) (max 0 0)
⊢ 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:
rw [Finset.fold_ite, Finset.fold_const]

Premises used: Finset.fold_const, Finset.fold_ite
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
simp : ∀ (x : ℕ), ¬p.coeff x = 0 → ¬(↑(x.choose n) : R) * p.coeff x = 0 → x ≤ p.natDegree - n + 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

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]

Premises used: and_imp, ite_self, Polynomial.mem_support_iff, Ne, tsub_le_iff_right, Finset.fold_max_le, max_eq_right, zero_le', Finset.mem_filter, true_and
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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

Tactic:
have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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
hxp : x ≤ p.natDegree
⊢ x ≤ p.natDegree - n + n

Tactic:
grind
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ Eq (α := ℕ) (max 0 (max 0 0)) (max 0 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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
h h₁ : Eq (α := ℕ) (max 0 (max 0 0)) (max 0 0)
⊢ natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) p) ≤ 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

Premises used: Finset.fold_const, Polynomial.natDegree_sum_le, and_imp, ite_self, Function.comp, Polynomial.mem_support_iff, Ne, tsub_le_iff_right, Finset.fold_max_le, max_eq_right, Polynomial.natDegree_monomial, Finset.fold_ite, Polynomial.sum_def, zero_le', Polynomial.hasseDeriv_apply, Finset.mem_filter, LE.le.trans, true_and
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ 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 ..