∀ {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul M']
  [inst_3 : Mul N'] (f : M →ₙ* M') (g : N →ₙ* N'),
  f.prodMap g = (f.comp (MulHom.fst M N)).prod (g.comp (MulHom.snd M N))