-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
eq₁ :
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))) n ⟶
      HomologicalComplex.X
        (Karoubi.X (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))) n)
    (HomologicalComplex.Hom.f PInfty n ≫
      P.p.app (op ⦋n⦌) ≫
        Cofan.inj (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌))
          (Splitting.IndexSet.id (op ⦋n⦌)))
⊢ Eq (α :=
    Splitting.N (X := Γ₀.obj (Karoubi.X (Functor.obj N₂ P))) (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) n ⟶ P.X _⦋n⦌)
    (CategoryStruct.comp (Y := HomologicalComplex.X K[Γ₀.obj (Karoubi.X (Functor.obj N₂ P))] n)
        (Cofan.inj (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌))
          (Splitting.IndexSet.id (op ⦋n⦌)))
        (NatTrans.app
          (Karoubi.Hom.f
            (CategoryTheory.Functor.map (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂)
                P.decompId_i ≫
              NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso ≫ Γ₂N₁.natTrans) P.X ≫ P.decompId_p))
          (op ⦋n⦌)) :
      Splitting.summand
          (Splitting.N (X := Γ₀.obj (Karoubi.X (Functor.obj N₂ P))) (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))))
          (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
        P.X _⦋n⦌)
    (CategoryStruct.comp (Y := P.X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[P.X] n ⟶ HomologicalComplex.X K[P.X] n)
      (P.p.app (op ⦋n⦌)))
have dsimp : Eq (α :=
  Splitting.N (X := Γ₀.obj (Karoubi.X (Functor.obj N₂ P))) (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) n ⟶ P.X _⦋n⦌)
  (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ (Karoubi.X (Functor.obj N₂ P)) (op ⦋n⦌))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌))
          (Splitting.IndexSet.id (op ⦋n⦌)) :
        Splitting.summand
            (Splitting.N (X := Γ₀.obj (Karoubi.X (Functor.obj N₂ P))) (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))))
            (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
            Discrete.functor
              (Splitting.summand
                (Splitting.N (X := Γ₀.obj (Karoubi.X (Functor.obj N₂ P))) (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))))
                (op ⦋n⦌)))
            (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌)))
      (CategoryStruct.comp (Y :=
          Γ₀.Obj.obj₂
            (Karoubi.X (Functor.obj N₂ { X := P.X, p := 𝟙 P.X, idem := sorry : Karoubi (SimplicialObject.{v_1, u_1} C) }))
            (op ⦋n⦌))
          (Splitting.desc (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
              CategoryStruct.comp (Y :=
                  P.X.obj (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })))
                  (HomologicalComplex.Hom.f PInfty
                      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len :
                    HomologicalComplex.X K[P.X]
                        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ⟶
                      HomologicalComplex.X K[P.X]
                        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len)
                  (P.p.app (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))) ≫
                Cofan.inj
                  (Splitting.cofan
                    (Γ₀.splitting
                      (Karoubi.X
                        (Functor.obj N₂ { X := P.X, p := 𝟙 P.X, idem := sorry : Karoubi (SimplicialObject.{v_1, u_1} C) })))
                    (op ⦋n⦌))
                  A :
            Γ₀.obj (Karoubi.X (Functor.obj N₂ P)) _⦋n⦌ ⟶
              Γ₀.Obj.obj₂
                (Karoubi.X
                  (Functor.obj N₂ { X := P.X, p := 𝟙 P.X, idem := sorry : Karoubi (SimplicialObject.{v_1, u_1} C) }))
                (op ⦋n⦌))
          (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ K[P.X] (op ⦋n⦌))
                (NatTrans.app (Karoubi.Hom.f (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) P.X)) (op ⦋n⦌) :
                  (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
                          (Functor.obj N₂
                            { X := P.X, p := 𝟙 P.X, idem := sorry : Karoubi (SimplicialObject.{v_1, u_1} C) })).X _⦋n⦌ ⟶
                    (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ P.X)).X _⦋n⦌)
                (Splitting.desc (Γ₀.splitting K[P.X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
                  HomologicalComplex.Hom.f PInfty
                      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
                    P.X.map A.e.op) ≫
              P.p.app (op ⦋n⦌) :
            Γ₀.Obj.obj₂
                (Karoubi.X
                  (Functor.obj N₂ { X := P.X, p := 𝟙 P.X, idem := sorry : Karoubi (SimplicialObject.{v_1, u_1} C) }))
                (op ⦋n⦌) ⟶
              P.X _⦋n⦌) :
        Γ₀.Obj.obj₂ (Karoubi.X (Functor.obj N₂ P)) (op ⦋n⦌) ⟶ P.X _⦋n⦌) :
    Splitting.N (X := Γ₀.obj (Karoubi.X (Functor.obj N₂ P))) (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) n ⟶ P.X _⦋n⦌)
  (CategoryStruct.comp (Y := P.X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[P.X] n ⟶ HomologicalComplex.X K[P.X] n)
      (P.p.app (op ⦋n⦌)) :
    P.X _⦋n⦌ ⟶ P.X _⦋n⦌)
Tactic: dsimp