perf(LinearAlgebra) remove a simp for Module.finrank

[mcdoll]

This is a bad simp lemma because it gets tried on any term Module.finrank _ _ and then invokes the typeclass inference to check the assumptions. Both of the assumptions are rarely satisfied, but typeclass inference might take a while to figure that out, hence causing a slowdown for every simp call that contains Module.finrank _ _.

---

[github-actions]

PR summary ee3a5404e5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

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

You can run this locally as follows

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

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

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

---

No changes to technical debt.

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

[eric-wieser]

Maybe we can still tag this nontriviality, assuming the attribute is still around

[mcdoll]

If it is the case that this lemma was used exactly once, then I don't know whether we should tag it anything.

[grunweg]

Shouldn't the question be "can this be a useful nontriviality lemma in the future" rather than "is it right now"? (I don't in this area a lot, so you might be a better judge of that.)

[mcdoll]

!radar

[leanprover-radar]

Benchmark results for dfdcfd6 against ee3a540 are in. No significant results found. @mcdoll

• ✅ build//instructions: -66.8G (-0.04%)

Medium changes (3✅)

• ✅ build/module/Mathlib.Algebra.Lie.CartanCriterion//instructions: -5.7G (-11.73%)
• ✅ build/module/Mathlib.Algebra.Lie.TraceForm//instructions: -6.1G (-6.45%)
• ✅ build/module/Mathlib.RingTheory.Spectrum.Prime.FreeLocus//instructions: -5.6G (-6.47%)

Small changes (10✅)

• ✅ build/module/Mathlib.Analysis.InnerProductSpace.Laplacian//instructions: -1.7G (-3.55%)
• ✅ build/module/Mathlib.Analysis.InnerProductSpace.SingularValues//instructions: -529.9M (-2.26%)
• ✅ build/module/Mathlib.FieldTheory.Finite.Basic//instructions: -541.4M (-1.14%)
• ✅ build/module/Mathlib.FieldTheory.IntermediateField.Adjoin.Basic//instructions: -2.0G (-2.10%)
• ✅ build/module/Mathlib.FieldTheory.Relrank//instructions: -2.3G (-3.27%)
• ✅ build/module/Mathlib.MeasureTheory.Constructions.HaarToSphere//instructions: -731.9M (-2.20%)
• ✅ build/module/Mathlib.NumberTheory.RamificationInertia.Galois//instructions: -1.1G (-2.67%)
• ✅ build/module/Mathlib.NumberTheory.RamificationInertia.Inertia//instructions: -1.1G (-5.37%)
• ✅ build/module/Mathlib.RingTheory.Norm.Transitivity//instructions: -931.0M (-2.55%)
• ✅ build/module/Mathlib.Tactic.SimpRw//instructions: -559.4M (-12.33%)

[mcdoll]

Seems to be a reasonably good improvement