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