∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (F : CategoryTheory.Functor Cᵒᵖ GrpCat) (α : (F.comp (CategoryTheory.forget GrpCat)).RepresentableBy X)
  (Y : Cᵒᵖ) (a b : ↑((CategoryTheory.yonedaMonObj X).obj Y)),
  (MonCat.Hom.hom
        ((CategoryTheory.yonedaMonObjIsoOfRepresentableBy X (F.comp (CategoryTheory.forget₂ GrpCat MonCat)) α).hom.app
          Y))
      (a * b) =
    (MonCat.Hom.hom
          ((CategoryTheory.yonedaMonObjIsoOfRepresentableBy X (F.comp (CategoryTheory.forget₂ GrpCat MonCat)) α).hom.app
            Y))
        a *
      (MonCat.Hom.hom
          ((CategoryTheory.yonedaMonObjIsoOfRepresentableBy X (F.comp (CategoryTheory.forget₂ GrpCat MonCat)) α).hom.app
            Y))
        b