∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.HasRightDual X] [inst_3 : CategoryTheory.HasRightDual Y] {f : X ⟶ Y} {g : Xᘁ ⟶ Z},
  CategoryTheory.CategoryStruct.comp (fᘁ) g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Yᘁ).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ (η_ X Xᘁ))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Yᘁ Y Z).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ Y Yᘁ) Z)
              (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom))))