awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
n : ℕ
rw : eval₂ f x ((monomial n : (a : R) → R[X]) 1) = x ^ n
⊢ eval₂ f x (HPow.hPow (α := R[X]) X n) = x ^ n

Tactic:
rw [X_pow_eq_monomial]

Premises used: Polynomial.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
x : S
n : ℕ
⊢ eval₂ f x ((monomial n : (a : R) → R[X]) 1) = HMul.hMul (α := S) ((f : (a : R) → S) 1 : S) (x ^ n)

Tactic:
eval₂_monomial f x (n := n) (r := 1)

Premises used: Polynomial.eval₂_monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
n : ℕ
h : x ^ n = HMul.hMul (α := S) ((f : (a : R) → S) 1 : S) (x ^ n)
⊢ eval₂ f x ((monomial n : (a : R) → R[X]) 1) = x ^ n

Tactic:
convert! eval₂_monomial f x (n := n) (r := 1)

Premises used: Polynomial.eval₂_monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ x ^ n = HMul.hMul (α := S) ((f : (a : R) → S) 1 : S) (x ^ n)

Tactic:
simp
-- 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
x : S
simp :
  ((p + q).sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e)) =
    HAdd.hAdd (α := S) (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e))
      (q.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e))
⊢ eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q

Tactic:
simp only [eval₂_eq_sum]

Premises used: Polynomial.eval₂_eq_sum
-- 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
x : S
hf : ∀ (i : ℕ), HMul.hMul (α := S) ((f : (a : R) → S) 0 : S) (x ^ i) = 0
h_add :
  ∀ (a : ℕ) (b₁ b₂ : R),
    HMul.hMul (α := S) ((f : (a : R) → S) (b₁ + b₂) : S) (x ^ a) =
      HMul.hMul (α := S) ((f : (a : R) → S) b₁ : S) (x ^ a) + HMul.hMul (α := S) ((f : (a : R) → S) b₂ : S) (x ^ a)
⊢ ((p + q).sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e)) =
    HAdd.hAdd (α := S) (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e))
      (q.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e))

Tactic:
apply sum_add_index

Premises used: Polynomial.sum_add_index
-- 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
x : S
⊢ ∀ (i : ℕ), HMul.hMul (α := S) ((f : (a : R) → S) 0 : S) (x ^ i) = 0

Tactic:
simp [add_mul]

Premises used: add_mul
-- 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
x : S
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    HMul.hMul (α := S) ((f : (a : R) → S) (b₁ + b₂) : S) (x ^ a) =
      HMul.hMul (α := S) ((f : (a : R) → S) b₁ : S) (x ^ a) + HMul.hMul (α := S) ((f : (a : R) → S) b₂ : S) (x ^ a)

Tactic:
simp [add_mul]

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

Tactic:
rw [← C_1, eval₂_C, f.map_one]

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

Tactic:
simp only [eval₂_zero, Nat.cast_zero]

Premises used: Polynomial.eval₂_zero, Nat.cast_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
n : ℕ
ih : eval₂ f x (↑n : R[X]) = (↑n : S)
succ : eval₂ f x (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) = (↑(n + 1) : S)
succ₁ : eval₂ f x (↑n : R[X]) + eval₂ f x 1 = (↑(n + 1) : S)
succ₂ : (↑n : S) + eval₂ f x 1 = (↑(n + 1) : S)
succ₃ : HAdd.hAdd (α := S) (↑n : S) 1 = (↑(n + 1) : S)
succ₄ succ₅ : HAdd.hAdd (α := S) (↑n : S) 1 = HAdd.hAdd (α := S) (↑n : S) 1
⊢ eval₂ f x (↑(n + 1) : R[X]) = (↑(n + 1) : S)

Tactic:
rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]

Premises used: Nat.cast_succ, Polynomial.eval₂_one, 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
x : S
n : ℕ
zero : eval₂ f x (↑0 : R[X]) = (↑0 : S)
succ : ∀ (n : ℕ) (ih : eval₂ f x (↑n : R[X]) = (↑n : S)), eval₂ f x (↑(n + 1) : R[X]) = (↑(n + 1) : S)
⊢ eval₂ f x (↑n : R[X]) = (↑n : S)

Tactic:
induction n with
  | zero => simp only [eval₂_zero, Nat.cast_zero]
  | succ n ih => rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]

