∀ {V : Type u_5} [inst : CategoryTheory.Category.{u_4, u_5} V] {G : Type u_2} [inst_1 : Monoid G] {W : Type u_3}
  [inst_2 : CategoryTheory.Category.{u_1, u_3} W] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [inst_5 : F.OplaxMonoidal]
  (x : Action V G),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor ((F.mapAction G).obj x)).inv =
    CategoryTheory.CategoryStruct.comp ((F.mapAction G).map (CategoryTheory.MonoidalCategoryStruct.leftUnitor x).inv)
      (CategoryTheory.CategoryStruct.comp
        {
          hom :=
            CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G)).V
              x.V,
          comm := ⋯ }
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          { hom := CategoryTheory.Functor.OplaxMonoidal.η F, comm := ⋯ } ((F.mapAction G).obj x)))