diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 405f60fe1c..c7678b81fc 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -313,20 +313,22 @@ macro_rules
     `($mods:declModifiers class $id $params* $[: $ty:term]? extends $[$parents:term],*
       attribute [instance] $ctor)
 
+-- TODO(kmill): Delete after stage0 update
 macro_rules
   | `(haveI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) =>
-    `(haveI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body)
+    `(haveI $(HygieneInfo.mkIdent hy `this (canonical := true)):ident $bs* $[: $ty]? := $val; $body)
   | `(haveI _ $bs* := $val; $body) => `(haveI x $bs* : _ := $val; $body)
   | `(haveI _ $bs* : $ty := $val; $body) => `(haveI x $bs* : $ty := $val; $body)
-  | `(haveI $x:ident $bs* := $val; $body) => `(haveI $x $bs* : _ := $val; $body)
+  | `(haveI $x:ident $bs* := $val; $body) => `(haveI $x:ident $bs* : _ := $val; $body)
   | `(haveI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab
 
+-- TODO(kmill): Delete after stage0 update
 macro_rules
   | `(letI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) =>
-    `(letI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body)
+    `(letI $(HygieneInfo.mkIdent hy `this (canonical := true)):ident $bs* $[: $ty]? := $val; $body)
   | `(letI _ $bs* := $val; $body) => `(letI x $bs* : _ := $val; $body)
   | `(letI _ $bs* : $ty := $val; $body) => `(letI x $bs* : $ty := $val; $body)
-  | `(letI $x:ident $bs* := $val; $body) => `(letI $x $bs* : _ := $val; $body)
+  | `(letI $x:ident $bs* := $val; $body) => `(letI $x:ident $bs* : _ := $val; $body)
   | `(letI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab
 
 
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index e483587e68..64b219f3cc 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -819,6 +819,12 @@ The `have` tactic is for adding hypotheses to the local context of the main goal
   hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
 -/
 syntax "have " haveDecl : tactic
+-- TODO(kmill) Remove after stage0 update
+macro_rules (kind := Lean.Parser.Tactic.tacticHave_)
+  | stx =>
+    let letDecl := stx.getArg 1
+    `(tactic| refine_lift have $(⟨letDecl⟩):haveDecl; ?_)
+/-
 macro_rules
   -- special case: when given a nested `by` block, move it outside of the `refine` to enable
   -- incrementality
@@ -849,6 +855,7 @@ macro_rules
       refine no_implicit_lambda% (have $id:haveId $bs* : $type := ?body; ?_)
       $tac)
   | `(tactic| have $d:haveDecl) => `(tactic| refine_lift have $d:haveDecl; ?_)
+-/
 
 /--
 Given a main goal `ctx ⊢ t`, `suffices h : t' from e` replaces the main goal with `ctx ⊢ t'`,
@@ -879,7 +886,7 @@ macro_rules
 /-- Similar to `refine_lift`, but using `refine'` -/
 macro "refine_lift' " e:term : tactic => `(tactic| focus (refine' no_implicit_lambda% $e; rotate_right))
 /-- Similar to `have`, but using `refine'` -/
-macro "have' " d:haveDecl : tactic => `(tactic| refine_lift' have $d:haveDecl; ?_)
+macro "have' " d:haveDecl : tactic => `(tactic| refine_lift' have $(⟨d⟩):haveDecl; ?_)
 set_option linter.missingDocs false in -- OK, because `tactic_alt` causes inheritance of docs
 macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x:ident : _ := $p)
 attribute [tactic_alt tacticHave'_] «tacticHave'_:=_»
@@ -1271,10 +1278,10 @@ syntax (name := substEqs) "subst_eqs" : tactic
 syntax (name := runTac) "run_tac " doSeq : tactic
 
 /-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/
-macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_)
+macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $(⟨d⟩):haveDecl; ?_)
 
 /-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
-macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_)
+macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $(⟨d⟩):haveDecl; ?_)
 
 /--
 Configuration for the `decide` tactic family.
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 46e4b43175..4b8959bdef 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -687,13 +687,56 @@ open Lean.Elab.Term.Quotation in
       mkLambdaFVars xs e
   | _ => throwUnsupportedSyntax
 
