diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 851cc3e171d7..ce32da7cd24a 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -8,7 +8,6 @@ module
 prelude
 public import Lean.Elab.Match
 meta import Lean.Parser.Tactic
-import Lean.Linter.Basic
 
 public section
 
@@ -943,12 +942,6 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (initConfig : L
 @[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? => 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 }
 
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 77bdae158bcf..5c371bdcde12 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -859,19 +859,6 @@ def liftCommandElabM (cmd : CommandElabM α) (throwOnError : Bool := true) : Cor
   -- `observing` ensures that if `cmd` throws an exception we still thread state back to `CoreM`.
   MonadExcept.ofExcept (← liftCommandElabMCore (observing cmd) throwOnError)
 
-/--
-Given a command elaborator `cmd`, returns a new command elaborator that
-first evaluates any local `set_option ... in ...` clauses and then invokes `cmd` on what remains.
--/
-partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
-  if stx.getKind == ``Lean.Parser.Command.in &&
-     stx[0].getKind == ``Lean.Parser.Command.set_option then
-      let opts ← Elab.elabSetOption stx[0][1] stx[0][3]
-      Command.withScope (fun scope => { scope with opts }) do
-        withSetOptionIn cmd stx[2]
-  else
-    cmd stx
-
 export Elab.Command (Linter addLinter)
 
 end Lean
diff --git a/src/Lean/Elab/SetOption.lean b/src/Lean/Elab/SetOption.lean
index 54fa9261c9bb..698ea1d761ba 100644
--- a/src/Lean/Elab/SetOption.lean
+++ b/src/Lean/Elab/SetOption.lean
@@ -42,14 +42,22 @@ where
         {indentExpr defValType}"
     | _ => throwUnconfigurable optionName
 
-def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
+/--
+Elaborates `id` as an identifier representing an option name with value given by `val`.
+
+Validates that `val` has the correct type for values of the option `id`, and returns the updated
+`Options`. Does **not** update the options in the monad `m`.
+
+If `addInfo := true` (the default), adds completion info and elaboration info to the infotrees.
+-/
+def elabSetOption (id : Syntax) (val : Syntax) (addInfo := true) : m Options := do
   let ref ← getRef
   -- For completion purposes, we discard `val` and any later arguments.
   -- We include the first argument (the keyword) for position information in case `id` is `missing`.
-  addCompletionInfo <| CompletionInfo.option (ref.setArgs (ref.getArgs[*...3]))
+  if addInfo then addCompletionInfo <| CompletionInfo.option (ref.setArgs (ref.getArgs[*...3]))
   let optionName := id.getId.eraseMacroScopes
   let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error ref ex.toString) (getOptionDecl optionName)
-  pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }
+  if addInfo then pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }
   let rec setOption (val : DataValue) : m Options := do
     validateOptionValue optionName decl val
     return (← getOptions).insert optionName val
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 3d5195bc254e..8dea31424a5e 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -1998,50 +1998,6 @@ def setAppPPExplicitForExposingMVars (e : Expr) : Expr :=
     mkAppN f args |>.setPPExplicit true
   | _      => e
 
-/--
-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
-
-/--
-Recognizes a `let_fun` expression.
-For `let_fun n : t := v; b`, returns `some (n, t, v, b)`, which are the first four arguments to `Lean.Expr.letE`.
-Warning: if the `let_fun` is applied to additional arguments (such as in `(let_fun f := id; id) 1`), this function returns `none`.
-
-`let_fun` expressions are encoded as `letFun v (fun (n : t) => b)`.
-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 =>
-    match f with
-    | .lam n _ b _ => some (n, t, v, b)
-    | _ => some (.anonymous, t, v, .app (f.liftLooseBVars 0 1) (.bvar 0))
-  | _ => none
-
-/--
-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
-  let args := e.getAppArgs
-  let t := args[0]!
-  let v := args[2]!
-  let f := args[3]!
-  let rest := args.extract 4 args.size
-  match f with
-  | .lam n _ b _ => some (rest, n, t, v, b)
-  | _ => some (rest, .anonymous, t, v, .app (f.liftLooseBVars 0 1) (.bvar 0))
-
 /-- Maps `f` on each immediate child of the given expression. -/
 @[specialize]
 def traverseChildren [Applicative M] (f : Expr → M Expr) : Expr → M Expr
diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean
index c45a70d5c009..bb4cb7515334 100644
--- a/src/Lean/Linter/Basic.lean
+++ b/src/Lean/Linter/Basic.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.MonadEnv
+public import Lean.Elab.Command
 
 public section
 
@@ -89,3 +90,23 @@ Whether a linter option is enabled or not is determined by the following sequenc
 def logLintIf [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadEnv m]
     (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit := do
   if getLinterValue linterOption (← getLinterOptions) then logLint linterOption stx msg
+
+/--
+Given a command elaborator `cmd`, returns a new command elaborator that
+first evaluates any local `set_option ... in ...` clauses and then invokes `cmd` on what remains.
+
+This is expected to be used in linters, after elaboration is complete. It is not appropriate for
+ordinary elaboration of `set_option`s, since it
+* does not update the infotrees with elaboration info from elaborating the `set_option` commands
+* silently ignores failures in setting the given options (e.g. we do not error if the option is
+  unknown or the wrong type of value is provided)
+-/
+partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
+  if stx.getKind == ``Lean.Parser.Command.in &&
+     stx[0].getKind == ``Lean.Parser.Command.set_option then
+      -- Do not modify the infotrees when elaborating, and silently ignore errors.
+      let opts ← try Elab.elabSetOption stx[0][1] stx[0][3] (addInfo := false) catch _ => getOptions
+      Command.withScope (fun scope => { scope with opts }) do
+        withSetOptionIn cmd stx[2]
+  else
+    cmd stx
diff --git a/src/Lean/Linter/List.lean b/src/Lean/Linter/List.lean
index 065d3aa7c3ca..cd85d7b2cbe2 100644
--- a/src/Lean/Linter/List.lean
+++ b/src/Lean/Linter/List.lean
@@ -179,7 +179,6 @@ def indexLinter : Linter
     if (← get).messages.hasErrors then return
     if ! (← getInfoState).enabled then return
     for t in ← getInfoTrees do
-      if let .context _ _ := t then -- Only consider info trees with top-level context
       for (idxStx, n) in numericalIndices t do
         if let .str _ n := n then
           if !allowedIndices.contains (stripBinderName n) then
@@ -236,32 +235,31 @@ def listVariablesLinter : Linter
     if (← get).messages.hasErrors then return
     if ! (← getInfoState).enabled then return
     for t in ← getInfoTrees do
-      if let .context _ _ := t then -- Only consider info trees with top-level context
-        let binders ← binders t
-        for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `List do
-          if let .str _ n := n then
-          let n := stripBinderName n
-          if !allowedListNames.contains n then
-            -- Allow `L` or `xss` for `List (List α)` or `List (Array α)`
-            unless ((ty.getArg! 0).isAppOf `List || (ty.getArg! 0).isAppOf `Array) && (n == "L" || n == "xss") do
-              Linter.logLint linter.listVariables stx
-                m!"Forbidden variable appearing as a `List` name: {n}"
-        for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Array do
-          if let .str _ n := n then
-          let n := stripBinderName n
-          if !allowedArrayNames.contains n then
-            -- Allow `xss` for `Array (Array α)` or `Array (Vector α)`
-            unless ((ty.getArg! 0).isAppOf `Array || (ty.getArg! 0).isAppOf `Vector) && n == "xss" do
-              Linter.logLint linter.listVariables stx
-                m!"Forbidden variable appearing as a `Array` name: {n}"
-        for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Vector do
-          if let .str _ n := n then
-          let n := stripBinderName n
-          if !allowedVectorNames.contains n then
-            -- Allow `xss` for `Vector (Vector α)`
-            unless (ty.getArg! 0).isAppOf `Vector && n == "xss" do
-              Linter.logLint linter.listVariables stx
-                m!"Forbidden variable appearing as a `Vector` name: {n}"
+      let binders ← binders t
+      for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `List do
+        if let .str _ n := n then
+        let n := stripBinderName n
+        if !allowedListNames.contains n then
+          -- Allow `L` or `xss` for `List (List α)` or `List (Array α)`
+          unless ((ty.getArg! 0).isAppOf `List || (ty.getArg! 0).isAppOf `Array) && (n == "L" || n == "xss") do
+            Linter.logLint linter.listVariables stx
+              m!"Forbidden variable appearing as a `List` name: {n}"
+      for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Array do
+        if let .str _ n := n then
+        let n := stripBinderName n
+        if !allowedArrayNames.contains n then
+          -- Allow `xss` for `Array (Array α)` or `Array (Vector α)`
+          unless ((ty.getArg! 0).isAppOf `Array || (ty.getArg! 0).isAppOf `Vector) && n == "xss" do
+            Linter.logLint linter.listVariables stx
+              m!"Forbidden variable appearing as a `Array` name: {n}"
+      for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Vector do
+        if let .str _ n := n then
+        let n := stripBinderName n
+        if !allowedVectorNames.contains n then
+          -- Allow `xss` for `Vector (Vector α)`
+          unless (ty.getArg! 0).isAppOf `Vector && n == "xss" do
+            Linter.logLint linter.listVariables stx
+              m!"Forbidden variable appearing as a `Vector` name: {n}"
 
 builtin_initialize addLinter listVariablesLinter
 
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index b687cf11f00e..688e7f1c2a98 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -37,25 +37,6 @@ def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : MetaM Expr := do
   let u ← getLevel expectedType
   return mkExpectedTypeHintCore e expectedType u
 
-/--
-`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
-    | .letE n t _ b _ => .lam n t b .default
-    | e@(.lam ..)     => e
-    | _               => unreachable!
-  let f ← ensureLambda <$> mkLambdaFVars (usedLetOnly := false) #[x] e
-  let ety ← inferType e
-  let α ← inferType x
-  let β ← ensureLambda <$> mkLambdaFVars (usedLetOnly := false) #[x] ety
-  let u1 ← getLevel α
-  let u2 ← getLevel ety
-  return mkAppN (.const ``letFun [u1, u2]) #[α, β, v, f]
-
 /-- Returns `a = b`. -/
 def mkEq (a b : Expr) : MetaM Expr := do
   let aType ← inferType a
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 300de7c41155..cdf13cd29f6f 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1689,9 +1689,9 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
 
     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)
-      apply p_of_q -- If we eagerly consume all metadata, the let_fun annotation is lost during `isDefEq`
+    theorem phave : p (have x := 0; x + 1) := by
+      -- ⊢ p (have x := 0; x + 1)
+      apply p_of_q -- If we eagerly consume all metadata, the `have` annotation is lost during `isDefEq`
       -- ⊢ q ((fun x => x + 1) 0)
       sorry
     ```
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 5c3d8e1b7011..0b8f95249d45 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -519,11 +519,6 @@ 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 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
-/--
 `let_delayed x := v; b` is similar to `let x := v; b`, but `b` is elaborated before `v`.
 -/
 @[builtin_term_parser] def «let_delayed» := leading_parser:leadPrec
diff --git a/tests/lean/consumePPHint.lean b/tests/lean/consumePPHint.lean
index 85e87c7a2537..224add4088a7 100644
--- a/tests/lean/consumePPHint.lean
+++ b/tests/lean/consumePPHint.lean
@@ -7,7 +7,7 @@ opaque q : Nat → Prop
 
 theorem p_of_q : q x → p x := sorry
 
-theorem pletfun : p (have x := 0; x + 1) := by
+theorem phave : p (have x := 0; x + 1) := by
   -- ⊢ p (have x := 0; x + 1)
   apply p_of_q
   trace_state -- `have` should not be consumed.
diff --git a/tests/lean/run/index_variables_linter.lean b/tests/lean/run/index_variables_linter.lean
index a215d326d652..31895192bd58 100644
--- a/tests/lean/run/index_variables_linter.lean
+++ b/tests/lean/run/index_variables_linter.lean
@@ -50,3 +50,21 @@ Note: This linter can be disabled with `set_option linter.indexVariables false`
 -/
 #guard_msgs in
 example (xs : List Nat) (m : Nat) : xs.drop m = xs.drop m := rfl
+
+/- Test that `set_option ... in` works; ensures that `withSetOptionIn` no longer leaves
+context-free info nodes (#11313) -/
+
+set_option linter.indexVariables false
+
+/--
+warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
+
+Note: This linter can be disabled with `set_option linter.indexVariables false`
+---
+warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
+
+Note: This linter can be disabled with `set_option linter.indexVariables false`
+-/
+#guard_msgs in
+set_option linter.indexVariables true in
+example (xs : List Nat) (m : Nat) : xs.drop m = xs.drop m := rfl
diff --git a/tests/lean/run/list_variables_linter.lean b/tests/lean/run/list_variables_linter.lean
index 0eabcc2c83c7..e6d1744f0bfd 100644
--- a/tests/lean/run/list_variables_linter.lean
+++ b/tests/lean/run/list_variables_linter.lean
@@ -50,3 +50,21 @@ Note: This linter can be disabled with `set_option linter.listVariables false`
 -/
 #guard_msgs in
 example (l : Array Nat) : l = l := rfl
+
+/- Test that `set_option ... in` works; ensures that `withSetOptionIn` no longer leaves
+context-free info nodes (#11313) -/
+
+set_option linter.listVariables false
+
+/--
+warning: Forbidden variable appearing as a `Array` name: l
+
+Note: This linter can be disabled with `set_option linter.listVariables false`
+---
+warning: Forbidden variable appearing as a `Array` name: l
+
+Note: This linter can be disabled with `set_option linter.listVariables false`
+-/
+#guard_msgs in
+set_option linter.listVariables true in
+example (l : Array Nat) : l = l := rfl
diff --git a/tests/lean/withSetOptionIn.lean b/tests/lean/withSetOptionIn.lean
index bc6e3a657ef8..05dd6ee71b39 100644
--- a/tests/lean/withSetOptionIn.lean
+++ b/tests/lean/withSetOptionIn.lean
@@ -2,7 +2,11 @@ import Lean
 
 /-!
 # `withSetOptionIn`
+-/
+
+section recurse
 
+/-!
 This test checks that `withSetOptionIn` recurses into the command syntax (`stx[2]`) in
 `set_option ... in <cmd>`.
 
@@ -25,7 +29,7 @@ Ensure that `#trace_debug_foo` works as expected.
 #guard_msgs in
 #trace_debug_foo
 
-/-- info: [debug] foo -/
+/-- trace: [debug] foo -/
 #guard_msgs(trace) in
 set_option trace.debug true in #trace_debug_foo
 
@@ -34,6 +38,113 @@ set_option trace.debug true in #trace_debug_foo
 Should trace `[debug] foo`, and not log the error "unexpected command 'in'".
 -/
 
-/-- info: [debug] foo -/
+/-- trace: [debug] foo -/
 #guard_msgs(trace) in
 #test set_option trace.debug true in #trace_debug_foo
+
+end recurse
+
+section infotree
+
+/-!
+These tests check that `withSetOptionIn` does not modify the infotrees (#11313).
+
+Modifying the infotrees in `withSetOptionIn` in linters created context-free info nodes, which
+caused `visitM` and related means of searching the infotrees, such as `collectNodesBottomUp`, to
+panic.
+
+We also check that we do not error inside linters due to malformed options.
+-/
+
+open Lean Elab Command
+
+/-- Two persistent arrays are equal if the corresponding elements are equal. -/
+def Lean.PersistentArray.eqOf [Inhabited α] (a b : PersistentArray α) (eq : α → α → Bool) : Bool :=
+  a.size == b.size && Id.run do
+    for i in 0...a.size do
+      unless eq a[i]! b[i]! do return false
+    return true
+
+/-- Compare the structure of an infotree. (Do not check that the infos are the same.) -/
+partial def Lean.Elab.InfoTree.structEq : InfoTree → InfoTree → Bool
+  | .context _ t, .context _ t' => t.structEq t'
+  | .node _ ts, .node _ ts' => ts.eqOf ts' structEq
+  | .hole _, .hole _ => true
+  | _, _ => false
+
+/-- Collect the option names from all `OptionInfo` infos in the infotrees. -/
+def getOptionNames (ts : PersistentArray InfoTree) : List Name :=
+  ts.foldl (init := []) fun acc t =>
+    acc ++ t.collectNodesBottomUp fun
+      | _, .ofOptionInfo i, _, ns => i.optionName :: ns
+      | _, _, _, ns => ns
+
+def compareWithSetOptionIn : CommandElab := fun stx => do
+  let originalTrees ← getInfoTrees
+  logInfo m!"without `withSetOptionIn`:\n\
+    - `linter.all := {← getBoolOption `linter.all}`\n\
+    - Found option names in trees: {getOptionNames (← getInfoTrees)}"
+  let runWithSetOptionIn : CommandElab := withSetOptionIn fun _ => do
+    logInfo m!"trees are structurally equal: {originalTrees.eqOf (← getInfoTrees) (·.structEq ·)}"
+    logInfo m!"with `withSetOptionIn`:\n\
+      - `linter.all := {← getBoolOption `linter.all}`\n\
+      - Found option names in trees: {getOptionNames (← getInfoTrees)}"
+  runWithSetOptionIn stx
+
+/-
+Should show `linter.all := false` without `withSetOptionIn`, and `linter.all := true` with.
+Should find the option name `linter.all` exactly once **both** with and without `withSetOptionIn`.
+This ensures that we're looking at correct post-elaboration infotrees in this test.
+-/
+
+/--
+info: without `withSetOptionIn`:
+- `linter.all := false`
+- Found option names in trees: [linter.all]
+---
+info: trees are structurally equal: true
+---
+info: with `withSetOptionIn`:
+- `linter.all := true`
+- Found option names in trees: [linter.all]
+-/
+#guard_msgs in
+run_cmd do
+  let stx ← `(command| set_option linter.all true in example : True := trivial)
+  elabCommand stx
+  compareWithSetOptionIn stx
+
+/-
+Should have `linter.all := false` both times, since the value is malformed, but still find an
+`OptionInfo`.
+
+Should only log the `set_option` error **once** from `elabCommand`. `compareWithSetOption` should
+not produce an error.
+-/
+
+/--
+error: set_option value type mismatch: The value
+  3
+has type
+  Nat
+but the option `linter.all` expects a value of type
+  Bool
+---
+info: without `withSetOptionIn`:
+- `linter.all := false`
+- Found option names in trees: [linter.all]
+---
+info: trees are structurally equal: true
+---
+info: with `withSetOptionIn`:
+- `linter.all := false`
+- Found option names in trees: [linter.all]
+-/
+#guard_msgs in
+run_cmd do
+  let stx ← `(command| set_option linter.all 3 in example : True := trivial)
+  elabCommand stx
+  try compareWithSetOptionIn stx catch ex =>
+    throwError "comparison produced error:\n\n{ex.toMessageData}"
+
+end infotree
diff --git a/tests/lean/withSetOptionIn.lean.expected.out b/tests/lean/withSetOptionIn.lean.expected.out
index fb4ec6f8e01b..e69de29bb2d1 100644
--- a/tests/lean/withSetOptionIn.lean.expected.out
+++ b/tests/lean/withSetOptionIn.lean.expected.out
@@ -1,10 +0,0 @@
-[debug] foo
-withSetOptionIn.lean:29:0-29:11: error: ❌️ Docstring on `#guard_msgs` does not match generated message:
-
-- info: [debug] foo
-+ trace: [debug] foo
-[debug] foo
-withSetOptionIn.lean:38:0-38:11: error: ❌️ Docstring on `#guard_msgs` does not match generated message:
-
-- info: [debug] foo
-+ trace: [debug] foo