awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p_1 : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
inst_4 : NatPowAssoc S
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:
simp_all only [smeval_add, coeff_add, add_smul]

Premises used: Polynomial.coeff_add, add_smul, Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
⊢ 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:
simp only [monomial_zero_left, smeval_C, npow_zero, coeff_C_zero]

Premises used: Polynomial.smeval_C, npow_zero, Polynomial.monomial_zero_left, Polynomial.coeff_C_zero
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
monomial₆ monomial₇ : Eq.{u_2 + 1} (α := S) 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

Tactic:
rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]

Premises used: smul_zero, npow_one, MulZeroClass.mul_zero, zero_smul, Polynomial.smeval_monomial, npow_add, Polynomial.coeff_monomial_succ
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
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
⊢ 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

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]

Premises used: smul_zero, npow_one, Polynomial.smeval_C, npow_zero, MulZeroClass.mul_zero, zero_smul, Polynomial.smeval_monomial, npow_add, Polynomial.monomial_zero_left, Polynomial.coeff_C_zero, Polynomial.coeff_monomial_succ
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
monomial :
  ∀ (n : ℕ) (a : R),
    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
⊢ p.smeval 0 = HSMul.hSMul (β := S) (p.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]

Premises used: smul_zero, npow_one, Polynomial.monomial, Polynomial.smeval_C, npow_zero, Polynomial.coeff_add, MulZeroClass.mul_zero, zero_smul, add_smul, Polynomial.smeval_monomial, npow_add, Polynomial.monomial_zero_left, Polynomial.smeval_add, Polynomial.coeff_C_zero, Polynomial.coeff_monomial_succ
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p_1 : 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
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:
simp only [smeval_add, ph, qh, mul_add]

Premises used: mul_add, Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
monomial₇ monomial₈ : x * a • x ^ n = x * a • x ^ n
⊢ (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

Tactic:
rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
      npow_one, ← mul_smul_comm, smeval_monomial]

Premises used: Polynomial.monomial_one_one_eq_X, npow_one, Polynomial.smeval_monomial, npow_add, mul_smul_comm, one_mul, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
monomial :
  ∀ (n : ℕ) (a : R),
    (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
⊢ (X * p).smeval x = x * p.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]

Premises used: Polynomial.monomial_one_one_eq_X, npow_one, Polynomial.monomial, Polynomial.smeval_monomial, npow_add, mul_smul_comm, mul_add, Polynomial.smeval_add, one_mul, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p_1 : 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 : ℕ
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:
simp only [smeval_add, ph, qh, mul_add]

Premises used: mul_add, Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
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_1 n : ℕ
a : R
⊢ x ^ m * x ^ n_1 * smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x =
    x ^ m * (x ^ n_1 * smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x)

Tactic:
simp only [smeval_monomial, mul_smul_comm, npow_mul_assoc]

Premises used: Polynomial.smeval_monomial, npow_mul_assoc, mul_smul_comm
-- Module: Mathlib.Algebra.Polynomial.Smeval
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 : ℕ
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)
monomial :
  ∀ (n_1 : ℕ) (a : R),
    x ^ m * x ^ n * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n_1 : (a : R) → R[X]) a) x =
      x ^ m * (x ^ n * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n_1 : (a : R) → R[X]) a) x)
⊢ x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.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]

Premises used: Polynomial.monomial, Polynomial.smeval_monomial, npow_mul_assoc, mul_smul_comm, mul_add, Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
⊢ (HPow.hPow (α := R[X]) (β := ℕ) X 0 * p).smeval x = HPow.hPow (β := ℕ) x 0 * p.smeval x

Tactic:
simp [npow_zero, one_mul]

