case i
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ HomologicalComplex.X ((ChainComplex.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
P : ProjectiveResolution Z
n : ℕ
⊢ HomologicalComplex.Hom.f P.π (n + 1) = 0
apply zero_of_target_iso_zero
case i
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ 0 ≅ 0
case i
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ HomologicalComplex.X ((ChainComplex.single₀ C).obj Z) (n + 1) ≅ 0
dsimp
no goals
case i
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ 0 ≅ 0
rfl