fix: auto-introduce in sym => mode when goal closes during preprocessing

This PR fixes a bug in `sym =>` interactive mode where satellite solvers
(`lia`, `ring`, `linarith`) would throw an internal error if their automatic
`intros + assertAll` preprocessing step already closed the goal. Previously,
`evalCheck` used `liftAction` which discarded the closure result, so the
subsequent `liftGoalM` call failed due to the absence of a main goal.
`liftAction` is now split so the caller can distinguish the closed and
subgoals cases and skip the solver body when preprocessing already finished
the job.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

src/Init/While.lean

@@ -13,11 +13,10 @@ public section
 namespace Lean
 
 /-!
-# `Loop` type backing `repeat`/`while`/`repeat ... until`
+# `while` and `repeat` loop support
 
-The parsers and elaborators for `repeat`, `while`, and `repeat ... until` live in
-`Lean.Parser.Do` and `Lean.Elab.BuiltinDo.Repeat`. This module only provides the
-`Loop` type (and `ForIn` instance) that those elaborators expand to.
+The parsers for `repeat`, `while`, and `repeat ... until` are
+`@[builtin_doElem_parser]` definitions in `Lean.Parser.Do`.
 -/
 
 inductive Loop where
@@ -34,4 +33,23 @@ partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop
 instance [Monad m] : ForIn m Loop Unit where
   forIn := Loop.forIn
 
+-- The canonical parsers for `repeat`/`while`/`repeat ... until` live in `Lean.Parser.Do`
+-- as `@[builtin_doElem_parser]` definitions. We register the expansion macros here so
+-- they are available to `prelude` files in `Init`, which do not import `Lean.Elab`.
+
+macro_rules
+  | `(doElem| repeat%$tk $seq) => `(doElem| for%$tk _ in Loop.mk do $seq)
+
+macro_rules
+  | `(doElem| while%$tk $h : $cond do $seq) =>
+    `(doElem| repeat%$tk if $h:ident : $cond then $seq else break)
+
+macro_rules
+  | `(doElem| while%$tk $cond do $seq) =>
+    `(doElem| repeat%$tk if $cond then $seq else break)
+
+macro_rules
+  | `(doElem| repeat%$tk $seq until $cond) =>
+    `(doElem| repeat%$tk do $seq:doSeq; if $cond then break)
+
 end Lean

src/Lean/Elab/Do/InferControlInfo.lean

