-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} Cᵒᵖ Dᵒᵖ
x x_1 x_2 : C
x_3 : D
a :
  Eq.{v_2 + 1} (α :=
    op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
            (op (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1) x_2)) (op x_3))) ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x)
            (op
              (unop
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                  (op x_1)
                  (op
                    (unop
                      (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct
                        _ (op x_2) (op x_3))))))))))
    (inv
      (Quiver.Hom.op
        (CategoryStruct.comp (Y :=
          unop
            (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
              (op (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorObj.{v_1, u_1} (𝒞 := inst) x_1 x_2))) (op x_3)))
          (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (α_ x x_1 x_2)) ⊵ₗ op x_3))
          (Iso.hom (Iso.unop (Iso.symm (αₗ (op x) (op (tensorObj.{v_1, u_1} (𝒞 := inst) x_1 x_2)) (op x_3)))) ≫
            Quiver.Hom.unop (op x ⊴ₗ Quiver.Hom.op (Iso.hom (Iso.unop (Iso.symm (αₗ (op x_1) (op x_2) (op x_3))))))))))
    (inv
      (Quiver.Hom.op
        (Iso.hom (Iso.unop (Iso.symm (αₗ (op (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1)) (op x_2) (op x_3)))) ≫
          Iso.hom
            (Iso.unop
              (Iso.symm
                (αₗ (op x) (op x_1)
                  (op
                    (unop
                      (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct
                        _ (op x_2) (op x_3))))))))))
⊢ Eq.{v_2 + 1} (α :=
    op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x)
            (op
              (unop
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                  (op x_1)
                  (op
                    (unop
                      (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct
                        _ (op x_2) (op x_3))))))))) ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
            (op (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1) x_2)) (op x_3))))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y :=
        unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
            (op (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorObj.{v_1, u_1} (𝒞 := inst) x_1 x_2))) (op x_3)))
        (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (α_ x x_1 x_2)) ⊵ₗ op x_3))
        (Iso.hom (Iso.unop (Iso.symm (αₗ (op x) (op (tensorObj.{v_1, u_1} (𝒞 := inst) x_1 x_2)) (op x_3)))) ≫
          Quiver.Hom.unop (op x ⊴ₗ Quiver.Hom.op (Iso.hom (Iso.unop (Iso.symm (αₗ (op x_1) (op x_2) (op x_3)))))))))
    (Quiver.Hom.op
      (Iso.hom (Iso.unop (Iso.symm (αₗ (op (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1)) (op x_2) (op x_3)))) ≫
        Iso.hom
          (Iso.unop
            (Iso.symm
              (αₗ (op x) (op x_1)
                (op
                  (unop
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                      (op x_2) (op x_3)))))))))

Tactic:
apply IsIso.inv_eq_inv.mp

Premises used: CategoryTheory.IsIso.inv_eq_inv, Iff.mp