-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Opposite (goal)
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
              (β_ (@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))
have 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))
Tactic: simp only [braiding_naturality_left_assoc,
      MonoidalCategory.whiskerLeft_comp, Category.assoc]