-- 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
rw :
  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₁ ◁
            (Iso.hom (β_ X₂ Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₂ ≫
                tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ X₂ ◁ Iso.hom (β_ X₃ Y₂)) ▷
              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 (α_ X₂ X₃ Y₁) ≫
                    X₂ ◁ Iso.hom (β_ X₃ Y₁) ≫ Iso.inv (α_ X₂ Y₁ X₃) ≫ Iso.hom (β_ X₂ Y₁) ▷ X₃ ≫ Iso.hom (α_ Y₁ X₂ X₃)) ▷
                  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₃)))
⊢ 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₃)))

Tactic:
rw [whisker_exchange, braiding_tensor_left_hom]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange, CategoryTheory.BraidedCategory.braiding_tensor_left_hom