@@ -139,14 +139,8 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     }
   | `(doRepeat| repeat $bodySeq) =>
     let info ← ofSeq bodySeq
-    -- Match `for ... in` and report `numRegularExits := 1` unconditionally. Reporting `0` when
-    -- the body has no `break` causes `ofSeq` (in any enclosing sequence whose `ControlInfo` is
-    -- inferred, e.g. a surrounding `for`/`if`/`match`/`try` body) to stop aggregating after this
-    -- element and miss any `return`/`break`/`continue` that follows. The corresponding elaborator
-    -- then sees the actual control flow disagree with the inferred info and throws errors like
-    -- "Early returning ... but the info said there is no early return". See #13437 for details.
     return { info with
-      numRegularExits := 1,
+      numRegularExits := if info.breaks then 1 else 0,
       continues := false,
       breaks := false
     }

src/Lean/Elab/PreDefinition/Basic.lean

@@ -222,8 +222,8 @@ private def addNonRecAux (docCtx : LocalContext × LocalInstances) (preDef : Pre
     if compile && shouldGenCodeFor preDef then
       compileDecl decl
     if applyAttrAfterCompilation then
-      saveEqnAffectingOptions preDef.declName
       enableRealizationsForConst preDef.declName
+      generateEagerEqns preDef.declName
     addPreDefDocs docCtx preDef
     if applyAttrAfterCompilation then
       applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation

src/Lean/Elab/PreDefinition/EqUnfold.lean

@@ -28,7 +28,7 @@ def getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
     trace[ReservedNameAction] "getConstUnfoldEqnFor? {declName} failed, no unfold theorem available"
     return none
   let name := mkEqLikeNameFor (← getEnv) declName eqUnfoldThmSuffix
-  realizeConst declName name <| withEqnOptions declName do
+  realizeConst declName name do
     -- we have to call `getUnfoldEqnFor?` again to make `unfoldEqnName` available in this context
     let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := true) declName | unreachable!
     let info ← getConstInfo unfoldEqnName

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -367,7 +367,7 @@ def mkEqns (declName : Name) (declNames : Array Name) : MetaM (Array Name) := do
     thmNames := thmNames.push name
     -- determinism: `type` should be independent of the environment changes since `baseName` was
     -- added
-    realizeConst declName name (withEqnOptions declName (doRealize name info type))
+    realizeConst declName name (doRealize name info type)
   return thmNames
 where
   doRealize name info type := withOptions (tactic.hygienic.set · false) do

src/Lean/Elab/PreDefinition/Mutual.lean

@@ -69,10 +69,8 @@ def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
           a.name = `instance_reducible || a.name = `implicit_reducible do
         setIrreducibleAttribute preDef.declName
 
-  for preDef in preDefs do
-    saveEqnAffectingOptions preDef.declName
-
   /-
+  `enableRealizationsForConst` must happen before `generateEagerEqns`
   It must happen in reverse order so that constants realized as part of the first decl
   have realizations for the other ones enabled
   -/
@@ -80,6 +78,7 @@ def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
     enableRealizationsForConst preDef.declName
 
   for preDef in preDefs do
+    generateEagerEqns preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
 end Lean.Elab.Mutual

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -163,7 +163,7 @@ public def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (r
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
   let name := mkEqLikeNameFor (← getEnv) info.declName unfoldThmSuffix
-  realizeConst info.declNames[0]! name (withEqnOptions declName (doRealize name))
+  realizeConst info.declNames[0]! name (doRealize name)
   return name
 where
   doRealize name := withOptions (tactic.hygienic.set · false) do

src/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -208,11 +208,11 @@ def structuralRecursion
         -/
         registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos fixedParamPerms
     addSmartUnfoldingDef docCtx preDef recArgPos
-  for preDef in preDefs do
-    saveEqnAffectingOptions preDef.declName
   for preDef in preDefs do
     -- must happen in separate loop so realizations can see eqnInfos of all other preDefs
     enableRealizationsForConst preDef.declName
+    -- must happen after `enableRealizationsForConst`
+    generateEagerEqns preDef.declName
   applyAttributesOf preDefsNonRec AttributeApplicationTime.afterCompilation
 
 

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -497,21 +497,14 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
 /--
   Searches for a metavariable `g` s.t. `tag` is its exact name.
   If none then searches for a metavariable `g` s.t. `tag` is a suffix of its name.
-  If none, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name.
-
-  We erase macro scopes from the metavariable's user name before comparing, so that
-  user-written tags match even when a previous tactic left hygienic macro scopes at
-  the end of the tag (e.g. `e_a.yield._@._internal._hyg.0`, where `yield` is not the
-  literal last component of the name). Case tags written by the user are never
-  macro-scoped, so erasing scopes on the mvar side is sufficient.
--/
+  If none, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. -/
 private def findTag? (mvarIds : List MVarId) (tag : Name) : TacticM (Option MVarId) := do
-  match (← mvarIds.findM? fun mvarId => return tag == (← mvarId.getDecl).userName.eraseMacroScopes) with
+  match (← mvarIds.findM? fun mvarId => return tag == (← mvarId.getDecl).userName) with
   | some mvarId => return mvarId
   | none =>
-  match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← mvarId.getDecl).userName.eraseMacroScopes) with
+  match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← mvarId.getDecl).userName) with
   | some mvarId => return mvarId
-  | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← mvarId.getDecl).userName.eraseMacroScopes
+  | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← mvarId.getDecl).userName
 
 private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List MVarId) := do
   let gs ← getUnsolvedGoals

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -68,10 +68,7 @@ def setGoals (goals : List Goal) : GrindTacticM Unit :=
 
 def pruneSolvedGoals : GrindTacticM Unit := do
   let gs ← getGoals
-  let gs ← gs.filterM fun g => do
-    if g.inconsistent then return false
-    -- The metavariable may have been assigned by `isDefEq`
-    return !(← g.mvarId.isAssigned)
+  let gs := gs.filter fun g => !g.inconsistent
   setGoals gs
 
 def getUnsolvedGoals : GrindTacticM (List Goal) := do

src/Lean/Meta/Eqns.lean

@@ -37,17 +37,12 @@ register_builtin_option backward.eqns.deepRecursiveSplit : Bool := {
 These options affect the generation of equational theorems in a significant way. For these, their
 value at definition time, not realization time, should matter.
 
-This is implemented by storing their values at definition time (when non-default) in an environment
-extension, and restoring them when the equations are lazily realized.
+This is implemented by
+ * eagerly realizing the equations when they are set to a non-default value
+ * when realizing them lazily, reset the options to their default
 -/
 def eqnAffectingOptions : Array (Lean.Option Bool) := #[backward.eqns.nonrecursive, backward.eqns.deepRecursiveSplit]
 
-/-- Environment extension that stores the values of `eqnAffectingOptions` at definition time,
-keyed by declaration name. Only populated when at least one option has a non-default value.
-Stores an association list of (option name, value) pairs for options that differ from defaults. -/
-builtin_initialize eqnOptionsExt : MapDeclarationExtension (Array (Name × DataValue)) ←
-  mkMapDeclarationExtension (asyncMode := .local)
-
 def eqnThmSuffixBase := "eq"
 def eqnThmSuffixBasePrefix := eqnThmSuffixBase ++ "_"
 def eqn1ThmSuffix := eqnThmSuffixBasePrefix ++ "1"
@@ -158,30 +153,12 @@ structure EqnsExtState where
 builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
   registerEnvExtension (pure {}) (asyncMode := .local)
 
-/--
-Runs `act` with the equation-affecting options restored to the values stored for `declName`
-at definition time (or reset to their defaults if none were stored). Use this inside
-`realizeConst` callbacks, which otherwise see the caller-independent `ctx.opts` rather than
-the outer `getEqnsFor?` context. -/
-def withEqnOptions (declName : Name) (act : MetaM α) : MetaM α := do
-  let env ← getEnv
-  let setOpts : Options → Options :=
-    if let some values := eqnOptionsExt.find? env declName then
-      fun os => Id.run do
-        let mut os := eqnAffectingOptions.foldl (fun os o => o.set os o.defValue) os
-        for (name, v) in values do
-          os := os.insert name v
-        return os
-    else
-      fun os => eqnAffectingOptions.foldl (fun os o => o.set os o.defValue) os
-  withOptions setOpts act
-
 /--
 Simple equation theorem for nonrecursive definitions.
 -/
 def mkSimpleEqThm (declName : Name) (name : Name) : MetaM (Option Name) := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
-    realizeConst declName name (withEqnOptions declName (doRealize name info))
+    realizeConst declName name (doRealize name info)
     return some name
   else
     return none
@@ -252,22 +229,19 @@ private def getEqnsFor?Core (declName : Name) : MetaM (Option (Array Name)) := w
 Returns equation theorems for the given declaration.
 -/
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := withLCtx {} {} do
-  withEqnOptions declName do
+  -- This is the entry point for lazy equation generation. Ignore the current value
+  -- of the options, and revert to the default.
+  withOptions (eqnAffectingOptions.foldl fun os o => o.set os o.defValue) do
     getEqnsFor?Core declName
 
 /--
-If any equation theorem affecting option is not the default value, store the option values
-for later use during lazy equation generation.
+If any equation theorem affecting option is not the default value, create the equations now.
 -/
-def saveEqnAffectingOptions (declName : Name) : MetaM Unit := do
+def generateEagerEqns (declName : Name) : MetaM Unit := do
   let opts ← getOptions
-  let mut nonDefaults : Array (Name × DataValue) := #[]
-  for o in eqnAffectingOptions do
-    if o.get opts != o.defValue then
-      nonDefaults := nonDefaults.push (o.name, KVMap.Value.toDataValue (o.get opts))
-  unless nonDefaults.isEmpty do
-    trace[Elab.definition.eqns] "saving equation-affecting options for {declName}"
-    modifyEnv (eqnOptionsExt.insert · declName nonDefaults)
+  if eqnAffectingOptions.any fun o => o.get opts != o.defValue then
+    trace[Elab.definition.eqns] "generating eager equations for {declName}"
+    let _ ← getEqnsFor?Core declName
 
 @[expose] def GetUnfoldEqnFn := Name → MetaM (Option Name)
 

src/Lean/Meta/Tactic/Apply.lean

@@ -128,6 +128,7 @@ def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array
     (synthAssignedInstances := true) (allowSynthFailures := false) : MetaM Unit := do
   synthAppInstances tacticName mvarId newMVars binderInfos synthAssignedInstances allowSynthFailures
   -- TODO: default and auto params
+  appendParentTag mvarId newMVars binderInfos
 
 private def dependsOnOthers (mvar : Expr) (otherMVars : Array Expr) : MetaM Bool :=
   otherMVars.anyM fun otherMVar => do
@@ -222,7 +223,6 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
     let e ← instantiateMVars e
     mvarId.assign (mkAppN e newMVars)
     let newMVars ← newMVars.filterM fun mvar => not <$> mvar.mvarId!.isAssigned
-    appendParentTag mvarId newMVars binderInfos
     let otherMVarIds ← getMVarsNoDelayed e
     let newMVarIds ← reorderGoals newMVars cfg.newGoals
     let otherMVarIds := otherMVarIds.filter fun mvarId => !newMVarIds.contains mvarId

src/Lean/Meta/Tactic/Rewrite.lean

@@ -82,7 +82,6 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           postprocessAppMVars `rewrite mvarId newMVars binderInfos
             (synthAssignedInstances := !tactic.skipAssignedInstances.get (← getOptions))
           let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
