C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty + (𝟙 K[X] - PInfty) = 𝟙 K[X]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty + QInfty = 𝟙 K[X]
dsimp only [QInfty]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty + (𝟙 K[X] - PInfty) = 𝟙 K[X]
simp only [add_sub_cancel'_right]