-- Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
theorem equivalenceUnitIso_eq (hε : υ hF = ε) :
    (equivalence hF hG).unitIso = equivalenceUnitIso hG ε

Proof state:
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_5, u_2} A'
inst✝¹ : Category.{u_8, u_3} B
inst✝ : Category.{u_7, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ (equivalence₂ eB hF).unitIso.hom.app X ≫
      ((𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj (eB.inverse.obj (F.obj X))))) ≫
            eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X)))) ≫
          eA.unitIso.inv.app (G.obj (eB.inverse.obj (F.obj X)))) ≫
        𝟙 (G.obj (eB.inverse.obj (F.obj X))) =
    (equivalenceUnitIso hG ε).hom.app X

Tactic:
simp only [assoc, comp_id, equivalenceUnitIso_hom_app, equivalence₂_inverse, Functor.comp_obj,
  id_comp, equivalence₂UnitIso_eq eB hF, equivalence₂UnitIso_hom_app,
  ← eA.inverse.map_comp_assoc, assoc, ← hε, υ_hom_app]

Result:
no goals

Proof state:
case w.app
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_5, u_2} A'
inst✝¹ : Category.{u_8, u_3} B
inst✝ : Category.{u_7, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
⊢ (equivalence hF hG).unitIso.hom.app = (equivalenceUnitIso hG ε).hom.app

Tactic:
ext X

Result:
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_5, u_2} A'
inst✝¹ : Category.{u_8, u_3} B
inst✝ : Category.{u_7, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ (equivalence hF hG).unitIso.hom.app X = (equivalenceUnitIso hG ε).hom.app X

Proof state:
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_5, u_2} A'
inst✝¹ : Category.{u_8, u_3} B
inst✝ : Category.{u_7, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ (equivalence hF hG).unitIso.hom.app X = (equivalenceUnitIso hG ε).hom.app X

Tactic:
dsimp [equivalence]

Result:
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_5, u_2} A'
inst✝¹ : Category.{u_8, u_3} B
inst✝ : Category.{u_7, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ (equivalence₂ eB hF).unitIso.hom.app X ≫
      ((𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj (eB.inverse.obj (F.obj X))))) ≫
            eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X)))) ≫
          eA.unitIso.inv.app (G.obj (eB.inverse.obj (F.obj X)))) ≫
        𝟙 (G.obj (eB.inverse.obj (F.obj X))) =
    (equivalenceUnitIso hG ε).hom.app X

Proof state:
case w
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_5, u_2} A'
inst✝¹ : Category.{u_8, u_3} B
inst✝ : Category.{u_7, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
⊢ (equivalence hF hG).unitIso.hom = (equivalenceUnitIso hG ε).hom

Tactic:
apply NatTrans.ext

Result:
case w.app
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_5, u_2} A'
inst✝¹ : Category.{u_8, u_3} B
inst✝ : Category.{u_7, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
⊢ (equivalence hF hG).unitIso.hom.app = (equivalenceUnitIso hG ε).hom.app

Proof state:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_5, u_2} A'
inst✝¹ : Category.{u_8, u_3} B
inst✝ : Category.{u_7, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
⊢ (equivalence hF hG).unitIso = equivalenceUnitIso hG ε

Tactic:
ext1

Result:
case w
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_5, u_2} A'
inst✝¹ : Category.{u_8, u_3} B
inst✝ : Category.{u_7, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
⊢ (equivalence hF hG).unitIso.hom = (equivalenceUnitIso hG ε).hom