∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ)
  {Y Z : Cᴹᵒᵖ} (f : Y ⟶ Z),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).unmop =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.unmop X.unmop