fix: induction pre-tactic should be indented (#5494)

Fixes #2876

src/Init/Tactics.lean

@@ -788,7 +788,7 @@ syntax inductionAlt  := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> synth
 After `with`, there is an optional tactic that runs on all branches, and
 then a list of alternatives.
 -/
-syntax inductionAlts := " with" (ppSpace tactic)? withPosition((colGe inductionAlt)+)
+syntax inductionAlts := " with" (ppSpace colGt tactic)? withPosition((colGe inductionAlt)+)
 
 /--
 Assuming `x` is a variable in the local context with an inductive type,

tests/lean/inductionParse.lean

@@ -0,0 +1,5 @@
+/-! should not parse `done` as part of `induction` -/
+
+example (a : Nat) : True := by
+  induction a with
+  done

tests/lean/inductionParse.lean.expected.out

@@ -0,0 +1 @@
+inductionParse.lean:4:18-5:6: error: unexpected identifier; expected '|'

tests/lean/run/inductionParse.lean

@@ -1,3 +1,5 @@
+/-! should not parse `case` as a `generalizing` variable -/
+
 example (a b : Nat) : True := by
   induction a generalizing b
   case zero => trivial