C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
X : C
⊢ (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)).hom =
    (Iso.refl (e.functor.obj ((𝟭 C).obj X))).hom
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
X : C
⊢ (counitInv e).app (e.functor.obj X) ≫ e.functor.map ((unitInv e).app X) = 𝟙 (e.functor.obj X)
erw [Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X))
    (Iso.refl _)]
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
e : C ≌ D
X : C
⊢ (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)).hom =
    (Iso.refl (e.functor.obj ((𝟭 C).obj X))).hom
exact e.functor_unit_comp X