∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  autoParam
    (∀ (X : C),
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor ((CategoryTheory.skeletonEquivalence C).inverse.obj X)).hom =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            CategoryTheory.instMonoidalSkeletonInverseSkeletonEquivalence._aux_1
            ((CategoryTheory.skeletonEquivalence C).inverse.obj X))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.instMonoidalSkeletonInverseSkeletonEquivalence._aux_3
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
            ((CategoryTheory.skeletonEquivalence C).inverse.map
              (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)))
    CategoryTheory.Functor.LaxMonoidal.left_unitality._autoParam