∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (a b n : ℤ) (h : a + b = n) (a' : ℤ) (ha' : a' = a + x) (n' : ℤ) (hn' : n' = n + x),
  CategoryTheory.CategoryStruct.comp
      (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).ιTotal (ComplexShape.up ℤ) a b n h)
      ((K.totalShift₁Iso x).hom.f n) =
    CategoryTheory.CategoryStruct.comp (K.shiftFunctor₁XXIso a x a' ha' b).hom
      (CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a' b n' ⋯)
        (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) x n n' hn').inv)