no goals
F : Type ?u.91573
α : Type ?u.91576
β : Type ?u.91579
R✝ : Type ?u.91582
S✝ : Type ?u.91585
S' : Type ?u.91588
inst✝⁴ : NonAssocSemiring R✝
inst✝³ : NonAssocSemiring S✝
inst✝² : NonAssocSemiring S'
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ ↑f = ↑g
rw [h]