diff --git a/lean-toolchain b/lean-toolchain
index b8f3deceb..7fad210be 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-08-27
+leanprover/lean4-pr-releases:pr-release-14968-d1863d1
diff --git a/mathlib4/Mathlib/Tactic/Translate/Core.lean b/mathlib4/Mathlib/Tactic/Translate/Core.lean
index 98bb65e31..e718491f0 100644
--- a/mathlib4/Mathlib/Tactic/Translate/Core.lean
+++ b/mathlib4/Mathlib/Tactic/Translate/Core.lean
@@ -902,7 +902,7 @@ def warnAttrCore (stx : Syntax) (f : Environment → Name → Bool)
       else ""
 
 /-- Warn the user when the declaration has a simple scoped attribute. -/
-def warnAttr {α β : Type} [Inhabited β] (stx : Syntax) (attr : SimpleScopedEnvExtension α β)
+def warnAttr {α β : Type} (stx : Syntax) (attr : SimpleScopedEnvExtension α β)
     (f : β → Name → Bool) (thisAttr attrName src tgt : Name) : CoreM Unit :=
   warnAttrCore stx (f <| attr.getState ·) thisAttr attrName src tgt