diff --git a/src/Lean/Compiler/LCNF/LCtx.lean b/src/Lean/Compiler/LCNF/LCtx.lean
index 00b9253510..571493e810 100644
--- a/src/Lean/Compiler/LCNF/LCtx.lean
+++ b/src/Lean/Compiler/LCNF/LCtx.lean
@@ -63,11 +63,11 @@ Convert a LCNF local context into a regular Lean local context.
 def LCtx.toLocalContext (lctx : LCtx) : LocalContext := Id.run do
   let mut result := {}
   for (_, param) in lctx.params.toArray do
-    result := result.addDecl (.cdecl 0 param.fvarId param.binderName param.type .default)
+    result := result.addDecl (.cdecl 0 param.fvarId param.binderName param.type .default .default)
   for (_, decl) in lctx.letDecls.toArray do
-    result := result.addDecl (.ldecl 0 decl.fvarId decl.binderName decl.type decl.value true)
+    result := result.addDecl (.ldecl 0 decl.fvarId decl.binderName decl.type decl.value true .default)
   for (_, decl) in lctx.funDecls.toArray do
-    result := result.addDecl (.cdecl 0 decl.fvarId decl.binderName decl.type .default)
+    result := result.addDecl (.cdecl 0 decl.fvarId decl.binderName decl.type .default .default)
   return result
 
 end Lean.Compiler.LCNF
diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index ca65809fd1..de28569c5f 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -110,6 +110,17 @@ def isInternal : Name → Bool
   | num p _ => isInternal p
   | _       => false
 
+/--
+Checks whether the name is an implementation-detail hypothesis name.
+
+Implementation-detail hypothesis names start with a double underscore.
+-/
+def isImplementationDetail : Name → Bool
+  | str anonymous s => s.startsWith "__"
+  | num p _ => p.isImplementationDetail
+  | str p _ => p.isImplementationDetail
+  | anonymous => false
+
 def isAtomic : Name → Bool
   | anonymous       => true
   | str anonymous _ => true
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 60df180bde..2b0e742241 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -1000,7 +1000,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     let searchCtx : Unit → TermElabM LValResolution := fun _ => do
       let fullName := Name.mkStr structName fieldName
       for localDecl in (← getLCtx) do
-        if localDecl.binderInfo == BinderInfo.auxDecl then
+        if localDecl.isAuxDecl then
           if let some localDeclFullName := (← read).auxDeclToFullName.find? localDecl.fvarId then
             if fullName == (privateToUserName? localDeclFullName).getD localDeclFullName then
               /- LVal notation is being used to make a "local" recursive call. -/
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 6923e52eac..2f2a1274fe 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -57,6 +57,17 @@ structure BinderView where
   type : Syntax
   bi   : BinderInfo
 
+/--
+Determines the local declaration kind depending on the variable name.
+
+The `__x` in `let __x := 42; body` gets kind `.implDetail`.
+-/
+def kindOfBinderName (binderName : Name) : LocalDeclKind :=
+  if binderName.isImplementationDetail then
+    .implDetail
+  else
+    .default
+
 partial def quoteAutoTactic : Syntax → TermElabM Syntax
   | stx@(.ident ..) => throwErrorAt stx "invalid auto tactic, identifier is not allowed"
   | stx@(.node _ k args) => do
