awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
n : ℕ
⊢ (p ^ n).comp q = p.comp q ^ n

Tactic:
(MonoidHom.mk (OneHom.mk (fun r : R[X] => r.comp q) one_comp) fun r s => mul_comp r s q).map_pow
    p n

Premises used: OneHom.mk, MonoidHom.mk, Polynomial.one_comp, Polynomial.mul_comp, Polynomial.comp, MonoidHom.map_pow
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_1
inst : CommSemiring R
φ ψ χ : R[X]
⊢ (φ.comp ψ).comp χ = φ.comp (ψ.comp χ)

Tactic:
Polynomial.induction_on φ ?_ ?_ ?_

Premises used: Polynomial.induction_on
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_1
inst : CommSemiring R
φ ψ χ : R[X]
refine_1 : ∀ (a : R), (comp ((C : (a : R) → R[X]) a) ψ).comp χ = comp ((C : (a : R) → R[X]) a) (ψ.comp χ)
refine_2 :
  ∀ (p q : R[X]),
    (p.comp ψ).comp χ = p.comp (ψ.comp χ) →
      (q.comp ψ).comp χ = q.comp (ψ.comp χ) → ((p + q).comp ψ).comp χ = (p + q).comp (ψ.comp χ)
refine_3 :
  ∀ (n : ℕ) (a : R),
    ((HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).comp ψ).comp χ =
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).comp (ψ.comp χ) →
      ((HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).comp ψ).comp χ =
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).comp (ψ.comp χ)
⊢ (φ.comp ψ).comp χ = φ.comp (ψ.comp χ)

Tactic:
refine Polynomial.induction_on φ ?_ ?_ ?_
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_1
inst : CommSemiring R
φ ψ χ : R[X]
a : R
⊢ (comp ((C : (a : R) → R[X]) a) ψ).comp χ = comp ((C : (a : R) → R[X]) a) (ψ.comp χ)

Tactic:
simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ, ← mul_assoc]

Premises used: Polynomial.X_comp, pow_succ, mul_assoc, Polynomial.add_comp, Polynomial.C_comp, Polynomial.mul_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_1
inst : CommSemiring R
φ ψ χ p q : R[X]
h : (p.comp ψ).comp χ = p.comp (ψ.comp χ)
h_1 : (q.comp ψ).comp χ = q.comp (ψ.comp χ)
⊢ ((p + q).comp ψ).comp χ = (p + q).comp (ψ.comp χ)

Tactic:
simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ, ← mul_assoc]

Premises used: Polynomial.X_comp, pow_succ, mul_assoc, Polynomial.add_comp, Polynomial.C_comp, Polynomial.mul_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_1
inst : CommSemiring R
φ ψ χ : R[X]
n : ℕ
a : R
h :
  ((HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).comp ψ).comp χ =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).comp (ψ.comp χ)
⊢ ((HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).comp ψ).comp χ =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).comp (ψ.comp χ)

Tactic:
simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ, ← mul_assoc]

Premises used: Polynomial.X_comp, pow_succ, mul_assoc, Polynomial.add_comp, Polynomial.C_comp, Polynomial.mul_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
ι : Type y
inst : Semiring R
s : Finset ι
p : ι → R[X]
q : R[X]
⊢ comp (∑ i ∈ s, p i) q = ∑ i ∈ s, (p i).comp q

Tactic:
Polynomial.eval₂_finsetSum _ _ _ _

Premises used: Polynomial.eval₂_finsetSum, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
a : R
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
⊢ map f ((C : (a : R) → R[X]) a) = (C : (a : S) → S[X]) ((f : (a : R) → S) a)

Tactic:
eval₂_C _ _

Premises used: Polynomial.eval₂_C, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
⊢ map f X = X

Tactic:
eval₂_X _ _

Premises used: Polynomial.eval₂_X, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
n : ℕ
a : R
rw :
  HMul.hMul (α := S[X]) ((RingHom.comp C f : (a : R) → S[X]) a : S[X]) (HPow.hPow (α := S[X]) X n) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X]) (HPow.hPow (α := S[X]) X n)
⊢ eval₂ (RingHom.comp C f) X ((monomial n : (a : R) → R[X]) a) = (monomial n : (a : S) → S[X]) ((f : (a : R) → S) a)

Tactic:
rw [eval₂_monomial, ← C_mul_X_pow_eq_monomial]

Premises used: Polynomial.eval₂_monomial, Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
n : ℕ
a : R
⊢ HMul.hMul (α := S[X]) ((RingHom.comp C f : (a : R) → S[X]) a : S[X]) (HPow.hPow (α := S[X]) X n) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X]) (HPow.hPow (α := S[X]) X n)

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
⊢ map f 0 = 0

Tactic:
eval₂_zero _ _

Premises used: Polynomial.eval₂_zero, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : Semiring S
f : R →+* S
⊢ map f (p + q) = map f p + map f q

Tactic:
eval₂_add _ _

Premises used: Polynomial.map, Polynomial.eval₂_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
⊢ map f 1 = 1

Tactic:
eval₂_one _ _

Premises used: Polynomial.eval₂_one, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : Semiring S
f : R →+* S
hf : ∀ (k : ℕ), Commute.{v} (S := S[X]) ((RingHom.comp C f : (a : R) → S[X]) (q.coeff k) : S[X]) (X : S[X])
⊢ map f (p * q) = map f p * map f q

Tactic:
rw [map, eval₂_mul_noncomm]

Premises used: Polynomial.map, Polynomial.eval₂_mul_noncomm
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : Semiring S
f : R →+* S
⊢ ∀ (k : ℕ), Commute.{v} (S := S[X]) ((RingHom.comp C f : (a : R) → S[X]) (q.coeff k) : S[X]) (X : S[X])

Tactic:
fun k => (commute_X _).symm

Premises used: Polynomial.C, Polynomial.coeff, RingHom.comp, Polynomial.commute_X, Commute.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : Semiring S
f : R →+* S
⊢ ∀ (k : ℕ), Commute.{v} (S := S[X]) ((RingHom.comp C f : (a : R) → S[X]) (q.coeff k) : S[X]) (X : S[X])

Tactic:
exact fun k => (commute_X _).symm

Premises used: Polynomial.commute_X, Commute.symm
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
⊢ (⇑(mapRingHom f) : (a : R[X]) → S[X]) = map f

Tactic:
rfl

Premises used: Polynomial.map, rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
n : ℕ
⊢ map f (↑n : R[X]) = (↑n : S[X])

Tactic:
map_natCast (mapRingHom f) n

Premises used: map_natCast, Polynomial.mapRingHom, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
n : ℕ
inst_2 : n.AtLeastTwo
rw rw₁ : Eq.{v + 1} (α := S[X]) (↑n : S[X]) (↑n : S[X])
⊢ map f (↑n : R[X]) = (↑n : S[X])

Tactic:
rw [Polynomial.map_natCast]

Premises used: Polynomial.map_natCast
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x y : R[X]
⊢ x ∣ y → map f x ∣ map f y

Tactic:
_root_.map_dvd (mapRingHom f)

Premises used: map_dvd, Polynomial.mapRingHom, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x y : R[X]
⊢ Associated x y → Associated (map f x) (map f y)

Tactic:
.map (mapRingHom f)

Premises used: Polynomial.mapRingHom, Polynomial.map, Associated.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
a :
  ∀ (x : R) (n : ℕ),
    Eq.{u_2 + 1} (α := S) (coeff (((mapRingHom f).comp C : (a : R) → S[X]) x) n)
      (coeff ((RingHom.comp C f : (a : R) → S[X]) x) n)
⊢ (mapRingHom f).comp C = RingHom.comp C f

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : R
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) (coeff (((mapRingHom f).comp C : (a : R) → S[X]) x) n)
    (coeff ((RingHom.comp C f : (a : R) → S[X]) x) n)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p_1 : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
p q : R[X]
hp : eval₂ f x p = eval x (map f p)
hq : eval₂ f x q = eval x (map f q)
⊢ eval₂ f x (p + q) = eval x (map f (p + q))

Tactic:
simp [hp, hq]
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
n : ℕ
r : R
⊢ eval₂ f x ((monomial n : (a : R) → R[X]) r) = eval x (map f ((monomial n : (a : R) → R[X]) r))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
add :
  ∀ (p q : R[X]) (hp : eval₂ f x p = eval x (map f p)) (hq : eval₂ f x q = eval x (map f q)),
    eval₂ f x (p + q) = eval x (map f (p + q))
monomial :
  ∀ (n : ℕ) (r : R),
    eval₂ f x ((Polynomial.monomial n : (a : R) → R[X]) r) = eval x (map f ((Polynomial.monomial n : (a : R) → R[X]) r))
⊢ eval₂ f x p = eval x (map f p)

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

