chore: fixing grind annotations using #grind_lint (#11206)

Slightly more extensive version of #11205, for which I want separate CI.

src/Init/Data/List/Erase.lean

@@ -291,9 +291,11 @@ theorem eraseP_comm {l : List α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) :
       · simp [h₁, h₂]
       · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]
 
+@[grind ←]
 theorem head_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).head h ∈ xs :=
   eraseP_sublist.head_mem h
 
+@[grind ←]
 theorem getLast_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).getLast h ∈ xs :=
   eraseP_sublist.getLast_mem h
 

src/Init/Data/List/Sublist.lean

@@ -212,13 +212,11 @@ theorem Sublist.head_mem (s : ys <+ xs) (h) : ys.head h ∈ xs :=
   s.mem (List.head_mem h)
 
 grind_pattern Sublist.head_mem => ys <+ xs, ys.head h
-grind_pattern Sublist.head_mem => ys.head h ∈ xs -- This is somewhat aggressive, as it initiates sublist based reasoning.
 
 theorem Sublist.getLast_mem (s : ys <+ xs) (h) : ys.getLast h ∈ xs :=
   s.mem (List.getLast_mem h)
 
 grind_pattern Sublist.getLast_mem => ys <+ xs, ys.getLast h
-grind_pattern Sublist.getLast_mem => ys.getLast h ∈ xs -- This is somewhat aggressive, as it initiates sublist based reasoning.
 
 instance : Trans (@Sublist α) Subset Subset :=
   ⟨fun h₁ h₂ => trans h₁.subset h₂⟩

tests/lean/run/grind_lint.lean

@@ -5,17 +5,15 @@
 
 -- In progress:
 
-#grind_lint check (min := 20) in List
-
 -- TODO: Not sure what to do here, see https://lean-fro.zulipchat.com/#narrow/channel/503415-grind/topic/.60.23grind_lint.60.20command/near/556730710
 #grind_lint inspect List.getLast?_concat
-#grind_lint mute List.getLast?_concat
+#grind_lint skip List.getLast?_concat
 
 -- TODO: We should consider changing the grind annotation for `List.getElem?_eq_none`
 -- so it only fires if we've already proved the hypothesis holds. (i.e. the new gadget)
 -- Other than that, everything looks sane here:
 #grind_lint inspect List.getLast?_pmap
-#grind_lint mute List.getLast?_pmap
+#grind_lint skip List.getLast?_pmap
 
 -- TODO: We should try to remove these attributes; if that's okay we can remove these mutes.
 attribute [-grind] List.Sublist.getLast_mem List.Sublist.head_mem
@@ -29,19 +27,18 @@ attribute [-grind] List.Sublist.getLast_mem List.Sublist.head_mem
 -- `List.replicate_sublist_iff` is reasonable at 30.
 #guard_msgs in
 #grind_lint inspect (min := 30) List.replicate_sublist_iff
-#grind_lint mute List.replicate_sublist_iff
+#grind_lint skip List.replicate_sublist_iff
 
 -- `List.Sublist.append` is reasonable at 25.
 #guard_msgs in
 #grind_lint inspect (min := 25) List.Sublist.append
-#grind_lint mute List.Sublist.append
+#grind_lint skip List.Sublist.append
 
 -- `List.Sublist.middle` is reasonable at 25.
 #guard_msgs in
 #grind_lint inspect (min := 25) List.Sublist.middle
-#grind_lint mute List.Sublist.middle
+#grind_lint skip List.Sublist.middle
 
--- FIXME: I think I've muted all of these, but they are still being reported.
 #grind_lint check (min := 20) in List
 
 -- TODO:

tests/lean/run/grind_list_erase.lean

@@ -23,9 +23,14 @@ theorem eraseP_append_right {l₁ : List α} {l₂} (h : ∀ b ∈ l₁, ¬p b)
     eraseP p (l₁ ++ l₂) = l₁ ++ l₂.eraseP p := by
   grind
 
-theorem head_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).head h ∈ xs := by grind
+theorem head_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).head h ∈ xs := by
+  -- This had previously been a `grind` lemma,
+  -- but it is quite aggressive as it initiates `Sublist` based reasoning.
+  grind [Sublist.head_mem]
 
-theorem getLast_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).getLast h ∈ xs := by grind
+theorem getLast_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).getLast h ∈ xs := by
+  -- As above, this had previously been a `grind` lemma.
+  grind [Sublist.getLast_mem]
 
 theorem set_getElem_succ_eraseIdx_succ
     {xs : Array α} {i : Nat} (h : i + 1 < xs.size) :