-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x x_1 x_2 x_3 : Cᵒᵖ
simp :
  Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := V)
      (tensorObj.{v₁, u₁} (𝒞 := inst) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_2) (Opposite.unop x_1))
          (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x_2))))
      (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x)))
    (Iso.inv
        (α_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
          (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_2) (Opposite.unop x_1))
          (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x_2))) ≫
      Iso.hom
          (β_
            (tensorObj.{v₁, u₁} (𝒞 := inst) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
              (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_2) (Opposite.unop x_1)))
            (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x_2))) ≫
        @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x_2) ◁
            Iso.hom
              (β_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
                (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_2) (Opposite.unop x_1))) ≫
          @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x_2) ◁
              comp (Opposite.unop x_2) (Opposite.unop x_1) (Opposite.unop x) ≫
            comp (Opposite.unop x_3) (Opposite.unop x_2) (Opposite.unop x))
    (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ◁
        Iso.hom
          (β_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_2) (Opposite.unop x_1))
            (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x_2))) ≫
      @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ◁
          comp (Opposite.unop x_3) (Opposite.unop x_2) (Opposite.unop x_1) ≫
        Iso.hom
            (β_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
              (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x_1))) ≫
          comp (Opposite.unop x_3) (Opposite.unop x_1) (Opposite.unop x))
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := V)
      (tensorObj.{v₁, u₁} (𝒞 := inst) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_2) (Opposite.unop x_1))
          (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x_2))))
      (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x)))
    (Iso.inv
        (α_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
          (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_2) (Opposite.unop x_1))
          (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x_2))) ≫
      (Iso.hom
              (β_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
                (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_2) (Opposite.unop x_1))) ≫
            comp (Opposite.unop x_2) (Opposite.unop x_1) (Opposite.unop x)) ▷
          @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x_2) ≫
        Iso.hom
            (β_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_2) (Opposite.unop x))
              (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x_2))) ≫
          comp (Opposite.unop x_3) (Opposite.unop x_2) (Opposite.unop x))
    (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ◁
        (Iso.hom
            (β_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_2) (Opposite.unop x_1))
              (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x_2))) ≫
          comp (Opposite.unop x_3) (Opposite.unop x_2) (Opposite.unop x_1)) ≫
      Iso.hom
          (β_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
            (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_3) (Opposite.unop x_1))) ≫
        comp (Opposite.unop x_3) (Opposite.unop x_1) (Opposite.unop x))

Tactic:
simp only [braiding_naturality_left_assoc,
      MonoidalCategory.whiskerLeft_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.BraidedCategory.braiding_naturality_left_assoc