∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} {inst : DecidableEq ι} {inst_1 : AddCommMonoid M} {inst_2 : SetLike σ M}
  {inst_3 : AddSubmonoidClass σ M} {ℳ : ι → σ} [self : DirectSum.Decomposition ℳ],
  Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) DirectSum.Decomposition.decompose'