-- Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean
theorem hε :
    Compatibility.υ (isoN₁) =
      (Γ₂N₁ : (toKaroubiEquivalence _).functor ≅
          (N₁ : SimplicialObject C ⥤ _) ⋙ Preadditive.DoldKan.equivalence.inverse)

Proof state:
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ (Γ₂N₁.inv ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom).app X = (𝟙 (N₁ ⋙ Γ₂)).app X

Tactic:
rw [NatTrans.comp_app, Γ₂N₁_inv, compatibility_Γ₂N₁_Γ₂N₂_natTrans X, Compatibility.υ_hom_app,
  Preadditive.DoldKan.equivalence_unitIso, Iso.app_inv, assoc]

Result:
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₂ToKaroubiIso.inv.app X ≫
      Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X) ≫
        Γ₂N₂.hom.app ((toKaroubiEquivalence (SimplicialObject C)).functor.obj X) ≫
          Preadditive.DoldKan.equivalence.inverse.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    (𝟙 (N₁ ⋙ Γ₂)).app X

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.υ isoN₁ = Γ₂N₁

Tactic:
dsimp only [isoN₁]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.υ toKaroubiCompN₂IsoN₁ = Γ₂N₁

Proof state:
case w
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom = Γ₂N₁.hom

Tactic:
rw [← cancel_epi Γ₂N₁.inv, Iso.inv_hom_id]

Result:
case w
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Γ₂N₁.inv ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom = 𝟙 (N₁ ⋙ Γ₂)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.υ toKaroubiCompN₂IsoN₁ = Γ₂N₁

Tactic:
ext1

Result:
case w
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom = Γ₂N₁.hom

Proof state:
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₂ToKaroubiIso.inv.app X ≫
      Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X) ≫
        Γ₂N₂.hom.app ((toKaroubi (SimplicialObject C)).obj X) ≫ Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    𝟙 (Γ₂.obj (N₁.obj 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]

Result:
no goals

Proof state:
case w
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Γ₂N₁.inv ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom = 𝟙 (N₁ ⋙ Γ₂)

Tactic:
ext X : 2

Result:
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ (Γ₂N₁.inv ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom).app X = (𝟙 (N₁ ⋙ Γ₂)).app X

Proof state:
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₂ToKaroubiIso.inv.app X ≫
      Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X) ≫
        Γ₂N₂.hom.app ((toKaroubiEquivalence (SimplicialObject C)).functor.obj X) ≫
          Preadditive.DoldKan.equivalence.inverse.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    (𝟙 (N₁ ⋙ Γ₂)).app X

Tactic:
dsimp only [Functor.comp_obj, Preadditive.DoldKan.equivalence_inverse, Preadditive.DoldKan.Γ.eq_1,
  toKaroubiEquivalence, Functor.asEquivalence_functor, Preadditive.DoldKan.N.eq_1,
  NatTrans.id_app]

Result:
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₂ToKaroubiIso.inv.app X ≫
      Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X) ≫
        Γ₂N₂.hom.app ((toKaroubi (SimplicialObject C)).obj X) ≫ Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    𝟙 (Γ₂.obj (N₁.obj X))