awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
⊢ Eq (α := R) (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (x ^ e))
    (p.sum fun (e : ℕ) (a : R) ↦ a * x ^ e)

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
f : R →+* S
r : R
rw :
  Eq.{u_1 + 1} (α := S)
    (∑ n ∈ p.support,
      HMul.hMul (α := S) ((f : (a : R) → S) (p.coeff n) : S) (HPow.hPow (α := S) ((f : (a : R) → S) r : S) n))
    (∑ x ∈ p.support, (f : (a : R) → S) (p.coeff x * r ^ x))
⊢ eval₂ f ((f : (a : R) → S) r) p = (f : (a : R) → S) (eval r p)

Tactic:
rw [eval₂_eq_sum, eval_eq_sum, sum, sum, map_sum f]

Premises used: Polynomial.sum, map_sum, Polynomial.eval_eq_sum, Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
f : R →+* S
r : R
⊢ Eq.{u_1 + 1} (α := S)
    (∑ n ∈ p.support,
      HMul.hMul (α := S) ((f : (a : R) → S) (p.coeff n) : S) (HPow.hPow (α := S) ((f : (a : R) → S) r : S) n))
    (∑ x ∈ p.support, (f : (a : R) → S) (p.coeff x * r ^ x))

Tactic:
simp only [f.map_mul, f.map_pow]

Premises used: RingHom.map_mul, RingHom.map_pow
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
f : R →+* S
⊢ eval₂ f ((f : (a : R) → S) 1) p = (f : (a : R) → S) (eval 1 p)

Tactic:
eval₂_at_apply (p := p) f 1

Premises used: Polynomial.eval₂_at_apply, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
f : R →+* S
h : Eq.{u_1 + 1} (α := S) (1 : S) ((f : (a : R) → S) 1 : S)
⊢ eval₂ f 1 p = (f : (a : R) → S) (eval 1 p)

Tactic:
convert! eval₂_at_apply (p := p) f 1

Premises used: Polynomial.eval₂_at_apply, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
f : R →+* S
⊢ Eq.{u_1 + 1} (α := S) (1 : S) ((f : (a : R) → S) 1 : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
f : R →+* S
n : ℕ
⊢ eval₂ f ((f : (a : R) → S) (↑n : R)) p = (f : (a : R) → S) (eval (↑n : R) p)

Tactic:
eval₂_at_apply (p := p) f n

Premises used: Nat.cast, Polynomial.eval₂_at_apply
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
f : R →+* S
n : ℕ
h : Eq.{u_1 + 1} (α := S) ((↑n : S) : S) ((f : (a : R) → S) (↑n : R) : S)
⊢ eval₂ f (↑n : S) p = (f : (a : R) → S) (eval (↑n : R) p)

Tactic:
convert! eval₂_at_apply (p := p) f n

Premises used: Nat.cast, Polynomial.eval₂_at_apply
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
f : R →+* S
n : ℕ
⊢ Eq.{u_1 + 1} (α := S) ((↑n : S) : S) ((f : (a : R) → S) (↑n : R) : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
f : R →+* S
n : ℕ
inst_2 : n.AtLeastTwo
⊢ eval₂ f (OfNat.ofNat n) p = (f : (a : R) → S) (eval (OfNat.ofNat n) p)

Tactic:
simp [OfNat.ofNat]

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
x : R
⊢ eval x ((C : (a : R) → R[X]) a) = a

Tactic:
eval₂_C _ _

Premises used: Polynomial.eval, Polynomial.eval₂_C
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
x : R
n : ℕ
⊢ eval x (↑n : R[X]) = (↑n : R)

Tactic:
simp only [← C_eq_natCast, eval_C]

Premises used: Polynomial.eval_C, Polynomial.C_eq_natCast
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
inst_1 : n.AtLeastTwo
a : R
⊢ eval a (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
simp only [OfNat.ofNat, eval_natCast]

Premises used: Polynomial.eval_natCast, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
x : R
⊢ eval x X = x

Tactic:
eval₂_X _ _

Premises used: Polynomial.eval, Polynomial.eval₂_X
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
x : R
n : ℕ
a : R
⊢ eval x ((monomial n : (a : R) → R[X]) a) = a * x ^ n

Tactic:
eval₂_monomial _ _

Premises used: Polynomial.eval, Polynomial.eval₂_monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
x : R
⊢ eval x 0 = 0

Tactic:
eval₂_zero _ _

Premises used: Polynomial.eval, Polynomial.eval₂_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
x : R
⊢ eval x (p + q) = eval x p + eval x q

Tactic:
eval₂_add _ _

Premises used: Polynomial.eval, Polynomial.eval₂_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
x : R
⊢ eval x 1 = 1

Tactic:
eval₂_one _ _

Premises used: Polynomial.eval, Polynomial.eval₂_one
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
p_1 : R[X]
x : R
p q : R[X]
ph : eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p) = a * eval x p
qh : eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q) = a * eval x q
⊢ eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p + q)) = a * eval x (p + q)

