no goals
A : Type ?u.38398
B : Type ?u.38401
G : Type ?u.38404
H : Type ?u.38407
M : Type u_1
N : Type u_3
P : Type u_2
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
f : M →ₙ* N × P
x : M
⊢ ↑(MulHom.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]