chore: prepare to fix ambiguity at induction/cases notation

@Kha I was writing the following example
```
  ...
  induction as
  | nil          => cases h -- `h` is an empty type
  | cons b bs ih => cases h
    | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
    | tail a b bs h1 => ...
```
The current `syntax` assumes the `| cons b bs ih => ...` alternative
is part of the first `cases h`. Forcing the `|` to occur in a column
>= of the corresponding `cases` is not a nice solution since it would
preven us from writing the second `cases` as I wrote it above.
That is we would have to write
```
  induction as
  | nil          => cases h -- `h` is an empty type
  | cons b bs ih =>
    cases h
    | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
    | tail a b bs h1 => ...
```
or
```
  induction as
  | nil          => cases h -- `h` is an empty type
  | cons b bs ih => cases h
                    | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
                    | tail a b bs h1 => ...
```
I think the best solution is to use `with` when we have explicit
alternatives with `|`. The new syntax is similar to `match ... with | ...`
That is, we would write
```
  ...
  induction as with
  | nil          => cases h
  | cons b bs ih => cases h with
    | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
    | tail a b bs h1 => ...
```

src/Lean/Elab/Tactic/Induction.lean

@@ -240,7 +240,10 @@ private def generalizeVars (stx : Syntax) (targets : Array Expr) : TacticM Nat :
     pure (fvarIds.size, [mvarId'])
 
 private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
-  inductionAlts[1].getSepArgs
+  if inductionAlts.getNumArgs == 2 then
+    inductionAlts[1].getSepArgs -- TODO remove
+  else
+    inductionAlts[2].getSepArgs
 
 private def getAltsOfOptInductionAlts (optInductionAlts : Syntax) : Array Syntax :=
   if optInductionAlts.isNone then #[] else getAltsOfInductionAlts optInductionAlts[0]