∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {Q' : C} (eQ : Q' ≅ h.Q),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Limits.parallelPair (h.hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) 0).map
        CategoryTheory.Limits.WalkingParallelPairHom.right)
      (CategoryTheory.Iso.refl S.X₃).hom =
    CategoryTheory.CategoryStruct.comp eQ.symm.hom
      ((CategoryTheory.Limits.parallelPair
            ((CategoryTheory.Limits.IsCokernel.cokernelIso S.f (CategoryTheory.CategoryStruct.comp h.p eQ.inv) h.hp
                  eQ.symm ⋯).desc
              (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯))
            0).map
        CategoryTheory.Limits.WalkingParallelPairHom.right)