awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
pos : Eq.{u + 1} (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] 0) 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]) 0 0
Tactic: rw [derivative_of_natDegree_zero hp, iterate_derivative_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
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 this : natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree
Tactic: have := natDegree_derivative_lt hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ f.natDegree = 0
have inl : ∀ (h : Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) 0) 0), natDegree.{u} (R := R) 0 = 0
Tactic: rcases eq_or_ne f 0 with (rfl | hf)
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
inl : ∀ (h : Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) 0) 0), natDegree.{u} (R := R) 0 = 0
⊢ f.natDegree = 0
have inr : ∀ (hf : f ≠ 0), f.natDegree = 0
Tactic: rcases eq_or_ne f 0 with (rfl | hf)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
⊢ f.natDegree = 0
have inr : f.degree ≤ 0
Tactic: rw [natDegree_eq_zero_iff_degree_le_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
⊢ f.degree ≤ 0
have inr : ∀ (f_nat_degree_pos : 0 < f.degree), False
Tactic: by_contra! f_nat_degree_pos
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
f_nat_degree_pos : 0 < f.degree
⊢ False
have f_nat_degree_pos₁ : 0 < f.natDegree
Tactic: rw [← natDegree_pos_iff_degree_pos] at f_nat_degree_pos
Cleared hypotheses: f_nat_degree_pos
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
⊢ False
have hm : m + 1 = f.natDegree
Tactic: have hm : m + 1 = f.natDegree := tsub_add_cancel_of_le f_nat_degree_pos
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
⊢ False
have h2 : coeff ((derivative : (a : R[X]) → R[X]) f) m = f.coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1
Tactic: have h2 := coeff_derivative f m
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : coeff ((derivative : (a : R[X]) → R[X]) f) m = f.coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1
⊢ False
have h₁ : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)
Tactic: rw [Polynomial.ext_iff] at h
Cleared hypotheses: h, hf, f_nat_degree_pos, m, hm, h2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : coeff ((derivative : (a : R[X]) → R[X]) f) m = f.coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1
⊢ False
have h2₁ : m + 1 = 0 ∨ f.coeff (m + 1) = 0
Tactic: rw [h m, coeff_zero, ← Nat.cast_add_one, ← nsmul_eq_mul', eq_comm, smul_eq_zero] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : m + 1 = 0 ∨ f.coeff (m + 1) = 0
⊢ False
have h2₁ : f.coeff (m + 1) = 0
Tactic: replace h2 := h2.resolve_left m.succ_ne_zero
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : f.coeff (m + 1) = 0
⊢ False
have h2₁ : f = 0
Tactic: rw [hm, ← leadingCoeff, leadingCoeff_eq_zero] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
f g : R[X]
⊢ (derivative : (a : R[X]) → R[X]) (f * g) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g +
      HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])
have monomial : ∀ (m : ℕ) (a : R),
  (derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((monomial m : (a : R) → R[X]) a : R[X]) g) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial m : (a : R) → R[X]) a) : R[X]) g +
      HMul.hMul (α := R[X]) (β := R[X]) ((monomial m : (a : R) → R[X]) a : R[X])
        ((derivative : (a : R[X]) → R[X]) g : R[X])
Tactic: induction f using Polynomial.induction_on' with
  | add => simp only [add_mul, map_add, add_assoc, add_left_comm, *]
  | monomial m a => ?_
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
g : R[X]
m : ℕ
a : R
⊢ (derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((monomial m : (a : R) → R[X]) a : R[X]) g) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial m : (a : R) → R[X]) a) : R[X]) g +
      HMul.hMul (α := R[X]) (β := R[X]) ((monomial m : (a : R) → R[X]) a : R[X])
        ((derivative : (a : R[X]) → R[X]) g : R[X])