-          appendParentTag mvarId newMVars binderInfos
           let otherMVarIds ← getMVarsNoDelayed heqIn
           let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)
           let newMVarIds := newMVarIds ++ otherMVarIds

src/Lean/Meta/WrapInstance.lean

@@ -145,6 +145,7 @@ public partial def wrapInstance (inst expectedType : Expr) (compile : Bool := tr
           else
             let name ← mkAuxDeclName
             let wrapped ← mkAuxDefinition name expectedType inst (compile := false)
+            setReducibilityStatus name .implicitReducible
             if isMeta then modifyEnv (markMeta · name)
             if compile then
               compileDecls (logErrors := logCompileErrors) #[name]

tests/elab/1856.lean.out.expected

@@ -1,3 +1,4 @@
+case h
 α : Type ?u
 inst✝ : DecidableEq α
 i : α

tests/elab/2042.lean

@@ -2,7 +2,8 @@
   2 * a
 
 /--
-trace: x : Nat
+trace: case h
+x : Nat
 ⊢ 2 * x = x + x
 -/
 #guard_msgs in
@@ -18,7 +19,8 @@ by
   | a => 2 * a
 
 /--
-trace: x : Nat
+trace: case h
+x : Nat
 ⊢ 2 * x = x + x
 -/
 #guard_msgs in

tests/elab/apply_subgoal_name_issue.lean

@@ -1,18 +0,0 @@
-/-!
-Regression test: `case <ctor>` must keep working after `congr; ext _; cases _`
-even though the subgoal tags produced by `apply`-family tactics now inherit
-the parent tag (without appending the binder name) when only one subgoal is
-left. The case-tag matcher erases macro scopes so that `case yield` still
-matches tags like `e_a.yield._@._internal._hyg.0`.
--/
-
-example {δ : Type} {m : Type → Type} [Monad m] [LawfulMonad m]
-    (x : m (ForInStep δ))
-    (f g : ForInStep δ → m (ForInStep δ))
-    (h : ∀ a, f a = g a) :
-    (x >>= f) = (x >>= g) := by
-  congr
-  ext step
-  cases step
-  case yield => apply h
-  case done  => apply h

tests/elab/consumePPHint.lean.out.expected

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

tests/elab/convInConv.lean.out.expected

@@ -10,6 +10,7 @@ y : Nat
 | (fun x => x + y = 0) = fun x => False
 y : Nat
 | fun x => x + y = 0
+case h
 y x : Nat
 | y + x = 0
 y : Nat

tests/elab/inductionCheckAltNames.lean

@@ -10,7 +10,7 @@ axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat)
 error: Invalid alternative name `lower2`: Expected `lower`
 ---
 error: unsolved goals
