case h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (QInfty ≫ PInfty) n = HomologicalComplex.Hom.f 0 n
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ QInfty ≫ PInfty = 0
ext n
no goals
case h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (QInfty ≫ PInfty) n = HomologicalComplex.Hom.f 0 n
apply QInfty_f_comp_PInfty_f