diff --git a/lake-manifest.json b/lake-manifest.json
index af8312a1..f369a676 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,14 +1,14 @@
-{"version": "1.2.0",
+{"version": "1.3.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "487140449b0eceeb60afe04cab75cdcaaebf227f",
+   "rev": "c55e6e786f49471c72fbddbec5415808896aec1e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "487140449b0eceeb60afe04cab75cdcaaebf227f",
+   "inputRev": "c55e6e786f49471c72fbddbec5415808896aec1e",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e50948299c4dc4a4c21b1c34b6a6a4fddc19f912",
+   "rev": "fb13df72ecefd8ddbf9291021d7f33a8673eb57b",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "95e037bfdc31d3916ac615446847fb01960e2719",
+   "rev": "29ff470276c725ae01505d55b17148c18fc7dfd3",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f8e94c24111148c9ad1b866212a6e1a0fabb5e76",
+   "rev": "7e81a29bda33a6b257bd37557a6aa6aebe175d96",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4c70ac059693669e5756e32a7a94b57ee1e99dc5",
+   "rev": "c643bbb3c24f8a25f9c14e3a6b1ceb13d01f3de1",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "75d936c7af167cc93fac0d31237682fc2204591d",
+   "rev": "a90fbf7b02ff06a0deebf74088dff9e5fe02c9ea",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "786b7acdca7eb4e9c76c5d1d5bd810e7e5c56334",
+   "rev": "37b0ba0b26109cf9f9c541f0f9557e50cfa1a3b9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "167242e0621ba382fd6f7b2a7e932ce0811f9ab1",
+   "rev": "3b7c8101932390d60e92a3f3d917901d5b5a773b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "2842b9871b04862f944c032e34052cb9448ccb71",
+   "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0-rc2",
+   "inputRev": "v4.35.0-rc3",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/illuminate",
diff --git a/lakefile.toml b/lakefile.toml
index 1a966181..2a8b8e3d 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -17,7 +17,7 @@ rev = "v4.35.0-rc2"
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "487140449b0eceeb60afe04cab75cdcaaebf227f"
+rev = "c55e6e786f49471c72fbddbec5415808896aec1e"
 
 [[lean_lib]]
 name = "LeanMachineLearning"
diff --git a/lean-toolchain b/lean-toolchain
index acc704ff..9d74fe15 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.35.0-rc2
+leanprover/lean4:v4.35.0-rc3
\ No newline at end of file