Premises used: Polynomial.monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
L : List R[X]
⊢ map f L.prod = (List.map (map f) L).prod

Tactic:
Eq.symm <| List.prod_hom _ (mapRingHom f).toMonoidHom

Premises used: Polynomial.mapRingHom, List.prod_hom, RingHom.toMonoidHom, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
n : ℕ
⊢ map f (p ^ n) = map f p ^ n

Tactic:
(mapRingHom f).map_pow _ _

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

Tactic:
(eval₂_eq_eval_map f).symm

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

Tactic:
eval_map f _ ▸ eval₂_at_apply ..

Premises used: Polynomial.eval_map, Eq.rec, Polynomial.eval₂_at_apply, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
ι : Type u_1
g : ι → R[X]
s : Finset ι
⊢ map f (∑ i ∈ s, g i) = ∑ i ∈ s, map f (g i)

Tactic:
map_sum (mapRingHom f) _ _

Premises used: map_sum, Polynomial.mapRingHom, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p q : R[X]
⊢ ∀ (a : R), map f (comp ((C : (a : R) → R[X]) a) q) = (map f ((C : (a : R) → R[X]) a)).comp (map f q)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p q : R[X]
⊢ ∀ (p q_1 : R[X]),
    map f (p.comp q) = (map f p).comp (map f q) →
      map f (q_1.comp q) = (map f q_1).comp (map f q) → map f ((p + q_1).comp q) = (map f (p + q_1)).comp (map f q)

Tactic:
simp +contextual only [Polynomial.map_add, add_comp, forall_const,
        imp_true_iff]

Premises used: Polynomial.map_add, imp_true_iff, Polynomial.add_comp, forall_const
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p q : R[X]
⊢ ∀ (n : ℕ) (a : R),
    map f ((HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).comp q) =
        (map f (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))).comp (map f q) →
      map f ((HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).comp q) =
        (map f (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))).comp (map f q)

Tactic:
simp +contextual only [pow_succ, ← mul_assoc, comp, forall_const,
        eval₂_mul_X, imp_true_iff, map_X, Polynomial.map_mul]

Premises used: Polynomial.map_mul, Polynomial.eval₂_mul_X, pow_succ, mul_assoc, Polynomial.map_X, imp_true_iff, forall_const, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
x : R
n : ℕ
⊢ eval x (HPow.hPow (α := R[X]) X n) = x ^ n

Tactic:
simp [eval]

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

Tactic:
eval₂_mul _ _

Premises used: Polynomial.eval, Polynomial.eval₂_mul
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
r : R
⊢ Eq (α := (a : R[X]) → R) (⇑(evalRingHom r) : (a : R[X]) → R) (eval r)

Tactic:
rfl

Premises used: Polynomial.eval, rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
x : R
n : ℕ
⊢ eval x (p ^ n) = eval x p ^ n

Tactic:
eval₂_pow _ _ _

Premises used: Polynomial.eval, Polynomial.eval₂_pow
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
x : R
r s : R[X]
hr : eval x (r.comp q) = eval (eval x q) r
hs : eval x (s.comp q) = eval (eval x q) s
⊢ eval x ((r + s).comp q) = eval (eval x q) (r + s)

Tactic:
simp [add_comp, hr, hs]

Premises used: Polynomial.add_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
x : R
n : ℕ
a : R
⊢ eval x (comp ((monomial n : (a : R) → R[X]) a) q) = eval (eval x q) ((monomial n : (a : R) → R[X]) a)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
x : R
add :
  ∀ (r s : R[X]) (hr : eval x (r.comp q) = eval (eval x q) r) (hs : eval x (s.comp q) = eval (eval x q) s),
    eval x ((r + s).comp q) = eval (eval x q) (r + s)
monomial :
  ∀ (n : ℕ) (a : R),
    eval x (comp ((Polynomial.monomial n : (a : R) → R[X]) a) q) =
      eval (eval x q) ((Polynomial.monomial n : (a : R) → R[X]) a)
⊢ eval x (p.comp q) = eval (eval x q) p

Tactic:
induction p using Polynomial.induction_on' with
  | add r s hr hs => simp [add_comp, hr, hs]
  | monomial n a => simp

Premises used: Polynomial.monomial, Polynomial.add_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
q : R[X]
⊢ Eq (α := (a : R[X]) → R[X]) (⇑q.compRingHom : (a : R[X]) → R[X]) fun (p : R[X]) ↦ p.comp q

Tactic:
rfl

