∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex)
  (n : ℕ) (g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) (g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1))
  (w :
    f.f (n + 1) =
      CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' +
        CategoryTheory.CategoryStruct.comp g (J.cocomplex.d n (n + 1))),
  CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 2) (n + 3))
      (CategoryTheory.InjectiveResolution.descHomotopyZeroSucc f n g g' w) =
    f.f (n + 2) - CategoryTheory.CategoryStruct.comp g' (J.cocomplex.d (n + 1) (n + 2))