diff --git a/batteries/Batteries/Lean/LawfulMonad.lean b/batteries/Batteries/Lean/LawfulMonad.lean
index 221b9c885..e6e097258 100644
--- a/batteries/Batteries/Lean/LawfulMonad.lean
+++ b/batteries/Batteries/Lean/LawfulMonad.lean
@@ -31,7 +31,7 @@ instance : LawfulMonad BaseIO := inferInstanceAs <| LawfulMonad (ST _)
 instance : LawfulMonad IO := inferInstanceAs <| LawfulMonad (EIO _)
 
 instance : LawfulMonad CoreM :=
-  inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ (EIO Exception))
+  inferInstanceAs <| LawfulMonad (ReaderT _ <| ReaderT _ <| StateRefT' _ _ (EIO Exception))
 instance : LawfulMonad MetaM :=
   inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ CoreM)
 instance : LawfulMonad TermElabM :=
diff --git a/lean-toolchain b/lean-toolchain
index b8f3deceb..b4014a58e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-08-27
+leanprover/lean4-pr-releases:pr-release-14970-08499f9
diff --git a/mathlib4/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean b/mathlib4/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean
index c7d0506df..b5ca93d33 100644
--- a/mathlib4/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean
+++ b/mathlib4/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean
@@ -142,7 +142,8 @@ Note: It is expensive to create two new `IO.Ref`s for every `MetaM` operation,
   -- mstate.modify fun s => { cache := s.cache }
   -- cstate.modify fun s => { env := s.env, cache := s.cache, ngen := s.ngen }
   let mctx := { keyedConfig := Config.toConfigWithKey { transparency := .reducible } }
-  match ← (((act name constInfo) mctx mstate) cctx cstate).toBaseIO with
+  -- `0` is the initial recursion depth of `CoreM`'s recursion-depth reader layer
+  match ← (((act name constInfo) mctx mstate) cctx 0 cstate).toBaseIO with
   | .ok a =>
     return a.foldl (fun t (val, entries) =>
       entries.foldl (fun t (key, entry) => t.push key (entry, val)) t) tree
diff --git a/mathlib4/Mathlib/Tactic/ClickSuggestions/SectionState.lean b/mathlib4/Mathlib/Tactic/ClickSuggestions/SectionState.lean
index 1dd1f3752..b852be359 100644
--- a/mathlib4/Mathlib/Tactic/ClickSuggestions/SectionState.lean
+++ b/mathlib4/Mathlib/Tactic/ClickSuggestions/SectionState.lean
@@ -79,8 +79,8 @@ where
 def SectionState.insertResult (s : SectionState α) (res : Result α)
     (isDup : α → α → MetaM Bool) : MetaM (SectionState α) := do
   let { results, errors } := s
-  let results ← fun c₁ c₂ c₃ c₄ ↦
-    (res.insertInArray results isDup c₁ c₂ c₃ c₄).catchExceptions fun ex ↦ do
+  let results ← fun c₁ c₂ c₃ c₄ c₅ ↦
+    (res.insertInArray results isDup c₁ c₂ c₃ c₄ c₅).catchExceptions fun ex ↦ do
     if let .internal id _ := ex then
       if id == interruptExceptionId then
         return default