C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X✝ : SimplicialObject C
s✝ : Splitting X✝
inst✝ : Preadditive C
X : SimplicialObject C
s : Splitting X
n : ℕ
A : IndexSet [n].op
hA : ¬Mono (IndexSet.e 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
X : SimplicialObject C
s : Splitting X
n : ℕ
A : IndexSet [n].op
hA : ¬IndexSet.EqId A
⊢ ιSummand s A ≫ HomologicalComplex.Hom.f PInfty n = 0
rw [SimplicialObject.Splitting.IndexSet.eqId_iff_mono] at hA
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X✝ : SimplicialObject C
s✝ : Splitting X✝
inst✝ : Preadditive C
X : SimplicialObject C
s : Splitting X
n : ℕ
A : IndexSet [n].op
hA : ¬Mono (IndexSet.e A)
⊢ ιSummand s A ≫ HomologicalComplex.Hom.f PInfty n = 0
rw [SimplicialObject.Splitting.ιSummand_eq, assoc, degeneracy_comp_PInfty X n A.e hA, comp_zero]