Premises used: Nat.cast_succ, Polynomial.eval₂_one, Polynomial.eval₂_zero, AddMonoidAlgebra.zero, Nat.cast_zero, Polynomial.eval₂_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
n : ℕ
inst_2 : n.AtLeastTwo
f : R →+* S
a : S
⊢ eval₂ f a (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
simp [OfNat.ofNat]

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
T_1 : Type w
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
inst_2 : Semiring T_1
p : T_1[X]
g : ℕ → T_1 → R[X]
x : S
T : AddMonoidHom.{u, v} R[X] S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
⊢ ∀ (y : R[X]), eval₂ f x y = (T : (a : R[X]) → S) y

Tactic:
have A : ∀ y, eval₂ f x y = T y := fun y => rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
T_1 : Type w
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
inst_2 : Semiring T_1
p : T_1[X]
g : ℕ → T_1 → R[X]
x : S
T : AddMonoidHom.{u, v} R[X] S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
A : ∀ (y : R[X]), eval₂ f x y = (T : (a : R[X]) → S) y
simp :
  Eq.{v + 1} (α := S) ((T : (a : R[X]) → S) (p.sum g) : S)
    (p.sum fun (n : ℕ) (a : T_1) ↦ (T : (a : R[X]) → S) (g n a) : S)
⊢ eval₂ f x (p.sum g) = p.sum fun (n : ℕ) (a : T_1) ↦ eval₂ f x (g n a)

Tactic:
simp only [A]
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
T_1 : Type w
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
inst_2 : Semiring T_1
p : T_1[X]
g : ℕ → T_1 → R[X]
x : S
T : AddMonoidHom.{u, v} R[X] S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
A : ∀ (y : R[X]), eval₂ f x y = (T : (a : R[X]) → S) y
rw :
  Eq.{v + 1} (α := S) ((T : (a : R[X]) → S) (∑ n ∈ p.support, g n (p.coeff n)) : S)
    (p.sum fun (n : ℕ) (a : T_1) ↦ (T : (a : R[X]) → S) (g n a) : S)
rw₁ :
  Eq.{v + 1} (α := S) (∑ x ∈ p.support, (T : (a : R[X]) → S) (g x (p.coeff x)))
    (p.sum fun (n : ℕ) (a : T_1) ↦ (T : (a : R[X]) → S) (g n a))
rw₂ rw₃ :
  Eq.{v + 1} (α := S) (∑ x ∈ p.support, (T : (a : R[X]) → S) (g x (p.coeff x)))
    (∑ n ∈ p.support, (T : (a : R[X]) → S) (g n (p.coeff n)))
⊢ Eq.{v + 1} (α := S) ((T : (a : R[X]) → S) (p.sum g) : S)
    (p.sum fun (n : ℕ) (a : T_1) ↦ (T : (a : R[X]) → S) (g n a) : S)

Tactic:
rw [sum, map_sum, sum]

Premises used: Polynomial.sum, map_sum
-- 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]
x : S
⊢ eval₂ f x l.sum = (List.map (eval₂ f x) l).sum

Tactic:
map_list_sum (eval₂AddMonoidHom f x) l

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

Tactic:
map_multiset_sum (eval₂AddMonoidHom f x) s

Premises used: map_multiset_sum, Polynomial.eval₂AddMonoidHom
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
ι : Type y
inst : Semiring R
inst_1 : Semiring 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_sum (eval₂AddMonoidHom f x) _ _

Premises used: map_sum, Polynomial.eval₂AddMonoidHom
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
p : R[ℕ]
simp :
  Eq.{v + 1} (α := S)
    (∑ x_1 ∈ p.support, HMul.hMul (α := S) ((f : (a : R) → S) ((p : (a : ℕ) → R) x_1 : R) : S) (x ^ x_1) : S)
    ((liftNC (↑f : R →+ S)
            (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) :
              (a : Multiplicative ℕ) → S) :
          (a : R[ℕ]) → S)
        p :
      S)
⊢ eval₂ f x { toFinsupp := p : R[X] } =
    (liftNC (↑f : R →+ S)
          (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) : (a : Multiplicative ℕ) → S) :
        (a : R[ℕ]) → S)
      p

Tactic:
simp only [eval₂_eq_sum, sum, support, coeff]

Premises used: Polynomial.sum, Polynomial.coeff, Polynomial.eval₂_eq_sum, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
p : R[ℕ]
⊢ Eq.{v + 1} (α := S)
    (∑ x_1 ∈ p.support, HMul.hMul (α := S) ((f : (a : R) → S) ((p : (a : ℕ) → R) x_1 : R) : S) (x ^ x_1) : S)
    ((liftNC (↑f : R →+ S)
            (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) :
              (a : Multiplicative ℕ) → S) :
          (a : R[ℕ]) → S)
        p :
      S)

