∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) (x y : M × N),
  ((↑f).noncommCoprod (↑g) comm).toFun (x * y) =
    ((↑f).noncommCoprod (↑g) comm).toFun x * ((↑f).noncommCoprod (↑g) comm).toFun y