awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
⊢ (derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))
have rw : (derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))
Tactic: rw [C_mul_X_pow_eq_monomial, C_mul_X_pow_eq_monomial, derivative_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
rw :
  (derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))
⊢ (derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))
have rw₁ : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a) : R[X])
  ((monomial (n - 1) : (a : R) → R[X]) (a * (↑n : R)) : R[X])
Tactic: rw [C_mul_X_pow_eq_monomial, C_mul_X_pow_eq_monomial, derivative_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
rw :
  (derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))
rw₁ :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a) : R[X])
    ((monomial (n - 1) : (a : R) → R[X]) (a * (↑n : R)) : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))
have rw₂ : Eq (α := R[X]) ((monomial (n - 1) : (a : R) → R[X]) (a * (↑n : R)) : R[X])
  ((monomial (n - 1) : (a : R) → R[X]) (a * (↑n : R)) : R[X])
Tactic: rw [C_mul_X_pow_eq_monomial, C_mul_X_pow_eq_monomial, derivative_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
⊢ (derivative : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X
have rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑2 : R)) : R[X]) (HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1)) =
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X
Tactic: rw [derivative_C_mul_X_pow, Nat.cast_two, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑2 : R)) : R[X])
      (HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X
⊢ (derivative : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X
have rw₁ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) (HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1)) =
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X
Tactic: rw [derivative_C_mul_X_pow, Nat.cast_two, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑2 : R)) : R[X])
      (HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X
rw₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) (HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X
⊢ (derivative : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X
have rw₂ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X =
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X
Tactic: rw [derivative_C_mul_X_pow, Nat.cast_two, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ (derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X n) =
    (C : (a : R) → R[X]) (↑n : R) * HPow.hPow (α := R[X]) X (n - 1)
have h : HPow.hPow (α := R[X]) X n = (C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) X n
Tactic: convert! derivative_C_mul_X_pow (1 : R) n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
h : HPow.hPow (α := R[X]) X n = (C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) X n
⊢ (derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X n) =
    (C : (a : R) → R[X]) (↑n : R) * HPow.hPow (α := R[X]) X (n - 1)
have h₁ : (↑n : R) = HMul.hMul (α := R) 1 (↑n : R)
Tactic: convert! derivative_C_mul_X_pow (1 : R) n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
⊢ (derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X
have rw : (C : (a : R) → R[X]) (↑2 : R) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X
Tactic: rw [derivative_X_pow, Nat.cast_two, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
rw :
  (C : (a : R) → R[X]) (↑2 : R) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X
⊢ (derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X
have rw₁ : (C : (a : R) → R[X]) 2 * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X
Tactic: rw [derivative_X_pow, Nat.cast_two, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
rw :
  (C : (a : R) → R[X]) (↑2 : R) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X
rw₁ :
  (C : (a : R) → R[X]) 2 * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X
⊢ (derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X
have rw₂ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X
Tactic: rw [derivative_X_pow, Nat.cast_two, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 0
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
have rw : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) (p.coeff 0)) : R[X]) (0 : R[X])
Tactic: rw [eq_C_of_natDegree_eq_zero hp, derivative_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 0
rw : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) (p.coeff 0)) : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
have rw₁ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [eq_C_of_natDegree_eq_zero hp, derivative_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
c : R
⊢ Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X])
    (1 : R[X])
have rw : HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) X : R[X])
    ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) =
  1
Tactic: rw [derivative_add, derivative_X, derivative_C, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
c : R
rw :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) X : R[X])
      ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) =
    1
⊢ Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X])
    (1 : R[X])
have rw₁ : HAdd.hAdd (α := R[X]) (β := R[X]) (1 : R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) = 1
Tactic: rw [derivative_add, derivative_X, derivative_C, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
c : R
rw :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) X : R[X])
      ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) =
    1
rw₁ :
  HAdd.hAdd (α := R[X]) (β := R[X]) (1 : R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) = 1
⊢ Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X])
    (1 : R[X])
have rw₂ : HAdd.hAdd (α := R[X]) 1 0 = 1
Tactic: rw [derivative_add, derivative_X, derivative_C, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
c : R
rw :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) X : R[X])
      ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) =
    1
rw₁ :
  HAdd.hAdd (α := R[X]) (β := R[X]) (1 : R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) = 1
rw₂ : HAdd.hAdd (α := R[X]) 1 0 = 1
⊢ Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X])
    (1 : R[X])
