case h
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ HomologicalComplex.Hom.f (lift f P Q ≫ Q.π) 0 = HomologicalComplex.Hom.f (P.π ≫ (ChainComplex.single₀ C).map f) 0
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ lift f P Q ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
ext
no goals
case h
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ HomologicalComplex.Hom.f (lift f P Q ≫ Q.π) 0 = HomologicalComplex.Hom.f (P.π ≫ (ChainComplex.single₀ C).map f) 0
simp [lift, liftZero]