diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index a22f03cab2..b33c4b4453 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -439,6 +439,53 @@ end
 
 end PSigma
 
+namespace WellFounded
+
+variable {α : Sort u}
+variable {motive : α → Sort v}
+variable (h : α → Nat)
+variable (F : (x : α) → ((y : α) → InvImage (· < ·) h y x → motive y) → motive x)
+
+/-- Helper gadget that prevents reduction of `Nat.eager n` unless `n` evalutes to a ground term. -/
+def Nat.eager (n : Nat) : Nat :=
+  if Nat.beq n n = true then n else n
+
+theorem Nat.eager_eq (n : Nat) : Nat.eager n = n := ite_self n
+
+/--
+A well-founded fixpoint operator specialized for `Nat`-valued measures. Given a measure `h`, it expects
+its higher order function argument `F` to invoke its argument only on values `y` that are smaller
+than `x` with regard to `h`.
+
+In contrast to to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely:
+when `h x` evalutes to a ground value)
+
+-/
+def Nat.fix : (x : α) → motive x :=
+  let rec go : ∀ (fuel : Nat) (x : α), (h x < fuel) → motive x :=
+    Nat.rec
+      (fun _ hfuel => (Nat.not_succ_le_zero _ hfuel).elim)
+      (fun _ ih x hfuel => F x (fun y hy => ih y (Nat.lt_of_lt_of_le hy (Nat.le_of_lt_add_one hfuel))))
+  fun x => go (Nat.eager (h x + 1)) x (Nat.eager_eq _ ▸ Nat.lt_add_one _)
+
+protected theorem Nat.fix.go_congr (x : α) (fuel₁ fuel₂ : Nat) (h₁ : h x < fuel₁) (h₂ : h x < fuel₂) :
+    Nat.fix.go h F fuel₁ x h₁ = Nat.fix.go h F fuel₂ x h₂ := by
+  induction fuel₁ generalizing x fuel₂ with
+  | zero => contradiction
+  | succ fuel₁ ih =>
+    cases fuel₂ with
+    | zero => contradiction
+    | succ fuel₂ =>
+      exact congrArg (F x) (funext fun y => funext fun hy => ih y fuel₂ _ _ )
+
+theorem Nat.fix_eq (x : α) :
+    Nat.fix h F x = F x (fun y _ => Nat.fix h F y) := by
+  unfold Nat.fix
+  simp [Nat.eager_eq]
+  exact congrArg (F x) (funext fun _ => funext fun _ => Nat.fix.go_congr ..)
+
+end WellFounded
+
 /--
 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
