-- 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
h :
  ∀ (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)
⊢ Eq (α :=
    (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)) Y))
    (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 := ⋯ }))
    (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))

Tactic:
apply (Γ₀.splitting K[X]).hom_ext

Premises used: AlgebraicTopology.DoldKan.Γ₀.splitting, AlgebraicTopology.AlternatingFaceMapComplex.obj, CategoryTheory.SimplicialObject.Splitting.hom_ext