∀ {I : Type u_3} {C : I → Type u_2} [inst : (i : I) → CategoryTheory.Category.{u_1, u_2} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] [inst_2 : (i : I) → CategoryTheory.BraidedCategory (C i)]
  (i : I) (X Y : (i : I) → C i),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Pi.eval C i) X Y)
      ((CategoryTheory.Pi.eval C i).map (β_ X Y).hom) =
    CategoryTheory.CategoryStruct.comp
      (β_ ((CategoryTheory.Pi.eval C i).obj X) ((CategoryTheory.Pi.eval C i).obj Y)).hom
      (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Pi.eval C i) Y X)