diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 796d1de9b805..60abd4e74632 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -1156,6 +1156,7 @@ where
     finishElab headers
     processDeriving headers
   elabAsync header view declId := do
+    assert! view.kind.isTheorem
     let env ← getEnv
     let async ← env.addConstAsync declId.declName .thm
       (exportedKind? := guard (!isPrivateName declId.declName) *> some .axiom)
@@ -1178,6 +1179,12 @@ where
       s := collectLevelParams s type
       let scopeLevelNames ← getLevelNames
       let levelParams ← IO.ofExcept <| sortDeclLevelParams scopeLevelNames allUserLevelNames s.params
+
+      let type ← if cleanup.letToHave.get (← getOptions) then
+        withRef header.declId <| Meta.letToHave type
+      else
+        pure type
+
       async.commitSignature { name := header.declName, levelParams, type }
 
     -- attributes should be applied on the main thread; see below
diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index 9ae6132c9a72..e4b131c6b24b 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -13,6 +13,7 @@ import Lean.Util.NumApps
 import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.ForEachExpr
 import Lean.Meta.Eqns
+import Lean.Meta.LetToHave
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.DefView
 import Lean.Elab.PreDefinition.TerminationHint
@@ -21,6 +22,11 @@ namespace Lean.Elab
 open Meta
 open Term
 
+register_builtin_option cleanup.letToHave : Bool := {
+  defValue := true
+  descr    := "Enables transforming `let`s to `have`s after elaborating declarations."
+}
+
 /--
   A (potentially recursive) definition.
   The elaborator converts it into Kernel definitions using many different strategies.
@@ -88,6 +94,31 @@ def applyAttributesOf (preDefs : Array PreDefinition) (applicationTime : Attribu
   for preDef in preDefs do
     applyAttributesAt preDef.declName preDef.modifiers.attrs applicationTime
 
+/--
+Applies `Meta.letToHave` to the values of defs, instances, and abbrevs.
+Does not apply the transformation to values that are proofs, or to unsafe definitions.
+-/
+def letToHaveValue (preDef : PreDefinition) : MetaM PreDefinition := withRef preDef.ref do
+  if !cleanup.letToHave.get (← getOptions)
+      || preDef.modifiers.isUnsafe
+      || preDef.kind matches .theorem | .example | .opaque then
+    return preDef
+  else if ← Meta.isProp preDef.type then
+    return preDef
+  else
+    let value ← Meta.letToHave preDef.value
+    return { preDef with value }
+
+/--
+Applies `Meta.letToHave` to the type of the predef.
+-/
+def letToHaveType (preDef : PreDefinition) : MetaM PreDefinition := withRef preDef.ref do
+  if !cleanup.letToHave.get (← getOptions) || preDef.kind matches .example then
+    return preDef
+  else
+    let type ← Meta.letToHave preDef.type
+    return { preDef with type }
+
 def abstractNestedProofs (preDef : PreDefinition) (cache := true) : MetaM PreDefinition := withRef preDef.ref do
   if preDef.kind.isTheorem || preDef.kind.isExample then
     pure preDef
@@ -138,9 +169,11 @@ private def checkMeta (preDef : PreDefinition) : TermElabM Unit := do
       | _, _ => pure ()
     return true
 
-private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List Name) (applyAttrAfterCompilation := true) (cacheProofs := true) : TermElabM Unit :=
+private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List Name) (applyAttrAfterCompilation := true) (cacheProofs := true) (cleanupValue := false) : TermElabM Unit :=
   withRef preDef.ref do
     let preDef ← abstractNestedProofs (cache := cacheProofs) preDef