Premises used: npow_zero, one_mul
-- Module: Mathlib.Algebra.Polynomial.Smeval
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 : ℕ
rw : (HPow.hPow (α := R[X]) X (1 + n) * p).smeval x = x ^ (1 + n) * p.smeval x
rw₁ : (HPow.hPow (α := R[X]) (β := ℕ) X 1 * HPow.hPow (α := R[X]) X n * p).smeval x = x ^ (1 + n) * p.smeval x
rw₂ : (HPow.hPow (α := R[X]) (β := ℕ) X 1 * (HPow.hPow (α := R[X]) X n * p)).smeval x = x ^ (1 + n) * p.smeval x
rw₃ : (X * (HPow.hPow (α := R[X]) X n * p)).smeval x = x ^ (1 + n) * p.smeval x
rw₄ : x * (HPow.hPow (α := R[X]) X n * p).smeval x = x ^ (1 + n) * p.smeval x
rw₅ : x * (x ^ n * p.smeval x) = x ^ (1 + n) * p.smeval x
rw₆ : x * (x ^ n * p.smeval x) = HPow.hPow (β := ℕ) x 1 * x ^ n * p.smeval x
rw₇ : x * (x ^ n * p.smeval x) = HPow.hPow (β := ℕ) x 1 * (x ^ n * p.smeval x)
rw₈ rw₉ : x * (x ^ n * p.smeval x) = x * (x ^ n * p.smeval x)
⊢ (HPow.hPow (α := R[X]) X (n + 1) * p).smeval x = x ^ (n + 1) * p.smeval x

Tactic:
rw [add_comm, npow_add, mul_assoc, npow_one, smeval_X_mul, smeval_X_pow_mul n, npow_add,
      smeval_X_pow_assoc, npow_one]

Premises used: mul_assoc, npow_one, add_comm, Polynomial.smeval_X_mul, npow_add, Polynomial.smeval_X_pow_assoc
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
r_1 : 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 : ℕ
r s : R[X]
hr : (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r_1 : R[X]) r).smeval x = r_1 • (x ^ n * r.smeval x)
hs : (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r_1 : R[X]) s).smeval x = r_1 • (x ^ n * s.smeval x)
add :
  (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r_1 : R[X]) (r + s)).smeval x =
    r_1 • (x ^ n * (r.smeval x + s.smeval x))
⊢ (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r_1 : R[X]) (r + s)).smeval x = r_1 • (x ^ n * (r + s).smeval x)

Tactic:
simp only [smeval_add]

Premises used: Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
r_1 : 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 : ℕ
r s : R[X]
hr : (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r_1 : R[X]) r).smeval x = r_1 • (x ^ n * r.smeval x)
hs : (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r_1 : R[X]) s).smeval x = r_1 • (x ^ n * s.smeval x)
add :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r_1 : R[X]) (HPow.hPow (α := R[X]) X n) * (r + s)).smeval x =
    r_1 • (x ^ n * (r.smeval x + s.smeval x))
add₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r_1 : R[X]) (HPow.hPow (α := R[X]) X n * (r + s))).smeval x =
    r_1 • (x ^ n * (r.smeval x + s.smeval x))
add₂ : r_1 • (HPow.hPow (α := R[X]) X n * (r + s)).smeval x = r_1 • (x ^ n * (r.smeval x + s.smeval x))
add₃ : r_1 • (x ^ n * (r + s).smeval x) = r_1 • (x ^ n * (r.smeval x + s.smeval x))
add₄ add₅ : r_1 • (x ^ n * (r.smeval x + s.smeval x)) = r_1 • (x ^ n * (r.smeval x + s.smeval x))
⊢ (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r_1 : R[X]) (r + s)).smeval x =
    r_1 • (x ^ n * (r.smeval x + s.smeval x))

Tactic:
rw [← C_mul_X_pow_eq_monomial, mul_assoc, smeval_C_mul, smeval_X_pow_mul, smeval_add]

Premises used: mul_assoc, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.smeval_X_pow_mul, Polynomial.smeval_C_mul, Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
r : 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_1 n : ℕ
a : R
monomial :
  (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial n_1 : (a : R) → R[X]) r : R[X])
          ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval
      x =
    r • (x ^ n_1 * a • x ^ n)
monomial₁ :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial (n_1 + n) : (a : R) → R[X]) (r * a)) x = r • (x ^ n_1 * a • x ^ n)
monomial₂ : (r * a) • x ^ (n_1 + n) = r • (x ^ n_1 * a • x ^ n)
monomial₃ : (r * a) • (x ^ n_1 * x ^ n) = r • (x ^ n_1 * a • x ^ n)
monomial₄ : r • a • (x ^ n_1 * x ^ n) = r • (x ^ n_1 * a • x ^ n)
monomial₅ monomial₆ : r • a • (x ^ n_1 * x ^ n) = r • a • (x ^ n_1 * x ^ n)
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial n_1 : (a : R) → R[X]) r : R[X])
          ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval
      x =
    r • (x ^ n_1 * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x)

