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 : C
rw :
  Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₁ rw₂ :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
rw [Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- 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 : C
rw rw₁ :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom (ρ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Iso.hom (ρ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (Iso.hom (ρ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))

Tactic:
rw [triangle]

Premises used: CategoryTheory.MonoidalCategory.triangle
-- 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 : C
rw :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    ((Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.hom (λ_ X)) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (Iso.hom (ρ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
rw₁ :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
      Iso.hom (λ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (Iso.hom (ρ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
rw₂ rw₃ :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom (ρ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Iso.hom (ρ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ X)
    (Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.hom (λ_ X)) (Iso.hom (ρ_ X))

Tactic:
rw [← whiskerRight_iff, comp_whiskerRight, braiding_leftUnitor_aux₂]

Premises used: CategoryTheory.MonoidalCategory.whiskerRight_iff, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.braiding_leftUnitor_aux₂
-- 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 : C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (Iso.inv (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
        Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ X))
    (X ◁ Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) 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 : C
⊢ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ X) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ 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 : C
⊢ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ X) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
          Iso.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ 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 : C
a :
  Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
    Iso.hom
        (β_ (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)))
| tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
    Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)

Tactic:
rw [← hexagon_reverse]

Premises used: CategoryTheory.BraidedCategory.hexagon_reverse
-- 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 : C
slice_lhs :
  (((Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
            Iso.hom
                (β_
                  (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.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ X) =
    Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom
          (β_ (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.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ X)
⊢ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
          Iso.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ X) =
    Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom
          (β_ (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.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ X)

Tactic:
slice_lhs 1 3 => rw [← hexagon_reverse]

Premises used: CategoryTheory.BraidedCategory.hexagon_reverse
-- 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 : C
⊢ (((Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
            Iso.hom
                (β_
                  (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.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ X) =
    Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom
          (β_ (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.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ X)

Tactic:
simp only [assoc]

Premises used: CategoryTheory.Category.assoc
-- 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 : C
⊢ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom
          (β_ (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.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ X) =
    Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom
          (β_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
            X) ≫
        X ◁ Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) 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 : C
a : Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
| Iso.hom
      (β_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) X) ≫
    X ◁ Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
rw [← braiding_naturality_left]

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_left
-- 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 : C
slice_lhs :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      (Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)) ≫
        Iso.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫
        Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ Iso.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
⊢ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom
          (β_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
            X) ≫
        X ◁ Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) =
    Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫
        Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ Iso.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)

Tactic:
slice_lhs 2 3 => rw [← braiding_naturality_left]

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_left
-- 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 : C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      (Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)) ≫
        Iso.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫
        Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ Iso.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))

Tactic:
simp only [assoc]

Premises used: CategoryTheory.Category.assoc
-- 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 : C
rw :
  Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫
        𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) =
    Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X
rw₁ rw₂ :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X)
    (Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X)
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫
        Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ Iso.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X)

Tactic:
rw [Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- 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 : C
rw rw₁ :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (λ_ X)) (tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (λ_ X))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (Iso.inv (α_ (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.hom (λ_ X))

Tactic:
rw [triangle_assoc_comp_right]

Premises used: CategoryTheory.MonoidalCategory.triangle_assoc_comp_right
-- 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 : C
rw :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ (Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ Iso.hom (ρ_ X)))
    (tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (λ_ X))
rw₁ :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
      tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ X))
    (tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (λ_ X))
rw₂ rw₃ :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (λ_ X)) (tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (λ_ X))
⊢ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ Iso.hom (ρ_ X) = Iso.hom (λ_ X)

Tactic:
rw [← whiskerLeft_iff, whiskerLeft_comp, braiding_rightUnitor_aux₂]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.whiskerLeft_iff, CategoryTheory.braiding_rightUnitor_aux₂
-- 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 : C
⊢ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) = Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X)

Tactic:
simp [← 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 : C
rw :
  Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ Iso.hom (ρ_ X) ≫ Iso.inv (λ_ X) =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
⊢ Iso.inv (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) = Iso.hom (ρ_ X) ≫ Iso.inv (λ_ X)

Tactic:
rw [Iso.inv_ext]

Premises used: CategoryTheory.Iso.inv_ext
-- 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 : C
rw :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X)) (Iso.hom (ρ_ X) ≫ Iso.inv (λ_ X)) =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
⊢ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ Iso.hom (ρ_ X) ≫ Iso.inv (λ_ X) =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)

Tactic:
rw [braiding_tensorUnit_left]

Premises used: CategoryTheory.braiding_tensorUnit_left
-- 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 : C
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X)) (Iso.hom (ρ_ X) ≫ Iso.inv (λ_ X)) =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) 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 : C
⊢ Iso.inv (λ_ X) ≫ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) = Iso.inv (ρ_ X)

Tactic:
simp