-- 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
w :
  ∀ (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)
⊢ Eq (α :=
    Iso (C := ChainComplex.{v_1, u_1, 0} C ℕ ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
        Equivalence.inverse Preadditive.DoldKan.equivalence ⋙ Equivalence.functor Preadditive.DoldKan.equivalence)
      (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))))
    (Compatibility.τ₀ :
      Iso (C := ChainComplex.{v_1, u_1, 0} C ℕ ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
        (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
          Equivalence.inverse Preadditive.DoldKan.equivalence ⋙ Equivalence.functor Preadditive.DoldKan.equivalence)
        (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))))
    (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₁Γ₀ :
      Iso (C := ChainComplex.{v_1, u_1, 0} C ℕ ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
        (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
          Equivalence.inverse Preadditive.DoldKan.equivalence ⋙ Equivalence.functor Preadditive.DoldKan.equivalence)
        (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ))))

Tactic:
ext K : 3