no goals
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f✝ f : R →+* S
n : ℕ
⊢ ↑(mapRingHom f) (X ^ n) = X ^ n
simp only [coe_mapRingHom, map_pow, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true,
  map_X, and_self_iff]