∀ {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddEquiv.prodAddUnits =
    { toFun := ⇑((AddUnits.map (AddMonoidHom.fst M N)).prod (AddUnits.map (AddMonoidHom.snd M N))),
      invFun := fun u => { val := (↑u.1, ↑u.2), neg := (↑(-u.1), ↑(-u.2)), val_neg := ⋯, neg_val := ⋯ }, left_inv := ⋯,
      right_inv := ⋯, map_add' := ⋯ }