@@ -187,7 +198,9 @@ private partial def elabBinderViews (binderViews : Array BinderView) (fvars : Ar
         unless (← isClass? type).isSome do
           throwErrorAt binderView.type "invalid binder annotation, type is not a class instance{indentExpr type}\nuse the command `set_option checkBinderAnnotations false` to disable the check"
         withRef binderView.type <| checkLocalInstanceParameters type
-      withLocalDecl binderView.id.getId binderView.bi type fun fvar => do
+      let id := binderView.id.getId
+      let kind := kindOfBinderName id
+      withLocalDecl id binderView.bi type (kind := kind) fun fvar => do
         addLocalVarInfo binderView.ref fvar
         loop (i+1) (fvars.push (binderView.id, fvar))
     else
@@ -405,22 +418,23 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat
       let fvarId ← mkFreshFVarId
       let fvar  := mkFVar fvarId
       let s     := { s with fvars := s.fvars.push fvar }
-      -- dbgTrace (toString binderView.id.getId ++ " : " ++ toString type)
+      let id    := binderView.id.getId
+      let kind  := kindOfBinderName id
       /-
         We do **not** want to support default and auto arguments in lambda abstractions.
         Example: `fun (x : Nat := 10) => x+1`.
         We do not believe this is an useful feature, and it would complicate the logic here.
       -/
-      let lctx  := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi
+      let lctx  := s.lctx.mkLocalDecl fvarId id type binderView.bi kind
       addTermInfo' (lctx? := some lctx) (isBinder := true) binderView.ref fvar
       let s ← withRef binderView.id <| propagateExpectedType fvar type s
       let s := { s with lctx }
-      match (← isClass? type) with
-      | none           => elabFunBinderViews binderViews (i+1) s
-      | some className =>
+      match ← isClass? type, kind with
+      | some className, .default =>
         resettingSynthInstanceCache do
           let localInsts := s.localInsts.push { className, fvar := mkFVar fvarId }
           elabFunBinderViews binderViews (i+1) { s with localInsts }
+      | _, _ => elabFunBinderViews binderViews (i+1) s
   else
     pure s
 
@@ -653,15 +667,16 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
        -/
       let val  ← mkLambdaFVars fvars val (usedLetOnly := false)
       pure (type, val, binders)
+  let kind := kindOfBinderName id.getId
   trace[Elab.let.decl] "{id.getId} : {type} := {val}"
   let result ← if useLetExpr then
-    withLetDecl id.getId type val fun x => do
+    withLetDecl id.getId (kind := kind) type val fun x => do
       addLocalVarInfo id x
       let body ← elabTermEnsuringType body expectedType?
       let body ← instantiateMVars body
       mkLetFVars #[x] body (usedLetOnly := usedLetOnly)
   else
-    let f ← withLocalDecl id.getId BinderInfo.default type fun x => do
+    let f ← withLocalDecl id.getId (kind := kind) .default type fun x => do
       addLocalVarInfo id x
       let body ← elabTermEnsuringType body expectedType?
       let body ← instantiateMVars body
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 4bd17366ab..bc49ece918 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -328,7 +328,7 @@ def mkFreshJP (ps : Array (Var × Bool)) (body : Code) : TermElabM JPDecl := do
   -- Remark: the compiler frontend implemented in C++ currently detects jointpoints created by
   -- the "do" notation by testing the name. See hack at method `visit_let` at `lcnf.cpp`
   -- We will remove this hack when we re-implement the compiler frontend in Lean.
-  let name ← mkFreshUserName `_do_jp
+  let name ← mkFreshUserName `__do_jp
   pure { name := name, params := ps, body := body }
 
 def addFreshJP (ps : Array (Var × Bool)) (body : Code) : StateRefT (Array JPDecl) TermElabM Name := do
@@ -1225,9 +1225,9 @@ private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Synt
         throwErrorAt stx "cannot lift `(<- ...)` over a binder, this error usually happens when you are trying to lift a method nested in a `fun`, `let`, or `match`-alternative, and it can often be fixed by adding a missing `do`"
       let term := args[1]!
       let term ← expandLiftMethodAux inQuot inBinder term
-      let auxDoElem : Syntax ← `(doElem| let a ← $term:term)
+      let auxDoElem : Syntax ← `(doElem| let __do_lift ← $term:term)
       modify fun s => s ++ [auxDoElem]
-      `(a)
+      `(__do_lift)
     else do
       let inAntiquot := stx.isAntiquot && !stx.isEscapedAntiquot
       let inBinder   := inBinder || (!inQuot && liftMethodForbiddenBinder stx)
@@ -1325,9 +1325,9 @@ mutual
       let optElse := decl[3]
       if optElse.isNone then withFreshMacroScope do
         let auxDo ← if isMutableLet doLetArrow then
-          `(do let%$doLetArrow discr ← $doElem; let%$doLetArrow mut $pattern:term := discr)
+          `(do let%$doLetArrow __discr ← $doElem; let%$doLetArrow mut $pattern:term := __discr)
         else
-          `(do let%$doLetArrow discr ← $doElem; let%$doLetArrow $pattern:term := discr)
+          `(do let%$doLetArrow __discr ← $doElem; let%$doLetArrow $pattern:term := __discr)
         doSeqToCode <| getDoSeqElems (getDoSeq auxDo) ++ doElems
       else
         let contSeq ← if isMutableLet doLetArrow then
@@ -1337,7 +1337,7 @@ mutual
           pure doElems.toArray
         let contSeq := mkDoSeq contSeq
         let elseSeq := mkSingletonDoSeq optElse[1]
-        let auxDo ← `(do let%$doLetArrow discr ← $doElem; match%$doLetArrow discr with | $pattern:term => $contSeq | _ => $elseSeq)
+        let auxDo ← `(do let%$doLetArrow __discr ← $doElem; match%$doLetArrow __discr with | $pattern:term => $contSeq | _ => $elseSeq)
         doSeqToCode <| getDoSeqElems (getDoSeq auxDo)
     else
       throwError "unexpected kind of `do` declaration"
@@ -1353,7 +1353,7 @@ mutual
     else
       pure doElems.toArray
     let contSeq := mkDoSeq contSeq
-    let auxDo ← `(do let discr := $val; match discr with | $pattern:term => $contSeq | _ => $elseSeq)
+    let auxDo ← `(do let __discr := $val; match __discr with | $pattern:term => $contSeq | _ => $elseSeq)
     doSeqToCode <| getDoSeqElems (getDoSeq auxDo)
 
   /-- Generate `CodeBlock` for `doReassignArrow; doElems`
@@ -1374,7 +1374,7 @@ mutual
       let doElem  := decl[2]
       let optElse := decl[3]
       if optElse.isNone then withFreshMacroScope do
-        let auxDo ← `(do let discr ← $doElem; $pattern:term := discr)
+        let auxDo ← `(do let __discr ← $doElem; $pattern:term := __discr)
         doSeqToCode <| getDoSeqElems (getDoSeq auxDo) ++ doElems
       else
         throwError "reassignment with `|` (i.e., \"else clause\") is not currently supported"
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index b90a89c3d6..c912f16d16 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -496,11 +496,11 @@ private def pushNewVars (toProcess : Array FVarId) (s : CollectFVars.State) : Ar
   s.fvarSet.fold (init := toProcess) fun toProcess fvarId =>
     if toProcess.contains fvarId then toProcess else toProcess.push fvarId
 
-private def pushLocalDecl (toProcess : Array FVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (bi := BinderInfo.default)
+private def pushLocalDecl (toProcess : Array FVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) (kind : LocalDeclKind)
     : StateRefT ClosureState TermElabM (Array FVarId) := do
   let type ← preprocess type
   modify fun s => { s with
-    newLocalDecls := s.newLocalDecls.push <| LocalDecl.cdecl default fvarId userName type bi
+    newLocalDecls := s.newLocalDecls.push <| LocalDecl.cdecl default fvarId userName type bi kind
     exprArgs      := s.exprArgs.push (mkFVar fvarId)
   }
   return pushNewVars toProcess (collectFVars {} type)
@@ -514,21 +514,21 @@ private partial def mkClosureForAux (toProcess : Array FVarId) : StateRefT Closu
     let toProcess := toProcess.erase fvarId
     let localDecl ← fvarId.getDecl
     match localDecl with
-    | .cdecl _ _ userName type bi =>
-      let toProcess ← pushLocalDecl toProcess fvarId userName type bi
+    | .cdecl _ _ userName type bi k =>
+      let toProcess ← pushLocalDecl toProcess fvarId userName type bi k
       mkClosureForAux toProcess
-    | .ldecl _ _ userName type val _ =>
+    | .ldecl _ _ userName type val _ k =>
       let zetaFVarIds ← getZetaFVarIds
       if !zetaFVarIds.contains fvarId then
         /- Non-dependent let-decl. See comment at src/Lean/Meta/Closure.lean -/
-        let toProcess ← pushLocalDecl toProcess fvarId userName type
+        let toProcess ← pushLocalDecl toProcess fvarId userName type .default k
         mkClosureForAux toProcess
       else
         /- Dependent let-decl. -/
         let type ← preprocess type
         let val  ← preprocess val
         modify fun s => { s with
-          newLetDecls   := s.newLetDecls.push <| LocalDecl.ldecl default fvarId userName type val false,
+          newLetDecls   := s.newLetDecls.push <| .ldecl default fvarId userName type val false k,
           /- We don't want to interleave let and lambda declarations in our closure. So, we expand any occurrences of fvarId
              at `newLocalDecls` and `localDecls` -/
           newLocalDecls := s.newLocalDecls.map (·.replaceFVarId fvarId val)
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index d4f4eb28cf..52b63bb7c7 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -313,7 +313,7 @@ structure HeadInfo where
   check : HeadCheck
   /-- compute compatibility of pattern with given head check -/
   onMatch (taken : HeadCheck) : MatchResult
-  /-- actually run the specified head check, with the discriminant bound to `discr` -/
+  /-- actually run the specified head check, with the discriminant bound to `__discr` -/
   doMatch (yes : (newDiscrs : List Term) → TermElabM Term) (no : TermElabM Term) : TermElabM Term
 
 /-- Adapt alternatives that do not introduce new discriminants in `doMatch`, but are covered by those that do so. -/
@@ -342,13 +342,13 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
       -- We assume that atoms are uniquely determined by the node kind and never have to be checked
       unconditionally pure
     else if quoted.isTokenAntiquot then
-      unconditionally (`(let $(quoted.getAntiquotTerm) := discr; $(·)))
+      unconditionally (`(let $(quoted.getAntiquotTerm) := __discr; $(·)))
     else if isAntiquots quoted && !isEscapedAntiquot (getCanonicalAntiquot quoted) then
       -- quotation contains a single antiquotation
       let (ks, pseudoKinds) := antiquotKinds quoted |>.unzip
       let rhsFn := match getAntiquotTerm (getCanonicalAntiquot quoted) with
         | `(_)         => pure
-        | `($id:ident) => fun stx => `(let $id := @TSyntax.mk $(quote ks) discr; $(stx))
+        | `($id:ident) => fun stx => `(let $id := @TSyntax.mk $(quote ks) __discr; $(stx))
         | anti =>         fun _   => throwErrorAt anti "unsupported antiquotation kind in pattern"
       -- Antiquotation kinds like `$id:ident` influence the parser, but also need to be considered by
       -- `match` (but not by quotation terms). For example, `($id:ident) and `($e) are not
@@ -370,7 +370,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
             else uncovered
           | _ => uncovered,
         doMatch := fun yes no => do
-          let cond ← ks.foldlM (fun cond k => `(or $cond (Syntax.isOfKind discr $(quote k)))) (← `(false))
+          let cond ← ks.foldlM (fun cond k => `(or $cond (Syntax.isOfKind __discr $(quote k)))) (← `(false))
           `(cond $cond $(← yes []) $(← no)),
       }
     else if isAntiquotSuffixSplice quoted then throwErrorAt quoted "unexpected antiquotation splice"
@@ -380,9 +380,9 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
       let anti := getAntiquotTerm (getCanonicalAntiquot inner)
       let ks := antiquotKinds inner |>.map (·.1)
       unconditionally fun rhs => match antiquotSuffixSplice? quoted[0] with
-        | `optional => `(let $anti := Option.map (@TSyntax.mk $(quote ks)) (Syntax.getOptional? discr); $rhs)
-        | `many     => `(let $anti := @TSyntaxArray.mk $(quote ks) (Syntax.getArgs discr); $rhs)
-        | `sepBy    => `(let $anti := @TSepArray.mk $(quote ks) $(quote <| getSepFromSplice quoted[0]) (Syntax.getArgs discr); $rhs)
+        | `optional => `(let $anti := Option.map (@TSyntax.mk $(quote ks)) (Syntax.getOptional? __discr); $rhs)
+        | `many     => `(let $anti := @TSyntaxArray.mk $(quote ks) (Syntax.getArgs __discr); $rhs)
+        | `sepBy    => `(let $anti := @TSepArray.mk $(quote ks) $(quote <| getSepFromSplice quoted[0]) (Syntax.getArgs __discr); $rhs)
         | k         => throwErrorAt quoted "invalid antiquotation suffix splice kind '{k}'"
     else if quoted.getArgs.size == 1 && isAntiquotSplice quoted[0] then pure {
       check   := other pat,
@@ -400,12 +400,12 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
         | `optional =>
           let nones := mkArray ids.size (← `(none))
           `(let_delayed yes _ $ids* := $yes;
-            if discr.isNone then yes () $[ $nones]*
-            else match discr with
+            if __discr.isNone then yes () $[ $nones]*
+            else match __discr with
               | `($(mkNullNode contents)) => yes () $[ (some $ids)]*
               | _                         => $no)
         | _ =>
-          let mut discrs ← `(Syntax.getArgs discr)
+          let mut discrs ← `(Syntax.getArgs __discr)
           if k == `sepBy then
             discrs ← `(Array.getSepElems $discrs)
           let tuple ← mkTuple ids
@@ -429,11 +429,11 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
     }
     else if let some idx := quoted.getArgs.findIdx? (fun arg => isAntiquotSuffixSplice arg || isAntiquotSplice arg) then do
       /-
-        patterns of the form `match discr, ... with | `(pat_0 ... pat_(idx-1) $[...]* pat_(idx+1) ...), ...`
+        patterns of the form `match __discr, ... with | `(pat_0 ... pat_(idx-1) $[...]* pat_(idx+1) ...), ...`
         transform to
         ```
-        if discr.getNumArgs >= $quoted.getNumArgs - 1 then
-          match discr[0], ..., discr[idx-1], mkNullNode (discr.getArgs.extract idx (discr.getNumArgs - $numSuffix))), ..., discr[quoted.getNumArgs - 1] with
+        if __discr.getNumArgs >= $quoted.getNumArgs - 1 then
+          match __discr[0], ..., __discr[idx-1], mkNullNode (__discr.getArgs.extract idx (__discr.getNumArgs - $numSuffix))), ..., __discr[quoted.getNumArgs - 1] with
             | `(pat_0), ... `(pat_(idx-1)), `($[...])*, `(pat_(idx+1)), ...
         ```
       -/
