diff --git a/lake-manifest.json b/lake-manifest.json
index 13e96041..acfdab79 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0291556f04e89d46cd2999f0f4c1164c81778207",
+   "rev": "5a111ebbb151dc6719734f39b1d3aea8d5affb76",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/PatrickMassot/checkdecls.git",
@@ -25,10 +25,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608",
+   "rev": "a57f31753dde989bc415cb64277a1688866e443c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/mhuisi/lean4-cli",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "470c41643209208d325a5a7315116f293c7443fb",
+   "rev": "51b0cd28a0ca79ccfa91b8c7d5eb94ba075dfdb4",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -61,24 +61,24 @@
    "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/acmepjz/md4lean",
+  {"url": "https://github.com/kim-em/md4lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f8ed91f3a9d806648ae6a03ab98c8b87e8bedc7e",
+   "rev": "17e3f60bca8b6fdc19a55e2a7c9840a9f7afd1dc",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "bump_to_v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
+   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -95,30 +95,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
+   "rev": "9cb79405471ae931ac718231d6299bfaffef9087",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
+   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.48",
+   "inputRev": "v0.0.50",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
+   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -135,10 +135,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "rev": "b2e8b6868397fcd93c00aca7278b933c16c0ffb3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "FLT",
diff --git a/lakefile.lean b/lakefile.lean
index 125bcbc6..cf368443 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -8,14 +8,14 @@ package FLT where
     ⟨`relaxedAutoImplicit, false⟩ -- switch off relaxed auto-implicit
   ]
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0"
+require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.16.0-rc1"
 
 require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 
 -- This is run only if we're in `dev` mode. This is so not everyone has to build doc-gen
 meta if get_config? env = some "dev" then
 require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "v4.15.0"
+  "https://github.com/leanprover/doc-gen4" @ "v4.16.0-rc1"
 
 @[default_target]
 lean_lib FLT where
diff --git a/lean-toolchain b/lean-toolchain
index d0eb99ff..62ccd717 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.16.0-rc1