C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ ((𝟙 (M.X ⊗ N.X) ⊗ (λ_ (𝟙_ C)).inv) ≫ (𝟙 (M.X ⊗ N.X) ⊗ M.one ⊗ N.one)) ≫
      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
⊢ (𝟙 (M.X ⊗ N.X) ⊗ (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one)) ≫ 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
⊢ (𝟙 (M.X ⊗ N.X) ⊗ (λ_ (𝟙_ C)).inv) ≫
      (tensor_μ C (M.X, N.X) (tensorUnit', 𝟙_ C) ≫ ((𝟙 M.X ⊗ M.one) ⊗ 𝟙 N.X ⊗ N.one)) ≫ (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
⊢ ((𝟙 (M.X ⊗ N.X) ⊗ (λ_ (𝟙_ C)).inv) ≫ (𝟙 (M.X ⊗ N.X) ⊗ M.one ⊗ N.one)) ≫
      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
⊢ (𝟙 (M.X ⊗ N.X) ⊗ (λ_ (𝟙_ C)).inv) ≫ tensor_μ C (M.X, N.X) (tensorUnit', 𝟙_ C) ≫ ((ρ_ 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
⊢ (𝟙 (M.X ⊗ N.X) ⊗ (λ_ (𝟙_ C)).inv) ≫
      (tensor_μ C (M.X, N.X) (tensorUnit', 𝟙_ C) ≫ ((𝟙 M.X ⊗ M.one) ⊗ 𝟙 N.X ⊗ N.one)) ≫ (M.mul ⊗ N.mul) =
    (ρ_ (M.X ⊗ N.X)).hom
slice_lhs 3 4 => rw [← tensor_comp, mul_one M, mul_one N]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (ρ_ (M.X ⊗ N.X)).hom =
    (𝟙 (M.X ⊗ N.X) ⊗ (λ_ (𝟙_ C)).inv) ≫ tensor_μ C (M.X, N.X) (tensorUnit', 𝟙_ C) ≫ ((ρ_ M.X).hom ⊗ (ρ_ N.X).hom)
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (𝟙 (M.X ⊗ N.X) ⊗ (λ_ (𝟙_ C)).inv) ≫ tensor_μ C (M.X, N.X) (tensorUnit', 𝟙_ C) ≫ ((ρ_ 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 =
    (𝟙 (M.X ⊗ N.X) ⊗ (λ_ (𝟙_ C)).inv) ≫ tensor_μ C (M.X, N.X) (tensorUnit', 𝟙_ C) ≫ ((ρ_ M.X).hom ⊗ (ρ_ N.X).hom)
exact tensor_right_unitality C M.X N.X