diff --git a/Manual/Grind.lean b/Manual/Grind.lean
index 9d29d94c..5f12dbaa 100644
--- a/Manual/Grind.lean
+++ b/Manual/Grind.lean
@@ -22,6 +22,9 @@ open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode
 
 set_option pp.rawOnError true
 
+-- TODO (@kim-em): `Lean.Grind.AddCommMonoid` and `Lean.Grind.AddCommGroup` are not yet documented.
+set_option verso.docstring.allowMissing true
+
 set_option linter.unusedVariables false
 
 -- The verso default max line length is 60, which is very restrictive.
@@ -1326,12 +1329,12 @@ Could not find a decreasing measure.
 The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
               #1 x2
-1) 1293:27-45  =  <
-2) 1294:27-45  =  <
-3) 1296:4-52   =  ?
-4) 1300:16-50  ?  _
-5) 1301:16-51  _  _
-6) 1303:16-50  _  _
+1) 1296:27-45  =  <
+2) 1297:27-45  =  <
+3) 1299:4-52   =  ?
+4) 1303:16-50  ?  _
+5) 1304:16-51  _  _
+6) 1306:16-50  _  _
 
 #1: assign
 
diff --git a/Manual/Releases/v4_22_0.lean b/Manual/Releases/v4_22_0.lean
index 5a2dd51e..5be3403e 100644
--- a/Manual/Releases/v4_22_0.lean
+++ b/Manual/Releases/v4_22_0.lean
@@ -12,7 +12,7 @@ open Manual
 open Verso.Genre
 
 
-#doc (Manual) "Lean 4.22.0-rc2 (2025-07-01)" =>
+#doc (Manual) "Lean 4.22.0-rc3 (2025-07-04)" =>
 %%%
 tag := "release-v4.22.0"
 file := "v4.22.0"
diff --git a/elan-init b/elan-init
new file mode 100755
index 00000000..3d14ee40
Binary files /dev/null and b/elan-init differ
diff --git a/lake-manifest.json b/lake-manifest.json
index 463eddc2..2b8e788e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "24694c2fbed4d6ef1b5c2fc9c55ae805ef4e731c",
+   "rev": "ba2618bedf2f6a866e7ef84ad6f47bb43a439a42",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ffe97dbb0002e15acd571649e93cecfb3d7c47d5",
+   "rev": "8d780d556de7ed7b1006805bcbc64959b8173e1d",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.lean b/lakefile.lean
index f0723e05..11dfd4fa 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -9,7 +9,7 @@ open Lake DSL
 open System (FilePath)
 
 require MD4Lean from git "https://github.com/acmepjz/md4lean"@"main"
-require verso from git "https://github.com/leanprover/verso.git"@"nightly-testing"
+require verso from git "https://github.com/leanprover/verso.git"@"main"
 
 package "verso-manual" where
   -- building the C code cost much more than the optimizations save
diff --git a/lean-toolchain b/lean-toolchain
index bfcebb12..fff0a20c 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.22.0-rc2
+leanprover/lean4:v4.22.0-rc3