chore (Data.Fintype.Basic): de-simp `Fintype.univ_ofSubsingleton`

[mattrobball]

In principle, Fintype.univ_ofSubsingleton could be a simp theorem but it applies to any occurence of univ and requires unification of the (possibly very complex) Fintype instances. It appears to not be needed in simp. So we remove the attribute. We get some performance gains as a benefit.

---

See the Zulip topic for an example of it causing problems in the wild.

[github-actions[bot]]

PR summary daecf0add0

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/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1060fe4319f3b5729e4ba1445e0a9c3362973c6e. There were significant changes against commit 202e9e09ef8391a1472b7ed0710cc9570daad850:

  Benchmark                                                    Metric         Change
  ==================================================================================
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic   instructions    -8.2%
+ ~Mathlib.NumberTheory.NumberField.Units.DirichletTheorem     instructions    -7.0%

[kim-em]

bors merge

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style