-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem one_associator {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))

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ (λ_ (𝟙_ C ⊗ 𝟙_ C)).inv ≫ (M.one ⊗ N.one ⊗ P.one) = (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)

Tactic:
rw [← cancel_epi (λ_ (𝟙_ C)).inv]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ (λ_ (𝟙_ C)).inv ≫ (λ_ (𝟙_ C ⊗ 𝟙_ C)).inv ≫ (M.one ⊗ N.one ⊗ P.one) =
    (λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ≫ (M.one ⊗ N.one ⊗ P.one) =
    (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)

Tactic:
slice_lhs 1 2 => rw [tensorHom_id, ← leftUnitor_tensor_inv]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ (λ_ (𝟙_ C ⊗ 𝟙_ C)).inv ≫ (M.one ⊗ N.one ⊗ P.one) = (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ≫ 𝟙_ C ◁ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one) =
    (λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ (λ_ (𝟙_ C)).inv ≫ (λ_ (𝟙_ C ⊗ 𝟙_ C)).inv ≫ (M.one ⊗ N.one ⊗ P.one) =
    (λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)

Tactic:
slice_lhs 1 2 => rw [leftUnitor_inv_naturality]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ≫ 𝟙_ C ◁ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one) =
    (λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} 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)

Tactic:
slice_lhs 2 3 => rw [associator_naturality]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ≫ (M.one ⊗ N.one ⊗ P.one) =
    M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ≫ (M.one ⊗ N.one ⊗ P.one) =
    M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one)

Tactic:
slice_rhs 1 2 => rw [← Category.id_comp M.one, tensor_comp]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M N P : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ≫ (M.one ⊗ N.one ⊗ P.one) =
    (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} 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)

Tactic:
slice_lhs 1 3 => rw [← Category.id_comp P.one, tensor_comp]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} 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)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} 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))

Tactic:
simp only [Category.assoc, Iso.cancel_iso_inv_left]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} 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)