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 n : ℕ
r : R
i : ℕ
pos :
  ∀ (hnik : n = i + k),
    ((↑((i + k).choose k) : R) * if n = i + k then r else 0) = if n - k = i then (↑(n.choose k) : R) * r else 0
⊢ ((↑((i + k).choose k) : R) * if n = i + k then r else 0) = if n - k = i then (↑(n.choose k) : R) * r else 0
have neg : ∀ (hnik : ¬n = i + k),
  ((↑((i + k).choose k) : R) * if n = i + k then r else 0) = if n - k = i then (↑(n.choose k) : R) * r else 0
Tactic: by_cases hnik : n = i + k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ ((↑((i + k).choose k) : R) * if n = i + k then r else 0) = if n - k = i then (↑(n.choose k) : R) * r else 0
have neg : 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
Tactic: rw [if_neg hnik, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
have pos : ∀ (hkn : k ≤ n), 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
Tactic: by_cases! hkn : k ≤ n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
pos : ∀ (hkn : k ≤ n), 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
⊢ 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
have neg : ∀ (hkn : n < k), 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
Tactic: by_cases! hkn : k ≤ n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : k ≤ n
⊢ 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
have hnik₁ : ¬n - k = i
Tactic: rw [← tsub_eq_iff_eq_add_of_le hkn] at hnik
Cleared hypotheses: hnik, hkn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n - k = i
hkn : k ≤ n
⊢ 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
have pos : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [if_neg hnik]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
⊢ 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
have neg : 0 = if n - k = i then (↑0 : R) * r else 0
Tactic: rw [Nat.choose_eq_zero_of_lt hkn, Nat.cast_zero, zero_mul, ite_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
neg : 0 = if n - k = i then (↑0 : R) * r else 0
⊢ 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
have neg₁ : 0 = if n - k = i then 0 * r else 0
Tactic: rw [Nat.choose_eq_zero_of_lt hkn, Nat.cast_zero, zero_mul, ite_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
neg : 0 = if n - k = i then (↑0 : R) * r else 0
neg₁ : 0 = if n - k = i then 0 * r else 0
⊢ 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
have neg₂ : Eq.{u_1 + 1} (α := R) 0 (if n - k = i then 0 else 0)
Tactic: rw [Nat.choose_eq_zero_of_lt hkn, Nat.cast_zero, zero_mul, ite_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
neg : 0 = if n - k = i then (↑0 : R) * r else 0
neg₁ : 0 = if n - k = i then 0 * r else 0
neg₂ : Eq.{u_1 + 1} (α := R) 0 (if n - k = i then 0 else 0)
⊢ 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
have neg₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [Nat.choose_eq_zero_of_lt hkn, Nat.cast_zero, zero_mul, ite_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
r : R
hk : 0 < k
⊢ Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) (0 : R[X])
have rw : Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 0 : (a : R) → R[X]) r) : R[X]) (0 : R[X])
Tactic: rw [← monomial_zero_left, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
r : R
hk : 0 < k
rw : Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 0 : (a : R) → R[X]) r) : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) (0 : R[X])
have rw₁ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) ((↑(choose 0 k) : R) * r) : R[X]) (0 : R[X])
Tactic: rw [← monomial_zero_left, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
r : R
hk : 0 < k
rw : Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 0 : (a : R) → R[X]) r) : R[X]) (0 : R[X])
rw₁ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) ((↑(choose 0 k) : R) * r) : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) (0 : R[X])
have rw₂ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) ((↑0 : R) * r) : R[X]) (0 : R[X])
Tactic: rw [← monomial_zero_left, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
r : R
hk : 0 < k
rw : Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 0 : (a : R) → R[X]) r) : R[X]) (0 : R[X])
rw₁ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) ((↑(choose 0 k) : R) * r) : R[X]) (0 : R[X])
rw₂ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) ((↑0 : R) * r) : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) (0 : R[X])
have rw₃ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) (0 * r) : R[X]) (0 : R[X])
Tactic: rw [← monomial_zero_left, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
r : R
hk : 0 < k
rw : Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 0 : (a : R) → R[X]) r) : R[X]) (0 : R[X])
rw₁ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) ((↑(choose 0 k) : R) * r) : R[X]) (0 : R[X])
rw₂ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) ((↑0 : R) * r) : R[X]) (0 : R[X])
rw₃ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) (0 * r) : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) (0 : R[X])
have rw₄ : Eq.{u_1 + 1} (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) 0) 0
Tactic: rw [← monomial_zero_left, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
r : R
hk : 0 < k
rw : Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 0 : (a : R) → R[X]) r) : R[X]) (0 : R[X])
rw₁ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) ((↑(choose 0 k) : R) * r) : R[X]) (0 : R[X])
rw₂ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) ((↑0 : R) * r) : R[X]) (0 : R[X])
rw₃ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) (0 * r) : R[X]) (0 : R[X])
rw₄ : Eq.{u_1 + 1} (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) 0) 0
⊢ Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) (0 : R[X])
have rw₅ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [← monomial_zero_left, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
hk : 0 < k
⊢ Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) 1) 0
have rw : Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) 1) : R[X]) (0 : R[X])
Tactic: rw [← C_1, hasseDeriv_C k _ hk]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
hk : 0 < k
rw : Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) 1) : R[X]) (0 : R[X])
⊢ Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) 1) 0
have rw₁ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [← C_1, hasseDeriv_C k _ hk]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
hk : 1 < k
⊢ Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) X : R[X]) (0 : R[X])
have rw : Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 1 : (a : R) → R[X]) 1) : R[X]) (0 : R[X])
Tactic: rw [← monomial_one_one_eq_X, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
hk : 1 < k
rw : Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 1 : (a : R) → R[X]) 1) : R[X]) (0 : R[X])
⊢ Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) X : R[X]) (0 : R[X])
have rw₁ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) (↑(choose 1 k) : R) 1) : R[X]) (0 : R[X])
Tactic: rw [← monomial_one_one_eq_X, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
hk : 1 < k
rw : Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 1 : (a : R) → R[X]) 1) : R[X]) (0 : R[X])
rw₁ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) (↑(choose 1 k) : R) 1) : R[X]) (0 : R[X])
⊢ Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) X : R[X]) (0 : R[X])
have rw₂ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) (↑0 : R) 1) : R[X]) (0 : R[X])
Tactic: rw [← monomial_one_one_eq_X, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
hk : 1 < k
rw : Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 1 : (a : R) → R[X]) 1) : R[X]) (0 : R[X])
rw₁ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) (↑(choose 1 k) : R) 1) : R[X]) (0 : R[X])
rw₂ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) (↑0 : R) 1) : R[X]) (0 : R[X])
⊢ Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) X : R[X]) (0 : R[X])
have rw₃ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) 0 1) : R[X]) (0 : R[X])
Tactic: rw [← monomial_one_one_eq_X, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
hk : 1 < k
rw : Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 1 : (a : R) → R[X]) 1) : R[X]) (0 : R[X])
rw₁ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) (↑(choose 1 k) : R) 1) : R[X]) (0 : R[X])
rw₂ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) (↑0 : R) 1) : R[X]) (0 : R[X])
rw₃ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) 0 1) : R[X]) (0 : R[X])
⊢ Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) X : R[X]) (0 : R[X])
have rw₄ : Eq.{u_1 + 1} (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) 0) 0
Tactic: rw [← monomial_one_one_eq_X, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
hk : 1 < k
rw : Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 1 : (a : R) → R[X]) 1) : R[X]) (0 : R[X])
rw₁ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) (↑(choose 1 k) : R) 1) : R[X]) (0 : R[X])
rw₂ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) (↑0 : R) 1) : R[X]) (0 : R[X])
rw₃ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) 0 1) : R[X]) (0 : R[X])
rw₄ : Eq.{u_1 + 1} (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) 0) 0
⊢ Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) X : R[X]) (0 : R[X])
have rw₅ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [← monomial_one_one_eq_X, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
⊢ Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) 0! (hasseDeriv 0)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
have zero : Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) 0! LinearMap.id) : (a : R[X]) → R[X])
  (⇑derivative : (a : R[X]) → R[X])^[0]
