-- 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
K : ChainComplex.{v_1, u_1, 0} C ℕ
⊢ Eq (α :=
    Functor.obj
        (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
          Equivalence.inverse Preadditive.DoldKan.equivalence ⋙ Equivalence.functor Preadditive.DoldKan.equivalence)
        K ⟶
      Functor.obj (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))) K)
    (NatTrans.app (Iso.hom Compatibility.τ₀) K :
      Functor.obj
          (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
            Equivalence.inverse Preadditive.DoldKan.equivalence ⋙ Equivalence.functor Preadditive.DoldKan.equivalence)
          K ⟶
        Functor.obj (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))) K)
    (NatTrans.app
        (Iso.hom
          (Compatibility.τ₁ (eA := toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C))
            (isoN₁ :
              Iso (C := SimplicialObject.{v_1, u_1} C ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C)) ⋙
                  Equivalence.functor Preadditive.DoldKan.equivalence)
                N₁)
            (G := Γ)
            (isoΓ₀ :
              Iso (C := ChainComplex.{v_1, u_1, 0} C ℕ ⥤ Karoubi (SimplicialObject.{v_1, u_1} C))
                (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
                  Equivalence.inverse Preadditive.DoldKan.equivalence)
                (Γ ⋙ Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C))))
            N₁Γ₀))
        K :
      Functor.obj
          (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
            Equivalence.inverse Preadditive.DoldKan.equivalence ⋙ Equivalence.functor Preadditive.DoldKan.equivalence)
          K ⟶
        Functor.obj (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))) K)
have w : Eq (α :=
  Functor.obj
      (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
        Equivalence.inverse Preadditive.DoldKan.equivalence ⋙ Equivalence.functor Preadditive.DoldKan.equivalence)
      K ⟶
    Functor.obj (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))) K)
  (NatTrans.app (Iso.hom (Equivalence.counitIso Preadditive.DoldKan.equivalence))
      (Functor.obj (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))) K) :
    Functor.obj
        (Equivalence.inverse Preadditive.DoldKan.equivalence ⋙ Equivalence.functor Preadditive.DoldKan.equivalence)
        (Functor.obj (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))) K) ⟶
      Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
        (Functor.obj (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))) K))
  (Functor.map (Equivalence.functor Preadditive.DoldKan.equivalence) (NatTrans.app (Iso.hom isoΓ₀) K) ≫
    NatTrans.app (Iso.hom isoN₁) (Functor.obj Γ K) ≫ NatTrans.app (Iso.hom N₁Γ₀) K)
Tactic: simp only [Compatibility.τ₀_hom_app, Compatibility.τ₁_hom_app]