no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
⊢ eval x (p * X) = eval x p * x
induction p using Polynomial.induction_on' with
| h_add p q ph qh =>
  simp only [add_mul, eval_add, ph, qh]
| h_monomial n a =>
  simp only [← monomial_one_one_eq_X, monomial_mul_monomial, eval_monomial, mul_one, pow_succ',
    mul_assoc]
no goals
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
x : R
p q : R[X]
ph : eval x (p * X) = eval x p * x
qh : eval x (q * X) = eval x q * x
⊢ eval x ((p + q) * X) = eval x (p + q) * x
simp only [add_mul, eval_add, ph, qh]
no goals
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
n : ℕ
a : R
⊢ eval x (↑(monomial n) a * X) = eval x (↑(monomial n) a) * x
simp only [← monomial_one_one_eq_X, monomial_mul_monomial, eval_monomial, mul_one, pow_succ',
  mul_assoc]