∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] (e : C ≌ D) [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.BraidedCategory C] (x x_1 : CategoryTheory.Monoidal.Transported e),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ e.inverse x x_1)
      (e.inverse.map ((fun x x_2 => e.functor.mapIso (β_ (e.inverse.obj x) (e.inverse.obj x_2))) x x_1).hom) =
    CategoryTheory.CategoryStruct.comp (β_ (e.inverse.obj x) (e.inverse.obj x_1)).hom
      (CategoryTheory.Functor.LaxMonoidal.μ e.inverse x_1 x)