awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
h₂ : MonObj X
one : tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X
mul : tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X
one_mul : one ▷ X ≫ mul = Iso.hom (λ_ X)
mul_one : X ◁ one ≫ mul = Iso.hom (ρ_ X)
mul_assoc : mul ▷ X ≫ mul = Iso.hom (α_ X X X) ≫ X ◁ mul ≫ mul
H : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ
this : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η
mk :
  ∀ (one_1 : tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) (mul_1 : tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X)
    (one_mul_1 : one_1 ▷ X ≫ mul_1 = Iso.hom (λ_ X)) (mul_one_1 : X ◁ one_1 ≫ mul_1 = Iso.hom (ρ_ X))
    (mul_assoc_1 : mul_1 ▷ X ≫ mul_1 = Iso.hom (α_ X X X) ≫ X ◁ mul_1 ≫ mul_1)
    (H : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ)
    (this : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η),
    { one := one, mul := mul, one_mul := one_mul, mul_one := mul_one, mul_assoc := mul_assoc : MonObj X } =
      { one := one_1, mul := mul_1, one_mul := one_mul_1, mul_one := mul_one_1, mul_assoc := mul_assoc_1 }
⊢ { one := one, mul := mul, one_mul := one_mul, mul_one := mul_one, mul_assoc := mul_assoc : MonObj X } = h₂

Tactic:
cases h₂
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
one : tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X
mul : tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X
one_mul : one ▷ X ≫ mul = Iso.hom (λ_ X)
mul_one : X ◁ one ≫ mul = Iso.hom (ρ_ X)
mul_assoc : mul ▷ X ≫ mul = Iso.hom (α_ X X X) ≫ X ◁ mul ≫ mul
one_1 : tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X
mul_1 : tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X
one_mul_1 : one_1 ▷ X ≫ mul_1 = Iso.hom (λ_ X)
mul_one_1 : X ◁ one_1 ≫ mul_1 = Iso.hom (ρ_ X)
mul_assoc_1 : mul_1 ▷ X ≫ mul_1 = Iso.hom (α_ X X X) ≫ X ◁ mul_1 ≫ mul_1
H : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ
this : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η
mk :
  ∀
    (mul_assoc_2 :
      Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X ⟶ X) (μ ▷ X ≫ μ)
        (Iso.hom (α_ X X X) ≫ X ◁ μ ≫ μ))
    (one_mul_2 :
      Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶ X) (η ▷ X ≫ μ)
        (Iso.hom (λ_ X)))
    (mul_one_2 :
      Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ X) (X ◁ η ≫ μ)
        (Iso.hom (ρ_ X))),
    { one := one, mul := mul, one_mul := one_mul, mul_one := mul_one, mul_assoc := mul_assoc : MonObj X } =
      { one := η, mul := μ, one_mul := one_mul_2, mul_one := mul_one_2, mul_assoc := mul_assoc_2 }
⊢ { one := one, mul := mul, one_mul := one_mul, mul_one := mul_one, mul_assoc := mul_assoc : MonObj X } =
    { one := one_1, mul := mul_1, one_mul := one_mul_1, mul_one := mul_one_1, mul_assoc := mul_assoc_1 }

Tactic:
subst H this
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
one : tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X
mul : tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X
one_mul : one ▷ X ≫ mul = Iso.hom (λ_ X)
mul_one : X ◁ one ≫ mul = Iso.hom (ρ_ X)
mul_assoc : mul ▷ X ≫ mul = Iso.hom (α_ X X X) ≫ X ◁ mul ≫ mul
mul_assoc_1 :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X ⟶ X) (μ ▷ X ≫ μ)
    (Iso.hom (α_ X X X) ≫ X ◁ μ ≫ μ)
one_mul_1 :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶ X) (η ▷ X ≫ μ)
    (Iso.hom (λ_ X))
mul_one_1 :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ X) (X ◁ η ≫ μ)
    (Iso.hom (ρ_ X))
⊢ { one := one, mul := mul, one_mul := one_mul, mul_one := mul_one, mul_assoc := mul_assoc : MonObj X } =
    { one := η, mul := μ, one_mul := one_mul_1, mul_one := mul_one_1, mul_assoc := mul_assoc_1 }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : MonObj X
H : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ
suffices : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η
⊢ h₁ = h₂

Tactic:
suffices h₁.one = h₂.one by cases h₁; cases h₂; subst H this; rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : MonObj X
H : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ
trans :
  Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ((η ⊗ₘ η) ≫ μ))
trans₁ :
  Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X)
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ((η ⊗ₘ η) ≫ μ))
    η
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η

