From f80597fe680926faafab5a257519b7299e21ec39 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 29 Jan 2025 09:59:25 -0800
Subject: [PATCH] chore: fix tests

---
 tests/lean/run/grind_split_issue.lean | 29 ++++++++++++++++++++++-----
 tests/lean/run/grind_t1.lean          |  2 +-
 2 files changed, 25 insertions(+), 6 deletions(-)

diff --git a/tests/lean/run/grind_split_issue.lean b/tests/lean/run/grind_split_issue.lean
index ea54d7cdd649..7073ed6b39c1 100644
--- a/tests/lean/run/grind_split_issue.lean
+++ b/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
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index 8a95221d8156..9d1904035d0c 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/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