experiment: run hammers on Mathlib

[kim-em]

This PR is just driving CI: we ask (via linters introduced in #30808) for every goal in Mathlib that can be closed by one of simp_all, aesop, or grind. We'll use these results as baselines for premise selection algorithm comparisons.

[github-actions]

PR summary 3eea33ecce

Import changes exceeding 2%

%	File
+2.27%	Mathlib.Data.String.Defs
+2.13%	Mathlib.Tactic.Linter.TextBased
+4.55%	Mathlib.Tactic.TacticAnalysis.Declarations
+2.17%	Mathlib.Tactic.ToAdditive.GuessName
+2.22%	Mathlib.Util.SleepHeartbeats
+2.27%	Mathlib.Util.Superscript

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Nat.Bitwise	384	386	+2 (+0.52%)
Mathlib.Data.Int.Bitwise	392	394	+2 (+0.51%)
Mathlib.SetTheory.Nimber.Basic	757	759	+2 (+0.26%)
Mathlib.ModelTheory.FinitelyGenerated	801	803	+2 (+0.25%)

Import changes for all files

Files	Import difference
There are 6581 files with changed transitive imports taking up over 283438 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ LawfulSingleton.insert_empty_eq'
+ check_tactic_support(locations,
+ continuous_function_at
+ count_subsets(tactic_support):
+ extract_suggestions(target):
+ format_subset(subset,
+ instance {K : Type*} [_root_.Field K] [CharZero K] : LawfulOfScientific K
+ main():
+ normalize_tactic(tactic):
+ ofList_eq
+ output_analysis(locations,
+ output_raw(locations):
+ print_table(counts,
+ sequence_tendsto
+ tryAtEachStepGrindSuggestions
+ tryAtEachStepSimpAllSuggestions
- toList_empty
- toList_inj
- tryAtEachStepGrindPremises
- xor_left_inj
- xor_left_injective
- xor_right_inj
- xor_right_injective
-+-+-+ ext

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (6.00, 0.12)

Current number	Change	Type
50	6	adaptation notes

Current commit 4f6573b2b9
Reference commit 3eea33ecce

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[kim-em]

Moved to leanprover-community#105