Tactic:
trans (λ_ _).inv ≫ (h₁.one ⊗ₘ h₂.one) ≫ h₁.mul

Premises used: CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.MonObj.one, CategoryTheory.MonoidalCategoryStruct.tensorHom, CategoryTheory.Iso.inv, CategoryTheory.MonObj.mul
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : MonObj X
H : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ((η ⊗ₘ η) ≫ μ))

Tactic:
simp [tensorHom_def, H, ← unitors_equal]

Premises used: CategoryTheory.MonoidalCategory.unitors_equal, CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : MonObj X
H : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X)
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ((η ⊗ₘ η) ≫ μ))
    η

Tactic:
simp [tensorHom_def']

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def'
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h : Z₁ ⟶ Z₂
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) Z₁ ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))
    (Iso.hom (α_ X₁ Y₁ Z₁) ≫ (f ⊗ₘ g ⊗ₘ h)) (((f ⊗ₘ g) ⊗ₘ h) ≫ Iso.hom (α_ X₂ Y₂ Z₂))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h : Z₁ ⟶ Z₂
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂) Z₂)
    (Iso.inv (α_ X₁ Y₁ Z₁) ≫ ((f ⊗ₘ g) ⊗ₘ h)) ((f ⊗ₘ g ⊗ₘ h) ≫ Iso.inv (α_ X₂ Y₂ Z₂))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h : Z₁ ⟶ Z₂
gh : tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂ ⟶ W
⊢ Iso.hom (α_ X₁ Y₁ Z₁) ≫ (f ⊗ₘ (g ⊗ₘ h) ≫ gh) = ((f ⊗ₘ g) ⊗ₘ h) ≫ Iso.hom (α_ X₂ Y₂ Z₂) ≫ (𝟙 X₂ ⊗ₘ gh)

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h : Z₁ ⟶ Z₂
fg : tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂ ⟶ W
⊢ Iso.inv (α_ X₁ Y₁ Z₁) ≫ ((f ⊗ₘ g) ≫ fg ⊗ₘ h) = (f ⊗ₘ g ⊗ₘ h) ≫ Iso.inv (α_ X₂ Y₂ Z₂) ≫ (fg ⊗ₘ 𝟙 Z₂)

Tactic:
simp [tensorHom_def']

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def'
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ⟶ M) (Iso.hom (λ_ M))
    ((η ⊗ₘ 𝟙 M) ≫ μ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ M) (Iso.hom (ρ_ M))
    ((𝟙 M ⊗ₘ η) ≫ μ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X₁ : C
inst_2 : MonObj M
f : X₁ ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁) (Iso.inv (λ_ X₁))
      ((η ⊗ₘ f) ≫ μ) =
    f

Tactic:
simp [tensorHom_def']

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def'
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X₁ : C
inst_2 : MonObj M
f : X₁ ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.inv (ρ_ X₁))
      ((f ⊗ₘ η) ≫ μ) =
    f

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X : C
inst_2 : MonObj M
f : X ⟶ M
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X M) M ⟶ M)
    (Iso.hom (α_ X M M) ≫ (f ⊗ₘ μ) ≫ μ) (((f ⊗ₘ 𝟙 M) ≫ μ ⊗ₘ 𝟙 M) ≫ μ)

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X : C
inst_2 : MonObj M
f : X ⟶ M
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorObj.{v₁, u₁} (𝒞 := inst) M X) ⟶ M)
    (Iso.inv (α_ M M X) ≫ (μ ⊗ₘ f) ≫ μ) ((𝟙 M ⊗ₘ (𝟙 M ⊗ₘ f) ≫ μ) ≫ μ)

Tactic:
simp [tensorHom_def']

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def'
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
e : M ≅ X
this : MonObj X := MonObj.ofIso e
⊢ IsMonHom e.hom

Tactic:

Premises used: CategoryTheory.IsMonHom.mk
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
e : M ≅ X
this : MonObj X := MonObj.ofIso e
⊢ IsMonHom e.hom

Tactic:
exact { }
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
f : M ≅ N
inst_5 : IsMonHom f.hom
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ M) (η ≫ f.inv) η

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
f : M ≅ N
inst_5 : IsMonHom f.hom
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) N N ⟶ M) (μ ≫ f.inv) ((f.inv ⊗ₘ f.inv) ≫ μ)

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
Z : C
f : Z ⟶ M
rw : tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f ≫ η ▷ M ≫ μ = Iso.hom (λ_ Z) ≫ f
rw₁ : tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f ≫ Iso.hom (λ_ M) = Iso.hom (λ_ Z) ≫ f
rw₂ rw₃ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Z ⟶ M) (Iso.hom (λ_ Z) ≫ f)
    (Iso.hom (λ_ Z) ≫ f)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Z ⟶ M) ((η ⊗ₘ f) ≫ μ) (Iso.hom (λ_ Z) ≫ f)

