diff --git a/LeanPlot/ToFloat.lean b/LeanPlot/ToFloat.lean
index ae07a9f..853aa51 100644
--- a/LeanPlot/ToFloat.lean
+++ b/LeanPlot/ToFloat.lean
@@ -47,7 +47,7 @@ instance instToFloatInt : ToFloat Int where
 instance [Coe α Float] : ToFloat α where
   toFloat a := ↑a
 
-/-! ### `Rat` instance
+/-! ## `Rat` instance
 
 Lean 4 ships with a rational number type `Rat` in `Init.Data.Rat`.
 The conversion takes the numerator/denominator and performs a floating-point
diff --git a/lake-manifest.json b/lake-manifest.json
index 8cc0d5f..2cffb19 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,31 +1,41 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "6f0c12be90063de6d4e5ca14867ad7243064ad99",
+   "rev": "8bcbd2b8723307c329c12997a0c16a6ac174d3e9",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.30.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "627a9728700546ebc9cc274821ad7c0b420c2e35",
+   "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v0.0.99",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/illuminate",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "99ada816d9929a51132d5b5dc4f43c51f16d67d8",
+   "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": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11",
+   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "38ac5945d744903ffcc473ce1030223991b11cf6",
+   "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,11 +55,12 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "eb77622e97e942ba2cfe02f60637705fc2d9481b",
+   "rev": "ce893b9042128037e2d3c0158b9567fab9fae268",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"}],
  "name": "LeanPlot",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.toml b/lakefile.toml
index 1a1d5e7..5a4a7d2 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -54,7 +54,9 @@ root = "TestExport"
 [[require]]
 name = "proofwidgets"
 scope = "leanprover-community"
+rev = "v0.0.99"
 
 [[require]]
 name = "verso"
 scope = "leanprover"
+rev = "v4.30.0"
diff --git a/lean-toolchain b/lean-toolchain
index bd19bde..af9e5d3 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.27.0-rc1
+leanprover/lean4:v4.30.0