∀ {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}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).hom
      (CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.KernelFork.ofι S.homologyι ⋯)) =
    CategoryTheory.Limits.Fork.ι
      ((CategoryTheory.Limits.Cones.postcompose
            (CategoryTheory.Limits.parallelPair.ext (S.isoOpcyclesOfIsColimit hcc)
                (CategoryTheory.Iso.refl
                  ((CategoryTheory.Limits.parallelPair
                        ((hcc.ofIsoColimit (CategoryTheory.Limits.Cofork.ext (CategoryTheory.Iso.refl cc.pt) ⋯)).desc
                          (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯))
                        0).obj
                    CategoryTheory.Limits.WalkingParallelPair.one))
                ⋯ ⋯).hom).obj
        (CategoryTheory.Limits.KernelFork.ofι ι ⋯))