perf: make the support of onFinset opaque

[eric-wieser]

It's very handy to have defeq of the function within a Finsupp, but we almost never care about the defeq of the support, especially since it almost always involves Classical.decidable which doesn't reduce.

This mplements my idea from #mathlib4 > simp timeout at `whnf` @ 💬, aimed at making (mapRange _ _ _).support irreducible.

This breaks the defeq of 0 = 0 + 0 on finsupp, but I think that's ok.

---

[github-actions]

PR summary 076d55acf7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Basis.algebraMapCoeffs_repr

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.

---

No changes to technical debt.

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).

[eric-wieser]

!bench

[leanprover-community-mathlib4-bot]

!bench

[leanprover-bot]

Here are the benchmark results for commit 076d55a.
There were significant changes against commit 4551f56:

  Benchmark                                           Metric         Change
  =========================================================================
+ ~Mathlib.Algebra.Category.ModuleCat.Presheaf.Free   instructions   -75.1%
+ ~Mathlib.Algebra.SkewMonoidAlgebra.Basic            instructions   -38.8%

[github-actions]

File	Instructions	%
build	-213.544⬝10⁹	(-0.13%)

5 files, Instructions -2.0⬝10⁹

File	Instructions	%
Mathlib.RingTheory.WittVector.Isocrystal	-1.177⬝10⁹	(-1.87%)
Mathlib.Algebra.MonoidAlgebra.Defs	-1.204⬝10⁹	(-1.70%)
Mathlib.Algebra.Polynomial.Basic	-1.291⬝10⁹	(-2.97%)
Mathlib.LinearAlgebra.TensorProduct.Vanishing	-1.543⬝10⁹	(-4.45%)
Mathlib.Algebra.MonoidAlgebra.Grading	-1.562⬝10⁹	(-5.07%)

2 files, Instructions -3.0⬝10⁹

File	Instructions	%
Mathlib.Algebra.Category.ModuleCat.Adjunctions	-2.550⬝10⁹	(-4.61%)
Mathlib.RepresentationTheory.GroupCohomology.Basic	-2.691⬝10⁹	(-3.49%)

2 files, Instructions -4.0⬝10⁹

File	Instructions	%
Mathlib.RingTheory.WittVector.FrobeniusFractionField	-3.267⬝10⁹	(-7.21%)
Mathlib.RingTheory.Localization.BaseChange	-3.729⬝10⁹	(-6.95%)

File	Instructions	%
Mathlib.RingTheory.Kaehler.JacobiZariski	-6.419⬝10⁹	(-1.05%)
Mathlib.RepresentationTheory.GroupCohomology.Resolution	-9.464⬝10⁹	(-8.29%)
Mathlib.Algebra.SkewMonoidAlgebra.Basic	-11.482⬝10⁹	(-38.76%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Free	-149.743⬝10⁹	(-75.06%)
CI run

[mattrobball]

Is the kernel problematic here or just the elaborator?

[eric-wieser]

I don't know. It would indeed be a good test to make this just @[irreducible] and see if the performance is any different. Do you mind trying that?

[mattrobball]

I can but I don't think I will have time until early next week.