C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ (tensor_μ C (𝟙_ C, M.X) (𝟙_ C, M.X) ≫ ((λ_ (𝟙_ C)).hom ⊗ 𝟙 (M.X ⊗ M.X)) ≫ (𝟙 (𝟙_ C) ⊗ M.mul)) ≫ (λ_ M.X).hom =
    ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ (tensor_μ C (𝟙_ C, M.X) (𝟙_ C, M.X) ≫ ((λ_ (𝟙_ C)).hom ⊗ M.mul)) ≫ (λ_ M.X).hom =
    ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ M.mul
rw [← Category.comp_id (λ_ (𝟙_ C)).hom, ← Category.id_comp M.mul, tensor_comp]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ tensor_μ C (𝟙_ C, M.X) (𝟙_ C, M.X) ≫ ((λ_ (𝟙_ C)).hom ⊗ 𝟙 (M.X ⊗ M.X)) ≫ (λ_ (M.X ⊗ M.X)).hom ≫ M.mul =
    ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ (tensor_μ C (𝟙_ C, M.X) (𝟙_ C, M.X) ≫ ((λ_ (𝟙_ C)).hom ⊗ 𝟙 (M.X ⊗ M.X)) ≫ (𝟙 (𝟙_ C) ⊗ M.mul)) ≫ (λ_ M.X).hom =
    ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
slice_lhs 3 4 => rw [leftUnitor_naturality]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ M.mul = ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ tensor_μ C (𝟙_ C, M.X) (𝟙_ C, M.X) ≫ ((λ_ (𝟙_ C)).hom ⊗ 𝟙 (M.X ⊗ M.X)) ≫ (λ_ (M.X ⊗ M.X)).hom ≫ M.mul =
    ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
slice_lhs 1 3 => rw [← leftUnitor_monoidal]
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ M.mul = ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
simp only [Category.assoc, Category.id_comp]