Tactic:
rw [tensorHom_def'_assoc, one_mul, leftUnitor_naturality]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_naturality, CategoryTheory.MonoidalCategory.tensorHom_def'_assoc, CategoryTheory.MonObj.one_mul
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
Z : C
f : Z ⟶ M
rw :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ M)
    (f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ M ◁ η ≫ μ) (Iso.hom (ρ_ Z) ≫ f)
rw₁ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ M)
    (f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ Iso.hom (ρ_ M)) (Iso.hom (ρ_ Z) ≫ f)
rw₂ rw₃ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ M) (Iso.hom (ρ_ Z) ≫ f)
    (Iso.hom (ρ_ Z) ≫ f)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ M) ((f ⊗ₘ η) ≫ μ) (Iso.hom (ρ_ Z) ≫ f)

Tactic:
rw [tensorHom_def_assoc, mul_one, rightUnitor_naturality]

Premises used: CategoryTheory.MonObj.mul_one, CategoryTheory.MonoidalCategory.rightUnitor_naturality, CategoryTheory.MonoidalCategory.tensorHom_def_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ⟶ M) (M ◁ μ ≫ μ)
    (Iso.inv (α_ M M M) ≫ μ ▷ M ≫ μ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N P : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj P
simp :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P))
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η) ⊗ₘ η) ≫ Iso.hom (α_ M N P))
    (η ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
⊢ (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η) ⊗ₘ η)) ≫
      Iso.hom (α_ M N P) =
    Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      (η ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.cancel_iso_inv_left
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N P : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj P
rw :
  ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ ((η ⊗ₘ η) ⊗ₘ η)) ≫
    Iso.hom (α_ M N P)
| (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η) ⊗ₘ η) ≫ Iso.hom (α_ M N P)

Tactic:
rw [← Category.id_comp (η : 𝟙_ C ⟶ P), ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.MonObj.one, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N P : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj P
slice_lhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P))
    (((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ ((η ⊗ₘ η) ⊗ₘ η)) ≫
      Iso.hom (α_ M N P))
    (η ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P))
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η) ⊗ₘ η) ≫ Iso.hom (α_ M N P))
    (η ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
slice_lhs 1 3 => rw [← Category.id_comp (η : 𝟙_ C ⟶ P), ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.MonObj.one, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N P : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj P
a :
  Iso.hom
      (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
    (η ⊗ₘ η ⊗ₘ η)
| ((η ⊗ₘ η) ⊗ₘ η) ≫ Iso.hom (α_ M N P)

Tactic:
rw [associator_naturality]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N P : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj P
slice_lhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P))
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        (η ⊗ₘ η ⊗ₘ η))
    (η ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P))
    (((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ ((η ⊗ₘ η) ⊗ₘ η)) ≫
      Iso.hom (α_ M N P))
    (η ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
slice_lhs 2 3 => rw [associator_naturality]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N P : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj P
rw : (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫ (η ⊗ₘ η ⊗ₘ η)
| η ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)

Tactic:
rw [← Category.id_comp η, ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.MonObj.one, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N P : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj P
slice_rhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P))
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        (η ⊗ₘ η ⊗ₘ η))
    ((𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫ (η ⊗ₘ η ⊗ₘ η))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P))
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        (η ⊗ₘ η ⊗ₘ η))
    (η ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
slice_rhs 1 2 => rw [← Category.id_comp η, ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.MonObj.one, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N P : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj P
a :
  Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
| (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
    Iso.hom
      (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
rw [tensorHom_id, ← leftUnitor_tensor_inv]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv, CategoryTheory.MonoidalCategory.tensorHom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N P : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj P
slice_lhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P))
    (Iso.inv
        (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      (η ⊗ₘ η ⊗ₘ η))
    ((𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫ (η ⊗ₘ η ⊗ₘ η))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P))
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        (η ⊗ₘ η ⊗ₘ η))
    ((𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫ (η ⊗ₘ η ⊗ₘ η))

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

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv, CategoryTheory.MonoidalCategory.tensorHom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N P : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj P
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P))
    (Iso.inv
        (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      (η ⊗ₘ η ⊗ₘ η))
    ((𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫ (η ⊗ₘ η ⊗ₘ η))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
⊢ (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗ₘ η)) ≫ Iso.hom (λ_ M) = η

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
⊢ (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫ Iso.hom (ρ_ M) = η

Tactic:
simp [← unitors_equal]

Premises used: CategoryTheory.MonoidalCategory.unitors_equal