∀ {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)
  (a :
    (j : C) ×
      (((M.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)).comp
                (CategoryTheory.forget₂ AddGrpCat AddMonCat)).comp
            (CategoryTheory.forget AddMonCat)).obj
        j),
  1 •
      Quot.mk
        (((M.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)).comp
                (CategoryTheory.forget₂ AddGrpCat AddMonCat)).comp
            (CategoryTheory.forget AddMonCat)).ColimitTypeRel
        a =
    Quot.mk
      (((M.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)).comp
              (CategoryTheory.forget₂ AddGrpCat AddMonCat)).comp
          (CategoryTheory.forget AddMonCat)).ColimitTypeRel
      a