fix tutorial

Author: RemyDegenne

tutorial/lake-manifest.json

@@ -1,21 +1,31 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7ae82ac2ae54ae5dcc9948a701669e9b596e5cae",
+   "rev": "14e7bf2c43076234c4f728d94f8b098dbb36e3cd",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/illuminate",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c7a8de81e102ee2a42a7395f98d1ed12a861a43b",
+   "name": "illuminate",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
+   "rev": "744117af710b1c0400cd297c9ce91f8d0ad3a347",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,11 +45,12 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "52b9dfbd2658408e37ae6e8b72601ddeaaa25a0c",
+   "rev": "a86770a5eba721c8554d1d7fce741bc4dde3bb61",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"}],
  "name": "manual",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

tutorial/lakefile.toml

@@ -8,7 +8,7 @@ autoImplicit = true
 [[require]]
 name = "verso"
 git = "https://github.com/leanprover/verso"
-rev = "v4.29.0"
+rev = "main"
 
 [[lean_lib]]
 name = "Manual"

tutorial/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.31.0-rc2