Tactic:
simp only [mul_add, eval_add, ph, qh]

Premises used: Polynomial.eval_add, mul_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
x : R
n : ℕ
b : R
⊢ eval x (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])) =
    a * eval x ((monomial n : (a : R) → R[X]) b)

Tactic:
simp only [mul_assoc, C_mul_monomial, eval_monomial]

Premises used: mul_assoc, Polynomial.C_mul_monomial, Polynomial.eval_monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
x : R
add :
  ∀ (p q : R[X]) (ph : eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p) = a * eval x p)
    (qh : eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q) = a * eval x q),
    eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p + q)) = a * eval x (p + q)
monomial :
  ∀ (n : ℕ) (b : R),
    eval x
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X])
          ((Polynomial.monomial n : (a : R) → R[X]) b : R[X])) =
      a * eval x ((Polynomial.monomial n : (a : R) → R[X]) b)
⊢ eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p) = a * eval x p

Tactic:
induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [mul_add, eval_add, ph, qh]
  | monomial n b => simp only [mul_assoc, C_mul_monomial, eval_monomial]

Premises used: mul_assoc, Polynomial.monomial, Polynomial.C_mul_monomial, Polynomial.eval_add, mul_add, Polynomial.eval_monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
n : ℕ
rw : eval x ((C : (a : R) → R[X]) (↑n : R) * p) = (↑n : R) * eval x p
rw₁ rw₂ : (↑n : R) * eval x p = (↑n : R) * eval x p
⊢ eval x ((↑n : R[X]) * p) = (↑n : R) * eval x p

Tactic:
rw [← C_eq_natCast, eval_C_mul]

Premises used: Polynomial.C_eq_natCast, Polynomial.eval_C_mul
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
⊢ eval x (p * X) = eval x p * x

Tactic:
eval₂_mul_X ..

Premises used: Polynomial.eval, Polynomial.eval₂_mul_X
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
⊢ eval x (p * HPow.hPow (α := R[X]) (β := ℕ) X 0) = eval x p * HPow.hPow (β := ℕ) x 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
k : ℕ
ih : eval x (p * HPow.hPow (α := R[X]) X k) = eval x p * x ^ k
⊢ eval x (p * HPow.hPow (α := R[X]) X (k + 1)) = eval x p * x ^ (k + 1)

Tactic:
simp [pow_succ, ← mul_assoc, ih]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
k : ℕ
zero : eval x (p * HPow.hPow (α := R[X]) (β := ℕ) X 0) = eval x p * HPow.hPow (β := ℕ) x 0
succ :
  ∀ (k : ℕ) (ih : eval x (p * HPow.hPow (α := R[X]) X k) = eval x p * x ^ k),
    eval x (p * HPow.hPow (α := R[X]) X (k + 1)) = eval x p * x ^ (k + 1)
⊢ eval x (p * HPow.hPow (α := R[X]) X k) = eval x p * x ^ k

Tactic:
induction k with
  | zero => simp
  | succ k ih => simp [pow_succ, ← mul_assoc, ih]

Premises used: pow_succ, mul_assoc, AddMonoidAlgebra.zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
x : R
h : Commute a x
rw : HMul.hMul (β := R) (eval₂ (RingHom.id R) x p) ((RingHom.id R : (a : R) → R) a : R) = eval x p * a
h₁ : Commute ((RingHom.id R : (a : R) → R) a) x
⊢ eval x (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])) = eval x p * a

