∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {γ : Type u₁}
  [inst_2 : AddCommMonoid γ],
  DirectSum.fromAddMonoid = DirectSum.toAddMonoid fun i => AddMonoidHom.compHom (DirectSum.of β i)