diff --git a/src/Init/ByCases.lean b/src/Init/ByCases.lean
index 4f391e383f69..6e0a21841901 100644
--- a/src/Init/ByCases.lean
+++ b/src/Init/ByCases.lean
@@ -38,7 +38,8 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
   apply_dite f P (fun _ => x) (fun _ => y)
 
 /-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
-@[simp] theorem dite_eq_ite [Decidable P] : (dite P (fun _ => a) fun _ => b) = ite P a b := rfl
+@[simp] theorem dite_eq_ite [Decidable P] :
+  (dite P (fun _ => a) (fun _ => b)) = ite P a b := rfl
 
 @[deprecated "Use `ite_eq_right_iff`" (since := "2024-09-18")]
 theorem ite_some_none_eq_none [Decidable P] :
diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
index 45df7e263973..c83cd6b2875a 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -5,6 +5,7 @@ Author: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Init.Core
+import Init.BinderNameHint
 
 universe u v w
 
@@ -35,6 +36,12 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
   simp [h]
   rfl
 
+@[wf_preprocess] theorem forIn_eq_forin' [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m]
+    (x : ρ) (b : β) (f : (a : α) → β → m (ForInStep β)) :
+    forIn x b f = forIn' x b (fun x h => binderNameHint x f <| binderNameHint h () <| f x) := by
+  simp [binderNameHint]
+  rfl -- very strange why `simp` did not close it
+
 /-- Extract the value from a `ForInStep`, ignoring whether it is `done` or `yield`. -/
 def ForInStep.value (x : ForInStep α) : α :=
   match x with
diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean
index a1c9b6578d15..667465d00a62 100644
--- a/src/Init/Data/Array/Attach.lean
+++ b/src/Init/Data/Array/Attach.lean
@@ -650,6 +650,16 @@ and simplifies these to the function directly taking the value.
   rw [List.filterMap_subtype]
   simp [hf]
 
+
+@[simp] theorem flatMap_subtype {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → Array β} {g : α → Array β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    (l.flatMap f) = l.unattach.flatMap g := by
+  cases l
+  simp only [size_toArray, List.flatMap_toArray, List.unattach_toArray, List.length_unattach,
+    mk.injEq]
+  rw [List.flatMap_subtype]
+  simp [hf]
+
 @[simp] theorem findSome?_subtype {p : α → Prop} {l : Array { x // p x }}
     {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.findSome? f = l.unattach.findSome? g := by
@@ -695,4 +705,67 @@ and simplifies these to the function directly taking the value.
     (Array.mkArray n x).unattach = Array.mkArray n x.1 := by
   simp [unattach]
 
+/-! ### Well-founded recursion preprocessing setup -/
+
+@[wf_preprocess] theorem Array.map_wfParam (xs : Array α) (f : α → β) :
+    (wfParam xs).map f = xs.attach.unattach.map f := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem Array.map_unattach (P : α → Prop) (xs : Array (Subtype P)) (f : α → β) :
+    xs.unattach.map f = xs.map fun ⟨x, h⟩ =>
+      binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem foldl_wfParam (xs : Array α) (f : β → α → β) (x : β) :
+    (wfParam xs).foldl f x = xs.attach.unattach.foldl f x := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem foldl_unattach (P : α → Prop) (xs : Array (Subtype P)) (f : β → α → β) (x : β):
+    xs.unattach.foldl f x = xs.foldl (fun s ⟨x, h⟩ =>
+      binderNameHint s f <| binderNameHint x (f s) <| binderNameHint h () <| f s (wfParam x)) x := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem foldr_wfParam (xs : Array α) (f : α → β → β) (x : β) :
+    (wfParam xs).foldr f x = xs.attach.unattach.foldr f x := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem foldr_unattach (P : α → Prop) (xs : Array (Subtype P)) (f : α → β → β) (x : β):
+    xs.unattach.foldr f x = xs.foldr (fun ⟨x, h⟩ s =>
+      binderNameHint x f <| binderNameHint s (f x) <| binderNameHint h () <| f (wfParam x) s) x := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem filter_wfParam (xs : Array α) (f : α → Bool) :
+    (wfParam xs).filter f = xs.attach.unattach.filter f:= by
+  simp [wfParam]
+
+@[wf_preprocess] theorem filter_unattach (P : α → Prop) (xs : Array (Subtype P)) (f : α → Bool) :
+    xs.unattach.filter f = (xs.filter (fun ⟨x, h⟩ =>
+      binderNameHint x f <| binderNameHint h () <| f (wfParam x))).unattach := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem reverse_wfParam (xs : Array α) :
+    (wfParam xs).reverse = xs.attach.unattach.reverse := by simp [wfParam]
+
+@[wf_preprocess] theorem reverse_unattach (P : α → Prop) (xs : Array (Subtype P)) :
+    xs.unattach.reverse = xs.reverse.unattach := by simp
+
+@[wf_preprocess] theorem filterMap_wfParam (xs : Array α) (f : α → Option β) :
+    (wfParam xs).filterMap f = xs.attach.unattach.filterMap f := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem filterMap_unattach (P : α → Prop) (xs : Array (Subtype P)) (f : α → Option β) :
+    xs.unattach.filterMap f = xs.filterMap fun ⟨x, h⟩ =>
+      binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem flatMap_wfParam (xs : Array α) (f : α → Array β) :
+    (wfParam xs).flatMap f = xs.attach.unattach.flatMap f := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem flatMap_unattach (P : α → Prop) (xs : Array (Subtype P)) (f : α → Array β) :
+    xs.unattach.flatMap f = xs.flatMap fun ⟨x, h⟩ =>
+      binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
+  simp [wfParam]
+
+
 end Array
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index ee0468d4e3fe..f57dfaa75ea5 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 prelude
 import Init.Data.List.Count
 import Init.Data.Subtype
+import Init.BinderNameHint
 
 namespace List
 
@@ -796,4 +797,66 @@ and simplifies these to the function directly taking the value.
     (List.replicate n x).unattach = List.replicate n x.1 := by
   simp [unattach, -map_subtype]
 
+/-! ### Well-founded recursion preprocessing setup -/
+
+@[wf_preprocess] theorem map_wfParam (xs : List α) (f : α → β) :
+    (wfParam xs).map f = xs.attach.unattach.map f := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem map_unattach (P : α → Prop) (xs : List (Subtype P)) (f : α → β) :
+    xs.unattach.map f = xs.map fun ⟨x, h⟩ =>
+      binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem foldl_wfParam (xs : List α) (f : β → α → β) (x : β) :
+    (wfParam xs).foldl f x = xs.attach.unattach.foldl f x := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem foldl_unattach (P : α → Prop) (xs : List (Subtype P)) (f : β → α → β) (x : β):
+    xs.unattach.foldl f x = xs.foldl (fun s ⟨x, h⟩ =>
+      binderNameHint s f <| binderNameHint x (f s) <| binderNameHint h () <| f s (wfParam x)) x := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem foldr_wfParam (xs : List α) (f : α → β → β) (x : β) :
+    (wfParam xs).foldr f x = xs.attach.unattach.foldr f x := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem foldr_unattach (P : α → Prop) (xs : List (Subtype P)) (f : α → β → β) (x : β):
+    xs.unattach.foldr f x = xs.foldr (fun ⟨x, h⟩ s =>
+      binderNameHint x f <| binderNameHint s (f x) <| binderNameHint h () <| f (wfParam x) s) x := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem filter_wfParam (xs : List α) (f : α → Bool) :
+    (wfParam xs).filter f = xs.attach.unattach.filter f:= by
+  simp [wfParam]
+
+@[wf_preprocess] theorem filter_unattach (P : α → Prop) (xs : List (Subtype P)) (f : α → Bool) :
+    xs.unattach.filter f = (xs.filter (fun ⟨x, h⟩ =>
+      binderNameHint x f <| binderNameHint h () <| f (wfParam x))).unattach := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem reverse_wfParam (xs : List α) :
+    (wfParam xs).reverse = xs.attach.unattach.reverse := by simp [wfParam]
+
+@[wf_preprocess] theorem reverse_unattach (P : α → Prop) (xs : List (Subtype P)) :
+    xs.unattach.reverse = xs.reverse.unattach := by simp
+
+@[wf_preprocess] theorem filterMap_wfParam (xs : List α) (f : α → Option β) :
+    (wfParam xs).filterMap f = xs.attach.unattach.filterMap f := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem filterMap_unattach (P : α → Prop) (xs : List (Subtype P)) (f : α → Option β) :
+    xs.unattach.filterMap f = xs.filterMap fun ⟨x, h⟩ =>
+      binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem flatMap_wfParam (xs : List α) (f : α → List β) :
+    (wfParam xs).flatMap f = xs.attach.unattach.flatMap f := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem flatMap_unattach (P : α → Prop) (xs : List (Subtype P)) (f : α → List β) :
+    xs.unattach.flatMap f = xs.flatMap fun ⟨x, h⟩ =>
+      binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
+  simp [wfParam]
+
 end List
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 1eb65caa9fd5..ee457f370934 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -5,6 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.SizeOf
+import Init.BinderNameHint
 import Init.Data.Nat.Basic
 
 universe u v
@@ -414,3 +415,18 @@ theorem mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β 
 end
 
 end PSigma
+
+/--
+The `wfParam` gadget is used internally during the construction of recursive functions by
+wellfounded recursion, to keep track of the parameter for which the automatic introduction
+of `List.attach` (or similar) is plausible.
+-/
+def wfParam {α : Sort u} (a : α) : α := a
+
+/--
+Reverse direction of `dite_eq_ite`. Used by the well-founded definition preprocessor to extend the
+context of a termination proof inside `if-then-else` with the condition.
+-/
+@[wf_preprocess] theorem ite_eq_dite [Decidable P] :
+    ite P a b = (dite P (fun h => binderNameHint h () a) (fun h => binderNameHint h () b)) := by
+  rfl
diff --git a/src/Lean/Elab/PreDefinition/WF/AutoAttach.lean b/src/Lean/Elab/PreDefinition/WF/AutoAttach.lean
deleted file mode 100644
index 13cc559dc158..000000000000
--- a/src/Lean/Elab/PreDefinition/WF/AutoAttach.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-/-
-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 wfPreprocessSimpExtension : SimpExtension ←
-  registerSimpAttr `wf_preprocess
-    "(not yet functional)"
-
-end Lean.Elab.WF
diff --git a/src/Lean/Elab/PreDefinition/WF/FloatRecApp.lean b/src/Lean/Elab/PreDefinition/WF/FloatRecApp.lean
new file mode 100644
index 000000000000..b677f607d74c
--- /dev/null
+++ b/src/Lean/Elab/PreDefinition/WF/FloatRecApp.lean
@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Transform
+import Lean.Elab.RecAppSyntax
+
+namespace Lean.Elab.WF
+open Meta
+
+/--
+Preprocesses the expressions to improve the effectiveness of `wfRecursion`.
+
+* Floats out the RecApp markers.
+  Example:
+  ```
+  def f : Nat → Nat
+    | 0 => 1
+    | i+1 => (f x) i
+  ```
+
+Unlike `Lean.Elab.Structural.preprocess`, do _not_ beta-reduce, as it could
+remove `let_fun`-lambdas that contain explicit termination proofs.
+-/
+def floatRecApp (e : Expr) : CoreM Expr :=
+  Core.transform e
+    (post := fun e => do
+      if e.isApp && e.getAppFn.isMData then
+        let .mdata m f := e.getAppFn | unreachable!
+        if m.isRecApp then
+          return .done (.mdata m (f.beta e.getAppArgs))
+      return .continue)
+
+end Lean.Elab.WF
diff --git a/src/Lean/Elab/PreDefinition/WF/Ite.lean b/src/Lean/Elab/PreDefinition/WF/Ite.lean
deleted file mode 100644
index 4634b16f13ca..000000000000
--- a/src/Lean/Elab/PreDefinition/WF/Ite.lean
+++ /dev/null
@@ -1,30 +0,0 @@
-/-
-Copyright (c) 2022 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Transform
-
-namespace Lean.Meta
-
-/--
-  Convert `ite` expressions in `e` to `dite`s.
-  It is useful to make this conversion in the `WF` module because the condition is often used in
-  termination proofs. -/
-def iteToDIte (e : Expr) : MetaM Expr := do
-  -- TODO: move this file to `Meta` if we decide to use it in other places.
-  let post (e : Expr) : MetaM TransformStep := do
-    if e.isAppOfArity ``ite 5 then
-      let f    := e.getAppFn
-      let args := e.getAppArgs
-      let c    := args[1]!
-      let h    ← mkFreshUserName `h
-      let args := args.set! 3 (Lean.mkLambda h BinderInfo.default c args[3]!)
-      let args := args.set! 4 (Lean.mkLambda h BinderInfo.default (mkNot c) args[4]!)
-      return .done <| mkAppN (mkConst ``dite f.constLevels!) args
-    else
-      return .done e
-  transform e (post := post)
-
-end Lean.Meta
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index 232582ff8a23..88694c98776b 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -8,12 +8,11 @@ import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.TerminationMeasure
 import Lean.Elab.PreDefinition.Mutual
 import Lean.Elab.PreDefinition.WF.PackMutual
-import Lean.Elab.PreDefinition.WF.Preprocess
+import Lean.Elab.PreDefinition.WF.FloatRecApp
 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.Preprocess
 import Lean.Elab.PreDefinition.WF.GuessLex
 
 namespace Lean.Elab
@@ -23,8 +22,8 @@ open Meta
 def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) : TermElabM Unit := do
   let termMeasures? := termMeasure?s.mapM id -- Either all or none, checked by `elabTerminationByHints`
   let preDefs ← preDefs.mapM fun preDef =>
-    return { preDef with value := (← preprocess preDef.value) }
-  let (fixedPrefixSize, argsPacker, unaryPreDef) ← withoutModifyingEnv do
+    return { preDef with value := (← floatRecApp preDef.value) }
+  let (fixedPrefixSize, argsPacker, unaryPreDef, wfPreprocessProofs) ← withoutModifyingEnv do
     for preDef in preDefs do
       addAsAxiom preDef
     let fixedPrefixSize ← Mutual.getFixedPrefix preDefs
@@ -34,8 +33,10 @@ def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option T
       if varNames.isEmpty then
         throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments"
     let argsPacker := { varNamess }
-    let preDefsDIte ← preDefs.mapM fun preDef => return { preDef with value := (← iteToDIte preDef.value) }
-    return (fixedPrefixSize, argsPacker, ← packMutual fixedPrefixSize argsPacker preDefsDIte)
+    let (preDefsAttached, wfPreprocessProofs) ← Array.unzip <$> preDefs.mapM fun preDef => do
+      let result ← preprocess preDef.value
+      return ({preDef with value := result.expr}, result)
+    return (fixedPrefixSize, argsPacker, ← packMutual fixedPrefixSize argsPacker preDefsAttached, wfPreprocessProofs)
 
   let wf : TerminationMeasures ← do
     if let some tms := termMeasures? then pure tms else
@@ -62,10 +63,10 @@ def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option T
   Mutual.addPreDefsFromUnary preDefs preDefsNonrec preDefNonRec
   let preDefs ← Mutual.cleanPreDefs preDefs
   registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
-  for preDef in preDefs do
+  for preDef in preDefs, wfPreprocessProof in wfPreprocessProofs do
     unless preDef.kind.isTheorem do
       unless (← isProp preDef.type) do
-        WF.mkUnfoldEq preDef preDefNonRec.declName
+        WF.mkUnfoldEq preDef preDefNonRec.declName wfPreprocessProof
   Mutual.addPreDefAttributes preDefs
 
 builtin_initialize registerTraceClass `Elab.definition.wf
diff --git a/src/Lean/Elab/PreDefinition/WF/Preprocess.lean b/src/Lean/Elab/PreDefinition/WF/Preprocess.lean
index 27cdd7b93bf7..4180110505fe 100644
--- a/src/Lean/Elab/PreDefinition/WF/Preprocess.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Preprocess.lean
@@ -1,42 +1,140 @@
 /-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Joachim Breitner
 -/
 prelude
 import Lean.Meta.Transform
-import Lean.Elab.RecAppSyntax
+import Lean.Meta.Match.MatcherApp.Basic
+import Lean.Elab.Tactic.Simp
+
+/-!
+This module implements the preprocessing of function definitions involved in well-founded recursion.
+The goal is to change higher order functions to add more information to the context, e.g. change
+`List.map (fun x => …) xs` to `List.map (fun ⟨x, h⟩ => …) xs.attach`.  This extra information can
+then be used by the termination proof tactic to determine that a recursive call is indeed
+decreasing.
+
+The process proceeds in these steps, to guide the transformation:
+
+1. The parameters of the function are annotated with the `wfParam` gadget.
+
+   We could be more selective here and only annotate those that have a `SizeOf` instance.
+   We cannot (easily) only consider the parameters that appear in the termination measure, as that
+   is not known yet.
+
+
+2. The `wfParam` gadget is pushed around:
+
+   - `f (wfParam x) ==> wfParam (f x)` if `f` is a projection
+
+   - `match (wfParam x) with con y => alt[y] ==> match x with con y => alt[wfParam y]`
+
+     In a match with multiple targets it suffices for any of the targets to be annotated with
+     `wfParam`, and all parameters of the match arms are annotated with `wfParam`. This is an
+     overapproximation.
+
+3. The `wf_preprocess` simpset is applied to do the actual transformation. It typically contains two
+   rules for each higher-order function of interest
+
+   - `(wfParam xs).map f = xs.attach.unattach.map f`
+   - `xs.unattach.map f = xs.map (fun ⟨x, h⟩ => binderNameHint x f (f (wfParam x)))`
+
+   The first rule “activates” the call, the second rule actually performs it. They are separated like
+   this so that for chains of the form `(xs.reverse.filter p).map f` the `.attach` is attached
+   to `xs` and we get the basic `x ∈ xs` in the context of `f`.
+
+   The `binderNameHint` preserves the user-chosen name in `f` if that is a lambda.
+
+   The `wfParam` on the right hand side ensurses that doubly-nested recursion works.
+
+4. All left-over `wfParam` gadgets are removed.
+
+The simplifier is used to perform steps 2 (using simprocs) and 3 (using rewrite rules) together.
+
+-/
+
+open Lean Meta
+
+register_builtin_option wf.preprocess : Bool := {
+  defValue := true
+  descr := "pre-process definitions defined by well-founded recursion with the `wf_preprocess` simp set"
+}
 
 namespace Lean.Elab.WF
-open Meta
 
-private def shouldBetaReduce (e : Expr) (recFnNames : Array Name) : Bool :=
-  if e.isHeadBetaTarget then
-    e.getAppFn.find? (fun e => recFnNames.any (e.isConstOf ·)) |>.isSome
+builtin_initialize wfPreprocessSimpExtension : SimpExtension ←
+  registerSimpAttr `wf_preprocess
+    "simp lemma used in the preprocessing of well-founded recursive function definitions, in \
+    particular to add additional hypotheses to the context. Also see `wfParam`."
+
+private def getSimpContext : MetaM Simp.Context := do
+  let simpTheorems ← wfPreprocessSimpExtension.getTheorems
+  Simp.mkContext
+    (simpTheorems  := #[simpTheorems])
+    (congrTheorems := {})
+    (config        := { Simp.neutralConfig with dsimp := false })
+
+def isWfParam? (e : Expr) : Option Expr :=
+  if e.isAppOfArity ``wfParam 2 then
+    e.appArg!
   else
-    false
+    none
 
-/--
-Preprocesses the expressions to improve the effectiveness of `wfRecursion`.
+def mkWfParam (e : Expr) : MetaM Expr :=
+  mkAppM ``wfParam #[e]
 
-* Floats out the RecApp markers.
-  Example:
-  ```
-  def f : Nat → Nat
-    | 0 => 1
-    | i+1 => (f x) i
-  ```
+/-- `f (wfParam x) ==> wfParam (f x)` if `f` is a projection -/
+builtin_dsimproc paramProj (_) := fun e => do
+  if h : e.isApp then
+    let some a' := isWfParam? (e.appArg h) | return .continue
+    let f := e.getAppFn
+    unless f.isConst do return .continue
+    unless (← isProjectionFn f.constName!) do return .continue
+    let e' ← mkWfParam (.app (e.appFn h) a')
+    return .done e'
+  else
+    return .continue
 
-Unlike `Lean.Elab.Structural.preprocess`, do _not_ beta-reduce, as it could
-remove `let_fun`-lambdas that contain explicit termination proofs.
--/
-def preprocess (e : Expr) : CoreM Expr :=
-  Core.transform e
-    (post := fun e => do
-      if e.isApp && e.getAppFn.isMData then
-        let .mdata m f := e.getAppFn | unreachable!
-        if m.isRecApp then
-          return .done (.mdata m (f.beta e.getAppArgs))
-      return .continue)
+/-- `match (wfParam x) with con y => alt[y] ==> match x with con y => alt[wfParam y] -/
+builtin_dsimproc paramMatcher (_) := fun e => do
+  let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true)  | return .continue
+  unless matcherApp.discrs.any (isWfParam? · |>.isSome) do return .continue
+  let discrs' := matcherApp.discrs.map (fun e => isWfParam? e |>.getD e)
+  let alts' ← matcherApp.alts.mapM fun alt =>
+    lambdaTelescope alt fun xs body => do
+      -- Annotate all xs with `wfParam`
+      let xs' ← xs.mapM (mkWfParam ·)
+      let body' := body.replaceFVars xs xs'
+      mkLambdaFVars xs body'
+  let matcherApp' := { matcherApp with discrs := discrs', alts := alts' }
+  return .continue <| matcherApp'.toExpr
+
+
+def preprocess (e : Expr) : MetaM Simp.Result := do
+  unless wf.preprocess.get (← getOptions) do
+    return { expr := e }
+  lambdaTelescope e fun xs _ => do
+    -- Annotate all xs with `wfParam`
+    let xs' ← xs.mapM mkWfParam
+    let e' := e.beta xs'
+
+    -- Now run the simplifier
+    let simprocs : Simprocs := {}
+    let simprocs ← simprocs.add ``paramProj (post := true)
+    let simprocs ← simprocs.add ``paramMatcher (post := false)
+    let (result, _) ← Meta.simp e' (← getSimpContext) (simprocs := #[simprocs])
+
+    -- Remove left-over markers
+    let e'' ← Core.transform result.expr fun e =>
+      e.withApp fun f as => do
+        if f.isConstOf ``wfParam then
+          if h : as.size ≥ 2 then
+            return .continue (mkAppN as[1] as[2:])
+        return .continue
+    let result := { result with expr := e'' }
+
+    trace[Elab.definition.wf] "Attach-introduction:{indentExpr e}\nto{indentExpr e'}\ncleaned up as{indentExpr e''}"
+    result.addLambdas xs
 
 end Lean.Elab.WF
diff --git a/src/Lean/Elab/PreDefinition/WF/Unfold.lean b/src/Lean/Elab/PreDefinition/WF/Unfold.lean
index 51145eccb988..9032d7a766da 100644
--- a/src/Lean/Elab/PreDefinition/WF/Unfold.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Unfold.lean
@@ -37,60 +37,60 @@ private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   mvarId.assign (← mkEqTrans h mvarNew)
   return mvarNew.mvarId!
 
-private partial def mkUnfoldProof (declName declNameNonRec : Name) (type : Expr) : MetaM Expr := do
-  trace[Elab.definition.wf.eqns] "proving: {type}"
-  withNewMCtxDepth do
-    let main ← mkFreshExprSyntheticOpaqueMVar type
-    let (_, mvarId) ← main.mvarId!.intros
-    let rec go (mvarId : MVarId) : MetaM Unit := do
-      trace[Elab.definition.wf.eqns] "step\n{MessageData.ofGoal mvarId}"
-      if ← withAtLeastTransparency .all (tryURefl mvarId) then
-        trace[Elab.definition.wf.eqns] "refl!"
-        return ()
-      else if (← tryContradiction mvarId) then
-        trace[Elab.definition.wf.eqns] "contradiction!"
-        return ()
-      else if let some mvarId ← simpMatch? mvarId then
-        trace[Elab.definition.wf.eqns] "simpMatch!"
-        go mvarId
-      else if let some mvarId ← simpIf? mvarId then
-        trace[Elab.definition.wf.eqns] "simpIf!"
-        go mvarId
-      else if let some mvarId ← whnfReducibleLHS? mvarId then
-        trace[Elab.definition.wf.eqns] "whnfReducibleLHS!"
-        go mvarId
+private partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
+  trace[Elab.definition.wf.eqns] "step\n{MessageData.ofGoal mvarId}"
+  if ← withAtLeastTransparency .all (tryURefl mvarId) then
+    trace[Elab.definition.wf.eqns] "refl!"
+    return ()
+  else if (← tryContradiction mvarId) then
+    trace[Elab.definition.wf.eqns] "contradiction!"
+    return ()
+  else if let some mvarId ← simpMatch? mvarId then
+    trace[Elab.definition.wf.eqns] "simpMatch!"
+    mkUnfoldProof declName mvarId
+  else if let some mvarId ← simpIf? mvarId then
+    trace[Elab.definition.wf.eqns] "simpIf!"
+    mkUnfoldProof declName mvarId
+  else if let some mvarId ← whnfReducibleLHS? mvarId then
+    trace[Elab.definition.wf.eqns] "whnfReducibleLHS!"
+    mkUnfoldProof declName mvarId
+  else
+    let ctx ← Simp.mkContext (config := { dsimp := false, etaStruct := .none })
+    match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
+    | TacticResultCNM.closed => return ()
+    | TacticResultCNM.modified mvarId =>
+      trace[Elab.definition.wf.eqns] "simp only!"
+      mkUnfoldProof declName mvarId
+    | TacticResultCNM.noChange =>
+      if let some mvarIds ← casesOnStuckLHS? mvarId then
+        trace[Elab.definition.wf.eqns] "case split into {mvarIds.size} goals"
+        mvarIds.forM (mkUnfoldProof declName)
+      else if let some mvarIds ← splitTarget? mvarId then
+        trace[Elab.definition.wf.eqns] "splitTarget into {mvarIds.length} goals"
+        mvarIds.forM (mkUnfoldProof declName)
       else
-        let ctx ← Simp.mkContext (config := { dsimp := false, etaStruct := .none })
-        match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
-        | TacticResultCNM.closed => return ()
-        | TacticResultCNM.modified mvarId =>
-          trace[Elab.definition.wf.eqns] "simp only!"
-          go mvarId
-        | TacticResultCNM.noChange =>
-          if let some mvarIds ← casesOnStuckLHS? mvarId then
-            trace[Elab.definition.wf.eqns] "case split into {mvarIds.size} goals"
-            mvarIds.forM go
-          else if let some mvarIds ← splitTarget? mvarId then
-            trace[Elab.definition.wf.eqns] "splitTarget into {mvarIds.length} goals"
-            mvarIds.forM go
-          else
-            -- At some point in the past, we looked for occurrences of Wf.fix to fold on the
-            -- LHS (introduced in 096e4eb), but it seems that code path was never used,
-            -- so #3133 removed it again (and can be recovered from there if this was premature).
-            throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
+        -- At some point in the past, we looked for occurrences of Wf.fix to fold on the
+        -- LHS (introduced in 096e4eb), but it seems that code path was never used,
+        -- so #3133 removed it again (and can be recovered from there if this was premature).
+        throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
 
-    let mvarId ← if declName != declNameNonRec then deltaLHS mvarId else pure mvarId
-    let mvarId ← rwFixEq mvarId
-    go mvarId
-    instantiateMVars main
-
-def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) : MetaM Unit := do
+def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) (wfPreprocessProof : Simp.Result) : MetaM Unit := do
   withOptions (tactic.hygienic.set · false) do
     let baseName := preDef.declName
     lambdaTelescope preDef.value fun xs body => do
       let us := preDef.levelParams.map mkLevelParam
-      let type ← mkEq (mkAppN (Lean.mkConst preDef.declName us) xs) body
-      let value ← mkUnfoldProof preDef.declName unaryPreDefName type
+      let lhs := mkAppN (Lean.mkConst preDef.declName us) xs
+      let type ← mkEq lhs body
+
+      let main ← mkFreshExprSyntheticOpaqueMVar type
+      let mvarId := main.mvarId!
+      let wfPreprocessProof ← Simp.mkCongr { expr := type.appFn! } (← wfPreprocessProof.addExtraArgs xs)
+      let mvarId ← applySimpResultToTarget mvarId type wfPreprocessProof
+      let mvarId ← if preDef.declName != unaryPreDefName then deltaLHS mvarId else pure mvarId
+      let mvarId ← rwFixEq mvarId
+      mkUnfoldProof preDef.declName mvarId
+
+      let value ← instantiateMVars main
       let type ← mkForallFVars xs type
       let value ← mkLambdaFVars xs value
       let name := Name.str baseName unfoldThmSuffix
diff --git a/src/Lean/Meta/BinderNameHint.lean b/src/Lean/Meta/BinderNameHint.lean
index 3e8391da9bcc..3dcb462ebf75 100644
--- a/src/Lean/Meta/BinderNameHint.lean
+++ b/src/Lean/Meta/BinderNameHint.lean
@@ -63,9 +63,9 @@ and the innermost binder is at the end. We update the binder names therein when
           modify (rememberName bidx n)
         | .bvar bidx, _ =>
           -- If we do not have a binder to use, ensure that name has macro scope.
-          -- This is used by the auto-attach lemmas so that the new binder `fun h =>`
-          -- has a macro-scope, and is inaccessible in the termination proof.
-          -- (Using `fun _ =>` causes `property†` to appear, which is bad UX)
+          -- This is used by the well-founded definition preprocessor so that the new binder
+          -- `fun h =>` has a macro-scope, and is inaccessible in the termination proof.
+          -- (Using `fun _ =>` would show up as `property†` to appear, which is bad UX)
           let xs ← get
           assert! xs.size > bidx
           let n := xs[xs.size - bidx - 1]!
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index ada06f05764a..5ba09d8850d0 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -299,13 +299,7 @@ def simpConst (e : Expr) : SimpM Result :=
 def simpLambda (e : Expr) : SimpM Result :=
   withParent e <| lambdaTelescopeDSimp e fun xs e => withNewLemmas xs do
     let r ← simp e
-    let eNew ← mkLambdaFVars xs r.expr
-    match r.proof? with
-    | none   => return { expr := eNew }
-    | some h =>
-      let p ← xs.foldrM (init := h) fun x h => do
-        mkFunExt (← mkLambdaFVars #[x] h)
-      return { expr := eNew, proof? := p }
+    r.addLambdas xs
 
 def simpArrow (e : Expr) : SimpM Result := do
   trace[Debug.Meta.Tactic.simp] "arrow {e}"
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index e86c445ad128..9c4f4becf1aa 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -772,6 +772,15 @@ def DStep.addExtraArgs (s : DStep) (extraArgs : Array Expr) : DStep :=
   | .continue none => .continue none
   | .continue (some eNew) => .continue (mkAppN eNew extraArgs)
 
+def Result.addLambdas (r : Result) (xs : Array Expr) : MetaM Result := do
+  let eNew ← mkLambdaFVars xs r.expr
+  match r.proof? with
+  | none   => return { expr := eNew }
+  | some h =>
+    let p ← xs.foldrM (init := h) fun x h => do
+      mkFunExt (← mkLambdaFVars #[x] h)
+    return { expr := eNew, proof? := p }
+
 end Simp
 
 export Simp (SimpM Simprocs)
diff --git a/tests/lean/run/wfWithSidecondition.lean b/tests/lean/run/wfWithSidecondition.lean
new file mode 100644
index 000000000000..be912b186fcd
--- /dev/null
+++ b/tests/lean/run/wfWithSidecondition.lean
@@ -0,0 +1,114 @@
+section setup
+
+variable {α : Sort u}
+variable {β : α → Sort v}
+variable {γ : Sort w}
+
+def callsOn (P : α → Prop) (F : (∀ y, β y) → γ) :=
+  ∃ (F': (∀ y, P y → β y) → γ), ∀ f, F' (fun y _ => f y) = F f
+
+variable (R : α → α → Prop)
+variable (F : (∀ y, β y) → (∀ x, β x))
+
+local infix:50 " ≺ " => R
+
+def recursesVia : Prop := ∀ x, callsOn (· ≺ x) (fun f => F f x)
+
+noncomputable def fix (wf : WellFounded R) (h : recursesVia R F) : (∀ x, β x) :=
+  wf.fix (fun x => (h x).choose)
+
+def fix_eq (wf : WellFounded R) h x : fix R F wf h x = F (fix R F wf h) x := by
+  unfold fix
+  rw [wf.fix_eq]
+  apply (h x).choose_spec
+
+theorem callsOn_base (y : α) (hy : P y) : callsOn P (fun (f : ∀ x, β x) => f y) := by
+  exists fun f => f y hy
+  intros; rfl
+
+@[simp]
+theorem callsOn_const (x : γ) : callsOn P (fun (_ : ∀ x, β x) => x) :=
+  ⟨fun _ => x, fun _ => rfl⟩
+
+theorem callsOn_app
+  {γ₁ : Sort uu} {γ₂ : Sort ww}
+  (F₁ :  (∀ y, β y) → γ₂ → γ₁) -- can this also support dependent types?
+  (F₂ :  (∀ y, β y) → γ₂)
+  (h₁ : callsOn P F₁)
+  (h₂ : callsOn P F₂) :
+  callsOn P (fun f => F₁ f (F₂ f)) := by
+  obtain ⟨F₁', h₁⟩ := h₁
+  obtain ⟨F₂', h₂⟩ := h₂
+  exists (fun f => F₁' f (F₂' f))
+  intros; simp_all
+
+theorem callsOn_lam
+  {γ₁ : Sort uu}
+  (F : γ₁ → (∀ y, β y) → γ) -- can this also support dependent types?
+  (h : ∀ x, callsOn P (F x)) :
+  callsOn P (fun f x => F x f) := by
+  exists (fun f x => (h x).choose f)
+  intro f
+  ext x
+  apply (h x).choose_spec
+
+theorem callsOn_app2
+  {γ₁ : Sort uu} {γ₂ : Sort ww}
+  (g : γ₁ → γ₂ → γ)
+  (F₁ :  (∀ y, β y) → γ₁) -- can this also support dependent types?
+  (F₂ :  (∀ y, β y) → γ₂)
+  (h₁ : callsOn P F₁)
+  (h₂ : callsOn P F₂) :
+  callsOn P (fun f => g (F₁ f) (F₂ f)) := by
+  apply_rules [callsOn_app, callsOn_const]
+
+theorem callsOn_map (δ : Type uu) (γ : Type ww)
+    (P : α → Prop) (F : (∀ y, β y) → δ → γ) (xs : List δ)
+    (h : ∀ x, x ∈ xs → callsOn P (fun f => F f x)) :
+  callsOn P (fun f => xs.map (fun x => F f x)) := by
+  suffices callsOn P (fun f => xs.attach.map (fun ⟨x, h⟩ => F f x)) by
+    simpa
+  apply callsOn_app
+  · apply callsOn_app
+    · apply callsOn_const
+    · apply callsOn_lam
+      intro ⟨x', hx'⟩
+      dsimp
+      exact (h x' hx')
+  · apply callsOn_const
+
+end setup
+
+section examples
+
+structure Tree (α : Type u) where
+  val : α
+  cs : List (Tree α)
+
+noncomputable def List.map' (f : α → β) : List α → List β :=
+  fix (sizeOf · < sizeOf ·) (fun map l => match l with | [] => [] | x::xs => f x :: map xs)
+    (InvImage.wf (sizeOf ·) WellFoundedRelation.wf) <| by
+  intro l
+  dsimp only
+  cases l -- check that the predicate of `callsOn` is appropriately refined
+  · simp
+  · simp only [cons.sizeOf_spec, sizeOf_default, Nat.add_zero]
+    apply callsOn_app2
+    · apply callsOn_const
+    · apply callsOn_base
+      simp
+
+noncomputable def Tree.map (f : α → β) : Tree α → Tree β :=
+  fix (sizeOf · < sizeOf ·) (fun map t => ⟨f t.val, t.cs.map map⟩)
+    (InvImage.wf (sizeOf ·) WellFoundedRelation.wf) <| by
+  intro ⟨v, cs⟩
+  dsimp only
+  apply callsOn_app2
+  · apply callsOn_const
+  · apply callsOn_map
+    intro t' ht'
+    apply callsOn_base
+    decreasing_trivial
+
+
+end examples
diff --git a/tests/lean/run/wf_preprocess.lean b/tests/lean/run/wf_preprocess.lean
new file mode 100644
index 000000000000..609c53e2e7fe
--- /dev/null
+++ b/tests/lean/run/wf_preprocess.lean
@@ -0,0 +1,276 @@
+set_option Elab.async false -- for stable output order in #guard_msgs
+
+universe u
+structure Tree (α : Type u) where
+  val : α
+  cs : List (Tree α)
+
+def Tree.isLeaf (t : Tree α) := t.cs.isEmpty
+
+/--
+info: α : Type u_1
+t t' : Tree α
+h✝ : t' ∈ t.cs
+⊢ sizeOf t' < sizeOf t
+-/
+#guard_msgs in
+def Tree.map (f : α → β) (t : Tree α) : Tree β :=
+    ⟨f t.val, t.cs.map (fun t' => t'.map f)⟩
+termination_by t
+decreasing_by trace_state; cases t; decreasing_tactic
+
+/--
+info: equations:
+theorem Tree.map.eq_1.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : Tree α),
+  Tree.map f t = { val := f t.val, cs := List.map (fun t' => Tree.map f t') t.cs }
+-/
+#guard_msgs in
+#print equations Tree.map
+
+/--
+info: Tree.map.induct.{u_1} {α : Type u_1} (motive : Tree α → Prop)
+  (case1 : ∀ (x : Tree α), (∀ (t' : Tree α), t' ∈ x.cs → motive t') → motive x) (t : Tree α) : motive t
+-/
+#guard_msgs in
+#check Tree.map.induct
+
+/--
+info: α : Type u_1
+t x✝ : Tree α
+h✝ : x✝ ∈ t.cs
+⊢ sizeOf x✝ < sizeOf t
+-/
+#guard_msgs in
+def Tree.pruneRevAndMap (f : α → β) (t : Tree α) : Tree β :=
+    ⟨f t.val, (t.cs.filter (fun t' => not t'.isLeaf)).reverse.map (·.pruneRevAndMap f)⟩
+termination_by t
+decreasing_by trace_state; cases t; decreasing_tactic
+
+/--
+info: equations:
+theorem Tree.pruneRevAndMap.eq_1.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : Tree α),
+  Tree.pruneRevAndMap f t =
+    { val := f t.val,
+      cs := List.map (fun x => Tree.pruneRevAndMap f x) (List.filter (fun t' => !t'.isLeaf) t.cs).reverse }
+-/
+#guard_msgs in
+#print equations Tree.pruneRevAndMap
+
+/--
+info: Tree.pruneRevAndMap.induct.{u_1} {α : Type u_1} (motive : Tree α → Prop)
+  (case1 : ∀ (x : Tree α), (∀ (x_1 : Tree α), x_1 ∈ x.cs → motive x_1) → motive x) (t : Tree α) : motive t
+-/
+#guard_msgs in
+#check Tree.pruneRevAndMap.induct
+
+/--
+info: α : Type u_1
+v : α
+cs : List (Tree α)
+x✝ : Tree α
+h✝ : x✝ ∈ cs
+⊢ sizeOf x✝ < sizeOf { val := v, cs := cs }
+-/
+#guard_msgs in
+def Tree.pruneRevAndMap' (f : α → β) : Tree α → Tree β
+  | ⟨v,cs⟩ => ⟨f v, (cs.filter (fun t' => not t'.isLeaf)).reverse.map (·.pruneRevAndMap' f)⟩
+termination_by t => t
+decreasing_by trace_state; decreasing_tactic
+
+/--
+info: equations:
+theorem Tree.pruneRevAndMap'.eq_1.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (v : α) (cs : List (Tree α)),
+  Tree.pruneRevAndMap' f { val := v, cs := cs } =
+    { val := f v, cs := List.map (fun x => Tree.pruneRevAndMap' f x) (List.filter (fun t' => !t'.isLeaf) cs).reverse }
+-/
+#guard_msgs in
+#print equations Tree.pruneRevAndMap'
+
+/--
+info: Tree.pruneRevAndMap'.induct.{u_1} {α : Type u_1} (motive : Tree α → Prop)
+  (case1 : ∀ (v : α) (cs : List (Tree α)), (∀ (x : Tree α), x ∈ cs → motive x) → motive { val := v, cs := cs })
+  (a✝ : Tree α) : motive a✝
+-/
+#guard_msgs in
+#check Tree.pruneRevAndMap'.induct
+
+structure MTree (α : Type u) where
+  val : α
+  cs : Array (List (MTree α))
+
+-- set_option trace.Elab.definition.wf true in
+/--
+warning: declaration uses 'sorry'
+---
+info: α : Type u_1
+t : MTree α
+x✝¹ : List (MTree α)
+h✝¹ : x✝¹ ∈ t.cs
+x✝ : MTree α
+h✝ : x✝ ∈ x✝¹
+⊢ sizeOf x✝ < sizeOf t
+-/
+#guard_msgs in
+def MTree.map (f : α → β) (t : MTree α) : MTree β :=
+    ⟨f t.val, t.cs.map (·.map (·.map f))⟩
+termination_by t
+decreasing_by trace_state; cases t; simp at *; decreasing_tactic; sorry
+
+/--
+info: equations:
+theorem MTree.map.eq_1.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : MTree α),
+  MTree.map f t = { val := f t.val, cs := Array.map (fun x => List.map (fun x => MTree.map f x) x) t.cs }
+-/
+#guard_msgs in
+#print equations MTree.map
+
+/--
+info: MTree.map.induct.{u_1} {α : Type u_1} (motive : MTree α → Prop)
+  (case1 : ∀ (x : MTree α), (∀ (x_1 : List (MTree α)), x_1 ∈ x.cs → ∀ (x : MTree α), x ∈ x_1 → motive x) → motive x)
+  (t : MTree α) : motive t
+-/
+#guard_msgs in
+#check MTree.map.induct
+
+/--
+info: α : Type u_1
+t : MTree α
+css : List (MTree α)
+h✝¹ : css ∈ t.cs
+c : MTree α
+h✝ : c ∈ css
+⊢ sizeOf c < sizeOf t
+-/
+#guard_msgs in
+def MTree.size (t : MTree α) : Nat := Id.run do
+  let mut s := 1
+  for css in t.cs do
+    for c in css do
+      s := s + c.size
+  pure s
+termination_by t
+decreasing_by
+  trace_state
+  fail_if_success grind -- eventually, grind should be able to handle this
+  cases t
+  have := Array.sizeOf_lt_of_mem ‹_ ∈ _›
+  have := List.sizeOf_lt_of_mem ‹_ ∈ _›
+  simp only [mk.sizeOf_spec, sizeOf_default, Nat.add_zero, gt_iff_lt] at *
+  omega
+
+/--
+info: equations:
+theorem MTree.size.eq_1.{u_1} : ∀ {α : Type u_1} (t : MTree α),
+  t.size =
+    (let s := 1;
+      do
+      let r ←
+        forIn t.cs s fun css r =>
+            let s := r;
+            do
+            let r ←
+              forIn css s fun c r =>
+                  let s := r;
+                  let s := s + c.size;
+                  do
+                  pure PUnit.unit
+                  pure (ForInStep.yield s)
+            let s : Nat := r
+            pure PUnit.unit
+            pure (ForInStep.yield s)
+      let s : Nat := r
+      pure s).run
+-/
+#guard_msgs in
+#print equations MTree.size
+
+/--
+info: MTree.size.induct.{u_1} {α : Type u_1} (motive : MTree α → Prop)
+  (case1 : ∀ (x : MTree α), (∀ (css : List (MTree α)), css ∈ x.cs → ∀ (c : MTree α), c ∈ css → motive c) → motive x)
+  (t : MTree α) : motive t
+-/
+#guard_msgs in
+#check MTree.size.induct
+
+namespace Ex1
+inductive Expression where
+| var: String → Expression
+| object: List (String × Expression) → Expression
+
+/--
+warning: declaration uses 'sorry'
+---
+info: L : List (String × Expression)
+x : String × Expression
+h✝ : x ∈ L
+⊢ sizeOf x.snd < sizeOf (Expression.object L)
+-/
+#guard_msgs in
+def t (exp: Expression) : List String :=
+  match exp with
+  | Expression.var s => [s]
+  | Expression.object L => List.foldl (fun L1 L2 => L1 ++ L2) [] (L.map (fun x => t x.2))
+termination_by exp
+decreasing_by trace_state; sorry
+
+/--
+info: equations:
+theorem Ex1.t.eq_1 : ∀ (s : String), t (Expression.var s) = [s]
+theorem Ex1.t.eq_2 : ∀ (L : List (String × Expression)),
+  t (Expression.object L) = List.foldl (fun L1 L2 => L1 ++ L2) [] (List.map (fun x => t x.snd) L)
+-/
+#guard_msgs in
+#print equations t
+
+/--
+info: Ex1.t.induct (motive : Expression → Prop) (case1 : ∀ (s : String), motive (Expression.var s))
+  (case2 :
+    ∀ (L : List (String × Expression)), (∀ (x : String × Expression), motive x.snd) → motive (Expression.object L))
+  (exp : Expression) : motive exp
+-/
+#guard_msgs in
+#check t.induct
+
+end Ex1
+
+namespace Ex2
+inductive Expression where
+| var: String → Expression
+| object: List (String × Expression) → Expression
+
+/--
+warning: declaration uses 'sorry'
+---
+info: L : List (String × Expression)
+x : String × Expression
+h✝ : x ∈ L
+⊢ sizeOf x.snd < sizeOf (Expression.object L)
+-/
+#guard_msgs in
+def t (exp: Expression) : List String :=
+  match exp with
+  | Expression.var s => [s]
+  | Expression.object L => L.foldl (fun L1 x => L1 ++ t x.2) []
+termination_by exp
+decreasing_by trace_state; sorry
+
+end Ex2
+
+
+namespace WithOptionOff
+
+set_option wf.preprocess false
+
+/--
+error: tactic 'fail' failed
+α : Type u_1
+t t' : Tree α
+⊢ sizeOf t' < sizeOf t
+-/
+#guard_msgs in
+def map (f : α → β) (t : Tree α) : Tree β :=
+    ⟨f t.val, t.cs.map (fun t' => map f t')⟩
+termination_by t
+decreasing_by fail
+
+end WithOptionOff
diff --git a/tests/lean/run/wf_preprocess_leak.lean b/tests/lean/run/wf_preprocess_leak.lean
new file mode 100644
index 000000000000..dd6d90823312
--- /dev/null
+++ b/tests/lean/run/wf_preprocess_leak.lean
@@ -0,0 +1,107 @@
+/-! This tests demonstrates where and how wf preprocessing leaks to the user -/
+
+structure Tree (α : Type) where
+  cs : List (Tree α)
+
+def Tree.isLeaf (t : Tree α) := t.cs.isEmpty
+
+-- The `cs.map` in the outer call to `revrev` gets the `attach`-attaching treatment and shows up in
+-- the proof state:
+
+/--
+info: α : Type
+n : Nat
+cs : List (Tree α)
+x✝ :
+  (y : (_ : Nat) ×' Tree α) →
+    (invImage (fun x => PSigma.casesOn x fun n t => (n, t)) Prod.instWellFoundedRelation).1 y ⟨n.succ, { cs := cs }⟩ →
+      Tree α
+⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => sizeOf a₁ < sizeOf a₂)
+    (n, { cs := List.map (fun x => x✝ ⟨n + 1, x.val⟩ ⋯) cs.attach }) (n.succ, { cs := cs })
+-/
+#guard_msgs in
+def Tree.revrev : (n : Nat) → (t : Tree α) → Tree α
+  | 0, t => t
+  | n + 1, Tree.mk cs => revrev n (Tree.mk (cs.map (·.revrev (n + 1))))
+termination_by n t => (n, t)
+decreasing_by
+  · apply Prod.Lex.right
+    simp
+    have := List.sizeOf_lt_of_mem ‹_ ∈ _›
+    omega
+  · trace_state
+    apply Prod.Lex.left
+    decreasing_tactic
+
+-- as well as in the induction principle:
+
+-- set_option trace.Meta.FunInd true
+
+/--
+info: Tree.revrev.induct {α : Type} (motive : Nat → Tree α → Prop) (case1 : ∀ (t : Tree α), motive 0 t)
+  (case2 :
+    ∀ (n : Nat) (cs : List (Tree α)),
+      (∀ (x : Tree α), x ∈ cs → motive (n + 1) x) →
+        (∀ (x : Subtype (Membership.mem cs)), motive (n + 1) x.val) →
+          motive n
+              {
+                cs :=
+                  List.map
+                    (fun x =>
+                      match x with
+                      | ⟨x, h⟩ => Tree.revrev (n + 1) x)
+                    cs.attach } →
+            motive n.succ { cs := cs })
+  (n : Nat) (t : Tree α) : motive n t
+-/
+#guard_msgs in
+#check Tree.revrev.induct
+
+-- Tangent: Why three IHs here? Because in the termination proof, the `
+--    match x with | ⟨x, h⟩ => Tree.revrev (n + 1) x)
+-- was replaced by
+--    Tree.revrev (n + 1) ↑x
+-- (maybe due to split/simpMatch) and funind picks up that recursive call as a separate one.
+-- See
+-- set_option pp.proofs true in #print Tree.revrev._unary
+-- set_option pp.proofs true in #print Tree.revrev._unary.proof_3
+
+
+-- It does not show up in the equational theorems:
+
+/--
+info: equations:
+theorem Tree.revrev.eq_1 : ∀ {α : Type} (x : Tree α), Tree.revrev 0 x = x
+theorem Tree.revrev.eq_2 : ∀ {α : Type} (n : Nat) (cs : List (Tree α)),
+  Tree.revrev n.succ { cs := cs } = Tree.revrev n { cs := List.map (fun x => Tree.revrev (n + 1) x) cs }
+-/
+#guard_msgs in
+#print equations Tree.revrev
+
+theorem sizeOf_map {α β : Type} [SizeOf α] [SizeOf β]
+    (f : α → β) (xs : List α) (hf : ∀ x, x ∈ xs → sizeOf (f x) = sizeOf x) :
+    sizeOf (List.map f xs) = sizeOf xs := by
+  induction xs with
+  | nil =>
+    simp
+  | cons x xs ih =>
+    simp [List.map]
+    simp [hf]
+    apply ih
+    intro x hx
+    apply hf
+    apply List.mem_cons.2
+    exact Or.inr hx
+
+
+-- Lets see how tedious it is to use the functional induction principle:
+example (n : Nat) (t : Tree α) : sizeOf (Tree.revrev n t) = sizeOf t := by
+  induction n, t using Tree.revrev.induct with
+  | case1 =>
+    simp [Tree.revrev]
+  | case2 n cs ih1 ih2 ih3 =>
+    simp [Tree.revrev]
+    simp only [Subtype.forall, List.map_subtype, List.unattach_attach, Tree.mk.sizeOf_spec] at *
+    rw [ih3]; clear ih3
+    rw [sizeOf_map]
+    · assumption
diff --git a/tests/lean/treeMap.lean.expected.out b/tests/lean/treeMap.lean.expected.out
index 14574d68e743..e69de29bb2d1 100644
--- a/tests/lean/treeMap.lean.expected.out
+++ b/tests/lean/treeMap.lean.expected.out
@@ -1,8 +0,0 @@
-treeMap.lean:8:62-8:72: error: failed to prove termination, possible solutions:
-  - Use `have`-expressions to prove the remaining goals
-  - Use `termination_by` to specify a different well-founded relation
-  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
-name : String
-children : List TreeNode
-t : TreeNode
-⊢ sizeOf t < 1 + sizeOf name + sizeOf children