∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J] (j : J) (x : ↑((F.comp AddCommGrpCat.uliftFunctor).obj j)),
  (AddCommGrpCat.Colimits.quotUliftToQuot F) ((AddCommGrpCat.Colimits.Quot.ι (F.comp AddCommGrpCat.uliftFunctor) j) x) =
    (AddCommGrpCat.Colimits.Quot.ι F j) x.down