∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  [inst_2 : CategoryTheory.ExactPairing X Y],
  CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (η_ X Y))
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ X Y) Y) =
    CategoryTheory.MonoidalCoherence.iso.hom