-case upper
+case upper.h
 q d : Nat
 ⊢ q + d.succ > q
 ---
@@ -62,7 +62,7 @@ theorem invalidWildCard (p: Nat) : p ≤ q ∨ p > q := by
 error: Invalid alternative name `lower2`: There are no unhandled alternatives
 ---
 error: unsolved goals
-case lower
+case lower.h
 p delta✝ : Nat
 ⊢ p > p + delta✝.succ
 -/

tests/elab/inferInstanceAs.lean

@@ -46,7 +46,7 @@ instCD2._aux_1
 #guard_msgs in
 #print instCD2
 /--
-info: private def instCD2._aux_1 : C D2 :=
+info: @[implicit_reducible] private def instCD2._aux_1 : C D2 :=
 instCI2
 -/
 #guard_msgs in

tests/elab/meta.lean

@@ -100,6 +100,7 @@ x y : Nat
 h : x = y
 ⊢ y = x
 -----
+case h
 x y : Nat
 h : x = y
 ⊢ x = y

tests/elab/newdo.lean

@@ -489,18 +489,4 @@ example : IO Bool := do
   for (x, y) in ([] : List (Nat × Nat)) do count := count + 1
   return Float.abs count > 0
 
--- A `repeat` (without `break`) followed by an early `return` inside an enclosing `for`. The for
--- elaborator computes the loop body's `ControlInfo` via `inferControlInfoSeq`, which stops
--- aggregating once it encounters an element with `numRegularExits := 0`. If `repeat` reported
--- `numRegularExits := 0` for break-less bodies, the trailing `return 2` would be skipped during
--- inference and the for elaborator would later throw "Early returning ... but the info said there
--- is no early return". This test pins down that `repeat` reports `numRegularExits := 1`, matching
--- `for ... in`.
-example : IO Nat := do
-  for _ in [1, 2] do
-    repeat
-      pure ()
-    return 2
-  return 1
-
 end Repros

