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