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
Z₁ Z₂ X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₂ Y₂))
    (((𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ⊗ₘ f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂) (tensorμ Z₁ Z₂ X₁ X₂ ≫ ((𝟙 Z₁ ⊗ₘ f₁) ⊗ₘ 𝟙 Z₂ ⊗ₘ f₂))

Tactic:
tensorμ_natural (𝟙 Z₁) (𝟙 Z₂) f₁ f₂

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.MonoidalCategory.tensorμ_natural
-- 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
Z₁ Z₂ X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
h :
  tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ◁ (f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂ =
    ((𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ⊗ₘ f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂
h₁ :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₂ Y₂))
    (tensorμ Z₁ Z₂ X₁ X₂ ≫ (Z₁ ◁ f₁ ⊗ₘ Z₂ ◁ f₂)) (tensorμ Z₁ Z₂ X₁ X₂ ≫ ((𝟙 Z₁ ⊗ₘ f₁) ⊗ₘ 𝟙 Z₂ ⊗ₘ f₂))
⊢ tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ◁ (f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂ = tensorμ Z₁ Z₂ X₁ X₂ ≫ (Z₁ ◁ f₁ ⊗ₘ Z₂ ◁ f₂)

Tactic:
convert! tensorμ_natural (𝟙 Z₁) (𝟙 Z₂) f₁ f₂ using 1

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.MonoidalCategory.tensorμ_natural
-- 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
Z₁ Z₂ X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ◁ (f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂ =
    ((𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ⊗ₘ f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂

Tactic:
simp
-- 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
Z₁ Z₂ X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₂ Y₂))
    (tensorμ Z₁ Z₂ X₁ X₂ ≫ (Z₁ ◁ f₁ ⊗ₘ Z₂ ◁ f₂)) (tensorμ Z₁ Z₂ X₁ X₂ ≫ ((𝟙 Z₁ ⊗ₘ f₁) ⊗ₘ 𝟙 Z₂ ⊗ₘ f₂))

Tactic:
simp
-- 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 (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ≫
      (Iso.hom
            (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
              (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁ X₂) ≫
            tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁) ▷ X₂ ≫
              tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ≫
                Iso.inv
                  (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁
                    (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂))) ≫
        (Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ X₂))
⊢ Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ≫
      tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁ X₂ ≫
        (Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ 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.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ≫
      Iso.hom
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) ≫
        tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁ X₂) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (λ_ X₁) ▷ X₂

Tactic:
simp
-- 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.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ≫
      Iso.hom
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) ≫
        tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁ X₂) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (λ_ X₁) ▷ X₂

Tactic:
have :
    ((λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂)) ≫
        (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ (𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv) =
      𝟙_ C ◁ (λ_ X₁).inv ▷ X₂ := by
    simp
-- 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.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ≫
      Iso.hom
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) ≫
        tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁ X₂) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (λ_ X₁) ▷ X₂
a : tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (λ_ X₁) ▷ X₂
| Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ≫
    Iso.hom
        (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) ≫
      tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := 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
this :
  Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ≫
      Iso.hom
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) ≫
        tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁ X₂) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (λ_ X₁) ▷ X₂
slice_rhs :
  Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    (((tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (λ_ X₁) ▷ X₂ ≫
            tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁) ▷ X₂) ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
        Iso.inv
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂))) ≫
      (Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ X₂))
⊢ Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ≫
      (Iso.hom
            (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
              (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁ X₂) ≫
            tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁) ▷ X₂ ≫
              tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ≫
                Iso.inv
                  (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁
                    (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂))) ≫
        (Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ X₂))

Tactic:
slice_rhs 1 3 => 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
a : tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (ρ_ X₁) ▷ X₂
| tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (λ_ X₁) ▷ X₂ ≫
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁) ▷ X₂

Tactic:
rw [← whiskerLeft_comp, ← comp_whiskerRight,
    leftUnitor_inv_braiding]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.leftUnitor_inv_braiding
-- 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
slice_rhs :
  Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    ((tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (ρ_ X₁) ▷ X₂ ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
        Iso.inv
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂))) ≫
      (Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ X₂))
⊢ Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    (((tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (λ_ X₁) ▷ X₂ ≫
            tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁) ▷ X₂) ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
        Iso.inv
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂))) ≫
      (Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ X₂))

Tactic:
slice_rhs 1 2 => rw [← whiskerLeft_comp, ← comp_whiskerRight,
    leftUnitor_inv_braiding]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.leftUnitor_inv_braiding
