-- 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⦌)))
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 :=
        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⦌)))
        (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₂ P)) (op ⦋n⦌))
            (HomologicalComplex.Hom.f PInfty n :
              HomologicalComplex.X
                  K[(Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)).X] n ⟶
                HomologicalComplex.X
                  K[(Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)).X] n)
            (NatTrans.app (Karoubi.Hom.f (NatTrans.app Γ₂N₂.natTrans P)) (op ⦋n⦌) :
              (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)).X _⦋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⦌)
⊢ Eq (α :=
    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⦌)) ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))) n)
    (CategoryStruct.comp (Y :=
      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⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌))
        (Splitting.IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))) n))
    (HomologicalComplex.Hom.f PInfty n ≫ P.p.app (op ⦋n⦌))

Tactic:
dsimp