awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
S : Type u_2
inst : NonAssocSemiring S
inst_1 : Pow S ℕ
inst_2 : NatPowAssoc S
q : ℕ[X]
add :
  ∀ (p q : ℕ[X]) (ph : ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) (p.smeval (↑n : S)) (↑(p.smeval n) : S))
    (qh : ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) (q.smeval (↑n : S)) (↑(q.smeval n) : S)) (n : ℕ),
    Eq.{u_2 + 1} (α := S) ((p + q).smeval (↑n : S)) (↑((p + q).smeval n) : S)
⊢ ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) (q.smeval (↑n : S)) (↑(q.smeval n) : S)
have monomial : ∀ (n a n_1 : ℕ),
  Eq.{u_2 + 1} (α := S) (smeval (R := ℕ) ((monomial n : (a : ℕ) → ℕ[X]) a) (↑n_1 : S))
    (↑(smeval (R := ℕ) ((monomial n : (a : ℕ) → ℕ[X]) a) n_1) : S)
Tactic: induction q using Polynomial.induction_on' with
  | add p q ph qh =>
    intro n
    simp only [smeval_add, ph, qh, Nat.cast_add]
  | monomial n a =>
    intro n
    rw [smeval_monomial, smeval_monomial, nsmul_eq_mul, smul_eq_mul, Nat.cast_mul, Nat.cast_npow]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
inst_4 : NatPowAssoc S
a : R
n : ℕ
⊢ smeval.{u_1, u_2} (R := R) ((monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) (coeff ((monomial (n + 1) : (a : R) → R[X]) a) 0) 1
have monomial : smeval.{u_1, u_2} (R := R) ((monomial (n + 1) : (a : R) → R[X]) a) 0 = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
Tactic: rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
inst_4 : NatPowAssoc S
a : R
n : ℕ
monomial :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
⊢ smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) (coeff ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0) 1
have monomial₁ : a • HPow.hPow (α := S) 0 (n + 1) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
Tactic: rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
inst_4 : NatPowAssoc S
a : R
n : ℕ
monomial :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₁ : a • HPow.hPow (α := S) 0 (n + 1) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
⊢ smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) (coeff ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0) 1
have monomial₂ : a • (HPow.hPow (α := S) 0 n * HPow.hPow (α := S) (β := ℕ) 0 1) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
Tactic: rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
inst_4 : NatPowAssoc S
a : R
n : ℕ
monomial :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₁ : a • HPow.hPow (α := S) 0 (n + 1) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₂ :
  a • (HPow.hPow (α := S) 0 n * HPow.hPow (α := S) (β := ℕ) 0 1) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
⊢ smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) (coeff ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0) 1
have monomial₃ : a • (HPow.hPow (α := S) 0 n * 0) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
Tactic: rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
inst_4 : NatPowAssoc S
a : R
n : ℕ
monomial :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₁ : a • HPow.hPow (α := S) 0 (n + 1) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₂ :
  a • (HPow.hPow (α := S) 0 n * HPow.hPow (α := S) (β := ℕ) 0 1) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₃ : a • (HPow.hPow (α := S) 0 n * 0) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
⊢ smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) (coeff ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0) 1
have monomial₄ : HSMul.hSMul (β := S) a 0 = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
Tactic: rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
inst_4 : NatPowAssoc S
a : R
n : ℕ
monomial :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₁ : a • HPow.hPow (α := S) 0 (n + 1) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₂ :
  a • (HPow.hPow (α := S) 0 n * HPow.hPow (α := S) (β := ℕ) 0 1) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₃ : a • (HPow.hPow (α := S) 0 n * 0) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₄ : HSMul.hSMul (β := S) a 0 = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
⊢ smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) (coeff ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0) 1
have monomial₅ : HSMul.hSMul (β := S) a 0 = 0
Tactic: rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
inst_4 : NatPowAssoc S
a : R
n : ℕ
monomial :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₁ : a • HPow.hPow (α := S) 0 (n + 1) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₂ :
  a • (HPow.hPow (α := S) 0 n * HPow.hPow (α := S) (β := ℕ) 0 1) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₃ : a • (HPow.hPow (α := S) 0 n * 0) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₄ : HSMul.hSMul (β := S) a 0 = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 1
