∀ (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] [inst_3 : CategoryTheory.BraidedCategory V] (X Y : Action V G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (Action.forget V G) X Y)
      ((Action.forget V G).map (β_ X Y).hom) =
    CategoryTheory.CategoryStruct.comp (β_ ((Action.forget V G).obj X) ((Action.forget V G).obj Y)).hom
      (CategoryTheory.Functor.LaxMonoidal.μ (Action.forget V G) Y X)