-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Opposites (goal)
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
⊢ Eq (α :=
    unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_3)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1) x_2))) ⟶
      unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
          (op
            (unop
              (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                (op
                  (unop
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                      (op x_3) (op x))))
                (op x_1))))
          (op x_2)))
    (Quiver.Hom.unop (op x_3 ⊴ᵣ Quiver.Hom.op (Iso.hom (α_ x x_1 x_2))) ≫
      Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_3) (op x) (op (tensorObj.{v_1, u_1} (𝒞 := inst) x_1 x_2))))) ≫
        Iso.hom
          (Iso.unop
            (Iso.symm
              (αᵣ
                (op
                  (unop
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                      (op x_3) (op x))))
                (op x_1) (op x_2)))))
    (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_3) (op (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1)) (op x_2)))) ≫
      Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_3) (op x) (op x_1))))) ⊵ᵣ op x_2))
have a : Eq.{v_2 + 1} (α :=
  op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
          (op
            (unop
              (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                (op
                  (unop
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                      (op x_3) (op x))))
                (op x_1))))
          (op x_2))) ⟶
    op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_3)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1) x_2)))))
  (Quiver.Hom.op
    (Quiver.Hom.unop (op x_3 ⊴ᵣ Quiver.Hom.op (Iso.hom (α_ x x_1 x_2))) ≫
      Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_3) (op x) (op (tensorObj.{v_1, u_1} (𝒞 := inst) x_1 x_2))))) ≫
        Iso.hom
          (Iso.unop
            (Iso.symm
              (αᵣ
                (op
                  (unop
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                      (op x_3) (op x))))
                (op x_1) (op x_2))))))
  (Quiver.Hom.op
    (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_3) (op (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1)) (op x_2)))) ≫
      Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_3) (op x) (op x_1))))) ⊵ᵣ op x_2)))
Tactic: apply Quiver.Hom.op_inj