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
inst_2 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
simp :
  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 ◁ Iso.hom (β_ Y X) ▷ Y ≫
          X ◁ Iso.hom (β_ X Y) ▷ 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)) ≫ (μ ⊗ₘ μ))
⊢ 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)
    ((tensorμ X Y X Y ≫ (μ ⊗ₘ μ)) ≫ Iso.hom (β_ X Y))
    ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫ tensorμ Y X Y X ≫ (μ ⊗ₘ μ))

Tactic:
simp only [tensorμ, Category.assoc, BraidedCategory.braiding_naturality,
    BraidedCategory.braiding_tensor_right_hom, BraidedCategory.braiding_tensor_left_hom,
    comp_whiskerRight, whisker_assoc, whiskerLeft_comp, pentagon_assoc,
    pentagon_inv_hom_hom_hom_inv_assoc, Iso.inv_hom_id_assoc, whiskerLeft_hom_inv_assoc]

Premises used: CategoryTheory.BraidedCategory.braiding_tensor_right_hom, CategoryTheory.Category.assoc, CategoryTheory.BraidedCategory.braiding_tensor_left_hom, CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_inv_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.BraidedCategory.braiding_naturality, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.MonoidalCategory.tensorμ, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv_assoc, CategoryTheory.MonoidalCategory.whisker_assoc, CategoryTheory.MonoidalCategory.pentagon_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
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
a : X ◁ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) ▷ Y
| X ◁ Iso.hom (β_ Y X) ▷ Y ≫ X ◁ Iso.hom (β_ X Y) ▷ Y

Tactic:
rw [← whiskerLeft_comp, ← comp_whiskerRight, SymmetricCategory.symmetry]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.SymmetricCategory.symmetry
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
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
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)) ≫
      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)) ≫ (μ ⊗ₘ μ))
⊢ 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 ◁ Iso.hom (β_ Y X) ▷ Y ≫
          X ◁ Iso.hom (β_ X Y) ▷ 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)) ≫ (μ ⊗ₘ μ))

Tactic:
slice_lhs 3 4 =>
    -- We use symmetry here:
    rw [← whiskerLeft_comp, ← comp_whiskerRight, SymmetricCategory.symmetry]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.SymmetricCategory.symmetry
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
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
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)) ≫ (μ ⊗ₘ μ)
⊢ 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)) ≫ (μ ⊗ₘ μ))

Tactic:
simp only [id_whiskerRight, whiskerLeft_id, Category.id_comp, Category.assoc, pentagon_inv_assoc,
    Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.id_whiskerRight, CategoryTheory.MonoidalCategory.pentagon_inv_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_id, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
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
a : Iso.hom (β_ X Y) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≫ Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y)
| Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) X Y) ≫ Iso.hom (β_ X Y) ▷ X ▷ Y

Tactic:
rw [← associator_inv_naturality_left]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_left
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
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
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)) ≫ (μ ⊗ₘ μ))
⊢ 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:
slice_lhs 1 2 =>
    rw [← associator_inv_naturality_left]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_left
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
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
a : 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) (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)

Tactic:
rw [Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
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
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)) ≫ (μ ⊗ₘ μ))
⊢ 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 2 3 =>
    rw [Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
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
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)) ≫ (μ ⊗ₘ μ))
⊢ 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:
rw [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
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
a : tensorObj.{v₁, u₁} (𝒞 := inst) Y X ◁ Iso.hom (β_ X Y) ≫ Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
| Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫ Y ◁ X ◁ Iso.hom (β_ X Y)

Tactic:
rw [← associator_naturality_right]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_right
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
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
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)) ≫ (μ ⊗ₘ μ)
⊢ 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:
slice_lhs 2 3 =>
    rw [← associator_naturality_right]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_right
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
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
a : Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)
| Iso.hom (β_ X Y) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≫ tensorObj.{v₁, u₁} (𝒞 := inst) Y X ◁ Iso.hom (β_ X Y)

Tactic:
rw [← 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
inst_2 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
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)) ≫ (μ ⊗ₘ μ))
⊢ 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 1 2 =>
    rw [← 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
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) ⊗ₘ 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:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
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
inst_5 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_6 : MonObj X
inst_7 : MonObj Y
⊢ IsMonHom.{v₁, u₁} (M := tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (Iso.hom (β_ X Y))

Tactic:
⟨one_braiding X Y, mul_braiding X Y⟩

Premises used: CategoryTheory.IsMonHom.mk, CategoryTheory.MonObj.one_braiding, CategoryTheory.MonObj.mul_braiding
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : SymmetricCategory.{v₁, u₁} C
M N : Mon.{v₁, u₁} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) M N).X ⟶ (tensorObj (𝒞 := instCategory) N M).X) (Hom.hom (Iso.hom (β_ M N)))
    (Iso.hom (β_ M.X N.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : SymmetricCategory.{v₁, u₁} C
M N : Mon.{v₁, u₁} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) N M).X ⟶ (tensorObj (𝒞 := instCategory) M N).X) (Hom.hom (Iso.inv (β_ M N)))
    (Iso.inv (β_ M.X N.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
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) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (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)))

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp