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