Tactic: rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
zero :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) 0! LinearMap.id) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
⊢ Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) 0! (hasseDeriv 0)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
have zero₁ : Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (α := ℕ) (β := R[X] →ₗ[R] R[X]) 1 LinearMap.id) : (a : R[X]) → R[X])
  (⇑derivative : (a : R[X]) → R[X])^[0]
Tactic: rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
zero :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) 0! LinearMap.id) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
zero₁ :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (α := ℕ) (β := R[X] →ₗ[R] R[X]) 1 LinearMap.id) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
⊢ Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) 0! (hasseDeriv 0)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
have zero₂ : Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (α := ℕ) (β := R[X] →ₗ[R] R[X]) 1 LinearMap.id) : (a : R[X]) → R[X]) id
Tactic: rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
zero :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) 0! LinearMap.id) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
zero₁ :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (α := ℕ) (β := R[X] →ₗ[R] R[X]) 1 LinearMap.id) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
zero₂ :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (α := ℕ) (β := R[X] →ₗ[R] R[X]) 1 LinearMap.id) : (a : R[X]) → R[X]) id
⊢ Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) 0! (hasseDeriv 0)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
have zero₃ : Eq.{u_1 + 1} (α := (a : R[X]) → R[X]) (⇑LinearMap.id : (a : R[X]) → R[X]) id
Tactic: rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
zero :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) 0! LinearMap.id) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
zero₁ :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (α := ℕ) (β := R[X] →ₗ[R] R[X]) 1 LinearMap.id) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
zero₂ :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (α := ℕ) (β := R[X] →ₗ[R] R[X]) 1 LinearMap.id) : (a : R[X]) → R[X]) id
zero₃ : Eq.{u_1 + 1} (α := (a : R[X]) → R[X]) (⇑LinearMap.id : (a : R[X]) → R[X]) id
⊢ Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) 0! (hasseDeriv 0)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
have zero₄ : Eq.{u_1 + 1} (α := (a : R[X]) → R[X]) id id
Tactic: rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
⊢ 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]
have succ : ∀ (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]),
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) (k + 1)! (hasseDeriv (k + 1))) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k + 1]
Tactic: induction k with
  | zero => rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]
  | succ k ih => ?_
