-- 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
n : ℕ
h :
  Eq (α := s.N n ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
            (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
              summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶
                Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
            (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) :
          s.N n ⟶ X _⦋n⦌)
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) :
      s.N n ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
          summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) :
      s.N n ⟶ X _⦋n⦌)
⊢ Eq.{v_1 + 1} (α := s.N n ⟶ X _⦋n⦌)
    (𝟙 (s.N n) ≫
      CategoryStruct.comp (Y := X _⦋n⦌)
        (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
            (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
              summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶
                Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
            (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) :
          s.N n ⟶ X _⦋n⦌)
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
        summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n))
have h₁ : Eq (α := s.N n ⟶ X _⦋n⦌)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
        summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (CategoryStruct.comp (Y := X _⦋n⦌)
          (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
          (HomologicalComplex.Hom.f PInfty n) :
        Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)) ⟶ X _⦋n⦌) :
    s.N n ⟶ X _⦋n⦌)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
        summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) :
    s.N n ⟶ X _⦋n⦌)
Tactic: rw [id_comp, assoc, PInfty_f_idem]