-- 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₂ Y₁ Y₂ Z₁ Z₂ : C
simp :
  (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 (α_ X₂ Y₂ Z₁) ≫
                    X₂ ◁ Iso.hom (β_ Y₂ Z₁) ≫ Iso.inv (α_ X₂ Z₁ Y₂) ≫ Iso.hom (β_ X₂ Z₁) ▷ Y₂ ≫ Iso.hom (α_ Z₁ X₂ Y₂)) ▷
                  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.inv (α_ X₂ Y₁ Z₁) ≫
                    Iso.hom (β_ X₂ Y₁) ▷ Z₁ ≫ Iso.hom (α_ Y₁ X₂ Z₁) ≫ Y₁ ◁ Iso.hom (β_ X₂ Z₁) ≫ Iso.inv (α_ Y₁ Z₁ X₂)) ▷
                  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₂)))
⊢ (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:
simp only [braiding_tensor_left_hom, braiding_tensor_right_hom]

Premises used: CategoryTheory.BraidedCategory.braiding_tensor_right_hom, CategoryTheory.BraidedCategory.braiding_tensor_left_hom