-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.AbelianStruct.mk.injEq : ∀ {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)