∀ {k G : Type u_1} [inst : CommRing k] [inst_1 : Monoid G] {X Y Z : ModuleCat (MonoidAlgebra k G)} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  {
      hom :=
        ModuleCat.ofHom
          (let __src := ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g);
          { toAddHom := __src.toAddHom, map_smul' := ⋯ }),
      comm := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      {
        hom :=
          ModuleCat.ofHom
            (let __src := ModuleCat.Hom.hom f;
            { toAddHom := __src.toAddHom, map_smul' := ⋯ }),
        comm := ⋯ }
      {
        hom :=
          ModuleCat.ofHom
            (let __src := ModuleCat.Hom.hom g;
            { toAddHom := __src.toAddHom, map_smul' := ⋯ }),
        comm := ⋯ }