test: split grind_lint.lean into 7 smaller files for faster CI (#11271)

This PR splits the single grind_lint.lean test (50+ seconds) into 7
separate files that each run in under 7 seconds:

- grind_lint_list.lean (5.7s): List namespace with exceptions
- grind_lint_array.lean (4.6s): Array namespace
- grind_lint_bitvec.lean (3.9s): BitVec namespace with exceptions
- grind_lint_std_hashmap.lean (6.8s): Std hash map/set namespaces
- grind_lint_std_treemap.lean (~6s): Std tree map/set namespaces
- grind_lint_std_misc.lean (~5s): Std.Do, Std.Range, Std.Tactic
- grind_lint_misc.lean (5.5s): All other non-Lean namespaces

Each file maintains complete namespace coverage and preserves all
existing exceptions. The split enables better CI parallelization and
faster feedback.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude <noreply@anthropic.com>

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

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

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

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

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

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

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