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
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
n : ℕ
ih : smeval.{u_1, u_2} (R := R) (↑n : R[X]) x = n • HPow.hPow (β := ℕ) x 0
succ : (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1).smeval x = (n + 1) • HPow.hPow (β := ℕ) x 0
succ₁ : smeval.{u_1, u_2} (R := R) (↑n : R[X]) x + smeval.{u_1, u_2} (R := R) 1 x = (n + 1) • HPow.hPow (β := ℕ) x 0
succ₂ : n • HPow.hPow (β := ℕ) x 0 + smeval.{u_1, u_2} (R := R) 1 x = (n + 1) • HPow.hPow (β := ℕ) x 0
succ₃ : n • HPow.hPow (β := ℕ) x 0 + HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) x 0) = (n + 1) • HPow.hPow (β := ℕ) x 0
⊢ smeval.{u_1, u_2} (R := R) (↑(n + 1) : R[X]) x = (n + 1) • HPow.hPow (β := ℕ) x 0
have succ₄ : (n + 1) • HPow.hPow (β := ℕ) x 0 = (n + 1) • HPow.hPow (β := ℕ) x 0
Tactic: rw [n.cast_succ, smeval_add, ih, smeval_one, ← add_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
n : ℕ
⊢ smeval.{u_1, u_2} (R := R) (↑n : R[X]) x = n • HPow.hPow (β := ℕ) x 0
have zero : smeval.{u_1, u_2} (R := R) (↑0 : R[X]) x = HSMul.hSMul (α := ℕ) 0 (HPow.hPow (β := ℕ) x 0)
Tactic: induction n with
  | zero => simp only [smeval_zero, Nat.cast_zero, zero_smul]
  | succ n ih => rw [n.cast_succ, smeval_add, ih, smeval_one, ← add_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
n : ℕ
zero : smeval.{u_1, u_2} (R := R) (↑0 : R[X]) x = HSMul.hSMul (α := ℕ) 0 (HPow.hPow (β := ℕ) x 0)
⊢ smeval.{u_1, u_2} (R := R) (↑n : R[X]) x = n • HPow.hPow (β := ℕ) x 0
have succ : ∀ (n : ℕ) (ih : smeval.{u_1, u_2} (R := R) (↑n : R[X]) x = n • HPow.hPow (β := ℕ) x 0),
  smeval.{u_1, u_2} (R := R) (↑(n + 1) : R[X]) x = (n + 1) • HPow.hPow (β := ℕ) x 0
Tactic: induction n with
  | zero => simp only [smeval_zero, Nat.cast_zero, zero_smul]
  | succ n ih => rw [n.cast_succ, smeval_add, ih, smeval_one, ← add_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p_1 : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
r : R
p q : R[X]
ph : (r • p).smeval x = r • p.smeval x
qh : (r • q).smeval x = r • q.smeval x
⊢ (r • (p + q)).smeval x = r • (p + q).smeval x
have add : (r • p + r • q).smeval x = r • (p + q).smeval x
Tactic: rw [smul_add, smeval_add, ph, qh, ← smul_add, smeval_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p_1 : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
r : R
p q : R[X]
ph : (r • p).smeval x = r • p.smeval x
qh : (r • q).smeval x = r • q.smeval x
add : (r • p + r • q).smeval x = r • (p + q).smeval x
⊢ (r • (p + q)).smeval x = r • (p + q).smeval x
have add₁ : (r • p).smeval x + (r • q).smeval x = r • (p + q).smeval x
Tactic: rw [smul_add, smeval_add, ph, qh, ← smul_add, smeval_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p_1 : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
r : R
p q : R[X]
ph : (r • p).smeval x = r • p.smeval x
qh : (r • q).smeval x = r • q.smeval x
add : (r • p + r • q).smeval x = r • (p + q).smeval x
add₁ : (r • p).smeval x + (r • q).smeval x = r • (p + q).smeval x
⊢ (r • (p + q)).smeval x = r • (p + q).smeval x
have add₂ : r • p.smeval x + (r • q).smeval x = r • (p + q).smeval x
Tactic: rw [smul_add, smeval_add, ph, qh, ← smul_add, smeval_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p_1 : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
r : R
p q : R[X]
ph : (r • p).smeval x = r • p.smeval x
qh : (r • q).smeval x = r • q.smeval x
add : (r • p + r • q).smeval x = r • (p + q).smeval x
add₁ : (r • p).smeval x + (r • q).smeval x = r • (p + q).smeval x
add₂ : r • p.smeval x + (r • q).smeval x = r • (p + q).smeval x
⊢ (r • (p + q)).smeval x = r • (p + q).smeval x
have add₃ : r • p.smeval x + r • q.smeval x = r • (p + q).smeval x
Tactic: rw [smul_add, smeval_add, ph, qh, ← smul_add, smeval_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p_1 : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
r : R
p q : R[X]
ph : (r • p).smeval x = r • p.smeval x
qh : (r • q).smeval x = r • q.smeval x
add : (r • p + r • q).smeval x = r • (p + q).smeval x
add₁ : (r • p).smeval x + (r • q).smeval x = r • (p + q).smeval x
add₂ : r • p.smeval x + (r • q).smeval x = r • (p + q).smeval x
add₃ : r • p.smeval x + r • q.smeval x = r • (p + q).smeval x
⊢ (r • (p + q)).smeval x = r • (p + q).smeval x
have add₄ : r • (p.smeval x + q.smeval x) = r • (p + q).smeval x
Tactic: rw [smul_add, smeval_add, ph, qh, ← smul_add, smeval_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p_1 : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
r : R
p q : R[X]
ph : (r • p).smeval x = r • p.smeval x
qh : (r • q).smeval x = r • q.smeval x
add : (r • p + r • q).smeval x = r • (p + q).smeval x
add₁ : (r • p).smeval x + (r • q).smeval x = r • (p + q).smeval x
add₂ : r • p.smeval x + (r • q).smeval x = r • (p + q).smeval x
add₃ : r • p.smeval x + r • q.smeval x = r • (p + q).smeval x
add₄ : r • (p.smeval x + q.smeval x) = r • (p + q).smeval x
⊢ (r • (p + q)).smeval x = r • (p + q).smeval x
have add₅ : r • (p.smeval x + q.smeval x) = r • (p.smeval x + q.smeval x)
Tactic: rw [smul_add, smeval_add, ph, qh, ← smul_add, smeval_add]
-- 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 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
r : R
n : ℕ
a : R
⊢ (HSMul.hSMul (β := R[X]) r ((monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    r • smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x
have monomial : smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) (r • a)) x =
  r • smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x
Tactic: rw [smul_monomial, smeval_monomial, smeval_monomial, smul_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 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
r : R
n : ℕ
a : R
monomial :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) (r • a)) x =
    r • smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
⊢ (HSMul.hSMul (β := R[X]) r ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    r • smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
have monomial₁ : (r • a) • x ^ n = r • smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
Tactic: rw [smul_monomial, smeval_monomial, smeval_monomial, smul_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 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
r : R
n : ℕ
a : R
monomial :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) (r • a)) x =
    r • smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₁ : (r • a) • x ^ n = r • smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
⊢ (HSMul.hSMul (β := R[X]) r ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    r • smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
have monomial₂ : (r • a) • x ^ n = r • a • x ^ n
Tactic: rw [smul_monomial, smeval_monomial, smeval_monomial, smul_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 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
r : R
n : ℕ
a : R
monomial :
  smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) (r • a)) x =
    r • smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₁ : (r • a) • x ^ n = r • smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
monomial₂ : (r • a) • x ^ n = r • a • x ^ n
⊢ (HSMul.hSMul (β := R[X]) r ((Polynomial.monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    r • smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x
have monomial₃ : r • a • x ^ n = r • a • x ^ n
Tactic: rw [smul_monomial, smeval_monomial, smeval_monomial, smul_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 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
r : R
⊢ (r • p).smeval x = r • p.smeval x
have add : ∀ (p q : R[X]) (ph : (r • p).smeval x = r • p.smeval x) (qh : (r • q).smeval x = r • q.smeval x),
  (r • (p + q)).smeval x = r • (p + q).smeval x
Tactic: induction p using Polynomial.induction_on' with
  | add p q ph qh => rw [smul_add, smeval_add, ph, qh, ← smul_add, smeval_add]
  | monomial n a => rw [smul_monomial, smeval_monomial, smeval_monomial, smul_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 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
r : R
add :
  ∀ (p q : R[X]) (ph : (r • p).smeval x = r • p.smeval x) (qh : (r • q).smeval x = r • q.smeval x),
    (r • (p + q)).smeval x = r • (p + q).smeval x
⊢ (r • p).smeval x = r • p.smeval x
have monomial : ∀ (n : ℕ) (a : R),
  (HSMul.hSMul (β := R[X]) r ((monomial n : (a : R) → R[X]) a : R[X])).smeval x =
    r • 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 => rw [smul_add, smeval_add, ph, qh, ← smul_add, smeval_add]
  | monomial n a => rw [smul_monomial, smeval_monomial, smeval_monomial, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_3
inst : Semiring R
r : R
⊢ Eq (α := (a : R[X]) → R) (⇑(leval r) : (a : R[X]) → R) fun (p : R[X]) ↦ p.smeval r
have h : ∀ (x : R[X]), (leval r : (a : R[X]) → R) x = x.smeval r
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_3
inst : Semiring R
r : R
⊢ Eq (α := R[X] →ₗ[R] R) (leval r) (smeval.linearMap R r)
have refine : ∀ (x : R[X]), Eq (α := R) ((leval r : (a : R[X]) → R) x : R) ((smeval.linearMap R r : (a : R[X]) → R) x : R)
Tactic: refine LinearMap.ext ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_3
inst : Semiring R
r : R
x : R[X]
⊢ Eq (α := R) ((leval r : (a : R[X]) → R) x : R) ((smeval.linearMap R r : (a : R[X]) → R) x : R)
have rw : eval r x = (smeval.linearMap R r : (a : R[X]) → R) x
Tactic: rw [leval_apply, smeval.linearMap_apply, eval_eq_smeval]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_3
inst : Semiring R
r : R
x : R[X]
rw : eval r x = (smeval.linearMap R r : (a : R[X]) → R) x
⊢ Eq (α := R) ((leval r : (a : R[X]) → R) x : R) ((smeval.linearMap R r : (a : R[X]) → R) x : R)
have rw₁ : eval r x = x.smeval r
Tactic: rw [leval_apply, smeval.linearMap_apply, eval_eq_smeval]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_3
inst : Semiring R
r : R
x : R[X]
rw : eval r x = (smeval.linearMap R r : (a : R[X]) → R) x
rw₁ : eval r x = x.smeval r
⊢ Eq (α := R) ((leval r : (a : R[X]) → R) x : R) ((smeval.linearMap R r : (a : R[X]) → R) x : R)
have rw₂ : x.smeval r = x.smeval r
Tactic: rw [leval_apply, smeval.linearMap_apply, eval_eq_smeval]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : AddCommGroup S
inst_2 : Pow S ℕ
inst_3 : Module R S
p : R[X]
x : S
⊢ (-p).smeval x = -p.smeval x
have rw : (-p).smeval x + p.smeval x = 0
Tactic: rw [← add_eq_zero_iff_eq_neg, ← smeval_add, neg_add_cancel, smeval_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : AddCommGroup S
inst_2 : Pow S ℕ
inst_3 : Module R S
p : R[X]
x : S
rw : (-p).smeval x + p.smeval x = 0
⊢ (-p).smeval x = -p.smeval x
have rw₁ : (-p + p).smeval x = 0
Tactic: rw [← add_eq_zero_iff_eq_neg, ← smeval_add, neg_add_cancel, smeval_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : AddCommGroup S
inst_2 : Pow S ℕ
inst_3 : Module R S
p : R[X]
x : S
rw : (-p).smeval x + p.smeval x = 0
rw₁ : (-p + p).smeval x = 0
⊢ (-p).smeval x = -p.smeval x
have rw₂ : smeval.{u_1, u_2} (R := R) 0 x = 0
Tactic: rw [← add_eq_zero_iff_eq_neg, ← smeval_add, neg_add_cancel, smeval_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : AddCommGroup S
inst_2 : Pow S ℕ
inst_3 : Module R S
p : R[X]
x : S
rw : (-p).smeval x + p.smeval x = 0
rw₁ : (-p + p).smeval x = 0
rw₂ : smeval.{u_1, u_2} (R := R) 0 x = 0
⊢ (-p).smeval x = -p.smeval x
have rw₃ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [← add_eq_zero_iff_eq_neg, ← smeval_add, neg_add_cancel, smeval_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : AddCommGroup S
inst_2 : Pow S ℕ
inst_3 : Module R S
p q : R[X]
x : S
⊢ (p - q).smeval x = p.smeval x - q.smeval x
have rw : (p + -q).smeval x = p.smeval x - q.smeval x
Tactic: rw [sub_eq_add_neg, smeval_add, smeval_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : AddCommGroup S
inst_2 : Pow S ℕ
inst_3 : Module R S
p q : R[X]
x : S
rw : (p + -q).smeval x = p.smeval x - q.smeval x
⊢ (p - q).smeval x = p.smeval x - q.smeval x
have rw₁ : p.smeval x + (-q).smeval x = p.smeval x - q.smeval x
Tactic: rw [sub_eq_add_neg, smeval_add, smeval_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : AddCommGroup S
inst_2 : Pow S ℕ
inst_3 : Module R S
p q : R[X]
x : S
rw : (p + -q).smeval x = p.smeval x - q.smeval x
rw₁ : p.smeval x + (-q).smeval x = p.smeval x - q.smeval x
⊢ (p - q).smeval x = p.smeval x - q.smeval x
have rw₂ : p.smeval x + -q.smeval x = p.smeval x - q.smeval x
Tactic: rw [sub_eq_add_neg, smeval_add, smeval_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : AddCommGroup S
inst_2 : Pow S ℕ
inst_3 : Module R S
p q : R[X]
x : S
rw : (p + -q).smeval x = p.smeval x - q.smeval x
rw₁ : p.smeval x + (-q).smeval x = p.smeval x - q.smeval x
rw₂ : p.smeval x + -q.smeval x = p.smeval x - q.smeval x
⊢ (p - q).smeval x = p.smeval x - q.smeval x
have rw₃ : p.smeval x + -q.smeval x = p.smeval x + -q.smeval x
Tactic: rw [sub_eq_add_neg, smeval_add, smeval_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
S : Type u_3
inst : NonAssocRing S
inst_1 : Pow S ℕ
inst_2 : NatPowAssoc S
q : ℕ[X]
n : ℕ
⊢ Eq.{u_3 + 1} (α := S) (q.smeval (-(↑n : S))) (↑(q.smeval (-(↑n : ℤ))) : S)
have rw : Eq.{u_3 + 1} (α := S) (q.sum (smul_pow (-(↑n : S)))) (↑(q.sum (smul_pow (-(↑n : ℤ)))) : S)
Tactic: rw [smeval_eq_sum, smeval_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
S : Type u_3
inst : NonAssocRing S
inst_1 : Pow S ℕ
inst_2 : NatPowAssoc S
q : ℕ[X]
n : ℕ
⊢ Eq.{u_3 + 1} (α := S) (q.sum (smul_pow (-(↑n : S)))) (↑(q.sum (smul_pow (-(↑n : ℤ)))) : S)
have simp : Eq.{u_3 + 1} (α := S) (∑ x ∈ q.support, q.coeff x • HPow.hPow (α := S) (-(↑n : S)) x)
  (↑(∑ x ∈ q.support, q.coeff x • HPow.hPow (α := ℤ) (-(↑n : ℤ)) x) : S)
Tactic: simp only [Polynomial.smul_pow, sum_def]
-- 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
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).smeval x = r • p.smeval x
have add : ∀ (p q : R[X]) (ph : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).smeval x = r • p.smeval x)
  (qh : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q).smeval x = r • q.smeval x),
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (p + q)).smeval x = r • (p + q).smeval x
Tactic: induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [mul_add, smeval_add, ph, qh, smul_add]
  | monomial n b => simp only [C_mul_monomial, smeval_monomial, mul_smul]
-- 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
add :
  ∀ (p q : R[X]) (ph : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).smeval x = r • p.smeval x)
    (qh : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q).smeval x = r • q.smeval x),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (p + q)).smeval x = r • (p + q).smeval x
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).smeval x = r • p.smeval x
have monomial : ∀ (n : ℕ) (b : R),
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])).smeval
      x =
    r • smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) b) x
Tactic: induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [mul_add, smeval_add, ph, qh, smul_add]
  | monomial n b => simp only [C_mul_monomial, smeval_monomial, mul_smul]
-- 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
n_1 a n : ℕ
⊢ Eq.{u_2 + 1} (α := S) (smeval (R := ℕ) ((monomial n_1 : (a : ℕ) → ℕ[X]) a) (↑n : S))
    (↑(smeval (R := ℕ) ((monomial n_1 : (a : ℕ) → ℕ[X]) a) n) : S)
have monomial : a • HPow.hPow (α := S) (↑n : S) n_1 = (↑(smeval (R := ℕ) ((monomial n_1 : (a : ℕ) → ℕ[X]) a) n) : S)
Tactic: rw [smeval_monomial, smeval_monomial, nsmul_eq_mul, smul_eq_mul, Nat.cast_mul, Nat.cast_npow]
-- 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
n_1 a n : ℕ
monomial :
  a • HPow.hPow (α := S) (↑n : S) n_1 = (↑(smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) n) : S)
⊢ Eq.{u_2 + 1} (α := S) (smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) (↑n : S))
    (↑(smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) n) : S)
have monomial₁ : a • HPow.hPow (α := S) (↑n : S) n_1 = (↑(a • n ^ n_1) : S)
Tactic: rw [smeval_monomial, smeval_monomial, nsmul_eq_mul, smul_eq_mul, Nat.cast_mul, Nat.cast_npow]
-- 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
n_1 a n : ℕ
monomial :
  a • HPow.hPow (α := S) (↑n : S) n_1 = (↑(smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) n) : S)
monomial₁ : a • HPow.hPow (α := S) (↑n : S) n_1 = (↑(a • n ^ n_1) : S)
⊢ Eq.{u_2 + 1} (α := S) (smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) (↑n : S))
    (↑(smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) n) : S)
have monomial₂ : (↑a : S) * HPow.hPow (α := S) (↑n : S) n_1 = (↑(a • n ^ n_1) : S)
Tactic: rw [smeval_monomial, smeval_monomial, nsmul_eq_mul, smul_eq_mul, Nat.cast_mul, Nat.cast_npow]
-- 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
n_1 a n : ℕ
monomial :
  a • HPow.hPow (α := S) (↑n : S) n_1 = (↑(smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) n) : S)
monomial₁ : a • HPow.hPow (α := S) (↑n : S) n_1 = (↑(a • n ^ n_1) : S)
monomial₂ : (↑a : S) * HPow.hPow (α := S) (↑n : S) n_1 = (↑(a • n ^ n_1) : S)
⊢ Eq.{u_2 + 1} (α := S) (smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) (↑n : S))
    (↑(smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) n) : S)
have monomial₃ : (↑a : S) * HPow.hPow (α := S) (↑n : S) n_1 = (↑(a * n ^ n_1) : S)
Tactic: rw [smeval_monomial, smeval_monomial, nsmul_eq_mul, smul_eq_mul, Nat.cast_mul, Nat.cast_npow]
-- 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
n_1 a n : ℕ
monomial :
  a • HPow.hPow (α := S) (↑n : S) n_1 = (↑(smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) n) : S)