+    let preDef ← letToHaveType preDef
+    let preDef ← if cleanupValue then letToHaveValue preDef else pure preDef
     let mkDefDecl : TermElabM Declaration :=
       return Declaration.defnDecl {
           name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value
@@ -185,11 +218,11 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List N
       generateEagerEqns preDef.declName
       applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
-def addAndCompileNonRec (preDef : PreDefinition) (all : List Name := [preDef.declName]) : TermElabM Unit := do
-  addNonRecAux preDef (compile := true) (all := all)
+def addAndCompileNonRec (preDef : PreDefinition) (all : List Name := [preDef.declName]) (cleanupValue := false) : TermElabM Unit := do
+  addNonRecAux preDef (compile := true) (all := all) (cleanupValue := cleanupValue)
 
-def addNonRec (preDef : PreDefinition) (applyAttrAfterCompilation := true) (all : List Name := [preDef.declName]) (cacheProofs := true) : TermElabM Unit := do
-  addNonRecAux preDef (compile := false) (applyAttrAfterCompilation := applyAttrAfterCompilation) (all := all) (cacheProofs := cacheProofs)
+def addNonRec (preDef : PreDefinition) (applyAttrAfterCompilation := true) (all : List Name := [preDef.declName]) (cacheProofs := true) (cleanupValue := false) : TermElabM Unit := do
+  addNonRecAux preDef (compile := false) (applyAttrAfterCompilation := applyAttrAfterCompilation) (all := all) (cacheProofs := cacheProofs) (cleanupValue := cleanupValue)
 
 /--
   Eliminate recursive application annotations containing syntax. These annotations are used by the well-founded recursion module
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 7b6506cc03ba..c55ae3c05552 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -319,9 +319,9 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
           let preDef ← eraseRecAppSyntax preDefs[0]!
           ensureEqnReservedNamesAvailable preDef.declName
           if preDef.modifiers.isNoncomputable then
-            addNonRec preDef
+            addNonRec preDef (cleanupValue := true)
           else
-            addAndCompileNonRec preDef
+            addAndCompileNonRec preDef (cleanupValue := true)
           preDef.termination.ensureNone "not recursive"
         else if preDefs.any (·.modifiers.isUnsafe) then
           addAndCompileUnsafe preDefs
diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean
index d02f8e0cecf6..dea65694ef54 100644
--- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean
@@ -97,6 +97,7 @@ where
         catch e =>
           throwError "failed to generate unfold theorem for '{declName}':\n{e.toMessageData}"
       let type ← mkForallFVars xs type
+      let type ← letToHave type
       let value ← mkLambdaFVars xs goal
       addDecl <| Declaration.thmDecl {
         name, type, value
diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
index 890cc07902b0..8f71a848021a 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -93,6 +93,7 @@ where
   doRealize name type := withOptions (tactic.hygienic.set · false) do
     let value ← mkProof info.declName type
     let (type, value) ← removeUnusedEqnHypotheses type value
+    let type ← letToHave type
     addDecl <| Declaration.thmDecl {
       name, type, value
       levelParams := info.levelParams
@@ -126,6 +127,7 @@ where
       let goal ← mkFreshExprSyntheticOpaqueMVar type
       mkUnfoldProof declName goal.mvarId!
       let type ← mkForallFVars xs type
+      let type ← letToHave type
       let value ← mkLambdaFVars xs (← instantiateMVars goal)
       addDecl <| Declaration.thmDecl {
         name, type, value
diff --git a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean
index 215a770b6093..62a5f277adfe 100644
--- a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean
@@ -66,6 +66,6 @@ partial def addSmartUnfoldingDef (preDef : PreDefinition) (recArgPos : Nat) : Te
   else
     withEnableInfoTree false do
       let preDefSUnfold ← addSmartUnfoldingDefAux preDef recArgPos
-      addNonRec preDefSUnfold
+      addNonRec preDefSUnfold (cleanupValue := true)
 
 end Lean.Elab.Structural
diff --git a/src/Lean/Elab/PreDefinition/WF/Unfold.lean b/src/Lean/Elab/PreDefinition/WF/Unfold.lean
index 01373ec6493c..58ae0838d233 100644
--- a/src/Lean/Elab/PreDefinition/WF/Unfold.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Unfold.lean
@@ -91,6 +91,7 @@ def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) (wfPreprocessPr
 
       let value ← instantiateMVars main
       let type ← mkForallFVars xs type
+      let type ← letToHave type
       let value ← mkLambdaFVars xs value
       addDecl <| Declaration.thmDecl {
         name, type, value
@@ -123,6 +124,7 @@ def mkBinaryUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) : MetaM U
 
       let value ← instantiateMVars main
       let type ← mkForallFVars xs type
+      let type ← letToHave type
       let value ← mkLambdaFVars xs value
       addDecl <| Declaration.thmDecl {
         name, type, value
diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean
index acce8162dde2..1d296a8813b6 100644
--- a/src/Lean/Meta/Eqns.lean
+++ b/src/Lean/Meta/Eqns.lean
@@ -10,6 +10,7 @@ import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
 import Lean.Meta.Match.MatcherInfo
 import Lean.DefEqAttrib
+import Lean.Meta.LetToHave
 
 namespace Lean.Meta
 
@@ -178,6 +179,8 @@ where doRealize name info := do
   lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
     let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs
     let type  ← mkForallFVars xs (← mkEq lhs body)
+    -- Note: if this definition was added using `def`, then `letToHave` has already been applied to the body.
+    let type  ← letToHave type
     let value ← mkLambdaFVars xs (← mkEqRefl lhs)
     addDecl <| Declaration.thmDecl {
       name, type, value
diff --git a/src/Lean/Meta/LetToHave.lean b/src/Lean/Meta/LetToHave.lean
index 2a392a56b97e..677852c5ba7d 100644
--- a/src/Lean/Meta/LetToHave.lean
+++ b/src/Lean/Meta/LetToHave.lean
@@ -434,7 +434,7 @@ The `Meta.letToHave` trace class logs errors and messages.
 def letToHave (e : Expr) : MetaM Expr := do
   profileitM Exception "let-to-have transformation" (← getOptions) do
     let e ← instantiateMVars e
-    LetToHave.main e
+    withoutExporting <| LetToHave.main e
 
 builtin_initialize
   registerTraceClass `Meta.letToHave
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 2530ef121a5a..e5ca3d0172ae 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -1057,6 +1057,7 @@ where doRealize (inductName : Name) := do
 
   let eTyp ← inferType e'
   let eTyp ← elimTypeAnnotations eTyp
+  let eTyp ← letToHave eTyp
   -- logInfo m!"eTyp: {eTyp}"
   let levelParams := (collectLevelParams {} eTyp).params
   -- Prune unused level parameters, preserving the original order
@@ -1090,6 +1091,7 @@ def projectMutualInduct (unfolding : Bool) (names : Array Name) (mutualInduct :
         let value ← PProdN.projM names.size idx value
         mkLambdaFVars xs value
       let type ← inferType value
+      let type ← letToHave type
       addDecl <| Declaration.thmDecl { name := inductName, levelParams, type, value }
 
       if idx == 0 then finalizeFirstInd
@@ -1248,6 +1250,7 @@ where doRealize inductName := do
     check value
   let type ← inferType value
   let type ← elimOptParam type
+  let type ← letToHave type
 
   addDecl <| Declaration.thmDecl
     { name := inductName, levelParams := ci.levelParams, type, value }
@@ -1480,6 +1483,7 @@ where doRealize inductName := do
 
   let eTyp ← inferType e'
   let eTyp ← elimTypeAnnotations eTyp
+  let eTyp ← letToHave eTyp
   -- logInfo m!"eTyp: {eTyp}"
   let levelParams := (collectLevelParams {} eTyp).params
   -- Prune unused level parameters, preserving the original order
@@ -1623,6 +1627,7 @@ def deriveCases (unfolding : Bool) (name : Name) : MetaM Unit := do
 
     let eTyp ← inferType e'
     let eTyp ← elimTypeAnnotations eTyp
+    let eTyp ← letToHave eTyp
     -- logInfo m!"eTyp: {eTyp}"
     let levelParams := (collectLevelParams {} eTyp).params
     -- Prune unused level parameters, preserving the original order
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index 182bc2660dda..5330b8741d45 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -37,8 +37,8 @@ partial def parserNodeKind? (e : Expr) : MetaM (Option Name) := do
   let reduceEval? e : MetaM (Option Name) := do
     try pure <| some (← reduceEval e) catch _ => pure none
   let e ← whnfCore e
-  if e matches Expr.lam .. then
-    lambdaLetTelescope e fun _ e => parserNodeKind? e
+  if e matches Expr.lam .. | Expr.letE .. then
+    lambdaLetTelescope (preserveNondepLet := false) e fun _ e => parserNodeKind? e
   else if e.isAppOfArity ``leadingNode 3 || e.isAppOfArity ``trailingNode 4 || e.isAppOfArity ``node 2 then
     reduceEval? (e.getArg! 0)
   else if e.isAppOfArity ``withAntiquot 2 then
@@ -61,7 +61,7 @@ variable {α} (ctx : Context α) (builtin : Bool) (force : Bool) in
 partial def compileParserExpr (e : Expr) : MetaM Expr := do
   let e ← whnfCore e
   match e with
-  | .lam ..  => mapLambdaLetTelescope e fun _ b => compileParserExpr b
+  | .lam .. | .letE .. => mapLambdaLetTelescope (preserveNondepLet := false) e fun _ b => compileParserExpr b
   | .fvar .. => return e
   | _ => do
     let fn := e.getAppFn
diff --git a/tests/lean/445.lean.expected.out b/tests/lean/445.lean.expected.out
index 816015d5d61d..512da23bf880 100644
--- a/tests/lean/445.lean.expected.out
+++ b/tests/lean/445.lean.expected.out
@@ -11,5 +11,5 @@ i + 1
 i + i * 2
 i + i * r i j
 i + i * r i j
-let z := s i j;
+have z := s i j;
 z + z
diff --git a/tests/lean/funind_errors.lean.expected.out b/tests/lean/funind_errors.lean.expected.out
index d6b20de5fcc7..6e9d9f21b774 100644
--- a/tests/lean/funind_errors.lean.expected.out
+++ b/tests/lean/funind_errors.lean.expected.out
@@ -3,11 +3,11 @@ funind_errors.lean:22:7-22:23: error: unknown constant 'takeWhile.induct'
 takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (motive : Nat → Array α → Prop)
   (case1 :
     ∀ (i : Nat) (r : Array α) (h : i < as.size),
-      let a := as.get i h;
+      have a := as.get i h;
       p a = true → motive (i + 1) (r.push a) → motive i r)
   (case2 :
     ∀ (i : Nat) (r : Array α) (h : i < as.size),
-      let a := as.get i h;
+      have a := as.get i h;
       ¬p a = true → motive i r)
   (case3 : ∀ (i : Nat) (r : Array α), ¬i < as.size → motive i r) (i : Nat) (r : Array α) : motive i r
 funind_errors.lean:38:7-38:20: error: unknown constant 'idEven.induct'
diff --git a/tests/lean/run/1026.lean b/tests/lean/run/1026.lean
index 995c9114c403..fd649b794fca 100644
--- a/tests/lean/run/1026.lean
+++ b/tests/lean/run/1026.lean
@@ -15,9 +15,21 @@ info: foo.eq_def (n : Nat) :
   foo n =
     if n = 0 then 0
     else
-      let x := n - 1;
+      have x := n - 1;
       have this := foo._proof_4;
       foo x
 -/
 #guard_msgs in
 #check foo.eq_def
+
+/--
+info: foo.eq_unfold :
+  foo = fun n =>
+    if n = 0 then 0
+    else
+      have x := n - 1;
+      have this := foo._proof_4;
+      foo x
+-/
+#guard_msgs in
+#check foo.eq_unfold
diff --git a/tests/lean/run/2058.lean b/tests/lean/run/2058.lean
index c86998069138..dc645cf234d8 100644
--- a/tests/lean/run/2058.lean
+++ b/tests/lean/run/2058.lean
@@ -39,7 +39,7 @@ def foo : IO Unit := do
 -- specializes to 0 on error
 /--
 info: def foo : IO Unit :=
-let x := PUnit.unit.{0};
+have x := PUnit.unit.{0};
 pure.{0, 0} Unit.unit
 -/
 #guard_msgs in set_option pp.universes true in #print foo
diff --git a/tests/lean/run/delabConst.lean b/tests/lean/run/delabConst.lean
index 868a33e400f0..c6fb2bd9d361 100644
--- a/tests/lean/run/delabConst.lean
+++ b/tests/lean/run/delabConst.lean
@@ -141,7 +141,7 @@ def f (true : Bool) : Nat :=
 /--
 info: def MatchTest2.f : Bool → Nat :=
 fun true =>
-  let Bool.true := 1;
+  have Bool.true := 1;
   match true with
   | _root_.Bool.true => 0
   | false => 1
@@ -169,8 +169,8 @@ def f (true : Bool) :=
 /--
 info: def MatchTest3.f : Bool → Bool :=
 fun true =>
-  let Bool.true := true;
-  let false := true;
+  have Bool.true := true;
+  have false := true;
   match true with
   | _root_.Bool.true => false
   | Bool.false =>
diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean
index 59a8f0f33fbf..a8fe7d604c36 100644
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -733,11 +733,11 @@ def foo (n : Nat) : Nat :=
 info: Dite.foo.induct (motive : Nat → Prop)
   (case1 :
     ∀ (x : Nat),
-      let j := x - 1;
+      have j := x - 1;
       j < x → motive j → motive x)
   (case2 :
     ∀ (x : Nat),
-      let j := x - 1;
+      have j := x - 1;
       ¬j < x → motive x)
   (n : Nat) : motive n
 -/
diff --git a/tests/lean/run/funind_unfolding.lean b/tests/lean/run/funind_unfolding.lean
index c149c1c74ae3..d66d6f9294b5 100644
--- a/tests/lean/run/funind_unfolding.lean
+++ b/tests/lean/run/funind_unfolding.lean
@@ -57,11 +57,11 @@ def fib'' (n : Nat) : Nat :=
 info: fib''.fun_cases_unfolding (n : Nat) (motive : Nat → Prop) (case1 : n < 2 → motive n)
   (case2 :
     ¬n < 2 →
-      let foo := n - 2;
+      have foo := n - 2;
       foo < 100 → motive (fib'' (n - 1) + fib'' foo))
   (case3 :
     ¬n < 2 →
-      let foo := n - 2;
+      have foo := n - 2;
       ¬foo < 100 → motive 0) :
   motive (fib'' n)
 -/
@@ -381,7 +381,7 @@ info: siftDown.induct_unfolding (e : Nat) (motive : (a : Array Int) → Nat →
     ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size),
       leftChild root < e →
         let child := leftChild root;
-        let child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child;
+        have child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child;
         ¬a[root]! < a[child]! → motive a root h a)
   (case3 : ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), ¬leftChild root < e → motive a root h a) (a : Array Int)
   (root : Nat) (h : e ≤ a.size) : motive a root h (siftDown a root e h)
@@ -403,7 +403,7 @@ info: siftDown.induct (e : Nat) (motive : (a : Array Int) → Nat → e ≤ a.si
     ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size),
       leftChild root < e →
         let child := leftChild root;
-        let child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child;
+        have child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child;
         ¬a[root]! < a[child]! → motive a root h)
   (case3 : ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), ¬leftChild root < e → motive a root h) (a : Array Int)
   (root : Nat) (h : e ≤ a.size) : motive a root h
diff --git a/tests/lean/run/issue5767.lean b/tests/lean/run/issue5767.lean
index c7ced93d71f5..920b197c1741 100644
--- a/tests/lean/run/issue5767.lean
+++ b/tests/lean/run/issue5767.lean
@@ -24,11 +24,11 @@ def go1 (ss : Int) (st0 : St) : Bool :=
 info: go1.induct (ss : Int) (motive : St → Prop)
   (case1 :
     ∀ (x : St),
-      let st1 := { m := x.m, map := x.map.insert };
+      have st1 := { m := x.m, map := x.map.insert };
       ∀ (val : Unit), st1.map.get? ss = some val → P st1 → P st1 → motive st1 → motive x)
   (case2 :
     ∀ (x : St),
-      let st1 := { m := x.m, map := x.map.insert };
+      have st1 := { m := x.m, map := x.map.insert };
       st1.map.get? ss = none → motive x)
   (st0 : St) : motive st0
 -/
@@ -55,7 +55,7 @@ def go2 (ss : Int) (st0 : St) : Bool :=
 /--
 info: go2.induct : ∀ (motive : St → Prop),
   (∀ (x : St),
-      let st1 := { m := x.m, map := x.map.insert };
+      have st1 := { m := x.m, map := x.map.insert };
       motive st1 → motive x) →
     ∀ (st0 : St), motive st0
 -/
diff --git a/tests/lean/run/letToHaveCleanup.lean b/tests/lean/run/letToHaveCleanup.lean
new file mode 100644
index 000000000000..dd13cf1d67c1
--- /dev/null
+++ b/tests/lean/run/letToHaveCleanup.lean
@@ -0,0 +1,342 @@
+import Lean
+/-!
+## Checking that let-to-have is applied to definitions and equation lemmas
+-/
+
+set_option pp.letVarTypes true
+set_option pp.mvars.anonymous false
+
+/-!
+Non-recursive definitions have the transformation applied on the declaration itself.
+-/
+
+def fnNonRec (n : Nat) : let α := Nat; α :=
+  let m := n + 1
+  m
+/--
+info: def fnNonRec : Nat →
+  have α : Type := Nat;
+  α :=
+fun n =>
+  have m : Nat := n + 1;
+  m
+-/
+#guard_msgs in #print fnNonRec
+/--
+info: fnNonRec.eq_def (n : Nat) :
+  fnNonRec n =
+    have m : Nat := n + 1;
+    m
+-/
+#guard_msgs in #check fnNonRec.eq_def
+/--
+info: fnNonRec.eq_unfold :
+  fnNonRec = fun n =>
+    have m : Nat := n + 1;
+    m
+-/
+#guard_msgs in #check fnNonRec.eq_unfold
+
+
+/-!
+For theorems, the proof doesn't get transformed, but the type does.
+-/
+theorem thm : let n := 1; n = 1 := by
+  let m := 1
+  intro
+  exact Eq.refl m
+/--
+info: theorem thm : have n : Nat := 1;
+n = 1 :=
+let m : Nat := 1;
+let n : Nat := 1;
+Eq.refl m
+-/
+#guard_msgs in #print thm
+
+
+/-!
+Structural recursion doesn't apply the transformation to the declaration value itself,
+but it's done to the type and to the equation lemmas.
+
+The smart unfolding definition has the transformation applied to the value.
+-/
+
+def fnStructRec (n : Nat) : let α := Nat; α :=
+  match n with
+  | 0 => 0
+  | n + 1 => id (let m := n + 1; m * fnStructRec n)
+/--
+info: def fnStructRec : Nat →
+  have α : Type := Nat;
+  α :=
+fun n =>
+  Nat.brecOn n fun n f =>
+    (match (motive :=
+        (n : Nat) →
+          Nat.below n →
+            let α : Type := Nat;
+            α)
+        n with
+      | 0 => fun x => 0
+      | n.succ => fun x =>
+        id
+          (let m : Nat := n + 1;
+          m * x.1))
+      f
+-/
+#guard_msgs in #print fnStructRec
+/--
+info: fnStructRec.eq_def (n : Nat) :
+  fnStructRec n =
+    match n with
+    | 0 => 0
+    | n.succ =>
+      id
+        (have m : Nat := n + 1;
+        m * fnStructRec n)
+-/
+#guard_msgs in #check fnStructRec.eq_def
+/-- info: fnStructRec.eq_1 : fnStructRec 0 = 0 -/
+#guard_msgs in #check fnStructRec.eq_1
+/--
+info: fnStructRec.eq_2 (n_2 : Nat) :
+  fnStructRec n_2.succ =
+    id
+      (have m : Nat := n_2 + 1;
+      m * fnStructRec n_2)
+-/
+#guard_msgs in #check fnStructRec.eq_2
+/--
+info: def fnStructRec._sunfold : Nat →
+  have α : Type := Nat;
+  α :=
+fun n =>
+  match n with
+  | 0 => 0
+  | n.succ =>
+    id
+      (have m : Nat := n + 1;
+      m * fnStructRec n)
+-/
+#guard_msgs in #print fnStructRec._sunfold
+
+/-!
+Smart unfolding check
+-/
+open Lean Elab Command in
+elab "#unfold1 " t:term : command => do
+  runTermElabM fun _ => do
+    let e ← Term.withSynthesize <| Term.elabTerm t none
+    let e? ← Meta.unfoldDefinition? e
+    logInfo m!"{e?}"
+/-- info: 0 -/
+#guard_msgs in #unfold1 fnStructRec 0
+/--
+info: id
+  (have m : Nat := 0 + 1;
+  m * fnStructRec 0)
+-/
+#guard_msgs in #unfold1 fnStructRec 1
+/--
+info: Nat.brecOn 1 fun n f =>
+  (match (motive :=
+      (n : Nat) →
+        Nat.below n →
+          let α : Type := Nat;
+          α)
+      n with
+    | 0 => fun x => 0
+    | n.succ => fun x =>
+      id
+        (let m : Nat := n + 1;
+        m * x.1))
+    f
+-/
+#guard_msgs in
+set_option smartUnfolding false in
+#unfold1 fnStructRec 1
+
+
+/-!
+Well-founded recursion doesn't apply the transformation to the declaration value itself,
+but it's done to the type and to the equation lemmas.
+-/
+
+def fnWFRec (n : Nat) : let α := Nat; α :=
+  match n with
+  | 0 => 0
+  | n + 1 => id (let m := n + 1; m * fnWFRec (n / 2))
+/--
+info: @[irreducible] def fnWFRec : Nat →
+  have α : Type := Nat;
+  α :=
+fnWFRec._proof_1.fix fun n a =>
+  (match (motive :=
+      (n : Nat) →
+        ((y : Nat) →
+            (invImage (fun x => x) sizeOfWFRel).1 y n →
+              let α : Type := Nat;
+              α) →
+          let α : Type := Nat;
+          α)
+      n with
+    | 0 => fun x => 0
+    | n.succ => fun x =>
+      id
+        (let m : Nat := n + 1;
+        m * x (n / 2) ⋯))
+    a
+-/
+#guard_msgs in #print fnWFRec
+/--
+info: fnWFRec.eq_def (n : Nat) :
+  fnWFRec n =
+    match n with
+    | 0 => 0
+    | n.succ =>
+      id
+        (have m : Nat := n + 1;
+        m * fnWFRec (n / 2))
+-/
+#guard_msgs in #check fnWFRec.eq_def
+/-- info: fnWFRec.eq_1 : fnWFRec 0 = 0 -/
+#guard_msgs in #check fnWFRec.eq_1
+/--
+info: fnWFRec.eq_2 (n_2 : Nat) :
+  fnWFRec n_2.succ =
+    id
+      (have m : Nat := n_2 + 1;
+      m * fnWFRec (n_2 / 2))
+-/
+#guard_msgs in #check fnWFRec.eq_2
+
+
+/-!
+Partial fixedpoint doesn't apply the transformation to the declaration value itself,
+but it's done to the type and to the equation lemmas.
+-/
+
+def fnPartialFixpoint (n : Nat) : let α := Nat; α :=
+  fnPartialFixpoint (let m := n + 1; m)
+partial_fixpoint
+/--
+info: @[irreducible] def fnPartialFixpoint : Nat →
+  have α : Type := Nat;
+  α :=
+Lean.Order.fix
+  (fun f n =>
+    f
+      (let m : Nat := n + 1;
+      m))
+  fnPartialFixpoint._proof_2
+-/
+#guard_msgs in #print fnPartialFixpoint
+/--
+info: fnPartialFixpoint.eq_def (n : Nat) :
+  fnPartialFixpoint n =
+    fnPartialFixpoint
+      (have m : Nat := n + 1;
+      m)
+-/
+#guard_msgs in #check fnPartialFixpoint.eq_def
+/--
+info: fnPartialFixpoint.eq_1 (n : Nat) :
+  fnPartialFixpoint n =
+    fnPartialFixpoint
+      (have m : Nat := n + 1;
+      m)
+-/
+#guard_msgs in #check fnPartialFixpoint.eq_1
+
+
+/-!
+Do notation, non-recursive.
+Note that the pretty printed `let __do_lift`s in the following are from the `do` notation itself;
+these are not `let` expressions.
+-/
+open Lean in
+def fnDo (x : MetaM Bool) (y : Nat → MetaM α) : MetaM (Array α) := do
+  let a := (← x)
+  if a then
+    let mut arr := #[]
+    for i in [0:10] do
+      let b := (← y i)
+      arr := arr.push b
+    return arr
+  else
+    return #[]
+/--
+info: def fnDo : {α : Type} → Lean.MetaM Bool → (Nat → Lean.MetaM α) → Lean.MetaM (Array α) :=
+fun {α} x y => do
+  let __do_lift ← x
+  have a : Bool := __do_lift
+  if a = true then
+      have arr : Array α := #[];
+      do
+      let r ←
+        forIn { stop := 10, step_pos := Nat.zero_lt_one } arr fun i r =>
+            have arr : Array α := r;
+            do
+            let __do_lift ← y i
+            have b : α := __do_lift
+            have arr : Array α := arr.push b
+            pure PUnit.unit
+            pure (ForInStep.yield arr)
+      have arr : Array α := r
+      pure arr
+    else pure #[]
+-/
+#guard_msgs in #print fnDo
+
+
+section
+/-!
+Tests of cases when `letToHave` is run.
+These are verifying that either it's not run, or when there are no `let`s the transformation is skipped.
+-/
+set_option trace.Meta.letToHave true
+
+/--
+trace: [Meta.letToHave] ✅️ no `let` expressions
+[Meta.letToHave] ✅️ no `let` expressions
+-/
+#guard_msgs in
+def fnNoLet (n : Nat) := n
+
+-- Not run for `example` at all.
+#guard_msgs in
+example (n : Nat) := n
+
+/-! Two times, once for `async.commitSignature`, another for `addDecl`, and only on the type. -/
+/--
+trace: [Meta.letToHave] ✅️ no `let` expressions
+---
+trace: [Meta.letToHave] ✅️ no `let` expressions
+-/
+#guard_msgs in
+theorem thmNoLet : True := let x := trivial; x
+/-! With async disabled, only applied once. -/
+/-- trace: [Meta.letToHave] ✅️ no `let` expressions -/
+#guard_msgs in
+set_option Elab.async false in
+theorem thmNoLet' : True := let x := trivial; x
+
+structure A where
+
+/--
+trace: [Meta.letToHave] ✅️ no `let` expressions
+[Meta.letToHave] ✅️ transformed 1 `let` expressions into `have` expressions
+  [Meta.letToHave] result:
+        have x : Inhabited A := { default := { } };
+        x
+-/
+#guard_msgs in
+instance : Inhabited A := let x := ⟨{}⟩; x
+
+/-! It's a theorem instance. Only applied to the type. -/
+/-- trace: [Meta.letToHave] ✅️ no `let` expressions -/
+#guard_msgs in
+instance : Nonempty A := let x := ⟨{}⟩; x
+
+end
diff --git a/tests/lean/run/magical.lean b/tests/lean/run/magical.lean
new file mode 100644
index 000000000000..d586e4602c73
--- /dev/null
+++ b/tests/lean/run/magical.lean
@@ -0,0 +1,111 @@
+import Lean
+/-!
+# The kernel does not allow primitive projections on propositions
+
+This test is adapted from the test introduced in commits
+7920db952116e838b31c6f59f17bde0af01df545 and 3746005f5fc35d030d26ced2f7bcaabc295224c2,
+and which was removed in #8986 because the elaborator is better at rejecting them.
+In this version, we do direct tests of the kernel.
+-/
+
+open Lean Meta
+
+set_option pp.proofs true
+
+/-!
+Projection to the witness should be rejected.
+
+This test is creating the declaration
+```
+def test.witness : Nat := (Exists.intro 0 True.intro : ∃ x : Nat, True).1
+```
+-/
+/--
+error: (kernel) invalid projection
+  (Exists.intro Nat.zero True.intro).1
+-/
+#guard_msgs in
+#eval do
+  addDecl <| .defnDecl {
+    name := `test.witness
+    levelParams := []
+    type := mkConst `Nat
+    hints := .abbrev
+    safety := .safe
+    value :=
+      mkProj ``Exists 0 <|
+        mkApp4 (mkConst ``Exists.intro [levelOne])
+          (mkConst ``Nat)
+          (mkLambda `x .default (mkConst ``Nat) (mkConst ``True))
+          (mkConst ``Nat.zero)
+          (mkConst ``True.intro)
+  }
+
+/-!
+`Subtype` version is accepted. (This is to check that the expression above was constructed correctly.)
+-/
+#guard_msgs in
+#eval do
+  addDecl <| .defnDecl {
+    name := `test.witness'
+    levelParams := []
+    type := mkConst `Nat
+    hints := .abbrev
+    safety := .safe
+    value :=
+      mkProj ``Subtype 0 <|
+        mkApp4 (mkConst ``Subtype.mk [levelOne])
+          (mkConst ``Nat)
+          (mkLambda `x .default (mkConst ``Nat) (mkConst ``True))
+          (mkConst ``Nat.zero)
+          (mkConst ``True.intro)
+  }
+
+/-!
+Projection to the property should be rejected as well (it could contain the witness projection).
+
+This test is creating the declaration
+```
+theorem test.witness_eq (h : ∃ x : Nat, True) : h.2 = h.2 := rfl
+```
+-/
+/--
+error: (kernel) invalid projection
+  h.2
+-/
+#guard_msgs in
+#eval do
+  addDecl <| .thmDecl {
+    name := `test.witness_eq
+    levelParams := []
+    type :=
+      mkForall `h .default
+        (mkApp2 (mkConst ``Exists [levelOne]) (mkConst ``Nat) (mkLambda `x .default (mkConst ``Nat) (mkConst ``True)))
+        (mkApp3 (mkConst ``Eq [levelZero])
+          (mkConst ``True)
+          (mkProj ``Exists 1 (mkBVar 0))
+          (mkProj ``Exists 1 (mkBVar 0)))
+    value := mkLambda `h .default
+      (mkApp2 (mkConst ``Exists [levelOne]) (mkConst ``Nat) (mkLambda `x .default (mkConst ``Nat) (mkConst ``True)))
+      (mkApp2 (mkConst ``Eq.refl [levelZero]) (mkConst ``True) (mkProj ``Exists 1 (mkBVar 0)))
+  }
+
+/-!
+`Subtype` version is accepted. (This is to check that the expression above was constructed correctly.)
+-/
+#guard_msgs in
+#eval do
+  addDecl <| .thmDecl {
+    name := `test.witness_eq'
+    levelParams := []
+    type :=
+      mkForall `h .default
+        (mkApp2 (mkConst ``Subtype [levelOne]) (mkConst ``Nat) (mkLambda `x .default (mkConst ``Nat) (mkConst ``True)))
+        (mkApp3 (mkConst ``Eq [levelZero])
+          (mkConst ``True)
+          (mkProj ``Subtype 1 (mkBVar 0))
+          (mkProj ``Subtype 1 (mkBVar 0)))
+    value := mkLambda `h .default
+      (mkApp2 (mkConst ``Subtype [levelOne]) (mkConst ``Nat) (mkLambda `x .default (mkConst ``Nat) (mkConst ``True)))
+      (mkApp2 (mkConst ``Eq.refl [levelZero]) (mkConst ``True) (mkProj ``Subtype 1 (mkBVar 0)))
+  }
diff --git a/tests/lean/run/prefixTableStep.lean b/tests/lean/run/prefixTableStep.lean
index 28c16afb93a5..8959ad202dc8 100644
--- a/tests/lean/run/prefixTableStep.lean
+++ b/tests/lean/run/prefixTableStep.lean
@@ -27,7 +27,7 @@ info: PrefixTable.step.eq_def.{u_1} {α : Type u_1} [BEq α] (t : PrefixTable α
   t.step x kf =
     match kf with
     | ⟨k, hk⟩ =>
-      let cont := fun x_1 =>
+      have cont := fun x_1 =>
         match k, hk with
         | 0, hk => ⟨0, ⋯⟩
         | k.succ, hk =>
diff --git a/tests/lean/run/rflTacticErrors.lean b/tests/lean/run/rflTacticErrors.lean
index 750b23ca014d..b5e3c2d2d265 100644
--- a/tests/lean/run/rflTacticErrors.lean
+++ b/tests/lean/run/rflTacticErrors.lean
@@ -8,6 +8,8 @@ This file tests the `rfl` tactic:
  * Effect of `with_reducible`
 -/
 
+set_option pp.mvars.levels false
+
 -- First, let's see what `rfl` does:
 
 /--
diff --git a/tests/lean/run/structInst3.lean b/tests/lean/run/structInst3.lean
index 91d4c62f136a..966266b52b38 100644
--- a/tests/lean/run/structInst3.lean
+++ b/tests/lean/run/structInst3.lean
@@ -31,7 +31,7 @@ rfl
 
 /--
 info: ex1 :
-  (let __src := c1;
+  (have __src := c1;
       { toB := __src.toB, z := 2 : C Nat }).z =
     2
 -/
@@ -42,7 +42,7 @@ rfl
 
 /--
 info: ex2 :
-  (let __src := c1;
+  (have __src := c1;
       { toB := __src.toB, z := 2 : C Nat }).x =
     c1.x
 -/
diff --git a/tests/lean/run/structInstExtraEta.lean b/tests/lean/run/structInstExtraEta.lean
index 4bdfc01fd2c2..d9377deda0a6 100644
--- a/tests/lean/run/structInstExtraEta.lean
+++ b/tests/lean/run/structInstExtraEta.lean
@@ -20,7 +20,7 @@ def a : A := ⟨ 0 ⟩
 def b : B := { a with }
 /--
 info: def b : B :=
-let __src := a;
+have __src := a;
 { toA := __src }
 -/
 #guard_msgs in #print b
@@ -28,7 +28,7 @@ let __src := a;
 def c : C := { a with }
 /--
 info: def c : C :=
-let __src := a;
+have __src := a;
 { toB := { toA := __src } }
 -/
 #guard_msgs in #print c
@@ -36,7 +36,7 @@ let __src := a;
 def d : D := { c with }
 /--
 info: def d : D :=
-let __src := c;
+have __src := c;
 { toB := __src.toB }
 -/
 #guard_msgs in #print d
diff --git a/tests/lean/run/wf_preprocess.lean b/tests/lean/run/wf_preprocess.lean
index 22a771d5a43a..c1d07426d484 100644
--- a/tests/lean/run/wf_preprocess.lean
+++ b/tests/lean/run/wf_preprocess.lean
@@ -206,23 +206,23 @@ decreasing_by
 info: equations:
 theorem MTree.size.eq_1.{u_1} : ∀ {α : Type u_1} (t : MTree α),
   t.size =
-    (let s := 1;
+    (have s := 1;
       do
       let r ←
         forIn t.cs s fun css r =>
-            let s := r;
+            have s := r;
             do
             let r ←
               forIn css s fun c r =>
-                  let s := r;
-                  let s := s + c.size;
+                  have s := r;
+                  have s := s + c.size;
                   do
                   pure PUnit.unit
                   pure (ForInStep.yield s)
-            let s : Nat := r
+            have s : Nat := r
             pure PUnit.unit
             pure (ForInStep.yield s)
-      let s : Nat := r
+      have s : Nat := r
       pure s).run
 -/
 #guard_msgs in
diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out
index 8070fab5c776..21cc51e4d748 100644
--- a/tests/lean/simp_trace.lean.expected.out
+++ b/tests/lean/simp_trace.lean.expected.out
@@ -40,7 +40,7 @@ Try this: simp only [foo]
     ==>
       True
 Try this: simp only [g, pure]
-[Meta.Tactic.simp.rewrite] unfold g, g x ==> (let x := x;
+[Meta.Tactic.simp.rewrite] unfold g, g x ==> (have x := x;
       pure x).run
 Try this: simp (config := { unfoldPartialApp := true }) only [f1, modify, modifyGet, MonadStateOf.modifyGet,
   StateT.modifyGet, pure, f2, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, set, StateT.set]
diff --git a/tests/lean/unusedLet.lean.expected.out b/tests/lean/unusedLet.lean.expected.out
index 8966ef27fc23..5a54516e81f0 100644
--- a/tests/lean/unusedLet.lean.expected.out
+++ b/tests/lean/unusedLet.lean.expected.out
@@ -1,5 +1,5 @@
 def pro : Bool :=
-let x := 42;
+have x := 42;
 false
 def f : Nat → Nat :=
 fun x =>