feat: show initial case goal on ... => for induction/cases/case/match

src/Lean/Elab/Tactic/Basic.lean

@@ -289,10 +289,10 @@ def admitGoal (mvarId : MVarId) : TacticM Unit := do
   assignExprMVar mvarId (← mkSorry mvarType (synthetic := true))
 
 /- Close the main goal using the given tactic. If it fails, log the error and `admit` -/
-def closeUsingOrAdmit (tac : Syntax) : TacticM Unit := do
+def closeUsingOrAdmit (tac : TacticM Unit) : TacticM Unit := do
   let mvarId :: mvarIds ← getUnsolvedGoals | throwNoGoalsToBeSolved
   try
-    focusAndDone (evalTactic tac)
+    focusAndDone tac
   catch ex =>
     logException ex
     admitGoal mvarId
@@ -542,7 +542,7 @@ def withCaseRef [Monad m] [MonadRef m] (arrow body : Syntax) (x : m α) : m α :
   withRef (mkNullNode #[arrow, body]) x
 
 @[builtinTactic «case»] def evalCase : Tactic
-  | `(tactic| case $tag $hs* =>%$arr $tac:tacticSeq) => do
+  | stx@`(tactic| case $tag $hs* =>%$arr $tac:tacticSeq) => do
     let tag := tag.getId
     let gs ← getUnsolvedGoals
     let some g ← findTag? gs tag | throwError "tag not found"
@@ -576,7 +576,7 @@ def withCaseRef [Monad m] [MonadRef m] (arrow body : Syntax) (x : m α) : m α :
     setMVarTag g Name.anonymous
     try
       withCaseRef arr tac do
-        closeUsingOrAdmit tac
+        closeUsingOrAdmit (withTacticInfoContext stx (evalTactic tac))
     finally
       setMVarTag g savedTag
     done

src/Lean/Elab/Tactic/Induction.lean

@@ -54,7 +54,7 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (remainingGoals : Array MVarId) : T
       return remainingGoals ++ gs'
     else
       setGoals [mvarId]
-      closeUsingOrAdmit rhs
+      closeUsingOrAdmit (withTacticInfoContext alt (evalTactic rhs))
       return remainingGoals
 
 /-

tests/lean/interactive/plainGoal.lean

@@ -10,3 +10,10 @@ example : α → α := by
 
 example : α → α := by
                   --^ $/lean/plainGoal
+
+example : 0 + n = n := by
+  induction n with
+  | zero => rfl
+       --^ $/lean/plainGoal
+  | succ
+   --^ $/lean/plainGoal

tests/lean/interactive/plainGoal.lean.expected.out

@@ -22,3 +22,13 @@
  "position": {"line": 10, "character": 20}}
 {"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```",
  "goals": ["α : Sort ?u\n⊢ α → α"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 15, "character": 9}}
+{"rendered": "```lean\ncase zero\n⊢ 0 + Nat.zero = Nat.zero\n```",
+ "goals": ["case zero\n⊢ 0 + Nat.zero = Nat.zero"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 17, "character": 5}}
+{"rendered":
+ "```lean\ncase succ\nn✝ : Nat\nn_ih✝ : 0 + n✝ = n✝\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝\n```",
+ "goals":
+ ["case succ\nn✝ : Nat\nn_ih✝ : 0 + n✝ = n✝\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝"]}