case w.w.h
A : Type u_4
A' : Type u_5
B : Type u_1
B' : Type u_6
inst✝³ : Category A
inst✝² : Category A'
inst✝¹ : Category B
inst✝ : Category 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
Y' : B
⊢ (equivalence₂ eB hF).counitIso.hom.app Y' = (equivalence₂CounitIso eB hF).hom.app Y'
A : Type u_4
A' : Type u_5
B : Type u_1
B' : Type u_6
inst✝³ : Category A
inst✝² : Category A'
inst✝¹ : Category B
inst✝ : Category 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
⊢ (equivalence₂ eB hF).counitIso = equivalence₂CounitIso eB hF
ext Y'
case w.w.h
A : Type u_4
A' : Type u_5
B : Type u_1
B' : Type u_6
inst✝³ : Category A
inst✝² : Category A'
inst✝¹ : Category B
inst✝ : Category 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
Y' : B
⊢ eB.inverse.map ((equivalence₁ hF).counitIso.hom.app (eB.functor.obj Y')) ≫ eB.unitIso.inv.app Y' =
    (equivalence₂CounitIso eB hF).hom.app Y'
case w.w.h
A : Type u_4
A' : Type u_5
B : Type u_1
B' : Type u_6
inst✝³ : Category A
inst✝² : Category A'
inst✝¹ : Category B
inst✝ : Category 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
Y' : B
⊢ (equivalence₂ eB hF).counitIso.hom.app Y' = (equivalence₂CounitIso eB hF).hom.app Y'
dsimp [equivalence₂, Iso.refl]
no goals
case w.w.h
A : Type u_4
A' : Type u_5
B : Type u_1
B' : Type u_6
inst✝³ : Category A
inst✝² : Category A'
inst✝¹ : Category B
inst✝ : Category 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
Y' : B
⊢ eB.inverse.map ((equivalence₁ hF).counitIso.hom.app (eB.functor.obj Y')) ≫ eB.unitIso.inv.app Y' =
    (equivalence₂CounitIso eB hF).hom.app Y'
simp only [equivalence₁CounitIso_eq, equivalence₂CounitIso_hom_app,
  equivalence₁CounitIso_hom_app, Functor.map_comp, assoc]