C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ πSummand s (IndexSet.id [n].op) ≫ ιSummand s (IndexSet.id [n].op) ≫ HomologicalComplex.Hom.f PInfty n =
    𝟙 (HomologicalComplex.X K[X] n) ≫ HomologicalComplex.Hom.f PInfty n
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ πSummand s (IndexSet.id [n].op) ≫ ιSummand s (IndexSet.id [n].op) ≫ HomologicalComplex.Hom.f PInfty n =
    HomologicalComplex.Hom.f PInfty n
conv_rhs => rw [← id_comp (PInfty.f n)]
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ πSummand s (IndexSet.id [n].op) ≫ ιSummand s (IndexSet.id [n].op) ≫ HomologicalComplex.Hom.f PInfty n =
    ∑ j : IndexSet [n].op, (πSummand s j ≫ ιSummand s j) ≫ HomologicalComplex.Hom.f PInfty n
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ πSummand s (IndexSet.id [n].op) ≫ ιSummand s (IndexSet.id [n].op) ≫ HomologicalComplex.Hom.f PInfty n =
    𝟙 (HomologicalComplex.X K[X] n) ≫ HomologicalComplex.Hom.f PInfty n
erw [s.decomposition_id, Preadditive.sum_comp]
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ ∀ (x : IndexSet [n].op),
    x ≠ IndexSet.id [n].op → (πSummand s x ≫ ιSummand s x) ≫ HomologicalComplex.Hom.f PInfty n = 0
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ πSummand s (IndexSet.id [n].op) ≫ ιSummand s (IndexSet.id [n].op) ≫ HomologicalComplex.Hom.f PInfty n =
    ∑ j : IndexSet [n].op, (πSummand s j ≫ ιSummand s j) ≫ HomologicalComplex.Hom.f PInfty n
rw [Fintype.sum_eq_single (IndexSet.id (op [n])), assoc]
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
A : IndexSet [n].op
hA : ¬IndexSet.EqId A
⊢ (πSummand s A ≫ ιSummand s A) ≫ HomologicalComplex.Hom.f PInfty n = 0
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ ∀ (x : IndexSet [n].op),
    x ≠ IndexSet.id [n].op → (πSummand s x ≫ ιSummand s x) ≫ HomologicalComplex.Hom.f PInfty n = 0
rintro A (hA : ¬A.EqId)
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
A : IndexSet [n].op
hA : ¬IndexSet.EqId A
⊢ (πSummand s A ≫ ιSummand s A) ≫ HomologicalComplex.Hom.f PInfty n = 0
rw [assoc, s.ιSummand_comp_PInfty_eq_zero A hA, comp_zero]