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₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
h :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))
    ((f₁ ⊗ₘ f₂) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ≫ tensorμ Y₁ Y₂ Z₁ Z₂)
    (((f₁ ⊗ₘ f₂) ⊗ₘ 𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂)
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))
    ((f₁ ⊗ₘ f₂) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ≫ tensorμ Y₁ Y₂ Z₁ Z₂)
    (tensorμ X₁ X₂ Z₁ Z₂ ≫ (f₁ ▷ Z₁ ⊗ₘ f₂ ▷ Z₂))
have h₁ : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))
  (tensorμ X₁ X₂ Z₁ Z₂ ≫ (f₁ ▷ Z₁ ⊗ₘ f₂ ▷ Z₂)) (tensorμ X₁ X₂ Z₁ Z₂ ≫ ((f₁ ⊗ₘ 𝟙 Z₁) ⊗ₘ f₂ ⊗ₘ 𝟙 Z₂))
Tactic: convert! tensorμ_natural f₁ f₂ (𝟙 Z₁) (𝟙 Z₂) using 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
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₂ = tensorμ Z₁ Z₂ X₁ X₂ ≫ (Z₁ ◁ f₁ ⊗ₘ Z₂ ◁ f₂)
have h : tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ◁ (f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂ =
  ((𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ⊗ₘ f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂
Tactic: convert! tensorμ_natural (𝟙 Z₁) (𝟙 Z₂) f₁ f₂ using 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
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₂
⊢ tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ◁ (f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂ = tensorμ Z₁ Z₂ X₁ X₂ ≫ (Z₁ ◁ f₁ ⊗ₘ Z₂ ◁ f₂)
have 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₂))
Tactic: convert! tensorμ_natural (𝟙 Z₁) (𝟙 Z₂) f₁ f₂ using 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₁ X₂ : C
⊢ 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₂))
have 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₂))
Tactic: dsimp only [tensorμ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (hypothesis)
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.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₂))
have 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₂
Tactic: have :
    ((λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂)) ≫
        (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ (𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv) =
      𝟙_ C ◁ (λ_ X₁).inv ▷ X₂ := by
    simp
-- 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₁ 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₂
| 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₂)
have a : tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (λ_ X₁) ▷ X₂
Tactic: rw [this]
-- 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₁ 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₂
⊢ 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₂))
have 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₂))
Tactic: slice_rhs 1 3 => rw [this]
-- 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₁ X₂ : C
| tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (λ_ X₁) ▷ X₂ ≫
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁) ▷ X₂
have a : tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (ρ_ X₁) ▷ X₂
Tactic: rw [← whiskerLeft_comp, ← comp_whiskerRight,
    leftUnitor_inv_braiding]
-- 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₁ 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 (β_ (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₂))
have 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₂))
Tactic: slice_rhs 1 2 => rw [← whiskerLeft_comp, ← comp_whiskerRight,
    leftUnitor_inv_braiding]
-- 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₁ X₂ : C
⊢ 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₂))
have 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₂))
Tactic: dsimp only [tensorμ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (hypothesis)
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₂)) =
    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₂))
have 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)
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
-- 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₁ 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)
| 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)))
have a : Iso.hom (α_ X₁ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ X₁ ◁ Iso.inv (ρ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)
Tactic: rw [this]
-- 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₁ 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)
⊢ 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₂))
have 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₂))
Tactic: slice_rhs 1 3 => rw [this]
-- 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₁ X₂ : C
| X₁ ◁ Iso.inv (ρ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
    X₁ ◁ Iso.hom (β_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)
have a : X₁ ◁ Iso.inv (λ_ X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)
Tactic: rw [← whiskerLeft_comp, ← comp_whiskerRight,
    rightUnitor_inv_braiding]
-- 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₁ 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 (β_ 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₂))
have 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₂))
Tactic: slice_rhs 2 3 => rw [← whiskerLeft_comp, ← comp_whiskerRight,
    rightUnitor_inv_braiding]
-- 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₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ 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₂)
have 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₂)))
Tactic: dsimp only [tensor_obj, prodMonoidal_tensorObj, tensorμ]
-- 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₁ X₂ : C
⊢ 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₂))
have 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₂))
Tactic: dsimp only [tensorμ]