∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j : J)
  (x y : ↑(F.obj j)),
  RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.of j (x * y))
    ((RingCat.Colimits.Prequotient.of j x).mul (RingCat.Colimits.Prequotient.of j y))