awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ (Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂)) ≫
          X₁ ◁ Iso.inv (α_ X₂ Y₁ Y₂) ≫
            X₁ ◁ Iso.hom (β_ X₂ Y₁) ▷ Y₂ ≫
              X₁ ◁ Iso.hom (α_ Y₁ X₂ Y₂) ≫ Iso.inv (α_ X₁ Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂))) ▷
        tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ≫
      (Iso.hom
            (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂)
              (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂)) ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁ Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂) Z₁ Z₂) ≫
            tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁
                (Iso.hom (α_ X₂ Y₂ Z₁) ≫
                    X₂ ◁ Iso.hom (β_ Y₂ Z₁) ≫ Iso.inv (α_ X₂ Z₁ Y₂) ≫ Iso.hom (β_ X₂ Z₁) ▷ Y₂ ≫ Iso.hom (α_ Z₁ X₂ Y₂)) ▷
                  Z₂ ≫
              tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁ Iso.hom (α_ Z₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂) Z₂) ≫
                Iso.inv
                  (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) Z₁
                    (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂) Z₂))) ≫
        (Iso.hom (α_ X₁ Y₁ Z₁) ⊗ₘ Iso.hom (α_ X₂ Y₂ Z₂)) =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁
        (tensorObj.{v₁, u₁} (𝒞 := inst)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₁))
          Z₂))
      (𝟙
        (tensorObj.{v₁, u₁} (𝒞 := inst)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂))
          (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂)))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁
          (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Z₁) Y₂)
              Z₂)))
        (X₁ ◁
          (Iso.hom (β_ X₂ Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₁ ≫
              tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ X₂ ◁ Iso.hom (β_ Y₂ Z₁)) ▷
            Z₂)
        (X₁ ◁ Y₁ ◁ Iso.hom (β_ X₂ Z₁) ▷ Y₂ ▷ Z₂ ⊗≫
          𝟙
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁))
              (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂)))))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁
        (tensorObj.{v₁, u₁} (𝒞 := inst)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₁))
          Z₂))
      (𝟙
        (tensorObj.{v₁, u₁} (𝒞 := inst)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂))
          (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂)))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁
          (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Z₁) Y₂)
              Z₂)))
        (X₁ ◁
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁ ◁ Iso.hom (β_ Y₂ Z₁) ≫
              Iso.hom (β_ X₂ Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Y₂) ▷
            Z₂)
        (X₁ ◁ Y₁ ◁ Iso.hom (β_ X₂ Z₁) ▷ Y₂ ▷ Z₂ ⊗≫
          𝟙
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁))
              (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))))) =
    Iso.hom
        (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂)
          (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂)) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁
          (Iso.hom (α_ Y₁ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂)) ≫
            Y₁ ◁ Iso.inv (α_ Y₂ Z₁ Z₂) ≫
              Y₁ ◁ Iso.hom (β_ Y₂ Z₁) ▷ Z₂ ≫
                Y₁ ◁ Iso.hom (α_ Z₁ Y₂ Z₂) ≫ Iso.inv (α_ Y₁ Z₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))) ≫
        Iso.hom
            (α_ X₁ X₂
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁)
                (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))) ≫
          X₁ ◁ Iso.inv (α_ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂)) ≫
            X₁ ◁
                (Iso.inv (α_ X₂ Y₁ Z₁) ≫
                    Iso.hom (β_ X₂ Y₁) ▷ Z₁ ≫ Iso.hom (α_ Y₁ X₂ Z₁) ≫ Y₁ ◁ Iso.hom (β_ X₂ Z₁) ≫ Iso.inv (α_ Y₁ Z₁ X₂)) ▷
                  tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂ ≫
              X₁ ◁ Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂)) ≫
                Iso.inv
                  (α_ X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁)
                    (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂)))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) (tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C)))
    (ε (tensor C)) (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) (tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C)) ⟶
      tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (η (tensor C)) (Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : C × C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) X)
        (Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) Y) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) X Y))
    (μ (tensor C) X Y) (tensorμ X.1 X.2 Y.1 Y.2)

Tactic:
rfl

Premises used: CategoryTheory.MonoidalCategory.tensorμ, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : C × C
⊢ Eq.{v₁ + 1} (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) X)
        (Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) Y))
    (δ (tensor C) X Y) (tensorδ X.1 X.2 Y.1 Y.2)

Tactic:
rfl

Premises used: CategoryTheory.MonoidalCategory.tensorδ, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ : C
dsimp :
  Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ X₂) =
    (Iso.hom
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
        tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X₂ ≫
            tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁ X₂) ≫
              Iso.inv
                (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                  (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))) ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ≫
        Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))
⊢ Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ X₂) =
    tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ≫
        Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))

Tactic:
dsimp only [tensorμ]

Premises used: CategoryTheory.MonoidalCategory.tensorμ
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ : C
⊢ Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ X₂) =
    Iso.hom
        (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
      tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ≫
        Iso.hom
            (λ_
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
                X₂)) ≫
          Iso.hom (ρ_ X₁) ▷ X₂

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ : C
⊢ Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ X₂) =
    Iso.hom
        (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
      tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ≫
        Iso.hom
            (λ_
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
                X₂)) ≫
          Iso.hom (ρ_ X₁) ▷ X₂

