∀ {V : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) (i j : ℕ),
  (ComplexShape.down ℕ).Rel i j →
    CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CategoryStruct.id ((ChainComplex.truncate.obj (C.augment f w)).X i)) (C.d i j) =
      CategoryTheory.CategoryStruct.comp ((ChainComplex.truncate.obj (C.augment f w)).d i j)
        (CategoryTheory.CategoryStruct.id ((ChainComplex.truncate.obj (C.augment f w)).X j))