tests/elab/rflTacticErrors.lean

@@ -505,24 +505,28 @@ is not definitionally equal to the right-hand side
 example : S true false  := by with_reducible apply_rfl -- Error
 /--
 error: unsolved goals
+case a
 ⊢ true = true
 -/
 #guard_msgs in
 example : S true true   := by apply_rfl -- Error (left-over goal)
 /--
 error: unsolved goals
+case a
 ⊢ true = true
 -/
 #guard_msgs in
 example : S true true   := by with_reducible apply_rfl -- Error (left-over goal)
 /--
 error: unsolved goals
+case a
 ⊢ false = true
 -/
 #guard_msgs in
 example : S false false := by apply_rfl -- Error (left-over goal)
 /--
 error: unsolved goals
+case a
 ⊢ false = true
 -/
 #guard_msgs in

tests/elab/sym_interactive_bugs.lean

@@ -14,8 +14,3 @@ example (x y : Nat) (h : x ≤ y) : (1 - 1) + x  ≤ y + (1 + 0) := by
     simp chainSimp
     -- In the following tactic the goal is closed while preprocessing the target
     lia
-
-example : ∃ x, x = a := by
-  sym =>
-    apply Exists.intro
-    apply Eq.refl

tests/elab_fail/conv1.lean.out.expected

