∀ (C : Type u_3) [inst : CategoryTheory.Category.{u_2, u_3} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C]
  (F : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u_1 + 1}) C)
  (X Y : CategoryTheory.Discrete PUnit.{u_1 + 1}),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxMonoidal.μ
        ((CategoryTheory.Functor.id (CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u_1 + 1}) C)).obj
            F).toFunctor
        X Y)
      ((fun x => F.mapIso (CategoryTheory.eqToIso ⋯)) (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom ((fun x => F.mapIso (CategoryTheory.eqToIso ⋯)) X).hom
        ((fun x => F.mapIso (CategoryTheory.eqToIso ⋯)) Y).hom)
      (CategoryTheory.Functor.LaxMonoidal.μ
        (((CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C).comp
                (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C)).obj
            F).toFunctor
        X Y)