-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
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 k : ℕ
h : (ComplexShape.down ℕ).Rel i j
h_1 : (ComplexShape.down ℕ).Rel j k
eq :
  Eq (α :=
    HomologicalComplex.X K[X] i ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋k⦌)))).len)
    (HomologicalComplex.d K[X] i j ≫
      CategoryStruct.comp (Y := X _⦋j⦌)
        (∑ A : IndexSet (op ⦋j⦌), s.πSummand A ≫ Cofan.inj (s.cofan (op ⦋j⦌)) A :
          X _⦋j⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
        (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) :
          X _⦋j⦌ ⟶
            s.N
              (unop
                  (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
                    (IndexSet.id (op ⦋k⦌)))).len))
    0
rw :
  ∀
    (eq :
      Eq (α :=
        HomologicalComplex.X K[X] i ⟶
          s.N
            (unop
                (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
                  (IndexSet.id (op ⦋k⦌)))).len)
        (HomologicalComplex.d K[X] i j ≫
          HAdd.hAdd (α := X _⦋j⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
              (CategoryStruct.comp (Y :=
                s.N
                  (unop
                      (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                        (IndexSet.id (op ⦋j⦌)))).len)
                (s.πSummand (IndexSet.id (op ⦋j⦌))) (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌))))
              (∑ i ∈ {IndexSet.id (op ⦋j⦌)}ᶜ, s.πSummand i ≫ Cofan.inj (s.cofan (op ⦋j⦌)) i) ≫
            HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)))
        0),
    Eq (α := s.N i ⟶ s.N k)
      (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 := HomologicalComplex.X K[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⦌)))
                  (CategoryStruct.comp (Y := HomologicalComplex.X K[X] k) (HomologicalComplex.d K[X] j k)
                      (s.πSummand (IndexSet.id (op ⦋k⦌))) :
                    Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)) ⟶ s.N k))) :
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N k) :
        s.N i ⟶ s.N k)
      (0 : s.N i ⟶ s.N k)
rw₁ :
  ∀
    (eq :
      HomologicalComplex.d K[X] i j ≫
          HAdd.hAdd (α :=
            HomologicalComplex.X K[X] j ⟶
              s.N
                (unop
                    (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
                      (IndexSet.id (op ⦋k⦌)))).len)
            (CategoryStruct.comp (Y := X _⦋j⦌)
              (CategoryStruct.comp (Y :=
                  s.N
                    (unop
                        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                          (IndexSet.id (op ⦋j⦌)))).len)
                  (s.πSummand (IndexSet.id (op ⦋j⦌))) (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌))) :
                X _⦋j⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
              (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌))))
            (CategoryStruct.comp (Y := X _⦋j⦌)
              (∑ i ∈ {IndexSet.id (op ⦋j⦌)}ᶜ, s.πSummand i ≫ Cofan.inj (s.cofan (op ⦋j⦌)) i :
                X _⦋j⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
              (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) :
                X _⦋j⦌ ⟶
                  s.N
                    (unop
                        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
                          (IndexSet.id (op ⦋k⦌)))).len)) =
        0),
    Eq (α := s.N i ⟶ s.N k)
      (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 := HomologicalComplex.X K[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⦌)))
                  (CategoryStruct.comp (Y := HomologicalComplex.X K[X] k) (HomologicalComplex.d K[X] j k)
                      (s.πSummand (IndexSet.id (op ⦋k⦌))) :
                    Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)) ⟶ s.N k))) :
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N k) :
        s.N i ⟶ s.N k)
      (0 : s.N i ⟶ s.N k)
