Lean4
/-- The unit isomorphism of `equivalence`. -/
@[simps!]
def equivalenceUnitIso : 𝟭 A ≅ (F ⋙ eB.inverse) ⋙ G :=
calc
𝟭 A ≅ eA.functor ⋙ eA.inverse := eA.unitIso
_ ≅ (F ⋙ e'.inverse) ⋙ eA.inverse := (isoWhiskerRight ε _)
_ ≅ F ⋙ e'.inverse ⋙ eA.inverse := (associator _ _ _)
_ ≅ F ⋙ 𝟭 B' ⋙ e'.inverse ⋙ eA.inverse := (isoWhiskerLeft _ (leftUnitor _).symm)
_ ≅ F ⋙ (eB.inverse ⋙ eB.functor) ⋙ e'.inverse ⋙ eA.inverse :=
(isoWhiskerLeft _ (isoWhiskerRight eB.counitIso.symm _))
_ ≅ (F ⋙ eB.inverse ⋙ eB.functor) ⋙ e'.inverse ⋙ eA.inverse := (associator _ _ _).symm
_ ≅ ((F ⋙ eB.inverse) ⋙ eB.functor) ⋙ e'.inverse ⋙ eA.inverse := (isoWhiskerRight (associator _ _ _).symm _)
_ ≅ (F ⋙ eB.inverse) ⋙ eB.functor ⋙ e'.inverse ⋙ eA.inverse := (associator _ _ _)
_ ≅ (F ⋙ eB.inverse) ⋙ (eB.functor ⋙ e'.inverse) ⋙ eA.inverse := (isoWhiskerLeft _ (associator _ _ _).symm)
_ ≅ (F ⋙ eB.inverse) ⋙ (G ⋙ eA.functor) ⋙ eA.inverse := (isoWhiskerLeft _ (isoWhiskerRight hG _))
_ ≅ ((F ⋙ eB.inverse) ⋙ G ⋙ eA.functor) ⋙ eA.inverse := (associator _ _ _).symm
_ ≅ (((F ⋙ eB.inverse) ⋙ G) ⋙ eA.functor) ⋙ eA.inverse := (isoWhiskerRight (associator _ _ _).symm _)
_ ≅ ((F ⋙ eB.inverse) ⋙ G) ⋙ eA.functor ⋙ eA.inverse := (associator _ _ _)
_ ≅ ((F ⋙ eB.inverse) ⋙ G) ⋙ 𝟭 A := (isoWhiskerLeft _ eA.unitIso.symm)
_ ≅ (F ⋙ eB.inverse) ⋙ G := rightUnitor _
