no goals
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f✝ f : R →+* S
r : R
⊢ ↑(mapRingHom f) (↑C r) = ↑C (↑f r)
simp only [coe_mapRingHom, map_C, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true,
  and_self_iff]