@@ -451,11 +451,11 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
             else uncovered
           | _ => uncovered
         doMatch := fun yes no => do
-          let prefixDiscrs ← (List.range idx).mapM (`(Syntax.getArg discr $(quote ·)))
-          let sliceDiscr ← `(mkNullNode (discr.getArgs.extract $(quote idx) (discr.getNumArgs - $(quote numSuffix))))
+          let prefixDiscrs ← (List.range idx).mapM (`(Syntax.getArg __discr $(quote ·)))
+          let sliceDiscr ← `(mkNullNode (__discr.getArgs.extract $(quote idx) (__discr.getNumArgs - $(quote numSuffix))))
           let suffixDiscrs ← (List.range numSuffix).mapM fun i =>
-            `(Syntax.getArg discr (discr.getNumArgs - $(quote (numSuffix - i))))
-          `(ite (GE.ge discr.getNumArgs $(quote (quoted.getNumArgs - 1)))
+            `(Syntax.getArg __discr (__discr.getNumArgs - $(quote (numSuffix - i))))
+          `(ite (GE.ge __discr.getNumArgs $(quote (quoted.getNumArgs - 1)))
               $(← yes (prefixDiscrs ++ sliceDiscr :: suffixDiscrs))
               $(← no))
       }
@@ -490,24 +490,24 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
           | _ => uncovered,
         doMatch := fun yes no => do
           let (cond, newDiscrs) ← if lit then
-            let cond ← `(Syntax.matchesLit discr $(quote kind) $(quote (isLit? kind quoted).get!))
+            let cond ← `(Syntax.matchesLit __discr $(quote kind) $(quote (isLit? kind quoted).get!))
             pure (cond, [])
           else
             let cond ← match kind with
-            | `null => `(Syntax.matchesNull discr $(quote argPats.size))
-            | `ident => `(Syntax.matchesIdent discr $(quote quoted.getId))
-            | _     => `(Syntax.isOfKind discr $(quote kind))
-            let newDiscrs ← (List.range argPats.size).mapM fun i => `(Syntax.getArg discr $(quote i))
+            | `null => `(Syntax.matchesNull __discr $(quote argPats.size))
+            | `ident => `(Syntax.matchesIdent __discr $(quote quoted.getId))
+            | _     => `(Syntax.isOfKind __discr $(quote kind))
+            let newDiscrs ← (List.range argPats.size).mapM fun i => `(Syntax.getArg __discr $(quote i))
             pure (cond, newDiscrs)
           `(ite (Eq $cond true) $(← yes newDiscrs) $(← no))
       }
   else match pat with
     | `(_)              => unconditionally pure
-    | `($id:ident)      => unconditionally (`(let $id := discr; $(·)))
+    | `($id:ident)      => unconditionally (`(let $id := __discr; $(·)))
     | `($id:ident@$pat) => do
       let info ← getHeadInfo (pat::alt.1.tail!, alt.2)
       return { info with onMatch := fun taken => match info.onMatch taken with
-          | covered f exh => covered (fun alt => f alt >>= adaptRhs (`(let $id := discr; $(·)))) exh
+          | covered f exh => covered (fun alt => f alt >>= adaptRhs (`(let $id := __discr; $(·)))) exh
           | r             => r }
     | _               => throwErrorAt pat "match (syntax) : unexpected pattern kind {pat}"
 
@@ -567,16 +567,16 @@ private partial def compileStxMatch (discrs : List Term) (alts : List Alt) : Ter
         let mut yesAlts := yesAlts
         if !undecidedAlts.isEmpty then
           -- group undecided alternatives in a new default case `| discr2, ... => match discr, discr2, ... with ...`
-          let vars ← discrs.mapM fun _ => withFreshMacroScope `(discr)
+          let vars ← discrs.mapM fun _ => withFreshMacroScope `(__discr)
           let pats := List.replicate newDiscrs.length (Unhygienic.run `(_)) ++ vars
           let alts ← undecidedAlts.mapM fun alt => `(matchAltExpr| | $(alt.1.toArray),* => no_error_if_unused% $(alt.2))
-          let rhs  ← `(match discr, $[$(vars.toArray):term],* with $alts:matchAlt*)
+          let rhs  ← `(match __discr, $[$(vars.toArray):term],* with $alts:matchAlt*)
           yesAlts := yesAlts.push (pats, rhs)
         withFreshMacroScope $ compileStxMatch (newDiscrs ++ discrs) yesAlts.toList)
       (no := withFreshMacroScope $ compileStxMatch (discr::discrs) nonExhaustiveAlts.toList)
     for d in floatedLetDecls do
       stx ← `(let_delayed $d:letDecl; $stx)
-    `(let discr := $discr; $stx)
+    `(let __discr := $discr; $stx)
   | _, _ => unreachable!
 
 abbrev IdxSet := HashSet Nat
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 21b2ae0327..cd3c9f72f6 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -17,10 +17,9 @@ def admitGoal (mvarId : MVarId) : MetaM Unit :=
 def goalsToMessageData (goals : List MVarId) : MessageData :=
   MessageData.joinSep (goals.map MessageData.ofGoal) m!"\n\n"
 
-def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit :=
-  withPPShowLetValues <| withPPInaccessibleNames do
-    logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{goalsToMessageData goals}"
-    goals.forM fun mvarId => admitGoal mvarId
+def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit := do
+  logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{goalsToMessageData goals}"
+  goals.forM fun mvarId => admitGoal mvarId
 
 namespace Tactic
 
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 9cba9ec603..1e893be462 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -210,7 +210,7 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
 
 @[builtinTactic traceState] def evalTraceState : Tactic := fun _ => do
   let gs ← getUnsolvedGoals
-  withPPForTacticGoal <| addRawTrace (goalsToMessageData gs)
+  addRawTrace (goalsToMessageData gs)
 
 @[builtinTactic traceMessage] def evalTraceMessage : Tactic := fun stx => do
   match stx[1].isStrLit? with
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index a6916c2207..b020ebff92 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -418,7 +418,7 @@ def withLevelNames (levelNames : List Name) (x : TermElabM α) : TermElabM α :=
   update the mapping `auxDeclToFullName`, and then execute `k`.
 -/
 def withAuxDecl (shortDeclName : Name) (type : Expr) (declName : Name) (k : Expr → TermElabM α) : TermElabM α :=
-  withLocalDecl shortDeclName BinderInfo.auxDecl type fun x =>
+  withLocalDecl shortDeclName .default (kind := .auxDecl) type fun x =>
     withReader (fun ctx => { ctx with auxDeclToFullName := ctx.auxDeclToFullName.insert x.fvarId! declName }) do
       k x
 
@@ -1669,7 +1669,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
     let givenName := givenNameView.review
     let localDecl? := lctx.decls.findSomeRev? fun localDecl? => do
       let localDecl ← localDecl?
-      if localDecl.binderInfo == .auxDecl then
+      if localDecl.isAuxDecl then
         guard (not skipAuxDecl)
         if let some fullDeclName := auxDeclToFullName.find? localDecl.fvarId then
           matchAuxRecDecl? localDecl fullDeclName givenNameView
@@ -1683,7 +1683,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
       -- Search auxDecls again trying an exact match of the given name
       lctx.decls.findSomeRev? fun localDecl? => do
         let localDecl ← localDecl?
-        guard (localDecl.binderInfo == .auxDecl)
+        guard localDecl.isAuxDecl
         matchLocalDecl? localDecl givenName
   let rec loop (n : Name) (projs : List String) :=
     let givenNameView := { view with name := n }
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 6c8bb8bc52..ad67987ddb 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -71,19 +71,6 @@ inductive BinderInfo where
   | strictImplicit
   /-- Local instance binder annotataion, e.g., `[Decidable α]` -/
   | instImplicit
-  /--
-  Auxiliary declarations used by Lean when elaborating recursive declarations.
-  When defining a function such as
-  ```
-       def f : Nat → Nat
-         | 0 => 1
-         | x+1 => (x+1)*f x
-  ```
-  Lean adds a local declaration `f : Nat → Nat` to the local context (`LocalContext`)
-  with `BinderInfo` set to `auxDecl`.
-  This local declaration is later removed by the termination checker.
-  -/
-  | auxDecl
   deriving Inhabited, BEq, Repr
 
 def BinderInfo.hash : BinderInfo → UInt64
@@ -91,7 +78,6 @@ def BinderInfo.hash : BinderInfo → UInt64
   | .implicit       => 1019
   | .strictImplicit => 1087
   | .instImplicit   => 1153
-  | .auxDecl        => 1229
 
 /--
 Return `true` if the given `BinderInfo` does not correspond to an implicit binder annotation
@@ -120,10 +106,6 @@ def BinderInfo.isStrictImplicit : BinderInfo → Bool
   | BinderInfo.strictImplicit => true
   | _                         => false
 
-def BinderInfo.isAuxDecl : BinderInfo → Bool
-  | BinderInfo.auxDecl => true
-  | _                  => false
-
 /-- Expression metadata. Used with the `Expr.mdata` constructor. -/
 abbrev MData := KVMap
 abbrev MData.empty : MData := {}
@@ -176,7 +158,6 @@ def BinderInfo.toUInt64 : BinderInfo → UInt64
   | .implicit       => 1
   | .strictImplicit => 2
   | .instImplicit   => 3
-  | .auxDecl        => 4
 
 def Expr.mkData
     (h : UInt64) (looseBVarRange : Nat := 0) (approxDepth : UInt32 := 0)
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index 6d0e2785f4..21352f5b79 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -9,6 +9,37 @@ import Lean.Hygiene
 
 namespace Lean
 
+/--
+Whether a local declaration should be found by type class search, tactics, etc.
+and shown in the goal display.
+-/
+inductive LocalDeclKind
+  /--
+  Participates fully in type class search, tactics, and is shown even if inaccessible.
+
+  For example: the `x` in `fun x => _` has the default kind.
+  -/
+  | default
+  /--
+  Invisible to type class search or tactics, and hidden in the goal display.
+
+  This kind is used for temporary variables in macros.
+  For example: `return (← foo) + bar` expands to
+  `foo >>= fun __tmp => pure (__tmp + bar)`,
+  where `__tmp` has the `implDetail` kind.
+  -/
+  | implDetail
+  /--
+  Auxiliary local declaration for recursive calls.
+  The behavior is similar to `implDetail`.
+
+  For example: `def foo (n : Nat) : Nat := _` adds the local declaration
+  `foo : Nat → Nat` to allow recursive calls.
+  This declaration has the `auxDecl` kind.
+  -/
+  | auxDecl
+  deriving Inhabited, Repr, DecidableEq, Hashable
+
 /-- A declaration for a LocalContext. This is used to register which free variables are in scope.
 Each declaration comes with
 - `index` the position of the decl in the local context
@@ -18,20 +49,20 @@ Each declaration comes with
 A `cdecl` is a local variable, a `ldecl` is a let-bound free variable with a `value : Expr`.
 -/
 inductive LocalDecl where
-  | cdecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo)
-  | ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep : Bool)
+  | cdecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) (kind : LocalDeclKind)
+  | ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep : Bool) (kind : LocalDeclKind)
   deriving Inhabited
 
 @[export lean_mk_local_decl]
 def mkLocalDeclEx (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) : LocalDecl :=
