awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← whiskerRight_iff, comp_whiskerRight, braiding_leftUnitor_aux₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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)
have 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)))
Tactic: rw [← hexagon_reverse]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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) ≫
          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)
have 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)
Tactic: slice_lhs 1 3 => rw [← hexagon_reverse]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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
      (β_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) X) ≫
    X ◁ Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
have a : Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
Tactic: rw [← braiding_naturality_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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) ≫
        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)
have 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))
Tactic: slice_lhs 2 3 => rw [← braiding_naturality_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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)
have 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
Tactic: rw [Iso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [Iso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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)
    (tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (λ_ X))
have 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))
Tactic: rw [triangle_assoc_comp_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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.hom (λ_ X)
have 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))
Tactic: rw [← whiskerLeft_iff, whiskerLeft_comp, braiding_rightUnitor_aux₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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))
⊢ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ Iso.hom (ρ_ X) = Iso.hom (λ_ X)
have 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))
Tactic: rw [← whiskerLeft_iff, whiskerLeft_comp, braiding_rightUnitor_aux₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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))
⊢ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ Iso.hom (ρ_ X) = Iso.hom (λ_ X)
have 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))
Tactic: rw [← whiskerLeft_iff, whiskerLeft_comp, braiding_rightUnitor_aux₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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)) X) = Iso.hom (ρ_ X) ≫ Iso.inv (λ_ X)
have 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)
Tactic: rw [Iso.inv_ext]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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) =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
have 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)
Tactic: rw [braiding_tensorUnit_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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} (α := X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (Iso.inv (ρ_ X) ≫ Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (Iso.inv (λ_ X))
have apply : Eq.{v₁ + 1} (α := X ⟶ X)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (Iso.inv (ρ_ X) ≫ Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (Iso.hom (λ_ X)))
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.inv (λ_ X))
    (Iso.hom (λ_ X)))
Tactic: apply (cancel_mono (λ_ X).hom).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))
have rw : Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X) =
  𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
Tactic: rw [Iso.inv_ext]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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 (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X) =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
have rw : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (Iso.hom (ρ_ X) ≫ Iso.inv (λ_ X)) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X)) =
  𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
Tactic: rw [braiding_tensorUnit_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : G.LaxBraided
X Y : C
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_6) ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ⟶ (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (μ (F ⋙ G) X Y ≫ (F ⋙ G).map (Iso.hom (β_ X Y))) (Iso.hom (β_ ((F ⋙ G).obj X) ((F ⋙ G).obj Y)) ≫ μ (F ⋙ G) Y X)
have dsimp : Eq (α :=
  tensorObj.{v₃, u₃} (𝒞 := inst_6) (G.obj (F.obj X)) (G.obj (F.obj Y)) ⟶
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y))) (μ G (F.obj X) (F.obj Y))
      (G.map (μ F X Y)) ≫
    G.map (F.map (Iso.hom (β_ X Y))))
  (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X))) (μ G (F.obj Y) (F.obj X))
      (G.map (μ F Y X)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : G.LaxBraided
X Y : C
| G.map (μ F X Y) ≫ G.map (F.map (Iso.hom (β_ X Y)))
have a : G.map (Iso.hom (β_ (F.obj X) (F.obj Y))) ≫ G.map (μ F Y X)
Tactic: rw [← CategoryTheory.Functor.map_comp, braided, CategoryTheory.Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : G.LaxBraided
X Y : C
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_6) (G.obj (F.obj X)) (G.obj (F.obj Y)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y))) (μ G (F.obj X) (F.obj Y))
        (G.map (μ F X Y)) ≫
      G.map (F.map (Iso.hom (β_ X Y))))
    (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X))) (μ G (F.obj Y) (F.obj X))
        (G.map (μ F Y X)))
have slice_lhs : Eq (α :=
  tensorObj.{v₃, u₃} (𝒞 := inst_6) (G.obj (F.obj X)) (G.obj (F.obj Y)) ⟶
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y))) (μ G (F.obj X) (F.obj Y))
    (G.map (Iso.hom (β_ (F.obj X) (F.obj Y))) ≫ G.map (μ F Y X)))
  (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X))) (μ G (F.obj Y) (F.obj X))
      (G.map (μ F Y X)))
Tactic: slice_lhs 2 3 =>
      rw [← CategoryTheory.Functor.map_comp, braided, CategoryTheory.Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : G.LaxBraided
X Y : C
| μ G (F.obj X) (F.obj Y) ≫ G.map (Iso.hom (β_ (F.obj X) (F.obj Y)))
have a : Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫ μ G (F.obj Y) (F.obj X)
Tactic: rw [braided]