∀ {R : Type u} [inst : Ring R] {ι : Type v} (Z : ι → ModuleCat R) [inst_1 : DecidableEq ι]
  [inst_2 : CategoryTheory.Limits.HasCoproduct Z] (i : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι Z i) (ModuleCat.coprodIsoDirectSum Z).hom =
    ModuleCat.ofHom (DirectSum.lof R ι (fun i => ↑(Z i)) i)