rw₂ :
  ∀
    (eq :
      HAdd.hAdd (α :=
          HomologicalComplex.X K[X] i ⟶
            s.N
              (unop
                  (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
                    (IndexSet.id (op ⦋k⦌)))).len)
          (HomologicalComplex.d K[X] i j ≫
            CategoryStruct.comp (Y := X _⦋j⦌)
              (CategoryStruct.comp (Y :=
                  s.N
                    (unop
                        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                          (IndexSet.id (op ⦋j⦌)))).len)
                  (s.πSummand (IndexSet.id (op ⦋j⦌))) (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌))) :
                X _⦋j⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
              (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌))))
          (HomologicalComplex.d K[X] i j ≫
            CategoryStruct.comp (Y := X _⦋j⦌)
              (∑ i ∈ {IndexSet.id (op ⦋j⦌)}ᶜ, s.πSummand i ≫ Cofan.inj (s.cofan (op ⦋j⦌)) i :
                X _⦋j⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
              (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) :
                X _⦋j⦌ ⟶
                  s.N
                    (unop
                        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
                          (IndexSet.id (op ⦋k⦌)))).len)) =
        0),
    Eq (α := s.N i ⟶ s.N k)
      (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 := HomologicalComplex.X K[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⦌)))
                  (CategoryStruct.comp (Y := HomologicalComplex.X K[X] k) (HomologicalComplex.d K[X] j k)
                      (s.πSummand (IndexSet.id (op ⦋k⦌))) :
                    Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)) ⟶ s.N k))) :
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N k) :
        s.N i ⟶ s.N k)
      (0 : s.N i ⟶ s.N k)
⊢ Eq (α := s.N i ⟶ s.N k)
    (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 := HomologicalComplex.X K[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⦌)))
                (CategoryStruct.comp (Y := HomologicalComplex.X K[X] k) (HomologicalComplex.d K[X] j k)
                    (s.πSummand (IndexSet.id (op ⦋k⦌))) :
                  Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)) ⟶ s.N k))) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N k) :
      s.N i ⟶ s.N k)
    (0 : s.N i ⟶ s.N k)
have rw₃ : ∀
  (eq :
    HAdd.hAdd (α :=
        HomologicalComplex.X K[X] i ⟶
          s.N
            (unop
                (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
                  (IndexSet.id (op ⦋k⦌)))).len)
        (HomologicalComplex.d K[X] i j ≫
          CategoryStruct.comp (Y :=
            s.N
              (unop
                  (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                    (IndexSet.id (op ⦋j⦌)))).len)
            (s.πSummand (IndexSet.id (op ⦋j⦌)))
            (CategoryStruct.comp (Y := X _⦋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.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)))))
        (HomologicalComplex.d K[X] i j ≫
          CategoryStruct.comp (Y := X _⦋j⦌)
            (∑ i ∈ {IndexSet.id (op ⦋j⦌)}ᶜ, s.πSummand i ≫ Cofan.inj (s.cofan (op ⦋j⦌)) i :
              X _⦋j⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
            (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) :
              X _⦋j⦌ ⟶
                s.N
                  (unop
                      (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
                        (IndexSet.id (op ⦋k⦌)))).len)) =
      0),
  Eq (α := s.N i ⟶ s.N k)
    (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 := HomologicalComplex.X K[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⦌)))
                (CategoryStruct.comp (Y := HomologicalComplex.X K[X] k) (HomologicalComplex.d K[X] j k)
                    (s.πSummand (IndexSet.id (op ⦋k⦌))) :
                  Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)) ⟶ s.N k))) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N k) :
      s.N i ⟶ s.N k)
    (0 : s.N i ⟶ s.N k)
Tactic: classical
    rw [Fintype.sum_eq_add_sum_compl (IndexSet.id (op ⦋j⦌)), add_comp, comp_add, assoc,
      Preadditive.sum_comp, Preadditive.comp_sum, Finset.sum_eq_zero, add_zero] at eq
    swap
    · intro A hA
      simp only [Finset.mem_compl, Finset.mem_singleton] at hA
      simp only [assoc, ιSummand_comp_d_comp_πSummand_eq_zero _ _ _ _ hA, comp_zero]
    rw [eq, comp_zero]
Cleared hypotheses: eq