Tactic:
rfl
-- 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
x : S
hf : ∀ (k : ℕ), Commute ((f : (a : R) → S) (q.coeff k)) x
rcases : ∀ (p : R[ℕ]), eval₂ f x ({ toFinsupp := p : R[X] } * q) = eval₂ f x { toFinsupp := p : R[X] } * eval₂ f x q
⊢ eval₂ f x (p * q) = eval₂ f x p * eval₂ f x q

Tactic:
rcases p with ⟨p⟩
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
q : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
hf : ∀ (k : ℕ), Commute ((f : (a : R) → S) (q.coeff k)) x
p : R[ℕ]
rcases :
  ∀ (q : R[ℕ]) (hf : ∀ (k : ℕ), Commute ((f : (a : R) → S) ({ toFinsupp := q : R[X] }.coeff k)) x),
    eval₂ f x ({ toFinsupp := p : R[X] } * { toFinsupp := q : R[X] }) =
      eval₂ f x { toFinsupp := p : R[X] } * eval₂ f x { toFinsupp := q : R[X] }
⊢ eval₂ f x ({ toFinsupp := p : R[X] } * q) = eval₂ f x { toFinsupp := p : R[X] } * eval₂ f x q

Tactic:
rcases q with ⟨q⟩
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
p q : R[ℕ]
hf : ∀ (k : ℕ), Commute ((f : (a : R) → S) ((q : (a : ℕ) → R) k : R)) x
simp :
  (liftNC (↑f : R →+ S)
          (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) : (a : Multiplicative ℕ) → S) :
        (a : R[ℕ]) → S)
      (p * q) =
    HMul.hMul (α := S) (β := S)
      ((liftNC (↑f : R →+ S)
              (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) :
                (a : Multiplicative ℕ) → S) :
            (a : R[ℕ]) → S)
          p :
        S)
      ((liftNC (↑f : R →+ S)
              (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) :
                (a : Multiplicative ℕ) → S) :
            (a : R[ℕ]) → S)
          q :
        S)
⊢ eval₂ f x ({ toFinsupp := p : R[X] } * { toFinsupp := q : R[X] }) =
    eval₂ f x { toFinsupp := p : R[X] } * eval₂ f x { toFinsupp := q : R[X] }

Tactic:
simp only [← ofFinsupp_mul, eval₂_ofFinsupp]

Premises used: Polynomial.eval₂_ofFinsupp, Polynomial.ofFinsupp_mul
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
p q : R[ℕ]
hf : ∀ (k : ℕ), Commute ((f : (a : R) → S) ((q : (a : ℕ) → R) k : R)) x
⊢ (liftNC (↑f : R →+ S)
          (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) : (a : Multiplicative ℕ) → S) :
        (a : R[ℕ]) → S)
      (p * q) =
    HMul.hMul (α := S) (β := S)
      ((liftNC (↑f : R →+ S)
              (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) :
                (a : Multiplicative ℕ) → S) :
            (a : R[ℕ]) → S)
          p :
        S)
      ((liftNC (↑f : R →+ S)
              (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) :
                (a : Multiplicative ℕ) → S) :
            (a : R[ℕ]) → S)
          q :
        S)

Tactic:
liftNC_mul _ _ p q fun {k n} _hn => (hf k).pow_right n

Premises used: AddMonoidAlgebra.liftNC_mul, Commute.pow_right
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
p q : R[ℕ]
hf : ∀ (k : ℕ), Commute ((f : (a : R) → S) ((q : (a : ℕ) → R) k : R)) x
⊢ (liftNC (↑f : R →+ S)
          (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) : (a : Multiplicative ℕ) → S) :
        (a : R[ℕ]) → S)
      (p * q) =
    HMul.hMul (α := S) (β := S)
      ((liftNC (↑f : R →+ S)
              (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) :
                (a : Multiplicative ℕ) → S) :
            (a : R[ℕ]) → S)
          p :
        S)
      ((liftNC (↑f : R →+ S)
              (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) :
                (a : Multiplicative ℕ) → S) :
            (a : R[ℕ]) → S)
          q :
        S)

Tactic:
exact liftNC_mul _ _ p q fun {k n} _hn => (hf k).pow_right n

