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
inst_2 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    (Iso.hom (α_ X Y (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
      X ◁ Iso.inv (α_ Y X Y) ≫
        ((((((((((X ◁ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) ▷ Y ≫
                              Iso.inv (α_ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) Y)) ≫
                            Iso.inv (α_ X Y X) ▷ Y) ≫
                          Iso.hom (β_ X Y) ▷ X ▷ Y) ≫
                        Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y)) ≫
                      Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))) ≫
                    Y ◁ X ◁ Iso.hom (β_ X Y)) ≫
                  Y ◁ Iso.inv (α_ X Y X)) ≫
                Y ◁ Iso.hom (β_ X Y) ▷ X) ≫
              Y ◁ Iso.hom (α_ Y X X)) ≫
            Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X))) ≫
          (μ ⊗ₘ μ))
    ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
      Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
        Y ◁ Iso.inv (α_ X Y X) ≫
          Y ◁ Iso.hom (β_ X Y) ▷ X ≫
            Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ))
have simp : Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) X Y) ≫
    Iso.hom (β_ X Y) ▷ X ▷ Y ≫
      Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y) ≫
        Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
          Y ◁ X ◁ Iso.hom (β_ X Y) ≫
            Y ◁ Iso.inv (α_ X Y X) ≫
              Y ◁ Iso.hom (β_ X Y) ▷ X ≫
                Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ) =
  (Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
    Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
      Y ◁ Iso.inv (α_ X Y X) ≫
        Y ◁ Iso.hom (β_ X Y) ▷ X ≫
          Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ)
Tactic: simp only [id_whiskerRight, whiskerLeft_id, Category.id_comp, Category.assoc, pentagon_inv_assoc,
    Iso.hom_inv_id_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 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
| Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) X Y) ≫ Iso.hom (β_ X Y) ▷ X ▷ Y
have a : Iso.hom (β_ X Y) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≫ Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y)
Tactic: rw [← associator_inv_naturality_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 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
⊢ Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) X Y) ≫
      Iso.hom (β_ X Y) ▷ X ▷ Y ≫
        Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y) ≫
          Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
            Y ◁ X ◁ Iso.hom (β_ X Y) ≫
              Y ◁ Iso.inv (α_ X Y X) ≫
                Y ◁ Iso.hom (β_ X Y) ▷ X ≫
                  Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ) =
    (Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
      Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
        Y ◁ Iso.inv (α_ X Y X) ≫
          Y ◁ Iso.hom (β_ X Y) ▷ X ≫
            Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ)
have slice_lhs : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
  (((((((((Iso.hom (β_ X Y) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≫
                    Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y)) ≫
                  Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y)) ≫
                Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))) ≫
              Y ◁ X ◁ Iso.hom (β_ X Y)) ≫
            Y ◁ Iso.inv (α_ X Y X)) ≫
          Y ◁ Iso.hom (β_ X Y) ▷ X) ≫
        Y ◁ Iso.hom (α_ Y X X)) ≫
      Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X))) ≫
    (μ ⊗ₘ μ))
  ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
    Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
      Y ◁ Iso.inv (α_ X Y X) ≫
        Y ◁ Iso.hom (β_ X Y) ▷ X ≫
          Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ))
Tactic: slice_lhs 1 2 =>
    rw [← associator_inv_naturality_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 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
| Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y) ≫ Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y)
have a : 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
Tactic: rw [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
inst_2 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    (((((((((Iso.hom (β_ X Y) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≫
                      Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y)) ≫
                    Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y)) ≫
                  Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))) ≫
                Y ◁ X ◁ Iso.hom (β_ X Y)) ≫
              Y ◁ Iso.inv (α_ X Y X)) ≫
            Y ◁ Iso.hom (β_ X Y) ▷ X) ≫
          Y ◁ Iso.hom (α_ Y X X)) ≫
        Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X))) ≫
      (μ ⊗ₘ μ))
    ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
      Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
        Y ◁ Iso.inv (α_ X Y X) ≫
          Y ◁ Iso.hom (β_ X Y) ▷ X ≫
            Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ))
