fix: report error if too many variable names have been provided at induction/cases alternative

src/Lean/Elab/Tactic/Induction.lean

@@ -210,6 +210,8 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (optPreTac :
     | some altStx =>
       subgoals ← withRef altStx do
         let altVarNames := getAltVarNames altStx
+        if altVarNames.size > numFields then
+          throwError! "too many variable names provided at alternative '{altName}', #{altVarNames.size} provided, but #{numFields} expected"
         let mut (_, altMVarId) ← introN altMVarId numFields altVarNames.toList (useNamesForExplicitOnly := !altHasExplicitModifier altStx)
         match (← Cases.unifyEqs numEqs altMVarId {}) with
         | none   => throwError! "alternative '{altName}' is not needed"

tests/lean/run/tacticTests.lean

@@ -10,7 +10,7 @@ theorem ex1 (m : Nat) : Le m 0 → m = 0 := by
 theorem ex2 (m n : Nat) : Le m n → Le m.succ n.succ := by
   intro h
   induction h with
-  | base n => apply Le.base
+  | base => apply Le.base
   | succ n m ih =>
     apply Le.succ
     apply ih

tests/lean/tooManyVarsAtInduction.lean

@@ -0,0 +1,9 @@
+theorem ex1 (n : Nat) : 0 + n = n := by
+  induction n with
+  | succ x ih₁ ih₂ ih₃ => admit
+  | zero => rfl
+
+theorem ex2 (n : Nat) : 0 + n = n := by
+  cases n with
+  | succ x ih => admit
+  | zero => rfl

tests/lean/tooManyVarsAtInduction.lean.expected.out

@@ -0,0 +1,2 @@
+tooManyVarsAtInduction.lean:3:2-3:31: error: too many variable names provided at alternative 'succ', #4 provided, but #2 expected
+tooManyVarsAtInduction.lean:8:2-8:22: error: too many variable names provided at alternative 'succ', #2 provided, but #1 expected