experiment: run hammers on Mathlib

Author: kim-em

lakefile.lean

@@ -31,6 +31,9 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.allScriptsDocumented, true⟩,
   ⟨`linter.pythonStyle, true⟩,
   ⟨`linter.style.longFile, .ofNat 1500⟩,
+  ⟨`linter.tacticAnalysis.tryAtEachStepAesop, true⟩,
+  ⟨`linter.tacticAnalysis.tryAtEachStepSimpAll, true⟩,
+  ⟨`linter.tacticAnalysis.tryAtEachStepGrind, true⟩,
   -- ⟨`linter.nightlyRegressionSet, true⟩,
   -- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
 ]