∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.unop =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Opposite.unop X)).inv