Tactic:
rw [eval, eval₂_mul_C']

Premises used: Polynomial.eval, Polynomial.eval₂_mul_C'
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
x : R
h : Commute a x
⊢ HMul.hMul (β := R) (eval₂ (RingHom.id R) x p) ((RingHom.id R : (a : R) → R) a : R) = eval x p * a

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
x : R
h : Commute a x
⊢ Commute ((RingHom.id R : (a : R) → R) a) x

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
l : List R[X]
x : R
⊢ eval x l.sum = (List.map (eval x) l).sum

Tactic:
eval₂_list_sum ..

Premises used: Polynomial.eval, Polynomial.eval₂_list_sum
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
s : Multiset R[X]
x : R
⊢ eval x s.sum = (Multiset.map (eval x) s).sum

Tactic:
eval₂_multiset_sum ..

Premises used: Polynomial.eval, Polynomial.eval₂_multiset_sum
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
f : ℕ → R → R[X]
x : R
⊢ eval x (p.sum f) = p.sum fun (n : ℕ) (a : R) ↦ eval x (f n a)

Tactic:
eval₂_sum _ _ _ _

Premises used: Polynomial.eval, Polynomial.eval₂_sum
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
ι : Type y
inst : Semiring R
s : Finset ι
g : ι → R[X]
x : R
⊢ eval x (∑ i ∈ s, g i) = ∑ i ∈ s, eval x (g i)

Tactic:
eval₂_finsetSum _ _ _ _

Premises used: Polynomial.eval, Polynomial.eval₂_finsetSum
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
⊢ p.IsRoot a ↔ eval a p = 0

Tactic:
Iff.rfl

Premises used: Polynomial.IsRoot, Iff.rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
h : p.IsRoot x
⊢ eval x p = 0

Tactic:
h

Premises used: Polynomial.IsRoot
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
x : R
h : p.IsRoot x
hpq : p ∣ q
rwa : eval x q = 0
rwa₁ : eval₂ (RingHom.id R) x q = 0
rwa₂ : Eq.{u_1 + 1} (α := R) 0 0
rwa₃ : eval₂ (RingHom.id R) x p = 0
rwa₄ : Eq.{u_1 + 1} (α := R) 0 0
rwa₅ rwa₆ rwa₇ : eval₂ (RingHom.id R) x p = 0
⊢ q.IsRoot x

Tactic:
rwa [IsRoot, eval, eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hpq]

Premises used: Polynomial.eval, Polynomial.IsRoot, Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
r a : R
hr : r ≠ 0
⊢ ¬IsRoot ((C : (a : R) → R[X]) r) a

Tactic:
simpa using hr
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
x : R
⊢ Function.Surjective (α := R[X]) (eval x)

Tactic:
fun y => ⟨C y, eval_C⟩

Premises used: Polynomial.C, Polynomial.eval_C, Exists.intro, DFunLike.coe, Function.Surjective
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
rw : eval₂ C q p = p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q ^ e)
rw₁ rw₂ :
  Eq (α := R[X]) (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q ^ e))
    (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q ^ e))
⊢ p.comp q = p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q ^ e)

Tactic:
rw [comp, eval₂_eq_sum]

Premises used: Polynomial.eval₂_eq_sum, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
simp : (p.sum fun (e : ℕ) (a : R) ↦ (monomial e : (a : R) → R[X]) a) = p
⊢ p.comp X = p

Tactic:
simp only [comp, eval₂_def, C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.eval₂_def, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (p.sum fun (e : ℕ) (a : R) ↦ (monomial e : (a : R) → R[X]) a) = p

Tactic:
sum_monomial_eq _

Premises used: Polynomial.sum_monomial_eq
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (p.sum fun (e : ℕ) (a : R) ↦ (monomial e : (a : R) → R[X]) a) = p

Tactic:
exact sum_monomial_eq _

Premises used: Polynomial.sum_monomial_eq
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ comp X p = p

Tactic:
eval₂_X _ _

Premises used: Polynomial.eval₂_X, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
⊢ p.comp ((C : (a : R) → R[X]) a) = (C : (a : R) → R[X]) (eval a p)

Tactic:
simp [comp]

Premises used: Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
⊢ comp ((C : (a : R) → R[X]) a) p = (C : (a : R) → R[X]) a

Tactic:
eval₂_C _ _

Premises used: Polynomial.eval₂_C, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
rw : comp ((C : (a : R) → R[X]) (↑n : R)) p = (C : (a : R) → R[X]) (↑n : R)
rw₁ rw₂ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) ((C : (a : R) → R[X]) (↑n : R))
⊢ comp (↑n : R[X]) p = (↑n : R[X])

Tactic:
rw [← C_eq_natCast, C_comp]

Premises used: Polynomial.C_eq_natCast, Polynomial.C_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
inst_1 : n.AtLeastTwo
⊢ comp (OfNat.ofNat n) p = (↑n : R[X])

Tactic:
natCast_comp

Premises used: Polynomial.natCast_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p.comp ((C : (a : R) → R[X]) 0) = (C : (a : R) → R[X]) (eval 0 p)
rw₁ rw₂ : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval 0 p) : R[X]) ((C : (a : R) → R[X]) (eval 0 p) : R[X])
⊢ p.comp 0 = (C : (a : R) → R[X]) (eval 0 p)

