-- 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
⊢ 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 ℕ))))
have 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)
Tactic: ext K : 3