awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
hpairwise :
  Set.Pairwise (α := ℕ) {i : ℕ | i ∈ s ∧ g i • (↑S : ℕ → R[X]) i ≠ 0}
    (Function.onFun (β := WithBot ℕ) Ne fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree)
n : WithBot ℕ
hn : (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) = n
hsum : degree.{u_1} (R := R) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) = s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree
⊢ degree.{u_1} (R := R) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) ≠ ⊥

Tactic:
exact hsum.trans hn |>.trans_ne <| (ne_of_ne_of_eq (hsupzero ·.symm) hn).symm

Premises used: Ne.symm, Eq.trans_ne, Eq.symm, ne_of_ne_of_eq, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
hCoeff : ∀ (i : ℕ), IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
i : ℕ
⊢ (S.basis hCoeff : (a : ℕ) → R[X]) i = (↑S : ℕ → R[X]) i

Tactic:
Basis.mk_apply _ _ _

Premises used: Module.Basis.mk_apply
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
hCoeff : ∀ (i : ℕ), IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
x x_1 : ℕ
⊢ x < x_1 →
    Function.comp (β := R[X]) degree (⇑(S.basis hCoeff) : (a : ℕ) → R[X]) x <
      Function.comp (β := R[X]) degree (⇑(S.basis hCoeff) : (a : ℕ) → R[X]) x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
hCoeff : ∀ (i : ℕ), IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
x x_1 : ℕ
⊢ x < x_1 →
    Function.comp (β := R[X]) natDegree (⇑(S.basis hCoeff) : (a : ℕ) → R[X]) x <
      Function.comp (β := R[X]) natDegree (⇑(S.basis hCoeff) : (a : ℕ) → R[X]) x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Smeval
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 : MulActionWithZero R S
x : S
rw rw₁ : p.sum (smul_pow x) = p.sum (smul_pow x)
⊢ p.smeval x = p.sum (smul_pow x)

Tactic:
rw [smeval_def]

Premises used: Polynomial.smeval_def
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
r : R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : MulActionWithZero R S
x : S
⊢ smeval.{u_1, u_2} (R := R) ((C : (a : R) → R[X]) r) x = r • HPow.hPow (β := ℕ) x 0

Tactic:
simp only [smeval_eq_sum, smul_pow, zero_smul, sum_C_index]

Premises used: Polynomial.sum_C_index, Polynomial.smul_pow, zero_smul, Polynomial.smeval_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
r : R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : MulActionWithZero R S
x : S
n : ℕ
⊢ smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) r) x = r • x ^ n

Tactic:
simp only [smeval_eq_sum, smul_pow, zero_smul, sum_monomial_index]

Premises used: Polynomial.sum_monomial_index, Polynomial.smul_pow, zero_smul, Polynomial.smeval_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
r : R
p : R[X]
rw : (p.sum fun (e : ℕ) (a : R) ↦ a * r ^ e) = p.sum (smul_pow r)
⊢ eval r p = p.smeval r

Tactic:
rw [eval_eq_sum, smeval_eq_sum]

Premises used: Polynomial.eval_eq_sum, Polynomial.smeval_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
r : R
p : R[X]
⊢ (p.sum fun (e : ℕ) (a : R) ↦ a * r ^ e) = p.sum (smul_pow r)

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_3
inst : Semiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
p : R[X]
x : S
rw :
  (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((RingHom.smulOneHom : (a : R) → S) a : S) (x ^ e)) =
    p.sum (smul_pow x)
⊢ eval₂ RingHom.smulOneHom x p = p.smeval x

Tactic:
rw [smeval_eq_sum, eval₂_eq_sum]

Premises used: Polynomial.smeval_eq_sum, Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_3
inst : Semiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
p : R[X]
x : S
e_f : ∀ (e : ℕ) (a : R), HMul.hMul (α := S) ((RingHom.smulOneHom : (a : R) → S) a : S) (x ^ e) = smul_pow x e a
⊢ (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((RingHom.smulOneHom : (a : R) → S) a : S) (x ^ e)) =
    p.sum (smul_pow x)

Tactic:
congr 1 with e a
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_3
inst : Semiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
p : R[X]
x : S
e : ℕ
a : R
⊢ HMul.hMul (α := S) ((RingHom.smulOneHom : (a : R) → S) a : S) (x ^ e) = smul_pow x e a