+/--
+Configuration for `let` elaboration.
+-/
+structure LetConfig where
+  /-- Elaborate as a nondependent `let` (a `have`). -/
+  nondep : Bool := false
+  /-- Eliminate the `let` if it is unused by the body. -/
+  usedOnly : Bool := false
+  /-- Zeta reduces (inlines) the `let`. -/
+  zeta : Bool := false
+  /-- Postpone elaboration of the value until after the body is elaborated. -/
+  postponeValue : Bool := false
+  /-- For `let x := v; b`, adds `eq : x = v` to the context. -/
+  eq? : Option Ident := none
+
+def LetConfig.setFrom (config : LetConfig) (key : Syntax) (val : Bool) : LetConfig :=
+  if key.isOfKind ``Parser.Term.letOptNondep then
+    { config with nondep := val }
+  else if key.isOfKind ``Parser.Term.letOptUsedOnly then
+    { config with usedOnly := val }
+  else if key.isOfKind ``Parser.Term.letOptZeta then
+    { config with zeta := val }
+  else if key.isOfKind ``Parser.Term.letOptPostponeValue then
+    { config with postponeValue := val }
+  else
+    config
+
+/--
+Interprets a `Parser.Term.letConfig`.
+-/
+def mkLetConfig (letConfig : Syntax) (initConfig : LetConfig) : TermElabM LetConfig := do
+  let mut config := initConfig
+  unless letConfig.isOfKind ``Parser.Term.letConfig do
+    return config
+  for item in letConfig[0].getArgs do
+    match item with
+    | `(letPosOpt| +$opt:letOpts) => config := config.setFrom opt.raw[0] true
+    | `(letNegOpt| -$opt:letOpts) => config := config.setFrom opt.raw[0] false
+    | `(letOptEq| (eq := $n:ident)) => config := { config with eq? := n }
+    | `(letOptEq| (eq := $b)) => config := { config with eq? := mkIdentFrom b (canonical := true) (← mkFreshBinderNameForTactic `h) }
+    | _ => pure ()
+  return config
+
 /-- If `useLetExpr` is true, then a kernel let-expression `let x : type := val; body` is created.
    Otherwise, we create a term of the form `letFun val (fun (x : type) => body)`
 
    The default elaboration order is `binders`, `typeStx`, `valStx`, and `body`.
    If `elabBodyFirst == true`, then we use the order `binders`, `typeStx`, `body`, and `valStx`. -/
 def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (valStx : Syntax) (body : Syntax)
-    (expectedType? : Option Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) (usedLetOnly : Bool) : TermElabM Expr := do
+    (expectedType? : Option Expr) (config : LetConfig) : TermElabM Expr := do
   let (type, val, binders) ← elabBindersEx binders fun xs => do
     let (binders, fvars) := xs.unzip
     /-
@@ -719,10 +762,10 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
     Recall that TC resolution does **not** produce synthetic opaque metavariables.
     -/
     let type ← withSynthesize (postpone := .partial) <| elabType typeStx
-    let letMsg := if useLetExpr then "let" else "have"
+    let letMsg := if config.nondep then "have" else "let"
     registerCustomErrorIfMVar type typeStx m!"failed to infer '{letMsg}' declaration type"
     registerLevelMVarErrorExprInfo type typeStx m!"failed to infer universe levels in '{letMsg}' declaration type"
-    if elabBodyFirst then
+    if config.postponeValue then
       let type ← mkForallFVars fvars type
       let val  ← mkFreshExprMVar type
       pure (type, val, binders)
@@ -742,19 +785,55 @@ 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 result ← if useLetExpr then
-    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
-    withLocalDecl id.getId (kind := kind) .default type fun x => do
-      addLocalVarInfo id x
-      let body ← elabTermEnsuringType body expectedType?
-      let body ← instantiateMVars body
-      mkLetFun x val body
-  if elabBodyFirst then
+  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
+          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
+            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
+  if config.postponeValue then
     forallBoundedTelescope type binders.size fun xs type => do
       -- the original `fvars` from above are gone, so add back info manually
       for b in binders, x in xs do
@@ -772,8 +851,21 @@ structure LetIdDeclView where
   value   : Syntax
 
 def mkLetIdDeclView (letIdDecl : Syntax) : LetIdDeclView :=
-  -- `letIdDecl` is of the form `binderIdent >> many bracketedBinder >> optType >> " := " >> termParser
-  let id      := letIdDecl[0]
+  /-
+  def letId := leading_parser binderIdent <|> hygieneInfo
+  def letIdBinder := binderIdent <|> bracketedBinder
+  def letIdLhs := letId >> many letIdBinder >> optType
+  def letIdDecl := leading_parser letIdLhs >> " := " >> termParser
+  -/
+  let letId := letIdDecl[0]
+  let id :=
+    if letId.isIdent then
+      letId
+    else if letId[0].isOfKind hygieneInfoKind then
+      HygieneInfo.mkIdent letId[0] `this (canonical := true)
+    else
+      -- Assumed to be binderIdent
+      letId[0]
   let binders := letIdDecl[1].getArgs
   let optType := letIdDecl[2]
   let type    := expandOptType id optType
@@ -786,52 +878,73 @@ def expandLetEqnsDecl (letDecl : Syntax) (useExplicit := true) : MacroM Syntax :
   let val ← expandMatchAltsIntoMatch ref matchAlts (useExplicit := useExplicit)
   return mkNode `Lean.Parser.Term.letIdDecl #[letDecl[0], letDecl[1], letDecl[2], mkAtomFrom ref " := ", val]
 
-def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) (usedLetOnly : Bool) : TermElabM Expr := do
-  let letDecl := stx[1][0]
-  let body    := stx[3]
-  if letDecl.getKind == ``Lean.Parser.Term.letIdDecl then
+def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (initConfig : LetConfig) : TermElabM Expr := do
+  let declIdx := stx.getNumArgs - 3
+  let letConfig := stx[1]
+  let config    ← mkLetConfig letConfig initConfig
+  let letDecl   := stx[declIdx][0]
+  let body      := stx[stx.getNumArgs - 1]
+  -- TODO(kmill): remove `have` kinds
+  if letDecl.getKind == ``Lean.Parser.Term.letIdDecl || letDecl.getKind == ``Lean.Parser.Term.haveIdDecl then
     let { id, binders, type, value } := mkLetIdDeclView letDecl
     let id ← if id.isIdent then pure id else mkFreshIdent id (canonical := true)
-    elabLetDeclAux id binders type value body expectedType? useLetExpr elabBodyFirst usedLetOnly
+    elabLetDeclAux id binders type value body expectedType? config
   else if letDecl.getKind == ``Lean.Parser.Term.letPatDecl then
     -- node `Lean.Parser.Term.letPatDecl  $ try (termParser >> pushNone >> optType >> " := ") >> termParser
-    if elabBodyFirst then
-      throwError "'let_delayed' with patterns is not allowed"
     let pat     := letDecl[0]
     let optType := letDecl[2]
     let val     := letDecl[4]
     if pat.getKind == ``Parser.Term.hole then
-      -- `let _ := ...` should not be treated as a `letIdDecl`
+      -- `let _ := ...` should be treated as a `letIdDecl`
       let id   ← mkFreshIdent pat (canonical := true)
       let type := expandOptType id optType
-      elabLetDeclAux id #[] type val body expectedType? useLetExpr elabBodyFirst usedLetOnly
+      elabLetDeclAux id #[] type val body expectedType? config
     else
-      -- We are currently treating `let_fun` and `let` the same way when patterns are used.
-      let stxNew ← if optType.isNone then
-        `(match $val:term with | $pat => $body)
+      if config.postponeValue then
+        throwError "`+deferValue` with patterns is not allowed"
+      if config.usedOnly then
+        throwError "`+usedOnly` with patterns is not allowed"
+      if config.zeta then
+        throwError "`+zeta` with patterns is not allowed"
+      -- We are currently ignore `config.nondep` when patterns are used.
+      let val ← if optType.isNone then
+        `($val:term)
       else
         let type := optType[0][1]
-        `(match ($val:term : $type) with | $pat => $body)
+        `(($val:term : $type))
+      let stxNew ← if let some h := config.eq? then
+        `(match $h:ident : $val:term with | $pat => $body)
+      else
+        `(match $val:term with | $pat => $body)
       withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
-  else if letDecl.getKind == ``Lean.Parser.Term.letEqnsDecl then
+  else if letDecl.getKind == ``Lean.Parser.Term.letEqnsDecl || letDecl.getKind == ``Lean.Parser.Term.haveEqnsDecl then
     let letDeclIdNew ← liftMacroM <| expandLetEqnsDecl letDecl
-    let declNew := stx[1].setArg 0 letDeclIdNew
-    let stxNew  := stx.setArg 1 declNew
+    let declNew := stx[declIdx].setArg 0 letDeclIdNew
+    let stxNew  := stx.setArg declIdx declNew
     withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
   else
     throwUnsupportedSyntax
 
 @[builtin_term_elab «let»] def elabLetDecl : TermElab :=
-  fun stx expectedType? => elabLetDeclCore stx expectedType? (useLetExpr := true) (elabBodyFirst := false) (usedLetOnly := false)
+  fun stx expectedType? => elabLetDeclCore stx expectedType? {}
+
+@[builtin_term_elab «have»] def elabHaveDecl : TermElab :=
+  fun stx expectedType? => elabLetDeclCore stx expectedType? { nondep := true }
 
 @[builtin_term_elab «let_fun»] def elabLetFunDecl : TermElab :=
-  fun stx expectedType? => elabLetDeclCore stx expectedType? (useLetExpr := false) (elabBodyFirst := false) (usedLetOnly := false)
+  fun stx expectedType? => elabLetDeclCore stx expectedType? { nondep := true }
 
 @[builtin_term_elab «let_delayed»] def elabLetDelayedDecl : TermElab :=
-  fun stx expectedType? => elabLetDeclCore stx expectedType? (useLetExpr := true) (elabBodyFirst := true) (usedLetOnly := false)
+  fun stx expectedType? => elabLetDeclCore stx expectedType? { postponeValue := true }
 
 @[builtin_term_elab «let_tmp»] def elabLetTmpDecl : TermElab :=
-  fun stx expectedType? => elabLetDeclCore stx expectedType? (useLetExpr := true) (elabBodyFirst := false) (usedLetOnly := true)
+  fun stx expectedType? => elabLetDeclCore stx expectedType? { usedOnly := true }
+
+@[builtin_term_elab «letI»] def elabLetIDecl : TermElab :=
+  fun stx expectedType? => elabLetDeclCore stx expectedType? { zeta := true }
+
+@[builtin_term_elab «haveI»] def elabHaveIDecl : TermElab :=
+  fun stx expectedType? => elabLetDeclCore stx expectedType? { zeta := true, nondep := true }
 
 builtin_initialize
   registerTraceClass `Elab.let
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index b51bfcd466..31935fc5b6 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -117,32 +117,19 @@ open Meta
     ```
     -/
     let thisId := mkIdentFrom stx `this
-    let valNew ← `(let_fun $thisId : $(← exprToSyntax type) := $val; $thisId)
+    let valNew ← `(let_fun $thisId:ident : $(← exprToSyntax type) := $val; $thisId)
     elabTerm valNew expectedType?
   | _ => throwUnsupportedSyntax
 
-@[builtin_macro Lean.Parser.Term.have] def expandHave : Macro := fun stx =>
-  match stx with
-  | `(have $hy:hygieneInfo $bs* $[: $type]? := $val; $body) =>
-    `(have $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $type]? := $val; $body)
-  | `(have $hy:hygieneInfo $bs* $[: $type]? $alts; $body)   =>
-    `(have $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $type]? $alts; $body)
-  | `(have $x:ident $bs* $[: $type]? := $val; $body) => `(let_fun $x $bs* $[: $type]? := $val; $body)
-  | `(have $x:ident $bs* $[: $type]? $alts; $body)   => `(let_fun $x $bs* $[: $type]? $alts; $body)
-  | `(have _%$x     $bs* $[: $type]? := $val; $body) => `(let_fun _%$x $bs* $[: $type]? := $val; $body)
-  | `(have _%$x     $bs* $[: $type]? $alts; $body)   => `(let_fun _%$x $bs* $[: $type]? $alts; $body)
-  | `(have $pattern:term $[: $type]? := $val; $body) => `(let_fun $pattern:term $[: $type]? := $val; $body)
-  | _                                                => Macro.throwUnsupported
-
 @[builtin_macro Lean.Parser.Term.suffices] def expandSuffices : Macro
