awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X Y : C
inst_2 : MonObj M
e : M ≅ X
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.inv (ρ_ X))
      (X ◁ (η ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.inv (ρ_ X))
      (Iso.hom (ρ_ X))
have simp : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.inv (ρ_ X))
    (X ◁ η ≫ e.inv ▷ M ≫ μ ≫ e.hom) =
  𝟙 X
Tactic: simp only [MonoidalCategory.whiskerLeft_comp, tensorHom_def', Category.assoc,
      whiskerLeft_hom_inv_assoc, Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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) μ μ
this : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η
⊢ h₁ = h₂
have mk : ∀ (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) η η),
  { one := one, mul := mul, one_mul := one_mul, mul_one := mul_one, mul_assoc := mul_assoc : MonObj X } = h₂
Tactic: cases h₁
Cleared hypotheses: h₁, H, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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) η η
⊢ { one := one, mul := mul, one_mul := one_mul, mul_one := mul_one, mul_assoc := mul_assoc : MonObj X } = h₂
have 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 }
Tactic: cases h₂
Cleared hypotheses: h₂, H, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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) η η
⊢ { 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 }
have 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 }
Tactic: subst H this
Cleared hypotheses: one_1, mul_1, one_mul_1, mul_one_1, mul_assoc_1, H, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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) μ μ
⊢ h₁ = h₂
have suffices : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η
Tactic: suffices h₁.one = h₂.one by cases h₁; cases h₂; subst H this; rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η
have 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)))) ((η ⊗ₘ η) ≫ μ))
Tactic: trans (λ_ _).inv ≫ (h₁.one ⊗ₘ h₂.one) ≫ h₁.mul
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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)))) ((η ⊗ₘ η) ≫ μ))
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η
have 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)))) ((η ⊗ₘ η) ≫ μ))
  η
Tactic: trans (λ_ _).inv ≫ (h₁.one ⊗ₘ h₂.one) ≫ h₁.mul
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Z ⟶ M) ((η ⊗ₘ f) ≫ μ) (Iso.hom (λ_ Z) ≫ f)
have rw : tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f ≫ η ▷ M ≫ μ = Iso.hom (λ_ Z) ≫ f
Tactic: rw [tensorHom_def'_assoc, one_mul, leftUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Z ⟶ M) ((η ⊗ₘ f) ≫ μ) (Iso.hom (λ_ Z) ≫ f)
have rw₁ : tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f ≫ Iso.hom (λ_ M) = Iso.hom (λ_ Z) ≫ f
Tactic: rw [tensorHom_def'_assoc, one_mul, leftUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Z ⟶ M) ((η ⊗ₘ f) ≫ μ) (Iso.hom (λ_ Z) ≫ f)
have rw₂ : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Z ⟶ M) (Iso.hom (λ_ Z) ≫ f)
  (Iso.hom (λ_ Z) ≫ f)
Tactic: rw [tensorHom_def'_assoc, one_mul, leftUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ M) ((f ⊗ₘ η) ≫ μ) (Iso.hom (ρ_ Z) ≫ f)
have rw : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ M)
  (f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ M ◁ η ≫ μ) (Iso.hom (ρ_ Z) ≫ f)
Tactic: rw [tensorHom_def_assoc, mul_one, rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ M) ((f ⊗ₘ η) ≫ μ) (Iso.hom (ρ_ Z) ≫ f)
have 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)
Tactic: rw [tensorHom_def_assoc, mul_one, rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ M) ((f ⊗ₘ η) ≫ μ) (Iso.hom (ρ_ Z) ≫ f)
have rw₂ : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ M) (Iso.hom (ρ_ Z) ≫ f)
  (Iso.hom (ρ_ Z) ≫ f)
Tactic: rw [tensorHom_def_assoc, mul_one, rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ (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))) ≫ (η ⊗ₘ η))
have 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))) ≫ (η ⊗ₘ η))
Tactic: simp only [Category.assoc, Iso.cancel_iso_inv_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
| (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η) ⊗ₘ η) ≫ Iso.hom (α_ M N P)
have rw : ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ ((η ⊗ₘ η) ⊗ₘ η)) ≫
  Iso.hom (α_ M N P)
