diff --git a/RELEASES.md b/RELEASES.md
index 940cc2de9b..32378cc2a6 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -11,7 +11,18 @@ of each version.
 v4.9.0 (development in progress)
 ---------
 
-v4.8.0 
+* Functions defined by well-founded recursion are now marked as
+  `@[irreducible]`, which should prevent expensive and often unfruitful
+  unfolding of such definitions.
+
+  Existing proofs that hold by definitional equality (e.g. `rfl`) can be
+  rewritten to explictly unfold the function definition (using `simp`,
+  `unfold`, `rw`), or the recursive function can be temporariliy made
+  semireducible (using `unseal f in` before the command) or the function
+  definition itself can be marked as `@[semireducible]` to get the previous
+  behavor.
+
+v4.8.0
 ---------
 
 * **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index 3f9fc0f431..1a0f5b9113 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -11,6 +11,9 @@ import Init.ByCases
 import Init.Conv
 import Init.Omega
 
+-- Remove after the next stage0 update
+set_option allowUnsafeReducibility true
+
 namespace Fin
 
 /-- If you actually have an element of `Fin n`, then the `n` is always positive -/
@@ -205,6 +208,7 @@ theorem val_add_one {n : Nat} (i : Fin (n + 1)) :
   | .inl h => cases Fin.eq_of_val_eq h; simp
   | .inr h => simpa [Fin.ne_of_lt h] using val_add_one_of_lt h
 
+unseal Nat.modCore in
 @[simp] theorem val_two {n : Nat} : (2 : Fin (n + 3)).val = 2 := rfl
 
 theorem add_one_pos (i : Fin (n + 1)) (h : i < Fin.last n) : (0 : Fin (n + 1)) < i + 1 := by
@@ -239,6 +243,7 @@ theorem succ_ne_zero {n} : ∀ k : Fin n, Fin.succ k ≠ 0
 
 @[simp] theorem succ_zero_eq_one : Fin.succ (0 : Fin (n + 1)) = 1 := rfl
 
+unseal Nat.modCore in
 /-- Version of `succ_one_eq_two` to be used by `dsimp` -/
 @[simp] theorem succ_one_eq_two : Fin.succ (1 : Fin (n + 2)) = 2 := rfl
 
@@ -390,6 +395,7 @@ theorem castSucc_lt_last (a : Fin n) : castSucc a < last n := a.is_lt
 
 @[simp] theorem castSucc_zero : castSucc (0 : Fin (n + 1)) = 0 := rfl
 
+unseal Nat.modCore in
 @[simp] theorem castSucc_one {n : Nat} : castSucc (1 : Fin (n + 2)) = 1 := rfl
 
 /-- `castSucc i` is positive when `i` is positive -/
diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index d532d40a42..a6a33b293f 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -14,6 +14,8 @@ import Init.RCases
 # Lemmas about integer division needed to bootstrap `omega`.
 -/
 
+-- Remove after the next stage0 update
+set_option allowUnsafeReducibility true
 
 open Nat (succ)
 
@@ -142,12 +144,14 @@ theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => show -ofNat _ = _ by simp
 
+unseal Nat.div in
 @[simp] protected theorem div_zero : ∀ a : Int, div a 0 = 0
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => rfl
 
 @[simp] theorem zero_fdiv (b : Int) : fdiv 0 b = 0 := by cases b <;> rfl
 
+unseal Nat.div in
 @[simp] protected theorem fdiv_zero : ∀ a : Int, fdiv a 0 = 0
   | 0      => rfl
   | succ _ => rfl
@@ -765,11 +769,13 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
   | (n:Nat) => congrArg ofNat (Nat.div_one _)
   | -[n+1] => by simp [Int.div, neg_ofNat_succ]; rfl
 
