perf(Data/Complex/Basic): no_expose the Inv and Norm instance

[JovanGerb]

This PR hides some more implementation details of complex numbers.

It would be possible to no_expose even more definitions, but this could be at the cost of some proof writing convenience.

---

[github-actions]

PR summary 03ab904979

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

[JovanGerb]

!bench

[JovanGerb]

(@grunweg, did you actually change the title? I just see the same title before and after?)

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for 33d46ee against 03ab904 are in. No significant results found. @JovanGerb

• 🟥 build//instructions: +12.1G (+0.01%)

Small changes (1✅)

• ✅ build/module/Mathlib.Algebra.Order.Module.Equiv//instructions: -219.1M (-4.34%)

[grunweg]

I fixed a typo "Comlex" :-)

[JovanGerb]

I tried putting no_expose on some other operations on the complex numbers. On the one hand, removing definitional equalities forces the proofs to be "better" in the sense that they can't secretly hide some steps somewhere. On the other hand, it is often quite convenient to be able to use certain defeq properties.

So, the only one that I ended up keeping is no_expose on Norm ℂ.

However, I already cleaned up some proofs that were abusing defeq, and I think we may as well take these cleaned up proofs now that I made them, so I've left them in this PR.