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