C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (((λ_ (𝟙_ C)).inv ⊗ 𝟙 (M.X ⊗ N.X)) ≫ ((M.one ⊗ N.one) ⊗ 𝟙 (M.X ⊗ N.X))) ≫
      tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) =
    (λ_ (M.X ⊗ N.X)).hom
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one) ⊗ 𝟙 (M.X ⊗ N.X)) ≫ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) =
    (λ_ (M.X ⊗ N.X)).hom
rw [← Category.id_comp (𝟙 (M.X ⊗ N.X)), tensor_comp]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (M.X ⊗ N.X)) ≫
      (tensor_μ C (tensorUnit', 𝟙_ C) (M.X, N.X) ≫ ((M.one ⊗ 𝟙 M.X) ⊗ N.one ⊗ 𝟙 N.X)) ≫ (M.mul ⊗ N.mul) =
    (λ_ (M.X ⊗ N.X)).hom
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (((λ_ (𝟙_ C)).inv ⊗ 𝟙 (M.X ⊗ N.X)) ≫ ((M.one ⊗ N.one) ⊗ 𝟙 (M.X ⊗ N.X))) ≫
      tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) =
    (λ_ (M.X ⊗ N.X)).hom
slice_lhs 2 3 => rw [← tensor_id, tensor_μ_natural]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (M.X ⊗ N.X)) ≫ tensor_μ C (tensorUnit', 𝟙_ C) (M.X, N.X) ≫ ((λ_ M.X).hom ⊗ (λ_ N.X).hom) =
    (λ_ (M.X ⊗ N.X)).hom
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (M.X ⊗ N.X)) ≫
      (tensor_μ C (tensorUnit', 𝟙_ C) (M.X, N.X) ≫ ((M.one ⊗ 𝟙 M.X) ⊗ N.one ⊗ 𝟙 N.X)) ≫ (M.mul ⊗ N.mul) =
    (λ_ (M.X ⊗ N.X)).hom
slice_lhs 3 4 => rw [← tensor_comp, one_mul M, one_mul N]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (λ_ (M.X ⊗ N.X)).hom =
    ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (M.X ⊗ N.X)) ≫ tensor_μ C (tensorUnit', 𝟙_ C) (M.X, N.X) ≫ ((λ_ M.X).hom ⊗ (λ_ N.X).hom)
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (M.X ⊗ N.X)) ≫ tensor_μ C (tensorUnit', 𝟙_ C) (M.X, N.X) ≫ ((λ_ M.X).hom ⊗ (λ_ N.X).hom) =
    (λ_ (M.X ⊗ N.X)).hom
symm
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (λ_ (M.X ⊗ N.X)).hom =
    ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (M.X ⊗ N.X)) ≫ tensor_μ C (tensorUnit', 𝟙_ C) (M.X, N.X) ≫ ((λ_ M.X).hom ⊗ (λ_ N.X).hom)
exact tensor_left_unitality C M.X N.X