Tactic:
rw [smeval_monomial, monomial_mul_monomial, smeval_monomial, npow_add, mul_smul, mul_smul_comm]

Premises used: Polynomial.smeval_monomial, npow_add, mul_smul_comm, SemigroupAction.mul_smul, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
r : 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 : ℕ
add :
  ∀ (r_1 s : R[X])
    (hr :
      (HMul.hMul (α := R[X]) ((Polynomial.monomial n : (a : R) → R[X]) r : R[X]) r_1).smeval x =
        r • (x ^ n * r_1.smeval x))
    (hs :
      (HMul.hMul (α := R[X]) ((Polynomial.monomial n : (a : R) → R[X]) r : R[X]) s).smeval x =
        r • (x ^ n * s.smeval x)),
    (HMul.hMul (α := R[X]) ((Polynomial.monomial n : (a : R) → R[X]) r : R[X]) (r_1 + s)).smeval x =
      r • (x ^ n * (r_1 + s).smeval x)
monomial :
  ∀ (n_1 : ℕ) (a : R),
    (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial n : (a : R) → R[X]) r : R[X])
            ((Polynomial.monomial n_1 : (a : R) → R[X]) a : R[X])).smeval
        x =
      r • (x ^ n * smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n_1 : (a : R) → R[X]) a) x)
⊢ (HMul.hMul (α := R[X]) ((Polynomial.monomial n : (a : R) → R[X]) r : R[X]) p).smeval x = r • (x ^ n * p.smeval x)

Tactic:
induction p using Polynomial.induction_on' with
  | add r s hr hs =>
    simp only [smeval_add]
    rw [← C_mul_X_pow_eq_monomial, mul_assoc, smeval_C_mul, smeval_X_pow_mul, smeval_add]
  | monomial n a =>
    rw [smeval_monomial, monomial_mul_monomial, smeval_monomial, npow_add, mul_smul, mul_smul_comm]

Premises used: mul_assoc, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.monomial, Polynomial.smeval_X_pow_mul, Polynomial.smeval_C_mul, Polynomial.smeval_monomial, npow_add, mul_smul_comm, Polynomial.smeval_add, SemigroupAction.mul_smul, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p_1 : 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 : IsScalarTower R S S
p q : R[X]
ph : (p * X).smeval x = p.smeval x * x
qh : (q * X).smeval x = q.smeval x * x
⊢ ((p + q) * X).smeval x = (p + q).smeval x * x

Tactic:
simp only [add_mul, smeval_add, ph, qh]

Premises used: add_mul, Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
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 : IsScalarTower R S S
n : ℕ
a : R
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) X).smeval x =
    smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x * x

Tactic:
simp only [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, mul_one,
      npow_add, smul_mul_assoc, npow_one]

Premises used: Polynomial.monomial_one_one_eq_X, npow_one, smul_mul_assoc, Polynomial.smeval_monomial, npow_add, mul_one, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Smeval
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 : IsScalarTower R S S
add :
  ∀ (p q : R[X]) (ph : (p * X).smeval x = p.smeval x * x) (qh : (q * X).smeval x = q.smeval x * x),
    ((p + q) * X).smeval x = (p + q).smeval x * x
monomial :
  ∀ (n : ℕ) (a : R),
    (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial n : (a : R) → R[X]) a : R[X]) X).smeval x =
      smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x * x
⊢ (p * X).smeval x = p.smeval x * x

Tactic:
induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [add_mul, smeval_add, ph, qh]
  | monomial n a =>
    simp only [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, mul_one,
      npow_add, smul_mul_assoc, npow_one]

Premises used: add_mul, Polynomial.monomial_one_one_eq_X, npow_one, Polynomial.monomial, smul_mul_assoc, Polynomial.smeval_monomial, npow_add, Polynomial.smeval_add, mul_one, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p_1 : 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 : IsScalarTower R S S
m n : ℕ
p q : R[X]
ph : p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)
qh : 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 * (x ^ m * x ^ n)

