-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
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⦌)))
rw :
  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 := 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⦌) ≫
          CategoryStruct.comp (Y := Γ₀.Obj.obj₂ K[P.X] (op ⦋n⦌))
            (CategoryStruct.comp (Y :=
                P.X.obj
                  (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
                    (Splitting.IndexSet.id (op ⦋n⦌))))
                (HomologicalComplex.Hom.f PInfty
                    (unop
                        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
                          (Splitting.IndexSet.id (op ⦋n⦌)))).len :
                  HomologicalComplex.X
                      (Karoubi.X
                        (Functor.obj N₂ { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) }))
                      (unop
                          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
                            (Splitting.IndexSet.id (op ⦋n⦌)))).len ⟶
                    HomologicalComplex.X K[P.X]
                      (unop
                          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
                            (Splitting.IndexSet.id (op ⦋n⦌)))).len)
                (Cofan.inj (Splitting.cofan (Γ₀.splitting K[P.X]) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌))) :
              Splitting.N (X :=
                  Γ₀.obj
                    (Karoubi.X
                      (Functor.obj N₂ { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) })))
                  (Γ₀.splitting
                    (Karoubi.X
                      (Functor.obj N₂ { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) })))
                  (unop
                      (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
                        (Splitting.IndexSet.id (op ⦋n⦌)))).len ⟶
                Γ₀.Obj.obj₂ K[P.X] (op ⦋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₂ K[P.X] (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⦌)
⊢ 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 := 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⦌) ≫
          CategoryStruct.comp (Y :=
            Γ₀.Obj.obj₂
              (Karoubi.X (Functor.obj N₂ { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) }))
              (op ⦋n⦌))
            (Cofan.inj
                (Splitting.cofan
                  (Γ₀.splitting
                    (Karoubi.X
                      (Functor.obj N₂ { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) })))
                  (op ⦋n⦌))
                (Splitting.IndexSet.id (op ⦋n⦌)) :
              Splitting.summand
                  (Splitting.N (X :=
                    Γ₀.obj
                      (Karoubi.X
                        (Functor.obj N₂ { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) })))
                    (Γ₀.splitting
                      (Karoubi.X
                        (Functor.obj N₂
                          { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) }))))
                  (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₂
                              { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) })))
                        (Γ₀.splitting
                          (Karoubi.X
                            (Functor.obj N₂
                              { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) }))))
                      (op ⦋n⦌)))
                  (Splitting.cofan
                    (Γ₀.splitting
                      (Karoubi.X
                        (Functor.obj N₂ { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) })))
                    (op ⦋n⦌)))
            (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ K[P.X] (op ⦋n⦌))
                (Splitting.desc
                    (Γ₀.splitting
                      (Karoubi.X
                        (Functor.obj N₂ { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) })))
                    (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
                            (Karoubi.X
                              (Functor.obj N₂
                                { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) }))
                            (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ⟶
                          HomologicalComplex.X K[P.X]
                            (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len)
                      (Cofan.inj (Splitting.cofan (Γ₀.splitting K[P.X]) (op ⦋n⦌)) A) :
                  Γ₀.obj
                        (Karoubi.X
                          (Functor.obj N₂
                            { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) })) _⦋n⦌ ⟶
                    Γ₀.Obj.obj₂ K[P.X] (op ⦋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₂ K[P.X] (op ⦋n⦌) ⟶ P.X _⦋n⦌) :
              Γ₀.Obj.obj₂
                  (Karoubi.X
                    (Functor.obj N₂ { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) }))
                  (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:
rw [Splitting.ι_desc_assoc]

Premises used: CategoryTheory.SimplicialObject.Splitting.ι_desc_assoc