-- 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
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
rw :
  Eq (α := s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := X _⦋i⦌)
            (HomologicalComplex.Hom.f PInfty i : HomologicalComplex.X K[X] i ⟶ HomologicalComplex.X K[X] i)
            (HomologicalComplex.d K[X] i j) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ X _⦋j⦌) :
      s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := s.N j)
        (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
            (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
              summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
                Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
            (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))) :
              Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N j) :
          s.N i ⟶ s.N j)
        (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
            (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
              summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
                Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
            (HomologicalComplex.Hom.f PInfty j : HomologicalComplex.X K[X] j ⟶ HomologicalComplex.X K[X] j) :
          s.N j ⟶ X _⦋j⦌) :
      s.N i ⟶ X _⦋j⦌)
rw₁ :
  Eq (α := s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := X _⦋i⦌)
            (HomologicalComplex.Hom.f PInfty i : HomologicalComplex.X K[X] i ⟶ HomologicalComplex.X K[X] i)
            (HomologicalComplex.d K[X] i j) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ X _⦋j⦌) :
      s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := s.N j)
            (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))) :
              Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N j)
            (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
                  summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
                    Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (HomologicalComplex.Hom.f PInfty j : HomologicalComplex.X K[X] j ⟶ HomologicalComplex.X K[X] j) :
              s.N j ⟶ X _⦋j⦌) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ X _⦋j⦌) :
      s.N i ⟶ X _⦋j⦌)
rw₂ :
  Eq (α := s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := X _⦋i⦌)
            (HomologicalComplex.Hom.f PInfty i : HomologicalComplex.X K[X] i ⟶ HomologicalComplex.X K[X] i)
            (HomologicalComplex.d K[X] i j) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ X _⦋j⦌) :
      s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j)
            (CategoryStruct.comp (Y := s.N j)
              (s.πSummand (IndexSet.id (op ⦋j⦌)) :
                X _⦋j⦌ ⟶
                  s.N
                    (unop
                        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                          (IndexSet.id (op ⦋j⦌)))).len)
              (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
                  summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
                    Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (HomologicalComplex.Hom.f PInfty j : HomologicalComplex.X K[X] j ⟶ HomologicalComplex.X K[X] j))) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ X _⦋j⦌) :
      s.N i ⟶ X _⦋j⦌)
rw₃ :
  Eq (α := s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := X _⦋i⦌)
            (HomologicalComplex.Hom.f PInfty i : HomologicalComplex.X K[X] i ⟶ HomologicalComplex.X K[X] i)
            (HomologicalComplex.d K[X] i j) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ X _⦋j⦌) :
      s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := X _⦋j⦌)
            (HomologicalComplex.d K[X] i j : HomologicalComplex.X K[X] i ⟶ HomologicalComplex.X K[X] j)
            (HomologicalComplex.Hom.f PInfty j) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ X _⦋j⦌) :
      s.N i ⟶ X _⦋j⦌)
rw₄ rw₅ :
  Eq (α := s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (HomologicalComplex.d K[X] i j ≫ HomologicalComplex.Hom.f PInfty j :
          HomologicalComplex.X K[X] i ⟶ HomologicalComplex.X K[X] j) :
      s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := X _⦋j⦌)
            (HomologicalComplex.d K[X] i j : HomologicalComplex.X K[X] i ⟶ HomologicalComplex.X K[X] j)
            (HomologicalComplex.Hom.f PInfty j) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ X _⦋j⦌) :
      s.N i ⟶ X _⦋j⦌)
⊢ Eq (α := s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := X _⦋i⦌)
        (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
          (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
            summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
              Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
          (HomologicalComplex.Hom.f PInfty i : HomologicalComplex.X K[X] i ⟶ HomologicalComplex.X K[X] i))
        (HomologicalComplex.d K[X] i j) :
      s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := s.N j)
        (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
            (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
              summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
                Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
            (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))) :
              Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N j) :
          s.N i ⟶ s.N j)
        (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
            (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
              summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
                Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
            (HomologicalComplex.Hom.f PInfty j : HomologicalComplex.X K[X] j ⟶ HomologicalComplex.X K[X] j) :
          s.N j ⟶ X _⦋j⦌) :
      s.N i ⟶ X _⦋j⦌)

Tactic:
rw [assoc, assoc, assoc, πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty,
              HomologicalComplex.Hom.comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, HomologicalComplex.Hom.comm