case i
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) (n + 1) ≅ 0
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ HomologicalComplex.Hom.f I.ι (n + 1) = 0
apply zero_of_source_iso_zero
no goals
case i
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) (n + 1) ≅ 0
rfl