no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n
simp only [PInfty_f, P_f_idem]