-  | `(suffices%$tk $x:ident      : $type from $val; $body)   => `(have%$tk $x : $type := $body; $val)
+  | `(suffices%$tk $x:ident      : $type from $val; $body)   => `(have%$tk $x:ident : $type := $body; $val)
   | `(suffices%$tk _%$x          : $type from $val; $body)   => `(have%$tk _%$x : $type := $body; $val)
   | `(suffices%$tk $hy:hygieneInfo $type from $val; $body)   => `(have%$tk $hy:hygieneInfo : $type := $body; $val)
   | `(suffices%$tk $x:ident      : $type $b:byTactic'; $body) =>
     -- Pass on `SourceInfo` of `b` to `have`. This is necessary to display the goal state in the
     -- trailing whitespace of `by` and sound since `byTactic` and `byTactic'` are identical.
     let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
-    `(have%$tk $x : $type := $body; $b:byTactic)
+    `(have%$tk $x:ident : $type := $body; $b:byTactic)
   | `(suffices%$tk _%$x          : $type $b:byTactic'; $body) =>
     let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
     `(have%$tk _%$x : $type := $body; $b:byTactic)
@@ -544,28 +531,4 @@ def elabUnsafe : TermElab := fun stx expectedType? =>
       (← `(do $cmds)))
   | _ => throwUnsupportedSyntax
 
-@[builtin_term_elab Lean.Parser.Term.haveI] def elabHaveI : TermElab := fun stx expectedType? => do
-  match stx with
-  | `(haveI $x:ident $bs* : $ty := $val; $body) =>
-    withExpectedType expectedType? fun expectedType => do
-      let (ty, val) ← elabBinders bs fun bs => do
-        let ty ← elabType ty
-        let val ← elabTermEnsuringType val ty
-        pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val)
-      withLocalDeclD x.getId ty fun x => do
-        return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val]
-  | _ => throwUnsupportedSyntax
-
-@[builtin_term_elab Lean.Parser.Term.letI] def elabLetI : TermElab := fun stx expectedType? => do
-  match stx with
-  | `(letI $x:ident $bs* : $ty := $val; $body) =>
-    withExpectedType expectedType? fun expectedType => do
-      let (ty, val) ← elabBinders bs fun bs => do
-        let ty ← elabType ty
-        let val ← elabTermEnsuringType val ty
-        pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val)
-      withLetDecl x.getId ty val fun x => do
-        return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val]
-  | _ => throwUnsupportedSyntax
-
 end Lean.Elab.Term
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index b79ce54be1..d83738428a 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -648,12 +648,23 @@ def concat (terminal : CodeBlock) (kRef : Syntax) (y? : Option Var) (k : CodeBlo
   let terminal ← liftMacroM <| convertTerminalActionIntoJmp terminal.code jp xs
   return { code  := attachJP jpDecl terminal, uvars := k.uvars }
 
-def getLetIdDeclVars (letIdDecl : Syntax) : Array Var :=
-  if letIdDecl[0].isIdent then
-    #[letIdDecl[0]]
+def getLetIdVars (letId : Syntax) : Array Var :=
+  -- def letId := leading_parser binderIdent <|> hygieneInfo
+  if letId.isIdent then
+    -- TODO(kmill): Remove this case after stage0 update
+    #[letId]
+  else if letId[0].isIdent then
+    #[letId[0]]
+  else if letId[0].isOfKind hygieneInfoKind then
+    #[HygieneInfo.mkIdent letId[0] `this (canonical := true)]
   else
     #[]
 
+def getLetIdDeclVars (letIdDecl : Syntax) : Array Var :=
+  -- def letIdLhs : Parser := letId >> many (ppSpace >> letIdBinder) >> optType
+  -- def letIdDecl := leading_parser letIdLhs >> " := " >> termParser
+  getLetIdVars letIdDecl[0]
+
 -- support both regular and syntax match
 def getPatternVarsEx (pattern : Syntax) : TermElabM (Array Var) :=
   getPatternVars pattern <|>
