chore: reduce imports

[JovanGerb]

This is a test to see how much imports can be reduced.

---

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for 4bdcb37 against 07107e4 are in. There are significant results. @JovanGerb

• ✅ build//instructions: -5.6T (-3.46%)

Large changes (3✅)

• ✅ build//instructions: -5.6T (-3.46%)
• ✅ build//wall-clock: -24s (-4.40%)
• ✅ build/profile/import//wall-clock: -20m 10s (-17.05%)

and 1 hidden

Medium changes (16✅)

• ✅ build/module/Aesop.Frontend.Basic//instructions: -1.1G (-48.31%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Frontend.Tactic//instructions: -1.3G (-21.73%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Index.DiscrTreeConfig//instructions: -1.0G (-47.38%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Options.Public//instructions: -1.1G (-34.80%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.RuleSet.Name//instructions: -1.1G (-54.04%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.RuleTac.Forward//instructions: -1.4G (-16.25%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Script.GoalWithMVars//instructions: -1.0G (-46.31%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Script.SpecificTactics//instructions: -1.4G (-12.60%)
• ✅ build/module/Aesop.Script.Tactic//instructions: -1.0G (-47.60%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Script.TacticState//instructions: -1.1G (-35.98%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Util.Basic//instructions: -1.2G (-12.21%)
• ✅ build/module/Aesop.Util.Tactic//instructions: -1.0G (-45.57%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Util.Unfold//instructions: -1.0G (-27.15%) (reduced significance based on absolute threshold)
• ✅ build/module/Mathlib.Algebra.Order.Field.Defs//instructions: -1.1G (-37.42%) (reduced significance based on absolute threshold)
• ✅ build/module/Mathlib.Tactic.GCongr//instructions: -1.1G (-35.59%)
• ✅ build/module/Mathlib.Tactic.Hint//instructions: -1.2G (-21.79%)

Small changes (2419✅)

Too many entries to display here. View the full report on radar instead.

[github-actions]

PR summary 359770281c

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.NormNum.Core	199	200	+1 (+0.50%)
Mathlib.Tactic.Common	248	249	+1 (+0.40%)

Import changes for all files

Files	Import difference
../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all
There are 7155 files with changed transitive imports taking up over 320608 characters: this is too many to display!
You can run this locally from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 359770281c
Reference commit 07107e4cfd

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for 1640267 against 07107e4 are in. There are significant results. @JovanGerb

• ✅ build//instructions: -5.6T (-3.49%)

Large changes (3✅)

• ✅ build//instructions: -5.6T (-3.49%)
• ✅ build//wall-clock: -24s (-4.31%)
• ✅ build/profile/import//wall-clock: -20m 7s (-17.02%)

and 1 hidden

Medium changes (16✅)

• ✅ build/module/Aesop.Frontend.Basic//instructions: -1.1G (-48.38%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Frontend.Tactic//instructions: -1.3G (-21.65%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Index.DiscrTreeConfig//instructions: -1.0G (-47.25%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Options.Public//instructions: -1.1G (-34.80%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.RuleSet.Name//instructions: -1.1G (-54.04%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.RuleTac.Forward//instructions: -1.4G (-16.26%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Script.GoalWithMVars//instructions: -1.0G (-46.25%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Script.SpecificTactics//instructions: -1.4G (-12.76%)
• ✅ build/module/Aesop.Script.Tactic//instructions: -1.0G (-47.60%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Script.TacticState//instructions: -1.1G (-35.98%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Util.Basic//instructions: -1.2G (-12.22%)
• ✅ build/module/Aesop.Util.Tactic//instructions: -1.0G (-45.54%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Util.Unfold//instructions: -1.0G (-27.20%) (reduced significance based on absolute threshold)
• ✅ build/module/Mathlib.Algebra.Order.Field.Defs//instructions: -1.1G (-37.44%) (reduced significance based on absolute threshold)
• ✅ build/module/Mathlib.Tactic.GCongr//instructions: -1.1G (-35.51%)
• ✅ build/module/Mathlib.Tactic.Hint//instructions: -1.2G (-21.74%)

Small changes (2433✅)

Too many entries to display here. View the full report on radar instead.

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for 3597702 against 07107e4 are in. There are significant results. @JovanGerb

• ✅ build//instructions: -4.4T (-2.74%)

Large changes (3✅)

• ✅ build//instructions: -4.4T (-2.74%)
• ✅ build//wall-clock: -20s (-3.64%)
• ✅ build/profile/import//wall-clock: -15m 25s (-13.04%)

and 1 hidden

Medium changes (16✅)

• ✅ build/module/Aesop.Frontend.Basic//instructions: -1.1G (-48.27%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Frontend.Tactic//instructions: -1.3G (-21.62%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Index.DiscrTreeConfig//instructions: -1.0G (-47.43%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Options.Public//instructions: -1.1G (-34.81%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.RuleSet.Name//instructions: -1.1G (-53.90%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.RuleTac.Forward//instructions: -1.4G (-16.24%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Script.GoalWithMVars//instructions: -1.0G (-46.32%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Script.SpecificTactics//instructions: -1.4G (-12.36%)
• ✅ build/module/Aesop.Script.Tactic//instructions: -1.0G (-47.58%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Script.TacticState//instructions: -1.1G (-35.92%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Util.Basic//instructions: -1.2G (-12.21%)
• ✅ build/module/Aesop.Util.Tactic//instructions: -1.0G (-45.56%) (reduced significance based on absolute threshold)
• ✅ build/module/Aesop.Util.Unfold//instructions: -1.0G (-27.17%) (reduced significance based on absolute threshold)
• ✅ build/module/Mathlib.Algebra.Order.Field.Defs//instructions: -1.1G (-37.43%) (reduced significance based on absolute threshold)
• ✅ build/module/Mathlib.Tactic.GCongr//instructions: -1.1G (-35.73%)
• ✅ build/module/Mathlib.Tactic.Hint//instructions: -1.2G (-21.82%)

Small changes (1775✅)

Too many entries to display here. View the full report on radar instead.

[JovanGerb]

Ok, yes, with importing Plausible the result is a lot worse!