-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.AbelianStruct.mk.inj : ∀ {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}
  {isLimitKernelFork : CategoryTheory.Limits.IsLimit kernelFork}
  {cokernelCofork : CategoryTheory.Limits.CokernelCofork f}
  {isColimitCokernelCofork : 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}
  {imageIsCokernel : 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}
  {imageIsKernel : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι imageι imageι_π)}
  {fac :
    autoParam (CategoryTheory.CategoryStruct.comp imageπ imageι = f)
      CategoryTheory.Abelian.AbelianStruct.fac._autoParam}
  {kernelFork_1 : CategoryTheory.Limits.KernelFork f} {isLimitKernelFork_1 : CategoryTheory.Limits.IsLimit kernelFork_1}
  {cokernelCofork_1 : CategoryTheory.Limits.CokernelCofork f}
  {isColimitCokernelCofork_1 : CategoryTheory.Limits.IsColimit cokernelCofork_1} {image_1 : C} {imageπ_1 : X ⟶ image_1}
  {ι_imageπ_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kernelFork_1) imageπ_1 = 0)
      CategoryTheory.Abelian.AbelianStruct.ι_imageπ._autoParam}
  {imageIsCokernel_1 : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ imageπ_1 ι_imageπ_1)}
  {imageι_1 : image_1 ⟶ Y}
  {imageι_π_1 :
    autoParam (CategoryTheory.CategoryStruct.comp imageι_1 (CategoryTheory.Limits.Cofork.π cokernelCofork_1) = 0)
      CategoryTheory.Abelian.AbelianStruct.imageι_π._autoParam}
  {imageIsKernel_1 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι imageι_1 imageι_π_1)}
  {fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp imageπ_1 imageι_1 = f)
      CategoryTheory.Abelian.AbelianStruct.fac._autoParam},
  { kernelFork := kernelFork, isLimitKernelFork := isLimitKernelFork, cokernelCofork := cokernelCofork,
        isColimitCokernelCofork := isColimitCokernelCofork, image := image, imageπ := imageπ, ι_imageπ := ι_imageπ,
        imageIsCokernel := imageIsCokernel, imageι := imageι, imageι_π := imageι_π, imageIsKernel := imageIsKernel,
        fac := fac } =
      { kernelFork := kernelFork_1, isLimitKernelFork := isLimitKernelFork_1, cokernelCofork := cokernelCofork_1,
        isColimitCokernelCofork := isColimitCokernelCofork_1, image := image_1, imageπ := imageπ_1,
        ι_imageπ := ι_imageπ_1, imageIsCokernel := imageIsCokernel_1, imageι := imageι_1, imageι_π := imageι_π_1,
        imageIsKernel := imageIsKernel_1, fac := fac_1 } →
    kernelFork = kernelFork_1 ∧
      isLimitKernelFork ≍ isLimitKernelFork_1 ∧
        cokernelCofork = cokernelCofork_1 ∧
          isColimitCokernelCofork ≍ isColimitCokernelCofork_1 ∧
            image = image_1 ∧
              imageπ ≍ imageπ_1 ∧
                imageIsCokernel ≍ imageIsCokernel_1 ∧ imageι ≍ imageι_1 ∧ imageIsKernel ≍ imageIsKernel_1