C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (λ_ Y).inv ≫ (η_ (ᘁZ) Z ⊗ 𝟙 Y) ≫ (α_ (ᘁZ) Z Y).hom ≫ (𝟙 ᘁZ ⊗ (𝟙 Z ⊗ f) ≫ ε_ (ᘁZ) Z) = f ≫ (ρ_ ᘁZ).inv
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ ↑(tensorLeftHomEquiv Y (ᘁZ) Z (𝟙_ C)) ((𝟙 Z ⊗ f) ≫ ε_ (ᘁZ) Z) = f ≫ (ρ_ ᘁZ).inv
dsimp [tensorLeftHomEquiv]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (λ_ Y).inv ≫ (η_ (ᘁZ) Z ⊗ 𝟙 Y) ≫ (α_ (ᘁZ) Z Y).hom ≫ (𝟙 ᘁZ ⊗ 𝟙 Z ⊗ f) ≫ (𝟙 ᘁZ ⊗ ε_ (ᘁZ) Z) = f ≫ (ρ_ ᘁZ).inv
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (λ_ Y).inv ≫ (η_ (ᘁZ) Z ⊗ 𝟙 Y) ≫ (α_ (ᘁZ) Z Y).hom ≫ (𝟙 ᘁZ ⊗ (𝟙 Z ⊗ f) ≫ ε_ (ᘁZ) Z) = f ≫ (ρ_ ᘁZ).inv
rw [id_tensor_comp]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (λ_ Y).inv ≫ (η_ (ᘁZ) Z ⊗ 𝟙 Y) ≫ (((𝟙 ᘁZ ⊗ 𝟙 Z) ⊗ f) ≫ (α_ (ᘁZ) Z ᘁZ).hom) ≫ (𝟙 ᘁZ ⊗ ε_ (ᘁZ) Z) = f ≫ (ρ_ ᘁZ).inv
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (λ_ Y).inv ≫ (η_ (ᘁZ) Z ⊗ 𝟙 Y) ≫ (α_ (ᘁZ) Z Y).hom ≫ (𝟙 ᘁZ ⊗ 𝟙 Z ⊗ f) ≫ (𝟙 ᘁZ ⊗ ε_ (ᘁZ) Z) = f ≫ (ρ_ ᘁZ).inv
slice_lhs 3 4 => rw [← associator_naturality]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (λ_ Y).inv ≫ (((𝟙 tensorUnit' ⊗ f) ≫ (η_ (ᘁZ) Z ⊗ 𝟙 ᘁZ)) ≫ (α_ (ᘁZ) Z ᘁZ).hom) ≫ (𝟙 ᘁZ ⊗ ε_ (ᘁZ) Z) = f ≫ (ρ_ ᘁZ).inv
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (λ_ Y).inv ≫ (η_ (ᘁZ) Z ⊗ 𝟙 Y) ≫ (((𝟙 ᘁZ ⊗ 𝟙 Z) ⊗ f) ≫ (α_ (ᘁZ) Z ᘁZ).hom) ≫ (𝟙 ᘁZ ⊗ ε_ (ᘁZ) Z) = f ≫ (ρ_ ᘁZ).inv
slice_lhs 2 3 => rw [tensor_id, tensor_id_comp_id_tensor, ← id_tensor_comp_tensor_id]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (λ_ Y).inv ≫ (𝟙 tensorUnit' ⊗ f) ≫ (λ_ ᘁZ).hom ≫ (ρ_ ᘁZ).inv = f ≫ (ρ_ ᘁZ).inv
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (λ_ Y).inv ≫ (((𝟙 tensorUnit' ⊗ f) ≫ (η_ (ᘁZ) Z ⊗ 𝟙 ᘁZ)) ≫ (α_ (ᘁZ) Z ᘁZ).hom) ≫ (𝟙 ᘁZ ⊗ ε_ (ᘁZ) Z) = f ≫ (ρ_ ᘁZ).inv
slice_lhs 3 5 => rw [evaluation_coevaluation]
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (λ_ Y).inv ≫ (𝟙 tensorUnit' ⊗ f) ≫ (λ_ ᘁZ).hom ≫ (ρ_ ᘁZ).inv = f ≫ (ρ_ ᘁZ).inv
simp