@@ -9,13 +9,14 @@ x y : Nat
 case x
 x y : Nat
 ⊢ x + y = y.add x
+case a
 a b : Nat
 | foo (0 + a) (b + 0)
-case x
+case a.x
 a b : Nat
 | 0 + a
 
-case y
+case a.y
 a b : Nat
 | b + 0
 a b : Nat
@@ -54,10 +55,13 @@ x y : Nat
 ⊢ f x (x.add y) y = y + x
 x y : Nat
 | x + y
+case h.h
 a b : Nat
 | 0 + a + b
+case h.h
 a b : Nat
 | a + b
+case h.h
 a b : Nat
 | 0 + a + b
 p : Nat → Prop
@@ -79,6 +83,7 @@ x : Nat
 p : Prop
 x : Nat
 ⊢ (True → p) → p
+case h
 x : Nat
 | 0 + x
 p : Prop

tests/elab_fail/decreasing_by.lean.out.expected

@@ -19,6 +19,7 @@ n m : Nat
 n m : Nat
 ⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (dec1 n, 100) (n, m)
 decreasing_by.lean:85:0-85:22: error: unsolved goals
+case a
 n m : Nat
 ⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (n, dec2 m) (n, m)
 

tests/elab_fail/inductionErrors.lean.out.expected

@@ -1,9 +1,9 @@
 inductionErrors.lean:11:12-11:27: error: unsolved goals
-case lower
+case lower.h
 p d : Nat
 ⊢ p ≤ p + d.succ
 inductionErrors.lean:12:12-12:27: error: unsolved goals
-case upper
+case upper.h
 q d : Nat
 ⊢ q + d.succ > q
 inductionErrors.lean:16:19-16:26: error(lean.unknownIdentifier): Unknown identifier `elimEx2`

tests/elab_fail/mutwf1.lean.out.expected

@@ -1,4 +1,5 @@
 mutwf1.lean:21:2-21:6: error: unsolved goals
+case h.a
 n : Nat
 h : n ≠ 0
 ⊢ n.sub 0 ≠ 0
@@ -6,5 +7,6 @@ mutwf1.lean:31:22-31:29: error: failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
+case h
 n : Nat
 ⊢ n + 1 < n

tests/server_interactive/6594.lean.out.expected

@@ -4,11 +4,12 @@
  "goals": ["case right\n⊢ True"]}
 {"textDocument": {"uri": "file:///6594.lean"},
  "position": {"line": 9, "character": 2}}
-{"rendered": "```lean\n⊢ True ∧ True\n```", "goals": ["⊢ True ∧ True"]}
+{"rendered": "```lean\ncase a\n⊢ True ∧ True\n```",
+ "goals": ["case a\n⊢ True ∧ True"]}
 {"textDocument": {"uri": "file:///6594.lean"},
  "position": {"line": 13, "character": 2}}
-{"rendered": "```lean\ncase right\n⊢ True\n```",
- "goals": ["case right\n⊢ True"]}
+{"rendered": "```lean\ncase a.right\n⊢ True\n```",
+ "goals": ["case a.right\n⊢ True"]}
 {"textDocument": {"uri": "file:///6594.lean"},
  "position": {"line": 20, "character": 2}}
 {"rendered": "```lean\ncase right\n⊢ True\n```",