Tactic:
have :
    (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom =
      (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).hom ≫
        (𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).inv) ≫ (λ_ ((X₁ ⊗ 𝟙_ C) ⊗ X₂)).hom ≫ ((ρ_ X₁).hom ▷ X₂) := by
    monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ : C
this :
  Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ X₂) =
    Iso.hom
        (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
      tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ≫
        Iso.hom
            (λ_
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
                X₂)) ≫
          Iso.hom (ρ_ X₁) ▷ X₂
⊢ Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ X₂) =
    (Iso.hom
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
        tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X₂ ≫
            tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁ X₂) ≫
              Iso.inv
                (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                  (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))) ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ≫
        Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))

Tactic:
simp [this]
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ : C
dsimp :
  Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂) =
    (Iso.hom
          (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          X₁ ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            X₁ ◁ Iso.hom (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              Iso.inv
                (α_ X₁ X₂
                  (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                    (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))
⊢ Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂) =
    tensorμ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))

Tactic:
dsimp only [tensorμ]

Premises used: CategoryTheory.MonoidalCategory.tensorμ
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ : C
⊢ Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂) =
    Iso.hom
        (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        X₁ ◁ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫ X₁ ◁ Iso.hom (λ_ X₂)

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ : C
⊢ Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂) =
    Iso.hom
        (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        X₁ ◁ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫ X₁ ◁ Iso.hom (λ_ X₂)

Tactic:
have :
    (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom =
      (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫
        (X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv) ≫ (X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom) ≫ (X₁ ◁ (λ_ X₂).hom) := by
    monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ : C
this :
  Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂) =
    Iso.hom
        (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        X₁ ◁ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫ X₁ ◁ Iso.hom (λ_ X₂)
rw :
  Iso.hom
        (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        X₁ ◁ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
          X₁ ◁ Iso.hom (λ_ X₂) =
    (Iso.hom
          (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          X₁ ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            X₁ ◁ Iso.hom (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              Iso.inv
                (α_ X₁ X₂
                  (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                    (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))
⊢ Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂) =
    (Iso.hom
          (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          X₁ ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            X₁ ◁ Iso.hom (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              Iso.inv
                (α_ X₁ X₂
                  (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                    (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ : C
rw :
  Iso.hom
        (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        X₁ ◁ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
          X₁ ◁ (Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ≫ Iso.hom (ρ_ X₂)) =
    (Iso.hom
          (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          X₁ ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            X₁ ◁ Iso.hom (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              Iso.inv
                (α_ X₁ X₂
                  (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                    (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))
⊢ Iso.hom
        (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        X₁ ◁ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
          X₁ ◁ Iso.hom (λ_ X₂) =
    (Iso.hom
          (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          X₁ ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            X₁ ◁ Iso.hom (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              Iso.inv
                (α_ X₁ X₂
                  (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                    (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))

Tactic:
rw [← braiding_rightUnitor]

Premises used: CategoryTheory.braiding_rightUnitor
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ : C
⊢ Iso.hom
        (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        X₁ ◁ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
          X₁ ◁ (Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ≫ Iso.hom (ρ_ X₂)) =
    (Iso.hom
          (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          X₁ ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            X₁ ◁ Iso.hom (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              Iso.inv
                (α_ X₁ X₂
                  (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                    (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
dsimp :
  (Iso.hom
          (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) X₃
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃)) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.inv (α_ X₃ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃) ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (β_ X₃ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂)) ▷ Y₃ ≫
            tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) X₃ Y₃) ≫
              Iso.inv
                (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂)
                  (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃))) ≫
      (Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂)) ≫
            X₁ ◁ Iso.inv (α_ X₂ Y₁ Y₂) ≫
              X₁ ◁ Iso.hom (β_ X₂ Y₁) ▷ Y₂ ≫
                X₁ ◁ Iso.hom (α_ Y₁ X₂ Y₂) ≫ Iso.inv (α_ X₁ Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂))) ▷
          tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃ ≫
        Iso.hom
          (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂)
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃)) =
    (Iso.hom (α_ X₁ X₂ X₃) ⊗ₘ Iso.hom (α_ Y₁ Y₂ Y₃)) ≫
      (Iso.hom
            (α_ X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃)
              (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃))) ≫
          X₁ ◁ Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
            X₁ ◁ Iso.hom (β_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃ ≫
              X₁ ◁ Iso.hom (α_ Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
                Iso.inv
                  (α_ X₁ Y₁
                    (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃)
                      (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)))) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁
          (Iso.hom (α_ X₂ X₃ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
            X₂ ◁ Iso.inv (α_ X₃ Y₂ Y₃) ≫
              X₂ ◁ Iso.hom (β_ X₃ Y₂) ▷ Y₃ ≫
                X₂ ◁ Iso.hom (α_ Y₂ X₃ Y₃) ≫ Iso.inv (α_ X₂ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃)))
⊢ tensorμ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) X₃ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃ ≫
      tensorμ X₁ X₂ Y₁ Y₂ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃ ≫
        Iso.hom
          (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂)
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃)) =
    (Iso.hom (α_ X₁ X₂ X₃) ⊗ₘ Iso.hom (α_ Y₁ Y₂ Y₃)) ≫
      tensorμ X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁ tensorμ X₂ X₃ Y₂ Y₃

Tactic:
dsimp only [tensorμ]

Premises used: CategoryTheory.MonoidalCategory.tensorμ