-- 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
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))
⊢ 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))
have 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))
Tactic: rw [Γ₂.map_id, N₂.map_id, comp_id, id_comp, id_comp, identity_N₂_objectwise P]