+unseal Nat.div in
 @[simp] protected theorem div_neg : ∀ a b : Int, a.div (-b) = -(a.div b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
   | ofNat m, -[n+1] | -[m+1], succ n => (Int.neg_neg _).symm
   | ofNat m, succ n | -[m+1], 0 | -[m+1], -[n+1] => rfl
 
+unseal Nat.div in
 @[simp] protected theorem neg_div : ∀ a b : Int, (-a).div b = -(a.div b)
   | 0, n => by simp [Int.neg_zero]
   | succ m, (n:Nat) | -[m+1], 0 | -[m+1], -[n+1] => rfl
@@ -938,6 +944,7 @@ theorem fdiv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.fdiv b :
   match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_fdiv .. ▸ ofNat_zero_le _
 
+unseal Nat.div in
 theorem fdiv_nonpos : ∀ {a b : Int}, 0 ≤ a → b ≤ 0 → a.fdiv b ≤ 0
   | 0, 0, _, _ | 0, -[_+1], _, _ | succ _, 0, _, _ | succ _, -[_+1], _, _ => ⟨_⟩
 
diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index c59bff8945..53467f2982 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -50,7 +50,10 @@ noncomputable def div2Induction {motive : Nat → Sort u}
       apply hyp
       exact Nat.div_lt_self n_pos (Nat.le_refl _)
 
-@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by rfl
+@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by
+  simp only [HAnd.hAnd, AndOp.and, land]
+  unfold bitwise
+  simp
 
 @[simp] theorem and_zero (x : Nat) : x &&& 0 = 0 := by
   simp only [HAnd.hAnd, AndOp.and, land]
diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean
index c5a633e586..78961e04e0 100644
--- a/src/Init/Data/Nat/Gcd.lean
+++ b/src/Init/Data/Nat/Gcd.lean
@@ -37,11 +37,11 @@ def gcd (m n : @& Nat) : Nat :=
   termination_by m
   decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
 
-@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y :=
-  rfl
+@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y := by
+  rw [gcd]; rfl
 
-theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) :=
-  rfl
+theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) := by
+  rw [gcd]; rfl
 
 @[simp] theorem gcd_one_left (n : Nat) : gcd 1 n = 1 := by
   rw [gcd_succ, mod_one]
@@ -64,7 +64,7 @@ instance : Std.IdempotentOp gcd := ⟨gcd_self⟩
 
 theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
   match m with
-  | 0 => by have := (mod_zero n).symm; rwa [gcd_zero_right]
+  | 0 => by have := (mod_zero n).symm; rwa [gcd, gcd_zero_right]
   | _ + 1 => by simp [gcd_succ]
 
 @[elab_as_elim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat)
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index 50124336f2..af9f3104b1 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -677,6 +677,10 @@ protected theorem pow_lt_pow_iff_right {a n m : Nat} (h : 1 < a) :
 
 /-! ### log2 -/
 
+@[simp]
+theorem log2_zero : Nat.log2 0 = 0 := by
+  simp [Nat.log2]
+
 theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
   match k with
   | 0 => simp [show 1 ≤ n from Nat.pos_of_ne_zero h]
@@ -697,7 +701,7 @@ theorem log2_self_le (h : n ≠ 0) : 2 ^ n.log2 ≤ n := (le_log2 h).1 (Nat.le_r
 
 theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=
   match n with
-  | 0 => Nat.zero_lt_two
+  | 0 => by simp
   | n+1 => (log2_lt n.succ_ne_zero).1 (Nat.le_refl _)
 
 /-! ### dvd -/
diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
index 8b1c6ae689..41d69f15b8 100644
--- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -81,7 +81,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
     let (_, mvarId) ← main.mvarId!.intros
     let rec go (mvarId : MVarId) : MetaM Unit := do
       trace[Elab.definition.wf.eqns] "step\n{MessageData.ofGoal mvarId}"
-      if (← tryURefl mvarId) then
+      if ← withAtLeastTransparency .all (tryURefl mvarId) then
         return ()
       else if (← tryContradiction mvarId) then
         return ()
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index f05f560bb7..97a7560e84 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -132,12 +132,15 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
       return { unaryPreDef with value }
   trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}"
   let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d
-  if (← isOnlyOneUnaryDef preDefs fixedPrefixSize) then
-    addNonRec preDefNonRec (applyAttrAfterCompilation := false)
-  else
-    withEnableInfoTree false do
+  -- Do not complain if the user sets @[semireducible], which usually is a noop,
+  -- we recognize that below and then do not set @[irreducible]
+  withOptions (allowUnsafeReducibility.set · true) do
+    if (← isOnlyOneUnaryDef preDefs fixedPrefixSize) then
       addNonRec preDefNonRec (applyAttrAfterCompilation := false)
-    addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec
+    else
+      withEnableInfoTree false do
+        addNonRec preDefNonRec (applyAttrAfterCompilation := false)
+      addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec
   -- We create the `_unsafe_rec` before we abstract nested proofs.
   -- Reason: the nested proofs may be referring to the _unsafe_rec.
   addAndCompilePartialRec preDefs
@@ -146,6 +149,10 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   for preDef in preDefs do
     markAsRecursive preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
+    -- Unless the user asks for something else, mark the definition as irreducible
+    unless preDef.modifiers.attrs.any fun a =>
+      a.name = `semireducible || a.name = `reducible || a.name = `semireducible do
+      setIrreducibleAttribute preDef.declName
 
 builtin_initialize registerTraceClass `Elab.definition.wf
 
diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean
index f843f0e4fc..2dac2267a2 100644
--- a/src/Lean/ReducibilityAttrs.lean
+++ b/src/Lean/ReducibilityAttrs.lean
@@ -184,4 +184,9 @@ def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   | .irreducible => return true
   | _ => return false
 
+/-- Set the given declaration as `[irreducible]` -/
+def setIrreducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
+  setReducibilityStatus declName ReducibilityStatus.irreducible
+
+
 end Lean
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 0699845ba4..158ed2fe60 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please auto update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/1921.lean b/tests/lean/run/1921.lean
index bdde9e9c3d..39cb992987 100644
--- a/tests/lean/run/1921.lean
+++ b/tests/lean/run/1921.lean
@@ -6,4 +6,4 @@ def f := #[true].any id 0 USize.size
 -- `native_decide` used to prove `false` here, due to a bug in `Array.anyMUnsafe`.
 example : f = true := by native_decide
 
-example : f = true := by simp (config := { decide := true }) [f, Array.any, Array.anyM]
+example : f = true := by simp (config := { decide := true }) [f, Array.any, Array.anyM, Array.anyM.loop]
diff --git a/tests/lean/run/2389.lean b/tests/lean/run/2389.lean
index 6923e6c5e6..c1d6cc1df8 100644
--- a/tests/lean/run/2389.lean
+++ b/tests/lean/run/2389.lean
@@ -26,7 +26,9 @@ def onlyZeros : Tree → Prop
   | .node [] => True
   | .node (x::s) => onlyZeros x ∧ onlyZeros (.node s)
 
-/-- Pattern-matching on `OnlyZeros` works despite `below` and `brecOn` not being generated. -/
+unseal onlyZeros in
+/-- Pattern-matching on `OnlyZeros` works despite `below` and `brecOn` not being generated
+if we make `onlyZeros` semireducible-/
 def toFixPoint : OnlyZeros t → onlyZeros t
   | .leaf => rfl
   | .node [] _ => True.intro
diff --git a/tests/lean/run/ack.lean b/tests/lean/run/ack.lean
index 41fd2ed6ea..54c8166c8e 100644
--- a/tests/lean/run/ack.lean
+++ b/tests/lean/run/ack.lean
@@ -28,6 +28,7 @@ info: [reduction] unfolded declarations (max: 1725, num: 4):
    Acc.rec ↦ 754use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
+unseal ack in
 set_option diagnostics.threshold 500 in
 set_option diagnostics true in
 theorem ex : ack 3 2 = 29 :=
diff --git a/tests/lean/run/casesRec.lean b/tests/lean/run/casesRec.lean
index 2adf9e10e1..a8f4c639a2 100644
--- a/tests/lean/run/casesRec.lean
+++ b/tests/lean/run/casesRec.lean
@@ -8,7 +8,7 @@ def f (x : Nat) : Nat := by
 
 #eval f 10
 
-example : f x.succ = 2 * f x := rfl
+example : f x.succ = 2 * f x := by rw [f]; rfl
 end Ex1
 
 namespace Ex2
diff --git a/tests/lean/run/defaultEliminator.lean b/tests/lean/run/defaultEliminator.lean
index 5884879315..bc9c02f25a 100644
--- a/tests/lean/run/defaultEliminator.lean
+++ b/tests/lean/run/defaultEliminator.lean
@@ -22,7 +22,7 @@ termination_by (x, y)
 
 example (x y : Nat) : f x y > 0 := by
   induction x, y with
-  | zero_zero => decide
+  | zero_zero => simp [f]
   | succ_zero x ih => simp [f, ih]
   | zero_succ y ih => simp [f, ih]
   | succ_succ x y ih => simp [f, ih]
