∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  {Z : C} (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Abelian.coimage.π g) = 0) =
    (CategoryTheory.CategoryStruct.comp f g = 0)