∀ (G H : GrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)),
  (G.binaryProductLimitCone H).isLimit.lift t =
    GrpCat.ofHom
      ((GrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod
        (GrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))