C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ 𝟙 (X.obj [0].op) - 𝟙 (X.obj [0].op) = 0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ HomologicalComplex.Hom.f QInfty 0 = 0
dsimp [QInfty]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ 𝟙 (X.obj [0].op) - 𝟙 (X.obj [0].op) = 0
simp only [sub_self]