Tactic:
simp only [RingHom.smulOneHom_apply, smul_one_mul, smul_pow]

Premises used: Polynomial.smul_pow, smul_one_mul, RingHom.smulOneHom_apply
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : MulActionWithZero R S
x : S
⊢ smeval.{u_1, u_2} (R := R) 0 x = 0

Tactic:
simp only [smeval_eq_sum, sum_zero_index]

Premises used: Polynomial.sum_zero_index, Polynomial.smeval_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : MulActionWithZero R S
x : S
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (HPow.hPow (β := ℕ) x 0) = HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) x 0)
⊢ smeval.{u_1, u_2} (R := R) 1 x = HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) x 0)

Tactic:
rw [← C_1, smeval_C]

Premises used: Polynomial.C_1, Polynomial.smeval_C
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : MulActionWithZero R S
x : S
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (HPow.hPow (β := ℕ) x 0) = HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) x 0)

Tactic:
simp only [one_smul]

Premises used: one_smul
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : MulActionWithZero R S
x : S
⊢ smeval.{u_1, u_2} (R := R) X x = HPow.hPow (β := ℕ) x 1

Tactic:
simp only [smeval_eq_sum, smul_pow, zero_smul, sum_X_index, one_smul]

Premises used: Polynomial.sum_X_index, Polynomial.smul_pow, one_smul, zero_smul, Polynomial.smeval_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : MulActionWithZero R S
x : S
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).smeval x = x ^ n

Tactic:
simp only [smeval_eq_sum, smul_pow, X_pow_eq_monomial, zero_smul, sum_monomial_index, one_smul]

Premises used: Polynomial.X_pow_eq_monomial, Polynomial.sum_monomial_index, Polynomial.smul_pow, one_smul, zero_smul, Polynomial.smeval_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
simp : (p + q).sum (smul_pow x) = p.sum (smul_pow x) + q.sum (smul_pow x)
⊢ (p + q).smeval x = p.smeval x + q.smeval x

Tactic:
simp only [smeval_eq_sum]

Premises used: Polynomial.smeval_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
⊢ (p + q).sum (smul_pow x) = p.sum (smul_pow x) + q.sum (smul_pow x)

Tactic:
sum_add_index p q (smul_pow x) (fun _ ↦ ?_) (fun _ _ _ ↦ ?_)

Premises used: Polynomial.smul_pow, Polynomial.sum_add_index
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
refine_1 : ∀ (x_1 : ℕ), smul_pow.{u_1, u_2} (R := R) x x_1 0 = 0
refine_2 : ∀ (x_1 : ℕ) (x_2 x_3 : R), smul_pow x x_1 (x_2 + x_3) = smul_pow x x_1 x_2 + smul_pow x x_1 x_3
⊢ (p + q).sum (smul_pow x) = p.sum (smul_pow x) + q.sum (smul_pow x)

Tactic:
refine sum_add_index p q (smul_pow x) (fun _ ↦ ?_) (fun _ _ _ ↦ ?_)

Premises used: Polynomial.smul_pow, Polynomial.sum_add_index
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
x_1 : ℕ
refine_1 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ x_1) = 0
refine_1₁ refine_1₂ : Eq.{u_2 + 1} (α := S) 0 0
⊢ smul_pow.{u_1, u_2} (R := R) x x_1 0 = 0

Tactic:
rw [smul_pow, zero_smul]

Premises used: Polynomial.smul_pow, zero_smul
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
x_1 : ℕ
x_2 x_3 : R
refine_2 : (x_2 + x_3) • x ^ x_1 = smul_pow x x_1 x_2 + smul_pow x x_1 x_3
refine_2₁ : (x_2 + x_3) • x ^ x_1 = x_2 • x ^ x_1 + smul_pow x x_1 x_3
refine_2₂ : (x_2 + x_3) • x ^ x_1 = x_2 • x ^ x_1 + x_3 • x ^ x_1
refine_2₃ refine_2₄ : x_2 • x ^ x_1 + x_3 • x ^ x_1 = x_2 • x ^ x_1 + x_3 • x ^ x_1
⊢ smul_pow x x_1 (x_2 + x_3) = smul_pow x x_1 x_2 + smul_pow x x_1 x_3

Tactic:
rw [smul_pow, smul_pow, smul_pow, add_smul]

Premises used: Polynomial.smul_pow, add_smul
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
⊢ smeval.{u_1, u_2} (R := R) (↑0 : R[X]) x = HSMul.hSMul (α := ℕ) 0 (HPow.hPow (β := ℕ) x 0)

