perf: make Equiv transfer instances more reduced

[JovanGerb]

This pr speeds up the instances that are tranferred through Equivs by using the projections .toFun and .invFun directly in the data.

I think that we should eventually deprecate these instances, and instead have a metaprogram that creates these instances for us in each use case.

---

[JovanGerb]

!radar

[leanprover-radar]

Benchmark results for 80eb309 against 9e46613 are in. No significant results found. @JovanGerb

• ✅ build//instructions: -39.7G (-0.03%)

Medium changes (2✅)

• ✅ build/module/Mathlib.Analysis.CStarAlgebra.Matrix//instructions: -4.3G (-4.90%)
• ✅ build/module/Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris//instructions: -9.9G (-13.65%)

Small changes (6✅)

• ✅ build/module/Mathlib.Algebra.Category.Ring.Limits//instructions: -1.3G (-1.69%)
• ✅ build/module/Mathlib.Analysis.Normed.Algebra.UnitizationL1//instructions: -635.0M (-4.04%)
• ✅ build/module/Mathlib.Analysis.Normed.Field.WithAbs//instructions: -1.0G (-4.18%)
• ✅ build/module/Mathlib.NumberTheory.NumberField.Completion.Ramification//instructions: -1.0G (-2.76%)
• ✅ build/module/Mathlib.NumberTheory.NumberField.Ideal.Asymptotics//instructions: -1.1G (-2.99%)
• ✅ build/module/Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily//instructions: -1.3G (-8.99%)

[github-actions]

PR summary d04eef70ae

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

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)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 3f364cc).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit d04eef70ae
Reference commit 9e46613652

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]

This strange rewrite of this definition was needed because otherwise the simps! lemmas would turn out very wrong.

[Whysoserioushah]

awaiting-author

[Whysoserioushah]

Thanks, LGTM!

[YaelDillies]

Thanks! 🚀

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.