monomial₁ : a • HPow.hPow (α := S) (↑n : S) n_1 = (↑(a • n ^ n_1) : S)
monomial₂ : (↑a : S) * HPow.hPow (α := S) (↑n : S) n_1 = (↑(a • n ^ n_1) : S)
monomial₃ : (↑a : S) * HPow.hPow (α := S) (↑n : S) n_1 = (↑(a * n ^ n_1) : S)
⊢ Eq.{u_2 + 1} (α := S) (smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) (↑n : S))
    (↑(smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) n) : S)
have monomial₄ : (↑a : S) * HPow.hPow (α := S) (↑n : S) n_1 = HMul.hMul (α := S) (↑a : S) (↑(n ^ n_1) : S)
Tactic: rw [smeval_monomial, smeval_monomial, nsmul_eq_mul, smul_eq_mul, Nat.cast_mul, Nat.cast_npow]
-- 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
n_1 a n : ℕ
monomial :
  a • HPow.hPow (α := S) (↑n : S) n_1 = (↑(smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) n) : S)
monomial₁ : a • HPow.hPow (α := S) (↑n : S) n_1 = (↑(a • n ^ n_1) : S)
monomial₂ : (↑a : S) * HPow.hPow (α := S) (↑n : S) n_1 = (↑(a • n ^ n_1) : S)
monomial₃ : (↑a : S) * HPow.hPow (α := S) (↑n : S) n_1 = (↑(a * n ^ n_1) : S)
monomial₄ : (↑a : S) * HPow.hPow (α := S) (↑n : S) n_1 = HMul.hMul (α := S) (↑a : S) (↑(n ^ n_1) : S)
⊢ Eq.{u_2 + 1} (α := S) (smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) (↑n : S))
    (↑(smeval (R := ℕ) ((Polynomial.monomial n_1 : (a : ℕ) → ℕ[X]) a) n) : S)
have monomial₅ : (↑a : S) * HPow.hPow (α := S) (↑n : S) n_1 = (↑a : S) * HPow.hPow (α := S) (↑n : S) n_1
Tactic: rw [smeval_monomial, smeval_monomial, nsmul_eq_mul, smul_eq_mul, Nat.cast_mul, Nat.cast_npow]
-- 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]
⊢ ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) (q.smeval (↑n : S)) (↑(q.smeval n) : S)
have 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)
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