∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → AddMonoid (N i)] [inst_3 : DecidableEq ι],
  AddMonoidHom.noncommPiCoprodEquiv =
    { toFun := fun ϕ => AddMonoidHom.noncommPiCoprod ↑ϕ ⋯,
      invFun := fun f => ⟨fun i => f.comp (AddMonoidHom.single N i), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }