-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬Mono A.e
rw :
  Eq (α :=
    summand s.N (op ⦋j⦌) A ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋k⦌)))).len)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
        (Cofan.inj (s.cofan (op ⦋j⦌)) A) (HomologicalComplex.d K[X] j k) ≫
      s.πSummand (IndexSet.id (op ⦋k⦌)))
    0
rw₁ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
        (Cofan.inj (s.cofan (op ⦋j⦌)) A) (HomologicalComplex.d K[X] j k) ≫
      HomologicalComplex.Hom.f PInfty k)
    0
rw₂ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
      (Cofan.inj (s.cofan (op ⦋j⦌)) A) (HomologicalComplex.d K[X] j k ≫ HomologicalComplex.Hom.f PInfty k))
    0
rw₃ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
      (Cofan.inj (s.cofan (op ⦋j⦌)) A) (HomologicalComplex.Hom.f PInfty j ≫ HomologicalComplex.d K[X] j k))
    0
rw₄ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    ((s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
        X.map A.e.op) ≫
      HomologicalComplex.Hom.f PInfty j ≫ HomologicalComplex.d K[X] j k)
    0
rw₅ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ HomologicalComplex.Hom.f PInfty j ≫ HomologicalComplex.d K[X] j k)
    0
rw₆ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      0 ≫ HomologicalComplex.d K[X] j k)
    0
rw₇ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫ 0) 0
rw₈ rw₉ : Eq.{v_1 + 1} (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k) 0 0
⊢ Eq (α :=
    summand s.N (op ⦋j⦌) A ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋k⦌)))).len)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
      (Cofan.inj (s.cofan (op ⦋j⦌)) A) (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌))))
    0

Tactic:
rw [← assoc, ← s.comp_PInfty_eq_zero_iff, assoc, ← PInfty.comm j k, s.cofan_inj_eq, assoc,
    degeneracy_comp_PInfty_assoc X j A.e hA, zero_comp, comp_zero]

Premises used: CategoryTheory.SimplicialObject.Splitting.cofan_inj_eq, CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, AlgebraicTopology.DoldKan.PInfty, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty_assoc, CategoryTheory.SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, CategoryTheory.SimplicialObject.Splitting.IndexSet.e, CategoryTheory.Limits.zero_comp, HomologicalComplex.Hom.comm