∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] (X Y : Action V G),
  CategoryTheory.Functor.OplaxMonoidal.δ (Action.forget V G) X Y =
    CategoryTheory.CategoryStruct.id ((Action.forget V G).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))