∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} {I : CategoryTheory.InjectiveResolution Z} {Z' : C}
  {I' : CategoryTheory.InjectiveResolution Z'} {f : Z ⟶ Z'} (self : I.Hom I' f) {Z_1 : C} (h : I'.cocomplex.X 0 ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (CategoryTheory.CategoryStruct.comp (self.hom.f 0) h) =
    CategoryTheory.CategoryStruct.comp (((CochainComplex.single₀ C).map f).f 0)
      (CategoryTheory.CategoryStruct.comp (I'.ι.f 0) h)