no goals
F : Type ?u.82658
α : Type ?u.82661
β : Type ?u.82664
R✝ : Type ?u.82667
S✝ : Type ?u.82670
S' : Type ?u.82673
inst✝⁴ : NonUnitalNonAssocSemiring R✝
inst✝³ : NonUnitalNonAssocSemiring S✝
inst✝² : NonUnitalNonAssocSemiring S'
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ ↑f = ↑g
rw [h]