∀ {V : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_3} [inst_3 : DecidableEq ι] {c : ComplexShape ι}
  {K : HomologicalComplex V c} {j : ι} {A : V} (φ : K.X j ⟶ A),
  (∀ (i : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (K.d i j) φ = 0) →
    ∀ (i k : ι),
      c.Rel i k →
        CategoryTheory.CategoryStruct.comp
            (if hi : i = j then
              CategoryTheory.CategoryStruct.comp (K.XIsoOfEq hi).hom
                (CategoryTheory.CategoryStruct.comp φ (HomologicalComplex.singleObjXIsoOfEq c j A i hi).inv)
            else 0)
            (((HomologicalComplex.single V c j).obj A).d i k) =
          CategoryTheory.CategoryStruct.comp (K.d i k)
            (if hi : k = j then
              CategoryTheory.CategoryStruct.comp (K.XIsoOfEq hi).hom
                (CategoryTheory.CategoryStruct.comp φ (HomologicalComplex.singleObjXIsoOfEq c j A k hi).inv)
            else 0)