-- 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]
⊢ Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) (k + 1)! (hasseDeriv (k + 1))) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k + 1]
have succ : ∀ (f : R[X]) (n : ℕ),
  coeff ((HSMul.hSMul (β := R[X] →ₗ[R] R[X]) (k + 1)! (hasseDeriv (k + 1)) : (a : R[X]) → R[X]) f) n =
    ((⇑derivative : (a : R[X]) → R[X])^[k + 1] f).coeff n
Tactic: ext f n : 2
-- 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 : ℕ
⊢ coeff ((HSMul.hSMul (β := R[X] →ₗ[R] R[X]) (k + 1)! (hasseDeriv (k + 1)) : (a : R[X]) → R[X]) f) n =
    ((⇑derivative : (a : R[X]) → R[X])^[k + 1] f).coeff n
have succ : 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: rw [iterate_succ_apply', ← ih]
-- 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 : ℕ
⊢ 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)
have 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)
Tactic: simp only [LinearMap.smul_apply, coeff_smul, LinearMap.map_smul_of_tower, coeff_derivative,
    hasseDeriv_coeff, ← @choose_symm_add _ k]
-- 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 + 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)
have 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)))
Tactic: simp only [nsmul_eq_mul, factorial_succ, mul_assoc, succ_eq_add_one, ← add_assoc,
    add_right_comm n 1 k, ← cast_succ]
-- 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 + 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)))
have 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)))
Tactic: rw [← (cast_commute (n + 1) (f.coeff (n + k + 1))).eq]
-- 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 + 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)))
have 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)
Tactic: simp only [← mul_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 : ℕ
⊢ 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)
have 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)
Tactic: norm_cast
-- 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 + 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)
have succ : (k + 1) * k ! * (n + k + 1).choose (k + 1) = k ! * (n + k + 1).choose (n + 1) * (n + 1)
Tactic: congr 2
-- 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 + 1) * k ! * (n + k + 1).choose (k + 1) = k ! * (n + k + 1).choose (n + 1) * (n + 1)
have succ : k ! * ((k + 1) * (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]