-  .cdecl index fvarId userName type bi
+  .cdecl index fvarId userName type bi .default
 @[export lean_mk_let_decl]
 def mkLetDeclEx (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : LocalDecl :=
-  .ldecl index fvarId userName type val false
+  .ldecl index fvarId userName type val false .default
 @[export lean_local_decl_binder_info]
 def LocalDecl.binderInfoEx : LocalDecl → BinderInfo
-  | .cdecl _ _ _ _ bi => bi
-  | _                 => BinderInfo.default
+  | .cdecl _ _ _ _ bi _ => bi
+  | _                   => BinderInfo.default
 namespace LocalDecl
 
 def isLet : LocalDecl → Bool
@@ -43,8 +74,8 @@ def index : LocalDecl → Nat
   | ldecl (index := i) .. => i
 
 def setIndex : LocalDecl → Nat → LocalDecl
-  | cdecl _  id n t bi,   idx => cdecl idx id n t bi
-  | ldecl _  id n t v nd, idx => ldecl idx id n t v nd
+  | cdecl _  id n t bi k,   idx => cdecl idx id n t bi k
+  | ldecl _  id n t v nd k, idx => ldecl idx id n t v nd k
 
 def fvarId : LocalDecl → FVarId
   | cdecl (fvarId := id) .. => id
@@ -59,15 +90,25 @@ def type : LocalDecl → Expr
   | ldecl (type := t) .. => t
 
 def setType : LocalDecl → Expr → LocalDecl
-  | cdecl idx id n _ bi, t   => cdecl idx id n t bi
-  | ldecl idx id n _ v nd, t => ldecl idx id n t v nd
+  | cdecl idx id n _ bi k, t   => cdecl idx id n t bi k
+  | ldecl idx id n _ v nd k, t => ldecl idx id n t v nd k
 
 def binderInfo : LocalDecl → BinderInfo
   | cdecl (bi := bi) .. => bi
   | ldecl ..            => BinderInfo.default
 
+def kind : LocalDecl → LocalDeclKind
+  | cdecl .. | ldecl .. => ‹_›
+
 def isAuxDecl (d : LocalDecl) : Bool :=
-  d.binderInfo.isAuxDecl
+  d.kind = .auxDecl
+
+/--
+Is the local declaration an implementation-detail hypothesis
+(including auxiliary declarations)?
+-/
+def isImplementationDetail (d : LocalDecl) : Bool :=
+  d.kind != .default
 
 def value? : LocalDecl → Option Expr
   | cdecl ..              => none
@@ -82,16 +123,16 @@ def hasValue : LocalDecl → Bool
   | ldecl .. => true
 
 def setValue : LocalDecl → Expr → LocalDecl
-  | ldecl idx id n t _ nd, v => ldecl idx id n t v nd
-  | d, _                     => d
+  | ldecl idx id n t _ nd k, v => ldecl idx id n t v nd k
+  | d, _                       => d
 
 def setUserName : LocalDecl → Name → LocalDecl
-  | cdecl index id _ type bi,     userName => cdecl index id userName type bi
-  | ldecl index id _ type val nd, userName => ldecl index id userName type val nd
+  | 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
 
 def setBinderInfo : LocalDecl → BinderInfo → LocalDecl
-  | cdecl index id n type _,  bi => cdecl index id n type bi
-  | ldecl .., _                  => panic! "unexpected let declaration"
+  | cdecl index id n type _ k,  bi => cdecl index id n type bi k
+  | ldecl .., _                    => panic! "unexpected let declaration"
 
 def toExpr (decl : LocalDecl) : Expr :=
   mkFVar decl.fvarId
@@ -129,23 +170,29 @@ def isEmpty (lctx : LocalContext) : Bool :=
 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`. -/
-@[export lean_local_ctx_mk_local_decl]
-def mkLocalDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) : LocalContext :=
+def mkLocalDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) (kind : LocalDeclKind := .default) : LocalContext :=
   match lctx with
   | { fvarIdToDecl := map, decls := decls } =>
     let idx  := decls.size
-    let decl := LocalDecl.cdecl idx fvarId userName type bi
+    let decl := LocalDecl.cdecl idx fvarId userName type bi kind
     { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl }
 
+@[export lean_local_ctx_mk_local_decl]
+private def mkLocalDeclExported (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) (kind : LocalDeclKind := .default) : LocalContext :=
+  mkLocalDecl lctx fvarId userName type bi kind
+
 /-- Low level API for let declarations. Do not use directly.-/
-@[export lean_local_ctx_mk_let_decl]
-def mkLetDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep := false) : 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 } =>
     let idx  := decls.size
-    let decl := LocalDecl.ldecl idx fvarId userName type value nonDep
+    let decl := LocalDecl.ldecl idx fvarId userName type value nonDep kind
     { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl }
 
+@[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
+
 /-- Low level API for adding a local declaration.
 Do not use directly. -/
 def addDecl (lctx : LocalContext) (newDecl : LocalDecl) : LocalContext :=
@@ -343,13 +390,13 @@ def isSubPrefixOf (lctx₁ lctx₂ : LocalContext) (exceptFVars : Array Expr :=
   xs.size.foldRev (init := b) fun i b =>
     let x := xs[i]!
     match lctx.findFVar? x with
-    | some (.cdecl _ _ n ty bi)  =>
+    | some (.cdecl _ _ n ty bi _)  =>
       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) =>
+    | some (.ldecl _ _ n ty val nonDep _) =>
       if b.hasLooseBVar 0 then
         let ty  := ty.abstractRange i xs
         let val := val.abstractRange i xs
@@ -417,8 +464,8 @@ instance [MonadLift m n] [MonadLCtx m] : MonadLCtx n where
 def LocalDecl.replaceFVarId (fvarId : FVarId) (e : Expr) (d : LocalDecl) : LocalDecl :=
   if d.fvarId == fvarId then d
   else match d with
-    | .cdecl idx id n type bi => .cdecl idx id n (type.replaceFVarId fvarId e) bi
-    | .ldecl idx id n type val nonDep => .ldecl idx id n (type.replaceFVarId fvarId e) (val.replaceFVarId fvarId e) nonDep
+    | .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
 
 def LocalContext.replaceFVarId (fvarId : FVarId) (e : Expr) (lctx : LocalContext) : LocalContext :=
   let lctx := lctx.erase fvarId
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index e13bc96cc6..189736c17a 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -169,7 +169,7 @@ def ParamInfo.isStrictImplicit (p : ParamInfo) : Bool :=
   p.binderInfo == BinderInfo.strictImplicit
 
 def ParamInfo.isExplicit (p : ParamInfo) : Bool :=
-  p.binderInfo == BinderInfo.default || p.binderInfo == BinderInfo.auxDecl
+  p.binderInfo == BinderInfo.default
 
 
 /--
@@ -906,10 +906,9 @@ def restoreSynthInstanceCache (cache : SynthInstanceCache) : MetaM Unit :=
 
 private def withNewLocalInstanceImp (className : Name) (fvar : Expr) (k : MetaM α) : MetaM α := do
   let localDecl ← getFVarLocalDecl fvar
-  /- Recall that we use `auxDecl` binderInfo when compiling recursive declarations. -/
-  match localDecl.binderInfo with
-  | .auxDecl => k
-  | _ =>
+  if localDecl.isImplementationDetail then
+    k
+  else
     resettingSynthInstanceCache <|
       withReader
         (fun ctx => { ctx with localInstances := ctx.localInstances.push { className := className, fvar := fvar } })
@@ -1199,23 +1198,24 @@ where
         process mvars bis j b
       | _ => finalize ()
 
-private def withNewFVar (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM α := do
-  match (← isClass? fvarType) with
-  | none   => k fvar
-  | some c => withNewLocalInstance c fvar <| k fvar
+private def withNewFVar (n : Name) (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM α := do
+  if let some c ← isClass? fvarType then
+    withNewLocalInstance c fvar <| k fvar
+  else
+    k fvar
 
-private def withLocalDeclImp (n : Name) (bi : BinderInfo) (type : Expr) (k : Expr → MetaM α) : MetaM α := do
+private def withLocalDeclImp (n : Name) (bi : BinderInfo) (type : Expr) (k : Expr → MetaM α) (kind : LocalDeclKind) : MetaM α := do
   let fvarId ← mkFreshFVarId
   let ctx ← read
-  let lctx := ctx.lctx.mkLocalDecl fvarId n type bi
+  let lctx := ctx.lctx.mkLocalDecl fvarId n type bi kind
   let fvar := mkFVar fvarId
   withReader (fun ctx => { ctx with lctx := lctx }) do
-    withNewFVar fvar type k
+    withNewFVar n fvar type k
 
 /-- Create a free variable `x` with name, binderInfo and type, add it to the context and run in `k`.
 Then revert the context. -/
-def withLocalDecl (name : Name) (bi : BinderInfo) (type : Expr) (k : Expr → n α) : n α :=
-  map1MetaM (fun k => withLocalDeclImp name bi type k) k
+def withLocalDecl (name : Name) (bi : BinderInfo) (type : Expr) (k : Expr → n α) (kind : LocalDeclKind := .default) : n α :=
+  map1MetaM (fun k => withLocalDeclImp name bi type k kind) k
 
 def withLocalDeclD (name : Name) (type : Expr) (k : Expr → n α) : n α :=
   withLocalDecl name BinderInfo.default type k
@@ -1265,32 +1265,32 @@ 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 α) : MetaM α := do
+private def withLetDeclImp (n : Name) (type : Expr) (val : Expr) (k : Expr → MetaM α) (kind : LocalDeclKind) : MetaM α := do
   let fvarId ← mkFreshFVarId
   let ctx ← read
-  let lctx := ctx.lctx.mkLetDecl fvarId n type val
+  let lctx := ctx.lctx.mkLetDecl fvarId n type val (nonDep := false) kind
   let fvar := mkFVar fvarId
   withReader (fun ctx => { ctx with lctx := lctx }) do
-    withNewFVar fvar type k
+    withNewFVar n fvar type k
 
 /--
   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 α) : n α :=
-  map1MetaM (fun k => withLetDeclImp name type val k) k
+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 withLocalInstancesImp (decls : List LocalDecl) (k : MetaM α) : MetaM α := do
-  let localInsts := (← read).localInstances
+  let mut localInsts := (← read).localInstances
   let size := localInsts.size
-  let localInstsNew ← decls.foldlM (init := localInsts) fun localInstsNew decl => do
-    match (← isClass? decl.type) with
-    | none => return localInstsNew
-    | some className => return localInstsNew.push { className, fvar := decl.toExpr }
-  if localInstsNew.size == size then
+  for decl in decls do
+    unless decl.isImplementationDetail do
+      if let some className ← isClass? decl.type then
+        localInsts := localInsts.push { className, fvar := decl.toExpr }
+  if localInsts.size == size then
     k
   else
-    resettingSynthInstanceCache <| withReader (fun ctx => { ctx with localInstances := localInstsNew }) k
+    resettingSynthInstanceCache <| withReader (fun ctx => { ctx with localInstances := localInsts }) k
 
 /-- Register any local instance in `decls` -/
 def withLocalInstances (decls : List LocalDecl) : n α → n α :=
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index ea05f613ae..925a3de957 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -18,7 +18,7 @@ private def ensureType (e : Expr) : MetaM Unit := do
 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 _ _) => do
     let vType ← inferType v
     throwError "invalid let 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 a21ea2fa86..4da4f78f25 100644
--- a/src/Lean/Meta/Closure.lean
+++ b/src/Lean/Meta/Closure.lean
@@ -202,7 +202,7 @@ partial def collectExprAux (e : Expr) : ClosureM Expr := do
     let newFVarId ← mkFreshFVarId
     let userName ← mkNextUserName
     modify fun s => { s with
-      newLocalDeclsForMVars := s.newLocalDeclsForMVars.push $ LocalDecl.cdecl default newFVarId userName type BinderInfo.default,
+      newLocalDeclsForMVars := s.newLocalDeclsForMVars.push $ .cdecl default newFVarId userName type .default .default,
       exprMVarArgs          := s.exprMVarArgs.push e
     }
     return mkFVar newFVarId
@@ -247,18 +247,18 @@ def pushFVarArg (e : Expr) : ClosureM Unit :=
 
 def pushLocalDecl (newFVarId : FVarId) (userName : Name) (type : Expr) (bi := BinderInfo.default) : ClosureM Unit := do
   let type ← collectExpr type
-  modify fun s => { s with newLocalDecls := s.newLocalDecls.push <| LocalDecl.cdecl default newFVarId userName type bi }
+  modify fun s => { s with newLocalDecls := s.newLocalDecls.push <| .cdecl default newFVarId userName type bi .default }
 
 partial def process : ClosureM Unit := do
   match (← pickNextToProcess?) with
   | none => pure ()
   | some ⟨fvarId, newFVarId⟩ =>
     match (← fvarId.getDecl) with
-    | .cdecl _ _ userName type bi =>
+    | .cdecl _ _ userName type bi _ =>
       pushLocalDecl newFVarId userName type bi
       pushFVarArg (mkFVar fvarId)
       process
-    | .ldecl _ _ userName type val _ =>
+    | .ldecl _ _ userName type val _ _ =>
       let zetaFVarIds ← getZetaFVarIds
       if !zetaFVarIds.contains fvarId then
         /- Non-dependent let-decl
@@ -275,7 +275,7 @@ partial def process : ClosureM Unit := do
         /- Dependent let-decl -/
         let type ← collectExpr type
         let val  ← collectExpr val
-        modify fun s => { s with newLetDecls := s.newLetDecls.push <| LocalDecl.ldecl default newFVarId userName type val false }
+        modify fun s => { s with newLetDecls := s.newLetDecls.push <| .ldecl default newFVarId userName type val false .default }
         /- We don't want to interleave let and lambda declarations in our closure. So, we expand any occurrences of newFVarId
            at `newLocalDecls` -/
         modify fun s => { s with newLocalDecls := s.newLocalDecls.map (·.replaceFVarId newFVarId val) }
@@ -287,13 +287,13 @@ partial def process : ClosureM Unit := do
   decls.size.foldRev (init := b) fun i b =>
     let decl := decls[i]!
     match decl with
-    | LocalDecl.cdecl _ _ n ty bi  =>
+    | .cdecl _ _ n ty bi _ =>
       let ty := ty.abstractRange i xs
       if isLambda then
         Lean.mkLambda n bi ty b
       else
         Lean.mkForall n bi ty b
-    | LocalDecl.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
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index e9bd6efbef..53af4b8688 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -233,7 +233,7 @@ Try to solve the problem by using the first alternative whose pending constraint
 -/
 private def processLeaf (p : Problem) : StateRefT State MetaM Unit :=
   p.mvarId.withContext do
-    withPPForTacticGoal do trace[Meta.Match.match] "local context at processLeaf:\n{(← mkFreshTypeMVar).mvarId!}"
+    trace[Meta.Match.match] "local context at processLeaf:\n{(← mkFreshTypeMVar).mvarId!}"
     go p.alts
 where
   go (alts : List Alt) : StateRefT State MetaM Unit := do
diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean
index 039cf6278a..d19e4673b0 100644
--- a/src/Lean/Meta/PPGoal.lean
+++ b/src/Lean/Meta/PPGoal.lean
@@ -13,182 +13,24 @@ register_builtin_option pp.auxDecls : Bool := {
   descr    := "display auxiliary declarations used to compile recursive functions"
 }
 
-register_builtin_option pp.inaccessibleNames : Bool := {
+register_builtin_option pp.implementationDetailHyps : Bool := {
   defValue := false
   group    := "pp"
+  descr    := "display implementation detail hypotheses in the local context"
+}
+
+register_builtin_option pp.inaccessibleNames : Bool := {
+  defValue := true
+  group    := "pp"
   descr    := "display inaccessible declarations in the local context"
 }
 
 register_builtin_option pp.showLetValues : Bool := {
-  defValue := false
+  defValue := true
   group    := "pp"
   descr    := "display let-declaration values in the info view"
 }
 
-def withPPInaccessibleNamesImp (flag : Bool) (x : MetaM α) : MetaM α :=
-  withTheReader Core.Context (fun ctx => { ctx with options := pp.inaccessibleNames.setIfNotSet ctx.options flag }) x
-
-def withPPInaccessibleNames [MonadControlT MetaM m] [Monad m] (x : m α) (flag := true) : m α :=
-  mapMetaM (withPPInaccessibleNamesImp flag) x
-
-def withPPShowLetValuesImp (flag : Bool) (x : MetaM α) : MetaM α :=
-  withTheReader Core.Context (fun ctx => { ctx with options := pp.showLetValues.setIfNotSet ctx.options flag }) x
-
-def withPPShowLetValues [MonadControlT MetaM m] [Monad m] (x : m α) (flag := true) : m α :=
-  mapMetaM (withPPShowLetValuesImp flag) x
-
-/--
-Set pretty-printing options (`pp.showLetValues = true` and `pp.inaccessibleNames = true`) for visualizing goals.
--/
-def withPPForTacticGoal [MonadControlT MetaM m] [Monad m] (x : m α) : m α :=
-  withPPShowLetValues <| withPPInaccessibleNames x
-
-namespace ToHide
-
-structure State where
-  /-- FVarIds of Propostions with inaccessible names but containing only visible names. We show only their types -/
-  hiddenInaccessibleProp : FVarIdSet := {}
-  /-- FVarIds with inaccessible names, but not in hiddenInaccessibleProp -/
-  hiddenInaccessible     : FVarIdSet := {}
-  modified               : Bool := false
-
-structure Context where
-  /--
-   If true we make a declaration "visible" if it has visible backward dependencies.
-   Remark: recall that for the `Prop` case, the declaration is moved to `hiddenInaccessibleProp`
-   -/
-  backwardDeps  : Bool
-  goalTarget    : Expr
-  showLetValues : Bool
-
-abbrev M := ReaderT Context $ StateRefT State MetaM
-
-/-- Return true if `fvarId` is marked as an hidden inaccessible or inaccessible proposition -/
-def isMarked (fvarId : FVarId) : M Bool := do
-  let s ← get
-  return s.hiddenInaccessible.contains fvarId || s.hiddenInaccessibleProp.contains fvarId
-
-/-- If `fvarId` isMarked, then unmark it. -/
-def unmark (fvarId : FVarId) : M Unit := do
-  modify fun s => {
-    hiddenInaccessible     := s.hiddenInaccessible.erase fvarId
-    hiddenInaccessibleProp := s.hiddenInaccessibleProp.erase fvarId
-    modified               := true
-  }
-
-def moveToHiddeProp (fvarId : FVarId) : M Unit := do
-  modify fun s => {
-    hiddenInaccessible     := s.hiddenInaccessible.erase fvarId
-    hiddenInaccessibleProp := s.hiddenInaccessibleProp.insert fvarId
-    modified               := true
-  }
-
-/-- Similar to `findLocalDeclDependsOn`, but it only considers `let`-values if `showLetValues = true` -/
-private def findDeps (localDecl : LocalDecl) (f : FVarId → Bool) : M Bool := do
-  if (← read).showLetValues then
-    findLocalDeclDependsOn localDecl f
-  else
-    findExprDependsOn localDecl.type f
-
-/-- Return true if the given local declaration has a "visible dependency", that is, it contains
-   a free variable that is `hiddenInaccessible`
-
-   Recall that hiddenInaccessibleProps are visible, only their names are hidden -/
-def hasVisibleDep (localDecl : LocalDecl) : M Bool := do
-  let s ← get
-  findDeps localDecl (!s.hiddenInaccessible.contains ·)
-
-/-- Return true if the given local declaration has a "nonvisible dependency", that is, it contains
-   a free variable that is `hiddenInaccessible` or `hiddenInaccessibleProp` -/
-def hasInaccessibleNameDep (localDecl : LocalDecl) : M Bool := do
-  let s ← get
-  findDeps localDecl fun fvarId =>
-    s.hiddenInaccessible.contains fvarId || s.hiddenInaccessibleProp.contains fvarId
-
-/-- If `e` is visible, then any inaccessible in `e` marked as hidden should be unmarked. -/
-partial def visitVisibleExpr (e : Expr) : M Unit := do
-  visit (← instantiateMVars e) |>.run
-where
-  visit (e : Expr) : MonadCacheT Expr Unit M Unit := do
-    if e.hasFVar then
-      checkCache e fun _ => do
-        match e with
-        | .forallE _ d b _   => visit d; visit b
-        | .lam _ d b _       => visit d; visit b
-        | .letE _ t v b _    => visit t; visit v; visit b
-        | .app f a           => visit f; visit a
-        | .mdata _ b         => visit b
-        | .proj _ _ b        => visit b
-        | .fvar fvarId       => if (← isMarked fvarId) then unmark fvarId
-        | _                  => return ()
-
-def fixpointStep : M Unit := do
-  visitVisibleExpr (← read).goalTarget -- The goal target is a visible forward dependency
-  (← getLCtx).forM fun localDecl => do
-    let fvarId := localDecl.fvarId
-    if (← get).hiddenInaccessible.contains fvarId then
-      if (← read).backwardDeps then
-        if (← hasVisibleDep localDecl) then
-          /- localDecl is marked to be hidden, but it has a (backward) visible dependency. -/
-          unmark fvarId
-        if (← isProp localDecl.type) then
-          unless (← hasInaccessibleNameDep localDecl) do
-            moveToHiddeProp fvarId
-    else
-      visitVisibleExpr localDecl.type
-      if (← read).showLetValues then
-        let some value := localDecl.value? | return ()
-        visitVisibleExpr value
-
-partial def fixpoint : M Unit := do
-  modify fun s => { s with modified := false }
-  fixpointStep
-  if (← get).modified then
-    fixpoint
-
-/--
-  Construct initial `FVarIdSet` containting free variables ids that have inaccessible user names.
--/
-private def getInitialHiddenInaccessible (propOnly : Bool) : MetaM FVarIdSet := do
-  let mut r := {}
-  for localDecl in (← getLCtx) do
-    if localDecl.userName.isInaccessibleUserName then
-      if (← pure !propOnly <||> isProp localDecl.type) then
-        r := r.insert localDecl.fvarId
-  return r
-
-/--
-If `pp.inaccessibleNames == false`, then collect two sets of `FVarId`s : `hiddenInaccessible` and `hiddenInaccessibleProp`
-1- `hiddenInaccessible` contains `FVarId`s of free variables with inaccessible names that
-    a) are not propositions or
-    b) are propositions containing "visible" names.
-2- `hiddenInaccessibleProp` contains `FVarId`s of free variables with inaccessible names that are propositions
-   containing "visible" names.
-Both sets do not contain `FVarId`s that contain visible backward or forward dependencies.
-The `goalTarget` counts as a forward dependency.
-
-We say a name is visible if it is a free variable with FVarId not in `hiddenInaccessible` nor `hiddenInaccessibleProp`
-
-For propositions in `hiddenInaccessibleProp`, we show only their types when displaying a goal.
-
-Remark: when `pp.inaccessibleNames == true`, we still compute `hiddenInaccessibleProp` to prevent the
-goal from being littered with irrelevant names.
-
--/
-def collect (goalTarget : Expr) : MetaM (FVarIdSet × FVarIdSet) := do
-  let showLetValues := pp.showLetValues.get (← getOptions)
-  if pp.inaccessibleNames.get (← getOptions) then
-    -- If `pp.inaccessibleNames == true`, we still must compute `hiddenInaccessibleProp`.
-    let hiddenInaccessible ← getInitialHiddenInaccessible (propOnly := true)
-    let (_, s) ← fixpoint.run { backwardDeps := false, goalTarget, showLetValues } |>.run { hiddenInaccessible }
-    return ({}, s.hiddenInaccessible)
-  else
-    let hiddenInaccessible ← getInitialHiddenInaccessible (propOnly := false)
-    let (_, s) ← fixpoint.run { backwardDeps := true, goalTarget, showLetValues } |>.run { hiddenInaccessible }
-    return (s.hiddenInaccessible, s.hiddenInaccessibleProp)
-
-end ToHide
-
 private def addLine (fmt : Format) : Format :=
   if fmt.isNil then fmt else fmt ++ Format.line
 
@@ -206,10 +48,10 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
     let indent         := 2 -- Use option
     let showLetValues  := pp.showLetValues.get (← getOptions)
     let ppAuxDecls     := pp.auxDecls.get (← getOptions)
+    let ppImplDetailHyps := pp.implementationDetailHyps.get (← getOptions)
     let lctx           := mvarDecl.lctx
     let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
     withLCtx lctx mvarDecl.localInstances do
-      let (hidden, hiddenProp) ← ToHide.collect mvarDecl.type
       -- The followint two `let rec`s are being used to control the generated code size.
       -- Then should be remove after we rewrite the compiler in Lean
       let rec pushPending (ids : List Name) (type? : Option Expr) (fmt : Format) : MetaM Format := do
@@ -223,38 +65,30 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
             let typeFmt ← ppExpr type
             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
-        if hiddenProp.contains localDecl.fvarId then
+        match localDecl with
+        | .cdecl _ _ varName type _ _ =>
+          let varName := varName.simpMacroScopes
+          let type ← instantiateMVars type
+          if prevType? == none || prevType? == some type then
+            return (varName :: varNames, some type, fmt)
+          else do
+            let fmt ← pushPending varNames prevType? fmt
+            return ([varName], some type, fmt)
+        | .ldecl _ _ varName type val _ _ => do
+          let varName := varName.simpMacroScopes
           let fmt ← pushPending varNames prevType? fmt
           let fmt  := addLine fmt
-          let type ← instantiateMVars localDecl.type
+          let type ← instantiateMVars type
           let typeFmt ← ppExpr type
-          let fmt  := fmt ++ ": " ++ typeFmt
+          let mut fmtElem  := format varName ++ " : " ++ typeFmt
+          if showLetValues then
+            let val ← instantiateMVars val
+            let valFmt ← ppExpr val
+            fmtElem := fmtElem ++ " :=" ++ Format.nest indent (Format.line ++ valFmt)
+          let fmt := fmt ++ fmtElem.group
           return ([], none, fmt)
-        else
-          match localDecl with
-          | .cdecl _ _ varName type _   =>
-            let varName := varName.simpMacroScopes
-            let type ← instantiateMVars type
-            if prevType? == none || prevType? == some type then
-              return (varName :: varNames, some type, fmt)
-            else do
-              let fmt ← pushPending varNames prevType? fmt
-              return ([varName], some type, fmt)
-          | .ldecl _ _ varName type val _ => do
-            let varName := varName.simpMacroScopes
-            let fmt ← pushPending varNames prevType? fmt
-            let fmt  := addLine fmt
-            let type ← instantiateMVars type
-            let typeFmt ← ppExpr type
-            let mut fmtElem  := format varName ++ " : " ++ typeFmt
-            if showLetValues then
-              let val ← instantiateMVars val
-              let valFmt ← ppExpr val
-              fmtElem := fmtElem ++ " :=" ++ Format.nest indent (Format.line ++ valFmt)
-            let fmt := fmt ++ fmtElem.group
-            return ([], none, fmt)
       let (varNames, type?, fmt) ← lctx.foldlM (init := ([], none, Format.nil)) fun (varNames, prevType?, fmt) (localDecl : LocalDecl) =>
-         if !ppAuxDecls && localDecl.isAuxDecl || hidden.contains localDecl.fvarId then
+         if !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail then
            return (varNames, prevType?, fmt)
          else
            ppVars varNames prevType? fmt localDecl
diff --git a/src/Lean/Meta/Tactic/Assumption.lean b/src/Lean/Meta/Tactic/Assumption.lean
index 27ccfa3e0b..83f275a300 100644
--- a/src/Lean/Meta/Tactic/Assumption.lean
+++ b/src/Lean/Meta/Tactic/Assumption.lean
@@ -10,7 +10,7 @@ namespace Lean.Meta
 /-- Return a local declaration whose type is definitionally equal to `type`. -/
 def findLocalDeclWithType? (type : Expr) : MetaM (Option FVarId) := do
   (← getLCtx).findDeclRevM? fun localDecl => do
-    if localDecl.isAuxDecl then
+    if localDecl.isImplementationDetail then
       return none
     else if (← isDefEq type localDecl.type) then
       return some localDecl.fvarId
diff --git a/src/Lean/Meta/Tactic/Contradiction.lean b/src/Lean/Meta/Tactic/Contradiction.lean
index cd01f8c991..607f1e9d95 100644
--- a/src/Lean/Meta/Tactic/Contradiction.lean
+++ b/src/Lean/Meta/Tactic/Contradiction.lean
@@ -155,7 +155,7 @@ def _root_.Lean.MVarId.contradictionCore (mvarId : MVarId) (config : Contradicti
     if (← nestedFalseElim mvarId) then
       return true
     for localDecl in (← getLCtx) do
-      unless localDecl.isAuxDecl do
+      unless localDecl.isImplementationDetail do
         -- (h : ¬ p) (h' : p)
         if let some p ← matchNot? localDecl.type then
           if let some pFVarId ← findLocalDeclWithType? p then
diff --git a/src/Lean/Meta/Tactic/FVarSubst.lean b/src/Lean/Meta/Tactic/FVarSubst.lean
index ebc51dac71..5d1b3ffe47 100644
--- a/src/Lean/Meta/Tactic/FVarSubst.lean
+++ b/src/Lean/Meta/Tactic/FVarSubst.lean
@@ -67,8 +67,8 @@ end FVarSubst
 end Meta
 
 def LocalDecl.applyFVarSubst (s : Meta.FVarSubst) : LocalDecl → LocalDecl
-  | LocalDecl.cdecl i id n t bi   => LocalDecl.cdecl i id n (s.apply t) bi
-  | LocalDecl.ldecl i id n t v nd => LocalDecl.ldecl i id n (s.apply t) (s.apply v) nd
+  | LocalDecl.cdecl i id n t bi k   => LocalDecl.cdecl i id n (s.apply t) bi k
+  | LocalDecl.ldecl i id n t v nd k => LocalDecl.ldecl i id n (s.apply t) (s.apply v) nd k
 
 abbrev Expr.applyFVarSubst (s : Meta.FVarSubst) (e : Expr) : Expr :=
   s.apply e
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 3aa63363d1..1125a39bf7 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -738,7 +738,7 @@ abbrev Discharge := Expr → SimpM (Option Expr)
 
 def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
   (← getLCtx).findDeclRevM? fun localDecl => do
-    if localDecl.isAuxDecl then
+    if localDecl.isImplementationDetail then
       return none
     else if (← isDefEq e localDecl.type) then
       return some localDecl.toExpr
diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean
index c01da416d4..fdb5255e52 100644
--- a/src/Lean/Meta/Tactic/Subst.lean
+++ b/src/Lean/Meta/Tactic/Subst.lean
@@ -183,7 +183,7 @@ where
       throwTacticEx `subst mvarId m!"variable '{mkFVar h}' is a let-declaration"
     let lctx ← getLCtx
     let some (fvarId, symm) ← lctx.findDeclM? fun localDecl => do
-       if localDecl.isAuxDecl then
+       if localDecl.isImplementationDetail then
          return none
        else
          match (← matchEq? localDecl.type) with
diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
index d7cdc69380..278cbf4381 100644
--- a/src/Lean/Meta/Tactic/Util.lean
+++ b/src/Lean/Meta/Tactic/Util.lean
@@ -36,11 +36,10 @@ def mkFreshExprSyntheticOpaqueMVar (type : Expr) (tag : Name := Name.anonymous)
   mkFreshExprMVar type MetavarKind.syntheticOpaque tag
 
 def throwTacticEx (tacticName : Name) (mvarId : MVarId) (msg : MessageData) : MetaM α :=
-  withPPForTacticGoal do
-    if msg.isEmpty then
-      throwError "tactic '{tacticName}' failed\n{mvarId}"
-    else
-      throwError "tactic '{tacticName}' failed, {msg}\n{mvarId}"
+  if msg.isEmpty then
+    throwError "tactic '{tacticName}' failed\n{mvarId}"
+  else
+    throwError "tactic '{tacticName}' failed, {msg}\n{mvarId}"
 
 def throwNestedTacticEx {α} (tacticName : Name) (ex : Exception) : MetaM α := do
   throwError "tactic '{tacticName}' failed, nested error:\n{ex.toMessageData}"
@@ -106,7 +105,7 @@ def _root_.Lean.MVarId.getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId
   mvarId.withContext do
     let mut candidates : FVarIdHashSet := {}
     for localDecl in (← getLCtx) do
-      unless localDecl.isAuxDecl do
+      unless localDecl.isImplementationDetail do
         candidates ← removeDeps localDecl.type candidates
         match localDecl.value? with
         | none => pure ()
@@ -152,7 +151,7 @@ def ensureAtMostOne (mvarIds : List MVarId) (msg : MessageData := "unexpected nu
 def getPropHyps : MetaM (Array FVarId) := do
   let mut result := #[]
   for localDecl in (← getLCtx) do
-    unless localDecl.isAuxDecl do
+    unless localDecl.isImplementationDetail do
       if (← isProp localDecl.type) then
         result := result.push localDecl.fvarId
   return result
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index bb77662da1..126475c775 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -598,13 +598,13 @@ def instantiateMVars [Monad m] [MonadMCtx m] (e : Expr) : m Expr := do
 def instantiateLCtxMVars [Monad m] [MonadMCtx m] (lctx : LocalContext) : m LocalContext :=
   lctx.foldlM (init := {}) fun lctx ldecl => do
      match ldecl with
-     | .cdecl _ fvarId userName type bi =>
+     | .cdecl _ fvarId userName type bi k =>
        let type ← instantiateMVars type
-       return lctx.mkLocalDecl fvarId userName type bi
-     | .ldecl _ fvarId userName type value nonDep =>
+       return lctx.mkLocalDecl fvarId userName type bi k
+     | .ldecl _ fvarId userName type value nonDep k =>
        let type ← instantiateMVars type
        let value ← instantiateMVars value
-       return lctx.mkLetDecl fvarId userName type value nonDep
+       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
@@ -614,10 +614,10 @@ def instantiateMVarDeclMVars [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Unit
 
 def instantiateLocalDeclMVars [Monad m] [MonadMCtx m] (localDecl : LocalDecl) : m LocalDecl := do
   match localDecl with
-  | .cdecl idx id n type bi  =>
-    return .cdecl idx id n (← instantiateMVars type) bi
-  | .ldecl idx id n type val nonDep =>
-    return .ldecl idx id n (← instantiateMVars type) (← instantiateMVars val) nonDep
+  | .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
 
 namespace DependsOn
 
@@ -1021,11 +1021,11 @@ mutual
       let x := xs[i]!
       if x.isFVar then
         match lctx.getFVar! x with
-        | LocalDecl.cdecl _ _ n type bi =>
+        | LocalDecl.cdecl _ _ n type bi _ =>
           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 _ _ n type value nonDep _ =>
           let type := type.headBeta
           let type  ← abstractRangeAux xs i type
           let value ← abstractRangeAux xs i value
@@ -1150,7 +1150,7 @@ partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr)
       let x := xs[i]!
       if x.isFVar then
         match lctx.getFVar! x with
-        | LocalDecl.cdecl _ _ n type bi =>
+        | LocalDecl.cdecl _ _ n type bi _ =>
           if !usedOnly || e.hasLooseBVar 0 then
             let type := type.headBeta;
             let type ← abstractRange xs i type
@@ -1160,7 +1160,7 @@ partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr)
               return (Lean.mkForall n bi type e, num + 1)
           else
             return (e.lowerLooseBVars 1 1, num)
-        | LocalDecl.ldecl _ _ n type value nonDep =>
+        | LocalDecl.ldecl _ _ n type value nonDep _ =>
           if !usedLetOnly || e.hasLooseBVar 0 then
             let type  ← abstractRange xs i type
             let value ← abstractRange xs i value
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 9d709ae6e0..683d02dca9 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -512,7 +512,6 @@ def delabLam : Delab :=
           pure curNames.back  -- here `curNames.size == 1`
       let group ← match e.binderInfo, ppTypes with
         | BinderInfo.default,        _      => defaultCase ()
-        | BinderInfo.auxDecl,        _      => defaultCase ()
         | BinderInfo.implicit,       true   => `(funBinder| {$curNames* : $stxT})
         | BinderInfo.implicit,       false  => `(funBinder| {$curNames*})
         | BinderInfo.strictImplicit, true   => `(funBinder| ⦃$curNames* : $stxT⦄)
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 3b1134f7e6..ee89be8e30 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -587,7 +587,6 @@ mutual
               | _                 => annotateNamedArg (← mvarName mvars[i]!)
             else annotateBool `pp.analysis.skip; provided := false
             modify fun s => { s with provideds := s.provideds.set! i provided }
-          | BinderInfo.auxDecl => pure ()
           if (← get).provideds[i]! then withKnowing (not (← typeUnknown mvars[i]!)) true analyze
           tryUnify mvars[i]! args[i]!
 
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 7de5b44ecb..079fb0c10c 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -169,7 +169,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
           -- compute the interactive goals
           let goals ← ci.runMetaM {} (do
             let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
-            let goals ← goals.mapM (fun g => Meta.withPPForTacticGoal (Widget.goalToInteractive g))
+            let goals ← goals.mapM Widget.goalToInteractive
             return {goals}
           )
           -- compute the goal diff
diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean
index 45b63ec1c4..aa6fabe948 100644
--- a/src/Lean/Widget/InteractiveGoal.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -137,9 +137,9 @@ open Meta in
 /-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
 def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
   let ppAuxDecls := pp.auxDecls.get (← getOptions)
+  let ppImplDetailHyps := pp.implementationDetailHyps.get (← getOptions)
   let showLetValues := pp.showLetValues.get (← getOptions)
   withGoalCtx mvarId fun lctx mvarDecl => do
-    let (hidden, hiddenProp) ← ToHide.collect mvarDecl.type
     let pushPending (ids : Array (Name × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
         : MetaM (Array InteractiveHypothesisBundle) :=
       if ids.isEmpty then
@@ -152,36 +152,27 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
     let mut prevType? : Option Expr := none
     let mut hyps : Array InteractiveHypothesisBundle := #[]
     for localDecl in lctx do
-      if !ppAuxDecls && localDecl.isAuxDecl || hidden.contains localDecl.fvarId then
+      if !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail then
         continue
       else
-        if hiddenProp.contains localDecl.fvarId then
-          -- localDecl has an inaccessible name and
-          -- is a proposition containing "visible" names.
-          let type ← instantiateMVars localDecl.type
+        match localDecl with
+        | LocalDecl.cdecl _index fvarId varName type _ _ =>
+          let varName := varName.simpMacroScopes
+          let type ← instantiateMVars type
+          if prevType? == none || prevType? == some type then
+            varNames := varNames.push (varName, fvarId)
+          else
+            hyps ← pushPending varNames prevType? hyps
+            varNames := #[(varName, fvarId)]
+          prevType? := some type
+        | LocalDecl.ldecl _index fvarId varName type val _ _ => do
+          let varName := varName.simpMacroScopes
           hyps ← pushPending varNames prevType? hyps
-          hyps ← addInteractiveHypothesisBundle hyps #[(Name.anonymous, localDecl.fvarId)] type
+          let type ← instantiateMVars type
+          let val? ← if showLetValues then pure (some (← instantiateMVars val)) else pure none
+          hyps ← addInteractiveHypothesisBundle hyps #[(varName, fvarId)] type val?
           varNames := #[]
           prevType? := none
-        else
-          match localDecl with
-          | LocalDecl.cdecl _index fvarId varName type _   =>
-            let varName := varName.simpMacroScopes
-            let type ← instantiateMVars type
-            if prevType? == none || prevType? == some type then
-              varNames := varNames.push (varName, fvarId)
-            else
-              hyps ← pushPending varNames prevType? hyps
-              varNames := #[(varName, fvarId)]
-            prevType? := some type
-          | LocalDecl.ldecl _index fvarId varName type val _ => do
-            let varName := varName.simpMacroScopes
-            hyps ← pushPending varNames prevType? hyps
-            let type ← instantiateMVars type
-            let val? ← if showLetValues then pure (some (← instantiateMVars val)) else pure none
-            hyps ← addInteractiveHypothesisBundle hyps #[(varName, fvarId)] type val?
-            varNames := #[]
-            prevType? := none
     hyps ← pushPending varNames prevType? hyps
     let goalTp ← instantiateMVars mvarDecl.type
     let goalFmt ← ppExprTagged goalTp
diff --git a/src/lake b/src/lake
index cabb1223b0..8d98d5616b 160000
--- a/src/lake
+++ b/src/lake
@@ -1 +1 @@
-Subproject commit cabb1223b02c6bf799bf99b4329e6b666e2bbc9a
+Subproject commit 8d98d5616bacc49700f63c78c30cefd00e040686
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index 6730492995..2bae236ab4 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -237,7 +237,7 @@ bool is_join_point_name(name const & n) {
 }
 
 bool is_pseudo_do_join_point_name(name const & n) {
-    return !n.is_atomic() && n.is_string() && strncmp(n.get_string().data(), "_do_jp", 6) == 0;
+    return !n.is_atomic() && n.is_string() && strncmp(n.get_string().data(), "__do_jp", 6) == 0;
 }
 
 bool has_fvar(expr const & e, expr const & fvar) {
diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h
index e5d358c442..bb7e457884 100644
--- a/src/library/compiler/util.h
+++ b/src/library/compiler/util.h
@@ -93,7 +93,7 @@ expr mk_lc_unreachable(type_checker::state & s, local_ctx const & lctx, expr con
 inline name mk_join_point_name(name const & n) { return name(n, "_join"); }
 bool is_join_point_name(name const & n);
 /* Pseudo "do" joinpoints are used to implement a temporary HACK. See `visit_let` method at `lcnf.cpp` */
-inline name mk_pseudo_do_join_point_name(name const & n) { return name(n, "_do_jp"); }
+inline name mk_pseudo_do_join_point_name(name const & n) { return name(n, "__do_jp"); }
 bool is_pseudo_do_join_point_name(name const & n);
 
 /* Create an auxiliary names for a declaration that saves the result of the compilation
diff --git a/tests/lean/run/frontend_meeting_2022_09_13.lean b/tests/lean/run/frontend_meeting_2022_09_13.lean
index b8074fcb50..4f217134d1 100644
--- a/tests/lean/run/frontend_meeting_2022_09_13.lean
+++ b/tests/lean/run/frontend_meeting_2022_09_13.lean
@@ -82,7 +82,7 @@ elab "seq" s:tacticSeq : tactic => do
   let tacs := getTactics s
   for tac in tacs do
     let gs ← getUnsolvedGoals
-    withRef tac <| Meta.withPPForTacticGoal <| addRawTrace (goalsToMessageData gs)
+    withRef tac <| addRawTrace (goalsToMessageData gs)
     evalTactic tac
 
 example (h : x = y) : 0 + x = y := by