∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C] (n m a a' a'' : ℤ),
  n + a = a' →
    m + a' = a'' →
      ∀ (X : C) (i : ℤ),
        (((HomologicalComplex.single C (ComplexShape.up ℤ) a'').comp
                    (CategoryTheory.shiftFunctor (CochainComplex C ℤ) (m + n))).obj
                X).X
            i =
          ((HomologicalComplex.single C (ComplexShape.up ℤ) a).obj X).X i