-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
_ :
  (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₃)) =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁
        (tensorObj.{v₁, u₁} (𝒞 := inst) X₂
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₁) Y₂)
            Y₃)))
      (𝟙
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) X₃)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃)))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁
          (tensorObj.{v₁, u₁} (𝒞 := inst)
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁)
              (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₂))
            Y₃))
        (X₁ ◁ X₂ ◁ Iso.hom (β_ X₃ Y₁) ▷ Y₂ ▷ Y₃)
        (X₁ ◁
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁ ◁ Iso.hom (β_ X₃ Y₂) ≫
                Iso.hom (β_ X₂ Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ X₃) ▷
              Y₃ ⊗≫
          𝟙
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁)
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂)
                (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃)))))
_₁ :
  monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁
        (tensorObj.{v₁, u₁} (𝒞 := inst) X₂
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₁) Y₂)
            Y₃)))
      (𝟙
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) X₃)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃)))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁
          (tensorObj.{v₁, u₁} (𝒞 := inst)
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁)
              (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₂))
            Y₃))
        (X₁ ◁ X₂ ◁ Iso.hom (β_ X₃ Y₁) ▷ Y₂ ▷ Y₃)
        (X₁ ◁
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁ ◁ Iso.hom (β_ X₃ Y₂) ≫
                Iso.hom (β_ X₂ Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ X₃) ▷
              Y₃ ⊗≫
          𝟙
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁)
              (tensorObj.{v₁, u₁} (𝒞 := inst) (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₃)))
⊢ (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:
calc
    _ = 𝟙 _ ⊗≫ X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫
      X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ X₃ Y₂).hom ≫
        (β_ X₂ Y₁).hom ▷ (Y₂ ⊗ X₃)) ▷ Y₃ ⊗≫ 𝟙 _ := by
          rw [braiding_tensor_right_hom]; monoidal
    _ = _ := by rw [whisker_exchange, braiding_tensor_left_hom]; monoidal

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.CategoryStruct.id, CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.CategoryStruct.comp, CategoryTheory.BraidedCategory.braiding, CategoryTheory.Iso.hom