∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{u_4, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c₁ c₂ c₃ c₄ : Cᵒᵖ} {d₁ d₂ : Dᵒᵖ} (x : c₁ ⟶ c₂)
  (x_1 : c₃ ⟶ c₄) (x_2 : d₁ ⟶ d₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom
          (CategoryTheory.MonoidalCategoryStruct.tensorHom x x_1).unop x_2.unop).op
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso (Opposite.unop c₂) (Opposite.unop c₄)
              (Opposite.unop d₂)).symm.op.hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso (Opposite.unop c₁) (Opposite.unop c₃)
              (Opposite.unop d₁)).symm.op.hom
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom x.unop
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom x_1.unop x_2.unop).op.unop).op