∀ {C : Type u_1} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.IsFiltered C]
  (R : CategoryTheory.Functor C RingCat) (M : CategoryTheory.Functor C Ab)
  [inst_2 : (i : C) → Module ↑(R.obj i) ↑(M.obj i)]
  (H :
    ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
      (CategoryTheory.ConcreteCategory.hom (M.map f)) (r • m) =
        (CategoryTheory.ConcreteCategory.hom (R.map f)) r • (CategoryTheory.ConcreteCategory.hom (M.map f)) m)
  (r s : ↑(RingCat.FilteredColimits.colimit R)) (m : ↑(AddCommGrpCat.FilteredColimits.colimit M)),
  (r * s) • m = r • s • m