Tactic: rw [← Category.id_comp (η : 𝟙_ C ⟶ P), ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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 (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η) ⊗ₘ η) ≫ Iso.hom (α_ M N P))
    (η ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have 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))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 1 3 => rw [← Category.id_comp (η : 𝟙_ C ⟶ P), ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
| ((η ⊗ₘ η) ⊗ₘ η) ≫ Iso.hom (α_ M N P)
have a : Iso.hom
    (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
  (η ⊗ₘ η ⊗ₘ η)
Tactic: rw [associator_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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 (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ ((η ⊗ₘ η) ⊗ₘ η)) ≫
      Iso.hom (α_ M N P))
    (η ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have 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))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 2 3 => rw [associator_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
| η ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)
have rw : (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗ₘ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫ (η ⊗ₘ η ⊗ₘ η)
Tactic: rw [← Category.id_comp η, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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 (λ_ (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))) ≫ (η ⊗ₘ η))
have 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)))) ≫ (η ⊗ₘ η ⊗ₘ η))
Tactic: slice_rhs 1 2 => rw [← Category.id_comp η, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
| (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)))
have a : Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
Tactic: rw [tensorHom_id, ← leftUnitor_tensor_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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 (λ_ (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)))) ≫ (η ⊗ₘ η ⊗ₘ η))
have 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)))) ≫ (η ⊗ₘ η ⊗ₘ η))
Tactic: slice_lhs 1 2 => rw [tensorHom_id, ← leftUnitor_tensor_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M N : C
inst_3 : MonObj M
inst_4 : MonObj N
⊢ (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫
      tensorμ M N M N ≫ (μ ⊗ₘ μ) =
    Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N))
have simp : Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫
    (η ⊗ₘ η) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) =
  Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N))
Tactic: simp only [comp_whiskerRight_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M N : C
inst_3 : MonObj M
inst_4 : MonObj N
| (η ⊗ₘ η) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫ tensorμ M N M N
have a : tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M N ≫ (η ▷ M ⊗ₘ η ▷ N)
Tactic: rw [tensorμ_natural_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M N : C
inst_3 : MonObj M
inst_4 : MonObj N
⊢ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫
      (η ⊗ₘ η) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) =
    Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N))
have slice_lhs : Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫
    (tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M N ≫ (η ▷ M ⊗ₘ η ▷ N)) ≫
      (μ ⊗ₘ μ) =
  Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N))
Tactic: slice_lhs 2 3 => rw [tensorμ_natural_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M N : C
inst_3 : MonObj M
inst_4 : MonObj N
| (η ▷ M ⊗ₘ η ▷ N) ≫ (μ ⊗ₘ μ)
have a : Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ N)
Tactic: rw [tensorHom_comp_tensorHom, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M N : C
inst_3 : MonObj M
inst_4 : MonObj N
⊢ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫
      (tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M N ≫ (η ▷ M ⊗ₘ η ▷ N)) ≫
        (μ ⊗ₘ μ) =
    Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N))
have slice_lhs : Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫
    tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M N ≫
      (Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ N)) =
  Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N))
Tactic: slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M N : C
inst_3 : MonObj M
inst_4 : MonObj N
⊢ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫
      tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M N ≫
        (Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ N)) =
    Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N))
have symm : Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N)) =
  Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫
    tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M N ≫
      (Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ N))
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M N : C
inst_3 : MonObj M
inst_4 : MonObj N
⊢ tensorObj.{v₁, u₁} (𝒞 := inst) M N ◁ (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)) ≫
      tensorμ M N M N ≫ (μ ⊗ₘ μ) =
    Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N))
have simp : tensorObj.{v₁, u₁} (𝒞 := inst) M N ◁ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
    tensorObj.{v₁, u₁} (𝒞 := inst) M N ◁ (η ⊗ₘ η) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) =
  Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N))
Tactic: simp only [whiskerLeft_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M N : C
inst_3 : MonObj M
inst_4 : MonObj N
| tensorObj.{v₁, u₁} (𝒞 := inst) M N ◁ (η ⊗ₘ η) ≫ tensorμ M N M N
have a : tensorμ M N (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ (M ◁ η ⊗ₘ N ◁ η)
Tactic: rw [tensorμ_natural_right]