diff --git a/src/Lean/Compiler/InlineAttrs.lean b/src/Lean/Compiler/InlineAttrs.lean
index 224b8261f7..2cec66e953 100644
--- a/src/Lean/Compiler/InlineAttrs.lean
+++ b/src/Lean/Compiler/InlineAttrs.lean
@@ -37,6 +37,7 @@ private def isValidMacroInline (declName : Name) : CoreM Bool := do
   let isRec (declName' : Name) : Bool :=
     isBRecOnRecursor env declName' ||
     declName' == ``WellFounded.fix ||
+    declName' == ``WellFounded.Nat.fix ||
     declName' == declName ++ `_unary -- Auxiliary declaration created by `WF` module
   if Option.isSome <| info.value.find? fun e => e.isConst && isRec e.constName! then
     -- It contains a `brecOn` or `WellFounded.fix` application. So, it should be recursvie
diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index afe0464f92..6e293abdeb 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -237,21 +237,32 @@ def solveDecreasingGoals (funNames : Array Name) (argsPacker : ArgsPacker) (decr
             Term.reportUnsolvedGoals remainingGoals
   instantiateMVars value
 
+def isNatLtWF (wfRel : Expr) : MetaM (Option Expr) := do
+  match_expr wfRel with
+  | invImage _ β f wfRelβ =>
+    unless (← isDefEq β (mkConst ``Nat)) do return none
+    unless (← isDefEq wfRelβ (mkConst ``Nat.lt_wfRel)) do return none
+    return f
+  | _ => return none
+
 def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (argsPacker : ArgsPacker)
     (wfRel : Expr) (funNames : Array Name) (decrTactics : Array (Option DecreasingBy)) :
     TermElabM Expr := do
   let type ← instantiateForall preDef.type prefixArgs
   let (wfFix, varName) ← forallBoundedTelescope type (some 1) fun x type => do
     let x := x[0]!
+    let varName ← x.fvarId!.getUserName -- See comment below.
     let α ← inferType x
     let u ← getLevel α
     let v ← getLevel type
     let motive ← mkLambdaFVars #[x] type
-    let rel := mkProj ``WellFoundedRelation 0 wfRel
-    let wf  := mkProj ``WellFoundedRelation 1 wfRel
-    let wf ← mkAppM `Lean.opaqueId #[wf]
-    let varName ← x.fvarId!.getUserName -- See comment below.
-    return (mkApp4 (mkConst ``WellFounded.fix [u, v]) α motive rel wf, varName)
+    if let some measure ← isNatLtWF wfRel then
+      return (mkApp3 (mkConst `WellFounded.Nat.fix [u, v]) α motive measure, varName)
+    else
+      let rel := mkProj ``WellFoundedRelation 0 wfRel
+      let wf  := mkProj ``WellFoundedRelation 1 wfRel
+      let wf ← mkAppM `Lean.opaqueId #[wf]
+      return (mkApp4 (mkConst ``WellFounded.fix [u, v]) α motive rel wf, varName)
   forallBoundedTelescope (← whnf (← inferType wfFix)).bindingDomain! (some 2) fun xs _ => do
     let x   := xs[0]!
     -- Remark: we rename `x` here to make sure we preserve the variable name in the
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index dc790be35e..ac0205bad6 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -53,12 +53,6 @@ def wfRecursion (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDe
     -- No termination_by here, so use GuessLex to infer one
     guessLex preDefs unaryPreDefProcessed fixedParamPerms argsPacker
 
-  -- Warn about likely unwanted reducibility attributes
-  preDefs.forM fun preDef =>
-    preDef.modifiers.attrs.forM fun a => do
-      if a.name = `reducible || a.name = `semireducible then
-        logWarningAt a.stx s!"marking functions defined by well-founded recursion as `{a.name}` is not effective"
-
   let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedParamPerms.numFixed fun fixedArgs type => do
     let type ← whnfForall type
     unless type.isForall do
@@ -66,6 +60,14 @@ def wfRecursion (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDe
     let packedArgType := type.bindingDomain!
     elabWFRel (preDefs.map (·.declName)) unaryPreDef.declName fixedParamPerms fixedArgs argsPacker packedArgType wf fun wfRel => do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
+      let useNatRec := (← isNatLtWF wfRel).isSome
+      -- Warn about likely unwanted reducibility attributes
+      unless useNatRec do
+        preDefs.forM fun preDef =>
+          preDef.modifiers.attrs.forM fun a => do
+            if a.name = `reducible || a.name = `semireducible then
+              logWarningAt a.stx s!"marking functions defined by well-founded recursion as `{a.name}` is not effective"
+
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
         let value ← mkFix unaryPreDefProcessed fixedArgs argsPacker wfRel (preDefs.map (·.declName)) (preDefs.map (·.termination.decreasingBy?))
diff --git a/src/Lean/Elab/PreDefinition/WF/Unfold.lean b/src/Lean/Elab/PreDefinition/WF/Unfold.lean
index 8a82212342..76b3fa7f73 100644
--- a/src/Lean/Elab/PreDefinition/WF/Unfold.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Unfold.lean
@@ -36,9 +36,14 @@ def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   -- lhs should be an application of the declNameNonrec, which unfolds to an
   -- application of fix in one step
   let some lhs' ← delta? lhs | throwError "rwFixEq: cannot delta-reduce {lhs}"
-  let_expr WellFounded.fix _α _C _r _hwf F x := lhs'
-    | throwTacticEx `rwFixEq mvarId "expected saturated fixed-point application in {lhs'}"
-  let h := mkAppN (mkConst ``WellFounded.fix_eq lhs'.getAppFn.constLevels!) lhs'.getAppArgs
+  let h ← match_expr lhs' with
+    | WellFounded.fix _α _C _r _hwf _F _x =>
+      pure <| mkAppN (mkConst ``WellFounded.fix_eq lhs'.getAppFn.constLevels!) lhs'.getAppArgs
+    | WellFounded.Nat.fix _α _C _motive _F _x =>
+      pure <| mkAppN (mkConst ``WellFounded.Nat.fix_eq lhs'.getAppFn.constLevels!) lhs'.getAppArgs
+    | _ => throwTacticEx `rwFixEq mvarId m!"expected saturated fixed-point application in {lhs'}"
+  let F := lhs'.appFn!.appArg!
+  let x := lhs'.appArg!
 
   -- We used to just rewrite with `fix_eq` and continue with whatever RHS that produces, but that
   -- would include more copies of `fix` resulting in large and confusing terms.
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index b279ca3850..b5e59ccd13 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -927,7 +927,7 @@ where doRealize (inductName : Name) := do
   -- to make sure that `target` indeed the last parameter
   let e := info.value
   let e ← lambdaTelescope e fun params body => do
-    if body.isAppOfArity ``WellFounded.fix 5 then
+    if body.isAppOfArity ``WellFounded.fix 5 || body.isAppOfArity ``WellFounded.Nat.fix 4 then
       forallBoundedTelescope (← inferType body) (some 1) fun xs _ => do
         unless xs.size = 1 do
           throwError "functional induction: Failed to eta-expand{indentExpr e}"
@@ -935,68 +935,76 @@ where doRealize (inductName : Name) := do
     else
       pure e
   let (e', paramMask) ← lambdaTelescope e fun params funBody => MatcherApp.withUserNames params varNames do
-    match_expr funBody with
-    | fix@WellFounded.fix α _motive rel wf body target =>
-      unless params.back! == target do
-        throwError "functional induction: expected the target as last parameter{indentExpr e}"
-      let fixedParamPerms := params.pop
-      let motiveType ←
-        if unfolding then
-          withLocalDeclD `r (← instantiateForall info.type params) fun r =>
-            mkForallFVars #[target, r] (.sort 0)
-        else
-          mkForallFVars #[target] (.sort 0)
-      withLocalDeclD `motive motiveType fun motive => do
-        let fn := mkAppN (← mkConstWithLevelParams name) fixedParamPerms
-        let isRecCall : Expr → Option Expr := fun e =>
-          e.withApp fun f xs =>
-            if f.isFVarOf motive.fvarId! && xs.size > 0 then
-            mkApp fn xs[0]!
-          else
-            none
-
-        let motiveArg ←
-          if unfolding then
-            let motiveArg := mkApp2 motive target (mkAppN (← mkConstWithLevelParams name) params)
-            mkLambdaFVars #[target] motiveArg
-          else
-            pure motive
-        let e' := .const ``WellFounded.fix [fix.constLevels![0]!, levelZero]
-        let e' := mkApp4 e' α motiveArg rel wf
-        check e'
-        let (body', mvars) ← M2.run do
-          forallTelescope (← inferType e').bindingDomain! fun xs goal => do
-            if xs.size ≠ 2 then
-              throwError "expected recursor argument to take 2 parameters, got {xs}" else
-            let targets : Array Expr := xs[*...1]
-            let genIH := xs[1]!
-            let extraParams := xs[2...*]
-            -- open body with the same arg
-            let body ← instantiateLambda body targets
-            lambdaTelescope1 body fun oldIH body => do
-              let body ← instantiateLambda body extraParams
-              let body' ← withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
-                buildInductionBody #[oldIH, genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
-              if body'.containsFVar oldIH then
-                throwError m!"Did not fully eliminate `{mkFVar oldIH}` from induction principle body:{indentExpr body}"
-              mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
-        let e' := mkApp2 e' body' target
-        let e' ← mkLambdaFVars #[target] e'
-        let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e'
-        let e' ← mkLambdaFVars #[motive] e'
-
-        -- We used to pass (usedOnly := false) below in the hope that the types of the
-        -- induction principle match the type of the function better.
-        -- But this leads to avoidable parameters that make functional induction strictly less
-        -- useful (e.g. when the unused parameter mentions bound variables in the users' goal)
-        let (paramMask, e') ← mkLambdaFVarsMasked fixedParamPerms e'
-        let e' ← instantiateMVars e'
-        return (e', paramMask)
-    | _ =>
-      if funBody.isAppOf ``WellFounded.fix then
-        throwError "Function `{name}` defined via `{.ofConstName ``WellFounded.fix}` with unexpected arity {funBody.getAppNumArgs}:{indentExpr funBody}"
+    unless funBody.isApp && funBody.appFn!.isApp do
+      throwError "functional induction: unexpected body {funBody}"
+    let body := funBody.appFn!.appArg!
+    let target := funBody.appArg!
+    unless params.back! == target do
+      throwError "functional induction: expected the target as last parameter{indentExpr e}"
+    let fixedParamPerms := params.pop
+    let motiveType ←
+      if unfolding then
+        withLocalDeclD `r (← instantiateForall info.type params) fun r =>
+          mkForallFVars #[target, r] (.sort 0)
       else
-        throwError "Function `{name}` not defined via `{.ofConstName ``WellFounded.fix}`:{indentExpr funBody}"
+        mkForallFVars #[target] (.sort 0)
+    withLocalDeclD `motive motiveType fun motive => do
+      let fn := mkAppN (← mkConstWithLevelParams name) fixedParamPerms
+      let isRecCall : Expr → Option Expr := fun e =>
+        e.withApp fun f xs =>
+          if f.isFVarOf motive.fvarId! && xs.size > 0 then
+          mkApp fn xs[0]!
+        else
+          none
+
+      let motiveArg ←
+        if unfolding then
+          let motiveArg := mkApp2 motive target (mkAppN (← mkConstWithLevelParams name) params)
+          mkLambdaFVars #[target] motiveArg
+        else
+          pure motive
+
+      let e' ← match_expr funBody with
+        | fix@WellFounded.fix α _motive rel wf _body _target =>
+          let e' := .const ``WellFounded.fix [fix.constLevels![0]!, levelZero]
+          pure <| mkApp4 e' α motiveArg rel wf
+        | fix@WellFounded.Nat.fix α _motive measure _body _target =>
+          let e' := .const `WellFounded.Nat.fix [fix.constLevels![0]!, levelZero]
+          pure <| mkApp3 e' α motiveArg measure
+        | _ =>
+          if funBody.isAppOf ``WellFounded.fix || funBody.isAppOf `WellFounded.Nat.Fix then
+            throwError "Function {name} defined via WellFounded.fix with unexpected arity {funBody.getAppNumArgs}:{indentExpr funBody}"
+          else
+            throwError "Function {name} not defined via WellFounded.fix:{indentExpr funBody}"
+      check e'
+      let (body', mvars) ← M2.run do
+        forallTelescope (← inferType e').bindingDomain! fun xs goal => do
+          if xs.size ≠ 2 then
+            throwError "expected recursor argument to take 2 parameters, got {xs}" else
+          let targets : Array Expr := xs[*...1]
+          let genIH := xs[1]!
+          let extraParams := xs[2...*]
+          -- open body with the same arg
+          let body ← instantiateLambda body targets
+          lambdaTelescope1 body fun oldIH body => do
+            let body ← instantiateLambda body extraParams
+            let body' ← withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
+              buildInductionBody #[oldIH, genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
+            if body'.containsFVar oldIH then
+              throwError m!"Did not fully eliminate `{mkFVar oldIH}` from induction principle body:{indentExpr body}"
+            mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
+      let e' := mkApp2 e' body' target
+      let e' ← mkLambdaFVars #[target] e'
+      let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e'
+      let e' ← mkLambdaFVars #[motive] e'
+
+      -- We used to pass (usedOnly := false) below in the hope that the types of the
+      -- induction principle match the type of the function better.
+      -- But this leads to avoidable parameters that make functional induction strictly less
+      -- useful (e.g. when the unused parameter mentions bound variables in the users' goal)
+      let (paramMask, e') ← mkLambdaFVarsMasked fixedParamPerms e'
+      let e' ← instantiateMVars e'
+      return (e', paramMask)
 
   unless (← isTypeCorrect e') do
     logError m!"failed to derive a type-correct induction principle:{indentExpr e'}"
diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean
index 6567d5c1d9..75a79e20b3 100644
--- a/src/Std/Sat/AIG/Basic.lean
+++ b/src/Std/Sat/AIG/Basic.lean
@@ -485,6 +485,7 @@ where
       let lval := go lhs.gate decls assign (by omega) h2
       let rval := go rhs.gate decls assign (by omega) h2
       xor lval lhs.invert && xor rval rhs.invert
+  termination_by (x, 0) -- Don't allow reduction, we have large concrete gate entries
 
 /--
 Denotation of an `AIG` at a specific `Entrypoint`.
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..f4d5f7ddae 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;
diff --git a/tests/lean/run/1026.lean b/tests/lean/run/1026.lean
index fd649b794f..945b4a4e7b 100644
--- a/tests/lean/run/1026.lean
+++ b/tests/lean/run/1026.lean
@@ -16,7 +16,7 @@ info: foo.eq_def (n : Nat) :
     if n = 0 then 0
     else
       have x := n - 1;
-      have this := foo._proof_4;
+      have this := foo._proof_3;
       foo x
 -/
 #guard_msgs in
@@ -28,7 +28,7 @@ info: foo.eq_unfold :
     if n = 0 then 0
     else
       have x := n - 1;
-      have this := foo._proof_4;
+      have this := foo._proof_3;
       foo x
 -/
 #guard_msgs in
diff --git a/tests/lean/run/4928.lean b/tests/lean/run/4928.lean
index d054f79d03..93ee9678e6 100644
--- a/tests/lean/run/4928.lean
+++ b/tests/lean/run/4928.lean
@@ -46,7 +46,7 @@ end
 /--
 error: Failed: `fail` tactic was invoked
 x : List Nat
-⊢ (invImage (fun x => PSum.casesOn x (fun x => x.length) fun x => x.length) sizeOfWFRel).1 (PSum.inr x.tail)
+⊢ InvImage (fun x1 x2 => x1 < x2) (fun x => PSum.casesOn x (fun x => x.length) fun x => x.length) (PSum.inr x.tail)
     (PSum.inl x)
 -/
 #guard_msgs in
diff --git a/tests/lean/run/hasNotBit.lean b/tests/lean/run/hasNotBit.lean
index c33e38857a..a1d9901623 100644
--- a/tests/lean/run/hasNotBit.lean
+++ b/tests/lean/run/hasNotBit.lean
@@ -30,13 +30,6 @@ elab "refl0" : tactic =>
   Lean.Elab.Tactic.closeMainGoalUsing `refl0 fun _ _ =>
     Lean.Meta.mkEqRefl (Lean.mkRawNatLit 0)
 
-/--
-error: (kernel) declaration type mismatch, '_example' has type
-  ∀ {α : Type u_1} {x : α}, 0 = 0
-but it is expected to have type
-  ∀ {α : Type u_1} {x : α}, Nat.land 1 (Nat.shiftRight 8 [x].ctorIdx) = 0
--/
-#guard_msgs in
 example : Nat.land 1 (Nat.shiftRight 8 ([x].ctorIdx)) = 0 := by
   refl0
 
@@ -45,13 +38,6 @@ elab "eagerrefl0" : tactic =>
   Lean.Elab.Tactic.closeMainGoalUsing `refl0 fun _ _ => do
     Lean.Meta.mkAppM `eagerReduce #[← Lean.Meta.mkEqRefl (Lean.mkRawNatLit 0)]
 
-/--
-error: (kernel) declaration type mismatch, '_example' has type
-  ∀ {α : Type u_1} {x : α}, 0 = 0
-but it is expected to have type
-  ∀ {α : Type u_1} {x : α}, Nat.land 1 (Nat.shiftRight 8 [x].ctorIdx) = 0
--/
-#guard_msgs in
 example : Nat.land 1 (Nat.shiftRight 8 ([x].ctorIdx)) = 0 := by
   eagerrefl0
 
@@ -61,15 +47,6 @@ elab "eagerrefl0'" : tactic =>
     let u ← getLevel goal
     return mkApp2 (mkConst ``eagerReduce [u]) goal (← mkEqRefl (mkRawNatLit 0))
 
-/--
-error: (kernel) application type mismatch
-  eagerReduce (Eq.refl 0)
-argument has type
-  0 = 0
-but function has type
-  Nat.land 1 (Nat.shiftRight 8 [x].ctorIdx) = 0 → Nat.land 1 (Nat.shiftRight 8 [x].ctorIdx) = 0
--/
-#guard_msgs in
 example : Nat.land 1 (Nat.shiftRight 8 ([x].ctorIdx)) = 0 := by
   eagerrefl0'
 
diff --git a/tests/lean/run/issue10651.lean b/tests/lean/run/issue10651.lean
index 9401d9763b..ab2d66da80 100644
--- a/tests/lean/run/issue10651.lean
+++ b/tests/lean/run/issue10651.lean
@@ -10,9 +10,9 @@ termination_by x
 
 /--
 info: equations:
-theorem f.eq_1 : f 0 = 1
-theorem f.eq_2 : f 100 = 2
-theorem f.eq_3 : f 1000 = 3
+@[defeq] theorem f.eq_1 : f 0 = 1
+@[defeq] theorem f.eq_2 : f 100 = 2
+@[defeq] theorem f.eq_3 : f 1000 = 3
 theorem f.eq_4 : ∀ (x_2 : Nat), (x_2 = 99 → False) → (x_2 = 999 → False) → f x_2.succ = f x_2
 -/
 #guard_msgs(pass trace, all) in
diff --git a/tests/lean/run/issue11181.lean b/tests/lean/run/issue11181.lean
new file mode 100644
index 0000000000..cea9b4484a
--- /dev/null
+++ b/tests/lean/run/issue11181.lean
@@ -0,0 +1,10 @@
+set_option warn.sorry false
+
+
+theorem Nat.foo₁ (n : Nat) : n ^^^ 0 = n ^^^ 0 := by
+  cases n
+  · simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]
+  · sorry
+
+theorem Nat.foo₂ : 0 ^^^ 0 = 0 ^^^ 0 := by
+  simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]
diff --git a/tests/lean/run/issue2021.lean b/tests/lean/run/issue2021.lean
new file mode 100644
index 0000000000..81ba85182b
--- /dev/null
+++ b/tests/lean/run/issue2021.lean
@@ -0,0 +1,46 @@
+prelude -- optional
+import Init.WF
+import Init.WFTactics
+import Init.Data.Nat.Basic
+namespace Nat'
+
+protected def modCore (y : Nat) : Nat → Nat → Nat
+  | Nat.zero, x => x
+  | Nat.succ fuel, x => if 0 < y ∧ y ≤ x then Nat'.modCore y fuel (x - y) else x
+
+protected def mod' (x y : @& Nat) : Nat :=
+Nat'.modCore y x x
+
+@[simp] theorem zero_mod' (b : Nat) : Nat'.mod' 0 b = 0 := rfl
+
+end Nat'
+
+namespace Nat
+
+private def gcdF' (x : Nat) : (∀ x₁, x₁ < x → Nat → Nat) → Nat → Nat :=
+  match x with
+  | 0      => fun _ y => y
+  | succ x => fun f y => f (Nat'.mod' y (succ x)) sorry (succ x)
+
+noncomputable def gcd' (a b : Nat) : Nat :=
+  WellFounded.fix (measure id).wf gcdF' a b
+
+@[simp] theorem gcd'_zero_left (y : Nat) : gcd' 0 y = y :=
+  rfl
+
+theorem gcd'_succ (x y : Nat) : gcd' (succ x) y = gcd' (Nat'.mod' y (succ x)) (succ x) :=
+  rfl   -- replace with `id rfl` and everything is ok
+
+/--
+error: (kernel) application type mismatch
+  @Eq.ndrec Nat (n✝ + 1) (fun n => gcd' n 0 = n) (of_eq_true (eq_self (n✝ + 1)))
+argument has type
+  n✝ + 1 = n✝ + 1
+but function has type
+  (fun n => gcd' n 0 = n) (n✝ + 1) → ∀ {b : Nat}, n✝ + 1 = b → (fun n => gcd' n 0 = n) b
+-/
+#guard_msgs in
+@[simp] theorem gcd'_zero_right (n : Nat) : gcd' n 0 = n := by
+  cases n <;> simp [gcd'_succ]
+
+end Nat
diff --git a/tests/lean/run/issue2102.lean b/tests/lean/run/issue2102.lean
index f56cf4909b..7668bf90b0 100644
--- a/tests/lean/run/issue2102.lean
+++ b/tests/lean/run/issue2102.lean
@@ -37,7 +37,8 @@ head✝ : T✝
 tl : List T✝
 x✝ :
   (y : (T : Type) ×' List T) →
-    (invImage (fun x => PSigma.casesOn x fun T ls => sizeOf ls) sizeOfWFRel).1 y ⟨T✝, head✝ :: tl⟩ → Option (List y.1)
+    InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun T ls => sizeOf ls) y ⟨T✝, head✝ :: tl⟩ →
+      Option (List y.1)
 res : Option { x // x✝ ⟨T✝, tl⟩ ⋯ = some x } := (x✝ ⟨T✝, tl⟩ ⋯).attach
 T : Type
 ls : List T
@@ -61,7 +62,8 @@ head✝ : T✝
 tl : List T✝
 x✝ :
   (y : (T : Type) ×' List T) →
-    (invImage (fun x => PSigma.casesOn x fun T ls => sizeOf ls) sizeOfWFRel).1 y ⟨T✝, head✝ :: tl⟩ → Option (List y.1)
+    InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun T ls => sizeOf ls) y ⟨T✝, head✝ :: tl⟩ →
+      Option (List y.1)
 res : Option { x // x✝ ⟨T✝, tl⟩ ⋯ = some x } := (x✝ ⟨T✝, tl⟩ ⋯).attach
 T : Type
 ls : List T
diff --git a/tests/lean/run/issue2171.lean b/tests/lean/run/issue2171.lean
index ed1ac3fd87..92d4963b70 100644
--- a/tests/lean/run/issue2171.lean
+++ b/tests/lean/run/issue2171.lean
@@ -3,7 +3,7 @@ def g (n : Nat) : Nat :=
     1
   else
     4 + g (n - 1)
-  termination_by n
+  termination_by (n,0)
   decreasing_by simp_wf; omega
 
 example : g 10000 = id g (id 10000) := rfl
diff --git a/tests/lean/run/letToHaveCleanup.lean b/tests/lean/run/letToHaveCleanup.lean
index da0138cd1d..84f3c4d383 100644
--- a/tests/lean/run/letToHaveCleanup.lean
+++ b/tests/lean/run/letToHaveCleanup.lean
@@ -171,11 +171,11 @@ def fnWFRec (n : Nat) : let α := Nat; α :=
 info: @[irreducible] def fnWFRec : Nat →
   have α : Type := Nat;
   α :=
-fnWFRec._proof_1.fix fun n a =>
+WellFounded.Nat.fix (fun x => x) fun n a =>
   (match (motive :=
       (n : Nat) →
         ((y : Nat) →
-            (invImage (fun x => x) sizeOfWFRel).1 y n →
+            InvImage (fun x1 x2 => x1 < x2) (fun x => x) y n →
               let α : Type := Nat;
               α) →
           let α : Type := Nat;
diff --git a/tests/lean/run/structuralEqn6.lean b/tests/lean/run/structuralEqn6.lean
index 1acb9df7b5..e88de20d03 100644
--- a/tests/lean/run/structuralEqn6.lean
+++ b/tests/lean/run/structuralEqn6.lean
@@ -80,7 +80,7 @@ info: equations:
 theorem trailingZeros2'.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (hk_2 : i.natAbs ≤ k_2 + 1),
   trailingZeros2'.aux k_2.succ i hi hk_2 acc =
     if h : i % 2 = 0 then trailingZeros2'.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
-theorem trailingZeros2'.aux.eq_2 : ∀ (i : Int) (hi : i ≠ 0) (acc : Nat) (hk_2 : i.natAbs ≤ 0),
+@[defeq] theorem trailingZeros2'.aux.eq_2 : ∀ (i : Int) (hi : i ≠ 0) (acc : Nat) (hk_2 : i.natAbs ≤ 0),
   trailingZeros2'.aux 0 i hi hk_2 acc = acc
 -/
 #guard_msgs(pass trace, all) in
diff --git a/tests/lean/run/wfEqns5.lean b/tests/lean/run/wfEqns5.lean
index 824f980835..245b3cf62a 100644
--- a/tests/lean/run/wfEqns5.lean
+++ b/tests/lean/run/wfEqns5.lean
@@ -6,7 +6,7 @@ termination_by n => n
 
 /--
 info: equations:
-theorem foo.eq_1 : foo 0 0 = 0
+@[defeq] theorem foo.eq_1 : foo 0 0 = 0
 theorem foo.eq_2 : ∀ (x : Nat), (x = 0 → False) → foo 0 x = x
 theorem foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
 -/
@@ -53,7 +53,7 @@ termination_by n => n
 
 /--
 info: equations:
-theorem bar.eq_1 : ∀ (x : Nat),
+@[defeq] theorem bar.eq_1 : ∀ (x : Nat),
   bar 0 x =
     match x with
     | 0 => 0
@@ -120,7 +120,7 @@ termination_by n => n
 
 /--
 info: equations:
-theorem Structural.bar.eq_1 : ∀ (x : Nat),
+@[defeq] theorem Structural.bar.eq_1 : ∀ (x : Nat),
   bar 0 x =
     match x with
     | 0 => 0
diff --git a/tests/lean/run/wfirred.lean b/tests/lean/run/wfirred.lean
index 718986522f..aeb415f738 100644
--- a/tests/lean/run/wfirred.lean
+++ b/tests/lean/run/wfirred.lean
@@ -1,13 +1,13 @@
 /-!
-Tests that definitions by well-founded recursion are irreducible.
+Tests that definitions by well-founded recursion (not on Nat) are irreducible.
 -/
 
 set_option pp.mvars false
 
-def foo : Nat → Nat
-  | 0 => 0
-  | n+1 => foo n
-termination_by n => n
+def foo : Nat → Nat → Nat
+  | 0,  m => m
+  | n+1, m => foo n (m + n)
+termination_by n m => (n, m)
 
 /--
 error: Type mismatch
@@ -15,10 +15,10 @@ error: Type mismatch
 has type
   ?_ = ?_
 but is expected to have type
-  foo 0 = 0
+  foo 0 m = m
 -/
 #guard_msgs in
-example : foo 0 = 0 := rfl
+example : foo 0 m = m := rfl
 
 /--
 error: Type mismatch
@@ -26,35 +26,22 @@ error: Type mismatch
 has type
   ?_ = ?_
 but is expected to have type
-  foo (n + 1) = foo n
+  foo (n + 1) m = foo n (m + n)
 -/
 #guard_msgs in
-example : foo (n+1) = foo n := rfl
+example : foo (n+1) m = foo n (m + n) := rfl
 
 -- also for closed terms
 /--
 error: Tactic `rfl` failed: The left-hand side
-  foo 0
+  foo 0 0
 is not definitionally equal to the right-hand side
   0
 
-⊢ foo 0 = 0
+⊢ foo 0 0 = 0
 -/
 #guard_msgs in
-example : foo 0 = 0 := by rfl
-
--- It only works on closed terms:
-/--
-error: Tactic `rfl` failed: The left-hand side
-  foo (n + 1)
-is not definitionally equal to the right-hand side
-  foo n
-
-n : Nat
-⊢ foo (n + 1) = foo n
--/
-#guard_msgs in
-example : foo (n+1) = foo n := by rfl
+example : foo 0 0 = 0 := by rfl
 
 section Unsealed
 
@@ -68,10 +55,10 @@ error: Type mismatch
 has type
   ?_ = ?_
 but is expected to have type
-  foo 0 = 0
+  foo 0 0 = 0
 -/
 #guard_msgs in
-example : foo 0 = 0 := rfl
+example : foo 0 0 = 0 := rfl
 
 /--
 error: Type mismatch
@@ -79,10 +66,10 @@ error: Type mismatch
 has type
   ?_ = ?_
 but is expected to have type
-  foo (n + 1) = foo n
+  foo (n + 1) m = foo n (n + m)
 -/
 #guard_msgs in
-example : foo (n+1) = foo n := rfl
+example : foo (n+1) m = foo n (n +m ):= rfl
 
 end Unsealed
 
@@ -94,15 +81,15 @@ error: Type mismatch
 has type
   ?_ = ?_
 but is expected to have type
-  foo 0 = 0
+  foo 0 m = m
 -/
 #guard_msgs in
-example : foo 0 = 0 := rfl
+example : foo 0 m = m := rfl
 
-def bar : Nat → Nat
-  | 0 => 0
-  | n+1 => bar n
-termination_by n => n
+def bar : Nat → Nat → Nat
+  | 0, m => m
+  | n+1, m => bar n (m + n)
+termination_by n m => (n, m)
 
 -- Once unsealed, the full internals are visible. This allows one to prove, for example
 -- an equality like the following
diff --git a/tests/lean/run/wfrec-nat.lean b/tests/lean/run/wfrec-nat.lean
new file mode 100644
index 0000000000..bae7eeba98
--- /dev/null
+++ b/tests/lean/run/wfrec-nat.lean
@@ -0,0 +1,130 @@
+/-!
+Tests around the special case of well-founded recursion on Nat.
+-/
+
+set_option warn.sorry false
+
+namespace T1
+
+@[semireducible]
+def foo : List α → Nat
+  | [] => 0
+  | _::xs => 1 + (foo xs)
+termination_by xs => xs.length
+
+-- Closed terms should evaluate
+
+example : foo ([] : List Unit) = 0 := rfl
+example : foo ([] : List Unit) = 0 := by decide
+example : foo ([] : List Unit) = 0 := by decide +kernel
+example : foo [1,2,3,4,5] = 5 := rfl
+example : foo [1,2,3,4,5] = 5 := by decide
+example : foo [1,2,3,4,5] = 5 := by decide +kernel
+
+-- Open terms should not (these wouldn't even without the provisions with `WellFounded.Nat.eager`,
+-- the fuel does not line up)
+
+example : foo (x::xs) = 1 + foo xs := by (fail_if_success rfl); simp [foo]
+example : foo (x::y::z::xs) = 1+ (1+(1+ foo xs)) := by (fail_if_success rfl); simp [foo]
+
+end T1
+
+-- Variant where the fuel does not line up
+
+namespace T2
+@[semireducible] def foo : List α → Nat
+  | [] => 0
+  | _::xs => 1 + (foo xs)
+termination_by xs => 2 * xs.length
+
+example : foo ([] : List Unit) = 0 := rfl
+example : foo ([] : List Unit) = 0 := by decide
+example : foo ([] : List Unit) = 0 := by decide +kernel
+example : foo [1,2,3,4,5] = 5 := rfl
+example : foo [1,2,3,4,5] = 5 := by decide
+example : foo [1,2,3,4,5] = 5 := by decide +kernel
+
+-- Open terms should not (these wouldn't even without the provisions, the fuel does not line up)
+
+example : foo (x::xs) = 1 + foo xs := by (fail_if_success rfl); simp [foo]
+example : foo (x::y::z::xs) = 1+ (1 + ( 1+ foo xs)) := by (fail_if_success rfl); simp [foo]
+
+end T2
+
+-- Idiom to switch to `WellFounded.fix`
+
+namespace T3
+def foo : List α → Nat
+  | [] => 0
+  | _::xs => 1 + (foo xs)
+termination_by xs => (xs.length, 0)
+
+example : foo ([] : List Unit) = 0 := by (fail_if_success rfl); simp [foo]
+example : foo ([] : List Unit) = 0 := by (fail_if_success decide); simp [foo]
+example : foo ([] : List Unit) = 0 := by (fail_if_success decide +kernel); simp [foo]
+example : foo [1,2,3,4,5] = 5 := by (fail_if_success rfl); simp [foo]
+example : foo [1,2,3,4,5] = 5 := by (fail_if_success decide); simp [foo]
+example : foo [1,2,3,4,5] = 5 := by (fail_if_success decide +kernel); simp [foo]
+
+-- Open terms should not (these wouldn't even without the provisions, the fuel does not line up)
+
+example : foo (x::xs) = 1 + foo xs := by (fail_if_success rfl); simp [foo]
+example : foo (x::y::z::xs) = 1+ (1 + ( 1+ foo xs)) := by (fail_if_success rfl); simp [foo]
+
+end T3
+
+-- Defeq between similar functions
+
+namespace T4
+
+@[semireducible] def foo (b : Bool) : Nat → Nat
+  | 0 => 0
+  | n+1 => 1 + foo b n
+termination_by n => n
+
+@[semireducible] def bar (b : Bool) : Nat → Nat
+  | 0 => 0
+  | n+1 => cond b 1 2 + bar b n
+termination_by n => n
+
+@[semireducible] def baz : Nat → Nat
+  | 0 => 0
+  | n+1 => 1 + baz n
+termination_by n => n
+
+example : foo true n = bar true n := rfl
+example : foo true n = baz n := rfl
+example : bar true n = baz n := rfl
+
+end T4
+
+-- For comparison: with wfrec
+
+namespace T4wfrec
+
+def foo (b : Bool) : Nat → Nat
+  | 0 => 0
+  | n+1 => 1 + foo b n
+termination_by n => (n, 0)
+
+def bar (b : Bool) : Nat → Nat
+  | 0 => 0
+  | n+1 => cond b 1 2 + bar b n
+termination_by n => (n, 0)
+
+def baz : Nat → Nat
+  | 0 => 0
+  | n+1 => 1 + baz n
+termination_by n => (n, 0)
+
+example : foo true n = bar true n := by (fail_if_success rfl); sorry
+example : foo true n = baz n := by (fail_if_success rfl); sorry
+example : bar true n = baz n := by (fail_if_success rfl); sorry
+
+unseal foo bar baz
+
+example : foo true n = bar true n := rfl
+example : foo true n = baz n := rfl
+example : bar true n = baz n := rfl
+
+end T4wfrec
diff --git a/tests/lean/wfrecUnusedLet.lean.expected.out b/tests/lean/wfrecUnusedLet.lean.expected.out
index df3e7ff0de..6bea16a759 100644
--- a/tests/lean/wfrecUnusedLet.lean.expected.out
+++ b/tests/lean/wfrecUnusedLet.lean.expected.out
@@ -1,5 +1,5 @@
 @[irreducible] def f : Nat → Nat :=
-f._proof_1.fix fun n a =>
+WellFounded.Nat.fix (fun x => x) fun n a =>
   if h : n = 0 then 1
   else
     let y := 42;
diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean
index 3173550061..dbfab41f79 100644
--- a/tests/pkg/module/Module/Basic.lean
+++ b/tests/pkg/module/Module/Basic.lean
@@ -259,7 +259,7 @@ info: private theorem f_struct.eq_unfold : f_struct = fun x =>
 -/
 #guard_msgs(pass trace, all) in #print sig f_struct.eq_unfold
 
-/-- info: private theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/
+/-- info: @[defeq] private theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/
 #guard_msgs(pass trace, all) in #print sig f_wfrec.eq_1
 
 /--
@@ -279,7 +279,7 @@ info: private theorem f_wfrec.eq_unfold : f_wfrec = fun x x_1 =>
 -/
 #guard_msgs in #print sig f_wfrec.eq_unfold
 
-/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
+/-- info: @[defeq] theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
 #guard_msgs in #print sig f_exp_wfrec.eq_1
 
 /--
diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean
index 0972a63b62..8de160d484 100644
--- a/tests/pkg/module/Module/ImportedAll.lean
+++ b/tests/pkg/module/Module/ImportedAll.lean
@@ -105,7 +105,7 @@ info: theorem f_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → P
 -/
 #guard_msgs(pass trace, all) in #print sig f_wfrec.induct_unfolding
 
-/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
+/-- info: @[defeq] theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
 #guard_msgs in #print sig f_exp_wfrec.eq_1
 
 /--
diff --git a/tests/pkg/module/Module/NonModule.lean b/tests/pkg/module/Module/NonModule.lean
index 48bfa62e2b..5e2bb12dd6 100644
--- a/tests/pkg/module/Module/NonModule.lean
+++ b/tests/pkg/module/Module/NonModule.lean
@@ -54,7 +54,7 @@ info: theorem f_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → P
 -/
 #guard_msgs(pass trace, all) in #print sig f_wfrec.induct_unfolding
 
-/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
+/-- info: @[defeq] theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
 #guard_msgs(pass trace, all) in
 #print sig f_exp_wfrec.eq_1