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