diff --git a/tests/lean/run/lazylistThunk.lean b/tests/lean/run/lazylistThunk.lean
index fc3f451ffb..785481da4f 100644
--- a/tests/lean/run/lazylistThunk.lean
+++ b/tests/lean/run/lazylistThunk.lean
@@ -25,7 +25,7 @@ in the list, ignoring delays
 
 theorem length_toList (l : LazyList α) : l.toList.length = l.length := by
   match l with
-  | nil => rfl
+  | nil => simp [length_toList]
   | cons a as => simp [length_toList as]
   | delayed as => simp [length_toList as.get]
 
diff --git a/tests/lean/run/splitIssue.lean b/tests/lean/run/splitIssue.lean
index b555f35416..fa0ee1dca1 100644
--- a/tests/lean/run/splitIssue.lean
+++ b/tests/lean/run/splitIssue.lean
@@ -15,23 +15,21 @@ termination_by l => l.length
 decreasing_by
   all_goals sorry
 
-theorem len_nil : len ([] : List α) = 0 := by
-  simp [len]
-
--- The `simp [len]` above generated the following equation theorems for len
+-- The equational theorems are
 #check @len.eq_1
 #check @len.eq_2
 #check @len.eq_3 -- It is conditional, and may be tricky to use.
+#check @len.eq_def
+
+theorem len_nil : len ([] : List α) = 0 := by
+  simp [len]
 
 theorem len_1 (a : α) : len [a] = 1 := by
   simp [len]
 
 theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
   conv => lhs; unfold len
-  rfl
-
--- The `unfold` tactic above generated the following theorem
-#check @len.eq_def
+  cases bs <;> simp [splitList, len_1]
 
 theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
   cases as with
@@ -41,7 +39,7 @@ theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
 theorem listlen : ∀ l : List α, l.length = len l := by
   intro l
   induction l with
-  | nil => rfl
+  | nil => simp [len]
   | cons h t ih =>
     simp [List.length, len_cons, ih]
     rw [Nat.add_comm]
diff --git a/tests/lean/run/splitList.lean b/tests/lean/run/splitList.lean
index 26f22f3a75..5d0229eb27 100644
--- a/tests/lean/run/splitList.lean
+++ b/tests/lean/run/splitList.lean
@@ -34,23 +34,21 @@ def len : List α → Nat
       len fst + len snd
 termination_by xs => xs.length
 
-theorem len_nil : len ([] : List α) = 0 := by
- simp [len]
 
--- The `simp [len]` above generated the following equation theorems for len
+-- The equational theorems are
 #check @len.eq_1
 #check @len.eq_2
 #check @len.eq_3
+#check @len.eq_def
+
+theorem len_nil : len ([] : List α) = 0 := by
+  simp [len]
 
 theorem len_1 (a : α) : len [a] = 1 := by
   simp [len]
 
 theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
-  conv => lhs; unfold len
-  rfl
-
--- The `unfold` tactic above generated the following theorem
-#check @len.eq_def
+  simp [len, splitList]
 
 theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
   cases as with
@@ -60,7 +58,7 @@ theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
 theorem listlen : ∀ l : List α, l.length = len l := by
   intro l
   induction l with
-  | nil => rfl
+  | nil => simp [len_nil]
   | cons h t ih =>
     simp [List.length, len_cons, ih]
     rw [Nat.add_comm]
@@ -85,23 +83,21 @@ decreasing_by
     subst h₂
     simp_arith [eq_of_heq h₃] at this |- ; simp [this]
 
-theorem len_nil : len ([] : List α) = 0 := by
-  simp [len]
-
--- The `simp [len]` above generated the following equation theorems for len
+-- The equational theorems are
 #check @len.eq_1
 #check @len.eq_2
 #check @len.eq_3
+#check @len.eq_def
+
+theorem len_nil : len ([] : List α) = 0 := by
+  simp [len]
 
 theorem len_1 (a : α) : len [a] = 1 := by
   simp [len]
 
 theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
   conv => lhs; unfold len
-  rfl
-
--- The `unfold` tactic above generated the following theorem
-#check @len.eq_def
+  simp [len, splitList]
 
 theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
   cases as with
