∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {M' : Type u_3} {N' : Type u_4}
  [inst_2 : MulOneClass N'] [inst_3 : MulOneClass M'] (f : M ≃* M') (g : N ≃* N') (x x_1 : M × N),
  (f.prodCongr g.toEquiv).toFun (x * x_1) = (f.prodCongr g.toEquiv).toFun x * (f.prodCongr g.toEquiv).toFun x_1