@@ -664,22 +675,24 @@ def getPatternsVarsEx (patterns : Array Syntax) : TermElabM (Array Var) :=
   Quotation.getPatternsVars patterns
 
 def getLetPatDeclVars (letPatDecl : Syntax) : TermElabM (Array Var) := do
+  -- def letPatDecl := leading_parser termParser >> pushNone >> optType >> " := " >> termParser
   let pattern := letPatDecl[0]
   getPatternVarsEx pattern
 
 def getLetEqnsDeclVars (letEqnsDecl : Syntax) : Array Var :=
-  if letEqnsDecl[0].isIdent then
-    #[letEqnsDecl[0]]
-  else
-    #[]
+  -- def letIdLhs : Parser := letId >> many (ppSpace >> letIdBinder) >> optType
+  -- def letEqnsDecl := leading_parser letIdLhs >> matchAlts
+  getLetIdVars letEqnsDecl[0]
 
 def getLetDeclVars (letDecl : Syntax) : TermElabM (Array Var) := do
+  -- def letDecl := leading_parser letIdDecl <|> letPatDecl <|> letEqnsDecl
   let arg := letDecl[0]
-  if arg.getKind == ``Parser.Term.letIdDecl then
+  -- TODO(kmill): remove haveIdDecl and haveEqnsDecl after stage0 update
+  if arg.getKind == ``Parser.Term.letIdDecl || arg.getKind == ``Parser.Term.haveIdDecl then
     return getLetIdDeclVars arg
   else if arg.getKind == ``Parser.Term.letPatDecl then
     getLetPatDeclVars arg
-  else if arg.getKind == ``Parser.Term.letEqnsDecl then
+  else if arg.getKind == ``Parser.Term.letEqnsDecl || arg.getKind == ``Parser.Term.haveEqnsDecl then
     return getLetEqnsDeclVars arg
   else
     throwError "unexpected kind of let declaration"
@@ -688,15 +701,9 @@ def getDoLetVars (doLet : Syntax) : TermElabM (Array Var) :=
   -- leading_parser "let " >> optional "mut " >> letDecl
   getLetDeclVars doLet[2]
 
-def getDoHaveVars : Syntax → TermElabM (Array Var)
-  -- NOTE: `hygieneInfo` case should come first as `id` will match anything else
-  | `(doElem| have $info:hygieneInfo $_params* $[$_:typeSpec]? := $_val)
-  | `(doElem| have $info:hygieneInfo $_params* $[$_:typeSpec]? $_eqns:matchAlts) =>
-    return #[HygieneInfo.mkIdent info `this]
-  | `(doElem| have $id $_params* $[$_:typeSpec]? := $_val)
-  | `(doElem| have $id $_params* $[$_:typeSpec]? $_eqns:matchAlts) => return #[id]
-  | `(doElem| have $pat:letPatDecl) => getLetPatDeclVars pat
-  | _ => throwError "unexpected kind of have declaration"
+def getDoHaveVars (doHave : Syntax) : TermElabM (Array Var) :=
+  -- leading_parser "have" >> letDecl
+  getLetDeclVars doHave[1]
 
 def getDoLetRecVars (doLetRec : Syntax) : TermElabM (Array Var) := do
   -- letRecDecls is an array of `(group (optional attributes >> letDecl))`
diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index 9f0b19a063..7d05d7fdaf 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -41,7 +41,8 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
     if decl.isOfKind `Lean.Parser.Term.letPatDecl then
       throwErrorAt decl "patterns are not allowed in 'let rec' expressions"
     else if decl.isOfKind ``Lean.Parser.Term.letIdDecl || decl.isOfKind ``Lean.Parser.Term.letEqnsDecl then
-      let declId := decl[0]
+      -- TODO(kmill) replace `if` with `decl[0][0]` after stage0 update
+      let declId := if decl[0].isIdent then decl[0] else decl[0][0]
       unless declId.isIdent do
         throwErrorAt declId "'let rec' expressions must be named"
       let shortDeclName := declId.getId
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 1d3e389549..e54b9b0202 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -19,7 +19,7 @@ open Meta
 open Lean.Parser.Term
 
 private def expandSimpleMatch (stx : Syntax) (discr : Term) (lhsVar : Ident) (rhs : Term) (expectedType? : Option Expr) : TermElabM Expr := do
-  let newStx ← `(let $lhsVar := $discr; $rhs)
+  let newStx ← `(let $lhsVar:ident := $discr; $rhs)
   withMacroExpansion stx newStx <| elabTerm newStx expectedType?
 
 private def mkUserNameFor (e : Expr) : TermElabM Name := do
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 8e103bbd33..052562a9e6 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -605,18 +605,20 @@ where
   liftMetaTactic (fun g => g.nthConstructor `right 1 (some 2))
 
 @[builtin_tactic replace] def evalReplace : Tactic := fun stx => do
-  match stx with
-  | `(tactic| replace $decl:haveDecl) =>
+  -- TODO(kmill): restore after stage0 update
+  -- match stx with
+  -- | `(tactic| replace $decl:haveDecl) =>
+    let decl : TSyntax ``Parser.Term.letDecl := ⟨stx[1]⟩
     withMainContext do
-      let vars ← Elab.Term.Do.getDoHaveVars (← `(doElem| have $decl:haveDecl))
+      let vars ← Elab.Term.Do.getLetDeclVars decl
       let origLCtx ← getLCtx
-      evalTactic $ ← `(tactic| have $decl:haveDecl)
+      evalTactic $ ← `(tactic| have $(⟨decl⟩):haveDecl)
       let mut toClear := #[]
       for fv in vars do
         if let some ldecl := origLCtx.findFromUserName? fv.getId then
           toClear := toClear.push ldecl.fvarId
       liftMetaTactic1 (·.tryClearMany toClear)
-  | _ => throwUnsupportedSyntax
+  -- | _ => throwUnsupportedSyntax
 
 @[builtin_tactic runTac] def evalRunTac : Tactic := fun stx => do
   match stx with
