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 : IsScalarTower R S S
⊢ (p * X).smeval x = p.smeval x * x
have 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
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]
-- 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 : 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
⊢ (p * X).smeval x = p.smeval x * x
have monomial : ∀ (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: 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]
-- 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 : IsScalarTower R S S
m n_1 n : ℕ
a : R
⊢ 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 * (x ^ m * x ^ n_1)
have monomial : a • x ^ n * x ^ m * x ^ n_1 = a • x ^ n * (x ^ m * x ^ n_1)
Tactic: rw [smeval_monomial, smul_mul_assoc, smul_mul_assoc, npow_mul_assoc, ← smul_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 : 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)
⊢ 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)
have monomial₁ : a • (x ^ n * x ^ m) * x ^ n_1 = a • x ^ n * (x ^ m * x ^ n_1)
Tactic: rw [smeval_monomial, smul_mul_assoc, smul_mul_assoc, npow_mul_assoc, ← smul_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 : 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)
⊢ 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)
have monomial₂ : a • (x ^ n * x ^ m * x ^ n_1) = a • x ^ n * (x ^ m * x ^ n_1)
Tactic: rw [smeval_monomial, smul_mul_assoc, smul_mul_assoc, npow_mul_assoc, ← smul_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 : 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)
⊢ 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)
have monomial₃ : a • (x ^ n * (x ^ m * x ^ n_1)) = a • x ^ n * (x ^ m * x ^ n_1)
Tactic: rw [smeval_monomial, smul_mul_assoc, smul_mul_assoc, npow_mul_assoc, ← smul_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 : 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)
⊢ 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)
have monomial₄ : a • x ^ n * (x ^ m * x ^ n_1) = a • x ^ n * (x ^ m * x ^ n_1)
Tactic: rw [smeval_monomial, smul_mul_assoc, smul_mul_assoc, npow_mul_assoc, ← smul_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 : IsScalarTower R S S
m n : ℕ
⊢ p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)
have 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)
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]
-- 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 : 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)
⊢ p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)
have monomial : ∀ (n_1 : ℕ) (a : R),
  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 * (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]
