C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (𝟙 K[X] - PInfty) n = 0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f QInfty n = 0
dsimp only [QInfty]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f (𝟙 K[X] - PInfty) n = 0
simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, comp_id,
  PInfty_f_idem, sub_self]