diff --git a/src/Lean/Elab/Tactic/RCases.lean b/src/Lean/Elab/Tactic/RCases.lean
index b11882518a..3ea8a666fa 100644
--- a/src/Lean/Elab/Tactic/RCases.lean
+++ b/src/Lean/Elab/Tactic/RCases.lean
@@ -27,11 +27,12 @@ instance : Coe (TSyntax ``rcasesPatMed) (TSyntax ``rcasesPatLo) where
 instance : Coe (TSyntax `rcasesPat) (TSyntax `rintroPat) where
   coe stx := Unhygienic.run `(rintroPat| $stx:rcasesPat)
 
-/-- A list, with a disjunctive meaning (like a list of inductive constructors, or subgoals) -/
-local notation "ListΣ" => List
+-- These frequently cause bootstrapping issues. Commented out for now, using `List/-Σ-/` and `List/-Π-/` instead.
+-- /-- A list, with a disjunctive meaning (like a list of inductive constructors, or subgoals) -/
+-- local notation "ListΣ" => List
 
-/-- A list, with a conjunctive meaning (like a list of constructor arguments, or hypotheses) -/
-local notation "ListΠ" => List
+-- /-- A list, with a conjunctive meaning (like a list of constructor arguments, or hypotheses) -/
+-- local notation "ListΠ" => List
 
 /--
 An `rcases` pattern can be one of the following, in a nested combination:
@@ -65,9 +66,9 @@ inductive RCasesPatt : Type
   /-- A type ascription like `pat : ty` (parentheses are optional) -/
   | typed (ref : Syntax) : RCasesPatt → Term → RCasesPatt
   /-- A tuple constructor like `⟨p1, p2, p3⟩` -/
-  | tuple (ref : Syntax) : ListΠ RCasesPatt → RCasesPatt
+  | tuple (ref : Syntax) : List/-Π-/ RCasesPatt → RCasesPatt
   /-- An alternation / variant pattern `p1 | p2 | p3` -/
-  | alts (ref : Syntax) : ListΣ RCasesPatt → RCasesPatt
+  | alts (ref : Syntax) : List/-Σ-/ RCasesPatt → RCasesPatt
   deriving Repr
 
 namespace RCasesPatt
@@ -97,7 +98,7 @@ def ref : RCasesPatt → Syntax
 /--
 Interpret an rcases pattern as a tuple, where `p` becomes `⟨p⟩` if `p` is not already a tuple.
 -/
-def asTuple : RCasesPatt → Bool × ListΠ RCasesPatt
+def asTuple : RCasesPatt → Bool × List/-Π-/ RCasesPatt
   | paren _ p    => p.asTuple
   | explicit _ p => (true, p.asTuple.2)
   | tuple _ ps   => (false, ps)
@@ -107,7 +108,7 @@ def asTuple : RCasesPatt → Bool × ListΠ RCasesPatt
 Interpret an rcases pattern as an alternation, where non-alternations are treated as one
 alternative.
 -/
-def asAlts : RCasesPatt → ListΣ RCasesPatt
+def asAlts : RCasesPatt → List/-Σ-/ RCasesPatt
   | paren _ p => p.asAlts
   | alts _ ps => ps
   | p         => [p]
@@ -118,7 +119,7 @@ def typed? (ref : Syntax) : RCasesPatt → Option Term → RCasesPatt
   | p, some ty => typed ref p ty
 
 /-- Convert a list of patterns to a tuple pattern, but mapping `[p]` to `p` instead of `⟨p⟩`. -/
-def tuple' : ListΠ RCasesPatt → RCasesPatt
+def tuple' : List/-Π-/ RCasesPatt → RCasesPatt
   | [p] => p
   | ps  => tuple (ps.head?.map (·.ref) |>.getD .missing) ps
 
@@ -126,7 +127,7 @@ def tuple' : ListΠ RCasesPatt → RCasesPatt
 Convert a list of patterns to an alternation pattern, but mapping `[p]` to `p` instead of
 a unary alternation `|p`.
 -/
-def alts' (ref : Syntax) : ListΣ RCasesPatt → RCasesPatt
+def alts' (ref : Syntax) : List/-Σ-/ RCasesPatt → RCasesPatt
   | [p] => p
   | ps  => alts ref ps
 
@@ -139,7 +140,7 @@ becomes `⟨a, b, c, d⟩` instead of `⟨a, b, ⟨c, d⟩⟩`.
 We must be careful to turn `[a, ⟨⟩]` into `⟨a, ⟨⟩⟩` instead of `⟨a⟩` (which will not perform the
 nested match).
 -/
-def tuple₁Core : ListΠ RCasesPatt → ListΠ RCasesPatt
+def tuple₁Core : List/-Π-/ RCasesPatt → List/-Π-/ RCasesPatt
   | []         => []
   | [tuple ref []] => [tuple ref []]
   | [tuple _ ps] => ps
@@ -150,7 +151,7 @@ This function is used for producing rcases patterns based on a case tree. This i
 `tuple₁Core` but it produces a pattern instead of a tuple pattern list, converting `[n]` to `n`
 instead of `⟨n⟩` and `[]` to `_`, and otherwise just converting `[a, b, c]` to `⟨a, b, c⟩`.
 -/
-def tuple₁ : ListΠ RCasesPatt → RCasesPatt
+def tuple₁ : List/-Π-/ RCasesPatt → RCasesPatt
   | []      => default
   | [one ref n] => one ref n
   | ps      => tuple ps.head!.ref $ tuple₁Core ps
@@ -162,7 +163,7 @@ produce a list of alternatives with the same effect. This function calls `tuple
 individual alternatives, and handles merging `[a, b, c | d]` to `a | b | c | d` instead of
 `a | b | (c | d)`.
 -/
-def alts₁Core : ListΣ (ListΠ RCasesPatt) → ListΣ RCasesPatt
+def alts₁Core : List/-Σ-/ (List/-Π-/ RCasesPatt) → List/-Σ-/ RCasesPatt
   | []          => []
   | [[alts _ ps]] => ps
   | p :: ps     => tuple₁ p :: alts₁Core ps
@@ -174,7 +175,7 @@ specially translate the empty alternation to `⟨⟩`, and translate `|(a | b)`
 don't have any syntax for unary alternation). Otherwise we can use the regular merging of
 alternations at the last argument so that `a | b | (c | d)` becomes `a | b | c | d`.
 -/
-def alts₁ (ref : Syntax) : ListΣ (ListΠ RCasesPatt) → RCasesPatt
+def alts₁ (ref : Syntax) : List/-Σ-/ (List/-Π-/ RCasesPatt) → RCasesPatt
   | [[]]        => tuple .missing []
   | [[alts ref ps]] => tuple ref ps
   | ps          => alts' ref $ alts₁Core ps
@@ -204,7 +205,7 @@ constructor. The `name` is the name which will be used in the top-level `cases`
 tactics.
 -/
 def processConstructor (ref : Syntax) (info : Array ParamInfo)
-    (explicit : Bool) (idx : Nat) (ps : ListΠ RCasesPatt) : ListΠ Name × ListΠ RCasesPatt :=
+    (explicit : Bool) (idx : Nat) (ps : List/-Π-/ RCasesPatt) : List/-Π-/ Name × List/-Π-/ RCasesPatt :=
   if _ : idx < info.size then
     if !explicit && info[idx].binderInfo != .default then
       let (ns, tl) := processConstructor ref info explicit (idx+1) ps
