Commit 2025-10-28 09:17 af1138bd

feat: linters to try hammers at every step (#30808) This PR adds three linters which respectively try running simp_all, aesop, and grind at each step in Mathlib. The intention is not to look at individual outputs and make replacements, but rather to use these as baselines for premise selection algorithm comparisons. In https://github.com/leanprover/lean4/pull/10920 I'm adding grind +premises (and I'd like to do the same with simp_all and aesop), and we can then measure how different premise selection algorithms compare at library scale.