case mk'
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
functor✝ : C ⥤ D
inverse✝ : D ⥤ C
unitIso✝ : 𝟭 C ≅ functor✝ ⋙ inverse✝
counitIso✝ : inverse✝ ⋙ functor✝ ≅ 𝟭 D
functor_unitIso_comp✝ :
  ∀ (X : C), functor✝.map (unitIso✝.hom.app X) ≫ counitIso✝.hom.app (functor✝.obj X) = 𝟙 (functor✝.obj X)
⊢ asEquivalence (mk' functor✝ inverse✝ unitIso✝ counitIso✝).functor = mk' functor✝ inverse✝ unitIso✝ counitIso✝
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
E : C ≌ D
⊢ asEquivalence E.functor = E
cases E
no goals
case mk'
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
functor✝ : C ⥤ D
inverse✝ : D ⥤ C
unitIso✝ : 𝟭 C ≅ functor✝ ⋙ inverse✝
counitIso✝ : inverse✝ ⋙ functor✝ ≅ 𝟭 D
functor_unitIso_comp✝ :
  ∀ (X : C), functor✝.map (unitIso✝.hom.app X) ≫ counitIso✝.hom.app (functor✝.obj X) = 𝟙 (functor✝.obj X)
⊢ asEquivalence (mk' functor✝ inverse✝ unitIso✝ counitIso✝).functor = mk' functor✝ inverse✝ unitIso✝ counitIso✝
congr