-- 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
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) Y)
    (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 := ⋯ })
    ({
        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)
have h : 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 := sorry },
        comm := sorry }))
  (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 := sorry :
            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 := sorry :
        (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: ext1