no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ HomologicalComplex.d J.cocomplex 0 1 ≫ descFOne f I J = descFZero f I J ≫ HomologicalComplex.d I.cocomplex 0 1
simp [descFZero, descFOne]