C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
j k : ℕ
A : IndexSet [j].op
hA : ¬Mono (IndexSet.e A)
⊢ ιSummand s A ≫ HomologicalComplex.d K[X] j k ≫ πSummand s (IndexSet.id [k].op) = 0
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
j k : ℕ
A : IndexSet [j].op
hA : ¬IndexSet.EqId A
⊢ ιSummand s A ≫ HomologicalComplex.d K[X] j k ≫ πSummand s (IndexSet.id [k].op) = 0
rw [A.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
j k : ℕ
A : IndexSet [j].op
hA : ¬Mono (IndexSet.e A)
⊢ ιSummand s A ≫ HomologicalComplex.d K[X] j k ≫ πSummand s (IndexSet.id [k].op) = 0
rw [← assoc, ← s.comp_PInfty_eq_zero_iff, assoc, ← PInfty.comm j k, s.ιSummand_eq, assoc,
  degeneracy_comp_PInfty_assoc X j A.e hA, zero_comp, comp_zero]