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