fix: index out of bounds

src/Lean/Meta/Match/MatchEqs.lean

@@ -58,6 +58,9 @@ structure MatchEqns where
   splitterAltNumParams : Array Nat
   deriving Inhabited, Repr
 
+def MatchEqns.size (e : MatchEqns) : Nat :=
+  e.eqnNames.size
+
 structure MatchEqnsExtState where
   map : Std.PHashMap Name MatchEqns := {}
   deriving Inhabited

src/Lean/Meta/Tactic/Split.lean

@@ -97,6 +97,8 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le
     let splitter := mkAppN (mkApp splitter motive) discrsNew
     check splitter
     let mvarIds ← apply mvarId splitter
+    unless mvarIds.length == matchEqns.size do
+      throwError "'applyMatchSplitter' failed, unexpected number of goals created after applying splitter for '{matcherDeclName}'."
     let (_, mvarIds) ← mvarIds.foldlM (init := (0, [])) fun (i, mvarIds) mvarId => do
       let numParams := matchEqns.splitterAltNumParams[i]
       let (_, mvarId) ← introN mvarId numParams