feat: eliminate letFun support, deprecate let_fun syntax (#9086)

This PR deprecates `let_fun` syntax in favor of `have` and removes
`letFun` support from WHNF and `simp`.

src/Init/Conv.lean

@@ -323,7 +323,7 @@ macro_rules
   | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | skip)
 
 /--
-Extracts `let` and `let_fun` expressions from within the target expression.
+Extracts `let` and `have` expressions from within the target expression.
 This is the conv mode version of the `extract_lets` tactic.
 
 - `extract_lets` extracts all the lets from the target.
@@ -336,7 +336,7 @@ See also `lift_lets`, which does not extract lets as local declarations.
 syntax (name := extractLets) "extract_lets " optConfig (ppSpace colGt (ident <|> hole))* : conv
 
 /--
-Lifts `let` and `let_fun` expressions within the target expression as far out as possible.
+Lifts `let` and `have` expressions within the target expression as far out as possible.
 This is the conv mode version of the `lift_lets` tactic.
 -/
 syntax (name := liftLets) "lift_lets " optConfig : conv

src/Init/Internal/Order/Basic.lean

@@ -544,12 +544,6 @@ end fun_order
 
 section monotone_lemmas
 
-theorem monotone_letFun
-    {α : Sort u} {β : Sort v} {γ : Sort w} [PartialOrder α] [PartialOrder β]
-    (v : γ) (k : α → γ → β)
-    (hmono : ∀ y, monotone (fun x => k x y)) :
-  monotone fun (x : α) => letFun v (k x) := hmono v
-
 @[partial_fixpoint_monotone]
 theorem monotone_ite
     {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β]

src/Init/Prelude.lean

@@ -63,15 +63,12 @@ Examples:
   fun _ => a
 
 /--
-The encoding of `let_fun x := v; b` is `letFun v (fun x => b)`.
+`letFun v (fun x => b)` is a function version of `have x := v; b`.
 This is equal to `(fun x => b) v`, so the value of `x` is not accessible to `b`.
 This is in contrast to `let x := v; b`, where the value of `x` is accessible to `b`.
 
-There is special support for `letFun`.
-Both WHNF and `simp` are aware of `letFun` and can reduce it when zeta reduction is enabled,
-despite the fact it is marked `irreducible`.
-For metaprogramming, the function `Lean.Expr.letFun?` can be used to recognize a `let_fun` expression
-to extract its parts as if it were a `let` expression.
+This used to be the way `have`/`let_fun` syntax was encoded,
+and there used to be special support for `letFun` in WHNF and `simp`.
 -/
 def letFun {α : Sort u} {β : α → Sort v} (v : α) (f : (x : α) → β x) : β v := f v
 

src/Init/SimpLemmas.lean

