-- 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
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
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)))
    ((μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W X) (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
        F.map (Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) W X) Y Z)) ≫
          F.map (Iso.hom (α_ W X Y) ▷ Z) ≫
            F.map ((W ◁ Iso.hom (β_ X Y)) ▷ Z) ≫
              F.map (Iso.inv (α_ W Y X) ▷ Z) ≫ F.map (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) 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))))
⊢ 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:
rw [whiskerLeft_μ_comp_μ,
    associator_inv_naturality_left_assoc, ← pentagon_inv_assoc,
    ← comp_whiskerRight_assoc, ← comp_whiskerRight_assoc, Category.assoc, μ_whiskerRight_comp_μ,
    whiskerLeft_hom_inv_assoc, Iso.inv_hom_id_assoc, comp_whiskerRight_assoc,
    comp_whiskerRight_assoc, μ_natural_left_assoc, associator_inv_naturality_middle_assoc,
    ← comp_whiskerRight_assoc, ← comp_whiskerRight_assoc, ← MonoidalCategory.whiskerLeft_comp,
    ← Functor.LaxBraided.braided,
    MonoidalCategory.whiskerLeft_comp_assoc, μ_natural_right, whiskerLeft_μ_comp_μ_assoc,
    comp_whiskerRight_assoc, comp_whiskerRight_assoc, comp_whiskerRight_assoc,
    comp_whiskerRight_assoc, pentagon_inv_assoc, μ_natural_left_assoc, μ_natural_left_assoc,
    Iso.hom_inv_id_assoc, ← associator_inv_naturality_left_assoc, μ_whiskerRight_comp_μ_assoc,
    Iso.inv_hom_id_assoc, ← tensorHom_def_assoc]

Premises used: CategoryTheory.Functor.LaxMonoidal.whiskerLeft_μ_comp_μ_assoc, CategoryTheory.Category.assoc, CategoryTheory.Functor.LaxMonoidal.μ_natural_right, CategoryTheory.Functor.LaxBraided.braided, CategoryTheory.MonoidalCategory.associator_inv_naturality_left_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc, CategoryTheory.MonoidalCategory.pentagon_inv_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.Functor.LaxMonoidal.μ_whiskerRight_comp_μ_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Functor.LaxMonoidal.whiskerLeft_μ_comp_μ, CategoryTheory.MonoidalCategory.tensorHom_def_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv_assoc, CategoryTheory.Functor.LaxMonoidal.μ_whiskerRight_comp_μ