case mk'
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (Funit.hom.app X) ≫ Fcounit.hom.app (F.obj X) = 𝟙 (F.obj X)
⊢ ofIso (Iso.refl F) (mk' Finv Funit Fcounit) = mk' Finv Funit Fcounit
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
hF : IsEquivalence F
⊢ ofIso (Iso.refl F) hF = hF
rcases hF with ⟨Finv, Funit, Fcounit, Fcomp⟩
case mk'
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (Funit.hom.app X) ≫ Fcounit.hom.app (F.obj X) = 𝟙 (F.obj X)
⊢ mk' Finv (Funit ≪≫ hcomp (Iso.refl F) (Iso.refl Finv)) (hcomp (Iso.refl Finv) (Iso.refl F) ≪≫ Fcounit) =
    mk' Finv Funit Fcounit
case mk'
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (Funit.hom.app X) ≫ Fcounit.hom.app (F.obj X) = 𝟙 (F.obj X)
⊢ ofIso (Iso.refl F) (mk' Finv Funit Fcounit) = mk' Finv Funit Fcounit
dsimp [ofIso]
case mk'.e_unitIso.w.w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (Funit.hom.app X) ≫ Fcounit.hom.app (F.obj X) = 𝟙 (F.obj X)
X : C
⊢ Funit.hom.app X ≫ 𝟙 (Finv.obj (F.obj X)) ≫ Finv.map (𝟙 (F.obj X)) = Funit.hom.app X

case mk'.e_counitIso.w.w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (Funit.hom.app X) ≫ Fcounit.hom.app (F.obj X) = 𝟙 (F.obj X)
X : D
⊢ (𝟙 (F.obj (Finv.obj X)) ≫ F.map (𝟙 (Finv.obj X))) ≫ Fcounit.hom.app X = Fcounit.hom.app X
case mk'
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (Funit.hom.app X) ≫ Fcounit.hom.app (F.obj X) = 𝟙 (F.obj X)
⊢ mk' Finv (Funit ≪≫ hcomp (Iso.refl F) (Iso.refl Finv)) (hcomp (Iso.refl Finv) (Iso.refl F) ≪≫ Fcounit) =
    mk' Finv Funit Fcounit
congr 1 <;> ext X <;> dsimp [NatIso.hcomp]
no goals
case mk'.e_unitIso.w.w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (Funit.hom.app X) ≫ Fcounit.hom.app (F.obj X) = 𝟙 (F.obj X)
X : C
⊢ Funit.hom.app X ≫ 𝟙 (Finv.obj (F.obj X)) ≫ Finv.map (𝟙 (F.obj X)) = Funit.hom.app X
simp only [comp_id, map_id]
no goals
case mk'.e_counitIso.w.w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (Funit.hom.app X) ≫ Fcounit.hom.app (F.obj X) = 𝟙 (F.obj X)
X : D
⊢ (𝟙 (F.obj (Finv.obj X)) ≫ F.map (𝟙 (Finv.obj X))) ≫ Fcounit.hom.app X = Fcounit.hom.app X
simp only [id_comp, map_id]