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