∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (s : CategoryTheory.Limits.Cocone F) (x : RingCat.Colimits.Prequotient F),
  RingCat.Colimits.descFunLift F s x =
    match x with
    | RingCat.Colimits.Prequotient.of j x => (CategoryTheory.ConcreteCategory.hom (s.ι.app j)) x
    | RingCat.Colimits.Prequotient.zero => 0
    | RingCat.Colimits.Prequotient.one => 1
    | x.neg => -RingCat.Colimits.descFunLift F s x
    | x.add y => RingCat.Colimits.descFunLift F s x + RingCat.Colimits.descFunLift F s y
    | x.mul y => RingCat.Colimits.descFunLift F s x * RingCat.Colimits.descFunLift F s y