diff --git a/tests/lean/run/grind_lint_array.lean b/tests/lean/run/grind_lint_array.lean
new file mode 100644
index 0000000000..c62a6a7e4c
--- /dev/null
+++ b/tests/lean/run/grind_lint_array.lean
@@ -0,0 +1,7 @@
+import Std
+import Lean.Elab.Tactic.Grind.Lint
+
+/-! Check Array namespace: -/
+
+#guard_msgs in
+#grind_lint check (min := 20) in Array
diff --git a/tests/lean/run/grind_lint_bitvec.lean b/tests/lean/run/grind_lint_bitvec.lean
new file mode 100644
index 0000000000..09f7bba9d7
--- /dev/null
+++ b/tests/lean/run/grind_lint_bitvec.lean
@@ -0,0 +1,17 @@
+import Std
+import Lean.Elab.Tactic.Grind.Lint
+
+/-! `BitVec` exceptions -/
+
+-- `BitVec.msb_replicate` is reasonable at 25.
+#guard_msgs in
+#grind_lint inspect (min := 30) BitVec.msb_replicate
+
+-- `BitVec.msb_signExtend` is reasonable at 22.
+#guard_msgs in
+#grind_lint inspect (min := 25)  BitVec.msb_signExtend
+
+/-! Check BitVec namespace: -/
+
+#guard_msgs in
+#grind_lint check (min := 20) in BitVec
diff --git a/tests/lean/run/grind_lint_list.lean b/tests/lean/run/grind_lint_list.lean
new file mode 100644
index 0000000000..453929ded5
--- /dev/null
+++ b/tests/lean/run/grind_lint_list.lean
@@ -0,0 +1,33 @@
+import Std
+import Lean.Elab.Tactic.Grind.Lint
+
+/-! `List` exceptions -/
+
+-- 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 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 skip List.getLast?_pmap
+
+-- TODO: `List.Sublist.eq_of_length` should probably only fire when we've already proved the hypotheses.
+
+-- `List.replicate_sublist_iff` is reasonable at 30.
+#guard_msgs in
+#grind_lint inspect (min := 30) List.replicate_sublist_iff
+
+-- `List.Sublist.append` is reasonable at 25.
+#guard_msgs in
+#grind_lint inspect (min := 25) List.Sublist.append
+
+-- `List.Sublist.middle` is reasonable at 25.
+#guard_msgs in
+#grind_lint inspect (min := 25) List.Sublist.middle
+
+/-! Check List namespace: -/
+
+#guard_msgs in
+#grind_lint check (min := 20) in List
diff --git a/tests/lean/run/grind_lint_misc.lean b/tests/lean/run/grind_lint_misc.lean
new file mode 100644
index 0000000000..a48d4dbde4
--- /dev/null
+++ b/tests/lean/run/grind_lint_misc.lean
@@ -0,0 +1,7 @@
+import Std
+import Lean.Elab.Tactic.Grind.Lint
+
+/-! Check miscellaneous namespaces: -/
+
+#guard_msgs in
+#grind_lint check (min := 20) in Acc Attr Bool Clause Const Decidable DefaultClause DHashMap Equiv ExceptT ExtDHashMap Fin Int Internal InvImage Lex LRAT Nat NormalizePattern OldCollector Option OptionT Perm Prod PSigma Quot Quotient Rat Raw ReaderT ReflCmp Setoid StateT Subrelation Subtype Sum Tactic Task Vector WellFounded
diff --git a/tests/lean/run/grind_lint_std_hashmap.lean b/tests/lean/run/grind_lint_std_hashmap.lean
new file mode 100644
index 0000000000..e822103088
--- /dev/null
+++ b/tests/lean/run/grind_lint_std_hashmap.lean
@@ -0,0 +1,7 @@
+import Std
+import Lean.Elab.Tactic.Grind.Lint
+
+/-! Check Std hash/tree map/set namespaces: -/
+
+#guard_msgs in
+#grind_lint check (min := 20) in Std.DHashMap Std.HashMap Std.HashSet Std.ExtDHashMap Std.ExtHashMap Std.ExtHashSet
diff --git a/tests/lean/run/grind_lint_std_misc.lean b/tests/lean/run/grind_lint_std_misc.lean
new file mode 100644
index 0000000000..5b998f6b37
--- /dev/null
+++ b/tests/lean/run/grind_lint_std_misc.lean
@@ -0,0 +1,7 @@
+import Std
+import Lean.Elab.Tactic.Grind.Lint
+
+/-! Check remaining Std sub-namespaces: -/
+
+#guard_msgs in
+#grind_lint check (min := 20) in Std.Do Std.Range Std.Tactic
diff --git a/tests/lean/run/grind_lint_std_treemap.lean b/tests/lean/run/grind_lint_std_treemap.lean
new file mode 100644
index 0000000000..285d212eb9
--- /dev/null
+++ b/tests/lean/run/grind_lint_std_treemap.lean
@@ -0,0 +1,7 @@
+import Std
+import Lean.Elab.Tactic.Grind.Lint
+
+/-! Check Std tree map/set namespaces: -/
+
+#guard_msgs in
+#grind_lint check (min := 20) in Std.DTreeMap Std.TreeMap Std.TreeSet Std.ExtDTreeMap Std.ExtTreeMap Std.ExtTreeSet