chore: fix tests

tests/lean/run/grind_split_issue.lean

@@ -5,25 +5,44 @@ inductive X : Nat → Prop
 
 /--
 error: `grind` failed
-case grind.1
+case grind.1.1
 c : Nat
 q : X c 0
+s✝ : Nat
+h✝² : 0 = s✝
+h✝¹ : HEq ⋯ ⋯
 s : Nat
-h✝ : 0 = s
+h✝ : c = s
 h : HEq ⋯ ⋯
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
     [prop] X c 0
-    [prop] 0 = s
+    [prop] X c 0
+    [prop] X c c → X c 0
+    [prop] X c c
+    [prop] 0 = s✝
+    [prop] HEq ⋯ ⋯
+    [prop] c = s
     [prop] HEq ⋯ ⋯
   [eqc] True propositions
     [prop] X c 0
+    [prop] X c c → X c 0
+    [prop] X c c
+    [prop] X c s✝
     [prop] X c s
   [eqc] Equivalence classes
-    [eqc] {s, 0}
+    [eqc] {c, s}
+    [eqc] {s✝, 0}
+  [ematch] E-matching patterns
+    [thm] X.f: [X #1 #0]
+    [thm] X.g: [X #2 #1]
 [grind] Issues
-  [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
+  [issue] #2 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
+[grind] Counters
+  [thm] E-Matching instances
+    [thm] X.f ↦ 2
+    [thm] X.g ↦ 2
 -/
 #guard_msgs (error) in
 example {c : Nat} (q : X c 0) : False := by

tests/lean/run/grind_t1.lean

@@ -300,7 +300,7 @@ example : (replicate n a).map f = replicate n (f a) := by
 
 open List in
 example : (replicate n a).map f = replicate n (f a) := by
-  grind only [Exists, Option.map_some', Option.map_none', getElem?_map, getElem?_replicate]
+  grind only [cases Exists, Option.map_some', Option.map_none', getElem?_map, getElem?_replicate]
 
 open List in
 example : (replicate n a).map f = replicate n (f a) := by