equivalence₁CounitIso — Mathlib

Lean4
/-- The counit isomorphism of the equivalence `equivalence₁` between `A` and `B'`. -/
@[simps!]
def equivalence₁CounitIso : (e'.inverse ⋙ eA.inverse) ⋙ F ≅ 𝟭 B' :=
  calc
    (e'.inverse ⋙ eA.inverse) ⋙ F ≅ (e'.inverse ⋙ eA.inverse) ⋙ eA.functor ⋙ e'.functor := isoWhiskerLeft _ hF.symm
    _ ≅ e'.inverse ⋙ (eA.inverse ⋙ eA.functor ⋙ e'.functor) := (associator _ _ _)
    _ ≅ e'.inverse ⋙ (eA.inverse ⋙ eA.functor) ⋙ e'.functor := (isoWhiskerLeft _ (associator _ _ _).symm)
    _ ≅ e'.inverse ⋙ 𝟭 _ ⋙ e'.functor := (isoWhiskerLeft _ (isoWhiskerRight eA.counitIso _))
    _ ≅ e'.inverse ⋙ e'.functor := (isoWhiskerLeft _ (leftUnitor _))
    _ ≅ 𝟭 B' := e'.counitIso
Похожие утверждения