fix test

src/Init/Data/Array/Lemmas.lean

@@ -1277,7 +1277,9 @@ theorem forall_mem_map {f : α → β} {xs : Array α} {P : β → Prop} :
   cases xs
   simp
 
-@[grind →]
+-- This would be helpful as a `grind` lemma if
+-- we could have it fire only once `map f l` and `#[]` are the same equivalence class.
+-- Otherwise it is too aggressive.
 theorem eq_empty_of_map_eq_empty {f : α → β} {xs : Array α} (h : map f xs = #[]) : xs = #[] :=
   map_eq_empty_iff.mp h
 

src/Init/Data/List/Lemmas.lean

@@ -1162,7 +1162,9 @@ theorem forall_mem_map {f : α → β} {l : List α} {P : β → Prop} :
 @[simp] theorem map_eq_nil_iff {f : α → β} {l : List α} : map f l = [] ↔ l = [] := by
   constructor <;> exact fun _ => match l with | [] => rfl
 
-@[grind →]
+-- This would be helpful as a `grind` lemma if
+-- we could have it fire only once `map f l` and `[]` are the same equivalence class.
+-- Otherwise it is too aggressive.
 theorem eq_nil_of_map_eq_nil {f : α → β} {l : List α} (h : map f l = []) : l = [] :=
   map_eq_nil_iff.mp h
 

tests/lean/run/grind_list2.lean

@@ -1,4 +1,3 @@
-module
 -- Note that `grind_list.lean` uses `reset_grind_attrs%` to clear the grind attributes.
 -- This file does not: it is testing the grind attributes in the library.
 
@@ -456,7 +455,7 @@ theorem map_eq_cons_iff' {f : α → β} {l : List α} :
 
 theorem map_eq_singleton_iff {f : α → β} {l : List α} {b : β} :
     map f l = [b] ↔ ∃ a, l = [a] ∧ f a = b := by
-  grind [map_eq_cons_iff]
+  grind [cases List]
 
 -- FIXME
 attribute [local grind] List.map_inj_left in