awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (λ_ 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₂))
have this : Iso.hom (λ_ X₁) ⊗ₘ Iso.hom (λ_ X₂) =
  Iso.hom
      (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₁
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ≫
      Iso.hom
          (λ_
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
              X₂)) ≫
        Iso.hom (ρ_ X₁) ▷ X₂
Tactic: have :
    (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom =
      (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).hom ≫
        (𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).inv) ≫ (λ_ ((X₁ ⊗ 𝟙_ C) ⊗ X₂)).hom ≫ ((ρ_ X₁).hom ▷ X₂) := by
    monoidal
-- 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μ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))
have dsimp : Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂) =
  (Iso.hom
        (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        X₁ ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
          X₁ ◁ Iso.hom (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
            Iso.inv
              (α_ X₁ X₂
                (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                  (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
    tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))
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 (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂) =
    (Iso.hom
          (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          X₁ ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            X₁ ◁ Iso.hom (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              Iso.inv
                (α_ X₁ X₂
                  (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                    (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))
have this : Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂) =
  Iso.hom
      (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
    X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X₁ ◁ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫ X₁ ◁ Iso.hom (λ_ X₂)
Tactic: have :
    (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom =
      (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫
        (X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv) ≫ (X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom) ≫ (X₁ ◁ (λ_ X₂).hom) := by
    monoidal
-- 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.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂) =
    Iso.hom
        (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        X₁ ◁ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫ X₁ ◁ Iso.hom (λ_ X₂)
⊢ Iso.hom (ρ_ X₁) ⊗ₘ Iso.hom (ρ_ X₂) =
    (Iso.hom
          (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          X₁ ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            X₁ ◁ Iso.hom (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              Iso.inv
                (α_ X₁ X₂
                  (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                    (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))
have rw : Iso.hom
      (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
    X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X₁ ◁ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫ X₁ ◁ Iso.hom (λ_ X₂) =
  (Iso.hom
        (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        X₁ ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
          X₁ ◁ Iso.hom (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
            Iso.inv
              (α_ X₁ X₂
                (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                  (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
    tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))
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
⊢ Iso.hom
        (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        X₁ ◁ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
          X₁ ◁ Iso.hom (λ_ X₂) =
    (Iso.hom
          (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          X₁ ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            X₁ ◁ Iso.hom (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              Iso.inv
                (α_ X₁ X₂
                  (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                    (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))
have rw : Iso.hom
      (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
    X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X₁ ◁ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂)) ≫
        X₁ ◁ (Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ≫ Iso.hom (ρ_ X₂)) =
  (Iso.hom
        (α_ X₁ (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      X₁ ◁ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        X₁ ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X₂) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
          X₁ ◁ Iso.hom (α_ X₂ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
            Iso.inv
              (α_ X₁ X₂
                (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
                  (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
    tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))
Tactic: rw [← braiding_rightUnitor]
-- 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₂ X₃ Y₁ Y₂ Y₃ : C
⊢ tensorμ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) X₃ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃ ≫
      tensorμ X₁ X₂ Y₁ Y₂ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃ ≫
        Iso.hom
          (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂)
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃)) =
    (Iso.hom (α_ X₁ X₂ X₃) ⊗ₘ Iso.hom (α_ Y₁ Y₂ Y₃)) ≫
      tensorμ X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁ tensorμ X₂ X₃ Y₂ Y₃
have dsimp : (Iso.hom
        (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) X₃
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃)) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.inv (α_ X₃ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (β_ X₃ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂)) ▷ Y₃ ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) X₃ Y₃) ≫
            Iso.inv
              (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂)
                (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃))) ≫
    (Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂)) ≫
          X₁ ◁ Iso.inv (α_ X₂ Y₁ Y₂) ≫
            X₁ ◁ Iso.hom (β_ X₂ Y₁) ▷ Y₂ ≫
              X₁ ◁ Iso.hom (α_ Y₁ X₂ Y₂) ≫ Iso.inv (α_ X₁ Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂))) ▷
        tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃ ≫
      Iso.hom
        (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃)) =
  (Iso.hom (α_ X₁ X₂ X₃) ⊗ₘ Iso.hom (α_ Y₁ Y₂ Y₃)) ≫
    (Iso.hom
          (α_ X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃)
            (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃))) ≫
        X₁ ◁ Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
          X₁ ◁ Iso.hom (β_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃ ≫
            X₁ ◁ Iso.hom (α_ Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
              Iso.inv
                (α_ X₁ Y₁
                  (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃)
                    (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)))) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁
        (Iso.hom (α_ X₂ X₃ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
          X₂ ◁ Iso.inv (α_ X₃ Y₂ Y₃) ≫
            X₂ ◁ Iso.hom (β_ X₃ Y₂) ▷ Y₃ ≫
              X₂ ◁ Iso.hom (α_ Y₂ X₃ Y₃) ≫ Iso.inv (α_ X₂ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃)))
Tactic: dsimp only [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
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.LaxBraided
W X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_3) (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj W) (F.obj X))
        (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z)))
    (tensorμ (F.obj W) (F.obj X) (F.obj Y) (F.obj Z) ≫
      (μ F W Y ⊗ₘ μ F X Z) ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z))
    ((μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W X) (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.map (tensorμ W X Y Z))
have rw : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_3) (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj W) (F.obj X))
      (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj Z)) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z)))
  (tensorμ (F.obj W) (F.obj X) (F.obj Y) (F.obj Z) ≫
    (μ F W Y ▷ tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Z) ≫
        F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) ◁ μ F X Z) ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z))
  ((μ F W X ⊗ₘ μ F Y Z) ≫
    μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W X) (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.map (tensorμ W X Y Z))
Tactic: rw [tensorHom_def]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.LaxBraided
W X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_3) (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj W) (F.obj X))
        (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z)))
    (tensorμ (F.obj W) (F.obj X) (F.obj Y) (F.obj Z) ≫
      (μ F W Y ▷ tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Z) ≫
          F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) ◁ μ F X Z) ≫
        μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z))
    ((μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W X) (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.map (tensorμ W X Y Z))
have simp : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_3) (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj W) (F.obj X))
      (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj Z)) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z)))
  (Iso.hom (α_ (F.obj W) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj Z))) ≫
    F.obj W ◁ Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
      F.obj W ◁ Iso.hom (β_ (F.obj X) (F.obj Y)) ▷ F.obj Z ≫
        F.obj W ◁ Iso.hom (α_ (F.obj Y) (F.obj X) (F.obj Z)) ≫
          Iso.inv (α_ (F.obj W) (F.obj Y) (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Z))) ≫
            μ F W Y ▷ tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Z) ≫
              F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) ◁ μ F X Z ≫
                μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z))
  ((μ F W X ⊗ₘ μ F Y Z) ≫
    μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W X) (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
      F.map
        (Iso.hom (α_ W X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
          W ◁ Iso.inv (α_ X Y Z) ≫
            W ◁ Iso.hom (β_ X Y) ▷ Z ≫ W ◁ Iso.hom (α_ Y X Z) ≫ Iso.inv (α_ W Y (tensorObj.{v₁, u₁} (𝒞 := inst) X Z))))
Tactic: simp only [tensorμ, Category.assoc]
-- 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
i : SymmetricCategory.{v₁, u₁} C
⊢ Eq (α := BraidedCategory.{v₁, u₁} C)
    { braiding := fun (X Y : C) ↦ Iso.symm (β_ Y X), braiding_naturality_right := ⋯, braiding_naturality_left := ⋯,
      hexagon_forward := ⋯, hexagon_reverse := ⋯ }
    toBraidedCategory
have e_braiding : Eq (α := (X Y : C) → tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≅ tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
  (fun (X Y : C) ↦ Iso.symm (β_ Y X)) β_
Tactic: congr
-- 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
i : SymmetricCategory.{v₁, u₁} C
⊢ Eq (α := (X Y : C) → tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≅ tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    (fun (X Y : C) ↦ Iso.symm (β_ Y X)) β_
have e_braiding : ∀ (X Y : C),
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X Y ≅ tensorObj.{v₁, u₁} (𝒞 := inst) Y X) (Iso.symm (β_ Y X))
    (β_ X Y)
Tactic: funext X Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
c : C
d : D
inst_7 :
  IsIso (X :=
    L.obj
      (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
    (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))
this :
  Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) d
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ⟶
      R.obj c)
    (d ◁ adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ≫ adjRetractionAux adj c d)
    (NatTrans.app (ihom.ev d) (R.obj c))
⊢ adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ≫ adjRetraction adj c d =
    𝟙 (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
have simp : curry (NatTrans.app (ihom.ev d) (R.obj c)) = 𝟙 (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))
Tactic: simp only [id_obj, comp_obj, adjRetraction, ← curry_natural_left, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
c : C
d : D
inst_7 :
  IsIso (X :=
    L.obj
      (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
    (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ≫ adjRetraction adj c d =
    𝟙 (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
have suffices : Eq (α :=
  tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ⟶
    R.obj c)
  (d ◁ adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ≫ adjRetractionAux adj c d)
  (NatTrans.app (ihom.ev d) (R.obj c))
Tactic: suffices (_ ◁ adj.unit.app _) ≫ adjRetractionAux adj c d = (ihom.ev _).app _ by
    simp only [id_obj, comp_obj, adjRetraction, ← curry_natural_left, this]
    simp [curry_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
c : C
d : D
inst_7 :
  IsIso (X :=
    L.obj
      (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
    (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) d
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ⟶
      R.obj c)
    (d ◁ adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ≫ adjRetractionAux adj c d)
    (NatTrans.app (ihom.ev d) (R.obj c))
have simp : Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ≫
    adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ▷ d ≫
      R.obj (L.obj (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ◁ adj.unit.app d ≫
        adj.unit.app
            (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj (L.obj (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))))
              (R.obj (L.obj d))) ≫
          inv (R.map (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))) ≫
            R.map (L.map (Iso.hom (β_ (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) d))) ≫
              R.map (L.map (NatTrans.app (ihom.ev d) (R.obj c))) ≫ inv (adj.unit.app (R.1 c)) =
  NatTrans.app (ihom.ev d) (R.obj c)
Tactic: simp only [id_obj, comp_obj, adjRetractionAux, Functor.map_inv, Functor.comp_map,
    braiding_naturality_right_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
c : C
d : D
inst_7 :
  IsIso (X :=
    L.obj
      (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
    (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))
| adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ▷ d ≫
    R.obj (L.obj (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ◁ adj.unit.app d
have a : adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d
Tactic: simp only [← id_tensorHom, ← tensorHom_id, tensorHom_comp_tensorHom, Category.id_comp,
      Category.comp_id]