no goals
α : Type ?u.58916
β : Type ?u.58919
R : Type u_2
S : Type ?u.58925
F : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : RingHomClass F ℕ R
f g : F
⊢ ↑f 1 = ↑g 1
simp only [map_one f, map_one g]