chore: move fixed tests

src/Init/Grind/Norm.lean

@@ -147,5 +147,8 @@ init_grind_norm
   Int.Linear.sub_fold Int.Linear.neg_fold
   -- Int divides
   Int.one_dvd Int.zero_dvd
+  -- Function composition
+  Function.const_apply Function.comp_apply Function.const_comp
+  Function.comp_const Function.true_comp Function.false_comp
 
 end Lean.Grind

tests/lean/grind/list_problems.lean

@@ -17,14 +17,3 @@ attribute [grind] List.getElem_append_left List.getElem_append_right
   subst h; grind
 -- [issue] failed to create E-match local theorem for
 --   ∀ (h₁ : True), (l ++ [a])[l.length] = [a][l.length - l.length]
-
-
-attribute [grind] List.map_nil List.map_cons
-attribute [grind] List.any_nil List.any_cons
-attribute [grind] List.all_nil List.all_cons
-
-@[simp] theorem any_map {l : List α} {p : β → Bool} : (l.map f).any p = l.any (p ∘ f) := by
-  induction l <;> grind -- Seems to have trouble with the Boolean `||`
-
-@[simp] theorem all_map {l : List α} {p : β → Bool} : (l.map f).all p = l.all (p ∘ f) := by
-  induction l <;> grind -- Seems to have trouble with the Boolean `&&`

tests/lean/run/grind_list_issue.lean

@@ -1,9 +1,19 @@
 reset_grind_attrs%
+set_option grind.warning false
 open List Nat
 
 attribute [grind] List.filter_nil List.filter_cons
 attribute [grind] List.any_nil List.any_cons
 
-@[simp] theorem any_filter {l : List α} {p q : α → Bool} :
+theorem any_filter {l : List α} {p q : α → Bool} :
     (filter p l).any q = l.any fun a => p a && q a := by
   induction l <;> grind
+
+attribute [grind] List.map_nil List.map_cons
+attribute [grind] List.all_nil List.all_cons
+
+theorem any_map {l : List α} {p : β → Bool} : (l.map f).any p = l.any (p ∘ f) := by
+  induction l <;> grind
+
+theorem all_map {l : List α} {p : β → Bool} : (l.map f).all p = l.all (p ∘ f) := by
+  induction l <;> grind