Premises used: AddMonoidAlgebra.liftNC_mul
-- 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
rw rw₁ : eval₂ f x p * x = eval₂ f x p * x
⊢ eval₂ f x p * eval₂ f x X = eval₂ f x p * x

Tactic:
rw [eval₂_X]

Premises used: Polynomial.eval₂_X
-- 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
refine : ∀ (k : ℕ), Commute ((f : (a : R) → S) (coeff X k)) x
⊢ eval₂ f x (p * X) = eval₂ f x p * x

Tactic:
refine _root_.trans (eval₂_mul_noncomm _ _ fun k => ?_) (by rw [eval₂_X])

Premises used: trans, Polynomial.eval₂_mul_noncomm
-- 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
k : ℕ
inl : Commute ((f : (a : R) → S) (coeff X 1)) x
inr : ∀ (hk : ¬k = 1), Commute ((f : (a : R) → S) (coeff X k)) x
⊢ Commute ((f : (a : R) → S) (coeff X k)) x

Tactic:
rcases em (k = 1) with (rfl | hk)

Premises used: em, OfNat.ofNat, Eq, rfl
-- 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
⊢ Commute ((f : (a : R) → S) (coeff X 1)) x

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
k : ℕ
hk : ¬k = 1
⊢ Commute ((f : (a : R) → S) (coeff X k)) x

Tactic:
simp [coeff_X_of_ne_one hk]

Premises used: Polynomial.coeff_X_of_ne_one
-- 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
rw : eval₂ f x (p * X) = eval₂ f x p * x
rw₁ rw₂ : eval₂ f x p * x = eval₂ f x p * x
⊢ eval₂ f x (X * p) = eval₂ f x p * x

Tactic:
rw [X_mul, eval₂_mul_X]

