∀ (C : Type u_4) (D : Type u_2) [inst : CategoryTheory.Category.{u_3, u_4} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{u_1, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' : Cᵒᵖ} (x : Cᵒᵖ) (x_1 : c ⟶ c') (x_2 : Dᵒᵖ),
  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight x_1 x).unop (Opposite.unop x_2)).op =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso (Opposite.unop c) (Opposite.unop x)
              (Opposite.unop x_2)).symm.op.hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft x_1.unop
            (Opposite.unop
              (Opposite.op
                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj (Opposite.unop x)
                  (Opposite.unop x_2))))).op
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso (Opposite.unop c') (Opposite.unop x)
                (Opposite.unop x_2)).symm.op.inv)