∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {p f g h pf : C}
  {η : f ≅ g} {θ : g ≅ h} (η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
  (η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj p g ≅ pf)
  (η_h : CategoryTheory.MonoidalCategoryStruct.tensorObj p h ≅ pf),
  CategoryTheory.MonoidalCategory.whiskerLeftIso p η ≪≫ η_g = η_f →
    CategoryTheory.MonoidalCategory.whiskerLeftIso p θ ≪≫ η_h = η_g →
      CategoryTheory.MonoidalCategory.whiskerLeftIso p (η ≪≫ θ) ≪≫ η_h = η_f