∀ {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 ι] (f : ((i : ι) → N i) →+ M) (i : ι) (x : N i),
  ((fun ϕ => AddMonoidHom.noncommPiCoprod ↑ϕ ⋯) ((fun f => ⟨fun i => f.comp (AddMonoidHom.single N i), ⋯⟩) f))
      (Pi.single i x) =
    f (Pi.single i x)