diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index eec5494f80..4a93db2782 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1662,6 +1662,14 @@ If there are several with the same priority, it is uses the "most recent one". E
 -/
 syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
 
+/--
+Theorems tagged with the `auto_attach` attribute are used during the processing of functions defined
+by well-founded recursion. They are applied to the function's body to add additional hypotheses,
+such as replacing `if c then _ else _` with `if h : c then _ else _` or `xs.map` with
+`xs.attach.map`. Also see `wfParam`.
+-/
+syntax (name := auto_attach) "auto_attach" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+
 /-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
 syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"
 
diff --git a/src/Lean/Elab/PreDefinition/WF/AutoAttach.lean b/src/Lean/Elab/PreDefinition/WF/AutoAttach.lean
new file mode 100644
index 0000000000..586c03708e
--- /dev/null
+++ b/src/Lean/Elab/PreDefinition/WF/AutoAttach.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+prelude
+import Lean.Meta.Transform
+import Lean.Meta.Match.MatcherApp.Basic
+import Lean.Elab.Tactic.Simp
+
+open Lean Meta
+
+namespace Lean.Elab.WF
+
+builtin_initialize autoAttachSimpExtension : SimpExtension ←
+  registerSimpAttr `auto_attach
+    "(not yet functional)"
+
+end Lean.Elab.WF
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index eb7ee40498..232582ff8a 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -13,6 +13,7 @@ import Lean.Elab.PreDefinition.WF.Rel
 import Lean.Elab.PreDefinition.WF.Fix
 import Lean.Elab.PreDefinition.WF.Unfold
 import Lean.Elab.PreDefinition.WF.Ite
+import Lean.Elab.PreDefinition.WF.AutoAttach
 import Lean.Elab.PreDefinition.WF.GuessLex
 
 namespace Lean.Elab
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index b647d85f37..51489f0e3c 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;