Lean4
/-- The isomorphism `eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor` deduced
from the isomorphisms `hF : eA.functor ⋙ e'.functor ≅ F`,
`hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor` and the datum of
an isomorphism `η : G ⋙ F ≅ eB.functor`. -/
@[simps! hom_app]
def τ₁ (η : G ⋙ F ≅ eB.functor) : eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor :=
calc
eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ (eB.functor ⋙ e'.inverse) ⋙ e'.functor := (associator _ _ _).symm
_ ≅ (G ⋙ eA.functor) ⋙ e'.functor := (isoWhiskerRight hG _)
_ ≅ G ⋙ eA.functor ⋙ e'.functor := (associator _ _ _)
_ ≅ G ⋙ F := (isoWhiskerLeft _ hF)
_ ≅ eB.functor := η