∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R}
  (h : S.moduleCatLeftHomologyData.K ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.toCycles (CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom h) =
    CategoryTheory.CategoryStruct.comp S.moduleCatLeftHomologyData.f' h