no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : CommSemiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
⊢ eval x (comp p q) = eval (eval x q) p
induction p using Polynomial.induction_on' with
| h_add r s hr hs =>
  simp [add_comp, hr, hs]
| h_monomial n a =>
  simp
no goals
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : CommSemiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
r s : R[X]
hr : eval x (comp r q) = eval (eval x q) r
hs : eval x (comp s q) = eval (eval x q) s
⊢ eval x (comp (r + s) q) = eval (eval x q) (r + s)
simp [add_comp, hr, hs]
no goals
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a✝ b : R
m n✝ : ℕ
inst✝¹ : CommSemiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
n : ℕ
a : R
⊢ eval x (comp (↑(monomial n) a) q) = eval (eval x q) (↑(monomial n) a)
simp