Tactic:
simp only [smeval_zero, Nat.cast_zero, zero_smul]

Premises used: zero_smul, Nat.cast_zero, Polynomial.smeval_zero
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
succ₄ succ₅ : (n + 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

Tactic:
rw [n.cast_succ, smeval_add, ih, smeval_one, ← add_nsmul]

Premises used: Nat.cast_succ, Polynomial.smeval_one, Polynomial.smeval_add, add_nsmul
-- Module: Mathlib.Algebra.Polynomial.Smeval
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)
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
⊢ smeval.{u_1, u_2} (R := R) (↑n : R[X]) x = n • 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]

Premises used: Nat.cast_succ, Polynomial.smeval_one, zero_smul, Polynomial.smeval_add, Nat.cast_zero, Polynomial.smeval_zero, add_nsmul
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
add₅ add₆ : r • (p.smeval x + q.smeval x) = r • (p.smeval x + q.smeval x)
⊢ (r • (p + q)).smeval x = r • (p + q).smeval x

Tactic:
rw [smul_add, smeval_add, ph, qh, ← smul_add, smeval_add]

Premises used: Polynomial.smeval_add, smul_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
monomial₃ 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

Tactic:
rw [smul_monomial, smeval_monomial, smeval_monomial, smul_assoc]

Premises used: smul_assoc, Polynomial.smul_monomial, Polynomial.smeval_monomial
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
monomial :
  ∀ (n : ℕ) (a : R),
    (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
⊢ (r • p).smeval x = r • p.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]

Premises used: smul_assoc, Polynomial.smul_monomial, Polynomial.monomial, Polynomial.smeval_monomial, Polynomial.smeval_add, smul_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
f g : R[X]
⊢ (f + g).smeval x = f.smeval x + g.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
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
c : R
f : R[X]
⊢ (c • f).smeval x = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (f.smeval x)

Tactic:
simp only [smeval_smul, RingHom.id_apply]

Premises used: RingHom.id_apply, Polynomial.smeval_smul
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
⊢ (linearMap R x : (a : R[X]) → S) p = p.smeval x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_3
inst : Semiring R
r : R
h : ∀ (x : R[X]), (leval r : (a : R[X]) → R) x = x.smeval r
⊢ Eq (α := (a : R[X]) → R) (⇑(leval r) : (a : R[X]) → R) fun (p : R[X]) ↦ p.smeval r

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_3
inst : Semiring R
r : R
x : R[X]
⊢ (leval r : (a : R[X]) → R) x = x.smeval r

Tactic:
simpa using eval_eq_smeval _ _

Premises used: Polynomial.eval_eq_smeval
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_3
inst : Semiring R
r : R
⊢ Eq (α := R[X] →ₗ[R] R) (leval r) (smeval.linearMap R r)

Tactic:
LinearMap.ext ?_

Premises used: LinearMap.ext
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_3
inst : Semiring R
r : R
refine : ∀ (x : R[X]), Eq (α := R) ((leval r : (a : R[X]) → R) x : R) ((smeval.linearMap R r : (a : R[X]) → R) x : R)
⊢ Eq (α := R[X] →ₗ[R] R) (leval r) (smeval.linearMap R r)

Tactic:
refine LinearMap.ext ?_

Premises used: LinearMap.ext
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
rw₂ rw₃ : x.smeval r = x.smeval r
⊢ Eq (α := R) ((leval r : (a : R[X]) → R) x : R) ((smeval.linearMap R r : (a : R[X]) → R) x : R)

Tactic:
rw [leval_apply, smeval.linearMap_apply, eval_eq_smeval]

Premises used: Polynomial.smeval.linearMap_apply, Polynomial.leval_apply, Polynomial.eval_eq_smeval
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
rw₃ rw₄ : Eq.{u_2 + 1} (α := S) 0 0
⊢ (-p).smeval x = -p.smeval x

Tactic:
rw [← add_eq_zero_iff_eq_neg, ← smeval_add, neg_add_cancel, smeval_zero]

Premises used: add_eq_zero_iff_eq_neg, neg_add_cancel, Polynomial.smeval_add, Polynomial.smeval_zero
-- Module: Mathlib.Algebra.Polynomial.Smeval
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
rw₃ rw₄ : p.smeval x + -q.smeval x = p.smeval x + -q.smeval x
⊢ (p - q).smeval x = p.smeval x - q.smeval x