Tactic:
rw [← C_0, comp_C]

Premises used: Polynomial.C_0, Polynomial.comp_C
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : comp ((C : (a : R) → R[X]) 0) p = (C : (a : R) → R[X]) 0
rw₁ rw₂ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 0) ((C : (a : R) → R[X]) 0)
⊢ comp 0 p = 0

Tactic:
rw [← C_0, C_comp]

Premises used: Polynomial.C_0, Polynomial.C_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p.comp ((C : (a : R) → R[X]) 1) = (C : (a : R) → R[X]) (eval 1 p)
rw₁ rw₂ : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval 1 p) : R[X]) ((C : (a : R) → R[X]) (eval 1 p) : R[X])
⊢ p.comp 1 = (C : (a : R) → R[X]) (eval 1 p)

Tactic:
rw [← C_1, comp_C]

Premises used: Polynomial.C_1, Polynomial.comp_C
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : comp ((C : (a : R) → R[X]) 1) p = (C : (a : R) → R[X]) 1
rw₁ rw₂ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) ((C : (a : R) → R[X]) 1)
⊢ comp 1 p = 1

Tactic:
rw [← C_1, C_comp]

Premises used: Polynomial.C_1, Polynomial.C_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p q r : R[X]
⊢ (p + q).comp r = p.comp r + q.comp r

Tactic:
eval₂_add _ _

Premises used: Polynomial.comp, Polynomial.eval₂_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
n : ℕ
⊢ comp ((monomial n : (a : R) → R[X]) a) p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p ^ n)

Tactic:
eval₂_monomial _ _

Premises used: Polynomial.eval₂_monomial, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p_1 r p q : R[X]
hp : (p * X).comp r = p.comp r * r
hq : (q * X).comp r = q.comp r * r
⊢ ((p + q) * X).comp r = (p + q).comp r * r

Tactic:
simp only [hp, hq, add_mul, add_comp]

Premises used: add_mul, Polynomial.add_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p r : R[X]
n : ℕ
b : R
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) b : R[X]) X).comp r =
    comp ((monomial n : (a : R) → R[X]) b) r * r

Tactic:
simp only [pow_succ, mul_assoc, monomial_mul_X, monomial_comp]

Premises used: pow_succ, mul_assoc, Polynomial.monomial_mul_X, Polynomial.monomial_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p r : R[X]
add :
  ∀ (p q : R[X]) (hp : (p * X).comp r = p.comp r * r) (hq : (q * X).comp r = q.comp r * r),
    ((p + q) * X).comp r = (p + q).comp r * r
monomial :
  ∀ (n : ℕ) (b : R),
    (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial n : (a : R) → R[X]) b : R[X]) X).comp r =
      comp ((Polynomial.monomial n : (a : R) → R[X]) b) r * r
⊢ (p * X).comp r = p.comp r * r

Tactic:
induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, add_mul, add_comp]
  | monomial n b => simp only [pow_succ, mul_assoc, monomial_mul_X, monomial_comp]

Premises used: add_mul, pow_succ, mul_assoc, Polynomial.monomial, Polynomial.monomial_mul_X, Polynomial.add_comp, Polynomial.monomial_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (HPow.hPow (α := R[X]) (β := ℕ) X 0).comp p = HPow.hPow (β := ℕ) p 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
ih : (HPow.hPow (α := R[X]) X k).comp p = p ^ k
⊢ (HPow.hPow (α := R[X]) X (k + 1)).comp p = p ^ (k + 1)

Tactic:
simp [pow_succ, mul_X_comp, ih]

Premises used: pow_succ, Polynomial.mul_X_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
zero : (HPow.hPow (α := R[X]) (β := ℕ) X 0).comp p = HPow.hPow (β := ℕ) p 0
succ :
  ∀ (k : ℕ) (ih : (HPow.hPow (α := R[X]) X k).comp p = p ^ k), (HPow.hPow (α := R[X]) X (k + 1)).comp p = p ^ (k + 1)
⊢ (HPow.hPow (α := R[X]) X k).comp p = p ^ k

Tactic:
induction k with
  | zero => simp
  | succ k ih => simp [pow_succ, mul_X_comp, ih]

