∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat) (x x_1 : J) (f : x ⟶ x_1),
  CategoryTheory.CategoryStruct.comp (F.map f)
      (AddGrpCat.ofHom
        (AddMonCat.Hom.hom
          ((AddMonCat.FilteredColimits.colimitCocone (F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat))).ι.app
            x_1))) =
    CategoryTheory.CategoryStruct.comp
      (AddGrpCat.ofHom
        (AddMonCat.Hom.hom
          ((AddMonCat.FilteredColimits.colimitCocone (F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat))).ι.app x)))
      (((CategoryTheory.Functor.const J).obj (AddGrpCat.FilteredColimits.colimit F)).map f)