∀ (X : CategoryTheory.Cat) {A B : CategoryTheory.Cat} (f : A ⟶ B),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).toFunctor.comp (CategoryTheory.Prod.snd ↑X ↑B) =
    (CategoryTheory.Prod.snd ↑X ↑A).comp f.toFunctor