C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (λ_ ᘁY).inv ≫ (η_ (ᘁX) X ⊗ 𝟙 ᘁY) ≫ (α_ (ᘁX) X ᘁY).hom ≫ (𝟙 ᘁX ⊗ (f ⊗ 𝟙 ᘁY) ≫ ε_ (ᘁY) Y) =
    ((λ_ ᘁY).inv ≫ (η_ (ᘁX) X ⊗ 𝟙 ᘁY) ≫ ((𝟙 ᘁX ⊗ f) ⊗ 𝟙 ᘁY) ≫ (α_ (ᘁX) Y ᘁY).hom ≫ (𝟙 ᘁX ⊗ ε_ (ᘁY) Y) ≫ (ρ_ ᘁX).hom) ≫
      (ρ_ ᘁX).inv
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ ↑(tensorLeftHomEquiv (ᘁY) (ᘁX) X (𝟙_ C)) ((f ⊗ 𝟙 ᘁY) ≫ ε_ (ᘁY) Y) = (ᘁf) ≫ (ρ_ ᘁX).inv
dsimp [tensorLeftHomEquiv, leftAdjointMate]
no goals
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (λ_ ᘁY).inv ≫ (η_ (ᘁX) X ⊗ 𝟙 ᘁY) ≫ (α_ (ᘁX) X ᘁY).hom ≫ (𝟙 ᘁX ⊗ (f ⊗ 𝟙 ᘁY) ≫ ε_ (ᘁY) Y) =
    ((λ_ ᘁY).inv ≫ (η_ (ᘁX) X ⊗ 𝟙 ᘁY) ≫ ((𝟙 ᘁX ⊗ f) ⊗ 𝟙 ᘁY) ≫ (α_ (ᘁX) Y ᘁY).hom ≫ (𝟙 ᘁX ⊗ ε_ (ᘁY) Y) ≫ (ρ_ ᘁX).hom) ≫
      (ρ_ ᘁX).inv
simp