diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index dd2874c965..72e333f66f 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -268,9 +268,9 @@ syntax (name := case') "case' " sepBy1(caseArg, " | ") " => " tacticSeq : tactic
 `next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
 inaccessible names to the given names.
 -/
-macro "next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
+macro nextTk:"next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
   -- Limit ref variability for incrementality; see Note [Incremental Macros]
-  withRef arrowTk `(tactic| case _ $args* =>%$arrowTk $tac)
+  withRef arrowTk `(tactic| case%$nextTk _ $args* =>%$arrowTk $tac)
 
 /-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
 syntax (name := allGoals) "all_goals " tacticSeq : tactic
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 20b2c5e71e..eb5ae628b0 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -135,13 +135,21 @@ open Meta
   | _                                                => 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          : $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 by%$b $tac:tacticSeq; $body) => `(have%$tk $x : $type := $body; by%$b $tac)
-  | `(suffices%$tk _%$x          : $type by%$b $tac:tacticSeq; $body) => `(have%$tk _%$x : $type := $body; by%$b $tac)
-  | `(suffices%$tk $hy:hygieneInfo $type by%$b $tac:tacticSeq; $body) => `(have%$tk $hy:hygieneInfo : $type := $body; by%$b $tac)
-  | _                                                                 => Macro.throwUnsupported
+  | `(suffices%$tk $x:ident      : $type from $val; $body)   => `(have%$tk $x : $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)
+  | `(suffices%$tk _%$x          : $type $b:byTactic'; $body) =>
+    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
+    `(have%$tk _%$x : $type := $body; $b:byTactic)
+  | `(suffices%$tk $hy:hygieneInfo $type $b:byTactic'; $body) =>
+    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
+    `(have%$tk $hy:hygieneInfo : $type := $body; $b:byTactic)
+  | _ => Macro.throwUnsupported
 
 open Lean.Parser in
 private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 65acc41907..ac150cf623 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -520,7 +520,7 @@ where
 
 @[builtin_tactic «case», builtin_incremental]
 def evalCase : Tactic
-  | stx@`(tactic| case $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>
+  | stx@`(tactic| case%$caseTk $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>
     -- disable incrementality if body is run multiple times
     Term.withoutTacticIncrementality (tag.size > 1) do
       for tag in tag, hs in hs do
@@ -528,20 +528,20 @@ def evalCase : Tactic
         let g ← renameInaccessibles g hs
         setGoals [g]
         g.setTag Name.anonymous
-        withCaseRef arr tac <| closeUsingOrAdmit <| withTacticInfoContext stx <|
+        withCaseRef arr tac <| closeUsingOrAdmit <| withTacticInfoContext (mkNullNode #[caseTk, arr]) <|
           Term.withNarrowedArgTacticReuse (argIdx := 3) (evalTactic ·) stx
         setGoals gs
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic «case'»] def evalCase' : Tactic
-  | `(tactic| case' $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
+  | `(tactic| case'%$caseTk $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
     let mut acc := #[]
     for tag in tag, hs in hs do
       let (g, gs) ← getCaseGoals tag
       let g ← renameInaccessibles g hs
       let mvarTag ← g.getTag
       setGoals [g]
-      withCaseRef arr tac (evalTactic tac)
+      withCaseRef arr tac <| withTacticInfoContext (mkNullNode #[caseTk, arr]) <| evalTactic tac
       let gs' ← getUnsolvedGoals
       if let [g'] := gs' then
         g'.setTag mvarTag
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 5c6e5ff2eb..9235f96f4a 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -27,8 +27,10 @@ open Meta
   syntax inductionAlt  := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> syntheticHole <|> tacticSeq)
   ```
 -/
+private def getAltLhses (alt : Syntax) : Syntax :=
+  alt[0]
 private def getFirstAltLhs (alt : Syntax) : Syntax :=
-  alt[0][0]
+  (getAltLhses alt)[0]
 /-- Return `inductionAlt` name. It assumes `alt` does not have multiple `inductionAltLHS` -/
 private def getAltName (alt : Syntax) : Name :=
   let lhs := getFirstAltLhs alt
@@ -70,7 +72,9 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) : Tactic
       let goals ← getGoals
       try
         setGoals [mvarId]
-        closeUsingOrAdmit (withTacticInfoContext alt (addInfo *> evalTactic rhs))
+        closeUsingOrAdmit <|
+          withTacticInfoContext (mkNullNode #[getAltLhses alt, getAltDArrow alt]) <|
+            (addInfo *> evalTactic rhs)
       finally
         setGoals goals
 
diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out
index f104f23ad6..aef0080bff 100644
--- a/tests/lean/1021.lean.expected.out
+++ b/tests/lean/1021.lean.expected.out
@@ -1,8 +1,8 @@
 some
   {
     range :=
-      { pos := { line := 194, column := 42 }, charUtf16 := 42, endPos := { line := 200, column := 31 },
+      { pos := { line := 202, column := 42 }, charUtf16 := 42, endPos := { line := 208, column := 31 },
         endCharUtf16 := 31 },
     selectionRange :=
-      { pos := { line := 194, column := 46 }, charUtf16 := 46, endPos := { line := 194, column := 58 },
+      { pos := { line := 202, column := 46 }, charUtf16 := 46, endPos := { line := 202, column := 58 },
         endCharUtf16 := 58 } }
diff --git a/tests/lean/interactive/2881.lean b/tests/lean/interactive/2881.lean
new file mode 100644
index 0000000000..6c50ba9577
--- /dev/null
+++ b/tests/lean/interactive/2881.lean
@@ -0,0 +1,49 @@
+example (n : Nat) : True := by
+  induction n
+  case zero => sorry -- `zero` goal
+ --^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  case zero => sorry
+     -- `succ` goal
+--^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  case' zero => sorry -- `zero` goal
+ --^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  case' zero => sorry
+     -- `succ` goal
+--^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  next => sorry -- `zero` goal
+ --^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  next => sorry
+     -- `succ` goal
+--^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n with
+  | zero => sorry -- `zero` goal
+ --^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n with
+  | zero => sorry
+    -- General goal
+--^ $/lean/plainGoal
+
+example : True := by
+  suffices True by
+      -- Goal assuming `True`
+  --^ $/lean/plainGoal
+    sorry
diff --git a/tests/lean/interactive/2881.lean.expected.out b/tests/lean/interactive/2881.lean.expected.out
new file mode 100644
index 0000000000..6afd534d60
--- /dev/null
+++ b/tests/lean/interactive/2881.lean.expected.out
@@ -0,0 +1,31 @@
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 2, "character": 3}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 8, "character": 2}}
+{"rendered": "```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```",
+ "goals": ["case succ\nn✝ : Nat\na✝ : True\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 13, "character": 3}}
+{"rendered": "```lean\ncase zero\n⊢ True\n```", "goals": ["case zero\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 19, "character": 2}}
+{"rendered": "```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```",
+ "goals": ["case succ\nn✝ : Nat\na✝ : True\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 24, "character": 3}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 30, "character": 2}}
+{"rendered": "```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```",
+ "goals": ["case succ\nn✝ : Nat\na✝ : True\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 35, "character": 3}}
+{"rendered": "```lean\ncase zero\n⊢ True\n```", "goals": ["case zero\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 41, "character": 2}}
+{"rendered": "```lean\nn : Nat\n⊢ True\n```", "goals": ["n : Nat\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 46, "character": 4}}
+{"rendered": "```lean\nthis : True\n⊢ True\n```",
+ "goals": ["this : True\n⊢ True"]}