-- Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
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 ℕ
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)
⊢ 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)

Tactic:
simp only [Compatibility.τ₀_hom_app, Compatibility.τ₁_hom_app]

Premises used: AlgebraicTopology.DoldKan.Compatibility.τ₁_hom_app, AlgebraicTopology.DoldKan.Compatibility.τ₀_hom_app