diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 5c3c607a1d..0a0bb7c055 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -785,54 +785,33 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
       pure (type, val, binders)
   let kind := kindOfBinderName id.getId
   trace[Elab.let.decl] "{id.getId} : {type} := {val}"
-  let elabBody : TermElabM Expr := do
-    let body ← elabTermEnsuringType body expectedType?
-    instantiateMVars body
   let result ←
-    if config.zeta then
-      let elabZetaCore (x : Expr) : TermElabM Expr := do
-        addLocalVarInfo id x
-        if let some h := config.eq? then
-          let hTy ← mkEq x val
-          withLocalDeclD h.getId hTy fun h' => do
-            addLocalVarInfo h h'
-            let body ← elabBody
-            pure <| (← body.abstractM #[x, h']).instantiateRev #[val, ← mkEqRefl val]
-        else
-          let body ← elabBody
+    withLetDecl id.getId (kind := kind) type val (nondep := config.nondep) fun x => do
+      let elabBody : TermElabM Expr :=
+        elabTermEnsuringType body expectedType? >>= instantiateMVars
+      addLocalVarInfo id x
+      match config.eq? with
+      | none =>
+        let body ← elabBody
+        if config.zeta then
           pure <| (← body.abstractM #[x]).instantiate1 val
-      if !config.nondep then
-        withLetDecl id.getId (kind := kind) type val elabZetaCore
-      else
-        withLocalDecl id.getId (kind := kind) .default type elabZetaCore
-    else
-      if !config.nondep then
-        withLetDecl id.getId (kind := kind) type val fun x => do
-          addLocalVarInfo id x
-          if let some h := config.eq? then
-            let hTy ← mkEq x val
-            withLocalDeclD h.getId hTy fun h' => do
-              addLocalVarInfo h h'
-              let body ← elabBody
-              let body := (← body.abstractM #[h']).instantiate1 (← mkEqRefl x)
-              mkLetFVars #[x] body (usedLetOnly := config.usedOnly)
+        else
+          mkLetFVars #[x] body (usedLetOnly := config.usedOnly) (generalizeNondepLet := false)
+      | some h =>
+        let hTy ← mkEq x val
+        withLetDecl h.getId hTy (← mkEqRefl x) (nondep := true) fun h' => do
+          addLocalVarInfo h h'
+          let body ← elabBody
+          if config.zeta then
+            pure <| (← body.abstractM #[x, h']).instantiateRev #[val, ← mkEqRefl val]
+          else if config.nondep then
+            -- TODO(kmill): Think more about how to encode this case.
+            -- Currently we produce `(fun (x : α) (h : x = val) => b) val rfl`.
+            -- N.B. the nondep lets become lambdas here.
+            let f ← mkLambdaFVars #[x, h'] body
+            return mkApp2 f val (← mkEqRefl val)
           else
-            let body ← elabBody
-            mkLetFVars #[x] body (usedLetOnly := config.usedOnly)
-      else
-        withLocalDecl id.getId (kind := kind) .default type fun x => do
-          addLocalVarInfo id x
-          if let some h := config.eq? then
-            -- TODO(kmill): Think about how to encode this case.
-            let hTy ← mkEq x val
-            withLocalDeclD h.getId hTy fun h' => do
-              addLocalVarInfo h h'
-              let body ← elabBody
-              let f ← mkLambdaFVars #[x, h'] body
-              return mkApp2 f val (← mkEqRefl val)
-          else
-            let body ← elabBody
-            mkLetFun x val body
+            mkLetFVars #[x, h'] body (usedLetOnly := config.usedOnly) (generalizeNondepLet := false)
   if config.postponeValue then
     forallBoundedTelescope type binders.size fun xs type => do
       -- the original `fvars` from above are gone, so add back info manually
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index e54b9b0202..ef7057ebc8 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -670,7 +670,7 @@ where
     match p with
     | .forallE n d b bi  => withLocalDecl n bi (← go d) fun x => do mkForallFVars #[x] (← go (b.instantiate1 x))
     | .lam n d b bi      => withLocalDecl n bi (← go d) fun x => do mkLambdaFVars #[x] (← go (b.instantiate1 x))
-    | .letE n t v b ..  => withLetDecl n (← go t) (← go v) fun x => do mkLetFVars #[x] (← go (b.instantiate1 x))
+    | .letE n t v b nondep => mapLetDecl n (← go t) (← go v) (nondep := nondep) fun x => go (b.instantiate1 x)
     | .app f a          => return mkApp (← go f) (← go a)
     | .proj _ _ b       => return p.updateProj! (← go b)
     | .mdata k b        =>
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 9699dfe2c9..962e3d1ef9 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -869,10 +869,11 @@ private partial def mkClosureForAux (toProcess : Array FVarId) : StateRefT Closu
     | .cdecl _ _ userName type bi k =>
       let toProcess ← pushLocalDecl toProcess fvarId userName type bi k
       mkClosureForAux toProcess
-    | .ldecl _ _ userName type val _ k =>
+    | .ldecl _ _ userName type val nondep k =>
       let zetaDeltaFVarIds ← getZetaDeltaFVarIds
-      if !zetaDeltaFVarIds.contains fvarId then
-        /- Non-dependent let-decl. See comment at src/Lean/Meta/Closure.lean -/
+      -- Note: If `nondep` is true then `zetaDeltaFVarIds.contains fvarId` must be false.
+      if nondep || !zetaDeltaFVarIds.contains fvarId then
+        /- Nondependent let-decl. See comment at src/Lean/Meta/Closure.lean -/
         let toProcess ← pushLocalDecl toProcess fvarId userName type .default k
         mkClosureForAux toProcess
       else
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 98fd2d37d2..5232e371ae 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -93,7 +93,7 @@ private partial def ensureNoUnassignedLevelMVarsAtPreDef (preDef : PreDefinition
           checkCache { val := e : ExprStructEq } fun _ => do
             match e with
             | .forallE n d b c | .lam n d b c => withExpr e do visit d; withLocalDecl n c d fun x => visit (b.instantiate1 x)
-            | .letE n t v b _ => withExpr e do visit t; visit v; withLetDecl n t v fun x => visit (b.instantiate1 x)
+            | .letE n t v b nondep => withExpr e do visit t; visit v; withLetDecl n t v (nondep := nondep) fun x => visit (b.instantiate1 x)
             | .mdata _ b     => withExpr e do visit b
             | .proj _ _ b    => withExpr e do visit b
             | .sort u        => visitLevel u (← read)
diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
index 6fbbca6c17..1ab0df3bf0 100644
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
@@ -133,9 +133,9 @@ private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions :
     | Expr.forallE n d b c =>
       withLocalDecl n c (← loop below d) fun x => do
         mkForallFVars #[x] (← loop below (b.instantiate1 x))
-    | Expr.letE n type val body _ =>
-      withLetDecl n (← loop below type) (← loop below val) fun x => do
-        mkLetFVars #[x] (← loop below (body.instantiate1 x)) (usedLetOnly := false)
+    | Expr.letE n type val body nondep =>
+      mapLetDecl n (← loop below type) (← loop below val) (nondep := nondep) (usedLetOnly := false) fun x => do
+        loop below (body.instantiate1 x)
     | Expr.mdata d b =>
       if let some stx := getRecAppSyntax? e then
         withRef stx <| loop below b
diff --git a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
index 5bfa77812e..51be0e27da 100644
--- a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
@@ -50,9 +50,9 @@ private partial def replaceIndPredRecApps (recArgInfo : RecArgInfo) (funType : E
     | Expr.forallE n d b c =>
       withLocalDecl n c (← loop d) fun x => do
         mkForallFVars #[x] (← loop (b.instantiate1 x))
-    | Expr.letE n type val body _ =>
-      withLetDecl n (← loop type) (← loop val) fun x => do
-        mkLetFVars #[x] (← loop (body.instantiate1 x))
+    | Expr.letE n type val body nondep =>
+      mapLetDecl n (← loop type) (← loop val) (nondep := nondep) fun x => do
+        loop (body.instantiate1 x)
     | Expr.mdata d b => do
       if let some stx := getRecAppSyntax? e then
         withRef stx <| loop b
diff --git a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean
index ea3ef8af45..215a770b60 100644
--- a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean
@@ -32,8 +32,9 @@ where
     match e with
     | Expr.lam ..     => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b)
     | Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)
-    | Expr.letE n type val body _ =>
-      withLetDecl n type (← visit val) fun x => do mkLetFVars #[x] (← visit (body.instantiate1 x))
+    | Expr.letE n type val body nondep =>
+      mapLetDecl n type (← visit val) (nondep := nondep) fun x => do
+        visit (body.instantiate1 x)
     | Expr.mdata d b     => return mkMData d (← visit b)
     | Expr.proj n i s    => return mkProj n i (← visit s)
     | Expr.app .. =>
diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index 6f2935db77..2a4b5ee91d 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -84,9 +84,9 @@ where
     | Expr.forallE n d b c =>
       withLocalDecl n c (← loop F d) fun x => do
         mkForallFVars #[x] (← loop F (b.instantiate1 x))
-    | Expr.letE n type val body _ =>
-      withLetDecl n (← loop F type) (← loop F val) fun x => do
-        mkLetFVars #[x] (← loop F (body.instantiate1 x)) (usedLetOnly := false)
+    | Expr.letE n type val body nondep =>
+      mapLetDecl n (← loop F type) (← loop F val) (nondep := nondep) (usedLetOnly := false) fun x => do
+        loop F (body.instantiate1 x)
     | Expr.mdata d b =>
       if let some stx := getRecAppSyntax? e then
         withRef stx <| loop F b
diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
index 5bcffd6ec1..72dfc110a9 100644
--- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
+++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -241,10 +241,10 @@ where
       loop param d
       withLocalDecl n c d fun x => do
         loop param (b.instantiate1 x)
-    | Expr.letE n type val body _ =>
+    | Expr.letE n type val body nondep =>
       loop param type
       loop param val
-      withLetDecl n type val fun x => do
+      withLetDecl n type val (nondep := nondep) fun x => do
         loop param (body.instantiate1 x)
     | Expr.mdata _d b =>
       if let some stx := getRecAppSyntax? e then
diff --git a/src/Lean/Elab/PreDefinition/WF/Preprocess.lean b/src/Lean/Elab/PreDefinition/WF/Preprocess.lean
index 24cb031b13..f5c8777d40 100644
--- a/src/Lean/Elab/PreDefinition/WF/Preprocess.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Preprocess.lean
@@ -110,14 +110,68 @@ builtin_dsimproc paramMatcher (_) := fun e => do
   let matcherApp' := { matcherApp with discrs := discrs', alts := alts' }
   return .continue <| matcherApp'.toExpr
 
-/-- `let x := (wfParam e); body[x] ==> let x := e; body[wfParam y] -/
+private def anyLetValueIsWfParam (e : Expr) : Bool :=
+  match e with
+  | .letE _ _ v b _ => (isWfParam? v).isSome || anyLetValueIsWfParam b
+  | _               => false
+
+private def numLetsWithValueNotIsWfParam (e : Expr) (acc := 0) : Nat :=
+  match e with
+  | .letE _ _ v b _ => if (isWfParam? v).isSome then acc else numLetsWithValueNotIsWfParam b (acc + 1)
+  | _               => acc
+
+private partial def processParamLet (e : Expr) : MetaM Expr := do
+  if let .letE _ t v b _ := e then
+    if let some v' := isWfParam? v then
+      if ← Meta.isProp t then
+        processParamLet <| e.updateLetE! t v' b
+      else
+        let u ← getLevel t
+        let b' := b.instantiate1 <| mkApp2 (.const ``wfParam [u]) t (.bvar 0)
+        processParamLet <| e.updateLetE! t v' b'
+    else
+      let num := numLetsWithValueNotIsWfParam e
+      assert! num > 0
+      letBoundedTelescope e num fun xs b => do
+        let b' ← processParamLet b
+        mkLetFVars (usedLetOnly := false) (generalizeNondepLet := false) xs b'
+  else
+    return e
+
+/--
+`let x : T := (wfParam e); body[x] ==> let x : T := e; body[wfParam y]` if `T` is not a proposition,
+otherwise `... ==> let x : T := e; body[x]`. (Applies to `have`s too.)
+
+Note: simprocs are provided the head of a let telescope, but not intermediate lets.
+-/
 builtin_dsimproc paramLet (_) := fun e => do
-  unless e.isLet do return .continue
-  let some v := isWfParam? e.letValue! | return .continue
-  let u ← getLevel e.letType!
-  let body' := e.letBody!.instantiate1 <|
-    mkApp2 (.const ``wfParam [u]) e.letType! (.bvar 0)
-  return .continue <| e.updateLetE! e.letType! v body'
+  unless e.isLet || anyLetValueIsWfParam e do return .continue
+  return .continue (← processParamLet e)
+
+/--
+Transforms non-Prop `have`s to `let`s, so that the values can be used in GuessLex and decreasing-by proofs.
+These `have`s may have been introdued by `simp`, which converts `let`s to `have`s.
+-/
+private def nonPropHaveToLet (e : Expr) : MetaM Expr := do
+  Meta.transform e (pre := fun e => do
+    if (← Meta.isProof e) then
+      return .done e
+    else if e.isLet then
+      -- Recall that `Meta.transform` processes entire let telescopes,
+      -- so we need to handle the telescope all at once.
+      let lctx ← getLCtx
+      let e' ← letTelescope e fun xs b => do
+        let lctx' ← xs.foldlM (init := lctx) fun lctx' x => do
+          let decl ← x.fvarId!.getDecl
+          -- Clear the flag if it's not a prop.
+          let decl' := decl.setNondep <| ← pure decl.isNondep <&&> Meta.isProp decl.type
+          pure <| lctx'.addDecl decl'
+        withLCtx' lctx' do
+          mkLetFVars (usedLetOnly := false) (generalizeNondepLet := false) xs b
+      return .continue e'
+    else
+      return .continue
+  )
 
 def preprocess (e : Expr) : MetaM Simp.Result := do
   unless wf.preprocess.get (← getOptions) do
@@ -141,9 +195,13 @@ def preprocess (e : Expr) : MetaM Simp.Result := do
           if h : as.size ≥ 2 then
             return .continue (mkAppN as[1] as[2:])
         return .continue
+
+    -- Transform `have`s to `let`s for non-propositions.
+    let e'' ← nonPropHaveToLet e''
+
     let result := { result with expr := e'' }
 
-    trace[Elab.definition.wf] "Attach-introduction:{indentExpr e'}\nto{indentExpr result.expr}\ncleaned up as{indentExpr e''}"
+    trace[Elab.definition.wf] "Attach-introduction:{indentExpr e'}\nto{indentExpr result.expr}"
     result.addLambdas xs
 
 end Lean.Elab.WF
diff --git a/src/Lean/Elab/Tactic/Monotonicity.lean b/src/Lean/Elab/Tactic/Monotonicity.lean
index 3ecd913272..2a5d5928c4 100644
--- a/src/Lean/Elab/Tactic/Monotonicity.lean
+++ b/src/Lean/Elab/Tactic/Monotonicity.lean
@@ -134,7 +134,7 @@ def solveMonoStep (failK : ∀ {α}, Expr → Array Name → MetaM α := @defaul
       return [goal'.mvarId!]
 
     -- Handle let
-    if let .letE n t v b _nonDep := e then
+    if let .letE n t v b nondep := e then
       if t.hasLooseBVars || v.hasLooseBVars then
         -- We cannot float the let to the context, so just zeta-reduce.
         let b' := f.updateLambdaE! f.bindingDomain! (b.instantiate1 v)
@@ -143,10 +143,10 @@ def solveMonoStep (failK : ∀ {α}, Expr → Array Name → MetaM α := @defaul
         return [goal'.mvarId!]
       else
         -- No recursive call in t or v, so float out
-        let goal' ← withLetDecl n t v fun x => do
+        let goal' ← withLetDecl n t v (nondep := nondep) fun x => do
           let b' := f.updateLambdaE! f.bindingDomain! (b.instantiate1 x)
           let goal' ← mkFreshExprSyntheticOpaqueMVar (mkApp type.appFn! b')
-          goal.assign (← mkLetFVars #[x] goal')
+          goal.assign (← mkLetFVars (generalizeNondepLet := false) #[x] goal')
           pure goal'
         return [goal'.mvarId!]
 
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index a47d50ea82..2173118152 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -48,10 +48,36 @@ See `LocalDecl.index`, `LocalDecl.fvarId`, `LocalDecl.userName`, `LocalDecl.type
 arguments common to both constructors.
 -/
 inductive LocalDecl where
-  /-- A local variable. -/
+  /-- A local variable without any value.
+  `Lean.LocalContext.mkBinding` creates lambdas or foralls from `cdecl`s. -/
   | cdecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) (kind : LocalDeclKind)
-  /-- A let-bound free variable, with a `value : Expr`. -/
-  | ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep : Bool) (kind : LocalDeclKind)
+  /-- A let-bound free variable, with a value `value : Expr`.
+  If `nondep := false`, then the variable is definitionally equal to its value.
+  If `nondep := true`, then the variable has an opaque value; we call these "have-bound free variables."
+  `Lean.LocalContext.mkBinding` creates let/have expressions from `ldecl`s.
+
+  **Important:** The `nondep := true` case is subtle; it is not merely an opaque `ldecl`!
+  - In most contexts, nondependent `ldecl`s should be treated like `cdecl`s.
+    For example, suppose we have a tactic goal `x : α := v (nondep) ⊢ b`.
+    It would be incorrect for `revert x` to produce the goal `⊢ have x : α := v; b`,
+    since this would be saying "to prove `b` without knowledge of the value of `x`, it suffices to
+    prove `have x : α := v; b` for this particular value of `x`."
+    Instead, `revert x` *must* produce the goal `⊢ ∀ x : α, b`.
+    Furthermore, given a goal `⊢ have x : α := v; b`, the `intro x` tactic should yield a *dependent* `ldecl`,
+    since users expect to be able to make use of the value of `x`,
+    plus, as discussed, if `intro` yielded a nondep `ldecl` then `intro x; revert x` would convert the goal into a forall, not a `have`.
+  - Also: `value` might not be type correct. Metaprograms may decide to pretend that all `nondep := true`
+    `ldecl`s are `cdecl`s (for example, when reverting variables). As a consequence, nondep `ldecl`s may
+    have type-incorrect values. This design decision allows metaprograms to not have to think about nondep `ldecl`s,
+    so long as `LocalDecl` values are consumed through `LocalDecl.isLet` and `LocalDecl.value?` with `(allowNondep := false)`.
+    **Rule:** never use `(generalizeNondepLet := false)` in `mkBinding`-family functions within a local context you do not own.
+    See `LocalDecl.setNondep` for some additional discussion.
+  - Where then do nondep ldecls come from? Common functions are `Meta.mapLetDecl`, `Meta.withLetDecl`, and `Meta.letTelescope`.
+    The `have` term syntax makes use of a nondep ldecl as well.
+
+  Therefore, `nondep := true` should be used with consideration.
+  Its primary use is in metaprograms that enter `let`/`have` telescopes and wish to reconstruct them. -/
+  | ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nondep : Bool) (kind : LocalDeclKind)
   deriving Inhabited
 
 @[export lean_mk_local_decl]
@@ -66,9 +92,15 @@ def LocalDecl.binderInfoEx : LocalDecl → BinderInfo
   | _                   => BinderInfo.default
 namespace LocalDecl
 
-def isLet : LocalDecl → Bool
-  | cdecl .. => false
-  | ldecl .. => true
+/--
+Returns true if this is an `ldecl` with a visible value.
+
+If `allowNondep` is true then includes `ldecl`s with `nondep := true`, whose values are normally hidden.
+-/
+def isLet : LocalDecl → (allowNondep : Bool := false) → Bool
+  | cdecl .., _ => false
+  | ldecl (nondep := false) .., _ => true
+  | ldecl (nondep := true) .., allowNondep => allowNondep
 
 /-- The position of the decl in the local context. -/
 def index : LocalDecl → Nat
@@ -115,22 +147,81 @@ Is the local declaration an implementation-detail hypothesis
 def isImplementationDetail (d : LocalDecl) : Bool :=
   d.kind != .default
 
-def value? : LocalDecl → Option Expr
-  | cdecl ..              => none
-  | ldecl (value := v) .. => some v
+/--
+Returns the value of the `ldecl` if it has a visible value.
 
-def value : LocalDecl → Expr
-  | cdecl ..              => panic! "let declaration expected"
-  | ldecl (value := v) .. => v
+If `allowNondep` is true, then allows nondependent `ldecl`s, whose values are normally hidden.
+-/
+def value? : LocalDecl → (allowNondep : Bool := false) → Option Expr
+  | ldecl (nondep := false) (value := v) .., _    => some v
+  | ldecl (nondep := true)  (value := v) .., true => some v
+  | _,                                       _    => none
 
-def hasValue : LocalDecl → Bool
-  | cdecl .. => false
-  | ldecl .. => true
+/--
+Returns the value of the `ldecl` if it has a visible value.
 
+If `allowNondep` is true, then allows nondependent `ldecl`s, whose values are normally hidden.
+-/
+def value : LocalDecl → (allowNondep : Bool := false) → Expr
+  | cdecl ..,                                _     => panic! "let declaration expected"
+  | ldecl (nondep := false) (value := v) .., _     => v
+  | ldecl (nondep := true)  (value := v) .., true  => v
+  | ldecl (nondep := true) ..,               false => panic! "dependent let declaration expected"
+
+/--
+Returns `true` if `LocalDecl.value?` is not `none`.
+-/
+def hasValue : LocalDecl → (allowNondep : Bool := false) → Bool
+  | cdecl ..,                    _           => false
+  | ldecl (nondep := nondep) .., allowNondep => !nondep || allowNondep
+
+/-- Sets the value of an `ldecl`, otherwise returns `cdecl`s unchanged. -/
 def setValue : LocalDecl → Expr → LocalDecl
   | ldecl idx id n t _ nd k, v => ldecl idx id n t v nd k
   | d, _                       => d
 
+/--
+Sets the `nondep` flag of an `ldecl`, otherwise returns `cdecl`s unchanged.
+
+This is a low-level function, and it is the responsibility of the caller to ensure that
+transitions of `nondep` are valid.
+
+Rules:
+- If the declaration is not under the caller's control, then setting `nondep := false` must not be done.
+  General nondependent `ldecl`s should be treated like `cdecl`s.
+  See also the docstring for `LocalDecl.ldecl` about the `value` not necessarily being type correct.
+- Setting `nondep := true` is usually fine.
+  - Caution: be sure any relevant caches are cleared so that the value associated to this `FVarId` does not leak.
+  - Caution: be sure that metavariables dependent on this declaration created before and after the transition are not mixed,
+    since unification does not check "`nondep`-compatibility" of local contexts when assigning metavariables.
+
+For example, setting `nondep := false` is fine from within a telescope combinator, to update the local context
+right before calling `mkLetFVars`:
+```lean
+let lctx ← getLCtx
+letTelescope e fun xs b => do
+  let lctx' ← xs.foldlM (init := lctx) fun lctx' x => do
+    let decl ← x.fvarId!.getDecl
+    -- Clear the flag if it's not a prop.
+    let decl' := decl.setNondep <| ← pure decl.isNondep <&&> Meta.isProp decl.type
+    pure <| lctx'.addDecl decl'
+  withLCtx' lctx' do
+    mkLetFVars (usedLetOnly := false) (generalizeNondepLet := false) xs b
+```
+1. The declarations for `xs` are in the control of this metaprogram.
+2. `mkLetFVars` does make use of `MetaM` caches.
+3. Even if `e` has metavariables, these do not include `xs` in their contexts,
+   so the change of the `nondep` flag does not cause any issues in the `abstractM` system used by `mkLetFVars`.
+-/
+def setNondep : LocalDecl → Bool → LocalDecl
+  | ldecl idx id n t v _ k, nd => ldecl idx id n t v nd k
+  | d, _                       => d
+
+/-- Returns `true` if this is an `ldecl` with `nondep := true`. -/
+def isNondep : LocalDecl → Bool
+  | ldecl (nondep := nondep) .. => nondep
+  | _                           => false
+
 def setUserName : LocalDecl → Name → LocalDecl
   | cdecl index id _ type bi k,     userName => cdecl index id userName type bi k
   | ldecl index id _ type val nd k, userName => ldecl index id userName type val nd k
@@ -152,8 +243,8 @@ Set the kind of a `LocalDecl`.
 def setKind : LocalDecl → LocalDeclKind → LocalDecl
   | cdecl index fvarId userName type bi _, kind =>
       cdecl index fvarId userName type bi kind
-  | ldecl index fvarId userName type value nonDep _, kind =>
-      ldecl index fvarId userName type value nonDep kind
+  | ldecl index fvarId userName type value nondep _, kind =>
+      ldecl index fvarId userName type value nondep kind
 
 end LocalDecl
 
@@ -182,7 +273,7 @@ def empty : LocalContext := {}
 def isEmpty (lctx : LocalContext) : Bool :=
   lctx.fvarIdToDecl.isEmpty
 
-/-- Low level API for creating local declarations.
+/-- Low level API for creating local declarations (`LocalDecl.cdecl`).
 It is used to implement actions in the monads `Elab` and `Tactic`.
 It should not be used directly since the argument `(fvarId : FVarId)` is
 assumed to be unique. You can create a unique fvarId with `mkFreshFVarId`. -/
@@ -199,16 +290,16 @@ private def mkLocalDeclExported (lctx : LocalContext) (fvarId : FVarId) (userNam
   mkLocalDecl lctx fvarId userName type bi
 
 /-- Low level API for let declarations. Do not use directly.-/
-def mkLetDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep := false) (kind : LocalDeclKind := default) : LocalContext :=
+def mkLetDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nondep := false) (kind : LocalDeclKind := default) : LocalContext :=
   match lctx with
   | { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
     let idx  := decls.size
-    let decl := LocalDecl.ldecl idx fvarId userName type value nonDep kind
+    let decl := LocalDecl.ldecl idx fvarId userName type value nondep kind
     { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl, auxDeclToFullName }
 
 @[export lean_local_ctx_mk_let_decl]
-private def mkLetDeclExported (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep : Bool) : LocalContext :=
-  mkLetDecl lctx fvarId userName type value nonDep
+private def mkLetDeclExported (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nondep : Bool) : LocalContext :=
+  mkLetDecl lctx fvarId userName type value nondep
 
 /-- Low level API for auxiliary declarations. Do not use directly. -/
 def mkAuxDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (fullName : Name) : LocalContext :=
@@ -431,35 +522,39 @@ partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) (exceptFVar
 def isSubPrefixOf (lctx₁ lctx₂ : LocalContext) (exceptFVars : Array Expr := #[]) : Bool :=
   isSubPrefixOfAux lctx₁.decls lctx₂.decls exceptFVars 0 0
 
-@[inline] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
+@[inline] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (b : Expr) (generalizeNondepLet := false) : Expr :=
   let b := b.abstract xs
   xs.size.foldRev (init := b) fun i _ b =>
     let x := xs[i]
-    match lctx.findFVar? x with
-    | some (.cdecl _ _ n ty bi _)  =>
+    let handleCDecl (n : Name) (ty : Expr) (bi : BinderInfo) : Expr :=
       let ty := ty.abstractRange i xs;
       if isLambda then
         Lean.mkLambda n bi ty b
       else
         Lean.mkForall n bi ty b
-    | some (.ldecl _ _ n ty val nonDep _) =>
-      if b.hasLooseBVar 0 then
+    match lctx.findFVar? x with
+    | some (.cdecl _ _ n ty bi _)  =>
+      handleCDecl n ty bi
+    | some (.ldecl _ _ n ty val nondep _) =>
+      if nondep && generalizeNondepLet then
+        handleCDecl n ty .default
+      else if b.hasLooseBVar 0 then
         let ty  := ty.abstractRange i xs
         let val := val.abstractRange i xs
-        mkLet n ty val b nonDep
+        mkLet n ty val b nondep
       else
         b.lowerLooseBVars 1 1
     | none => panic! "unknown free variable"
 
 /-- Creates the expression `fun x₁ .. xₙ => b` for free variables `xs = #[x₁, .., xₙ]`,
 suitably abstracting `b` and the types for each of the `xᵢ`. -/
-def mkLambda (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
-  mkBinding true lctx xs b
+def mkLambda (lctx : LocalContext) (xs : Array Expr) (b : Expr) (generalizeNondepLet := false) : Expr :=
+  mkBinding true lctx xs b generalizeNondepLet
 
 /-- Creates the expression `(x₁:α₁) → .. → (xₙ:αₙ) → b` for free variables `xs = #[x₁, .., xₙ]`,
 suitably abstracting `b` and the types for each of the `xᵢ`, `αᵢ`. -/
-def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
-  mkBinding false lctx xs b
+def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) (generalizeNondepLet := false) : Expr :=
+  mkBinding false lctx xs b generalizeNondepLet
 
 @[inline] def anyM [Monad m] (lctx : LocalContext) (p : LocalDecl → m Bool) : m Bool :=
   lctx.decls.anyM fun d => match d with
@@ -539,7 +634,7 @@ def LocalDecl.replaceFVarId (fvarId : FVarId) (e : Expr) (d : LocalDecl) : Local
   if d.fvarId == fvarId then d
   else match d with
     | .cdecl idx id n type bi k => .cdecl idx id n (type.replaceFVarId fvarId e) bi k
-    | .ldecl idx id n type val nonDep k => .ldecl idx id n (type.replaceFVarId fvarId e) (val.replaceFVarId fvarId e) nonDep k
+    | .ldecl idx id n type val nondep k => .ldecl idx id n (type.replaceFVarId fvarId e) (val.replaceFVarId fvarId e) nondep k
 
 def LocalContext.replaceFVarId (fvarId : FVarId) (e : Expr) (lctx : LocalContext) : LocalContext :=
   let lctx := lctx.erase fvarId
diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean
index 4ab81ff747..ea0d756ac2 100644
--- a/src/Lean/Meta/AbstractNestedProofs.lean
+++ b/src/Lean/Meta/AbstractNestedProofs.lean
@@ -60,7 +60,7 @@ partial def visit (e : Expr) : M Expr := do
         let localDecl ← xFVarId.getDecl
         let type      ← visit localDecl.type
         let localDecl := localDecl.setType type
-        let localDecl ← match localDecl.value? with
+        let localDecl ← match localDecl.value? (allowNondep := true) with
            | some value => let value ← visit value; pure <| localDecl.setValue value
            | none       => pure localDecl
         lctx := lctx.modifyLocalDecl xFVarId fun _ => localDecl
@@ -70,8 +70,8 @@ partial def visit (e : Expr) : M Expr := do
         /- Ensure proofs nested in type are also abstracted -/
         abstractProof e (← read).cache visit
       else match e with
-        | .lam ..      => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) (usedLetOnly := false)
-        | .letE ..     => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) (usedLetOnly := false)
+        | .lam ..
+        | .letE ..     => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) (usedLetOnly := false) (generalizeNondepLet := false)
         | .forallE ..  => forallTelescope e fun xs b => visitBinders xs do mkForallFVars xs (← visit b)
         | .mdata _ b   => return e.updateMData! (← visit b)
         | .proj _ _ b  => return e.updateProj! (← visit b)
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index a1403290a3..04a60a8242 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -445,8 +445,8 @@ structure Context where
   When `trackZetaDelta = true`, we track all free variables that have been zetaDelta-expanded.
   That is, suppose the local context contains
   the declaration `x : t := v`, and we reduce `x` to `v`, then we insert `x` into `State.zetaDeltaFVarIds`.
