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
hf : Function.Injective ↑f
p q : R[X]
h : map f p = map f q
m : ℕ
⊢ ↑f (coeff p m) = ↑f (coeff q m)
rw [← coeff_map f, ← coeff_map f, h]