case h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HomologicalComplex.Hom.f (P q ≫ P q) n = HomologicalComplex.Hom.f (P q) n
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q ≫ P q = P 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 (P q ≫ P q) n = HomologicalComplex.Hom.f (P q) n
exact P_f_idem q n