-- 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)
w :
  Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
      (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (CategoryStruct.comp (Y :=
        Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
        (CategoryStruct.comp (Y :=
          Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
          (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))
          (CategoryTheory.Functor.map N₂
            (𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))))
        (𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))) ≫
          𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))) ≫
            CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)) :
      Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
        (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
        (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (𝟙 (Functor.obj N₂ P) :
      Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Functor.obj N₂ P) (Functor.obj N₂ P))
w₁ :
  Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
      (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (CategoryStruct.comp (Y :=
      Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
      (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P) ≫
        𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))))
      (𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))) ≫
        𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))) ≫
          CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)))
    (𝟙 (Functor.obj N₂ P))
w₂ :
  Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
      (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (CategoryStruct.comp (Y :=
      Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
      (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))
      (𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))) ≫
        𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))) ≫
          CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)))
    (𝟙 (Functor.obj N₂ P))
w₃ :
  Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
      (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (CategoryStruct.comp (Y :=
      Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
      (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))
      (𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))) ≫
        CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)))
    (𝟙 (Functor.obj N₂ P))
w₄ :
  Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
      (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (CategoryStruct.comp (Y :=
      Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
      (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)) (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)))
    (𝟙 (Functor.obj N₂ P))
w₅ w₆ :
  Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
      (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (𝟙 (Functor.obj N₂ P)) (𝟙 (Functor.obj N₂ P))
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
      (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (CategoryStruct.comp (Y :=
        Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
        (CategoryStruct.comp (Y :=
          Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
          (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))
          (CategoryTheory.Functor.map N₂ (CategoryTheory.Functor.map Γ₂ (𝟙 (Functor.obj N₂ P)))))
        (𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))) ≫
          𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))) ≫
            CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)) :
      Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
        (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
        (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (𝟙 (Functor.obj N₂ P) :
      Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Functor.obj N₂ P) (Functor.obj N₂ P))

Tactic:
rw [Γ₂.map_id, N₂.map_id, comp_id, id_comp, id_comp, identity_N₂_objectwise P]

Premises used: AlgebraicTopology.DoldKan.Γ₂, AlgebraicTopology.DoldKan.N₂, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, AlgebraicTopology.DoldKan.identity_N₂_objectwise, CategoryTheory.Category.id_comp