have slice_lhs : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
  (Iso.hom (β_ X Y) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≫
    ((((((𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
                  Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))) ≫
                Y ◁ X ◁ Iso.hom (β_ X Y)) ≫
              Y ◁ Iso.inv (α_ X Y X)) ≫
            Y ◁ Iso.hom (β_ X Y) ▷ X) ≫
          Y ◁ Iso.hom (α_ Y X X)) ≫
        Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X))) ≫
      (μ ⊗ₘ μ))
  ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
    Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
      Y ◁ Iso.inv (α_ X Y X) ≫
        Y ◁ Iso.hom (β_ X Y) ▷ X ≫
          Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ))
Tactic: slice_lhs 2 3 =>
    rw [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
inst_2 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    (Iso.hom (β_ X Y) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≫
      ((((((𝟙
                      (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
                        (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
                    Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))) ≫
                  Y ◁ X ◁ Iso.hom (β_ X Y)) ≫
                Y ◁ Iso.inv (α_ X Y X)) ≫
              Y ◁ Iso.hom (β_ X Y) ▷ X) ≫
            Y ◁ Iso.hom (α_ Y X X)) ≫
          Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X))) ≫
        (μ ⊗ₘ μ))
    ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
      Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
        Y ◁ Iso.inv (α_ X Y X) ≫
          Y ◁ Iso.hom (β_ X Y) ▷ X ≫
            Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ))
have rw : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
  (Iso.hom (β_ X Y) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≫
    (((((Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫ Y ◁ X ◁ Iso.hom (β_ X Y)) ≫ Y ◁ Iso.inv (α_ X Y X)) ≫
            Y ◁ Iso.hom (β_ X Y) ▷ X) ≫
          Y ◁ Iso.hom (α_ Y X X)) ≫
        Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X))) ≫
      (μ ⊗ₘ μ))
  ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
    Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
      Y ◁ Iso.inv (α_ X Y X) ≫
        Y ◁ Iso.hom (β_ X Y) ▷ X ≫
          Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ))
Tactic: rw [Category.id_comp]
-- 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 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
| Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫ Y ◁ X ◁ Iso.hom (β_ X Y)
have a : tensorObj.{v₁, u₁} (𝒞 := inst) Y X ◁ Iso.hom (β_ X Y) ≫ Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
Tactic: rw [← associator_naturality_right]
-- 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 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    (Iso.hom (β_ X Y) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≫
      (((((Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫ Y ◁ X ◁ Iso.hom (β_ X Y)) ≫ Y ◁ Iso.inv (α_ X Y X)) ≫
              Y ◁ Iso.hom (β_ X Y) ▷ X) ≫
            Y ◁ Iso.hom (α_ Y X X)) ≫
          Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X))) ≫
        (μ ⊗ₘ μ))
    ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
      Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
        Y ◁ Iso.inv (α_ X Y X) ≫
          Y ◁ Iso.hom (β_ X Y) ▷ X ≫
            Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ))
have slice_lhs : Iso.hom (β_ X Y) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≫
    (((((tensorObj.{v₁, u₁} (𝒞 := inst) Y X ◁ Iso.hom (β_ X Y) ≫
                Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))) ≫
              Y ◁ Iso.inv (α_ X Y X)) ≫
            Y ◁ Iso.hom (β_ X Y) ▷ X) ≫
          Y ◁ Iso.hom (α_ Y X X)) ≫
        Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X))) ≫
      (μ ⊗ₘ μ) =
  (Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
    Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
      Y ◁ Iso.inv (α_ X Y X) ≫
        Y ◁ Iso.hom (β_ X Y) ▷ X ≫
          Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ)
Tactic: slice_lhs 2 3 =>
    rw [← associator_naturality_right]