-  We use `trackZetaDelta` to discover which let-declarations `let x := v; e` can be represented as `(fun x => e) v`.
-  When we find these declarations we set their `nonDep` flag with `true`.
+  We use `trackZetaDelta` to discover which let-declarations `let x := v; e` can be represented as `have x := v; e`.
+  When we find these declarations we set their `nondep` flag with `true`.
   To find these let-declarations in a given term `s`, we
   1- Reset `State.zetaDeltaFVarIds`
   2- Set `trackZetaDelta := true`
@@ -978,17 +978,27 @@ def _root_.Lean.FVarId.getType (fvarId : FVarId) : MetaM Expr :=
 def _root_.Lean.FVarId.getBinderInfo (fvarId : FVarId) : MetaM BinderInfo :=
   return (← fvarId.getDecl).binderInfo
 
-/-- Return `some value` if the given free variable is a let-declaration, and `none` otherwise. -/
-def _root_.Lean.FVarId.getValue? (fvarId : FVarId) : MetaM (Option Expr) :=
-  return (← fvarId.getDecl).value?
+/--
+Returns `some value` if the given free let-variable has a visible local definition in the current local context
+(using `Lean.LocalDecl.value?`), and `none` otherwise.
+
+Setting `allowNondep := true` allows access of the normally hidden value of a nondependent let declaration.
+-/
+def _root_.Lean.FVarId.getValue? (fvarId : FVarId) (allowNondep : Bool := false) : MetaM (Option Expr) :=
+  return (← fvarId.getDecl).value? allowNondep
 
 /-- Return the user-facing name for the given free variable. -/
 def _root_.Lean.FVarId.getUserName (fvarId : FVarId) : MetaM Name :=
   return (← fvarId.getDecl).userName
 
