∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddCommMonCat),
  AddCommMonCat.FilteredColimits.colimitCoconeIsColimit F =
    CategoryTheory.Limits.isColimitOfReflects (CategoryTheory.forget₂ AddCommMonCat AddMonCat)
      (AddMonCat.FilteredColimits.colimitCoconeIsColimit (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)))