∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u_3 + 1}) C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxMonoidal.ε
        ((CategoryTheory.Functor.id (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u_3 + 1}) C)).obj
            F).toFunctor)
      ((fun x => F.mapIso (CategoryTheory.eqToIso ⋯))
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{u_3 + 1}))).hom =
    CategoryTheory.Functor.LaxMonoidal.ε
      (((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).comp
              (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C)).obj
          F).toFunctor