-- 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 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
| Iso.hom (β_ X Y) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≫ tensorObj.{v₁, u₁} (𝒞 := inst) Y X ◁ Iso.hom (β_ X Y)
have a : Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)
Tactic: rw [← tensorHom_def]
-- 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 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
⊢ Iso.hom (β_ X Y) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≫
      (((((tensorObj.{v₁, u₁} (𝒞 := inst) Y X ◁ Iso.hom (β_ X Y) ≫
                  Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))) ≫
                Y ◁ Iso.inv (α_ X Y X)) ≫
              Y ◁ Iso.hom (β_ X Y) ▷ X) ≫
            Y ◁ Iso.hom (α_ Y X X)) ≫
          Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X))) ≫
        (μ ⊗ₘ μ) =
    (Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
      Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
        Y ◁ Iso.inv (α_ X Y X) ≫
          Y ◁ Iso.hom (β_ X Y) ▷ X ≫
            Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ)
have slice_lhs : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
  (((((((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫ Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))) ≫
            Y ◁ Iso.inv (α_ X Y X)) ≫
          Y ◁ Iso.hom (β_ X Y) ▷ X) ≫
        Y ◁ Iso.hom (α_ Y X X)) ≫
      Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X))) ≫
    (μ ⊗ₘ μ))
  ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
    Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
      Y ◁ Iso.inv (α_ X Y X) ≫
        Y ◁ Iso.hom (β_ X Y) ▷ X ≫
          Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ))
Tactic: slice_lhs 1 2 =>
    rw [← tensorHom_def]
-- 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 O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxMonoidal
inst_10 : F'.LaxMonoidal
inst_11 : G.LaxMonoidal
X Y : C
inst_12 : MonObj X
inst_13 : MonObj Y
f : X ⟶ Y
inst_14 : IsMonHom f
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (F.obj X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) («μ» F X X) (F.map μ) ▷ F.obj X ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) («μ» F X X) (F.map μ))
    (Iso.hom (α_ (F.obj X) (F.obj X) (F.obj X)) ≫
      F.obj X ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) («μ» F X X) (F.map μ) ≫
        CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) («μ» F X X) (F.map μ))
have simp_rw : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (F.obj X) ⟶ F.obj X)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.obj X))
    («μ» F X X ▷ F.obj X)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X))
      («μ» F (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X) (F.map (μ ▷ X) ≫ F.map μ)))
  (Iso.hom (α_ (F.obj X) (F.obj X) (F.obj X)) ≫
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
      (F.obj X ◁ «μ» F X X)
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
        («μ» F X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.map (X ◁ μ) ≫ F.map μ)))
Tactic: simp_rw [comp_whiskerRight, Category.assoc, μ_natural_left_assoc,
      MonoidalCategory.whiskerLeft_comp, Category.assoc, μ_natural_right_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
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxMonoidal
inst_10 : F'.LaxMonoidal
inst_11 : G.LaxMonoidal
X Y : C
inst_12 : MonObj X
inst_13 : MonObj Y
f : X ⟶ Y
inst_14 : IsMonHom f
| F.map (μ ▷ X) ≫ F.map μ
have a : F.map (Iso.hom (α_ X X X) ≫ X ◁ μ ≫ μ)
Tactic: rw [← F.map_comp, MonObj.mul_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
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxMonoidal
inst_10 : F'.LaxMonoidal
inst_11 : G.LaxMonoidal
X Y : C
inst_12 : MonObj X
inst_13 : MonObj Y
f : X ⟶ Y
inst_14 : IsMonHom f
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (F.obj X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.obj X))
      («μ» F X X ▷ F.obj X)
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X))
        («μ» F (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X) (F.map (μ ▷ X) ≫ F.map μ)))
    (Iso.hom (α_ (F.obj X) (F.obj X) (F.obj X)) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
        (F.obj X ◁ «μ» F X X)
        (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
          («μ» F X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.map (X ◁ μ) ≫ F.map μ)))
