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