@@ -137,21 +137,6 @@ theorem have_body_congr' {α : Sort u} {β : Sort v} (a : α) {f f' : α → β}
     (h : ∀ x, f x = f' x) : f a = f' a :=
   h a
 
-theorem letFun_unused {α : Sort u} {β : Sort v} (a : α) {b b' : β} (h : b = b') : @letFun α (fun _ => β) a (fun _ => b) = b' :=
-  h
-
-theorem letFun_congr {α : Sort u} {β : Sort v}  {a a' : α} {f f' : α → β} (h₁ : a = a') (h₂ : ∀ x, f x = f' x)
-    : @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a' f' := by
-  rw [h₁, funext h₂]
-
-theorem letFun_body_congr {α : Sort u} {β : Sort v}  (a : α) {f f' : α → β} (h : ∀ x, f x = f' x)
-    : @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a f' := by
-  rw [funext h]
-
-theorem letFun_val_congr {α : Sort u} {β : Sort v} {a a' : α} {f : α → β} (h : a = a')
-    : @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a' f := by
-  rw [h]
-
 @[congr]
 theorem ite_congr {x y u v : α} {s : Decidable b} [Decidable c]
     (h₁ : b = c) (h₂ : c → x = u) (h₃ : ¬ c → y = v) : ite b x y = ite c u v := by

src/Init/Tactics.lean

@@ -544,7 +544,7 @@ performs the unification, and replaces the target with the unified version of `t
 syntax (name := «show») "show " term : tactic
 
 /--
-Extracts `let` and `let_fun` expressions from within the target or a local hypothesis,
+Extracts `let` and `have` expressions from within the target or a local hypothesis,
 introducing new local definitions.
 
 - `extract_lets` extracts all the lets from the target.
@@ -558,7 +558,7 @@ introduces a new local definition `z := v` and changes `h` to be `h : b z`.
 syntax (name := extractLets) "extract_lets " optConfig (ppSpace colGt (ident <|> hole))* (location)? : tactic
 
 /--
-Lifts `let` and `let_fun` expressions within a term as far out as possible.
+Lifts `let` and `have` expressions within a term as far out as possible.
 It is like `extract_lets +lift`, but the top-level lets at the end of the procedure
 are not extracted as local hypotheses.
 
@@ -1281,10 +1281,10 @@ syntax (name := substEqs) "subst_eqs" : tactic
 /-- The `run_tac doSeq` tactic executes code in `TacticM Unit`. -/
 syntax (name := runTac) "run_tac " doSeq : tactic
 
-/-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/
+/-- `haveI` behaves like `have`, but inlines the value instead of producing a `have` term. -/
 macro "haveI" c:letConfig d:letDecl : tactic => `(tactic| refine_lift haveI $c:letConfig $d:letDecl; ?_)
 
-/-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
+/-- `letI` behaves like `let`, but inlines the value instead of producing a `let` term. -/
 macro "letI" c:letConfig d:letDecl : tactic => `(tactic| refine_lift letI $c:letConfig $d:letDecl; ?_)
 
 /--

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -679,9 +679,7 @@ where
       visit (f.beta e.getAppArgs)
 
   visitApp (e : Expr) : M Arg := do
-    if let some (args, n, t, v, b) := e.letFunAppArgs? then
-      visitCore <| mkAppN (.letE n t v b (nondep := true)) args
-    else if let .const declName us := CSimp.replaceConstants (← getEnv) e.getAppFn then
+    if let .const declName us := CSimp.replaceConstants (← getEnv) e.getAppFn then
       if declName == ``Quot.lift then
         visitQuotLift e
       else if declName == ``Quot.mk then

src/Lean/Elab/Binders.lean

@@ -932,7 +932,10 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (initConfig : L
   fun stx expectedType? => elabLetDeclCore stx expectedType? { nondep := true }
 
 @[builtin_term_elab «let_fun»] def elabLetFunDecl : TermElab :=
-  fun stx expectedType? => elabLetDeclCore stx expectedType? { nondep := true }
+  fun stx expectedType? => do
+    withRef stx <| Linter.logLintIf Linter.linter.deprecated stx[0]
+      "`let_fun` has been deprecated in favor of `have`"
+    elabLetDeclCore stx expectedType? { nondep := true }
 
 @[builtin_term_elab «let_delayed»] def elabLetDelayedDecl : TermElab :=
   fun stx expectedType? => elabLetDeclCore stx expectedType? { postponeValue := true }

src/Lean/Elab/BuiltinNotation.lean

@@ -108,7 +108,7 @@ open Meta
     Recall that we do not use the same approach used to elaborate type ascriptions.
     For the `($val : $type)` notation, we just elaborate `val` using `type` and
     ensure it has type `type`. This approach only ensure the type resulting expression
-    is definitionally equal to `type`. For the `show` notation we use `let_fun` to ensure the type
+    is definitionally equal to `type`. For the `show` notation we use `have` to ensure the type
     of the resulting expression is *structurally equal* `type`. Structural equality is important,
     for example, if the resulting expression is a `simp`/`rw` parameter. Here is an example:
     ```

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -25,18 +25,14 @@ structure EqnInfoCore where
   deriving Inhabited
 
 /--
-Zeta reduces `let` and `let_fun` while consuming metadata.
+Zeta reduces `let` and `have` while consuming metadata.
 Returns true if progress is made.
 -/
 partial def expand (progress : Bool) (e : Expr) : Bool × Expr :=
   match e with
   | Expr.letE _ _ v b _ => expand true (b.instantiate1 v)
   | Expr.mdata _ b      => expand true b
-  | e =>
-    if let some (_, _, v, b) := e.letFun? then
-      expand true (b.instantiate1 v)
-    else
-      (progress, e)
+  | e                   => (progress, e)
 
 def expandRHS? (mvarId : MVarId) : MetaM (Option MVarId) := do
   let target ← mvarId.getType'

src/Lean/Elab/PreDefinition/Main.lean

@@ -98,11 +98,7 @@ private partial def ensureNoUnassignedLevelMVarsAtPreDef (preDef : PreDefinition
             | .proj _ _ b    => withExpr e do visit b
             | .sort u        => visitLevel u (← read)
             | .const _ us    => (if head then id else withExpr e) <| us.forM (visitLevel · (← read))
-            | .app ..        => withExpr e do
-                                  if let some (args, n, t, v, b) := e.letFunAppArgs? then
-                                    visit t; visit v; withLocalDeclD n t fun x => visit (b.instantiate1 x); args.forM visit
-                                  else
-                                    e.withApp fun f args => do visit f true; args.forM visit
+            | .app ..        => withExpr e do e.withApp fun f args => do visit f true; args.forM visit
             | _              => pure ()
       try
         visit preDef.value |>.run preDef.value |>.run {}

src/Lean/Elab/PreDefinition/WF/FloatRecApp.lean

@@ -23,6 +23,7 @@ Preprocesses the expressions to improve the effectiveness of `wfRecursion`.
 
 Unlike `Lean.Elab.Structural.preprocess`, do _not_ beta-reduce, as it could
 remove `let_fun`-lambdas that contain explicit termination proofs.
+(Note(kmill): this last statement no longer affects `let_fun`/`have`.)
 -/
 def floatRecApp (e : Expr) : CoreM Expr :=
   Core.transform e

src/Lean/Elab/Tactic/Monotonicity.lean

@@ -111,7 +111,7 @@ def solveMonoStep (failK : ∀ {α}, Expr → Array Name → MetaM α := @defaul
     return [goal]
 
   match_expr type with
-  | monotone α inst_α β inst_β f =>
+  | monotone α inst_α _ _ f =>
     -- Ensure f is not headed by a redex and headed by at least one lambda, and clean some
     -- redexes left by some of the lemmas we tend to apply
     let f ← instantiateMVars f
@@ -150,26 +150,6 @@ def solveMonoStep (failK : ∀ {α}, Expr → Array Name → MetaM α := @defaul
           pure goal'
         return [goal'.mvarId!]
 
-    -- Float `letFun` to the environment.
-    -- (cannot use `applyConst`, it tends to reduce the let redex)
-    match_expr e with
-    | letFun γ _ v b =>
-      if γ.hasLooseBVars || v.hasLooseBVars then
-        failK f #[]
-      let b' := f.updateLambdaE! f.bindingDomain! b
-      let p  ← mkAppOptM ``monotone_letFun #[α, β, γ, inst_α, inst_β, v, b']
-      let new_goals ← prependError m!"Could not apply {p}:" do
-        goal.apply p
-      let [new_goal] := new_goals
-          | throwError "Unexpected number of goals after {.ofConstName ``monotone_letFun}."
-      let (_, new_goal) ←
-        if b.isLambda then
-          new_goal.intro b.bindingName!
-        else
-          new_goal.intro1
-      return [new_goal]
-    | _ => pure ()
-
     -- Handle lambdas, preserving the name of the binder
     if e.isLambda then
       let [new_goal] ← applyConst goal ``monotone_of_monotone_apply

src/Lean/Expr.lean

@@ -1963,10 +1963,11 @@ def setAppPPExplicitForExposingMVars (e : Expr) : Expr :=
   | _      => e
 
 /--
-Returns true if `e` is a `let_fun` expression, which is an expression of the form `letFun v f`.
+Returns true if `e` is an expression of the form `letFun v f`.
 Ideally `f` is a lambda, but we do not require that here.
 Warning: if the `let_fun` is applied to additional arguments (such as in `(let_fun f := id; id) 1`), this function returns `false`.
 -/
+@[deprecated Expr.isHave (since := "2025-06-29")]
 def isLetFun (e : Expr) : Bool := e.isAppOfArity ``letFun 4
 
 /--
@@ -1979,6 +1980,7 @@ They can be created using `Lean.Meta.mkLetFun`.
 
 If in the encoding of `let_fun` the last argument to `letFun` is eta reduced, this returns `Name.anonymous` for the binder name.
 -/
+@[deprecated Expr.isHave (since := "2025-06-29")]
 def letFun? (e : Expr) : Option (Name × Expr × Expr × Expr) :=
   match e with
   | .app (.app (.app (.app (.const ``letFun _) t) _β) v) f =>
@@ -1991,6 +1993,7 @@ def letFun? (e : Expr) : Option (Name × Expr × Expr × Expr) :=
 Like `Lean.Expr.letFun?`, but handles the case when the `let_fun` expression is possibly applied to additional arguments.
 Returns those arguments in addition to the values returned by `letFun?`.
 -/
+@[deprecated Expr.isHave (since := "2025-06-29")]
 def letFunAppArgs? (e : Expr) : Option (Array Expr × Name × Expr × Expr × Expr) := do
   guard <| 4 ≤ e.getAppNumArgs
   guard <| e.isAppOf ``letFun

src/Lean/Meta/AppBuilder.lean

@@ -34,9 +34,10 @@ def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : MetaM Expr := do
   return mkExpectedTypeHintCore e expectedType u
 
 /--
-`mkLetFun x v e` creates the encoding for the `let_fun x := v; e` expression.
+`mkLetFun x v e` creates `letFun v (fun x => e)`.
 The expression `x` can either be a free variable or a metavariable, and the function suitably abstracts `x` in `e`.
 -/
+@[deprecated mkLetFVars (since := "2026-06-29")]
 def mkLetFun (x : Expr) (v : Expr) (e : Expr) : MetaM Expr := do
   -- If `x` is an `ldecl`, then the result of `mkLambdaFVars` is a let expression.
   let ensureLambda : Expr → Expr

src/Lean/Meta/Tactic/FunInd.lean

@@ -290,14 +290,6 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
   withTraceNode `Meta.FunInd (pure m!"{exceptEmoji ·} foldAndCollect ({mkFVar oldIH} → {mkFVar newIH})::{indentExpr e}") do
 
   let e' ← id do
-    if let some (n, t, v, b) := e.letFun? then
-      let t' ← foldAndCollect oldIH newIH isRecCall t
-      let v' ← foldAndCollect oldIH newIH isRecCall v
-      return ← withLocalDeclD n t' fun x => do
-        M.localMapM (mkLetFun x v' ·) do
-          let b' ← foldAndCollect oldIH newIH isRecCall (b.instantiate1 x)
-          mkLetFun x v' b'
-
     if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then
       if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
         -- We do different things to the matcher when folding recursive calls and when
@@ -673,12 +665,6 @@ def rwLetWith (h : Expr) (e : Expr) : MetaM Simp.Result := do
 def rwMData (e : Expr) : MetaM Simp.Result := do
   return { expr := e.consumeMData }
 
-def rwHaveWith (h : Expr) (e : Expr) : MetaM Simp.Result := do
-  if let some (_n, t, _v, b) := e.letFun? then
-    if (← isDefEq t (← inferType h)) then
-      return { expr := b.instantiate1 h }
-  return { expr := e }
-
 def rwFun (names : Array Name) (e : Expr) : MetaM Simp.Result := do
   e.withApp fun f xs => do
     if let some name := names.find? f.isConstOf then
@@ -910,14 +896,6 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
         buildInductionBody toErase toClear goal' oldIH newIH isRecCall (b.instantiate1 x)
       mkLetFVars #[x] b'
 
-  if let some (n, t, v, b) := e.letFun? then
-    let t' ← foldAndCollect oldIH newIH isRecCall t
-    let v' ← foldAndCollect oldIH newIH isRecCall v
-    return ← withLetDecl n t' v' fun x => M2.branch do
-      let b' ← withRewrittenMotiveArg goal (rwHaveWith x) fun goal' =>
-        buildInductionBody toErase toClear goal' oldIH newIH isRecCall (b.instantiate1 x)
-      mkLetFVars #[x] b' (usedLetOnly := false)
-
   -- Special case for traversing the PProd’ed bodies in our encoding of structural mutual recursion
   if let .lam n t b bi := e then
     if goal.isForall then
@@ -1550,9 +1528,6 @@ where
                 modify (·.set! i true)
             for alt in args[matchInfo.getFirstAltPos...matchInfo.arity] do
               go xs alt
-        if f.isConstOf ``letFun then
-          for arg in args[3...4] do
-            go xs arg
         if f.isConstOf ``ite || f.isConstOf ``dite then
           for arg in args[3...5] do
             go xs arg

src/Lean/Meta/Tactic/Grind/Intro.lean

@@ -89,10 +89,7 @@ private def intro1 : GoalM FVarId := do
   let (name, type) ← match target with
     | .forallE n d .. => pure (n, d)
     | .letE n d .. => pure (n, d)
-    | _ =>
-      let some (n, d, _) := target.letFun? |
-        throwError "`grind` internal error, binder expected"
-      pure (n, d)
+    | _ => throwError "`grind` internal error, binder expected"
   let name ← mkCleanName name type
   let (fvarId, mvarId) ← (← get).mvarId.intro name
   modify fun s => { s with mvarId }
@@ -149,7 +146,7 @@ private partial def introNext (goal : Goal) (generation : Nat) : GrindM IntroRes
             let h ← mkLambdaFVars #[mkFVar fvarId] mvarNew
             mvarId.assign h
             return .newHyp fvarId { (← get) with mvarId := mvarIdNew }
-    else if target.isLet || target.isLetFun then
+    else if target.isLet then
       if (← getConfig).zetaDelta then
         let targetNew := expandLet target #[]
         let mvarId := (← get).mvarId

src/Lean/Meta/Tactic/Intro.lean

@@ -50,35 +50,24 @@ namespace Lean.Meta
       let fvars  := fvars.push fvar
       loop i lctx fvars j s body
     | i+1, type =>
-      if let some (n, type, val, body) := type.letFun? then
-        let type   := type.instantiateRevRange j fvars.size fvars
-        let type   := type.headBeta
-        let val    := val.instantiateRevRange j fvars.size fvars
-        let fvarId ← mkFreshFVarId
-        let (n, s) ← mkName lctx n true s
-        let lctx   := lctx.mkLetDecl fvarId n type val
-        let fvar   := mkFVar fvarId
-        let fvars  := fvars.push fvar
-        loop i lctx fvars j s body
-      else
-        let type := type.instantiateRevRange j fvars.size fvars
-        withLCtx' lctx do
-          withNewLocalInstances fvars j do
-            /- We used to use just `whnf`, but it produces counterintuitive behavior if
-              - `type` is a metavariable `?m` such that `?m := let x := v; b`, or
-              - `type` has `MData` or annotations such as `optParam` around a `let`-expression.
+      let type := type.instantiateRevRange j fvars.size fvars
+      withLCtx' lctx do
+        withNewLocalInstances fvars j do
+          /- We used to use just `whnf`, but it produces counterintuitive behavior if
+            - `type` is a metavariable `?m` such that `?m := let x := v; b`, or
+            - `type` has `MData` or annotations such as `optParam` around a `let`-expression.
 
-              `whnf` instantiates metavariables, and consumes `MData`, but it also expands the `let`.
-            -/
-            let newType := (← instantiateMVars type).cleanupAnnotations
-            if newType.isForall || newType.isLet || newType.isLetFun then
+            `whnf` instantiates metavariables, and consumes `MData`, but it also expands the `let`.
+          -/
+          let newType := (← instantiateMVars type).cleanupAnnotations
+          if newType.isForall || newType.isLet then
+            loop (i+1) lctx fvars fvars.size s newType
+          else
+            let newType ← whnf newType
+            if newType.isForall then
               loop (i+1) lctx fvars fvars.size s newType
             else
-              let newType ← whnf newType
-              if newType.isForall then
-                loop (i+1) lctx fvars fvars.size s newType
-              else
-                throwTacticEx `introN mvarId "insufficient number of binders"
+              throwTacticEx `introN mvarId "insufficient number of binders"
   let (fvars, mvarId) ← loop n lctx #[] 0 s mvarType
   return (fvars.map Expr.fvarId!, mvarId)
 
@@ -114,7 +103,7 @@ private def mkAuxNameImp (preserveBinderNames : Bool) (hygienic : Bool) (useName
       mkAuxNameWithoutGivenName rest
 where
   mkAuxNameWithoutGivenName (rest : List Name) : MetaM (Name × List Name) := do
-    -- Use a nicer binder name than `[anonymous]`, which can appear in for example `letFun x f` when `f` is not a lambda expression.
+    -- Use a nicer binder name than `[anonymous]`.
     -- In this case, we make sure the name is hygienic.
     let binderName ← if binderName.isAnonymous then mkFreshUserName `a else pure binderName
     if preserveBinderNames then
@@ -177,11 +166,7 @@ partial def getIntrosSize : Expr → Nat
   | .forallE _ _ b _ => getIntrosSize b + 1
   | .letE _ _ _ b _  => getIntrosSize b + 1
   | .mdata _ b       => getIntrosSize b
-  | e                =>
-    if let some (_, _, _, b) := e.letFun? then
-      getIntrosSize b + 1
-    else
-      0
+  | _                => 0
 
 /--
 Introduce as many binders as possible without unfolding definitions.

src/Lean/Meta/Tactic/Lets.lean

@@ -68,7 +68,7 @@ def nextNameForBinderName? (binderName : Name) : M (Option Name) := do
       return n
     else
       if binderName.isAnonymous then
-        -- Use a nicer binder name than `[anonymous]`, which can appear for example in `letFun x f` when `f` is not a lambda expression.
+        -- Use a nicer binder name than `[anonymous]`.
         mkFreshUserName `a
       else if (← read).preserveBinderNames || n.hasMacroScopes then
         return n
@@ -133,7 +133,7 @@ def withEnsuringDeclsInContext [Monad m] [MonadControlT MetaM m] [MonadLCtx m] (
   withExistingLocalDecls decls.toList k
 
 /--
-Closes all the local declarations in `e`, creating `let` and `letFun` expressions.
+Closes all the local declarations in `e`, creating `let` and `have` expressions.
 Does not require that any of the declarations are in context.
 Assumes that `e` contains no metavariables with local contexts that contain any of these metavariables
 (the extraction procedure creates no new metavariables, so this is the case).
@@ -148,7 +148,7 @@ def mkLetDecls (decls : Array LocalDecl') (e : Expr) : Expr :=
 
 /--
 Makes sure the declaration for `fvarId` is marked with `isLet := true`.
-Used in `lift + merge` mode to ensure that, after merging, if any version was a `let` then it's a `let` rather than a `letFun`.
+Used in `lift + merge` mode to ensure that, after merging, if any version was a `let` then it's a `let` rather than a `have`.
 -/
 def ensureIsLet (fvarId : FVarId) : M Unit := do
   modify fun s => { s with
@@ -185,12 +185,11 @@ def initializeValueMap : M Unit := do
       modify fun s => { s with valueMap := s.valueMap.insert value decl.fvarId }
 
 /--
-Returns `true` if the expression contains a `let` expression or a `letFun`
-(this does not verify that the `letFun`s are well-formed).
+Returns `true` if the expression contains a `let` expression or a `have`.
 Its purpose is to be a check for whether a subexpression can be skipped.
 -/
 def containsLet (e : Expr) : Bool :=
-  Option.isSome <| e.find? fun e' => e'.isLet || e'.isConstOf ``letFun
+  Option.isSome <| e.find? (·.isLet)
 
 /--
 Extracts lets from `e`.
@@ -214,7 +213,7 @@ partial def extractCore (fvars : List Expr) (e : Expr) (topLevel : Bool := false
       if !containsLet e then
         return e
       -- Don't honor `proofs := false` or `types := false` for top-level lets, since it's confusing not having them be extracted.
-      unless topLevel && (e.isLet || e.isLetFun || e.isMData) do
+      unless topLevel && (e.isLet || e.isMData) do
         if !cfg.proofs then
           if ← isProof e then
             return e
@@ -225,12 +224,8 @@ partial def extractCore (fvars : List Expr) (e : Expr) (topLevel : Bool := false
       match e with
       | .bvar .. | .fvar .. | .mvar .. | .sort .. | .const .. | .lit .. => unreachable!
       | .mdata _ e'      => return e.updateMData! (← extractCore fvars e' (topLevel := topLevel))
-      | .letE n t v b nondep  => extractLetLike (!nondep) n t v b (fun t v b => pure <| e.updateLetE! t v b) (topLevel := topLevel)
-      | .app ..          =>
-        if e.isLetFun then
-          extractLetFun e (topLevel := topLevel)
-        else
-          whenDescend do extractApp e.getAppFn e.getAppArgs
+      | .letE n t v b nondep  => extractLetLike (!nondep) n t v b (topLevel := topLevel)
+      | .app ..          => whenDescend do extractApp e.getAppFn e.getAppArgs
       | .proj _ _ s      => whenDescend do return e.updateProj! (← extractCore fvars s)
       | .lam n t b i     => whenDescend do extractBinder n t b i (fun t b => e.updateLambda! i t b)
       | .forallE n t b i => whenDescend do extractBinder n t b i (fun t b => e.updateForall! i t b)
@@ -248,7 +243,7 @@ where
           return mk t (b.abstract #[x])
     else
       return mk t b
-  extractLetLike (isLet : Bool) (n : Name) (t v b : Expr) (mk : Expr → Expr → Expr → M Expr) (topLevel : Bool) : M Expr := do
+  extractLetLike (isLet : Bool) (n : Name) (t v b : Expr) (topLevel : Bool) : M Expr := do
     let cfg ← read
     let t ← extractCore fvars t
     let v ← extractCore fvars v
@@ -261,39 +256,26 @@ where
           extractCore fvars (b.instantiate1 (.fvar fvarId)) (topLevel := topLevel)
     let (extract, n) ← isExtractableLet fvars n t v
     if !extract && (!cfg.underBinder || !cfg.descend) then
-      return ← mk t v b
+      return e.updateLetE! t v b
     withLetDecl n t v fun x => do
       if extract then
         addDecl (← x.fvarId!.getDecl) isLet
         extractCore fvars (b.instantiate1 x) (topLevel := topLevel)
       else
         let b ← extractCore (x :: fvars) (b.instantiate1 x)
-        mk t v (b.abstract #[x])
-  /-- `e` is the letFun expression -/
-  extractLetFun (e : Expr) (topLevel : Bool) : M Expr := do
-    let letFunE := e.getAppFn
-    let β := e.getArg! 1
-    let (n, t, v, b) := e.letFun?.get!
-    extractLetLike false n t v b (topLevel := topLevel)
-      (fun t v b =>
-        -- Strategy: construct letFun directly rather than use `mkLetFun`.
-        -- We don't update the `β` argument.
-        return mkApp4 letFunE t β v (.lam n t b .default))
+        return e.updateLetE! t v (b.abstract #[x])
   extractApp (f : Expr) (args : Array Expr) : M Expr := do
     let cfg ← read
-    if f.isConstOf ``letFun && args.size ≥ 4 then
-      extractApp (mkAppN f args[*...4]) args[4...*]
+    let f' ← extractCore fvars f
+    if cfg.implicits then
+      return mkAppN f' (← args.mapM (extractCore fvars))
     else
-      let f' ← extractCore fvars f
-      if cfg.implicits then
-        return mkAppN f' (← args.mapM (extractCore fvars))
-      else
-        let (paramInfos, _) ← instantiateForallWithParamInfos (← inferType f) args
-        let mut args := args
-        for i in [0:args.size] do
-          if paramInfos[i]!.binderInfo.isExplicit then
-            args := args.set! i (← extractCore fvars args[i]!)
-        return mkAppN f' args
+      let (paramInfos, _) ← instantiateForallWithParamInfos (← inferType f) args
+      let mut args := args
+      for i in [0:args.size] do
+        if paramInfos[i]!.binderInfo.isExplicit then
+          args := args.set! i (← extractCore fvars args[i]!)
+      return mkAppN f' args
 
 def extractTopLevel (e : Expr) : M Expr := do
   let e ← instantiateMVars e

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -210,12 +210,6 @@ private def reduceStep (e : Expr) : SimpM Expr := do
       return expandLet b #[v] (zetaHave := cfg.zetaHave)
     else if cfg.zetaUnused && !b.hasLooseBVars then
       return consumeUnusedLet b
-  -- TODO(kmill): we are going to remove `letFun` support.
-  if let some (args, _, _, v, b) := e.letFunAppArgs? then
-    if cfg.zeta && cfg.zetaHave then
-      return mkAppN (expandLet b #[v] (zetaHave := cfg.zetaHave)) args
-    else if cfg.zetaUnused && !b.hasLooseBVars then
-      return mkAppN (consumeUnusedLet b) args
   match (← unfold? e) with
   | some e' =>
     trace[Meta.Tactic.simp.rewrite] "unfold {.ofConst e.getAppFn}, {e} ==> {e'}"
@@ -986,12 +980,6 @@ def simpApp (e : Expr) : SimpM Result := do
   if isOfNatNatLit e || isOfScientificLit e || isCharLit e then
     -- Recall that we fold "orphan" kernel Nat literals `n` into `OfNat.ofNat n`
     return { expr := e }
-  else if let some (args, n, t, v, b) := e.letFunAppArgs? then
-    /-
-    Note: we will be removing `letFun`, and we want everything to be in terms of `nondep := true` lets.
-    This will then use `simpLet`.
-    -/
-    return { expr := mkAppN (Expr.letE n t v b true) args }
   else
     congr e
 

src/Lean/Meta/WHNF.lean

@@ -601,12 +601,6 @@ partial def expandLet (e : Expr) (vs : Array Expr) (zetaHave : Bool := true) : E
       expandLet b (vs.push <| v.instantiateRev vs) zetaHave
     else
       e.instantiateRev vs
-  -- TODO(kmill): we are going to remove `letFun` support.
-  else if let some (_, _, v, b) := e.letFun? then
-    if zetaHave then
-      expandLet b (vs.push <| v.instantiateRev vs) zetaHave
-    else
-      e.instantiateRev vs
   else
     e.instantiateRev vs
 
@@ -620,13 +614,8 @@ In the case of `isDefEqQuick`, it is also used when `zeta` is set.
 -/
 partial def consumeUnusedLet (e : Expr) (consumeNondep : Bool := false) : Expr :=
   match e with
-  | e@(.letE _ _ _ b nondep) => if b.hasLooseBVars || (nondep && !consumeNondep) then e else consumeUnusedLet b consumeNondep
-  | e =>
-    -- TODO(kmill): we are going to remove `letFun` support.
-    if let some (_, _, _, b) := e.letFun? then
-      if b.hasLooseBVars || !consumeNondep then e else consumeUnusedLet b consumeNondep
-    else
-      e
+  | .letE _ _ _ b nondep => if b.hasLooseBVars || (nondep && !consumeNondep) then e else consumeUnusedLet b consumeNondep
+  | _ => e
 
 /--
 Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
@@ -650,13 +639,6 @@ where
           return e
       | .app f ..       =>
         let cfg ← getConfig
-        -- TODO(kmill): we are going to remove `letFun` support.
-        if let some (args, _, _, v, b) := e.letFunAppArgs? then
-          -- When zeta reducing enabled, always reduce `letFun` no matter the current reducibility level
-          if cfg.zeta && cfg.zetaHave then
-            return (← go <| mkAppN (expandLet b #[v] (zetaHave := cfg.zetaHave)) args)
-          else if cfg.zetaUnused && !b.hasLooseBVars then
-            return (← go <| mkAppN (consumeUnusedLet b) args)
         let f := f.getAppFn
         let f' ← go f
         /-

src/Lean/Parser/Term.lean

@@ -692,9 +692,7 @@ 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`.
+`let_fun x := v; b` is deprecated syntax sugar for `have x := v; b`.
 -/
 @[builtin_term_parser] def «let_fun»     := leading_parser:leadPrec
   withPosition ((symbol "let_fun " <|> "let_λ ") >> letDecl) >> optSemicolon termParser

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -836,23 +836,6 @@ where
     else
       x
 
-/--
-Delaborates applications of the form `letFun v (fun x => b)` as `have x := v; b`.
--/
-@[builtin_delab app.letFun]
-def delabLetFun : Delab := whenPPOption getPPNotation <| withOverApp 4 do
-  let e ← getExpr
-  guard <| e.getAppNumArgs == 4
-  let Expr.lam n _ b _ := e.appArg! | failure
-  let n ← getUnusedName n b
-  let stxV ← withAppFn <| withAppArg delab
-  let (stxN, stxB) ← withAppArg <| withBindingBody' n (mkAnnotatedIdent n) fun stxN => return (stxN, ← delab)
-  if ← getPPOption getPPLetVarTypes <||> getPPOption getPPAnalysisLetVarType then
-    let stxT ← SubExpr.withNaryArg 0 delab
-    `(have $stxN : $stxT := $stxV; $stxB)
-  else
-    `(have $stxN := $stxV; $stxB)
-
 @[builtin_delab mdata]
 def delabMData : Delab := do
   if let some _ := inaccessible? (← getExpr) then
@@ -1312,16 +1295,6 @@ partial def delabDoElems : DelabM (List Syntax) := do
           prependAndRec `(doElem|have $(mkIdent n) : $stxT := $stxV)
         else
           prependAndRec `(doElem|let $(mkIdent n) : $stxT := $stxV)
-  else if e.isLetFun then
-    -- letFun.{u, v} : {α : Sort u} → {β : α → Sort v} → (v : α) → ((x : α) → β x) → β v
-    let stxT ← withNaryArg 0 delab
-    let stxV ← withNaryArg 2 delab
-    withAppArg do
-      match (← getExpr) with
-      | Expr.lam .. =>
-        withBindingBodyUnusedName fun n => do
-          prependAndRec `(doElem|have $n:term : $stxT := $stxV)
-      | _ => failure
   else
     let stx ← delab
     return [← `(doElem|$stx:term)]

tests/lean/consumePPHint.lean

@@ -1,10 +1,14 @@
+/-!
+This test used to check that metadata wasn't consumed by `apply`.
+-/
+
 opaque p : Nat → Prop
 opaque q : Nat → Prop
 
 theorem p_of_q : q x → p x := sorry
 
-theorem pletfun : p (let_fun x := 0; x + 1) := by
-  -- ⊢ p (let_fun x := 0; x + 1)
+theorem pletfun : p (have x := 0; x + 1) := by
+  -- ⊢ p (have x := 0; x + 1)
   apply p_of_q
-  trace_state -- `let_fun` hint should not be consumed.
+  trace_state -- `have` should not be consumed.
   sorry

tests/lean/consumePPHint.lean.expected.out

@@ -1,6 +1,6 @@
-consumePPHint.lean:4:8-4:14: warning: declaration uses 'sorry'
+consumePPHint.lean:8:8-8:14: warning: declaration uses 'sorry'
 case a
 ⊢ q
     (have x := 0;
     x + 1)
-consumePPHint.lean:6:8-6:15: warning: declaration uses 'sorry'
+consumePPHint.lean:10:8-10:15: warning: declaration uses 'sorry'

tests/lean/convPatternMatchIssue.lean

@@ -1,7 +1,7 @@
 def test : (λ x => x)
            =
            (λ x : Nat =>
-             let_fun foo := λ y => id (id y)
+             have foo := λ y => id (id y)
              foo x) := by
   conv =>
     pattern (id _)

tests/lean/delabDoLetFun.lean

@@ -1,5 +1,5 @@
 /-!
-Testing delaboration of `letFun` as a `doElem`
+Testing delaboration of `have` as a `doElem`
 -/
 
 /-!

tests/lean/ppBeta.lean

@@ -1,12 +1,12 @@
 #check (fun x => x) Nat
 
-#check let_fun x := Nat; x
+#check have x := Nat; x
 
 set_option pp.beta true
 
 #check (fun x => x) Nat
 
-#check let_fun x := Nat; x
+#check have x := Nat; x
 
 set_option pp.all true
 

tests/lean/run/968.lean

@@ -2,6 +2,6 @@ example (p q r : Prop) : (p ∧ q ∧ r)
                        = (r ∧ p ∧ q) :=
 by simp only [and_comm, and_left_comm, and_assoc]
 
-example (p q r : Prop) : ((let_fun x := p; x) ∧ (let_fun x := q; x) ∧ (let_fun x := r; x))
-                       = ((let_fun x := r; x) ∧ (let_fun x := p; x) ∧ (let_fun x := q; x)) :=
+example (p q r : Prop) : ((have x := p; x) ∧ (have x := q; x) ∧ (have x := r; x))
+                       = ((have x := r; x) ∧ (have x := p; x) ∧ (have x := q; x)) :=
 by simp only [and_comm, and_left_comm, and_assoc]

tests/lean/run/delabApp.lean

@@ -40,7 +40,7 @@ structure Foo where
 #guard_msgs in #check ∀ (x : Foo), x.f 1 = 0
 
 /-!
-Overapplied `letFun`
+`have` in function position
 -/
 /--
 info: (have f := id;

tests/lean/run/extract_lets.lean

@@ -652,7 +652,7 @@ example : ∀ n : Nat, n = (let x := n; x) := by
   rfl
 
 /-!
-Same example, but testing `letFun`.
+Same example, but testing `have`.
 -/
 /--
 trace: ⊢ ∀ (n : Nat),

tests/lean/run/funind_tests.lean

@@ -520,7 +520,7 @@ info: GramSchmidt.foo.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), (
 
 end GramSchmidt
 
-namespace LetFun
+namespace Have
 
 def foo {α} (x : α) : List α → Nat
   | .nil => 0
@@ -529,7 +529,7 @@ def foo {α} (x : α) : List α → Nat
       this
 termination_by xs => xs
 /--
-info: LetFun.foo.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
+info: Have.foo.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
   (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) (a✝ : List α) : motive a✝
 -/
 #guard_msgs in
@@ -544,13 +544,13 @@ def bar {α} (x : α) : List α → Nat
 termination_by xs => xs
 
 /--
-info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
+info: Have.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
   (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) (a✝ : List α) : motive a✝
 -/
 #guard_msgs in
 #check bar.induct
 
-end LetFun
+end Have
 
 
 namespace RecCallInDisrs

tests/lean/run/grind_t1.lean

@@ -129,7 +129,7 @@ trace: [grind.eqc] x = 2 * a
 -/
 #guard_msgs (trace) in
 set_option trace.grind.eqc true in
-example (a : Nat) : let_fun x := a + a; y = x → y = a + a := by
+example (a : Nat) : have x := a + a; y = x → y = a + a := by
   grind -zetaDelta
 
 /--
@@ -138,7 +138,7 @@ trace: [grind.eqc] y = 2 * a
 -/
 #guard_msgs (trace) in
 set_option trace.grind.eqc true in
-example (a : Nat) : let_fun x := a + a; y = x → y = a + a := by
+example (a : Nat) : have x := a + a; y = x → y = a + a := by
   grind
 
 example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β)

tests/lean/run/introLetFun.lean

@@ -1,7 +1,7 @@
 import Lean.Elab.Tactic.Basic
 import Lean.Meta.Tactic.Intro
 /-!
-# Testing `intro` with `letFun`
+# Testing `intro` with `have`
 -/
 
 /-!
@@ -12,15 +12,8 @@ example : have x := 2; ∀ _ : Nat, x = x := by
   rfl
 
 /-!
-`intros` is aware of `letFun`.
+`intros` is aware of `have`.
 -/
 example : have x := 2; ∀ _ : Nat, x = x := by
   intros
   rfl
-
-/-!
-Check that it works for `letFun` with an eta reduced argument.
--/
-example (p : Nat → Prop) (h : ∀ x, p x) : letFun 2 p := by
-  intro
-  apply h

tests/lean/run/letFunUnusedVarBug.lean

@@ -1,29 +1,29 @@
 theorem ex1 (h : a = 5) :
-   let_fun x := 1
-   let_fun _y := 2
-   let_fun _z := 3
-   let_fun w := 4
+   have x := 1
+   have _y := 2
+   have _z := 3
+   have w := 4
    x + w = a := by
   simp -zeta only
   guard_target =ₛ
-    let_fun x := 1;
-    let_fun w := 4;
+    have x := 1;
+    have w := 4;
     x + w = a
   simp only
   guard_target =ₛ 1 + 4 = a
   simp [h]
 
 theorem ex2 (h : a = 6) :
-   let_fun x := 1
-   let_fun _y := 2 + x
-   let_fun _z := 3 + x
-   let_fun w := 4 + x
-   let_fun _z := 2 + w
+   have x := 1
+   have _y := 2 + x
+   have _z := 3 + x
+   have w := 4 + x
+   have _z := 2 + w
    x + w = a := by
   simp -zeta only
   guard_target =ₛ
-    let_fun x := 1;
-    let_fun w := 4 + x;
+    have x := 1;
+    have w := 4 + x;
     x + w = a
   simp only
   guard_target =ₛ 1 + (4 + 1) = a

tests/lean/run/lift_lets.lean

@@ -135,7 +135,7 @@ example : ∀ n : Nat, n = (let x := 0; n + x) := by
   rfl
 
 /-!
-Lifting `letFun` under a binder, dependency.
+Lifting `have` under a binder, dependency.
 -/
 /--
 trace: ⊢ ∀ (n : Nat),
@@ -150,7 +150,7 @@ example : ∀ n : Nat, n = (have x := n; x) := by
   rfl
 
 /-!
-Lifting `letFun` under a binder, no dependency.
+Lifting `have` under a binder, no dependency.
 -/
 /--
 trace: ⊢ have x := 0;

tests/lean/run/newfrontend5.lean

@@ -58,4 +58,4 @@ def h (x := 10) (y := 20) : Nat := x + y
 #check let f := fun (x : optParam Nat 10) => x + 1; f + f 1
 #check (fun (x : optParam Nat 10) => x)
 
-#check let_fun x := 10; x + 1
+#check have x := 10; x + 1

tests/lean/run/simpLetFunIssue.lean

@@ -92,7 +92,7 @@ example (a b : Nat) (h : a = b) : g 2 true (0 + a) = b := by
   simp -zeta only [Bool.not_true, Nat.one_mul]
   guard_target =ₛ
     (have b' := false; have x := 0 + a; have b' := !b';
-     let_fun x := x; if b' = true then x else 0) = b
+     have x := x; if b' = true then x else 0) = b
   simp [h]
 
 example (a : Nat) : g 33 true (0 + a) = 0 := by

tests/lean/run/zetaUnused.lean

@@ -61,7 +61,7 @@ example (b : Bool) : if b then have unused := (); True else False := by
   simp (config := Lean.Meta.Simp.neutralConfig) +zetaUnused only; trace_state; sorry
 
 
--- Before the introduction of zetaUnused, split would do collateral damage to unused letFuns.
+-- Before the introduction of zetaUnused, split would do collateral damage to unused `have`s.
 -- Now they are preserved:
 
 /--