chore(MathlibTest/grind/lint): improve documentation (leanprover-community#32935)

This PR updates the grind_lint test file to:
- Explain why `Path.symm_apply` and `Set.Icc.convexCombo_symm` are skipped (they each instantiate 24 lemmas, which seems reasonable)
- Improve the instructions for what to do when the test fails

🤖 Prepared with Claude Code

Author: kim-em

MathlibTest/grind/lint.lean

@@ -1,15 +1,15 @@
 import Mathlib
 
-#adaptation_note
-/--
-FIXME: please investigate these lemmas, and add guard conditions as needed.
-(These appeared at nightly-2025-12-13.)
---/
+-- These each instantiate 24 further lemmas (pretty much the same ones), but they seem reasonable.
+-- We'll make an exception for this one,
+-- but if we accumulate too many we can raise the threshold below.
 #grind_lint skip Path.symm_apply
 #grind_lint skip Set.Icc.convexCombo_symm
 
 -- This check verifies that `grind` annotations in Mathlib do not trigger run-away instantiations.
--- If this test fails, please modify newly introduced `grind` annotations to use the
+-- If this test fails, please follow the "Try this:" suggestions
+-- which will explain the excessive instantations.
+-- Please modify newly introduced `grind` annotations to use the
 -- `grind_pattern ... where ...` syntax to add side conditions that will prevent the run-away.
 -- See https://lean-lang.org/doc/reference/latest/The--grind--tactic/E___matching/ for details.
 #grind_lint check (min := 20) in module Mathlib