∀ {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.MonoidalLeftAction C D] {c₁ c₂ c₃ c₄ : C} {d₁ d₂ : D} (f : c₁ ⟶ c₂)
  (g : c₃ ⟶ c₄) (h : d₁ ⟶ d₂) {Z : D}
  (h_1 :
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj c₂ c₄) d₂ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom g h))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₂ c₄ d₂).inv h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₁ c₃ d₁).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
        h_1)