-- 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 : IsScalarTower R S S
n : ℕ
⊢ (p * HPow.hPow (α := R[X]) X (n + 1)).smeval x = p.smeval x * x ^ (n + 1)
have rw : (p * (HPow.hPow (α := R[X]) X n * HPow.hPow (α := R[X]) (β := ℕ) X 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]
-- 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 : 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)
⊢ (p * HPow.hPow (α := R[X]) X (n + 1)).smeval x = p.smeval x * x ^ (n + 1)
have rw₁ : (p * HPow.hPow (α := R[X]) X n * HPow.hPow (α := R[X]) (β := ℕ) X 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]
-- 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 : 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)
⊢ (p * HPow.hPow (α := R[X]) X (n + 1)).smeval x = p.smeval x * x ^ (n + 1)
have rw₂ : (p * HPow.hPow (α := R[X]) X n * X).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]
-- 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 : 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)
⊢ (p * HPow.hPow (α := R[X]) X (n + 1)).smeval x = p.smeval x * x ^ (n + 1)
have rw₃ : (p * HPow.hPow (α := R[X]) X n).smeval x * 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]
-- 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 : 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)
⊢ (p * HPow.hPow (α := R[X]) X (n + 1)).smeval x = p.smeval x * x ^ (n + 1)
have rw₄ : p.smeval x * x ^ n * 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]
-- 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 : 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)
⊢ (p * HPow.hPow (α := R[X]) X (n + 1)).smeval x = p.smeval x * x ^ (n + 1)
have rw₅ : p.smeval x * x ^ n * x = p.smeval x * (x ^ n * HPow.hPow (β := ℕ) x 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]
-- 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 : 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)
⊢ (p * HPow.hPow (α := R[X]) X (n + 1)).smeval x = p.smeval x * x ^ (n + 1)
have rw₆ : p.smeval x * x ^ n * x = p.smeval x * x ^ n * HPow.hPow (β := ℕ) x 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]
-- 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 : 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
⊢ (p * HPow.hPow (α := R[X]) X (n + 1)).smeval x = p.smeval x * x ^ (n + 1)
have rw₇ : p.smeval x * x ^ n * x = p.smeval x * x ^ n * x
Tactic: rw [npow_add, ← mul_assoc, npow_one, smeval_mul_X, smeval_mul_X_pow n, npow_add,
      ← smeval_assoc_X_pow, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : 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
inst_6 : SMulCommClass R S S
⊢ (p * q).smeval x = p.smeval x * q.smeval x
have add : ∀ (r s : R[X]) (hr : (r * q).smeval x = r.smeval x * q.smeval x) (hs : (s * q).smeval x = s.smeval x * q.smeval x),
  ((r + s) * q).smeval x = (r + s).smeval x * q.smeval x
Tactic: induction p using Polynomial.induction_on' with
  | add r s hr hs => simp only [hr, hs, smeval_add, add_mul]
  | monomial n a =>
    simp only [smeval_monomial, smeval_monomial_mul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : 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
inst_6 : SMulCommClass R S S
add :
  ∀ (r s : R[X]) (hr : (r * q).smeval x = r.smeval x * q.smeval x) (hs : (s * q).smeval x = s.smeval x * q.smeval x),
    ((r + s) * q).smeval x = (r + s).smeval x * q.smeval x
⊢ (p * q).smeval x = p.smeval x * q.smeval x
have monomial : ∀ (n : ℕ) (a : R),
  (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) q).smeval x =
    smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x * q.smeval x
Tactic: induction p using Polynomial.induction_on' with
  | add r s hr hs => simp only [hr, hs, smeval_add, add_mul]
  | monomial n a =>
    simp only [smeval_monomial, smeval_monomial_mul, smul_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 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
n : ℕ
⊢ (p ^ (n + 1)).smeval x = p.smeval x ^ (n + 1)
have rw : (p ^ n * HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
Tactic: rw [npow_add, smeval_mul, smeval_pow n, pow_one, npow_add, 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 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
n : ℕ
rw : (p ^ n * HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
⊢ (p ^ (n + 1)).smeval x = p.smeval x ^ (n + 1)
have rw₁ : (p ^ n).smeval x * (HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
Tactic: rw [npow_add, smeval_mul, smeval_pow n, pow_one, npow_add, 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 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
n : ℕ
rw : (p ^ n * HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
rw₁ : (p ^ n).smeval x * (HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
⊢ (p ^ (n + 1)).smeval x = p.smeval x ^ (n + 1)
have rw₂ : p.smeval x ^ n * (HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
Tactic: rw [npow_add, smeval_mul, smeval_pow n, pow_one, npow_add, 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 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
n : ℕ
rw : (p ^ n * HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
rw₁ : (p ^ n).smeval x * (HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
rw₂ : p.smeval x ^ n * (HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
⊢ (p ^ (n + 1)).smeval x = p.smeval x ^ (n + 1)
have rw₃ : p.smeval x ^ n * p.smeval x = p.smeval x ^ (n + 1)
Tactic: rw [npow_add, smeval_mul, smeval_pow n, pow_one, npow_add, 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 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
n : ℕ
rw : (p ^ n * HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
rw₁ : (p ^ n).smeval x * (HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
rw₂ : p.smeval x ^ n * (HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
rw₃ : p.smeval x ^ n * p.smeval x = p.smeval x ^ (n + 1)
⊢ (p ^ (n + 1)).smeval x = p.smeval x ^ (n + 1)
have rw₄ : p.smeval x ^ n * p.smeval x = p.smeval x ^ n * HPow.hPow (β := ℕ) (p.smeval x) 1
Tactic: rw [npow_add, smeval_mul, smeval_pow n, pow_one, npow_add, 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 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
n : ℕ
rw : (p ^ n * HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
rw₁ : (p ^ n).smeval x * (HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
rw₂ : p.smeval x ^ n * (HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
rw₃ : p.smeval x ^ n * p.smeval x = p.smeval x ^ (n + 1)
rw₄ : p.smeval x ^ n * p.smeval x = p.smeval x ^ n * HPow.hPow (β := ℕ) (p.smeval x) 1
⊢ (p ^ (n + 1)).smeval x = p.smeval x ^ (n + 1)
have rw₅ : p.smeval x ^ n * p.smeval x = p.smeval x ^ n * p.smeval x
Tactic: rw [npow_add, smeval_mul, smeval_pow n, pow_one, npow_add, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : 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
inst_6 : SMulCommClass R S S
⊢ (p.comp q).smeval x = p.smeval (q.smeval x)
have add : ∀ (r s : R[X]) (hr : (r.comp q).smeval x = r.smeval (q.smeval x)) (hs : (s.comp q).smeval x = s.smeval (q.smeval x)),
  ((r + s).comp q).smeval x = (r + s).smeval (q.smeval x)
Tactic: induction p using Polynomial.induction_on' with
  | add r s hr hs => simp [add_comp, hr, hs, smeval_add]
  | monomial n a => simp [smeval_monomial, smeval_C_mul, smeval_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : 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
inst_6 : SMulCommClass R S S
add :
  ∀ (r s : R[X]) (hr : (r.comp q).smeval x = r.smeval (q.smeval x)) (hs : (s.comp q).smeval x = s.smeval (q.smeval x)),
    ((r + s).comp q).smeval x = (r + s).smeval (q.smeval x)
⊢ (p.comp q).smeval x = p.smeval (q.smeval x)
have monomial : ∀ (n : ℕ) (a : R),
  (comp ((monomial n : (a : R) → R[X]) a) q).smeval x =
    smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) (q.smeval x)
Tactic: induction p using Polynomial.induction_on' with
  | add r s hr hs => simp [add_comp, hr, hs, smeval_add]
  | monomial n a => simp [smeval_monomial, smeval_C_mul, smeval_pow]
-- 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 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
⊢ Commute (p.smeval x) y
have add : ∀ (r s : R[X]) (hr : Commute (r.smeval x) y) (hs : Commute (s.smeval x) y), Commute ((r + s).smeval x) y
Tactic: induction p using Polynomial.induction_on' with
  | add r s hr hs => exact (smeval_add R r s x) ▸ Commute.add_left hr hs
  | monomial n a => simpa [smeval_monomial] using Commute.smul_left (Commute.pow_left hc _) _
-- 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 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
add : ∀ (r s : R[X]) (hr : Commute (r.smeval x) y) (hs : Commute (s.smeval x) y), Commute ((r + s).smeval x) y
⊢ Commute (p.smeval x) y
have monomial : ∀ (n : ℕ) (a : R), Commute (smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x) y
Tactic: induction p using Polynomial.induction_on' with
  | add r s hr hs => exact (smeval_add R r s x) ▸ Commute.add_left hr hs
  | monomial n a => simpa [smeval_monomial] using Commute.smul_left (Commute.pow_left hc _) _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
⊢ Commute (smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x) (q.smeval y)
have monomial : Commute (a • x ^ n) (q.smeval y)
Tactic: simp only [smeval_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
⊢ Commute (a • x ^ n) (q.smeval y)
have monomial : Commute (x ^ n) (q.smeval y)
Tactic: refine Commute.smul_left ?_ a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : Commute (x ^ n) (q.smeval y)
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)
have ih₁ : x ^ n * q.smeval y = q.smeval y * x ^ n
Tactic: rw [commute_iff_eq (x ^ n) (q.smeval y)] at ih
Cleared hypotheses: ih