fix: default parameter value in constructor footgun at cases tactic

This PR fixes another instance of the “default parameter value in
constructor” footgun, which was affecting the `cases` tactic in the
`grind` interactive mode.

src/Lean/Meta/Tactic/Grind/Split.lean

@@ -503,7 +503,7 @@ Tries to perform a case-split using `c`. Returns `none` if `c` has already been
 is not ready.
 -/
 def split? (c : SplitInfo) : SearchM (Option (List Goal × Nat)) := do
-  let .ready numCases isRec ← checkSplitStatus c | return none
+  let .ready numCases isRec _ ← checkSplitStatus c | return none
   let mvarId := (← getGoal).mvarId
   return some (← splitCore mvarId c numCases isRec)
 

tests/lean/run/grind_ite_trace.lean

@@ -93,8 +93,8 @@ theorem normalize_spec (assign : Std.HashMap Nat Bool) (e : IfExpr) :
   next => grind => finish?
   next => grind => finish?
   next => grind => finish?
-  next => grind => finish -- TODO: ensure `finish?` works here
-  next => grind => finish -- TODO: ensure `finish?` works here
+  next => grind => finish?
+  next => grind => finish?
   next => grind => finish?
 
 example (assign : Std.HashMap Nat Bool) (e : IfExpr) :
@@ -108,6 +108,6 @@ example (assign : Std.HashMap Nat Bool) (e : IfExpr) :
   next => grind => finish?
   next => grind => finish?
   next => grind => finish?
-  next => grind => finish -- TODO: ensure `finish?` works here
-  next => grind => finish -- TODO: ensure `finish?` works here
+  next => grind => finish?
+  next => grind => finish?
   next => grind => finish?