-/-- Return `true` is the free variable is a let-variable. -/
-def _root_.Lean.FVarId.isLetVar (fvarId : FVarId) : MetaM Bool :=
-  return (← fvarId.getDecl).isLet
+/--
+Returns `true` if the free variable is a let-variable with a visible local definition in the current local context
+(using `Lean.LocalDecl.isLet`).
+
+Setting `allowNondep := true` includes nondependent let declarations, whose values are normally hidden.
+-/
+def _root_.Lean.FVarId.isLetVar (fvarId : FVarId) (allowNondep : Bool := false) : MetaM Bool :=
+  return (← fvarId.getDecl).isLet allowNondep
 
 /-- Get the local declaration associated to the given `Expr` in the current local
 context. Fails if the given expression is not a fvar or if no such declaration exists. -/
@@ -1054,26 +1064,30 @@ def _root_.Lean.Expr.abstractM (e : Expr) (xs : Array Expr) : MetaM Expr :=
 /--
 Collect forward dependencies for the free variables in `toRevert`.
 Recall that when reverting free variables `xs`, we must also revert their forward dependencies.
+
+When `generalizeNondepLet := true` (the default), then the values of nondependent lets are not considered
+when computing forward dependencies.
 -/
-def collectForwardDeps (toRevert : Array Expr) (preserveOrder : Bool) : MetaM (Array Expr) := do
-  liftMkBindingM <| MetavarContext.collectForwardDeps toRevert preserveOrder
+def collectForwardDeps (toRevert : Array Expr) (preserveOrder : Bool) (generalizeNondepLet := true) : MetaM (Array Expr) := do
+  liftMkBindingM <| MetavarContext.collectForwardDeps toRevert preserveOrder generalizeNondepLet
 
 /-- Takes an array `xs` of free variables or metavariables and a term `e` that may contain those variables, and abstracts and binds them as universal quantifiers.
 
 - if `usedOnly = true` then only variables that the expression body depends on will appear.
 - if `usedLetOnly = true` same as `usedOnly` except for let-bound variables. (That is, local constants which have been assigned a value.)
+- if `generalizeNondepLet = true` then nondependent `ldecl`s become foralls too.
  -/
-def mkForallFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr :=
-  if xs.isEmpty then return e else liftMkBindingM <| MetavarContext.mkForall xs e usedOnly usedLetOnly binderInfoForMVars
+def mkForallFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (generalizeNondepLet := true) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr :=
+  if xs.isEmpty then return e else liftMkBindingM <| MetavarContext.mkForall xs e usedOnly usedLetOnly generalizeNondepLet binderInfoForMVars
 
 /-- Takes an array `xs` of free variables and metavariables and a
 body term `e` and creates `fun ..xs => e`, suitably
 abstracting `e` and the types in `xs`. -/
-def mkLambdaFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce : Bool := false) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr :=
-  if xs.isEmpty then return e else liftMkBindingM <| MetavarContext.mkLambda xs e usedOnly usedLetOnly etaReduce binderInfoForMVars
+def mkLambdaFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce : Bool := false) (generalizeNondepLet := true) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr :=
+  if xs.isEmpty then return e else liftMkBindingM <| MetavarContext.mkLambda xs e usedOnly usedLetOnly etaReduce generalizeNondepLet binderInfoForMVars
 
-def mkLetFVars (xs : Array Expr) (e : Expr) (usedLetOnly := true) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr :=
-  mkLambdaFVars xs e (usedLetOnly := usedLetOnly) (binderInfoForMVars := binderInfoForMVars)
+def mkLetFVars (xs : Array Expr) (e : Expr) (usedLetOnly := true) (generalizeNondepLet := true) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr :=
+  mkLambdaFVars xs e (usedLetOnly := usedLetOnly) (generalizeNondepLet := generalizeNondepLet) (binderInfoForMVars := binderInfoForMVars)
 
 /-- `fun _ : Unit => a` -/
 def mkFunUnit (a : Expr) : MetaM Expr :=
@@ -1519,40 +1533,48 @@ private def forallBoundedTelescopeImp (type : Expr) (maxFVars? : Option Nat) (k
 def forallBoundedTelescope (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) (whnfType := false) : n α :=
   map2MetaM (fun k => forallBoundedTelescopeImp type maxFVars? k cleanupAnnotations (whnfType := whnfType)) k
 
-private partial def lambdaTelescopeImp (e : Expr) (consumeLet : Bool) (maxFVars? : Option Nat)
+private partial def lambdaTelescopeImp (e : Expr) (consumeLambda : Bool) (consumeLet : Bool) (preserveNondepLet : Bool) (nondepLetOnly : Bool) (maxFVars? : Option Nat)
     (k : Array Expr → Expr → MetaM α) (cleanupAnnotations := false) : MetaM α := do
-  process consumeLet (← getLCtx) #[] e
+  process consumeLambda consumeLet (← getLCtx) #[] e
 where
-  process (consumeLet : Bool) (lctx : LocalContext) (fvars : Array Expr) (e : Expr) : MetaM α := do
-    match fvarsSizeLtMaxFVars fvars maxFVars?, consumeLet, e with
-    | true, _, .lam n d b bi =>
+  process (consumeLambda : Bool) (consumeLet : Bool) (lctx : LocalContext) (fvars : Array Expr) (e : Expr) : MetaM α := do
+    let finish (e : Expr) : MetaM α :=
+      let e := e.instantiateRevRange 0 fvars.size fvars
+      withReader (fun ctx => { ctx with lctx := lctx }) do
+        withNewLocalInstancesImp fvars 0 do
+          k fvars e
+    match fvarsSizeLtMaxFVars fvars maxFVars?, consumeLambda, consumeLet, e with
+    | true, true, _, .lam n d b bi =>
       let d := d.instantiateRevRange 0 fvars.size fvars
       let d := if cleanupAnnotations then d.cleanupAnnotations else d
       let fvarId ← mkFreshFVarId
       let lctx := lctx.mkLocalDecl fvarId n d bi
       let fvar := mkFVar fvarId
-      process consumeLet lctx (fvars.push fvar) b
-    | true, true, .letE n t v b _ => do
-      let t := t.instantiateRevRange 0 fvars.size fvars
-      let t := if cleanupAnnotations then t.cleanupAnnotations else t
-      let v := v.instantiateRevRange 0 fvars.size fvars
-      let fvarId ← mkFreshFVarId
-      let lctx := lctx.mkLetDecl fvarId n t v
-      let fvar := mkFVar fvarId
-      process true lctx (fvars.push fvar) b
-    | _, _, e =>
-      let e := e.instantiateRevRange 0 fvars.size fvars
-      withReader (fun ctx => { ctx with lctx := lctx }) do
-        withNewLocalInstancesImp fvars 0 do
-          k fvars e
+      process true consumeLet lctx (fvars.push fvar) b
+    | true, _, true, .letE n t v b nondep => do
+      if !nondep && nondepLetOnly then
+        finish e
+      else
+        let t := t.instantiateRevRange 0 fvars.size fvars
+        let t := if cleanupAnnotations then t.cleanupAnnotations else t
+        let v := v.instantiateRevRange 0 fvars.size fvars
+        let fvarId ← mkFreshFVarId
+        let lctx := lctx.mkLetDecl fvarId n t v (nondep && preserveNondepLet)
+        let fvar := mkFVar fvarId
+        process consumeLambda true lctx (fvars.push fvar) b
+    | _, _, _, e =>
+      finish e
 
 /--
 Similar to `lambdaTelescope` but for lambda and let expressions.
 
-If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
+- If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
+- If `preserveNondep` is `false`, all `have`s are converted to `let`s.
+
+See also `mapLambdaLetTelescope` for entering and rebuilding the telescope.
 -/
-def lambdaLetTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α :=
-  map2MetaM (fun k => lambdaTelescopeImp e true .none k (cleanupAnnotations := cleanupAnnotations)) k
+def lambdaLetTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) (preserveNondepLet := true) : n α :=
+  map2MetaM (fun k => lambdaTelescopeImp e true true preserveNondepLet false .none k (cleanupAnnotations := cleanupAnnotations)) k
 
 /--
   Given `e` of the form `fun ..xs => A`, execute `k xs A`.
