∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {f f' g g' h i : C} {α : f ≅ g} {η : g ⟶ h} {ηs : h ⟶ i} {β : f' ≅ g'}
  {η₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj g g' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj h g'}
  {ηs₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj h g' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i g'}
  {η₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj g g' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i g'}
  {η₃ : CategoryTheory.MonoidalCategoryStruct.tensorObj f f' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i g'},
  CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl g).hom
          (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl h).hom))
        g' =
      η₁ →
    CategoryTheory.MonoidalCategoryStruct.whiskerRight ηs g' = ηs₁ →
      CategoryTheory.CategoryStruct.comp η₁ ηs₁ = η₂ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorIso α β).hom η₂ = η₃ →
          CategoryTheory.MonoidalCategoryStruct.tensorHom
              (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) β.hom =
            η₃