Tactic:
simp only [smeval_add, ph, qh, add_mul]

Premises used: add_mul, Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
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 : IsScalarTower R S S
m n_1 n : ℕ
a : R
monomial : a • x ^ n * x ^ m * x ^ n_1 = a • x ^ n * (x ^ m * x ^ n_1)
monomial₁ : a • (x ^ n * x ^ m) * x ^ n_1 = a • x ^ n * (x ^ m * x ^ n_1)
monomial₂ : a • (x ^ n * x ^ m * x ^ n_1) = a • x ^ n * (x ^ m * x ^ n_1)
monomial₃ : a • (x ^ n * (x ^ m * x ^ n_1)) = a • x ^ n * (x ^ m * x ^ n_1)
monomial₄ monomial₅ : a • x ^ n * (x ^ m * x ^ n_1) = a • x ^ n * (x ^ m * x ^ n_1)
⊢ smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x * x ^ m * x ^ n_1 =
    smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x * (x ^ m * x ^ n_1)

Tactic:
rw [smeval_monomial, smul_mul_assoc, smul_mul_assoc, npow_mul_assoc, ← smul_mul_assoc]

Premises used: smul_mul_assoc, Polynomial.smeval_monomial, npow_mul_assoc
-- Module: Mathlib.Algebra.Polynomial.Smeval
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 : IsScalarTower R S S
m n : ℕ
add :
  ∀ (p q : R[X]) (ph : p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n))
    (qh : 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 * (x ^ m * x ^ n)
monomial :
  ∀ (n_1 : ℕ) (a : R),
    smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n_1 : (a : R) → R[X]) a) x * x ^ m * x ^ n =
      smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n_1 : (a : R) → R[X]) a) x * (x ^ m * x ^ n)
⊢ p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)

Tactic:
induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [smeval_add, ph, qh, add_mul]
  | monomial n a =>
    rw [smeval_monomial, smul_mul_assoc, smul_mul_assoc, npow_mul_assoc, ← smul_mul_assoc]

Premises used: add_mul, Polynomial.monomial, smul_mul_assoc, Polynomial.smeval_monomial, npow_mul_assoc, Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
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 : IsScalarTower R S S
⊢ (p * HPow.hPow (α := R[X]) (β := ℕ) X 0).smeval x = p.smeval x * HPow.hPow (β := ℕ) x 0

Tactic:
simp only [npow_zero, mul_one]

Premises used: npow_zero, mul_one
-- Module: Mathlib.Algebra.Polynomial.Smeval
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 : IsScalarTower R S S
n : ℕ
rw : (p * (HPow.hPow (α := R[X]) X n * HPow.hPow (α := R[X]) (β := ℕ) X 1)).smeval x = p.smeval x * x ^ (n + 1)
rw₁ : (p * HPow.hPow (α := R[X]) X n * HPow.hPow (α := R[X]) (β := ℕ) X 1).smeval x = p.smeval x * x ^ (n + 1)
rw₂ : (p * HPow.hPow (α := R[X]) X n * X).smeval x = p.smeval x * x ^ (n + 1)
rw₃ : (p * HPow.hPow (α := R[X]) X n).smeval x * x = p.smeval x * x ^ (n + 1)
rw₄ : p.smeval x * x ^ n * x = p.smeval x * x ^ (n + 1)
rw₅ : p.smeval x * x ^ n * x = p.smeval x * (x ^ n * HPow.hPow (β := ℕ) x 1)
rw₆ : p.smeval x * x ^ n * x = p.smeval x * x ^ n * HPow.hPow (β := ℕ) x 1
rw₇ rw₈ : p.smeval x * x ^ n * x = p.smeval x * x ^ n * x
⊢ (p * HPow.hPow (α := R[X]) X (n + 1)).smeval x = p.smeval x * x ^ (n + 1)

Tactic:
rw [npow_add, ← mul_assoc, npow_one, smeval_mul_X, smeval_mul_X_pow n, npow_add,
      ← smeval_assoc_X_pow, npow_one]

Premises used: Polynomial.smeval_mul_X, Polynomial.smeval_assoc_X_pow, mul_assoc, npow_one, npow_add