∀ {V : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} V] {G : Type u_3} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] (X Y : Action V G) (g h : G),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj ((Action.functorCategoryEquivalence V G).symm.inverse.obj X)
          ((Action.functorCategoryEquivalence V G).symm.inverse.obj Y)).map
      (CategoryTheory.CategoryStruct.comp h g) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.MonoidalCategoryStruct.tensorObj ((Action.functorCategoryEquivalence V G).symm.inverse.obj X)
            ((Action.functorCategoryEquivalence V G).symm.inverse.obj Y)).map
        h)
      ((CategoryTheory.MonoidalCategoryStruct.tensorObj ((Action.functorCategoryEquivalence V G).symm.inverse.obj X)
            ((Action.functorCategoryEquivalence V G).symm.inverse.obj Y)).map
        g)