∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {z z' : D} (f : z ⟶ z') (x y : C) {Z : D}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj z'
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y))
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso z x y).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f x) y)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso z' x y).inv h))