∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] (F : CategoryTheory.Functor J MonCat)
  (s : CategoryTheory.Limits.Cocone F) (j : J) (x_1 : ↑(F.obj j)),
  MonCat.Colimits.descFunLift F s (MonCat.Colimits.Prequotient.of j x_1) =
    (CategoryTheory.ConcreteCategory.hom (s.ι.app j)) x_1