chore: clean up grind annotations (#212)

Author: TwoFX

HumanEvalLean/HumanEval11.lean

@@ -5,7 +5,7 @@ def stringXor (a b : List Bool) : List Bool :=
     |>.map (fun p => Bool.xor p.1 p.2)
     |>.toList
 
-@[simp, grind]
+@[simp, grind =]
 theorem length_stringXor {a b : List Bool} : (stringXor a b).length = min a.length b.length := by
   simp [stringXor]
 

HumanEvalLean/HumanEval3.lean

@@ -28,19 +28,19 @@ theorem hasPrefix_iff {P : List α → Prop} {l : List α} :
     l.HasPrefix P ↔ ∃ n, P (l.take n) := by
   grind [HasPrefix]
 
-@[simp, grind]
+@[simp, grind =]
 theorem hasPrefix_nil {P : List α → Prop} : [].HasPrefix P ↔ P [] := by
   simp [hasPrefix_iff]
 
-@[simp, grind]
+@[simp, grind .]
 theorem hasPrefix_of_nil {P : List α → Prop} {l : List α} (h : P []) : l.HasPrefix P :=
   ⟨⟨0, by simpa⟩⟩
 
-@[simp, grind]
+@[simp, grind .]
 theorem hasPrefix_of_all {P : List α → Prop} {l : List α} (h : P l) : l.HasPrefix P :=
   ⟨⟨l.length, by simpa⟩⟩
 
-@[grind]
+@[grind =]
 theorem hasPrefix_cons {P : List α → Prop} {a : α} {l : List α} :
     (a :: l).HasPrefix P ↔ P [] ∨ l.HasPrefix (fun l' => P (a :: l')) := by
   refine ⟨?_, ?_⟩
@@ -51,12 +51,12 @@ theorem hasPrefix_cons {P : List α → Prop} {a : α} {l : List α} :
     · exact hasPrefix_of_nil h
     · exact ⟨n + 1, by simpa⟩
 
-@[grind]
+@[grind =]
 theorem hasPrefix_append {P : List α → Prop} {l l' : List α} :
     (l ++ l').HasPrefix P ↔ l.HasPrefix P ∨ l'.HasPrefix (fun l'' => P (l ++ l'')) := by
   induction l generalizing P with grind
 
-@[grind]
+@[grind =]
 theorem sum_append_singleton_int {l₁ : List Int} {x : Int} : (l₁ ++ [x]).sum = l₁.sum + x := by
   simp [List.sum, ← List.foldr_assoc]
 

HumanEvalLean/HumanEval43.lean

@@ -14,16 +14,16 @@ theorem List.any₂_iff_not_pairwise {P : α → α → Prop} {l : List α} :
     l.Any₂ P ↔ ¬l.Pairwise (fun x y => ¬P x y) := by
   grind [List.Any₂]
 
-@[simp, grind]
+@[simp, grind .]
 theorem not_any₂_nil {P : α → α → Prop} : ¬List.Any₂ P [] := by
   simp [List.any₂_iff_not_pairwise]
 
-@[simp, grind]
+@[simp, grind =]
 theorem List.any₂_cons {P : α → α → Prop} {x : α} {xs : List α} :
     List.Any₂ P (x::xs) ↔ (∃ y ∈ xs, P x y) ∨ List.Any₂ P xs := by
   grind [List.any₂_iff_not_pairwise, pairwise_cons]
 
-@[simp, grind]
+@[simp, grind =]
 theorem List.any₂_append {P : α → α → Prop} {xs ys : List α} :
     List.Any₂ P (xs ++ ys) ↔ List.Any₂ P xs ∨ List.Any₂ P ys ∨ (∃ x ∈ xs, ∃ y ∈ ys, P x y) := by
   grind [List.any₂_iff_not_pairwise]
@@ -173,11 +173,11 @@ theorem List.any₂_iff_exists_getElem (P : α → α → Prop) (l : List α) :
     exact ⟨l.take i, l[i], l.drop (i + 1), by simp,
       (List.exists_mem_iff_exists_getElem _ _).2 ⟨j - i - 1, by grind, by grind⟩⟩
 
-@[simp, grind]
+@[simp, grind =]
 theorem List.any₂_append_singleton {P : α → α → Prop} {xs : List α} {x : α} :
     List.Any₂ P (xs ++ [x]) ↔ List.Any₂ P xs ∨ ∃ y ∈ xs, P y x := by
   grind [List.any₂_iff_not_pairwise]
 
-@[simp, grind]
+@[simp, grind .]
 theorem not_any₂_singleton {P : α → α → Prop} {x : α} : ¬List.Any₂ P [x] := by
   simp [List.any₂_iff_not_pairwise]