∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (x : C × C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor ((CategoryTheory.MonoidalCategory.tensor C).obj x)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((CategoryTheory.MonoidalCategory.tensor C).obj x)
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).symm.hom)
      (CategoryTheory.CategoryStruct.comp
        {
            hom :=
              CategoryTheory.MonoidalCategory.tensorμ x.1 x.2
                (CategoryTheory.MonoidalCategoryStruct.tensorUnit (C × C)).1
                (CategoryTheory.MonoidalCategoryStruct.tensorUnit (C × C)).2,
            inv :=
              CategoryTheory.MonoidalCategory.tensorδ x.1 x.2
                (CategoryTheory.MonoidalCategoryStruct.tensorUnit (C × C)).1
                (CategoryTheory.MonoidalCategoryStruct.tensorUnit (C × C)).2,
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom
        ((CategoryTheory.MonoidalCategory.tensor C).map (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).hom))