Premises used: Polynomial.eval₂_mul_X, Polynomial.X_mul
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
a : R
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
h : Commute ((f : (a : R) → S) a) x
hf : ∀ (k : ℕ), Commute ((f : (a : R) → S) (coeff ((C : (a : R) → R[X]) a) k)) x
⊢ eval₂ f x (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (β := S) (eval₂ f x p) ((f : (a : R) → S) a : S)

Tactic:
rw [eval₂_mul_noncomm, eval₂_C]

Premises used: Polynomial.eval₂_C, Polynomial.eval₂_mul_noncomm
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
a : R
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
h : Commute ((f : (a : R) → S) a) x
k : ℕ
pos : ∀ (hk : k = 0), Commute ((f : (a : R) → S) (coeff ((C : (a : R) → R[X]) a) k)) x
neg : ∀ (hk : ¬k = 0), Commute ((f : (a : R) → S) (coeff ((C : (a : R) → R[X]) a) k)) x
⊢ Commute ((f : (a : R) → S) (coeff ((C : (a : R) → R[X]) a) k)) x

Tactic:
by_cases hk : k = 0
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
a : R
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
h : Commute ((f : (a : R) → S) a) x
k : ℕ
hk : k = 0
⊢ Commute ((f : (a : R) → S) (coeff ((C : (a : R) → R[X]) a) k)) x

Tactic:
simp only [hk, h, coeff_C_zero]

Premises used: Polynomial.coeff_C_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
a : R
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
h : Commute ((f : (a : R) → S) a) x
k : ℕ
hk : ¬k = 0
⊢ Commute ((f : (a : R) → S) (coeff ((C : (a : R) → R[X]) a) k)) x

Tactic:
simp only [coeff_C_of_ne_zero hk, map_zero, Commute.zero_left]

Premises used: Commute.zero_left, map_zero, Polynomial.coeff_C_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
hf : ∀ (p : R[X]), Membership.mem (γ := List R[X]) [] p → ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x
⊢ eval₂ f x (List.prod []) = (List.map (eval₂ f x) []).prod

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
x : S
ps : List R[X]
p : R[X]
ihp :
  ∀ (hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x),
    eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
hf : ∀ p_1 ∈ ps ++ [p], ∀ (k : ℕ), Commute ((f : (a : R) → S) (p_1.coeff k)) x
⊢ (∀ x_1 ∈ ps, ∀ (k : ℕ), Commute ((f : (a : R) → S) (x_1.coeff k)) x) ∧
    ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x

Tactic:
simp only [List.forall_mem_append, List.forall_mem_singleton] at hf

Premises used: List.forall_mem_singleton, List.forall_mem_append
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
ps : List R[X]
p : R[X]
ihp :
  ∀ (hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x),
    eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
hf :
  (∀ x_1 ∈ ps, ∀ (k : ℕ), Commute ((f : (a : R) → S) (x_1.coeff k)) x) ∧
    ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x
⊢ eval₂ f x (ps ++ [p]).prod = (List.map (eval₂ f x) (ps ++ [p])).prod

Tactic:
simp [eval₂_mul_noncomm _ _ hf.2, ihp hf.1]

Premises used: And.right, And.left, Polynomial.eval₂_mul_noncomm
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
ps : List R[X]
hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x
nil :
  ∀ (hf : ∀ (p : R[X]), Membership.mem (γ := List R[X]) [] p → ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x),
    eval₂ f x (List.prod []) = (List.map (eval₂ f x) []).prod
append_singleton :
  ∀ (ps : List R[X]) (p : R[X])
    (ihp :
      ∀ (hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x),
        eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod)
    (hf : ∀ p_1 ∈ ps ++ [p], ∀ (k : ℕ), Commute ((f : (a : R) → S) (p_1.coeff k)) x),
    eval₂ f x (ps ++ [p]).prod = (List.map (eval₂ f x) (ps ++ [p])).prod
⊢ eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod

Tactic:
induction ps using List.reverseRecOn with
  | nil => simp
  | append_singleton ps p ihp =>
    simp only [List.forall_mem_append, List.forall_mem_singleton] at hf
    simp [eval₂_mul_noncomm _ _ hf.2, ihp hf.1]

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

Tactic:
eval₂_mul_noncomm _ _ fun _k => Commute.all _ _

Premises used: Polynomial.coeff, Commute.all, DFunLike.coe, Polynomial.eval₂_mul_noncomm
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : CommSemiring S
f : R →+* S
x : S
q : R[X]
hp : eval₂ f x p = 0
rw : eval₂ f x p * eval₂ f x q = 0
⊢ eval₂ f x (p * q) = 0

Tactic:
rw [eval₂_mul f x]

Premises used: Polynomial.eval₂_mul
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : CommSemiring S
f : R →+* S
x : S
q : R[X]
hp : eval₂ f x p = 0
⊢ eval₂ f x p * eval₂ f x q = 0

Tactic:
mul_eq_zero_of_left hp (q.eval₂ f x)

Premises used: mul_eq_zero_of_left, Polynomial.eval₂
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : CommSemiring S
f : R →+* S
x : S
q : R[X]
hp : eval₂ f x p = 0
⊢ eval₂ f x p * eval₂ f x q = 0

Tactic:
exact mul_eq_zero_of_left hp (q.eval₂ f x)

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

Tactic:
rw [eval₂_mul f x]

Premises used: Polynomial.eval₂_mul
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
q : R[X]
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hq : eval₂ f x q = 0
⊢ eval₂ f x p * eval₂ f x q = 0

Tactic:
mul_eq_zero_of_right (p.eval₂ f x) hq

Premises used: mul_eq_zero_of_right, Polynomial.eval₂
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
q : R[X]
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hq : eval₂ f x q = 0
⊢ eval₂ f x p * eval₂ f x q = 0

Tactic:
exact mul_eq_zero_of_right (p.eval₂ f x) hq

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : CommSemiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x (p ^ n) = eval₂ f x p ^ n

Tactic:
(eval₂RingHom _ _).map_pow _ _

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

Tactic:
map_dvd (eval₂RingHom f x)

Premises used: map_dvd, Polynomial.eval₂RingHom
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : CommSemiring S
f : R →+* S
x : S
h : p ∣ q
h0 : eval₂ f x p = 0
⊢ eval₂ f x q = 0

Tactic:
zero_dvd_iff.mp (h0 ▸ eval₂_dvd f x h)

Premises used: Polynomial.eval₂_dvd, zero_dvd_iff, Eq.rec, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommSemiring S
f : R →+* S
l : List R[X]
x : S
⊢ eval₂ f x l.prod = (List.map (eval₂ f x) l).prod

Tactic:
map_list_prod (eval₂RingHom f x) l

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

Tactic:
rfl

Premises used: Polynomial.eval, rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
rw :
  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)
⊢ eval x p = p.sum fun (e : ℕ) (a : R) ↦ a * x ^ e

Tactic:
rw [eval, eval₂_eq_sum]

Premises used: Polynomial.eval, Polynomial.eval₂_eq_sum