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