awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
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)
⊢ x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x)
have monomial : ∀ (n_1 : ℕ) (a : R),
  x ^ m * x ^ n * smeval.{u_1, u_2} (R := R) ((monomial n_1 : (a : R) → R[X]) a) x =
    x ^ m * (x ^ n * smeval.{u_1, u_2} (R := R) ((monomial n_1 : (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 => simp only [smeval_monomial, mul_smul_comm, npow_mul_assoc]
-- 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 : ℕ
⊢ (HPow.hPow (α := R[X]) X (n + 1) * p).smeval x = x ^ (n + 1) * p.smeval x
have rw : (HPow.hPow (α := R[X]) X (1 + n) * p).smeval x = x ^ (1 + n) * 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]
-- 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 : ℕ
rw : (HPow.hPow (α := R[X]) X (1 + n) * p).smeval x = x ^ (1 + n) * p.smeval x
⊢ (HPow.hPow (α := R[X]) X (n + 1) * p).smeval x = x ^ (n + 1) * p.smeval x
have rw₁ : (HPow.hPow (α := R[X]) (β := ℕ) X 1 * HPow.hPow (α := R[X]) X n * p).smeval x = x ^ (1 + n) * 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]
-- 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 : ℕ
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
⊢ (HPow.hPow (α := R[X]) X (n + 1) * p).smeval x = x ^ (n + 1) * p.smeval x
have rw₂ : (HPow.hPow (α := R[X]) (β := ℕ) X 1 * (HPow.hPow (α := R[X]) X n * p)).smeval x = x ^ (1 + n) * 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]
-- 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 : ℕ
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
⊢ (HPow.hPow (α := R[X]) X (n + 1) * p).smeval x = x ^ (n + 1) * p.smeval x
have rw₃ : (X * (HPow.hPow (α := R[X]) X n * p)).smeval x = x ^ (1 + n) * 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]
-- 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 : ℕ
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
⊢ (HPow.hPow (α := R[X]) X (n + 1) * p).smeval x = x ^ (n + 1) * p.smeval x
have rw₄ : x * (HPow.hPow (α := R[X]) X n * p).smeval x = x ^ (1 + n) * 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]
-- 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 : ℕ
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
⊢ (HPow.hPow (α := R[X]) X (n + 1) * p).smeval x = x ^ (n + 1) * p.smeval x
have rw₅ : x * (x ^ n * p.smeval x) = x ^ (1 + n) * 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]
-- 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 : ℕ
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
⊢ (HPow.hPow (α := R[X]) X (n + 1) * p).smeval x = x ^ (n + 1) * p.smeval x
have rw₆ : x * (x ^ n * p.smeval x) = HPow.hPow (β := ℕ) x 1 * x ^ n * 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]
-- 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 : ℕ
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
⊢ (HPow.hPow (α := R[X]) X (n + 1) * p).smeval x = x ^ (n + 1) * p.smeval x
have rw₇ : x * (x ^ n * p.smeval x) = HPow.hPow (β := ℕ) x 1 * (x ^ n * 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]
-- 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 : ℕ
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)
⊢ (HPow.hPow (α := R[X]) X (n + 1) * p).smeval x = x ^ (n + 1) * p.smeval x
have rw₈ : x * (x ^ n * p.smeval x) = x * (x ^ n * 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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)
⊢ (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)
have 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))
Tactic: simp only [smeval_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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)
⊢ (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))
have 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))
Tactic: rw [← C_mul_X_pow_eq_monomial, mul_assoc, smeval_C_mul, smeval_X_pow_mul, smeval_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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))
⊢ (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))
have 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))
Tactic: rw [← C_mul_X_pow_eq_monomial, mul_assoc, smeval_C_mul, smeval_X_pow_mul, smeval_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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))
⊢ (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))
have add₂ : r_1 • (HPow.hPow (α := R[X]) X n * (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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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))
⊢ (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))
have add₃ : r_1 • (x ^ n * (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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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))
⊢ (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))
have add₄ : r_1 • (x ^ n * (r.smeval x + 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((monomial n_1 : (a : R) → R[X]) r : R[X])
          ((monomial n : (a : R) → R[X]) a : R[X])).smeval
      x =
    r • (x ^ n_1 * smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x)
have monomial : (HMul.hMul (α := R[X]) (β := R[X]) ((monomial n_1 : (a : R) → R[X]) r : R[X])
        ((monomial n : (a : R) → R[X]) a : R[X])).smeval
    x =
  r • (x ^ n_1 * a • x ^ n)
Tactic: rw [smeval_monomial, monomial_mul_monomial, smeval_monomial, npow_add, mul_smul, mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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)
⊢ (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)
have 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)
Tactic: rw [smeval_monomial, monomial_mul_monomial, smeval_monomial, npow_add, mul_smul, mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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)
⊢ (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)
have monomial₂ : (r * a) • x ^ (n_1 + n) = r • (x ^ n_1 * a • x ^ n)
Tactic: rw [smeval_monomial, monomial_mul_monomial, smeval_monomial, npow_add, mul_smul, mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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)
⊢ (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)
have monomial₃ : (r * a) • (x ^ n_1 * x ^ n) = r • (x ^ n_1 * a • x ^ n)
Tactic: rw [smeval_monomial, monomial_mul_monomial, smeval_monomial, npow_add, mul_smul, mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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)
⊢ (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)
have monomial₄ : r • a • (x ^ n_1 * x ^ n) = r • (x ^ n_1 * a • x ^ n)
Tactic: rw [smeval_monomial, monomial_mul_monomial, smeval_monomial, npow_add, mul_smul, mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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)
⊢ (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)
have monomial₅ : r • a • (x ^ n_1 * x ^ n) = r • a • (x ^ n_1 * x ^ n)
Tactic: rw [smeval_monomial, monomial_mul_monomial, smeval_monomial, npow_add, mul_smul, mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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 : ℕ
⊢ (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) p).smeval x = r • (x ^ n * p.smeval x)
have add : ∀ (r_1 s : R[X])
  (hr : (HMul.hMul (α := R[X]) ((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]) ((monomial n : (a : R) → R[X]) r : R[X]) s).smeval x = r • (x ^ n * s.smeval x)),
  (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (r_1 + s)).smeval x = r • (x ^ n * (r_1 + s).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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
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]) ((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]) ((monomial n : (a : R) → R[X]) r : R[X]) s).smeval x = r • (x ^ n * s.smeval x)),
    (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (r_1 + s)).smeval x =
      r • (x ^ n * (r_1 + s).smeval x)
⊢ (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) p).smeval x = r • (x ^ n * p.smeval x)
have monomial : ∀ (n_1 : ℕ) (a : R),
  (HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) r : R[X])
          ((monomial n_1 : (a : R) → R[X]) a : R[X])).smeval
      x =
    r • (x ^ n * smeval.{u_1, u_2} (R := R) ((monomial n_1 : (a : R) → R[X]) a) 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]