∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z) (n : ℕ)
  (g : J.cocomplex.X n ⟶ I.cocomplex.X n) (g' : J.cocomplex.X (n + 1) ⟶ I.cocomplex.X (n + 1))
  (w :
    CategoryTheory.CategoryStruct.comp g (I.cocomplex.d n (n + 1)) =
      CategoryTheory.CategoryStruct.comp (J.cocomplex.d n (n + 1)) g'),
  CategoryTheory.CategoryStruct.comp g' (I.cocomplex.d (n + 1) (n + 2)) =
    CategoryTheory.CategoryStruct.comp (J.cocomplex.d (n + 1) (n + 2)) (I.descFSucc J n g g' ⋯).fst