have rw₃ : Eq.{u + 1} (α := R[X]) 1 1
Tactic: rw [derivative_add, derivative_X, derivative_C, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
ι : Type y
inst : Semiring R
k : ℕ
s : Finset ι
f : ι → R[X]
⊢ Eq.{u + 1} (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (∑ b ∈ s, f b))
    (∑ b ∈ s, (⇑derivative : (a : R[X]) → R[X])^[k] (f b))
have simp_rw : Eq (α := R[X]) ((HPow.hPow (α := Module.End R R[X]) derivative k : (a : R[X]) → R[X]) (∑ b ∈ s, f b))
  (∑ x ∈ s, (HPow.hPow (α := Module.End R R[X]) derivative k : (a : R[X]) → R[X]) (f x))
Tactic: simp_rw [← Module.End.pow_apply, map_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p : R[X]
k : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (s • p) = s • (⇑derivative : (a : R[X]) → R[X])^[k] p
have zero : ∀ (p : R[X]), (⇑derivative : (a : R[X]) → R[X])^[0] (s • p) = s • (⇑derivative : (a : R[X]) → R[X])^[0] p
Tactic: induction k generalizing p with
  | zero => simp
  | succ k ih => simp [ih]
Cleared hypotheses: p, k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p : R[X]
k : ℕ
zero : ∀ (p : R[X]), (⇑derivative : (a : R[X]) → R[X])^[0] (s • p) = s • (⇑derivative : (a : R[X]) → R[X])^[0] p
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (s • p) = s • (⇑derivative : (a : R[X]) → R[X])^[k] p
have succ : ∀ (k : ℕ)
  (ih : ∀ (p : R[X]), (⇑derivative : (a : R[X]) → R[X])^[k] (s • p) = s • (⇑derivative : (a : R[X]) → R[X])^[k] p)
  (p : R[X]), (⇑derivative : (a : R[X]) → R[X])^[k + 1] (s • p) = s • (⇑derivative : (a : R[X]) → R[X])^[k + 1] p
Tactic: induction k generalizing p with
  | zero => simp
  | succ k ih => simp [ih]
Cleared hypotheses: p, k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
p : R[X]
k : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] p)
have simp_rw : (⇑derivative : (a : R[X]) → R[X])^[k] (a • p) = a • (⇑derivative : (a : R[X]) → R[X])^[k] p
Tactic: simp_rw [← smul_eq_C_mul, iterate_derivative_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n ∈ support.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p)
h1 : p.coeff (n + 1) = 0
⊢ Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) p) n) 0
have rw : p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1 = 0
Tactic: rw [coeff_derivative, h1, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n ∈ support.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p)
h1 : p.coeff (n + 1) = 0
rw : p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1 = 0
⊢ Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) p) n) 0
have rw₁ : 0 * HAdd.hAdd (α := R) (↑n : R) 1 = 0
Tactic: rw [coeff_derivative, h1, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n ∈ support.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p)
h1 : p.coeff (n + 1) = 0
rw : p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1 = 0
rw₁ : 0 * HAdd.hAdd (α := R) (↑n : R) 1 = 0
⊢ Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) p) n) 0
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [coeff_derivative, h1, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
this : DecidableEq R := Classical.decEq R
H : p = 0
⊢ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) = p.degree
have rw : degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) 0) = degree.{u} (R := R) 0
Tactic: rw [H, derivative_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
this : DecidableEq R := Classical.decEq R
H : p = 0
rw : degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) 0) = degree.{u} (R := R) 0
⊢ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) = p.degree
have rw₁ : degree.{u} (R := R) 0 = degree.{u} (R := R) 0
Tactic: rw [H, derivative_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree
have inl : ∀ (hp' : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])),
  natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree
Tactic: rcases eq_or_ne (derivative p) 0 with hp' | hp'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
inl :
  ∀ (hp' : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])),
    natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree
have inr : ∀ (hp' : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])),
  natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree
Tactic: rcases eq_or_ne (derivative p) 0 with hp' | hp'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree
have inl : 0 < p.natDegree
Tactic: rw [hp', Polynomial.natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree
have inr : degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.degree
Tactic: rw [natDegree_lt_natDegree_iff hp']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ p.natDegree - 1
have pos : ∀ (p0 : p.natDegree = 0), natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ p.natDegree - 1
Tactic: by_cases p0 : p.natDegree = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
pos : ∀ (p0 : p.natDegree = 0), natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ p.natDegree - 1
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ p.natDegree - 1
have neg : ∀ (p0 : ¬p.natDegree = 0), natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ p.natDegree - 1
Tactic: by_cases p0 : p.natDegree = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ ((⇑derivative : (a : R[X]) → R[X])^[0] p).natDegree ≤ p.natDegree - 0
have zero : p.natDegree ≤ p.natDegree - 0
Tactic: rw [Function.iterate_zero_apply, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
zero : p.natDegree ≤ p.natDegree - 0
⊢ ((⇑derivative : (a : R[X]) → R[X])^[0] p).natDegree ≤ p.natDegree - 0
have zero₁ : p.natDegree ≤ p.natDegree
Tactic: rw [Function.iterate_zero_apply, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
d : ℕ
hd : ((⇑derivative : (a : R[X]) → R[X])^[d] p).natDegree ≤ p.natDegree - d
⊢ ((⇑derivative : (a : R[X]) → R[X])^[d + 1] p).natDegree ≤ p.natDegree - (d + 1)
have succ : natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[d] p)) ≤
  p.natDegree - d - 1
Tactic: rw [Function.iterate_succ_apply', Nat.sub_succ']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
⊢ ((⇑derivative : (a : R[X]) → R[X])^[k] p).natDegree ≤ p.natDegree - k
have zero : ((⇑derivative : (a : R[X]) → R[X])^[0] p).natDegree ≤ p.natDegree - 0
Tactic: induction k with
  | zero => rw [Function.iterate_zero_apply, Nat.sub_zero]
  | succ d hd =>
      rw [Function.iterate_succ_apply', Nat.sub_succ']
      exact (natDegree_derivative_le _).trans <| Nat.sub_le_sub_right hd 1
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
zero : ((⇑derivative : (a : R[X]) → R[X])^[0] p).natDegree ≤ p.natDegree - 0
⊢ ((⇑derivative : (a : R[X]) → R[X])^[k] p).natDegree ≤ p.natDegree - k
have succ : ∀ (d : ℕ) (hd : ((⇑derivative : (a : R[X]) → R[X])^[d] p).natDegree ≤ p.natDegree - d),
  ((⇑derivative : (a : R[X]) → R[X])^[d + 1] p).natDegree ≤ p.natDegree - (d + 1)
Tactic: induction k with
  | zero => rw [Function.iterate_zero_apply, Nat.sub_zero]
  | succ d hd =>
      rw [Function.iterate_succ_apply', Nat.sub_succ']
      exact (natDegree_derivative_le _).trans <| Nat.sub_le_sub_right hd 1
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) (↑n : R[X])) 0
have rw : Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) (↑n : R)) : R[X]) (0 : R[X])
Tactic: rw [← map_natCast C n]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : ℕ
hx : p.natDegree < x
⊢ (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
have h : ∀ (n : ℕ)
  (ih :
    ∀ m < n,
      ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0)
  {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = n), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
Tactic: induction h : p.natDegree using Nat.strong_induction_on generalizing p x with | _ _ ih
Cleared hypotheses: p, x, hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : Semiring R
n : ℕ
ih :
  ∀ m < n,
    ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
p : R[X]
x : ℕ
hx : p.natDegree < x
h : p.natDegree = n
⊢ (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
have ih₁ : ∀ m < p.natDegree,
  ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
Tactic: subst h
Cleared hypotheses: n, ih, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : ℕ
hx : p.natDegree < x
ih :
  ∀ m < p.natDegree,
    ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
⊢ (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
have h : ∀ (t : ℕ) (hx : p.natDegree < t.succ), (⇑derivative : (a : R[X]) → R[X])^[t.succ] p = 0
Tactic: obtain ⟨t, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (pos_of_gt hx).ne'
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
ih :
  ∀ m < p.natDegree,
    ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
⊢ (⇑derivative : (a : R[X]) → R[X])^[t.succ] p = 0
have h : Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])
Tactic: rw [Function.iterate_succ_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
ih :
  ∀ m < p.natDegree,
    ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])
have pos : ∀ (hp : p.natDegree = 0),
  Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])
Tactic: by_cases hp : p.natDegree = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
ih :
  ∀ m < p.natDegree,
    ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
pos :
  ∀ (hp : p.natDegree = 0),
    Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])
have neg : ∀ (hp : ¬p.natDegree = 0),
  Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])
Tactic: by_cases hp : p.natDegree = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
ih :
  ∀ m < p.natDegree,
    ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : p.natDegree = 0
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])
have pos : Eq.{u + 1} (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] 0) 0
Tactic: rw [derivative_of_natDegree_zero hp, iterate_derivative_zero]