{C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          (kernelFork : CategoryTheory.Limits.KernelFork f) →
            CategoryTheory.Limits.IsLimit kernelFork →
              (cokernelCofork : CategoryTheory.Limits.CokernelCofork f) →
                CategoryTheory.Limits.IsColimit cokernelCofork →
                  (image : C) →
                    (imageπ : X ⟶ image) →
                      (ι_imageπ :
                          autoParam
                            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kernelFork) imageπ = 0)
                            CategoryTheory.Abelian.AbelianStruct.ι_imageπ._autoParam) →
                        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ imageπ ι_imageπ) →
                          (imageι : image ⟶ Y) →
                            (imageι_π :
                                autoParam
                                  (CategoryTheory.CategoryStruct.comp imageι
                                      (CategoryTheory.Limits.Cofork.π cokernelCofork) =
                                    0)
                                  CategoryTheory.Abelian.AbelianStruct.imageι_π._autoParam) →
                              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι imageι imageι_π) →
                                autoParam (CategoryTheory.CategoryStruct.comp imageπ imageι = f)
                                    CategoryTheory.Abelian.AbelianStruct.fac._autoParam →
                                  CategoryTheory.Abelian.AbelianStruct f