@@ -227,7 +228,7 @@ and the list of `(constructor name, patterns)` for each constructor, where `patt
 (conjunctive) list of patterns to apply to each constructor argument.
 -/
 def processConstructors (ref : Syntax) (params : Nat) (altVarNames : Array AltVarNames := #[]) :
-    ListΣ Name → ListΣ RCasesPatt → MetaM (Array AltVarNames × ListΣ (Name × ListΠ RCasesPatt))
+    List/-Σ-/ Name → List/-Σ-/ RCasesPatt → MetaM (Array AltVarNames × List/-Σ-/ (Name × List/-Π-/ RCasesPatt))
   | [], _ => pure (altVarNames, [])
   | c :: cs, ps => do
     let info := (← getFunInfo (← mkConstWithLevelParams c)).paramInfo
@@ -354,7 +355,7 @@ partial def rcasesCore (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (e
       let rec
       /-- Runs `rcasesContinue` on the first pattern in `r` with a matching `ctorName`.
       The unprocessed patterns (subsequent to the matching pattern) are returned. -/
-      align : ListΠ (Name × ListΠ RCasesPatt) → TermElabM (ListΠ (Name × ListΠ RCasesPatt) × α)
+      align : List/-Π-/ (Name × List/-Π-/ RCasesPatt) → TermElabM (List/-Π-/ (Name × List/-Π-/ RCasesPatt) × α)
       | [] => pure ([], a)
       | (tgt, ps) :: as => do
         if tgt == ctorName then
@@ -372,7 +373,7 @@ earlier arguments. For example `⟨a | b, ⟨c, d⟩⟩` performs the `⟨c, d
 `a` branch and once on `b`.
 -/
 partial def rcasesContinue (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (a : α)
-  (pats : ListΠ (RCasesPatt × Expr)) (cont : MVarId → FVarSubst → Array FVarId → α → TermElabM α) :
+  (pats : List/-Π-/ (RCasesPatt × Expr)) (cont : MVarId → FVarSubst → Array FVarId → α → TermElabM α) :
   TermElabM α :=
   match pats with
   | []  => cont g fs clears a
diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean
index cb929cc045..88a0708125 100644
--- a/src/Lean/Meta/Tactic/TryThis.lean
+++ b/src/Lean/Meta/Tactic/TryThis.lean
@@ -426,19 +426,19 @@ def addHaveSuggestion (ref : Syntax) (h? : Option Name) (t? : Option Expr) (e :
       let tstx ← delabToRefinableSyntax t
       if prop then
         match h? with
-        | some h => pure (← `(tactic| have $(mkIdent h) : $tstx := $estx), m!"have {h} : {t} := {e}")
+        | some h => pure (← `(tactic| have $(mkIdent h):ident : $tstx := $estx), m!"have {h} : {t} := {e}")
         | none => pure (← `(tactic| have : $tstx := $estx), m!"have : {t} := {e}")
       else
         let h := h?.getD `_
-        pure (← `(tactic| let $(mkIdent h) : $tstx := $estx), m!"let {h} : {t} := {e}")
+        pure (← `(tactic| let $(mkIdent h):ident : $tstx := $estx), m!"let {h} : {t} := {e}")
     else
       if prop then
         match h? with
-        | some h => pure (← `(tactic| have $(mkIdent h) := $estx), m!"have {h} := {e}")
+        | some h => pure (← `(tactic| have $(mkIdent h):ident := $estx), m!"have {h} := {e}")
         | none => pure (← `(tactic| have := $estx), m!"have := {e}")
       else
         let h := h?.getD `_
-        pure (← `(tactic| let $(mkIdent h) := $estx), m!"let {h} := {e}")
+        pure (← `(tactic| let $(mkIdent h):ident := $estx), m!"let {h} := {e}")
     pure (tac, ← addMessageContext msg)
   if let some checkState := checkState? then
     let some (tac', msg') ← mkValidatedTactic tac msg checkState
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 59534b7fb7..4b06d40482 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -89,7 +89,7 @@ def letIdDeclNoBinders := node ``letIdDecl <|
 @[builtin_doElem_parser] def doReassignArrow := leading_parser
   notFollowedByRedefinedTermToken >> (doIdDecl <|> doPatDecl)
 @[builtin_doElem_parser] def doHave     := leading_parser
-  "have" >> Term.haveDecl
+  "have" >> Term.letDecl
 /-
 In `do` blocks, we support `if` without an `else`.
 Thus, we use indentation to prevent examples such as
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 69044c3c2b..a2a8e43ff9 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -575,18 +575,25 @@ existent in the current context, or else fails.
 @[builtin_term_parser] def doubleQuotedName := leading_parser
   "`" >> checkNoWsBefore >> rawCh '`' (trailingWs := false) >> ident
 
+def letId := (leading_parser (withAnonymousAntiquot := false)
+  (ppSpace >> binderIdent >> notFollowedBy (checkNoWsBefore "" >> "[")
+    "space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`")
+  <|> hygieneInfo)
+  <|> -- TODO(kmill): remove after stage0 update
+    (withAntiquot (mkAntiquot "haveId" `Lean.Parser.Term.letId false)
+      (error "in bootstrapping parser for haveId"))
 def letIdBinder :=
   withAntiquot (mkAntiquot "letIdBinder" decl_name% (isPseudoKind := true)) <|
     binderIdent <|> bracketedBinder
 /- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/
 def letIdLhs    : Parser :=
-  binderIdent >> notFollowedBy (checkNoWsBefore "" >> "[")
-    "space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`" >>
-  many (ppSpace >> letIdBinder) >> optType
+  letId >> many (ppSpace >> letIdBinder) >> optType
 def letIdDecl   := leading_parser (withAnonymousAntiquot := false)
   atomic (letIdLhs >> " := ") >> termParser
-def letPatDecl  := leading_parser (withAnonymousAntiquot := false)
-  atomic (termParser >> pushNone >> optType >> " := ") >> termParser
+/- Remark: `requireParens` forces the pattern to have parentheses, for trying before `letIdDecl`.
+   We need this because for `let (rfl) := h`, which would parse as `letIdDecl` due to `hygieneInfo`. -/
+def letPatDecl (requireParens := false) := leading_parser (withAnonymousAntiquot := false)
+  atomic ((if requireParens then lookahead "(" >> paren else termParser) >> pushNone >> optType >> " := ") >> termParser
 /-
   Remark: the following `(" := " <|> matchAlts)` is a hack we use
   to produce a better error message at `letDecl`.
@@ -609,11 +616,49 @@ def letEqnsDecl := leading_parser (withAnonymousAntiquot := false)
 `let pat := e` (where `pat` is an arbitrary term) or `let f | pat1 => e1 | pat2 => e2 ...`
 (a pattern matching declaration), except for the `let` keyword itself.
 `let rec` declarations are not handled here. -/
-@[builtin_doc] def letDecl := leading_parser (withAnonymousAntiquot := false)
+@[builtin_doc] def letDecl := (leading_parser (withAnonymousAntiquot := false)
   -- Remark: we disable anonymous antiquotations here to make sure
   -- anonymous antiquotations (e.g., `$x`) are not `letDecl`
   notFollowedBy (nonReservedSymbol "rec") "rec" >>
-  (letIdDecl <|> letPatDecl <|> letEqnsDecl)
+  (letPatDecl true <|> letIdDecl <|> letPatDecl <|> letEqnsDecl))
+  <|> -- TODO(kmill): remove after stage0 update
+    (withAntiquot (mkAntiquot "haveDecl" `Lean.Parser.Term.letDecl false)
+      (error "in bootstrapping parser for haveDecl"))
+/--
+`+nondep` elaborates as a nondependent `let`, a `have` expression.
+-/
+@[builtin_doc] def letOptNondep := leading_parser
+  nonReservedSymbol "nondep"
+/--
+`+postponeValue` causes the body of the `let` to be elaborated before the value.
+-/
+@[builtin_doc] def letOptPostponeValue := leading_parser
+  nonReservedSymbol "postponeValue"
+/--
+`+usedOnly` causes unused `let`s bindings to be eliminated.
+-/
+@[builtin_doc] def letOptUsedOnly := leading_parser
+  nonReservedSymbol "usedOnly"
+/--
+`+zeta` immediately inlines the `let` value after elaboration (it zeta reduces the `let`).
+-/
+@[builtin_doc] def letOptZeta := leading_parser
+  nonReservedSymbol "zeta"
+def letOpts := leading_parser
+  letOptNondep <|> letOptPostponeValue <|> letOptUsedOnly <|> letOptZeta
+def letPosOpt := leading_parser (withAnonymousAntiquot := false)
+  " +" >> checkNoWsBefore >> letOpts
+def letNegOpt := leading_parser (withAnonymousAntiquot := false)
+  " -" >> checkNoWsBefore >> letOpts
+/--
+`let (eq := h) x := v; ...` adds the equality `h : x = v` to the context while elaborating the body.
+-/
+@[builtin_doc] def letOptEq := leading_parser (withAnonymousAntiquot := false)
+  atomic (" (" >> nonReservedSymbol "eq" >> " := ") >> binderIdent >> ")"
+def letConfigItem := letPosOpt <|> letNegOpt <|> letOptEq
+/-- Configuration options for tactics. -/
+def letConfig := leading_parser (withAnonymousAntiquot := false)
+  many letConfigItem
 /--
 `let` is used to declare a local definition. Example:
 ```
@@ -634,11 +679,21 @@ assume `p` has type `Nat × Nat`, then you can write
 let (x, y) := p
 x + y
 ```
+
+The *anaphoric let* `let := v` defines a variable called `this`.
 -/
 @[builtin_term_parser] def «let» := leading_parser:leadPrec
-  withPosition ("let " >> letDecl) >> optSemicolon termParser
+  withPosition ("let" >> letConfig >> letDecl) >> optSemicolon termParser
 /--
-`let_fun x := v; b` is syntax sugar for `(fun x => b) v`.
+`have` is used to declare local hypotheses and opaque local definitions.
+
+It has the same syntax as `let`, and it is equivalent to `let +nondep`,
+creating a *nondependent* let expression.
+-/
+@[builtin_term_parser] def «have» := leading_parser:leadPrec
+  withPosition ("have" >> letConfig >> letDecl) >> optSemicolon termParser
+/--
+`let_fun x := v; b` is syntax sugar for `letFun v (fun x => b)`.
 It is very similar to `let x := v; b`, but they are not equivalent.
 In `let_fun`, the value `v` has been abstracted away and cannot be accessed in `b`.
 -/
@@ -655,29 +710,19 @@ It is often used when building macros.
 -/
 @[builtin_term_parser] def «let_tmp» := leading_parser:leadPrec
   withPosition ("let_tmp " >> letDecl) >> optSemicolon termParser
-
-def haveId := leading_parser (withAnonymousAntiquot := false)
-  (ppSpace >> binderIdent) <|> hygieneInfo
-/- like `let_fun` but with optional name -/
-def haveIdLhs    :=
-  haveId >> many (ppSpace >> letIdBinder) >> optType
-def haveIdDecl   := leading_parser (withAnonymousAntiquot := false)
-  atomic (haveIdLhs >> " := ") >> termParser
-def haveEqnsDecl := leading_parser (withAnonymousAntiquot := false)
-  haveIdLhs >> matchAlts
-/-- `haveDecl` matches the body of a have declaration: `have := e`, `have f x1 x2 := e`,
-`have pat := e` (where `pat` is an arbitrary term) or `have f | pat1 => e1 | pat2 => e2 ...`
-(a pattern matching declaration), except for the `have` keyword itself. -/
-@[builtin_doc] def haveDecl := leading_parser (withAnonymousAntiquot := false)
-  haveIdDecl <|> (ppSpace >> letPatDecl) <|> haveEqnsDecl
-@[builtin_term_parser] def «have» := leading_parser:leadPrec
-  withPosition ("have" >> haveDecl) >> optSemicolon termParser
 /-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/
 @[builtin_term_parser] def «haveI» := leading_parser
-  withPosition ("haveI " >> haveDecl) >> optSemicolon termParser
+  withPosition ("haveI " >> letDecl) >> optSemicolon termParser
 /-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
 @[builtin_term_parser] def «letI» := leading_parser
-  withPosition ("letI " >> haveDecl) >> optSemicolon termParser
+  withPosition ("letI " >> letDecl) >> optSemicolon termParser
+
+-- TODO(kmill): remove these after stage0 update
+abbrev haveId := letId
+abbrev haveIdLhs := letIdLhs
+abbrev haveIdDecl := letIdDecl
+abbrev haveEqnsDecl := letEqnsDecl
+abbrev haveDecl := letDecl
 
 def «scoped» := leading_parser "scoped "
 def «local»  := leading_parser "local "
@@ -1164,7 +1209,7 @@ end Term
 open Term in
 builtin_initialize
   register_parser_alias letDecl
-  register_parser_alias haveDecl
+  register_parser_alias "haveDecl" letDecl
   register_parser_alias sufficesDecl
   register_parser_alias letRecDecls
   register_parser_alias hole
diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out
index 76ee330e51..28eda0adff 100644
--- a/tests/lean/1021.lean.expected.out
+++ b/tests/lean/1021.lean.expected.out
@@ -1,8 +1,8 @@
 some
   {
     range :=
-      { pos := { line := 202, column := 0 }, charUtf16 := 0, endPos := { line := 207, column := 31 },
+      { pos := { line := 189, column := 0 }, charUtf16 := 0, endPos := { line := 194, column := 31 },
         endCharUtf16 := 31 },
     selectionRange :=
-      { pos := { line := 202, column := 46 }, charUtf16 := 46, endPos := { line := 202, column := 58 },
+      { pos := { line := 189, column := 46 }, charUtf16 := 46, endPos := { line := 189, column := 58 },
         endCharUtf16 := 58 } }
diff --git a/tests/lean/interactive/incrementalCombinator.lean b/tests/lean/interactive/incrementalCombinator.lean
index 0f9911a747..d6899516fd 100644
--- a/tests/lean/interactive/incrementalCombinator.lean
+++ b/tests/lean/interactive/incrementalCombinator.lean
@@ -44,7 +44,7 @@ def have : True := by
                 --^ sync
                 --^ insert: ".5"
   dbg_trace "h 3"
-
+-- TODO(kmill) make sure extra h 1 is no longer in output
 /-!
 Updating the `have` header should update the unsolved goals position (and currently re-run the body)
 -/
diff --git a/tests/lean/interactive/incrementalCombinator.lean.expected.out b/tests/lean/interactive/incrementalCombinator.lean.expected.out
index 8a4f7f9bb1..88c7c27a3e 100644
--- a/tests/lean/interactive/incrementalCombinator.lean.expected.out
+++ b/tests/lean/interactive/incrementalCombinator.lean.expected.out
@@ -22,6 +22,7 @@ h 0
 h 1
 h 2
 h 3
+h 1
 h 2.5
 h 3
 sh
diff --git a/tests/lean/noTabs.lean b/tests/lean/noTabs.lean
index 9475259eba..80fca24caf 100644
--- a/tests/lean/noTabs.lean
+++ b/tests/lean/noTabs.lean
@@ -1,3 +1,4 @@
+#guard_msgs (drop error) in
 #check
   let a := 1
 	let b := 2
diff --git a/tests/lean/noTabs.lean.expected.out b/tests/lean/noTabs.lean.expected.out
index 5262009f31..ae4363fa4e 100644
--- a/tests/lean/noTabs.lean.expected.out
+++ b/tests/lean/noTabs.lean.expected.out
@@ -1,3 +1 @@
-noTabs.lean:3:0: error: tabs are not allowed; please configure your editor to expand them
-let a := 1;
-sorry : ?m
+noTabs.lean:4:0: error: tabs are not allowed; please configure your editor to expand them
diff --git a/tests/lean/run/4405.lean b/tests/lean/run/4405.lean
index 6178bba1f8..f27f100944 100644
--- a/tests/lean/run/4405.lean
+++ b/tests/lean/run/4405.lean
@@ -24,11 +24,11 @@ but is expected to have type
   ?_ < ?_ : Prop
 ---
 error: unsolved goals
-case a
-⊢ Nat
-
 this : ?_ < ?_
 ⊢ True
+
+case a
+⊢ Nat
 -/
 #guard_msgs in
 def test : True := by
diff --git a/tests/lean/run/elabLet.lean b/tests/lean/run/elabLet.lean
new file mode 100644
index 0000000000..7898499dc3
--- /dev/null
+++ b/tests/lean/run/elabLet.lean
@@ -0,0 +1,154 @@
+import Lean
+/-!
+# Tests of the various `let` options
+-/
+
+set_option linter.unusedVariables false
+
+/-!
+No options.
+-/
+/--
+info: let x := true;
+!x : Bool
+-/
+#guard_msgs in #check let x := true; !x
+
+/-!
+The `+nondep` option gives `have`.
+-/
+/--
+info: have x := true;
+!x : Bool
+-/
+#guard_msgs in #check let +nondep x := true; !x
+
+/-!
+The `-nondep` option on `have` is a `let`.
+-/
+/--
+info: let x := true;
+!x : Bool
+-/
+#guard_msgs in #check have -nondep x := true; !x
+
+/-!
+The `+zeta` option.
+-/
+/-- info: !true : Bool -/
+#guard_msgs in #check let +zeta x := true; !x
+
+/-!
+The `+usedOnly` option.
+-/
+/--
+info: let x := true;
+!x : Bool
+-/
+#guard_msgs in #check let +usedOnly x := true; !x
+/-- info: !false : Bool -/
+#guard_msgs in #check let +usedOnly x := true; !false
+
+/-!
+`eq` for plain `let`
+-/
+/--
+trace: m : Nat := 1
+hyp : m = 1
+⊢ True
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : True := by
+  refine let (eq := hyp) m := 1; ?_
+  trace_state
+  sorry
+
+/-!
+`eq` for `have`
+-/
+/--
+trace: m : Nat
+hyp : m = 1
+⊢ True
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : True := by
+  refine have (eq := hyp) m := 1; ?_
+  trace_state
+  sorry
+
+/-!
+Patterns with `(eq := _)`
+-/
+/--
+trace: p : Nat × Nat
+x y : Nat
+h : p = (x, y)
+this : x + y = p.fst + p.snd
+⊢ True
+-/
+#guard_msgs in
+example (p : Nat × Nat) : True :=
+  let (eq := h) (x, y) := p
+  have : x + y = p.1 + p.2 := by
+    simp [h]
+  by
+    trace_state
+    trivial
+/--
+trace: p : Nat × Nat
+x y : Nat
+h✝ : p = (x, y)
+⊢ x + y = p.fst + p.snd
+-/
+#guard_msgs in
+example (p : Nat × Nat) : True :=
+  let (eq := _) (x, y) := p
+  have : x + y = p.1 + p.2 := by
+    trace_state
+    simp [*]
+  trivial
+
+/-!
+`+postponeValue`, example from `Lean.Elab.Term.Do.ToTerm.mkJoinPoint`.
+-/
+/--
+error: type mismatch
+  jp ()
+has type
+  IO (IO.Ref Bool) : Type
+but is expected to have type
+  IO Unit : Type
+-/
+#guard_msgs in
+def f (x : Nat) : IO Unit :=
+  let jp (u : Unit) : IO _ :=
+    IO.mkRef true
+  do
+    if x > 0 then
+      IO.println "not zero"
+      jp ()
+    else
+      jp ()
+/--
+error: type mismatch
+  IO.mkRef true
+has type
+  BaseIO (IO.Ref Bool) : Type
+but is expected to have type
+  IO Unit : Type
+-/
+#guard_msgs in
+def f' (x : Nat) : IO Unit :=
+  let +postponeValue jp (u : Unit) : IO _ :=
+    IO.mkRef true
+  do
+    if x > 0 then
+      IO.println "not zero"
+      jp ()
+    else
+      jp ()
diff --git a/tests/lean/unknownTactic.lean.expected.out b/tests/lean/unknownTactic.lean.expected.out
index a80599a311..34b401dab7 100644
--- a/tests/lean/unknownTactic.lean.expected.out
+++ b/tests/lean/unknownTactic.lean.expected.out
@@ -5,11 +5,5 @@ a✝ : x = x
 ⊢ x = x
 ---
 unknownTactic.lean:8:22: error: unknown tactic
-unknownTactic.lean:8:18-8:24: error: unsolved goals
-x : Nat
-⊢ x = x
 ---
 unknownTactic.lean:14:22: error: unknown tactic
-unknownTactic.lean:14:18-14:24: error: unsolved goals
-x : Nat
-⊢ x = x