∀ (C : Type u_2) {ι : Type u_3} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (i j : ι) [inst_2 : CategoryTheory.CategoryWithHomology C] {K L : HomologicalComplex C c}
  (φ : K ⟶ L),
  CategoryTheory.CategoryStruct.comp
      ((HomologicalComplex.HomologySequence.composableArrows₃ K i j).map' 2 3 _proof_291✝ _proof_292✝)
      (HomologicalComplex.homologyMap φ j) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ j)
      ((HomologicalComplex.HomologySequence.composableArrows₃ L i j).map' 2 3 _proof_291✝¹ _proof_292✝¹)