-- 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
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
h :
  Eq (α := Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X]) n ⟶ Y _⦋n⦌)
    (Splitting.ι (Γ₀.splitting K[X]) n ≫
      CategoryStruct.comp (Y := Γ₀.Obj.obj₂ K[Y] (op ⦋n⦌))
        (Splitting.desc (Γ₀.splitting K[X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
            CategoryStruct.comp (Y :=
                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[X]
                      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ⟶
                    HomologicalComplex.X K[X]
                      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len)
                (f.app (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))) ≫
              Cofan.inj (Splitting.cofan (Γ₀.splitting K[Y]) (op ⦋n⦌)) A :
          Γ₀.obj K[X] _⦋n⦌ ⟶ Γ₀.Obj.obj₂ K[Y] (op ⦋n⦌))
        (Splitting.desc (Γ₀.splitting K[Y]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
            HomologicalComplex.Hom.f PInfty
                (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
              Y.map A.e.op :
          Γ₀.obj K[Y] _⦋n⦌ ⟶ Y _⦋n⦌))
    (Splitting.ι (Γ₀.splitting K[X]) n ≫
      (Splitting.desc (Γ₀.splitting K[X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
            X.map A.e.op) ≫
        f.app (op ⦋n⦌))
⊢ Eq (α :=
    Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X]) n ⟶
      Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) Y) _⦋n⦌)
    (Splitting.φ (Γ₀.splitting K[X])
      (Karoubi.Hom.f
        (CategoryTheory.Functor.map (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) f ≫
          {
            f :=
              {
                app := fun (Δ : SimplexCategoryᵒᵖ) ↦
                  Splitting.desc (Γ₀.splitting K[Y]) Δ fun (A : Splitting.IndexSet Δ) ↦
                    HomologicalComplex.Hom.f PInfty
                        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
                      Y.map A.e.op,
                naturality := ⋯ },
            comm := ⋯ }))
      n)
    (Splitting.φ (Γ₀.splitting K[X])
      (Karoubi.Hom.f
        ({
            f :=
              {
                app := fun (Δ : SimplexCategoryᵒᵖ) ↦
                  Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
                    HomologicalComplex.Hom.f PInfty
                        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
                      X.map A.e.op,
                naturality := ⋯ :
                NatTrans (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).X
                  (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) },
            comm := ⋯ :
            (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).Hom
              (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) } ≫
          CategoryTheory.Functor.map (toKaroubi (SimplicialObject.{v_1, u_1} C)) f))
      n)

Tactic:
dsimp [N₁, toKaroubi]

Premises used: CategoryTheory.Idempotents.toKaroubi, AlgebraicTopology.DoldKan.N₁