diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 46c7a99954..86c8c2065f 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -243,8 +243,9 @@ private def generalizeVars (stx : Syntax) (targets : Array Expr) : TacticM Nat :
       Meta.throwTacticEx `induction mvarId "major premise depends on variable being generalized"
     pure (fvarIds.size, [mvarId'])
 
+-- syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
 private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
-  inductionAlts[1].getArgs
+  inductionAlts[2].getArgs
 
 private def getAltsOfOptInductionAlts (optInductionAlts : Syntax) : Array Syntax :=
   if optInductionAlts.isNone then #[] else getAltsOfInductionAlts optInductionAlts[0]