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)) ((fᘁ ⊗ 𝟙 X) ≫ ε_ X Xᘁ) =
    ↑(tensorRightHomEquiv Yᘁ X Xᘁ (𝟙_ C)) ((𝟙 Yᘁ ⊗ f) ≫ ε_ Y Yᘁ)
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ (fᘁ ⊗ 𝟙 X) ≫ ε_ X Xᘁ = (𝟙 Yᘁ ⊗ f) ≫ ε_ Y Yᘁ
apply_fun tensorRightHomEquiv _ X (Xᘁ) _
no goals
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)) ((fᘁ ⊗ 𝟙 X) ≫ ε_ X Xᘁ) =
    ↑(tensorRightHomEquiv Yᘁ X Xᘁ (𝟙_ C)) ((𝟙 Yᘁ ⊗ f) ≫ ε_ Y Yᘁ)
simp