have slice_lhs : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (F.obj X) ⟶ F.obj X)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.obj X))
    («μ» F X X ▷ F.obj X) («μ» F (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X ≫ F.map (Iso.hom (α_ X X X) ≫ X ◁ μ ≫ μ)))
  (Iso.hom (α_ (F.obj X) (F.obj X) (F.obj X)) ≫
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
      (F.obj X ◁ «μ» F X X)
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
        («μ» F X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.map (X ◁ μ) ≫ F.map μ)))
Tactic: slice_lhs 3 4 => rw [← F.map_comp, MonObj.mul_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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
M : Mon.{v₂, u₂} D
N : C
e : F.obj N ≅ M.X
this_1 : MonObj (F.obj N) := MonObj.ofIso e.symm
this : MonObj N := (FullyFaithful.ofFullyFaithful F).monObj N
⊢ essImage (C := Mon.{v₁, u₁} C) F.mapMon M
have refine_1 : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ M.X) (η ≫ e.hom) η
Tactic: refine ⟨.mk N, ⟨Mon.mkIso e ?_ ?_⟩⟩
-- 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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
M : Mon.{v₂, u₂} D
N : C
e : F.obj N ≅ M.X
this_1 : MonObj (F.obj N) := MonObj.ofIso e.symm
this : MonObj N := (FullyFaithful.ofFullyFaithful F).monObj N
refine_1 : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ M.X) (η ≫ e.hom) η
⊢ essImage (C := Mon.{v₁, u₁} C) F.mapMon M
have refine_2 : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (Mon.X (obj (C := Mon.{v₁, u₁} C) F.mapMon { X := N, mon := this : Mon.{v₁, u₁} C }))
      (Mon.X (obj (C := Mon.{v₁, u₁} C) F.mapMon { X := N, mon := this : Mon.{v₁, u₁} C })) ⟶
    M.X)
  (μ ≫ e.hom) ((e.hom ⊗ₘ e.hom) ≫ μ)
Tactic: refine ⟨.mk N, ⟨Mon.mkIso e ?_ ?_⟩⟩
-- 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_1 N_1 O X : C
inst_2 : MonObj M_1
inst_3 : MonObj N_1
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : SymmetricCategory.{v₁, u₁} C
inst_10 : SymmetricCategory.{v₂, u₂} D
inst_11 : F.LaxBraided
M N : Mon.{v₁, u₁} C
⊢ Eq (α :=
    Quiver.Hom (V := Mon.{v₂, u₂} D) (tensorObj (𝒞 := Mon.instCategory) (obj F.mapMon M) (obj F.mapMon N))
      (obj F.mapMon (tensorObj (𝒞 := Mon.instCategory) N M)))
    («μ» F.mapMon M N ≫ map F.mapMon (Iso.hom (β_ M N)))
    (Iso.hom (β_ (obj F.mapMon M) (obj F.mapMon N)) ≫ «μ» F.mapMon N M)
have w : Eq (α :=
  Mon.X (tensorObj (𝒞 := Mon.instCategory) (obj F.mapMon M) (obj F.mapMon N)) ⟶
    Mon.X (obj F.mapMon (tensorObj (𝒞 := Mon.instCategory) N M)))
  (Mon.Hom.hom («μ» F.mapMon M N ≫ map F.mapMon (Iso.hom (β_ M N))))
  (Mon.Hom.hom (Iso.hom (β_ (obj F.mapMon M) (obj F.mapMon N)) ≫ «μ» F.mapMon N M))
Tactic: ext
-- 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 O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : BraidedCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ μ) μ
have dsimp : Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
    Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
  Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
Tactic: dsimp
-- 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 O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : BraidedCategory.{v₁, u₁} C
⊢ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
have rw : Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) = Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
Tactic: rw [braiding_leftUnitor, unitors_equal]