no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : Function.Injective ↑f
⊢ support (map f p) = support p
simp_rw [Finset.ext_iff, mem_support_iff, coeff_map, ← map_zero f, hf.ne_iff,
  forall_const]