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