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