@@ -111,7 +107,7 @@ theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
 theorem listlen : ∀ l : List α, l.length = len l := by
   intro l
   induction l with
-  | nil => rfl
+  | nil => simp [len_nil]
   | cons h t ih =>
     simp [List.length, len_cons, ih]
     rw [Nat.add_comm]
diff --git a/tests/lean/run/wfirred.lean b/tests/lean/run/wfirred.lean
new file mode 100644
index 0000000000..6916071e95
--- /dev/null
+++ b/tests/lean/run/wfirred.lean
@@ -0,0 +1,139 @@
+/-!
+Tests that definitions by well-founded recursion are irreducible.
+-/
+
+def foo : Nat → Nat
+  | 0 => 0
+  | n+1 => foo n
+termination_by n => n
+
+/--
+error: type mismatch
+  rfl
+has type
+  foo 0 = foo 0 : Prop
+but is expected to have type
+  foo 0 = 0 : Prop
+-/
+#guard_msgs in
+example : foo 0 = 0 := rfl
+
+/--
+error: type mismatch
+  rfl
+has type
+  foo (n + 1) = foo (n + 1) : Prop
+but is expected to have type
+  foo (n + 1) = foo n : Prop
+-/
+#guard_msgs in
+example : foo (n+1) = foo n := rfl
+
+-- This succeeding is a bug or misfeature in the rfl tactic, using the kernel defeq check
+#guard_msgs in
+example : foo 0 = 0 := by rfl
+
+-- It only works on closed terms:
+/--
+error: The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+n : Nat
+⊢ foo (n + 1) = foo n
+-/
+#guard_msgs in
+example : foo (n+1) = foo n := by rfl
+
+section Unsealed
+
+unseal foo
+
+example : foo 0 = 0 := rfl
+example : foo 0 = 0 := by rfl
+
+example : foo (n+1) = foo n := rfl
+example : foo (n+1) = foo n := by rfl
+
+end Unsealed
+
+--should be sealed again here
+
+/--
+error: type mismatch
+  rfl
+has type
+  foo 0 = foo 0 : Prop
+but is expected to have type
+  foo 0 = 0 : Prop
+-/
+#guard_msgs in
+example : foo 0 = 0 := rfl
+
+
+def bar : Nat → Nat
+  | 0 => 0
+  | n+1 => bar n
+termination_by n => n
+
+-- Once unsealed, the full internals are visible. This allows one to prove, for example
+
+/--
+error: type mismatch
+  rfl
+has type
+  foo = foo : Prop
+but is expected to have type
+  foo = bar : Prop
+-/
+#guard_msgs in
+example : foo = bar := rfl
+
+
+unseal foo bar in
+example : foo = bar := rfl
+
+
+-- Attributes on the definition take precedence
+@[semireducible] def baz : Nat → Nat
+  | 0 => 0
+  | n+1 => baz n
+termination_by n => n
+
+example : baz 0 = 0 := rfl
+
+seal baz in
+/--
+error: type mismatch
+  rfl
+has type
+  baz 0 = baz 0 : Prop
+but is expected to have type
+  baz 0 = 0 : Prop
+-/
+#guard_msgs in
+example : baz 0 = 0 := rfl
+
+example : baz 0 = 0 := rfl
+
+@[reducible] def quux : Nat → Nat
+  | 0 => 0
+  | n+1 => quux n
+termination_by n => n
+
+example : quux 0 = 0 := rfl
+
+set_option allowUnsafeReducibility true in
+seal quux in
+/--
+error: type mismatch
+  rfl
+has type
+  quux 0 = quux 0 : Prop
+but is expected to have type
+  quux 0 = 0 : Prop
+-/
+#guard_msgs in
+example : quux 0 = 0 := rfl
+
+example : quux 0 = 0 := rfl
diff --git a/tests/lean/wfrecUnusedLet.lean.expected.out b/tests/lean/wfrecUnusedLet.lean.expected.out
index 7fbd9db3dc..a9c7f8c558 100644
--- a/tests/lean/wfrecUnusedLet.lean.expected.out
+++ b/tests/lean/wfrecUnusedLet.lean.expected.out
@@ -1,4 +1,4 @@
-def f : Nat → Nat :=
+@[irreducible] def f : Nat → Nat :=
 f.proof_1.fix fun n a =>
   if h : n = 0 then 1
   else