no goals
A : Type ?u.58502
B : Type ?u.58505
G : Type ?u.58508
H : Type ?u.58511
M : Type u_1
N : Type u_3
P : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : M →* N × P
x : M
⊢ ↑(MonoidHom.prod (comp (fst N P) f) (comp (snd N P) f)) x = ↑f x
simp only [prod_apply, coe_fst, coe_snd, comp_apply, Prod.mk.eta]