feat: add `simp` configuration option `Simp.Config.instances`

[leodemoura]

Depends on #3124

Mathlib adaptation PR is at https://github.com/leanprover-community/mathlib4/pull/9572

[leodemoura]

!bench

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2024-01-06' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2024-01-09 00:39:23)
• 💥 Mathlib branch lean-pr-testing-3151 build failed against this PR. (2024-01-09 02:15:34) View Log
• 💥 Mathlib branch lean-pr-testing-3151 build failed against this PR. (2024-01-09 04:59:06) View Log
• 🟡 Mathlib branch lean-pr-testing-3151 build against this PR was cancelled. (2024-01-09 06:22:08) View Log
• ✅ Mathlib branch lean-pr-testing-3151 has successfully built against this PR. (2024-01-09 07:25:47) View Log
• ✅ Mathlib branch lean-pr-testing-3151 has successfully built against this PR. (2024-01-09 11:34:16) View Log
• ✅ Mathlib branch lean-pr-testing-3151 has successfully built against this PR. (2024-01-09 12:00:53) View Log

[leanprover-bot]

Here are the benchmark results for commit 9be86b5f40360b2260b54a2dba4d7d9e8ffa18db. There were significant changes against commit 903493799dd943193aa019e7df042b1e656203a7:

  Benchmark                  Metric             Change
  ===============================================================
- import Lean                branches             1.8%  (105.8 σ)
- import Lean                instructions         1.8%  (136.9 σ)
- import Lean                maxrss               1.5%   (53.7 σ)
- lake startup               instructions         1.5%   (54.6 σ)
- libleanshared.so           binary size          2.0%
- reduceMatch                maxrss               1.3%  (101.8 σ)
- stdlib                     instructions         1.4% (1184.2 σ)
- stdlib                     wall-clock           1.6%   (18.8 σ)
- stdlib size                bytes .olean         1.4%
- stdlib size                lines C              2.5%
- tests/bench/ interpreted   maxrss               1.3%   (56.7 σ)
- tests/compiler             sum binary sizes     1.9%
- workspaceSymbols           instructions         2.2% (3266.8 σ)
- workspaceSymbols           maxrss               1.5%   (88.3 σ)

[kim-em]

~~This does cause a variety of Mathlib failures. Can we start out with this defaulting to true?~~

Maybe it's not so bad. I think we could proceed with this.

[kim-em]

I've created a discussion on zulip to forewarn users about this, and to discuss impact.

[kim-em]

This PR was superseded by #3507.