-- 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x x_1 x_2 : Cᵒᵖ
x_3 : Dᵒᵖ
a :
  Eq.{v_2 + 1} (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3)
            (unop
              (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)
                x_2)))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop
              (op
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
                  (unop
                    (op
                      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3) (unop x))))
                  (unop x_1))))
            (unop x_2))))
    (inv
      (Quiver.Hom.unop
        (Quiver.Hom.op (unop x_3 ⊴ᵣ Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2))) ≫
          Iso.hom
              (Iso.op
                (Iso.symm (αᵣ (unop x_3) (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2))))) ≫
            Iso.hom
              (Iso.op
                (Iso.symm
                  (αᵣ
                    (unop
                      (op
                        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3)
                          (unop x))))
                    (unop x_1) (unop x_2)))))))
    (inv
      (Quiver.Hom.unop
        (Iso.hom
            (Iso.op
              (Iso.symm (αᵣ (unop x_3) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2)))) ≫
          Quiver.Hom.op
            (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_3) (unop x) (unop x_1))))) ⊵ᵣ unop x_2))))
⊢ Eq.{v_2 + 1} (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop
              (op
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
                  (unop
                    (op
                      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3) (unop x))))
                  (unop x_1))))
            (unop x_2))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3)
            (unop
              (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)
                x_2)))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (unop x_3 ⊴ᵣ Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2))) ≫
        Iso.hom
            (Iso.op
              (Iso.symm (αᵣ (unop x_3) (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2))))) ≫
          Iso.hom
            (Iso.op
              (Iso.symm
                (αᵣ
                  (unop
                    (op
                      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3) (unop x))))
                  (unop x_1) (unop x_2))))))
    (Quiver.Hom.unop
      (Iso.hom
          (Iso.op (Iso.symm (αᵣ (unop x_3) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2)))) ≫
        Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_3) (unop x) (unop x_1))))) ⊵ᵣ unop x_2)))

Tactic:
apply IsIso.inv_eq_inv.mp

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