C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one) ⊗ P.one) ≫ (α_ M.X N.X P.X).hom = M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one)
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ≫ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one) ⊗ P.one)) ≫ (α_ M.X N.X P.X).hom =
    (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one))
simp
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ (((λ_ (𝟙_ C)).inv ⊗ 𝟙 (𝟙_ C)) ≫ ((M.one ⊗ N.one) ⊗ P.one)) ≫ (α_ M.X N.X P.X).hom =
    M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one)
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one) ⊗ P.one) ≫ (α_ M.X N.X P.X).hom = M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one)
slice_lhs 1 3 => rw [← Category.id_comp P.one, tensor_comp]
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ tensorUnit' (𝟙_ C) (𝟙_ C)).hom ≫ (M.one ⊗ N.one ⊗ P.one) =
    M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one)
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ (((λ_ (𝟙_ C)).inv ⊗ 𝟙 (𝟙_ C)) ≫ ((M.one ⊗ N.one) ⊗ P.one)) ≫ (α_ M.X N.X P.X).hom =
    M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one)
slice_lhs 2 3 => rw [associator_naturality]
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ tensorUnit' (𝟙_ C) (𝟙_ C)).hom ≫ (M.one ⊗ N.one ⊗ P.one) =
    (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ tensorUnit' (𝟙_ C) (𝟙_ C)).hom ≫ (M.one ⊗ N.one ⊗ P.one) =
    M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one)
slice_rhs 1 2 => rw [← Category.id_comp M.one, tensor_comp]
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ (λ_ (tensorUnit' ⊗ 𝟙_ C)).inv ≫ (M.one ⊗ N.one ⊗ P.one) = (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ tensorUnit' (𝟙_ C) (𝟙_ C)).hom ≫ (M.one ⊗ N.one ⊗ P.one) =
    (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)
slice_lhs 1 2 => rw [← leftUnitor_tensor_inv]
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ (λ_ (𝟙_ C)).inv ≫ (λ_ (tensorUnit' ⊗ 𝟙_ C)).inv ≫ (M.one ⊗ N.one ⊗ P.one) =
    (λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ (λ_ (tensorUnit' ⊗ 𝟙_ C)).inv ≫ (M.one ⊗ N.one ⊗ P.one) = (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)
rw [← cancel_epi (λ_ (𝟙_ C)).inv]
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ≫ (𝟙 tensorUnit' ⊗ (λ_ (𝟙_ C)).inv)) ≫ (M.one ⊗ N.one ⊗ P.one) =
    (λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ (λ_ (𝟙_ C)).inv ≫ (λ_ (tensorUnit' ⊗ 𝟙_ C)).inv ≫ (M.one ⊗ N.one ⊗ P.one) =
    (λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)
slice_lhs 1 2 => rw [leftUnitor_inv_naturality]
no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ≫ (𝟙 tensorUnit' ⊗ (λ_ (𝟙_ C)).inv)) ≫ (M.one ⊗ N.one ⊗ P.one) =
    (λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)
simp only [Category.assoc]