∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  (hkf : CategoryTheory.Limits.IsLimit kf),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Limits.parallelPair
            ((hkf.ofIsoLimit (CategoryTheory.Limits.Fork.ext (CategoryTheory.Iso.refl kf.pt) ⋯)).lift
              (CategoryTheory.Limits.KernelFork.ofι S.f ⋯))
            0).map
        CategoryTheory.Limits.WalkingParallelPairHom.right)
      (S.isoCyclesOfIsLimit hkf).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl
          ((CategoryTheory.Limits.parallelPair
                ((hkf.ofIsoLimit (CategoryTheory.Limits.Fork.ext (CategoryTheory.Iso.refl kf.pt) ⋯)).lift
                  (CategoryTheory.Limits.KernelFork.ofι S.f ⋯))
                0).obj
            CategoryTheory.Limits.WalkingParallelPair.zero)).hom
      ((CategoryTheory.Limits.parallelPair S.toCycles 0).map CategoryTheory.Limits.WalkingParallelPairHom.right)