∀ {G H : AddCommGrpCat} (f : G ⟶ H) (x : CategoryTheory.Limits.Cofork f 0)
  (x_1 : (AddCommGrpCat.cokernelCocone f).pt ⟶ x.pt),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π (AddCommGrpCat.cokernelCocone f)) x_1 = x.π →
    x_1 = AddCommGrpCat.ofHom (QuotientAddGroup.lift (AddCommGrpCat.Hom.hom f).range x.π.hom' ⋯)