-- 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 (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    ((tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (ρ_ X₁) ▷ X₂ ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
        Iso.inv
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂))) ≫
      (Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ X₂))

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- 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 (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      (Iso.hom
            (α_ X₁ X₂
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
          X₁ ◁ Iso.inv (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
            X₁ ◁ Iso.hom (β_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
              X₁ ◁ Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
                Iso.inv
                  (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                    (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
        (Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂))
⊢ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      tensorμ X₁ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        (Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ 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
⊢ tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom
          (α_ X₁ X₂
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        X₁ ◁ Iso.inv (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (α_ X₁ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ X₁ ◁ Iso.inv (ρ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)

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
⊢ tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom
          (α_ X₁ X₂
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        X₁ ◁ Iso.inv (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (α_ X₁ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ X₁ ◁ Iso.inv (ρ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)

Tactic:
have :
    ((X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv) ≫
        (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) =
      (α_ X₁ X₂ (𝟙_ C)).hom ≫ (X₁ ◁ (ρ_ X₂).inv ▷ 𝟙_ C) := 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 :
  tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom
          (α_ X₁ X₂
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        X₁ ◁ Iso.inv (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (α_ X₁ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ X₁ ◁ Iso.inv (ρ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)
a : Iso.hom (α_ X₁ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ X₁ ◁ Iso.inv (ρ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)
| tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
    Iso.hom
        (α_ X₁ X₂
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      X₁ ◁ Iso.inv (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

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
this :
  tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom
          (α_ X₁ X₂
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        X₁ ◁ Iso.inv (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (α_ X₁ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ X₁ ◁ Iso.inv (ρ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)
slice_rhs :
  Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    ((((Iso.hom (α_ X₁ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              X₁ ◁ Iso.inv (ρ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
            X₁ ◁ Iso.hom (β_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
          X₁ ◁ Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        Iso.inv
          (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
      (Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂))
⊢ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      (Iso.hom
            (α_ X₁ X₂
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
          X₁ ◁ Iso.inv (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
            X₁ ◁ Iso.hom (β_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
              X₁ ◁ Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
                Iso.inv
                  (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                    (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
        (Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂))

Tactic:
slice_rhs 1 3 => 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
a : X₁ ◁ Iso.inv (λ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)
| X₁ ◁ Iso.inv (ρ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
    X₁ ◁ Iso.hom (β_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)

Tactic:
rw [← whiskerLeft_comp, ← comp_whiskerRight,
    rightUnitor_inv_braiding]

Premises used: CategoryTheory.rightUnitor_inv_braiding, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight
-- 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
slice_rhs :
  Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    Iso.hom (α_ X₁ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      ((X₁ ◁ Iso.inv (λ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            X₁ ◁ Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
          Iso.inv
            (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
              (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
        (Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂))
⊢ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    ((((Iso.hom (α_ X₁ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              X₁ ◁ Iso.inv (ρ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
            X₁ ◁ Iso.hom (β_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
          X₁ ◁ Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        Iso.inv
          (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
      (Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂))

Tactic:
slice_rhs 2 3 => rw [← whiskerLeft_comp, ← comp_whiskerRight,
    rightUnitor_inv_braiding]

Premises used: CategoryTheory.rightUnitor_inv_braiding, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight
-- 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 (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂)) =
    Iso.hom (α_ X₁ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      ((X₁ ◁ Iso.inv (λ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            X₁ ◁ Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
          Iso.inv
            (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
              (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
        (Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂))

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- 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
dsimp :
  (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 (β_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂) Z₁) ▷ 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₂)) =
    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.hom (β_ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁)) ▷ 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₂)))
⊢ tensorμ X₁ X₂ Y₁ Y₂ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ≫
      tensorμ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂) Z₁ Z₂ ≫
        (Iso.hom (α_ X₁ Y₁ Z₁) ⊗ₘ Iso.hom (α_ X₂ 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₂ ◁ tensorμ Y₁ Y₂ Z₁ Z₂ ≫
        tensorμ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂)

Tactic:
dsimp only [tensor_obj, prodMonoidal_tensorObj, tensorμ]

Premises used: CategoryTheory.MonoidalCategory.tensor_obj, CategoryTheory.MonoidalCategory.tensorμ, CategoryTheory.MonoidalCategory.prodMonoidal_tensorObj