@@ -1562,7 +1584,7 @@ def lambdaLetTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnn
   If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
 -/
 def lambdaTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α :=
-  map2MetaM (fun k => lambdaTelescopeImp e false none k (cleanupAnnotations := cleanupAnnotations)) k
+  map2MetaM (fun k => lambdaTelescopeImp e true false true false none k (cleanupAnnotations := cleanupAnnotations)) k
 
 /--
   Given `e` of the form `fun ..xs ..ys => A`, execute `k xs (fun ..ys => A)` where
@@ -1573,7 +1595,42 @@ def lambdaTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnota
   If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
 -/
 def lambdaBoundedTelescope (e : Expr) (maxFVars : Nat) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α :=
-  map2MetaM (fun k => lambdaTelescopeImp e false (.some maxFVars) k (cleanupAnnotations := cleanupAnnotations)) k
+  map2MetaM (fun k => lambdaTelescopeImp e true false true false (.some maxFVars) k (cleanupAnnotations := cleanupAnnotations)) k
+
+/--
+Given `e` of the form `let x₁ := v₁; ...; let xₙ := vₙ; A`, executes `k xs A`,
+where `xs` is an array of free variables for the binders.
+The `let`s can also be `have`s.
+
+- If `cleanupAnnotations` is `true`, applies `Expr.cleanupAnnotations` to each type in the telescope.
+- If `preserveNondep` is `false`, all `have`s are converted to `let`s.
+- If `nondepLetOnly` is `true`, then only `have`s are consumed (it stops at the first dependent `let`).
+
+See also `mapLetTelescope` for entering and rebuilding the telescope.
+-/
+def letTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) (preserveNondepLet := true) (nondepLetOnly := false) : n α :=
+  map2MetaM (fun k => lambdaTelescopeImp e false true preserveNondepLet nondepLetOnly none k (cleanupAnnotations := cleanupAnnotations)) k
+
+/--
+Like `letTelescope`, but limits the number of `let`/`have`s consumed to `maxFVars?`.
+If `maxFVars?` is none, then this is the same as `letTelescope`.
+-/
+def letBoundedTelescope (e : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) (preserveNondepLet := true) (nondepLetOnly := false) : n α :=
+  map2MetaM (fun k => lambdaTelescopeImp e false true preserveNondepLet nondepLetOnly maxFVars? k (cleanupAnnotations := cleanupAnnotations)) k
+
+/--
+Evaluates `k` from within a `lambdaLetTelescope`, then uses `mkLetFVars` to rebuild the telescope.
+-/
+def mapLambdaLetTelescope [MonadLiftT MetaM n] (e : Expr) (k : Array Expr → Expr → n Expr) (cleanupAnnotations := false) (preserveNondepLet := true) (usedLetOnly := true) : n Expr :=
+  lambdaLetTelescope e (cleanupAnnotations := cleanupAnnotations) (preserveNondepLet := preserveNondepLet) fun xs b => do
+    mkLambdaFVars (usedLetOnly := usedLetOnly) (generalizeNondepLet := false) xs (← k xs b)
+
+/--
+Evaluates `k` from within a `letTelescope`, then uses `mkLetFVars` to rebuild the telescope.
+-/
+def mapLetTelescope [MonadLiftT MetaM n] (e : Expr) (k : Array Expr → Expr → n Expr) (cleanupAnnotations := false) (preserveNondepLet := true) (nondepLetOnly := false) (usedLetOnly := true) : n Expr :=
+  letTelescope e (cleanupAnnotations := cleanupAnnotations) (preserveNondepLet := preserveNondepLet) (nondepLetOnly := nondepLetOnly) fun xs b => do
+    mkLetFVars (usedLetOnly := usedLetOnly) (generalizeNondepLet := false) xs (← k xs b)
 
 /-- Return the parameter names for the given global declaration. -/
 def getParamNames (declName : Name) : MetaM (Array Name) := do
@@ -1754,10 +1811,10 @@ def withInstImplicitAsImplict (xs : Array Expr) (k : MetaM α) : MetaM α := do
       return none
   withNewBinderInfos newBinderInfos k
 
-private def withLetDeclImp (n : Name) (type : Expr) (val : Expr) (k : Expr → MetaM α) (kind : LocalDeclKind) : MetaM α := do
+private def withLetDeclImp (n : Name) (type : Expr) (val : Expr) (k : Expr → MetaM α) (nondep : Bool) (kind : LocalDeclKind) : MetaM α := do
   let fvarId ← mkFreshFVarId
   let ctx ← read
-  let lctx := ctx.lctx.mkLetDecl fvarId n type val (nonDep := false) kind
+  let lctx := ctx.lctx.mkLetDecl fvarId n type val nondep kind
   let fvar := mkFVar fvarId
   withReader (fun ctx => { ctx with lctx := lctx }) do
     withNewFVar fvar type k
@@ -1766,8 +1823,17 @@ private def withLetDeclImp (n : Name) (type : Expr) (val : Expr) (k : Expr → M
   Add the local declaration `<name> : <type> := <val>` to the local context and execute `k x`, where `x` is a new
   free variable corresponding to the `let`-declaration. After executing `k x`, the local context is restored.
 -/
-def withLetDecl (name : Name) (type : Expr) (val : Expr) (k : Expr → n α) (kind : LocalDeclKind := .default) : n α :=
-  map1MetaM (fun k => withLetDeclImp name type val k kind) k
+def withLetDecl (name : Name) (type : Expr) (val : Expr) (k : Expr → n α) (nondep : Bool := false) (kind : LocalDeclKind := .default) : n α :=
+  map1MetaM (fun k => withLetDeclImp name type val k nondep kind) k
+
+/--
+Runs `k x` with the local declaration `<name> : <type> := <val>` added to the local context, where `x` is the new free variable.
+Afterwards, the result is wrapped in the given `let`/`have` expression (according to the value of `nondep`).
+- If `usedLetOnly := true` (the default) then the the `let`/`have` is not created if the variable is unused.
+-/
+def mapLetDecl [MonadLiftT MetaM n] (name : Name) (type : Expr) (val : Expr) (k : Expr → n Expr) (nondep : Bool := false) (kind : LocalDeclKind := .default) (usedLetOnly : Bool := true) : n Expr :=
+  withLetDecl name type val (nondep := nondep) (kind := kind) fun x => do
+    mkLetFVars (usedLetOnly := usedLetOnly) (generalizeNondepLet := false) #[x] (← k x)
 
 def withLocalInstancesImp (decls : List LocalDecl) (k : MetaM α) : MetaM α := do
   let mut localInsts := (← read).localInstances
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index 1ef9926127..a5c1b6937b 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -183,10 +183,11 @@ where
 def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
   let lctx ← getLCtx
   match lctx.find? fvarId with
-  | some (LocalDecl.ldecl _ _ _ t v _ _) => do
+  | some (LocalDecl.ldecl _ _ _ t v nondep _) => do
     let vType ← inferType v
     let (vType, t) ← addPPExplicitToExposeDiff vType t
-    throwError "invalid let declaration, term{indentExpr v}\nhas type{indentExpr vType}\nbut is expected to have type{indentExpr t}"
+    let declKind := if nondep then "have" else "let"
+    throwError "invalid {declKind} declaration, term{indentExpr v}\nhas type{indentExpr vType}\nbut is expected to have type{indentExpr t}"
   | _ => unreachable!
 
 /--
diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean
index 999707eb25..c9598ee06e 100644
--- a/src/Lean/Meta/Closure.lean
+++ b/src/Lean/Meta/Closure.lean
@@ -286,9 +286,10 @@ partial def process : ClosureM Unit := do
       pushLocalDecl newFVarId userName type bi
       pushFVarArg (mkFVar fvarId)
       process
-    | .ldecl _ _ userName type val _ _ =>
+    | .ldecl _ _ userName type val nondep _ =>
       let zetaDeltaFVarIds ← getZetaDeltaFVarIds
-      if !zetaDeltaFVarIds.contains fvarId then
+      -- Note: If `nondep` is true then `zetaDeltaFVarIds.contains fvarId` must be false.
+      if nondep || !zetaDeltaFVarIds.contains fvarId then
         /- Non-dependent let-decl
 
             Recall that if `fvarId` is in `zetaDeltaFVarIds`, then we zetaDelta-expanded it
@@ -321,11 +322,11 @@ partial def process : ClosureM Unit := do
         Lean.mkLambda n bi ty b
       else
         Lean.mkForall n bi ty b
-    | .ldecl _ _ n ty val nonDep _ =>
+    | .ldecl _ _ n ty val nondep _ =>
       if b.hasLooseBVar 0 then
         let ty  := ty.abstractRange i xs
         let val := val.abstractRange i xs
-        mkLet n ty val b nonDep
+        mkLet n ty val b nondep
       else
         b.lowerLooseBVars 1 1
 
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 29cc6a8f11..856edcff85 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -426,7 +426,7 @@ private partial def mkLambdaFVarsWithLetDeps (xs : Array Expr) (v : Expr) : Meta
     mkLambdaFVars ys v (etaReduce := true)
 
 where
-  /-- Return true if there are let-declarions between `xs[0]` and `xs[xs.size-1]`.
+  /-- Return true if there are let-declarations between `xs[0]` and `xs[xs.size-1]`.
      We use it a quick-check to avoid the more expensive collection procedure. -/
   hasLetDeclsInBetween : MetaM Bool := do
     let check (lctx : LocalContext) : Bool := Id.run do
@@ -728,7 +728,21 @@ mutual
     else
       let lctx := ctxMeta.lctx
       match lctx.findFVar? fvar with
-      | some (.ldecl (value := v) ..) => check v
+      /-
+      Recall: if `nondep := true`, then the ldecl is locally a cdecl, so the `value` field is not relevant.
+      In the following example, switching the indicated `have` for a `let` causes the unification to fail,
+      since then `v` depends on a variable not in `?mvar`'s local context.
+      ```
+      example : Nat → Nat :=
+        let f : Nat → Nat := ?mvar
+        let x : Nat := 2
+        -- if this is a `let`, then `refine rfl` fails.
+        have v := x
+        have : ?mvar v = v := by refine rfl
+        f
+      ```
+      -/
+      | some (.ldecl (nondep := false) (value := v) ..) => check v
       | _ =>
         if ctx.fvars.contains fvar then pure fvar
         else
@@ -917,7 +931,10 @@ unsafe def checkImpl
     | .fvar fvarId ..  =>
       if mvarDecl.lctx.contains fvarId then
         return true
-      if let some (LocalDecl.ldecl ..) := lctx.find? fvarId then
+      /-
+      Recall: if `nondep := true` then the ldecl is locally a cdecl. See comment in `CheckAssignment.checkFVar`.
+      -/
+      if let some (LocalDecl.ldecl (nondep := false) ..) := lctx.find? fvarId then
         return false -- need expensive CheckAssignment.check
       if fvars.any fun x => x.fvarId! == fvarId then
         return true
diff --git a/src/Lean/Meta/ExprLens.lean b/src/Lean/Meta/ExprLens.lean
index a9e5dd4385..1a47f09962 100644
--- a/src/Lean/Meta/ExprLens.lean
+++ b/src/Lean/Meta/ExprLens.lean
@@ -38,7 +38,7 @@ private def lensCoord (g : Expr → M Expr) (n : Nat) (e : Expr) : M Expr := do
   | 1, .forallE n y b c => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
   | 0, .letE _ y a b _  => return e.updateLetE! (← g y) a b
   | 1, .letE _ y a b _  => return e.updateLetE! y (← g a) b
-  | 2, .letE n y a b _  => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x]
+  | 2, .letE n y a b nondep => mapLetDecl n y a (nondep := nondep) (usedLetOnly := false) fun x => g <| b.instantiate1 x
   | 0, .proj _ _ b      => e.updateProj! <$> g b
   | n, .mdata _ a       => e.updateMData! <$> lensCoord g n a
   | 3, _                => throwError "Lensing on types is not supported"
diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index d1bbfed744..9e5d163587 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -121,7 +121,7 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp
       | .forallE _ d _ _ => return d.consumeTypeAnnotations
       | _                => failed ()
 
-def throwTypeExcepted {α} (type : Expr) : MetaM α :=
+def throwTypeExpected {α} (type : Expr) : MetaM α :=
   throwError "type expected{indentExpr type}"
 
 def getLevel (type : Expr) : MetaM Level := do
@@ -131,12 +131,12 @@ def getLevel (type : Expr) : MetaM Level := do
   | Expr.sort lvl     => return lvl
   | Expr.mvar mvarId  =>
     if (← mvarId.isReadOnlyOrSyntheticOpaque) then
-      throwTypeExcepted type
+      throwTypeExpected type
     else
       let lvl ← mkFreshLevelMVar
       mvarId.assign (mkSort lvl)
       return lvl
-  | _ => throwTypeExcepted type
+  | _ => throwTypeExpected type
 
 private def inferForallType (e : Expr) : MetaM Expr :=
   forallTelescope e fun xs e => do
@@ -151,7 +151,7 @@ private def inferForallType (e : Expr) : MetaM Expr :=
 private def inferLambdaType (e : Expr) : MetaM Expr :=
   lambdaLetTelescope e fun xs e => do
     let type ← inferType e
-    mkForallFVars xs type
+    mkForallFVars (generalizeNondepLet := false) xs type
 
 def throwUnknownMVar {α} (mvarId : MVarId) : MetaM α :=
   throwError "unknown metavariable '?{mvarId.name}'"
diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean
index 641bb8b523..c90ca3c881 100644
--- a/src/Lean/Meta/PPGoal.lean
+++ b/src/Lean/Meta/PPGoal.lean
@@ -102,7 +102,8 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
             return fmt ++ (Format.joinSep ids.reverse (format " ") ++ " :" ++ Format.nest indent (Format.line ++ typeFmt)).group
       let rec ppVars (varNames : List Name) (prevType? : Option Expr) (fmt : Format) (localDecl : LocalDecl) : MetaM (List Name × Option Expr × Format) := do
         match localDecl with
-        | .cdecl _ _ varName type _ _ =>
+        | .cdecl _ _ varName type ..
+        | .ldecl _ _ varName type (nondep := true) .. =>
           let varName := varName.simpMacroScopes
           let type ← instantiateMVars type
           if prevType? == none || prevType? == some type then
@@ -110,7 +111,7 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
           else do
             let fmt ← pushPending varNames prevType? fmt
             return ([varName], some type, fmt)
-        | .ldecl _ _ varName type val _ _ => do
+        | .ldecl _ _ varName type val (nondep := false) .. => do
           let varName := varName.simpMacroScopes
           let fmt ← pushPending varNames prevType? fmt
           let fmt  := addLine fmt
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index f722f80069..d5ed78720d 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -379,13 +379,13 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
           let body' ← foldAndCollect oldIH newIH isRecCall (body.instantiate1 x)
           mkForallFVars #[x] body'
 
-    | .letE n t v b _ =>
+    | .letE n t v b nondep =>
       let t' ← foldAndCollect oldIH newIH isRecCall t
       let v' ← foldAndCollect oldIH newIH isRecCall v
