no goals
α : Type ?u.36124
β : Type ?u.36127
R : Type u_1
R' : Type ?u.36133
S : Type u_3
S' : Type ?u.36139
T : Type u_2
T' : Type ?u.36145
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
f✝ : R →+* S
g : R →+* T
f : R →+* S × T
x : R
⊢ ↑(RingHom.prod (comp (fst S T) f) (comp (snd S T) f)) x = ↑f x
simp only [prod_apply, coe_fst, coe_snd, comp_apply, Prod.mk.eta]