monomial₅ : HSMul.hSMul (β := S) a 0 = 0
⊢ smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) (coeff ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0) 1
have monomial₆ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
inst_4 : NatPowAssoc S
n : ℕ
a : R
⊢ smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) (coeff ((monomial n : (a : R) → R[X]) a) 0) 1
have monomial : smeval.{u_1, u_2} (R := R) ((monomial 0 : (a : R) → R[X]) a) 0 =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) (coeff ((monomial 0 : (a : R) → R[X]) a) 0) 1
Tactic: cases n with
    | zero => simp only [monomial_zero_left, smeval_C, npow_zero, coeff_C_zero]
    | succ n => rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
inst_4 : NatPowAssoc S
n : ℕ
a : R
monomial :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial 0 : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) (coeff ((Polynomial.monomial 0 : (a : R) → R[X]) a) 0) 1
⊢ smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) (coeff ((Polynomial.monomial n : (a : R) → R[X]) a) 0) 1
have monomial₁ : ∀ (n : ℕ),
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) (coeff ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a) 0) 1
Tactic: cases n with
    | zero => simp only [monomial_zero_left, smeval_C, npow_zero, coeff_C_zero]
    | succ n => rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
inst_4 : NatPowAssoc S
⊢ p.smeval 0 = HSMul.hSMul (β := S) (p.coeff 0) 1
have add : ∀ (p q : R[X]) (ph : p.smeval 0 = HSMul.hSMul (β := S) (p.coeff 0) 1)
  (qh : q.smeval 0 = HSMul.hSMul (β := S) (q.coeff 0) 1), (p + q).smeval 0 = HSMul.hSMul (β := S) ((p + q).coeff 0) 1
Tactic: induction p using Polynomial.induction_on' with
  | add p q ph qh => simp_all only [smeval_add, coeff_add, add_smul]
  | monomial n a =>
    cases n with
    | zero => simp only [monomial_zero_left, smeval_C, npow_zero, coeff_C_zero]
    | succ n => rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
inst_4 : NatPowAssoc S
add :
  ∀ (p q : R[X]) (ph : p.smeval 0 = HSMul.hSMul (β := S) (p.coeff 0) 1)
    (qh : q.smeval 0 = HSMul.hSMul (β := S) (q.coeff 0) 1), (p + q).smeval 0 = HSMul.hSMul (β := S) ((p + q).coeff 0) 1
⊢ p.smeval 0 = HSMul.hSMul (β := S) (p.coeff 0) 1
have monomial : ∀ (n : ℕ) (a : R),
  smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) 0 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) (coeff ((monomial n : (a : R) → R[X]) a) 0) 1
Tactic: induction p using Polynomial.induction_on' with
  | add p q ph qh => simp_all only [smeval_add, coeff_add, add_smul]
  | monomial n a =>
    cases n with
    | zero => simp only [monomial_zero_left, smeval_C, npow_zero, coeff_C_zero]
    | succ n => rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : SMulCommClass R S S
n : ℕ
a : R
⊢ (HMul.hMul (α := R[X]) (β := R[X]) X ((monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    x * smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x
have monomial : (HMul.hMul (α := R[X]) (β := R[X]) ((monomial 1 : (a : R) → R[X]) 1 : R[X])
        ((monomial n : (a : R) → R[X]) a : R[X])).smeval
    x =
  x * smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x
Tactic: rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
      npow_one, ← mul_smul_comm, smeval_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : SMulCommClass R S S
n : ℕ
a : R
monomial :
  (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial 1 : (a : R) → R[X]) 1 : R[X])
          ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval
      x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
⊢ (HMul.hMul (α := R[X]) (β := R[X]) X ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
have monomial₁ : smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (1 + n) : (a : R) → R[X]) (1 * a)) x =
  x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
Tactic: rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
      npow_one, ← mul_smul_comm, smeval_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : SMulCommClass R S S
n : ℕ
a : R
monomial :
  (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial 1 : (a : R) → R[X]) 1 : R[X])
          ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval
      x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₁ :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (1 + n) : (a : R) → R[X]) (1 * a)) x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