-      withLetDecl n t' v' fun x => do
-        M.localMapM (mkLetFVars (usedLetOnly := true) #[x] ·) do
+      withLetDecl n t' v' (nondep := nondep) fun x => do
+        M.localMapM (mkLetFVars (usedLetOnly := true) (generalizeNondepLet := false) #[x] ·) do
           let b' ← foldAndCollect oldIH newIH isRecCall (b.instantiate1 x)
-          mkLetFVars #[x] b'
+          mkLetFVars (generalizeNondepLet := false) #[x] b'
 
     | .mdata m b =>
       pure <| .mdata m (← foldAndCollect oldIH newIH isRecCall b)
@@ -474,6 +474,11 @@ where
       for localDecl in (← getLCtx) do
         if localDecl.index > index && (!firstPass || localDecl.userName.hasMacroScopes) then
           if localDecl.isLet then
+            if ← Meta.isProp localDecl.type then
+              if let some mvarId' ← observing? <| mvarId.clearValue localDecl.fvarId then
+                return some mvarId'
+              else
+                continue
             if let some mvarId' ← observing? <| mvarId.clear localDecl.fvarId then
               return some mvarId'
           if let some mvarId' ← substVar? mvarId localDecl.fvarId then
@@ -908,10 +913,10 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
   if let some (n, t, v, b) := e.letFun? then
     let t' ← foldAndCollect oldIH newIH isRecCall t
     let v' ← foldAndCollect oldIH newIH isRecCall v
-    return ← withLocalDeclD n t' fun x => M2.branch do
+    return ← withLetDecl n t' v' fun x => M2.branch do
       let b' ← withRewrittenMotiveArg goal (rwHaveWith x) fun goal' =>
         buildInductionBody toErase toClear goal' oldIH newIH isRecCall (b.instantiate1 x)
-      mkLetFun x v' b'
+      mkLetFVars #[x] b' (usedLetOnly := false)
 
   -- Special case for traversing the PProd’ed bodies in our encoding of structural mutual recursion
   if let .lam n t b bi := e then
diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean
index 6be402666e..6a6cd137f5 100644
--- a/src/Lean/Meta/Tactic/Intro.lean
+++ b/src/Lean/Meta/Tactic/Intro.lean
@@ -31,6 +31,11 @@ namespace Lean.Meta
       let val    := val.instantiateRevRange j fvars.size fvars
       let fvarId ← mkFreshFVarId
       let (n, s) ← mkName lctx n true s
+      /-
+      We have both dependent and non-dependent `let` expressions result in dependent `ldecl`s.
+      It is counterintuitive if `have` expressions are introduced with opaque values,
+      especially when we run transformations to aggressively turn `let`s into `have`s.
+      -/
       let lctx   := lctx.mkLetDecl fvarId n type val
       let fvar   := mkFVar fvarId
       let fvars  := fvars.push fvar
diff --git a/src/Lean/Meta/Tactic/Lets.lean b/src/Lean/Meta/Tactic/Lets.lean
index 3ae92820e2..c67eb8023e 100644
--- a/src/Lean/Meta/Tactic/Lets.lean
+++ b/src/Lean/Meta/Tactic/Lets.lean
@@ -17,17 +17,18 @@ namespace Lean.Meta
 /-!
 ### `let` extraction
 
-Extracting `let`s means to locate `let`/`letFun`s in a term and to extract them
+Extracting `let`s means to locate `let`/`have`s in a term and to extract them
 from the term, extending the local context with new declarations in the process.
-A related process is lifting `lets`, which means to move `let`/`letFun`s toward the root of a term.
+A related process is lifting `lets`, which means to move `let`/`have`s toward the root of a term.
 -/
 
 namespace ExtractLets
 
 structure LocalDecl' where
+  /-- An `ldecl` with `nondep := false`. -/
   decl : LocalDecl
   /--
-  If true, is a `let`, if false, is a `letFun`.
+  If true, is a `let`, if false, is a `have`.
   Used in `lift` mode.
   -/
   isLet : Bool
@@ -90,13 +91,13 @@ def isExtractableLet (fvars : List Expr) (n : Name) (t v : Expr) : M (Bool × Na
     if let some n ← nextNameForBinderName? n then
       return (true, n)
   -- In lift mode, we temporarily extract non-extractable lets, but we do not make use of `givenNames` for them.
-  -- These will be flushed as let/letFun expressions, and we wish to preserve the original binder name.
+  -- These will be flushed as let/have expressions, and we wish to preserve the original binder name.
   if (← read).lift then
     return (true, n)
   return (false, n)
 
 /--
-Adds the `decl` to the `decls` list. Assumes that `decl` is an ldecl.
+Adds the `decl` to the `decls` list. Assumes that `decl` is an ldecl with `nondep := false`.
 -/
 def addDecl (decl : LocalDecl) (isLet : Bool) : M Unit := do
   let cfg ← read
@@ -140,13 +141,9 @@ This should *not* be used when closing lets for new goal metavariables, since
 1. The goal contains the decls in its local context, violating the assumption.
 2. We need to use true `let`s in that case, since tactics may zeta-delta reduce these declarations.
 -/
-def mkLetDecls (decls : Array LocalDecl') (e : Expr) : MetaM Expr := do
-  withEnsuringDeclsInContext decls do
-    decls.foldrM (init := e) fun { decl, isLet } e => do
-      if isLet then
-        return .letE decl.userName decl.type decl.value (e.abstract #[decl.toExpr]) false
-      else
-        mkLetFun decl.toExpr decl.value e
+def mkLetDecls (decls : Array LocalDecl') (e : Expr) : Expr :=
+  decls.foldr (init := e) fun { decl, isLet } e =>
+    Expr.letE decl.userName decl.type decl.value (e.abstract #[decl.toExpr]) (nondep := !isLet)
 
 /--
 Makes sure the declaration for `fvarId` is marked with `isLet := true`.
@@ -227,7 +224,7 @@ partial def extractCore (fvars : List Expr) (e : Expr) (topLevel : Bool := false
       match e with
       | .bvar .. | .fvar .. | .mvar .. | .sort .. | .const .. | .lit .. => unreachable!
       | .mdata _ e'      => return e.updateMData! (← extractCore fvars e' (topLevel := topLevel))
-      | .letE n t v b _  => extractLetLike true n t v b (fun t v b => pure <| e.updateLetE! t v b) (topLevel := topLevel)
+      | .letE n t v b nondep  => extractLetLike (!nondep) n t v b (fun t v b => pure <| e.updateLetE! t v b) (topLevel := topLevel)
       | .app ..          =>
         if e.isLetFun then
           extractLetFun e (topLevel := topLevel)
@@ -244,7 +241,7 @@ where
         let b ← extractCore (x :: fvars) (b.instantiate1 x)
         if (← read).lift then
           let toFlush ← flushDecls x.fvarId!
-          let b ← mkLetDecls toFlush b
+          let b := mkLetDecls toFlush b
           return mk t (b.abstract #[x])
         else
           return mk t (b.abstract #[x])
@@ -326,7 +323,7 @@ private def extractLetsImp (es : Array Expr) (givenNames : List Name)
   withExistingLocalDecls decls.toList <| k (decls.map (·.fvarId)) es givenNames'
 
 /--
-Extracts `let` and `letFun` expressions into local definitions,
+Extracts `let` and `have` expressions into local definitions,
 evaluating `k` at the post-extracted expressions and the extracted fvarids, within a context containing those local declarations.
 - The `givenNames` is a list of explicit names to use for extracted local declarations.
   If a name is `_` (or if there is no provided given name and `config.onlyGivenNames` is true) then uses a hygienic name
@@ -337,11 +334,11 @@ def extractLets [Monad m] [MonadControlT MetaM m] (es : Array Expr) (givenNames
   map3MetaM (fun k => extractLetsImp es givenNames k config) k
 
 /--
-Lifts `let` and `letFun` expressions in the given expression as far out as possible.
+Lifts `let` and `have` expressions in the given expression as far out as possible.
 -/
 def liftLets (e : Expr) (config : LiftLetsConfig := {}) : MetaM Expr := do
   let (es, st) ← ExtractLets.extract #[e] |>.run { config with onlyGivenNames := true } |>.run' {} |>.run { givenNames := [] }
-  ExtractLets.mkLetDecls st.decls es[0]!
+  return ExtractLets.mkLetDecls st.decls es[0]!
 
 end Lean.Meta
 
@@ -349,7 +346,7 @@ private def throwMadeNoProgress (tactic : Name) (mvarId : MVarId) : MetaM α :=
   throwTacticEx tactic mvarId m!"made no progress"
 
 /--
-Extracts `let` and `letFun` expressions from the target,
+Extracts `let` and `have` expressions from the target,
 returning `FVarId`s for the extracted let declarations along with the new goal.
 - The `givenNames` is a list of explicit names to use for extracted local declarations.
   If a name is `_` (or if there is no provided given name and `config.onlyGivenNames` is true) then uses a hygienic name
@@ -397,7 +394,7 @@ def Lean.MVarId.extractLetsLocalDecl (mvarId : MVarId) (fvarId : FVarId) (givenN
     | _ => throwTacticEx `extract_lets mvarId "unexpected auxiliary target"
 
 /--
-Lifts `let` and `letFun` expressions in target as far out as possible.
+Lifts `let` and `have` expressions in target as far out as possible.
 Throws an exception if nothing is lifted.
 
 Like `Lean.MVarId.extractLets`, but top-level lets are not added to the local context.
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 56f1785356..682beea1fe 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -235,9 +235,23 @@ inductive SimpLetCase where
   | nondep -- `let x := v; b` is equivalent to `(fun x => b) v`, and result type does not depend on `x`
 deriving Repr
 
-def getSimpLetCase (n : Name) (t : Expr) (b : Expr) : MetaM SimpLetCase := do
+def getSimpLetCase (n : Name) (t : Expr) (b : Expr) (nondep : Bool) : MetaM SimpLetCase := do
   withLocalDeclD n t fun x => do
     let bx := b.instantiate1 x
+    /-
+    If the let has `nondep := true`, then we know the body does not depend on the value already.
+    Then there are two cases, depending on whether or not the type of the body refers to the variable.
+    -/
+    if nondep then
+      let bxType ← whnf (← inferType bx)
+      if (← dependsOn bxType x.fvarId!) then
+        return .nondepDepVar
+      else
+        return .nondep
+    /-
+    Otherwise, we first detect whether `nondep := true` *should* have been set by checking type correctness of the body.
+    If that fails, the let is dependent.
+    -/
     /- The following step is potentially very expensive when we have many nested let-decls.
        TODO: handle a block of nested let decls in a single pass if this becomes a performance problem. -/
     if (← isTypeCorrect bx) then
@@ -389,11 +403,13 @@ def simpForall (e : Expr) : SimpM Result := withParent e do
     return { expr := (← dsimp e) }
 
 def simpLet (e : Expr) : SimpM Result := do
-  let .letE n t v b _ := e | unreachable!
+  let .letE n t v b nondep := e | unreachable!
   if (← getConfig).zeta then
     return { expr := b.instantiate1 v }
+  else if !b.hasLooseBVars && (← getConfig).zetaUnused then
+    return { expr := b.lowerLooseBVars 1 1 }
   else
-    let simpLetCase ← getSimpLetCase n t b
+    let simpLetCase ← getSimpLetCase n t b nondep
     trace[Debug.Meta.Tactic.simp] "getSimpLetCase is {repr simpLetCase}:{indentExpr e}"
     match simpLetCase with
     | SimpLetCase.dep => return { expr := (← dsimp e) }
@@ -405,7 +421,7 @@ def simpLet (e : Expr) : SimpM Result := do
         let hb? ← match rbx.proof? with
           | none => pure none
           | some h => pure (some (← mkLambdaFVars #[x] h))
-        let e' := mkLet n t rv.expr (← rbx.expr.abstractM #[x])
+        let e' := mkLet n t rv.expr (← rbx.expr.abstractM #[x]) (nondep := true)
         match rv.proof?, hb? with
         | none,   none   => return { expr := e' }
         | some h, none   => return { expr := e', proof? := some (← mkLetValCongr (← mkLambdaFVars #[x] rbx.expr) h) }
@@ -415,7 +431,7 @@ def simpLet (e : Expr) : SimpM Result := do
       withLocalDeclD n t fun x => withNewLemmas #[x] do
         let bx := b.instantiate1 x
         let rbx ← simp bx
-        let e' := mkLet n t v' (← rbx.expr.abstractM #[x])
+        let e' := mkLet n t v' (← rbx.expr.abstractM #[x]) (nondep := true)
         match rbx.proof? with
         | none => return { expr := e' }
         | some h =>
@@ -721,8 +737,16 @@ def simpApp (e : Expr) : SimpM Result := do
   if isOfNatNatLit e || isOfScientificLit e || isCharLit e then
     -- Recall that we fold "orphan" kernel Nat literals `n` into `OfNat.ofNat n`
     return { expr := e }
-  else if isNonDepLetFun e then
-    simpNonDepLetFun e
+  else if let some (args, n, t, v, b) := e.letFunAppArgs? then
+    /-
+    Note: we will be removing `letFun`, and we want everything to be in terms of `nondep := true` lets.
+    This used to call `simpNonDepLetFun`, which is optimized for letFun telescopes.
+    Considerations:
+    - we will soon replace `simpNonDepLetFun` with a `let` version
+    - simp is now using the `nondep` flag to cache which `let`s are nondependent.
+    - even without the optimized version we still manage to pass the test suite for now without timing out.
+    -/
+    return { expr := mkAppN (Expr.letE n t v b true) args }
   else
     congr e
 
diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean
index 1f2f5185ea..aaa968f565 100644
--- a/src/Lean/Meta/Transform.lean
+++ b/src/Lean/Meta/Transform.lean
@@ -113,10 +113,10 @@ partial def transformWithCache {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT
         | e => visitPost (← mkForallFVars (usedLetOnly := usedLetOnly) fvars (← visit (e.instantiateRev fvars)))
       let rec visitLet (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
         match e with
-        | .letE n t v b _ =>
-          withLetDecl n (← visit (t.instantiateRev fvars)) (← visit (v.instantiateRev fvars)) fun x =>
+        | .letE n t v b nondep =>
+          withLetDecl n (← visit (t.instantiateRev fvars)) (← visit (v.instantiateRev fvars)) (nondep := nondep) fun x =>
             visitLet (fvars.push x) b
-        | e => visitPost (← mkLetFVars (usedLetOnly := usedLetOnly) fvars (← visit (e.instantiateRev fvars)))
+        | e => visitPost (← mkLetFVars (usedLetOnly := usedLetOnly) (generalizeNondepLet := false) fvars (← visit (e.instantiateRev fvars)))
       let visitApp (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
         e.withApp fun f args => do
           if skipConstInApp && f.isConst then
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 4c6344fd29..53af950a18 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -372,8 +372,7 @@ end
   | .fvar fvarId   =>
     let decl ← fvarId.getDecl
     match decl with
-    | .cdecl .. => return e
-    | .ldecl (value := v) .. =>
+    | .ldecl (value := v) (nondep := false) .. =>
       -- Let-declarations marked as implementation detail should always be unfolded
       -- We initially added this feature for `simp`, and added it here for consistency.
       let cfg ← getConfig
@@ -383,6 +382,7 @@ end
       if (← read).trackZetaDelta then
         modify fun s => { s with zetaDeltaFVarIds := s.zetaDeltaFVarIds.insert fvarId }
       whnfEasyCases v k
+    | _ => return e
   | .mvar mvarId   =>
     match (← getExprMVarAssignment? mvarId) with
     | some v => whnfEasyCases v k
@@ -697,7 +697,7 @@ partial def smartUnfoldingReduce? (e : Expr) : MetaM (Option Expr) :=
 where
   go (e : Expr) : OptionT MetaM Expr := do
     match e with
-    | .letE n t v b _ => withLetDecl n t (← go v) fun x => do mkLetFVars #[x] (← go (b.instantiate1 x))
+    | .letE n t v b nondep => mapLetDecl n t (← go v) (nondep := nondep) fun x => go (b.instantiate1 x)
     | .lam .. => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← go b)
     | .app f a .. => return mkApp (← go f) (← go a)
     | .proj _ _ s => return e.updateProj! (← go s)
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 82a5db59e2..25e7beda45 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -144,7 +144,7 @@ the requirements imposed by these modules.
     process above is recursive. We claim it terminates because we keep
     creating new metavariables with smaller local contexts.
 
-  - Suppose, we have `t[?m]` and we want to create a let-expression by
+  - Suppose we have `t[?m]` and we want to create a `let`-expression by
     abstracting a let-decl free variable `x`, and the local context of
     `?m` contains `x`. Similarly to the previous case
     ```
@@ -153,13 +153,14 @@ the requirements imposed by these modules.
     will be ill-formed if we later assign a term `s` to `?m`, and
     `s` contains free variable `x`. Again, assume the type of `?m` is `A[x]`.
 
-    1. If `?m` is natural or synthetic, then we create `?n : (let x : T := v; A[x])` with
-       and local context := local context of `?m` - `x`, we assign `?m := ?n`,
-       and produce the term `let x : T := v; t[?n]`. That is, we are just making
+    1. If `?m` is natural or synthetic, then we create `?n : (let x : T := v; A[x])` whose
+       local context is the local context of `?m` minus `x`, we assign `?m := ?n`
+       (which is correct since the types of `?m` and `?n` both reduce to `A[v]`),
+       and then produce the term `let x : T := v; t[?n]`. That is, we are just making
        sure `?n` must never be assigned to a term containing `x`.
 
     2. If `?m` is syntheticOpaque, we create a fresh syntheticOpaque `?n`
-       with type `?n : T -> (let x : T := v; A[x])` and local context := local context of `?m` - `x`,
+       with type `?n : T -> (let x : T := v; A[x])` whose local context is the local context of `?m` minus `x`,
        create the delayed assignment `?n #[x] := ?m`, and produce the term `let x : T := v; t[?n x]`.
 
        Now suppose we assign `s` to `?m`. We do not assign the term `fun (x : T) => s` to `?n`, since
@@ -170,6 +171,18 @@ the requirements imposed by these modules.
        We are essentially using the pair "delayed assignment + application" to implement a delayed
        substitution.
 
+  - Suppose we have `t[?m]` and we want to create a `have`-expression
+    by abstracting a *nondependent* let-decl free variable `x`.
+    This needs a different procedure since `A[x]` does not reduce to `A[v]`.
+    It is the same as abstracting for lambda expressions, but it produces `have` instead of lambda terms:
+
+    1. If `?m` is natural or synthetic, then we create `?n : ∀ (x : T), A[x]` whose
+       local context is the local context of `?m` minus `x`, and then we assign `?m := ?n x`,
+       and we produce the term `have x : T := v; t[?n x]`.
+
+    2. If `?m` is syntheticOpaque, we create the same `?n` but as syntheticOpaque,
+       create the delayed assignment `?n #[x] := ?m`, and produce the term `have x : T := v; t[?n x]`.
+
 - We use TC for implementing coercions. Both Joe Hendrix and Reid Barton
   reported a nasty limitation. In Lean3, TC will not be used if there are
   metavariables in the TC problem. For example, the elaborator will not try
@@ -600,10 +613,10 @@ def instantiateLCtxMVars [Monad m] [MonadMCtx m] (lctx : LocalContext) : m Local
      | .cdecl _ fvarId userName type bi k =>
        let type ← instantiateMVars type
        return lctx.mkLocalDecl fvarId userName type bi k
-     | .ldecl _ fvarId userName type value nonDep k =>
+     | .ldecl _ fvarId userName type value nondep k =>
        let type ← instantiateMVars type
        let value ← instantiateMVars value
-       return lctx.mkLetDecl fvarId userName type value nonDep k
+       return lctx.mkLetDecl fvarId userName type value nondep k
 
 def instantiateMVarDeclMVars [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Unit := do
   let mvarDecl     := (← getMCtx).getDecl mvarId
@@ -616,8 +629,8 @@ def instantiateLocalDeclMVars [Monad m] [MonadMCtx m] (localDecl : LocalDecl) :
   match localDecl with
   | .cdecl idx id n type bi k =>
     return .cdecl idx id n (← instantiateMVars type) bi k
-  | .ldecl idx id n type val nonDep k =>
-    return .ldecl idx id n (← instantiateMVars type) (← instantiateMVars val) nonDep k
+  | .ldecl idx id n type val nondep k =>
+    return .ldecl idx id n (← instantiateMVars type) (← instantiateMVars val) nondep k
 
 namespace DependsOn
 
@@ -698,15 +711,21 @@ end DependsOn
   return result
 
 /--
-  Similar to `findExprDependsOn`, but checks the expressions in the given local declaration
-  depends on a free variable `x` s.t. `pf x` is `true` or an unassigned metavariable `?m` s.t. `pm ?m` is true. -/
-@[inline] def findLocalDeclDependsOn [Monad m] [MonadMCtx m] (localDecl : LocalDecl) (pf : FVarId → Bool := fun _ => false) (pm : MVarId → Bool := fun _ => false) : m Bool := do
+Similar to `findExprDependsOn`, but checks the expressions in the given local declaration
+depends on a free variable `x` s.t. `pf x` is `true` or an unassigned metavariable `?m` s.t. `pm ?m` is true.
+- When `generalizeNondepLet := true` (the default), then values of nondependent lets are ignored,
+  for computing dependencies from "within" a telescope.
+-/
+@[inline] def findLocalDeclDependsOn [Monad m] [MonadMCtx m] (localDecl : LocalDecl) (pf : FVarId → Bool := fun _ => false) (pm : MVarId → Bool := fun _ => false) (generalizeNondepLet := true) : m Bool := do
   match localDecl with
   | .cdecl (type := t) ..  => findExprDependsOn t pf pm
-  | .ldecl (type := t) (value := v) .. =>
-    let (result, { mctx, .. }) := (DependsOn.main pf pm t <||> DependsOn.main pf pm v).run { mctx := (← getMCtx) }
-    setMCtx mctx
-    return result
+  | .ldecl (type := t) (value := v) (nondep := nondep) .. =>
+    if generalizeNondepLet && nondep then
+      findExprDependsOn t pf pm
+    else
+      let (result, { mctx, .. }) := (DependsOn.main pf pm t <||> DependsOn.main pf pm v).run { mctx := (← getMCtx) }
+      setMCtx mctx
+      return result
 
 def exprDependsOn [Monad m] [MonadMCtx m] (e : Expr) (fvarId : FVarId) : m Bool :=
   findExprDependsOn e (fvarId == ·)
@@ -715,9 +734,13 @@ def exprDependsOn [Monad m] [MonadMCtx m] (e : Expr) (fvarId : FVarId) : m Bool
 def dependsOn [Monad m] [MonadMCtx m] (e : Expr) (fvarId : FVarId) : m Bool :=
   exprDependsOn e fvarId
 
-/-- Return true iff `localDecl` depends on the free variable `fvarId` -/
-def localDeclDependsOn [Monad m] [MonadMCtx m] (localDecl : LocalDecl) (fvarId : FVarId) : m Bool :=
-  findLocalDeclDependsOn localDecl (fvarId == ·)
+/--
+Returns true iff `localDecl` depends on the free variable `fvarId`
+- When `generalizeNondepLet := true` (the default), then values of nondependent lets are ignored,
+  for computing dependencies from "within" a telescope.
+-/
+def localDeclDependsOn [Monad m] [MonadMCtx m] (localDecl : LocalDecl) (fvarId : FVarId) (generalizeNondepLet := true) : m Bool :=
+  findLocalDeclDependsOn localDecl (fvarId == ·) (generalizeNondepLet := generalizeNondepLet)
 
 /-- Similar to `exprDependsOn`, but `x` can be a free variable or an unassigned metavariable. -/
 def exprDependsOn' [Monad m] [MonadMCtx m] (e : Expr) (x : Expr) : m Bool :=
@@ -729,11 +752,11 @@ def exprDependsOn' [Monad m] [MonadMCtx m] (e : Expr) (x : Expr) : m Bool :=
     return false
 
 /-- Similar to `localDeclDependsOn`, but `x` can be a free variable or an unassigned metavariable. -/
-def localDeclDependsOn' [Monad m] [MonadMCtx m] (localDecl : LocalDecl) (x : Expr) : m Bool :=
+def localDeclDependsOn' [Monad m] [MonadMCtx m] (localDecl : LocalDecl) (x : Expr) (generalizeNondepLet := true) : m Bool :=
   if x.isFVar then
-    findLocalDeclDependsOn localDecl (x.fvarId! == ·)
+    findLocalDeclDependsOn localDecl (x.fvarId! == ·) (generalizeNondepLet := generalizeNondepLet)
   else if x.isMVar then
-    findLocalDeclDependsOn localDecl (pm := (x.mvarId! == ·))
+    findLocalDeclDependsOn localDecl (pm := (x.mvarId! == ·)) (generalizeNondepLet := generalizeNondepLet)
   else
     return false
 
@@ -742,8 +765,8 @@ def dependsOnPred [Monad m] [MonadMCtx m] (e : Expr) (pf : FVarId → Bool := fu
   findExprDependsOn e pf pm
 
 /-- Return true iff the local declaration `localDecl` depends on a free variable `x` s.t. `pf x`, an unassigned metavariable `?m` s.t. `pm ?m` is true. -/
-def localDeclDependsOnPred [Monad m] [MonadMCtx m] (localDecl : LocalDecl) (pf : FVarId → Bool := fun _ => false) (pm : MVarId → Bool := fun _ => false) : m Bool := do
-  findLocalDeclDependsOn localDecl pf pm
+def localDeclDependsOnPred [Monad m] [MonadMCtx m] (localDecl : LocalDecl) (pf : FVarId → Bool := fun _ => false) (pm : MVarId → Bool := fun _ => false) (generalizeNondepLet := true) : m Bool := do
+  findLocalDeclDependsOn localDecl pf pm (generalizeNondepLet := generalizeNondepLet)
 
 
 namespace MetavarContext
@@ -949,6 +972,9 @@ private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr)
   return a new array of free variables that contains `toRevert` and all variables
   in `lctx` that may depend on `toRevert`.
 
+  When `generalizeNondepLet := true` (the default), then the values of nondependent lets are not considered
+  when computing forward dependencies.
+
   Remark: the result is sorted by `LocalDecl` indices.
 
   Remark: We used to throw an `Exception.revertFailure` exception when an auxiliary declaration
@@ -969,7 +995,7 @@ private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr)
   When we try to create the lambda `fun {α : Type} (a : α) => ?m`, we first need to create
   an auxiliary `?n` which does not contain `α` and `a` in its context. That is,
   we create the metavariable `?n : {α : Type} → (a : α) → (f : α → List α) → List α`,
-  add the delayed assignment `?n #[α, a, f] := ?m`, and create the lambda
+  add the delayed assignment `?n #[l, a, f] := ?m`, and create the lambda
   `fun {α : Type} (a : α) => ?n α a f`.
 
   See `elimMVarDeps` for more information.
@@ -980,7 +1006,7 @@ private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr)
   Note that <https://github.com/leanprover/lean/issues/1258> is not an issue in Lean4 because
   we have changed how we compile recursive definitions.
 -/
-def collectForwardDeps (lctx : LocalContext) (toRevert : Array Expr) : M (Array Expr) := do
+def collectForwardDeps (lctx : LocalContext) (toRevert : Array Expr) (generalizeNondepLet := true) : M (Array Expr) := do
   if toRevert.size == 0 then
     pure toRevert
   else
@@ -991,7 +1017,7 @@ def collectForwardDeps (lctx : LocalContext) (toRevert : Array Expr) : M (Array
         i.forM fun j _ => do
           let prevFVar := toRevert[j]
           let prevDecl := lctx.getFVar! prevFVar
-          if (← localDeclDependsOn prevDecl fvar.fvarId!) then
+          if (← localDeclDependsOn prevDecl fvar.fvarId! (generalizeNondepLet := generalizeNondepLet)) then
             throw (Exception.revertFailure (← getMCtx) lctx toRevert prevDecl.userName.toString)
     let newToRevert      := if (← preserveOrder) then toRevert else Array.mkEmpty toRevert.size
     let firstDeclToVisit := getLocalDeclWithSmallestIdx lctx toRevert
@@ -1001,7 +1027,7 @@ def collectForwardDeps (lctx : LocalContext) (toRevert : Array Expr) : M (Array
         return newToRevert
       else if toRevert.any fun x => decl.fvarId == x.fvarId! then
         return newToRevert.push decl.toExpr
-      else if (← findLocalDeclDependsOn decl (newToRevert.any fun x => x.fvarId! == ·)) then
+      else if (← findLocalDeclDependsOn decl (newToRevert.any fun x => x.fvarId! == ·) (generalizeNondepLet := generalizeNondepLet)) then
         return newToRevert.push decl.toExpr
       else
         return newToRevert
@@ -1076,12 +1102,16 @@ mutual
           let type := type.headBeta
           let type ← abstractRangeAux xs i type
           return Lean.mkForall n bi type e
-        | LocalDecl.ldecl _ _ n type value nonDep _ =>
+        | LocalDecl.ldecl (nondep := true) _ _ n type _ _ =>
+          let type := type.headBeta
+          let type ← abstractRangeAux xs i type
+          return Lean.mkForall n .default type e
+        | LocalDecl.ldecl (nondep := false) _ _ n type value _ =>
           if !usedLetOnly || e.hasLooseBVar 0 then
             let type := type.headBeta
             let type  ← abstractRangeAux xs i type
             let value ← abstractRangeAux xs i value
-            let e := mkLet n type value e nonDep
+            let e := mkLet n type value e false
             match kind with
             | MetavarKind.syntheticOpaque =>
               -- See "Gruesome details" section in the beginning of the file
@@ -1233,16 +1263,25 @@ private def mkLambda' (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) (etaRed
     mkLambda x bi t b
 
 /--
-  Similar to `LocalContext.mkBinding`, but handles metavariables correctly.
-  If `usedOnly == true` then `forall` and `lambda` expressions are created only for used variables.
-  If `usedLetOnly == true` then `let` expressions are created only for used (let-) variables. -/
-def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool) (usedLetOnly : Bool) (etaReduce : Bool) : M Expr := do
+Similar to `LocalContext.mkBinding`, but handles metavariables correctly.
+This function trusts that `xs` has all forward dependencies that appear in `e` and that the variables are in order.
+
+- If `usedOnly := true` then `forall` and `lambda` expressions are created only for used variables.
+- If `usedLetOnly := true` then `let` expressions are created only for used (let-) variables.
+- If `generalizeNondepLet := true` then nondependent let variables become `forall` or `lambda` expressions
+  according to the value of `usedOnly`.
+  Generally, `generalizeNondepLet` should be `true` *unless* `mkBinding` is being used when leaving a telescope combinator (like `Meta.lambdaLetTelescope`).
+  This needs to be `true` when making terms that should remain type correct with respect to the same `lctx`;
+  for example, if `e' ← mkBinding true lctx xs e (generalizeNondepLet := true)` and `xs' ← xs.filterM (FVarId.isLetVar · false)`,
+  then one has that `mkAppN e' xs'` is definitionally equal to `e` with respect to `lctx`.
+  **Note:** `generalizeNondepLet := true` is the common case, so `mkBinding` API uses it as the default.
+-/
+def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool) (usedLetOnly : Bool) (etaReduce : Bool) (generalizeNondepLet : Bool) : M Expr := do
   let e ← abstractRange xs xs.size e
   xs.size.foldRevM (init := e) fun i _ e => do
       let x := xs[i]
       if x.isFVar then
-        match lctx.getFVar! x with
-        | LocalDecl.cdecl _ _ n type bi _ =>
+        let handleCDecl (n : Name) (type : Expr) (bi : BinderInfo) : M Expr := do
           if !usedOnly || e.hasLooseBVar 0 then
             let type := type.headBeta;
             let type ← abstractRange xs i type
@@ -1252,11 +1291,16 @@ def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Exp
               return Lean.mkForall n bi type e
           else
             return e.lowerLooseBVars 1 1
-        | LocalDecl.ldecl _ _ n type value nonDep _ =>
-          if !usedLetOnly || e.hasLooseBVar 0 then
+        match lctx.getFVar! x with
+        | LocalDecl.cdecl _ _ n type bi _ =>
+          handleCDecl n type bi
+        | LocalDecl.ldecl _ _ n type value nondep _ =>
+          if generalizeNondepLet && nondep then
+            handleCDecl n type .default
+          else if !usedLetOnly || e.hasLooseBVar 0 then
             let type  ← abstractRange xs i type
             let value ← abstractRange xs i value
-            return mkLet n type value e nonDep
+            return mkLet n type value e nondep
           else
             return e.lowerLooseBVars 1 1
       else
@@ -1283,21 +1327,21 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool) : MkBinding
 def revert (xs : Array Expr) (mvarId : MVarId) (preserveOrder : Bool) : MkBindingM (Expr × Array Expr) := fun ctx =>
   MkBinding.revert xs mvarId { preserveOrder, mainModule := ctx.mainModule }
 
-def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce := false) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr := fun ctx =>
+def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce := false) (generalizeNondepLet := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr := fun ctx =>
   let mvarIdsToAbstract := xs.foldl (init := {}) fun s x => if x.isMVar then s.insert x.mvarId! else s
-  MkBinding.mkBinding isLambda ctx.lctx xs e usedOnly usedLetOnly etaReduce { preserveOrder := false, binderInfoForMVars, mvarIdsToAbstract, mainModule := ctx.mainModule }
+  MkBinding.mkBinding isLambda ctx.lctx xs e usedOnly usedLetOnly etaReduce generalizeNondepLet { preserveOrder := false, binderInfoForMVars, mvarIdsToAbstract, mainModule := ctx.mainModule }
 
-@[inline] def mkLambda (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce := false) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
-  mkBinding (isLambda := true) xs e usedOnly usedLetOnly etaReduce binderInfoForMVars
+@[inline] def mkLambda (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce := false) (generalizeNondepLet := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
+  mkBinding (isLambda := true) xs e usedOnly usedLetOnly etaReduce generalizeNondepLet binderInfoForMVars
 
-@[inline] def mkForall (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
-  mkBinding (isLambda := false) xs e usedOnly usedLetOnly false binderInfoForMVars
+@[inline] def mkForall (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (generalizeNondepLet := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
+  mkBinding (isLambda := false) xs e usedOnly usedLetOnly false generalizeNondepLet binderInfoForMVars
 
 @[inline] def abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : MkBindingM Expr := fun ctx =>
   MkBinding.abstractRange xs n e { preserveOrder := false, mainModule := ctx.mainModule }
 
-@[inline] def collectForwardDeps (toRevert : Array Expr) (preserveOrder : Bool) : MkBindingM (Array Expr) := fun ctx =>
-  MkBinding.collectForwardDeps ctx.lctx toRevert { preserveOrder, mainModule := ctx.mainModule }
+@[inline] def collectForwardDeps (toRevert : Array Expr) (preserveOrder : Bool) (generalizeNondepLet := true) : MkBindingM (Array Expr) := fun ctx =>
+  MkBinding.collectForwardDeps ctx.lctx toRevert generalizeNondepLet { preserveOrder, mainModule := ctx.mainModule }
 
 /--
   `isWellFormed lctx e` returns true iff
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index c9ec2229ca..182bc2660d 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -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 ..  => lambdaLetTelescope e fun xs b => compileParserExpr b >>= mkLambdaFVars xs
+  | .lam ..  => mapLambdaLetTelescope e fun _ b => compileParserExpr b
   | .fvar .. => return e
   | _ => do
     let fn := e.getAppFn
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 566453f0ff..e8b844f412 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -1031,7 +1031,7 @@ def delabLetE : Delab := do
   let Expr.letE n t v b nondep ← getExpr | unreachable!
   let n ← getUnusedName n b
   let stxV ← descend v 1 delab
-  let (stxN, stxB) ← withLetDecl n t v fun fvar => do
+  let (stxN, stxB) ← withLetDecl n t v (nondep := nondep) fun fvar => do
     let b := b.instantiate1 fvar
     return (← mkAnnotatedIdent n fvar, ← descend b 2 delab)
   if ← getPPOption getPPLetVarTypes <||> getPPOption getPPAnalysisLetVarType then
@@ -1305,7 +1305,7 @@ partial def delabDoElems : DelabM (List Syntax) := do
     let n ← getUnusedName n b
     let stxT ← descend t 0 delab
     let stxV ← descend v 1 delab
-    withLetDecl n t v fun fvar =>
+    withLetDecl n t v (nondep := nondep) fun fvar =>
       let b := b.instantiate1 fvar
       descend b 2 $
         if nondep then
diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
index 30909660e4..09f49b2696 100644
--- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
@@ -121,8 +121,8 @@ def withLetValue (x : m α) : m α := do
   descend v 1 x
 
 def withLetBody (x : m α) : m α := do
-  let Expr.letE n t v b _ ← getExpr | unreachable!
-  Meta.withLetDecl n t v fun fvar =>
+  let Expr.letE n t v b nondep ← getExpr | unreachable!
+  Meta.withLetDecl n t v (nondep := nondep) fun fvar =>
     let b := b.instantiate1 fvar
     descend b 2 x
 
diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean
index 1282084ec5..56ca994923 100644
--- a/src/Lean/Widget/InteractiveGoal.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -176,7 +176,8 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
         continue
       else
         match localDecl with
-        | LocalDecl.cdecl _index fvarId varName type _ _ =>
+        | LocalDecl.cdecl _index fvarId varName type ..
+        | LocalDecl.ldecl _index fvarId varName type (nondep := true) .. =>
           -- We rely on the fact that `withGoalCtx` runs `LocalContext.sanitizeNames`,
           -- so the `userName`s of local hypotheses are already pretty-printed
           -- and it suffices to simply `toString` them.
@@ -188,7 +189,7 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
             hyps ← pushPending varNames prevType? hyps
             varNames := #[(varName, fvarId)]
           prevType? := some type
-        | LocalDecl.ldecl _index fvarId varName type val _ _ => do
+        | LocalDecl.ldecl _index fvarId varName type val (nondep := false) .. => do
           let varName := toString varName
           hyps ← pushPending varNames prevType? hyps
           let type ← instantiateMVars type
diff --git a/tests/lean/letFun.lean b/tests/lean/letFun.lean
index c7bede1899..98a2c494f6 100644
--- a/tests/lean/letFun.lean
+++ b/tests/lean/letFun.lean
@@ -1,34 +1,34 @@
 import Lean.Elab.Command
 
 /-!
-# Tests for `let_fun x := v; b` notation
+# Tests for `have x := v; b` notation
 -/
 
 /-!
-Checks that types can be inferred and that default instances work with `let_fun`.
+Checks that types can be inferred and that default instances work with `have`.
 -/
 #check
-  let_fun f x := x * 2
-  let_fun x := 1
-  let_fun y := x + 1
+  have f x := x * 2
+  have x := 1
+  have y := x + 1
   f (y + x)
 
 /-!
-Checks that `simp` can do zeta reduction of `let_fun`s
+Checks that `simp` can do zeta reduction of `have`s
 -/
-example (a b : Nat) (h1 : a = 0) (h2 : b = 0) : (let_fun x := a + 1; x + x) > b := by
+example (a b : Nat) (h1 : a = 0) (h2 : b = 0) : (have x := a + 1; x + x) > b := by
   simp (config := { zeta := false }) [h1]
   trace_state
   simp (config := { decide := true }) [h2]
 
 /-!
-Checks that the underlying encoding for `let_fun` can be overapplied.
-This still pretty prints with `let_fun` notation.
+Checks that the underlying encoding for `have` can be overapplied.
+This still pretty prints with `have` notation.
 -/
 #check (show Nat → Nat from id) 1
 
 /-!
-Checks that zeta reduction still occurs even if the `let_fun` is applied to an argument.
+Checks that zeta reduction still occurs even if the `have` is applied to an argument.
 -/
 example (a b : Nat) (h : a > b) : (show Nat → Nat from id) a > b := by
   simp
@@ -36,23 +36,23 @@ example (a b : Nat) (h : a > b) : (show Nat → Nat from id) a > b := by
   exact h
 
 /-!
-Checks that the type of a `let_fun` can depend on the value.
+Checks that the type of a `have` can depend on the value.
 -/
-#check let_fun n := 5
+#check have n := 5
   (⟨[], Nat.zero_le n⟩ : { as : List Bool // as.length ≤ n })
 
 /-!
-Check that `let_fun` is reducible.
+Check that `have` is reducible.
 -/
-#check (rfl : (let_fun n := 5; n) = 5)
+#check (rfl : (have n := 5; n) = 5)
 
 /-!
-Exercise `isDefEqQuick` for `let_fun`.
+Exercise `isDefEqQuick` for `have`.
 -/
-#check (rfl : (let_fun _n := 5; 2) = 2)
+#check (rfl : (have _n := 5; 2) = 2)
 
 /-!
-Check that `let_fun` responds to WHNF's `zeta` option.
+Check that `have` responds to WHNF's `zeta` option.
 -/
 
 open Lean Meta Elab Term in
@@ -61,5 +61,5 @@ elab "#whnfCore " z?:(&"noZeta")? t:term : command => Command.runTermElabM fun _
   let e ← withConfig (fun c => { c with zeta := z?.isNone }) <| Meta.whnfCore e
   logInfo m!"{e}"
 
-#whnfCore let_fun n := 5; n
-#whnfCore noZeta let_fun n := 5; n
+#whnfCore have n := 5; n
+#whnfCore noZeta have n := 5; n
diff --git a/tests/lean/letFun.lean.expected.out b/tests/lean/letFun.lean.expected.out
index a55c0573d3..e7294ef0bb 100644
--- a/tests/lean/letFun.lean.expected.out
+++ b/tests/lean/letFun.lean.expected.out
@@ -15,7 +15,8 @@ a b : Nat
 h : a > b
 ⊢ b < a
 have n := 5;
-⟨[], ⋯⟩ : { as // as.length ≤ 5 }
+⟨[], ⋯⟩ : have n := 5;
+{ as // as.length ≤ n }
 rfl : (have n := 5;
   n) =
   have n := 5;
diff --git a/tests/lean/run/3943.lean b/tests/lean/run/3943.lean
index 2f7059709e..915e71fa94 100644
--- a/tests/lean/run/3943.lean
+++ b/tests/lean/run/3943.lean
@@ -9,8 +9,8 @@ example (f : Nat → Nat) : f x = 0 → f x + 1 = y := by
   sorry
 
 example (f : Nat → Nat) : let _  : f x = 0 := sorryAx _ false; f x + 1 = y := by
-  simp (config := { contextual := true, zeta := false })
-  guard_target =ₛ let _  : f x = 0 := sorryAx _ false; 1 = y
+  simp (config := { contextual := true, zeta := false, zetaUnused := false })
+  guard_target =ₛ have _  : f x = 0 := sorryAx _ false; 1 = y
   sorry
 
 def overlap : Nat → Nat
@@ -46,6 +46,6 @@ example : (if p x then g x else g x + 1) + g x = y := by
   sorry
 
 example : (let _  : p x := sorryAx _ false; g x + 1 = y) ↔ g x = y := by
-  simp (config := { zeta := false }) (discharger := assumption)
-  guard_target =ₛ (let _  : p x := sorryAx _ false; x + 1 = y) ↔ g x = y
+  simp (config := { zeta := false, zetaUnused := false }) (discharger := assumption)
+  guard_target =ₛ (have _  : p x := sorryAx _ false; x + 1 = y) ↔ g x = y
   sorry
diff --git a/tests/lean/run/clear_value.lean b/tests/lean/run/clear_value.lean
index 19a4c2bb6a..6cb9aca8a7 100644
--- a/tests/lean/run/clear_value.lean
+++ b/tests/lean/run/clear_value.lean
@@ -16,6 +16,21 @@ example : let x := 22; 0 ≤ x := by
   trace_state
   exact Nat.zero_le _
 
+/-!
+Check that `clear_value` preserves the order of the local context.
+-/
+/--
+trace: x : Nat
+y : Nat := 23
+⊢ True
+-/
+#guard_msgs in
+example : let _x := 22; let _y := 23; True := by
+  intro x y
+  clear_value x
+  trace_state
+  trivial
+
 /-!
 Test `*` mode.
 -/
diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean
index 30c0438744..79a99d86be 100644
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -109,8 +109,8 @@ def let_tailrec : Nat → Nat
 termination_by n => n
 
 /--
-info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) (a✝ : Nat) :
-  motive a✝
+info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive n.succ)
+  (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check let_tailrec.induct
@@ -545,7 +545,7 @@ termination_by xs => xs
 
 /--
 info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (_y : α) (ys : List α) (this : Nat), motive ys → motive (_y :: ys)) (a✝ : List α) : motive a✝
+  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) (a✝ : List α) : motive a✝
 -/
 #guard_msgs in
 #check bar.induct
diff --git a/tests/lean/run/letNonDep.lean b/tests/lean/run/letNonDep.lean
index 9770fc3405..0672eb5e3f 100644
--- a/tests/lean/run/letNonDep.lean
+++ b/tests/lean/run/letNonDep.lean
@@ -4,6 +4,8 @@ import Lean
 
 This file exercises the Lean/C++ interface to make sure that the `nondep` field
 is successfully part of the data model.
+
+It also tests the metaprogramming API.
 -/
 
 open Lean
@@ -83,3 +85,22 @@ info: Lean.Expr.letE `n (Lean.Expr.const `Nat []) (Lean.Expr.const `Nat.zero [])
   let m ← Meta.mkFreshExprMVar none
   m.mvarId!.assign (mkConst ``Unit)
   Lean.instantiateMVars (Lean.mkLet `n (mkConst ``Nat) (mkConst ``Nat.zero) m true)
+
+namespace TestLambdaLetTelescope
+/-!
+Check that `lambdaLetTelescope` consumes `haves`. Also checks that `preserveNondepLet := false` turns `have`s into `let`s.
+-/
+def c : Nat → Nat → Bool := fun x => have y := 1; fun z => x == y + z
+/--
+info: #[false, true, false]
+#[false, false, false]
+-/
+#guard_msgs in
+open Lean Meta in
+run_meta do
+  let decl ← getConstInfo ``c
+  lambdaLetTelescope decl.value! fun xs _ => do
+    IO.println <| ← xs.mapM fun x => return (← x.fvarId!.getDecl).isNondep
+  lambdaLetTelescope decl.value! (preserveNondepLet := false) fun xs _ => do
+    IO.println <| ← xs.mapM fun x => return (← x.fvarId!.getDecl).isNondep
+end TestLambdaLetTelescope
diff --git a/tests/lean/run/wf_preprocess.lean b/tests/lean/run/wf_preprocess.lean
index 2f52a7bcf3..22a771d5a4 100644
--- a/tests/lean/run/wf_preprocess.lean
+++ b/tests/lean/run/wf_preprocess.lean
@@ -19,6 +19,27 @@ def Tree.map (f : α → β) (t : Tree α) : Tree β :=
 termination_by t
 decreasing_by trace_state; cases t; decreasing_tactic
 
+/-!
+Checking that the attaches make their way through `let`s.
+-/
+/--
+trace: α : Type u_1
+t : Tree α
+cs : List (Tree α) := t.cs
+t' : Tree α
+h✝ : t' ∈ cs
+⊢ sizeOf t' < sizeOf t
+-/
+#guard_msgs(trace) in
+def Tree.map' (f : α → β) (t : Tree α) : Tree β :=
+  have n := 22
+  let v := t.val
+  let cs := t.cs
+  have : n = n := rfl
+  ⟨f v, 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 α),
diff --git a/tests/lean/run/zetaDelta.lean b/tests/lean/run/zetaDelta.lean
index 697648ddcf..7d81bb9025 100644
--- a/tests/lean/run/zetaDelta.lean
+++ b/tests/lean/run/zetaDelta.lean
@@ -19,5 +19,5 @@ example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
 example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
   intro x
   simp (config := { zetaDelta := true, zeta := false })
-  guard_target =ₛlet y := 4; 5 + y = z
+  guard_target =ₛ have y := 4; 5 + y = z
   rw [h]
diff --git a/tests/lean/simpZetaFalse.lean.expected.out b/tests/lean/simpZetaFalse.lean.expected.out
index 3e00ee99cc..df93d0ab67 100644
--- a/tests/lean/simpZetaFalse.lean.expected.out
+++ b/tests/lean/simpZetaFalse.lean.expected.out
@@ -1,6 +1,6 @@
 x : Nat
 h : f (f x) = x
-⊢ (let y := x * x;
+⊢ (have y := x * x;
     if True then 1 else y + 1) =
     1
 theorem ex1 : ∀ (x : Nat),
@@ -19,7 +19,7 @@ fun x h =>
 x z : Nat
 h : f (f x) = x
 h' : z = x
-⊢ (let y := x;
+⊢ (have y := x;
     y) =
     z
 theorem ex2 : ∀ (x z : Nat),
@@ -37,7 +37,7 @@ x z : Nat
     id
 p : Prop
 h : p
-⊢ (let n := 10;
+⊢ (have n := 10;
     fun x => True) =
     fun z => p
 theorem ex4 : ∀ (p : Prop),