-- 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ᵒᵖ
⊢ 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))) ≫
          Iso.inv
              (α_ (@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_2) (Opposite.unop x_1))
                (@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) ▷
                @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ≫
              comp (Opposite.unop x_3) (Opposite.unop x_1) (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))

Tactic:
simp only [braiding_tensor_left_hom, Category.assoc, Iso.inv_hom_id_assoc,
      braiding_naturality_right_assoc, braiding_tensor_right_hom]

Premises used: CategoryTheory.BraidedCategory.braiding_tensor_right_hom, CategoryTheory.Category.assoc, CategoryTheory.BraidedCategory.braiding_tensor_left_hom, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.BraidedCategory.braiding_naturality_right_assoc