Premises used: Polynomial.comp, rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
⊢ (q.compRingHom : (a : R[X]) → R[X]) p = p.comp q

Tactic:
rfl

Premises used: Polynomial.comp, rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
H : q.IsRoot a
rw : eval a (p * q) = 0
rw₁ : eval a p * eval a q = 0
rw₂ : eval a p * 0 = 0
rw₃ rw₄ : Eq.{u + 1} (α := R) 0 0
⊢ (p * q).IsRoot a

Tactic:
rw [IsRoot, eval_mul, IsRoot.def.1 H, mul_zero]

Premises used: Polynomial.IsRoot, Polynomial.IsRoot.def, Polynomial.eval_mul, MulZeroClass.mul_zero, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
H : p.IsRoot a
rw : eval a (p * q) = 0
rw₁ : eval a p * eval a q = 0
rw₂ : 0 * eval a q = 0
rw₃ rw₄ : Eq.{u + 1} (α := R) 0 0
⊢ (p * q).IsRoot a

Tactic:
rw [IsRoot, eval_mul, IsRoot.def.1 H, zero_mul]

Premises used: Polynomial.IsRoot, MulZeroClass.zero_mul, Polynomial.IsRoot.def, Polynomial.eval_mul, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
s : Multiset R[X]
x : S
⊢ eval₂ f x s.prod = (Multiset.map (eval₂ f x) s).prod

Tactic:
map_multiset_prod (eval₂RingHom f x) s

Premises used: map_multiset_prod, Polynomial.eval₂RingHom
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
ι : Type y
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
s : Finset ι
g : ι → R[X]
x : S
⊢ eval₂ f x (∏ i ∈ s, g i) = ∏ i ∈ s, eval₂ f x (g i)

Tactic:
map_prod (eval₂RingHom f x) _ _

Premises used: map_prod, Polynomial.eval₂RingHom
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
l : List R[X]
x : R
⊢ eval x l.prod = (List.map (eval x) l).prod

Tactic:
map_list_prod (evalRingHom x) l

Premises used: Polynomial.eval, map_list_prod, Polynomial.evalRingHom
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
s : Multiset R[X]
x : R
⊢ eval x s.prod = (Multiset.map (eval x) s).prod

Tactic:
(evalRingHom x).map_multiset_prod s

Premises used: Polynomial.eval, Polynomial.evalRingHom, MonoidHom.map_multiset_prod, RingHom.toMonoidHom
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_1
s : Finset ι
p : ι → R[X]
x : R
⊢ eval x (∏ j ∈ s, p j) = ∏ j ∈ s, eval x (p j)

Tactic:
map_prod (evalRingHom x) _ _

Premises used: Polynomial.eval, map_prod, Polynomial.evalRingHom
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
l : List R[X]
q : R[X]
⊢ l.prod.comp q = List.prod (List.map (fun (p : R[X]) ↦ p.comp q) l)

Tactic:
map_list_prod (compRingHom q) _

Premises used: map_list_prod, Polynomial.comp, Polynomial.compRingHom
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
s : Multiset R[X]
q : R[X]
⊢ s.prod.comp q = Multiset.prod (Multiset.map (fun (p : R[X]) ↦ p.comp q) s)

Tactic:
map_multiset_prod (compRingHom q) _

Premises used: map_multiset_prod, Polynomial.comp, Polynomial.compRingHom
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_1
s : Finset ι
p : ι → R[X]
q : R[X]
⊢ comp (∏ j ∈ s, p j) q = ∏ j ∈ s, (p j).comp q

Tactic:
map_prod (compRingHom q) _ _

Premises used: map_prod, Polynomial.comp, Polynomial.compRingHom
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
ι : Type u_1
s : Finset ι
p : ι → R[X]
x : R
⊢ IsRoot (∏ j ∈ s, p j) x ↔ ∃ i ∈ s, (p i).IsRoot x

Tactic:
simp only [IsRoot, eval_prod, Finset.prod_eq_zero_iff]

Premises used: Polynomial.eval_prod, Polynomial.IsRoot, Finset.prod_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
x : R
⊢ p ∣ q → eval x p ∣ eval x q

Tactic:
eval₂_dvd _ _

Premises used: Polynomial.eval, Polynomial.eval₂_dvd
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
x : R
⊢ p ∣ q → eval x p = 0 → eval x q = 0

Tactic:
eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _

Premises used: Polynomial.eval, Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
x : R
⊢ eval x (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) = ∑ i ∈ range n, x ^ i

Tactic:
simp [eval_finsetSum]

