∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u_2} [inst_3 : CategoryTheory.Category.{u_1, u_2} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_6 : F.Braided] [inst_7 : F'.Braided] (e : F ≅ F')
  (X : CategoryTheory.CommGrp C),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (e.app X.toGrp.X).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.app X.toGrp.X).hom (e.app X.toGrp.X).hom)
      CategoryTheory.MonObj.mul