Premises used: pow_succ, AddMonoidAlgebra.zero, Polynomial.mul_X_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p r : R[X]
⊢ (p * HPow.hPow (α := R[X]) (β := ℕ) X 0).comp r = p.comp r * HPow.hPow (β := ℕ) r 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p r : R[X]
k : ℕ
ih : (p * HPow.hPow (α := R[X]) X k).comp r = p.comp r * r ^ k
⊢ (p * HPow.hPow (α := R[X]) X (k + 1)).comp r = p.comp r * r ^ (k + 1)

Tactic:
simp [ih, pow_succ, ← mul_assoc, mul_X_comp]

Premises used: pow_succ, mul_assoc, Polynomial.mul_X_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p r : R[X]
k : ℕ
zero : (p * HPow.hPow (α := R[X]) (β := ℕ) X 0).comp r = p.comp r * HPow.hPow (β := ℕ) r 0
succ :
  ∀ (k : ℕ) (ih : (p * HPow.hPow (α := R[X]) X k).comp r = p.comp r * r ^ k),
    (p * HPow.hPow (α := R[X]) X (k + 1)).comp r = p.comp r * r ^ (k + 1)
⊢ (p * HPow.hPow (α := R[X]) X k).comp r = p.comp r * r ^ k

Tactic:
induction k with
  | zero => simp
  | succ k ih => simp [ih, pow_succ, ← mul_assoc, mul_X_comp]

Premises used: pow_succ, mul_assoc, AddMonoidAlgebra.zero, Polynomial.mul_X_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
p_1 r p q : R[X]
hp :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).comp r =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p.comp r)
hq :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q).comp r =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q.comp r)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p + q)).comp r =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((p + q).comp r)

Tactic:
simp [hp, hq, mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
p r : R[X]
n : ℕ
b : R
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])).comp r =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (comp ((monomial n : (a : R) → R[X]) b) r)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : Semiring R
p r : R[X]
add :
  ∀ (p q : R[X])
    (hp :
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).comp r =
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p.comp r))
    (hq :
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q).comp r =
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q.comp r)),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p + q)).comp r =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((p + q).comp r)
monomial :
  ∀ (n : ℕ) (b : R),
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X])
            ((Polynomial.monomial n : (a : R) → R[X]) b : R[X])).comp
        r =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (comp ((Polynomial.monomial n : (a : R) → R[X]) b) r)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).comp r =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p.comp r)

Tactic:
induction p using Polynomial.induction_on' with
  | add p q hp hq => simp [hp, hq, mul_add]
  | monomial n b => simp [mul_assoc]

Premises used: mul_assoc, Polynomial.monomial, mul_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p r : R[X]
n : ℕ
rw : ((C : (a : R) → R[X]) (↑n : R) * p).comp r = (C : (a : R) → R[X]) (↑n : R) * p.comp r
rw₁ rw₂ : (C : (a : R) → R[X]) (↑n : R) * p.comp r = (C : (a : R) → R[X]) (↑n : R) * p.comp r
⊢ ((↑n : R[X]) * p).comp r = (↑n : R[X]) * p.comp r

Tactic:
rw [← C_eq_natCast, C_mul_comp]

Premises used: Polynomial.C_eq_natCast, Polynomial.C_mul_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
rw : (p * X + p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₁ : (p * X).comp q + (p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₂ : p.comp q * q + (p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₃ : p.comp q * q + ((↑n : R[X]) * p).comp q = p.comp q * (q + (↑n : R[X]))
rw₄ : p.comp q * q + (↑n : R[X]) * p.comp q = p.comp q * (q + (↑n : R[X]))
rw₅ : p.comp q * q + p.comp q * (↑n : R[X]) = p.comp q * (q + (↑n : R[X]))
rw₆ rw₇ : p.comp q * q + p.comp q * (↑n : R[X]) = p.comp q * q + p.comp q * (↑n : R[X])
⊢ (p * HAdd.hAdd (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))

Tactic:
rw [mul_add, add_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_add]

Premises used: Nat.cast_comm, Polynomial.add_comp, Polynomial.mul_X_comp, mul_add, Polynomial.natCast_mul_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_1
inst : CommSemiring R
p q r : R[X]
⊢ (p * q).comp r = p.comp r * q.comp r

Tactic:
eval₂_mul _ _

Premises used: Polynomial.eval₂_mul, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
⊢ (p * q).comp (-X) = p.comp (-X) * q.comp (-X)

Tactic:
eval₂_mul_noncomm C (-X) fun _ ↦ Commute.symm (commute_X _).neg_left

Premises used: Polynomial.C, Commute.neg_left, Polynomial.coeff, Polynomial.commute_X, Commute.symm, Polynomial.X, Polynomial.comp, DFunLike.coe, Neg.neg, Polynomial.eval₂_mul_noncomm