∀ {J : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddGrpCat)
  (x : CategoryTheory.Limits.Cone F) (x_1 : ↑((CategoryTheory.forget₂ AddGrpCat AddMonCat).mapCone x).1) {j j' : J}
  (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGrpCat AddMonCat).mapCone x)).π.app j)
      (((F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat)).comp (CategoryTheory.forget AddMonCat)).map f) x_1 =
    ((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGrpCat AddMonCat).mapCone x)).π.app j' x_1