{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {X : C} →
        (one : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) →
          (mul : CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ X) →
            autoParam
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight one X) mul =
                  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)
                CategoryTheory.MonObj.one_mul._autoParam →
              autoParam
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X one) mul =
                    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)
                  CategoryTheory.MonObj.mul_one._autoParam →
                autoParam
                    (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight mul X) mul =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X mul)
                          mul))
                    CategoryTheory.MonObj.mul_assoc._autoParam →
                  (inv : X ⟶ X) →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.CartesianMonoidalCategory.lift inv (CategoryTheory.CategoryStruct.id X))
                            mul =
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
                            one)
                        CategoryTheory.GrpObj.left_inv._autoParam →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) inv)
                              mul =
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
                              one)
                          CategoryTheory.GrpObj.right_inv._autoParam →
                        CategoryTheory.GrpObj X