fix test

src/Init/Data/Int/Order.lean

@@ -329,9 +329,9 @@ protected theorem le_iff_lt_add_one {a b : Int} : a ≤ b ↔ a < b + 1 := by
 
 /- ### min and max -/
 
-protected theorem min_def (n m : Int) : min n m = if n ≤ m then n else m := rfl
+@[grind =] protected theorem min_def (n m : Int) : min n m = if n ≤ m then n else m := rfl
 
-protected theorem max_def (n m : Int) : max n m = if n ≤ m then m else n := rfl
+@[grind =] protected theorem max_def (n m : Int) : max n m = if n ≤ m then m else n := rfl
 
 @[simp] protected theorem neg_min_neg (a b : Int) : min (-a) (-b) = -max a b := by
   rw [Int.min_def, Int.max_def]

src/Init/Data/List/Lemmas.lean

@@ -105,7 +105,7 @@ abbrev length_eq_zero := @length_eq_zero_iff
 theorem eq_nil_iff_length_eq_zero : l = [] ↔ length l = 0 :=
   length_eq_zero_iff.symm
 
-@[grind] theorem length_pos_of_mem {a : α} : ∀ {l : List α}, a ∈ l → 0 < length l
+@[grind →] theorem length_pos_of_mem {a : α} : ∀ {l : List α}, a ∈ l → 0 < length l
   | _::_, _ => Nat.zero_lt_succ _
 
 theorem exists_mem_of_length_pos : ∀ {l : List α}, 0 < length l → ∃ a, a ∈ l
@@ -185,7 +185,7 @@ theorem singleton_inj {α : Type _} {a b : α} : [a] = [b] ↔ a = b := by
 We simplify `l.get i` to `l[i.1]'i.2` and `l.get? i` to `l[i]?`.
 -/
 
-@[simp, grind]
+@[simp, grind =]
 theorem get_eq_getElem {l : List α} {i : Fin l.length} : l.get i = l[i.1]'i.2 := rfl
 
 set_option linter.deprecated false in
@@ -225,7 +225,7 @@ theorem get?_eq_getElem? {l : List α} {i : Nat} : l.get? i = l[i]? := by
 We simplify `l[i]!` to `(l[i]?).getD default`.
 -/
 
-@[simp, grind]
+@[simp, grind =]
 theorem getElem!_eq_getElem?_getD [Inhabited α] {l : List α} {i : Nat} :
     l[i]! = (l[i]?).getD (default : α) := by
   simp only [getElem!_def]
@@ -235,16 +235,16 @@ theorem getElem!_eq_getElem?_getD [Inhabited α] {l : List α} {i : Nat} :
 
 /-! ### getElem? and getElem -/
 
-@[simp, grind] theorem getElem?_nil {i : Nat} : ([] : List α)[i]? = none := rfl
+@[simp, grind =] theorem getElem?_nil {i : Nat} : ([] : List α)[i]? = none := rfl
 
 theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
     (a :: l)[i] =
       if h : i = 0 then a else l[i-1]'(match i, h with | i+1, _ => succ_lt_succ_iff.mp w) := by
   cases i <;> simp
 
-@[grind] theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := rfl
+@[grind =] theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := rfl
 
-@[simp, grind] theorem getElem?_cons_succ {l : List α} : (a::l)[i+1]? = l[i]? := rfl
+@[simp, grind =] theorem getElem?_cons_succ {l : List α} : (a::l)[i+1]? = l[i]? := rfl
 
 theorem getElem?_cons : (a :: l)[i]? = if i = 0 then some a else l[i-1]? := by
   cases i <;> simp [getElem?_cons_zero]
@@ -337,7 +337,7 @@ We simplify away `getD`, replacing `getD l n a` with `(l[n]?).getD a`.
 Because of this, there is only minimal API for `getD`.
 -/
 
-@[simp, grind]
+@[simp, grind =]
 theorem getD_eq_getElem?_getD {l : List α} {i : Nat} {a : α} : getD l i a = (l[i]?).getD a := by
   simp [getD]
 

src/Init/Data/Nat/Basic.lean

@@ -6,6 +6,7 @@ Authors: Floris van Doorn, Leonardo de Moura
 prelude
 import Init.SimpLemmas
 import Init.Data.NeZero
+import Init.Grind.Tactics
 
 set_option linter.missingDocs true -- keep it documented
 universe u
@@ -867,7 +868,7 @@ Examples:
 -/
 protected abbrev min (n m : Nat) := min n m
 
-protected theorem min_def {n m : Nat} : min n m = if n ≤ m then n else m := rfl
+@[grind =] protected theorem min_def {n m : Nat} : min n m = if n ≤ m then n else m := rfl
 
 instance : Max Nat := maxOfLe
 
@@ -884,7 +885,7 @@ Examples:
 -/
 protected abbrev max (n m : Nat) := max n m
 
-protected theorem max_def {n m : Nat} : max n m = if n ≤ m then m else n := rfl
+@[grind =] protected theorem max_def {n m : Nat} : max n m = if n ≤ m then m else n := rfl
 
 
 /-! # Auxiliary theorems for well-founded recursion -/

tests/lean/run/grind_cutsat_omega.lean

@@ -193,8 +193,6 @@ example {a₁ a₂ p₁ p₂ : Nat}
 example {i : Nat} (h1 : i < 330) (_h2 : 7 ∣ (660 + i) * (1319 - i)) : 1319 - i < 1979 := by
   grind
 
-attribute [grind =] Int.min_def Int.max_def Nat.max_def Nat.min_def
-
 example {a : Int} (_ : a < min a b) : False := by grind
 example {a : Int} (_ : max a b < b) : False := by grind
 example {a : Nat} (_ : a < min a b) : False := by grind

tests/lean/run/grind_ite_split_issue.lean

@@ -1,7 +1,5 @@
 set_option grind.warning false
 
-attribute [grind =] Int.min_def Int.max_def
-
 example (a b : Int) : min a b = 10 → a ≥ 10 := by
   grind
 

tests/lean/run/grind_min.lean

@@ -1,6 +1,4 @@
 set_option grind.warning false
-reset_grind_attrs%
-attribute [grind =] Nat.min_def -- This annotation should eventually be in the Std library
 
 example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j ≤ hi) (_ : j < as.size)
     (_ : ¬as.size = 0) : min lo (as.size - 1) ≤ i := by

tests/lean/run/grind_t1.lean

@@ -190,6 +190,7 @@ info: [grind.assert] ∀ (a : α), a ∈ b → p a
 [grind.assert] w ∈ b
 [grind.assert] ¬p w
 [grind.ematch.instance] h₁: w ∈ b → p w
+[grind.ematch.instance] List.length_pos_of_mem: w ∈ b → 0 < b.length
 [grind.assert] w ∈ b → p w
 -/
 #guard_msgs (info) in