C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ ↑(tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (η_ Y Yᘁ ≫ (𝟙 Y ⊗ fᘁ)) =
    ↑(tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (η_ X Xᘁ ≫ (f ⊗ 𝟙 Xᘁ))
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ η_ Y Yᘁ ≫ (𝟙 Y ⊗ fᘁ) = η_ X Xᘁ ≫ (f ⊗ 𝟙 Xᘁ)
apply_fun (tensorLeftHomEquiv _ Y (Yᘁ) _).symm
no goals
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ ↑(tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (η_ Y Yᘁ ≫ (𝟙 Y ⊗ fᘁ)) =
    ↑(tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (η_ X Xᘁ ≫ (f ⊗ 𝟙 Xᘁ))
simp