Tactic:
rw [sub_eq_add_neg, smeval_add, smeval_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, Polynomial.smeval_add, Polynomial.smeval_neg
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
S : Type u_3
inst : NonAssocRing S
inst_1 : Pow S ℕ
inst_2 : NatPowAssoc S
q : ℕ[X]
n : ℕ
rw : Eq.{u_3 + 1} (α := S) (q.sum (smul_pow (-(↑n : S)))) (↑(q.sum (smul_pow (-(↑n : ℤ)))) : S)
⊢ Eq.{u_3 + 1} (α := S) (q.smeval (-(↑n : S))) (↑(q.smeval (-(↑n : ℤ))) : S)

Tactic:
rw [smeval_eq_sum, smeval_eq_sum]

Premises used: Polynomial.smeval_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
S : Type u_3
inst : NonAssocRing S
inst_1 : Pow S ℕ
inst_2 : NatPowAssoc S
q : ℕ[X]
n : ℕ
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)
⊢ Eq.{u_3 + 1} (α := S) (q.sum (smul_pow (-(↑n : S)))) (↑(q.sum (smul_pow (-(↑n : ℤ)))) : S)

Tactic:
simp only [Polynomial.smul_pow, sum_def]

Premises used: Polynomial.smul_pow, Polynomial.sum_def
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
S : Type u_3
inst : NonAssocRing S
inst_1 : Pow S ℕ
inst_2 : NatPowAssoc S
q : ℕ[X]
n : ℕ
⊢ 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
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
r : R
p_1 : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
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:
simp only [mul_add, smeval_add, ph, qh, smul_add]

Premises used: mul_add, Polynomial.smeval_add, smul_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
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:
simp only [C_mul_monomial, smeval_monomial, mul_smul]

Premises used: Polynomial.C_mul_monomial, Polynomial.smeval_monomial, SemigroupAction.mul_smul
-- 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
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
monomial :
  ∀ (n : ℕ) (b : R),
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
            ((Polynomial.monomial n : (a : R) → R[X]) b : R[X])).smeval
        x =
      r • smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) b) x
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).smeval x = r • p.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]

Premises used: Polynomial.monomial, Polynomial.C_mul_monomial, Polynomial.smeval_monomial, mul_add, Polynomial.smeval_add, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
S : Type u_2
inst : NonAssocSemiring S
inst_1 : Pow S ℕ
inst_2 : NatPowAssoc S
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:
simp only [smeval_add, ph, qh, Nat.cast_add]

Premises used: Nat.cast_add, Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
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)
monomial₅ monomial₆ : (↑a : S) * HPow.hPow (α := S) (↑n : S) n_1 = (↑a : S) * HPow.hPow (α := S) (↑n : S) n_1
⊢ 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)

Tactic:
rw [smeval_monomial, smeval_monomial, nsmul_eq_mul, smul_eq_mul, Nat.cast_mul, Nat.cast_npow]

Premises used: Nat.cast_npow, Nat.cast_mul, Polynomial.smeval_monomial, nsmul_eq_mul, smul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
S : Type u_2
inst : NonAssocSemiring S
inst_1 : Pow S ℕ
inst_2 : NatPowAssoc S
q : ℕ[X]
add :
  ∀ (p q : ℕ[X]) (ph : ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) (p.smeval (↑n : S)) (↑(p.smeval n) : S))
    (qh : ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) (q.smeval (↑n : S)) (↑(q.smeval n) : S)) (n : ℕ),
    Eq.{u_2 + 1} (α := S) ((p + q).smeval (↑n : S)) (↑((p + q).smeval n) : S)
monomial :
  ∀ (n a n_1 : ℕ),
    Eq.{u_2 + 1} (α := S) (smeval (R := ℕ) ((Polynomial.monomial n : (a : ℕ) → ℕ[X]) a) (↑n_1 : S))
      (↑(smeval (R := ℕ) ((Polynomial.monomial n : (a : ℕ) → ℕ[X]) a) n_1) : S)
⊢ ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) (q.smeval (↑n : S)) (↑(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]

Premises used: Polynomial.monomial, Nat.cast_npow, Nat.cast_add, Nat.cast_mul, Polynomial.smeval_monomial, nsmul_eq_mul, Polynomial.smeval_add, smul_eq_mul