perf(Analysis/CStarAlgebra/Matrix): speed up simp call

[kbuzzard]

Remove a lemma from the simp set to stop typeclass inference taking an expensive wrong turn.

---

The theorem Matrix.l2_opNorm_diagonal currently takes 66018097 mHeartbeats to elaborate (a couple of seconds, even on a fast machine). The reason for this is the final simp call, which takes 2/3 of the time, and the reason it takes so long is this misstep:

[Meta.synthInstance] [17395634.000000] ❌️ Nontrivial (EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) ▶

This can't be proved (n can have size 0) but simp is darn well going to try anyway. Unfolding the profiler gives over 1000 lines for this failure. To add insult to injury, simp attempts to prove this twice! These two failed proof attempts eat up over 50% of the total time spent on this proof.

The simplifier attempts to prove this because it wants to apply CStarRing.norm_of_mem_unitary, which needs nontriviality as a hypothesis. If we remove this lemma from the simp set then this speeds up elaboration by a factor of slightly more than 2.

I noticed this because a change in the algebra hierarchy which I'm experimenting with, pushed this proof over the line. I'm fixing up my change because of this but having diagnosed the poor performance I thought there was no harm in fixing it anyway.

[kbuzzard]

!radar

[github-actions]

PR summary 00dbc4ec64

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.

You can run this locally as

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

[leanprover-radar]

Benchmark results for 100b1a8 against 00dbc4e are in. No significant results found. @kbuzzard

• ✅ build//instructions: -30.1G (-0.02%)

Medium changes (1✅)

• ✅ build/module/Mathlib.Analysis.CStarAlgebra.Matrix//instructions: -9.5G (-6.93%)

Small changes (2✅, 2🟥)

• ✅ build/module/Mathlib.Algebra.Order.Monoid.Submonoid//instructions: -275.0M (-5.20%)
• 🟥 build/module/Mathlib.ModelTheory.Algebra.Ring.Definability//instructions: +415.2M (+4.85%)
• ✅ build/module/Mathlib.Order.Monotone.Extension//instructions: -275.3M (-4.86%)
• 🟥 build/module/Mathlib.Topology.Category.CompHaus.Frm//instructions: +407.4M (+6.68%)