∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] [inst_2 : CategoryTheory.MonoidalCategory D]
  [inst_3 : CategoryTheory.BraidedCategory D] {X Y : CategoryTheory.Functor C (CategoryTheory.CommMon D)} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.comp
            CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor).map
        f)
      ((fun A =>
            CategoryTheory.NatIso.ofComponents
              (fun X =>
                CategoryTheory.Iso.refl
                  (((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.comp
                            CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor).obj
                        A).obj
                    X))
              ⋯)
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun A =>
            CategoryTheory.NatIso.ofComponents
              (fun X =>
                CategoryTheory.Iso.refl
                  (((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.comp
                            CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor).obj
                        A).obj
                    X))
              ⋯)
          X).hom
      ((CategoryTheory.Functor.id (CategoryTheory.Functor C (CategoryTheory.CommMon D))).map f)