Premises used: Polynomial.eval_finsetSum
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
inst_1 : NoZeroDivisors R
simp_rw : eval a (p * q) = 0 ↔ eval a p = 0 ∨ eval a q = 0
simp_rw₁ : eval a p * eval a q = 0 ↔ eval a p = 0 ∨ eval a q = 0
⊢ (p * q).IsRoot a ↔ p.IsRoot a ∨ q.IsRoot a

Tactic:
simp_rw [IsRoot, eval_mul, mul_eq_zero]

Premises used: Polynomial.IsRoot, Polynomial.eval_mul, mul_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
inst_1 : NoZeroDivisors R
h : (p * q).IsRoot a
⊢ p.IsRoot a ∨ q.IsRoot a

Tactic:
root_mul.1 h

Premises used: Polynomial.root_mul, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
m : Multiset R[X]
⊢ map f m.prod = (Multiset.map (map f) m).prod

Tactic:
Eq.symm <| Multiset.prod_hom _ (mapRingHom f).toMonoidHom

Premises used: Polynomial.mapRingHom, Multiset.prod_hom, RingHom.toMonoidHom, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
ι : Type u_1
g : ι → R[X]
s : Finset ι
⊢ map f (∏ i ∈ s, g i) = ∏ i ∈ s, map f (g i)

Tactic:
map_prod (mapRingHom f) _ _

Premises used: map_prod, Polynomial.mapRingHom, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p q : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
⊢ map f (p - q) = map f p - map f q

Tactic:
(mapRingHom f).map_sub p q

Premises used: RingHom.map_sub, Polynomial.mapRingHom, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
⊢ map f (-p) = -map f p

Tactic:
(mapRingHom f).map_neg p

Premises used: RingHom.map_neg, Polynomial.mapRingHom, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
S : Type u_1
inst_1 : Ring S
f : R →+* S
n : ℤ
⊢ map f (↑n : R[X]) = (↑n : S[X])

Tactic:
map_intCast (mapRingHom f) n

Premises used: map_intCast, Polynomial.mapRingHom, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
n : ℤ
x : R
⊢ eval x (↑n : R[X]) = (↑n : R)

Tactic:
simp only [← C_eq_intCast, eval_C]

Premises used: Polynomial.eval_C, Polynomial.C_eq_intCast
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
x : S
rw : eval₂ f x (-p) + eval₂ f x p = 0
rw₁ : eval₂ f x (-p + p) = 0
rw₂ : eval₂ f x 0 = 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := S) 0 0
⊢ eval₂ f x (-p) = -eval₂ f x p

Tactic:
rw [eq_neg_iff_add_eq_zero, ← eval₂_add, neg_add_cancel, eval₂_zero]

Premises used: Polynomial.eval₂_zero, neg_add_cancel, eq_neg_iff_add_eq_zero, Polynomial.eval₂_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p q : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
x : S
rw : eval₂ f x (p + -q) = eval₂ f x p - eval₂ f x q
rw₁ : eval₂ f x p + eval₂ f x (-q) = eval₂ f x p - eval₂ f x q
rw₂ : eval₂ f x p + -eval₂ f x q = eval₂ f x p - eval₂ f x q
rw₃ rw₄ : eval₂ f x p + -eval₂ f x q = eval₂ f x p + -eval₂ f x q
⊢ eval₂ f x (p - q) = eval₂ f x p - eval₂ f x q

Tactic:
rw [sub_eq_add_neg, eval₂_add, eval₂_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, Polynomial.eval₂_neg, Polynomial.eval₂_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p : R[X]
x : R
⊢ eval x (-p) = -eval x p

Tactic:
eval₂_neg _

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

Tactic:
eval₂_sub _

Premises used: Polynomial.eval, Polynomial.eval₂_sub
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
a b : R
inst : Ring R
rw : eval b (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ a = b
rw₁ : eval b X - eval b ((C : (a : R) → R[X]) a) = 0 ↔ a = b
rw₂ : b - eval b ((C : (a : R) → R[X]) a) = 0 ↔ a = b
rw₃ : b - a = 0 ↔ a = b
rw₄ : b = a ↔ a = b
rw₅ rw₆ : a = b ↔ a = b
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).IsRoot b ↔ a = b

Tactic:
rw [IsRoot.def, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm]

Premises used: Polynomial.eval_C, sub_eq_zero, Polynomial.eval_X, Polynomial.IsRoot.def, eq_comm, Polynomial.eval_sub