no goals
α : Type ?u.22238
β : Type ?u.22241
R : Type u_1
R' : Type ?u.22247
S : Type u_3
S' : Type ?u.22253
T : Type u_2
T' : Type ?u.22259
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
f✝ : R →ₙ+* S
g : R →ₙ+* T
f : R →ₙ+* S × T
x : R
⊢ ↑(NonUnitalRingHom.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]