-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq.{v_1 + 1} (α := Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n :
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n ⟶
            HomologicalComplex.X (Karoubi.X (obj N₂ (obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) (obj Γ₀ X)))) n)
        (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
          (HomologicalComplex.Hom.f PInfty n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
            Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
          (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
              (HomologicalComplex.Hom.f PInfty n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
                Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
              (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
                  (HomologicalComplex.Hom.f PInfty n :
                    HomologicalComplex.X
                        (AlternatingFaceMapComplex.obj (obj Γ₂ (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)).X)
                        n ⟶
                      HomologicalComplex.X
                        (AlternatingFaceMapComplex.obj (obj Γ₂ (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)).X)
                        n)
                  (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
                      𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
                        Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
                    Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
                Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
            Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))) :
      Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n ⟶
        HomologicalComplex.X (Karoubi.X (obj N₂ (obj Γ₂ (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)))) n)
have h : Eq.{v_1 + 1} (α := Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
  (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
      (HomologicalComplex.Hom.f PInfty n :
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n)
      (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
          𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
            Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
        Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
    Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
  (HomologicalComplex.Hom.f PInfty n :
    HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n ⟶
      HomologicalComplex.X (Karoubi.X (obj N₂ (obj Γ₂ (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)))) n)
Tactic: simp only [comp_id, PInfty_f_idem_assoc, AlternatingFaceMapComplex.obj_X, Γ₀_obj_obj]