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