∀ (C : Type u_4) (D : Type u_1) [inst : CategoryTheory.Category.{u_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{u_2, u_1} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (X : C),
  {
      app := fun y =>
        CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight y (CategoryTheory.CategoryStruct.id X),
      naturality := ⋯ } =
    CategoryTheory.CategoryStruct.id
      { obj := fun y => CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj y X,
        map := fun {X_1 Y} f => CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f X,
        map_id := ⋯, map_comp := ⋯ }