-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
w :
  NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
            (Equivalence.functor Preadditive.DoldKan.equivalence) Γ₂)
          (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (NatTrans.app (Γ₂N₂.natTrans ≫ Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
w₁ :
  NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
            (Equivalence.functor Preadditive.DoldKan.equivalence) Γ₂)
          (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (NatTrans.app (Iso.inv Γ₂N₂ ≫ Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
w₂ :
  NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      NatTrans.app (𝟙 (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂))
          (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) ≫
        Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
w₃ :
  NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      𝟙
          (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂)
            (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
        Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
w₄ :
  NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫ Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
w₅ :
  Functor.map Γ₂ (NatTrans.app (Iso.inv toKaroubiCompN₂IsoN₁) X) ≫
      Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
w₆ :
  Functor.map Γ₂ (NatTrans.app (Iso.inv toKaroubiCompN₂IsoN₁) X ≫ NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
⊢ NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      NatTrans.app Γ₂N₂.natTrans (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) ≫
        CategoryStruct.comp (Y :=
          Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
            (Functor.obj (Equivalence.functor Preadditive.DoldKan.equivalence)
              (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)))
          (NatTrans.app (Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
          (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
have w₇ : Functor.map Γ₂ (𝟙 (Functor.obj N₁ X)) =
  𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
Tactic: rw [← NatTrans.comp_app_assoc, ← Γ₂N₂_inv, Iso.inv_hom_id, NatTrans.id_app, id_comp,
    Γ₂N₂ToKaroubiIso_inv_app, ← Γ₂.map_comp, Iso.inv_hom_id_app, Γ₂.map_id]