∀ {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'} (hom : I.cocomplex ⟶ I'.cocomplex)
  (ι_f_zero_comp_hom_f_zero :
    CategoryTheory.CategoryStruct.comp (I.ι.f 0) (hom.f 0) =
      CategoryTheory.CategoryStruct.comp (((CochainComplex.single₀ C).map f).f 0) (I'.ι.f 0))
  (hom_1 : I.cocomplex ⟶ I'.cocomplex)
  (ι_f_zero_comp_hom_f_zero_1 :
    CategoryTheory.CategoryStruct.comp (I.ι.f 0) (hom_1.f 0) =
      CategoryTheory.CategoryStruct.comp (((CochainComplex.single₀ C).map f).f 0) (I'.ι.f 0)),
  ({ hom := hom, ι_f_zero_comp_hom_f_zero := ι_f_zero_comp_hom_f_zero } =
      { hom := hom_1, ι_f_zero_comp_hom_f_zero := ι_f_zero_comp_hom_f_zero_1 }) =
    (hom = hom_1)