∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections],
  AddGrpCat.limitConeIsLimit F =
    CategoryTheory.liftedLimitIsLimit
      (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat)))