C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n ≫ πSummand s (IndexSet.id [n].op) =
    𝟙 (X.obj [n].op) ≫ πSummand s (IndexSet.id [n].op)
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n ≫ πSummand s (IndexSet.id [n].op) = πSummand s (IndexSet.id [n].op)
conv_rhs => rw [← id_comp (s.πSummand _)]
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ 𝟙 (X.obj [n].op) ≫ πSummand s (IndexSet.id [n].op) =
    HomologicalComplex.Hom.f PInfty n ≫ πSummand s (IndexSet.id [n].op)
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n ≫ πSummand s (IndexSet.id [n].op) =
    𝟙 (X.obj [n].op) ≫ πSummand s (IndexSet.id [n].op)
symm
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ 𝟙 (X.obj [n].op) ≫ πSummand s (IndexSet.id [n].op) =
    HomologicalComplex.Hom.f PInfty n ≫ πSummand s (IndexSet.id [n].op)
rw [← sub_eq_zero, ← sub_comp, ← comp_PInfty_eq_zero_iff, sub_comp, id_comp, PInfty_f_idem,
  sub_self]