awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
q : R[X]
n : ℕ
a : R
⊢ (derivative : (a : R[X]) → R[X]) (comp ((monomial n : (a : R) → R[X]) a) q) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
      (comp ((derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a)) q)
have monomial : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
    (HMul.hMul (β := R[X]) ((↑n : R[X]) * q ^ (n - 1)) ((derivative : (a : R[X]) → R[X]) q : R[X])) =
  HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((↑n : R[X]) : R[X]) * q ^ (n - 1))
Tactic: simp only [derivative_pow, derivative_mul, monomial_comp, derivative_monomial, derivative_C,
      zero_mul, C_eq_natCast, zero_add, map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
r : R
⊢ (derivative : (a : R[X]) → R[X]) (eval₂ C q ((C : (a : R) → R[X]) r)) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw : (derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) =
  HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)))
    ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [eval₂_C, derivative_C, eval₂_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
r : R
rw :
  (derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (eval₂ C q ((C : (a : R) → R[X]) r)) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw₁ : 0 = HMul.hMul (β := R[X]) (eval₂ C q 0) ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [eval₂_C, derivative_C, eval₂_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
r : R
rw :
  (derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₁ : 0 = HMul.hMul (β := R[X]) (eval₂ C q 0) ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (eval₂ C q ((C : (a : R) → R[X]) r)) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw₂ : 0 = HMul.hMul (α := R[X]) (β := R[X]) (0 : R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [eval₂_C, derivative_C, eval₂_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
r : R
rw :
  (derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₁ : 0 = HMul.hMul (β := R[X]) (eval₂ C q 0) ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₂ : 0 = HMul.hMul (α := R[X]) (β := R[X]) (0 : R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (eval₂ C q ((C : (a : R) → R[X]) r)) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw₃ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [eval₂_C, derivative_C, eval₂_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X])
ih₂ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂)) ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (eval₂ C q (p₁ + p₂)) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw : (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁ + eval₂ C q p₂) =
  HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
    ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [eval₂_add, derivative_add, ih₁, ih₂, derivative_add, eval₂_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X])
ih₂ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂)) ((derivative : (a : R[X]) → R[X]) q : R[X])
rw :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁ + eval₂ C q p₂) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (eval₂ C q (p₁ + p₂)) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw₁ : HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₁) : R[X])
    ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) : R[X]) =
  HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
    ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [eval₂_add, derivative_add, ih₁, ih₂, derivative_add, eval₂_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X])
ih₂ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂)) ((derivative : (a : R[X]) → R[X]) q : R[X])
rw :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁ + eval₂ C q p₂) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₁ :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₁) : R[X])
      ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) : R[X]) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (eval₂ C q (p₁ + p₂)) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw₂ : HAdd.hAdd (β := R[X])
    (HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁))
      ((derivative : (a : R[X]) → R[X]) q : R[X]))
    ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) : R[X]) =
  HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
    ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [eval₂_add, derivative_add, ih₁, ih₂, derivative_add, eval₂_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X])
ih₂ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂)) ((derivative : (a : R[X]) → R[X]) q : R[X])
rw :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁ + eval₂ C q p₂) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₁ :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₁) : R[X])
      ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) : R[X]) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₂ :
  HAdd.hAdd (β := R[X])
      (HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁))
        ((derivative : (a : R[X]) → R[X]) q : R[X]))
      ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) : R[X]) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (eval₂ C q (p₁ + p₂)) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw₃ : HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X]) +
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂))
      ((derivative : (a : R[X]) → R[X]) q : R[X]) =
  HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
    ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [eval₂_add, derivative_add, ih₁, ih₂, derivative_add, eval₂_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X])
ih₂ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂)) ((derivative : (a : R[X]) → R[X]) q : R[X])
rw :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁ + eval₂ C q p₂) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₁ :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₁) : R[X])
      ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) : R[X]) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₂ :
  HAdd.hAdd (β := R[X])
      (HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁))
        ((derivative : (a : R[X]) → R[X]) q : R[X]))
      ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) : R[X]) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₃ :
  HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X]) +
      HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂))
        ((derivative : (a : R[X]) → R[X]) q : R[X]) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (eval₂ C q (p₁ + p₂)) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw₄ : HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X]) +
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂))
      ((derivative : (a : R[X]) → R[X]) q : R[X]) =
  HMul.hMul (β := R[X])
    (eval₂ C q
      (HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) p₁ : R[X])
        ((derivative : (a : R[X]) → R[X]) p₂ : R[X])))
    ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [eval₂_add, derivative_add, ih₁, ih₂, derivative_add, eval₂_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X])
ih₂ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂)) ((derivative : (a : R[X]) → R[X]) q : R[X])
rw :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁ + eval₂ C q p₂) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₁ :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₁) : R[X])
      ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) : R[X]) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₂ :
  HAdd.hAdd (β := R[X])
      (HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁))
        ((derivative : (a : R[X]) → R[X]) q : R[X]))
      ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) : R[X]) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₃ :
  HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X]) +
      HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂))
        ((derivative : (a : R[X]) → R[X]) q : R[X]) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₄ :
  HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X]) +
      HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂))
        ((derivative : (a : R[X]) → R[X]) q : R[X]) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        (HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) p₁ : R[X])
          ((derivative : (a : R[X]) → R[X]) p₂ : R[X])))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (eval₂ C q (p₁ + p₂)) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw₅ : HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X]) +
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂))
      ((derivative : (a : R[X]) → R[X]) q : R[X]) =
  HMul.hMul (β := R[X])
    (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁) + eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂))
    ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [eval₂_add, derivative_add, ih₁, ih₂, derivative_add, eval₂_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw : (derivative : (a : R[X]) → R[X])
    (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * X))) =
  HMul.hMul (β := R[X])
    (eval₂ C q
      ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * X))))
    ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [pow_succ, ← mul_assoc, eval₂_mul, eval₂_X, derivative_mul, ih, @derivative_mul _ _ _ X,
      derivative_X, mul_one, eval₂_add, @eval₂_mul _ _ _ _ X, eval₂_X, add_mul, mul_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * X))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * X))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw₁ : (derivative : (a : R[X]) → R[X])
    (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)) =
  HMul.hMul (β := R[X])
    (eval₂ C q
      ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)))
    ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [pow_succ, ← mul_assoc, eval₂_mul, eval₂_X, derivative_mul, ih, @derivative_mul _ _ _ X,
      derivative_X, mul_one, eval₂_add, @eval₂_mul _ _ _ _ X, eval₂_X, add_mul, mul_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * X))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * X))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₁ :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw₂ : (derivative : (a : R[X]) → R[X])
    (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) * eval₂ C q X) =
  HMul.hMul (β := R[X])
    (eval₂ C q
      ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)))
    ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [pow_succ, ← mul_assoc, eval₂_mul, eval₂_X, derivative_mul, ih, @derivative_mul _ _ _ X,
      derivative_X, mul_one, eval₂_add, @eval₂_mul _ _ _ _ X, eval₂_X, add_mul, mul_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * X))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * X))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₁ :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₂ :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) * eval₂ C q X) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw₃ : (derivative : (a : R[X]) → R[X])
    (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) * q) =
  HMul.hMul (β := R[X])
    (eval₂ C q
      ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)))
    ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [pow_succ, ← mul_assoc, eval₂_mul, eval₂_X, derivative_mul, ih, @derivative_mul _ _ _ X,
      derivative_X, mul_one, eval₂_add, @eval₂_mul _ _ _ _ X, eval₂_X, add_mul, mul_right_comm]