case w.w.h
A : Type u_4
A' : Type u_5
B : Type ?u.10546
B' : Type u_1
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₁ hF).counitIso.hom.app Y = (equivalence₁CounitIso hF).hom.app Y
A : Type u_4
A' : Type u_5
B : Type ?u.10546
B' : Type u_1
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₁ hF).counitIso = equivalence₁CounitIso hF
ext Y
case w.w.h
A : Type u_4
A' : Type u_5
B : Type ?u.10546
B' : Type u_1
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'
⊢ (Functor.asEquivalence F).counitIso.hom.app Y = (equivalence₁CounitIso hF).hom.app Y
case w.w.h
A : Type u_4
A' : Type u_5
B : Type ?u.10546
B' : Type u_1
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₁ hF).counitIso.hom.app Y = (equivalence₁CounitIso hF).hom.app Y
dsimp [equivalence₁]
case w.w.h
A : Type u_4
A' : Type u_5
B : Type ?u.10546
B' : Type u_1
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.mk' F (IsEquivalence.inverse F) IsEquivalence.unitIso IsEquivalence.counitIso).counitIso.hom.app Y =
    (equivalence₁CounitIso hF).hom.app Y
case w.w.h
A : Type u_4
A' : Type u_5
B : Type ?u.10546
B' : Type u_1
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'
⊢ (Functor.asEquivalence F).counitIso.hom.app Y = (equivalence₁CounitIso hF).hom.app Y
unfold Functor.asEquivalence
case w.w.h
A : Type u_4
A' : Type u_5
B : Type ?u.10546
B' : Type u_1
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'
⊢ IsEquivalence.counitIso.hom.app Y = (equivalence₁CounitIso hF).hom.app Y
case w.w.h
A : Type u_4
A' : Type u_5
B : Type ?u.10546
B' : Type u_1
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.mk' F (IsEquivalence.inverse F) IsEquivalence.unitIso IsEquivalence.counitIso).counitIso.hom.app Y =
    (equivalence₁CounitIso hF).hom.app Y
dsimp [equivalence₀, IsEquivalence.inverse, IsEquivalence.ofEquivalence]
no goals
case w.w.h
A : Type u_4
A' : Type u_5
B : Type ?u.10546
B' : Type u_1
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'
⊢ IsEquivalence.counitIso.hom.app Y = (equivalence₁CounitIso hF).hom.app Y
simp