have monomial : ∀ (n : ℕ) (b : R),
  (derivative : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((monomial m : (a : R) → R[X]) a : R[X])
        ((monomial n : (a : R) → R[X]) b : R[X])) =
    HMul.hMul (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial m : (a : R) → R[X]) a) : R[X])
        ((monomial n : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((monomial m : (a : R) → R[X]) a : R[X])
        ((derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) b) : R[X])
Tactic: induction g using Polynomial.induction_on' with
  | add => simp only [mul_add, map_add, add_assoc, add_left_comm, *]
  | monomial n b => ?_
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ (derivative : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((monomial m : (a : R) → R[X]) a : R[X])
        ((monomial n : (a : R) → R[X]) b : R[X])) =
    HMul.hMul (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial m : (a : R) → R[X]) a) : R[X])
        ((monomial n : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((monomial m : (a : R) → R[X]) a : R[X])
        ((derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) b) : R[X])
have monomial : (monomial (m + n - 1) : (a : R) → R[X]) (a * b * (↑(m + n) : R)) =
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial (m - 1 + n) : (a : R) → R[X]) (a * (↑m : R) * b) : R[X])
    ((monomial (m + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])
Tactic: simp only [monomial_mul_monomial, derivative_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ (monomial (m + n - 1) : (a : R) → R[X]) (a * b * (↑(m + n) : R)) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial (m - 1 + n) : (a : R) → R[X]) (a * (↑m : R) * b) : R[X])
      ((monomial (m + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])
have monomial : HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial (m + n - 1) : (a : R) → R[X]) (a * (b * (↑m : R))) : R[X])
    ((monomial (m + n - 1) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X]) =
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial (m - 1 + n) : (a : R) → R[X]) (a * (b * (↑m : R))) : R[X])
    ((monomial (m + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])
Tactic: simp only [mul_assoc, (Nat.cast_commute _ _).eq, Nat.cast_add, mul_add, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
b : R
m : ℕ
⊢ HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial (m + 1 + n - 1) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((monomial (m + 1 + n - 1) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial (m + 1 - 1 + n) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((monomial (m + 1 + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])
have monomial : HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial (m + 1 + 0 - 1) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
    ((monomial (m + 1 + 0 - 1) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X]) =
  HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial (m + 1 - 1 + 0) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
    ((monomial (m + 1 + HSub.hSub (α := ℕ) 0 1) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X])
Tactic: cases n with
  | zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
  | succ n => grind
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
b : R
m : ℕ
monomial :
  HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (m + 1 + 0 - 1) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((Polynomial.monomial (m + 1 + 0 - 1) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (m + 1 - 1 + 0) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((Polynomial.monomial (m + 1 + HSub.hSub (α := ℕ) 0 1) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X])
⊢ HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (m + 1 + n - 1) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((Polynomial.monomial (m + 1 + n - 1) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (m + 1 - 1 + n) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((Polynomial.monomial (m + 1 + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])
have monomial₁ : ∀ (n : ℕ),
  HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (m + 1 + (n + 1) - 1) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((Polynomial.monomial (m + 1 + (n + 1) - 1) : (a : R) → R[X]) (a * (b * (↑(n + 1) : R))) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (m + 1 - 1 + (n + 1)) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((Polynomial.monomial (m + 1 + (n + 1 - 1)) : (a : R) → R[X]) (a * (b * (↑(n + 1) : R))) : R[X])
Tactic: cases n with
  | zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
  | succ n => grind
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial (m + n - 1) : (a : R) → R[X]) (a * (b * (↑m : R))) : R[X])
      ((monomial (m + n - 1) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial (m - 1 + n) : (a : R) → R[X]) (a * (b * (↑m : R))) : R[X])
      ((monomial (m + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])
have monomial : HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial (0 + n - 1) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X])
    ((monomial (0 + n - 1) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X]) =
  HAdd.hAdd (α := R[X]) (β := R[X])
    ((monomial (HSub.hSub (α := ℕ) 0 1 + n) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X])
    ((monomial (0 + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])
Tactic: cases m with
  | zero => simp only [zero_add, Nat.cast_zero, mul_zero, map_zero]
  | succ m =>
  cases n with
  | zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
  | succ n => grind
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
m : ℕ
a : R
n : ℕ
b : R
monomial :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((Polynomial.monomial (0 + n - 1) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X])
      ((Polynomial.monomial (0 + n - 1) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (HSub.hSub (α := ℕ) 0 1 + n) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X])
      ((Polynomial.monomial (0 + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])
⊢ HAdd.hAdd (α := R[X]) (β := R[X]) ((Polynomial.monomial (m + n - 1) : (a : R) → R[X]) (a * (b * (↑m : R))) : R[X])
      ((Polynomial.monomial (m + n - 1) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((Polynomial.monomial (m - 1 + n) : (a : R) → R[X]) (a * (b * (↑m : R))) : R[X])
      ((Polynomial.monomial (m + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])
have monomial₁ : ∀ (m : ℕ),
  HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (m + 1 + n - 1) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((Polynomial.monomial (m + 1 + n - 1) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (m + 1 - 1 + n) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((Polynomial.monomial (m + 1 + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])
Tactic: cases m with
  | zero => simp only [zero_add, Nat.cast_zero, mul_zero, map_zero]
  | succ m =>
  cases n with
  | zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
  | succ n => grind
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
⊢ eval x ((derivative : (a : R[X]) → R[X]) p) = p.sum fun (n : ℕ) (a : R) ↦ a * (↑n : R) * x ^ (n - 1)
have simp_rw : eval x
    (p.sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
  p.sum fun (n : ℕ) (a : R) ↦ a * (↑n : R) * x ^ (n - 1)
Tactic: simp_rw [derivative_apply, eval_sum, eval_mul_X_pow, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
simp_rw :
  eval x
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    p.sum fun (n : ℕ) (a : R) ↦ a * (↑n : R) * x ^ (n - 1)
⊢ eval x ((derivative : (a : R[X]) → R[X]) p) = p.sum fun (n : ℕ) (a : R) ↦ a * (↑n : R) * x ^ (n - 1)
have simp_rw₁ : Eq (α := R)
  (p.sum fun (n : ℕ) (a : R) ↦
    eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))))
  (p.sum fun (n : ℕ) (a : R) ↦ a * (↑n : R) * x ^ (n - 1))
Tactic: simp_rw [derivative_apply, eval_sum, eval_mul_X_pow, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
simp_rw :
  eval x
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    p.sum fun (n : ℕ) (a : R) ↦ a * (↑n : R) * x ^ (n - 1)
simp_rw₁ :
  Eq (α := R)
    (p.sum fun (n : ℕ) (a : R) ↦
      eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))))
    (p.sum fun (n : ℕ) (a : R) ↦ a * (↑n : R) * x ^ (n - 1))
⊢ eval x ((derivative : (a : R[X]) → R[X]) p) = p.sum fun (n : ℕ) (a : R) ↦ a * (↑n : R) * x ^ (n - 1)
have simp_rw₂ : Eq (α := R) (p.sum fun (n : ℕ) (a : R) ↦ eval x ((C : (a : R) → R[X]) (a * (↑n : R))) * x ^ (n - 1))
  (p.sum fun (n : ℕ) (a : R) ↦ a * (↑n : R) * x ^ (n - 1))
Tactic: simp_rw [derivative_apply, eval_sum, eval_mul_X_pow, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ (derivative : (a : S[X]) → S[X]) (map f p) = map f ((derivative : (a : R[X]) → R[X]) p)
have rw : ((map f p).sum fun (n : ℕ) (a : S) ↦
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
  map f
    (p.sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
Tactic: rw [derivative_apply, derivative_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ((map f p).sum fun (n : ℕ) (a : S) ↦
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
    map f
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
have rw : ((map f p).sum fun (n : ℕ) (a : S) ↦
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
  map f
    (∑ a ∈ range (n + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))
Tactic: rw [sum_over_range' _ _ (n + 1) ((le_max_left _ _).trans_lt (lt_add_one _))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
rw :
  ((map f p).sum fun (n : ℕ) (a : S) ↦
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
    map f
      (∑ a ∈ range (n + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))
⊢ ((map f p).sum fun (n : ℕ) (a : S) ↦
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
    map f
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
have rw₁ : ∀ (n : ℕ),
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HMul.hMul (α := R) 0 (↑n : R)) : R[X])
      (HPow.hPow (α := R[X]) X (n - 1)) =
    0
Tactic: rw [sum_over_range' _ _ (n + 1) ((le_max_left _ _).trans_lt (lt_add_one _))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ((map f p).sum fun (n : ℕ) (a : S) ↦
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
    map f
      (∑ a ∈ range (n + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))
have rw : ∑ a ∈ range (n + 1),
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((map f p).coeff a * (↑a : S)) : S[X])
      (HPow.hPow (α := S[X]) X (a - 1)) =
  map f
    (∑ a ∈ range (n + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))
Tactic: rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
rw :
  ∑ a ∈ range (n + 1),
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((map f p).coeff a * (↑a : S)) : S[X])
        (HPow.hPow (α := S[X]) X (a - 1)) =
    map f
      (∑ a ∈ range (n + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))
⊢ ((map f p).sum fun (n : ℕ) (a : S) ↦
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
    map f
      (∑ a ∈ range (n + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))
have rw₁ : ∀ (n : ℕ),
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (HMul.hMul (α := S) 0 (↑n : S)) : S[X])
      (HPow.hPow (α := S[X]) X (n - 1)) =
    0
Tactic: rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ((map f p).sum fun (n : ℕ) (a : S) ↦
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
    map f
      (∑ a ∈ range (n + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))
have on_goal : ∑ a ∈ range (n + 1),
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((map f p).coeff a * (↑a : S)) : S[X])
      (HPow.hPow (α := S[X]) X (a - 1)) =
  map f
    (∑ a ∈ range (n + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))
Tactic: on_goal 1 => rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
on_goal :
  ∑ a ∈ range (n + 1),
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((map f p).coeff a * (↑a : S)) : S[X])
        (HPow.hPow (α := S[X]) X (a - 1)) =
    map f
      (∑ a ∈ range (n + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))
⊢ ((map f p).sum fun (n : ℕ) (a : S) ↦
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
    map f
      (∑ a ∈ range (n + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))
have on_goal₁ : ∀ (n : ℕ),
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (HMul.hMul (α := S) 0 (↑n : S)) : S[X])
      (HPow.hPow (α := S[X]) X (n - 1)) =
    0
Tactic: on_goal 1 => rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]