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]
inst✝² : Semiring S✝
f✝ : R✝ →+* S✝
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
p : R[X]
i : ℤ
⊢ eval (↑i) (map f p) = ↑f (eval (↑i) p)
induction p using Polynomial.induction_on' with
| h_add p q hp hq =>
  simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
| h_monomial n r =>
  simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]
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]
inst✝² : Semiring S✝
f✝ : R✝ →+* S✝
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
i : ℤ
p q : R[X]
hp : eval (↑i) (map f p) = ↑f (eval (↑i) p)
hq : eval (↑i) (map f q) = ↑f (eval (↑i) q)
⊢ eval (↑i) (map f (p + q)) = ↑f (eval (↑i) (p + q))
simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
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]
inst✝² : Semiring S✝
f✝ : R✝ →+* S✝
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
i : ℤ
n : ℕ
r : R
⊢ eval (↑i) (map f (↑(monomial n) r)) = ↑f (eval (↑i) (↑(monomial n) r))
simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]