∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {M' : Type u_6} {N' : Type u_7}
  [inst_2 : AddZeroClass N'] [inst_3 : AddZeroClass M'] (f : M ≃+ M') (g : N ≃+ N'),
  f.prodCongr g = { toEquiv := f.prodCongr g.toEquiv, map_add' := ⋯ }