⊢ (HMul.hMul (α := R[X]) (β := R[X]) X ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
have monomial₂ : (1 * a) • x ^ (1 + n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
Tactic: rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
      npow_one, ← mul_smul_comm, smeval_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : SMulCommClass R S S
n : ℕ
a : R
monomial :
  (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial 1 : (a : R) → R[X]) 1 : R[X])
          ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval
      x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₁ :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (1 + n) : (a : R) → R[X]) (1 * a)) x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₂ : (1 * a) • x ^ (1 + n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
⊢ (HMul.hMul (α := R[X]) (β := R[X]) X ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
have monomial₃ : a • x ^ (1 + n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
Tactic: rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
      npow_one, ← mul_smul_comm, smeval_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : SMulCommClass R S S
n : ℕ
a : R
monomial :
  (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial 1 : (a : R) → R[X]) 1 : R[X])
          ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval
      x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₁ :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (1 + n) : (a : R) → R[X]) (1 * a)) x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₂ : (1 * a) • x ^ (1 + n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₃ : a • x ^ (1 + n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
⊢ (HMul.hMul (α := R[X]) (β := R[X]) X ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
have monomial₄ : a • (HPow.hPow (β := ℕ) x 1 * x ^ n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
Tactic: rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
      npow_one, ← mul_smul_comm, smeval_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : SMulCommClass R S S
n : ℕ
a : R
monomial :
  (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial 1 : (a : R) → R[X]) 1 : R[X])
          ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval
      x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₁ :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (1 + n) : (a : R) → R[X]) (1 * a)) x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₂ : (1 * a) • x ^ (1 + n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₃ : a • x ^ (1 + n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₄ :
  a • (HPow.hPow (β := ℕ) x 1 * x ^ n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
⊢ (HMul.hMul (α := R[X]) (β := R[X]) X ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
have monomial₅ : a • (x * x ^ n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
Tactic: rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
      npow_one, ← mul_smul_comm, smeval_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : SMulCommClass R S S
n : ℕ
a : R
monomial :
  (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial 1 : (a : R) → R[X]) 1 : R[X])
          ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval
      x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₁ :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (1 + n) : (a : R) → R[X]) (1 * a)) x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₂ : (1 * a) • x ^ (1 + n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₃ : a • x ^ (1 + n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₄ :
  a • (HPow.hPow (β := ℕ) x 1 * x ^ n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₅ : a • (x * x ^ n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
⊢ (HMul.hMul (α := R[X]) (β := R[X]) X ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
have monomial₆ : x * a • x ^ n = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
Tactic: rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
      npow_one, ← mul_smul_comm, smeval_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : SMulCommClass R S S
n : ℕ
a : R
monomial :
  (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial 1 : (a : R) → R[X]) 1 : R[X])
          ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval
      x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₁ :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (1 + n) : (a : R) → R[X]) (1 * a)) x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₂ : (1 * a) • x ^ (1 + n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₃ : a • x ^ (1 + n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₄ :
  a • (HPow.hPow (β := ℕ) x 1 * x ^ n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₅ : a • (x * x ^ n) = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₆ : x * a • x ^ n = x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
⊢ (HMul.hMul (α := R[X]) (β := R[X]) X ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    x * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
have monomial₇ : x * a • x ^ n = x * a • x ^ n
Tactic: rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
      npow_one, ← mul_smul_comm, smeval_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : SMulCommClass R S S
⊢ (X * p).smeval x = x * p.smeval x
have add : ∀ (p q : R[X]) (ph : (X * p).smeval x = x * p.smeval x) (qh : (X * q).smeval x = x * q.smeval x),
  (X * (p + q)).smeval x = x * (p + q).smeval x
Tactic: induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [smeval_add, ph, qh, mul_add]
  | monomial n a =>
    rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
      npow_one, ← mul_smul_comm, smeval_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : SMulCommClass R S S
add :
  ∀ (p q : R[X]) (ph : (X * p).smeval x = x * p.smeval x) (qh : (X * q).smeval x = x * q.smeval x),
    (X * (p + q)).smeval x = x * (p + q).smeval x
⊢ (X * p).smeval x = x * p.smeval x
have monomial : ∀ (n : ℕ) (a : R),
  (HMul.hMul (α := R[X]) (β := R[X]) X ((monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    x * smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x
Tactic: induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [smeval_add, ph, qh, mul_add]
  | monomial n a =>
    rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
      npow_one, ← mul_smul_comm, smeval_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : SMulCommClass R S S
m n : ℕ
⊢ x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x)
have add : ∀ (p q : R[X]) (ph : x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x))
  (qh : x ^ m * x ^ n * q.smeval x = x ^ m * (x ^ n * q.smeval x)),
  x ^ m * x ^ n * (p + q).smeval x = x ^ m * (x ^ n * (p + q).smeval x)
Tactic: induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [smeval_add, ph, qh, mul_add]
  | monomial n a => simp only [smeval_monomial, mul_smul_comm, npow_mul_assoc]