feat: shorten auto-generated instance names

[kmill]

Implements a new method to generate instance names for anonymous instances that uses a heuristic that tends to produce shorter names. A design goal is to make them relatively unique within projects and definitely unique across projects, while also using accessible names so that they can be referred to as needed, both in Lean code and in discussions.

The new method also takes into account binders provided to the instance, and it adds project-based suffixes. Despite this, a median new name is 73% its original auto-generated length. (Compare: old generated names and new generated names.)

Some notes:

• The naming is sensitive to what is explicitly provided as a binder vs what is provided via a variable. It does not make use of variables since, when names are generated, it is not yet known which variables are used in the body of the instance.
• If the instance name refers to declarations in the current "project" (given by the root module), then it does not add a suffix. Otherwise, it adds the project name as a suffix to protect against cross-project collisions.
• set_option trace.Elab.instance.mkInstanceName true can be used to see what name the auto-generator would give, even if the instance already has an explicit name.

There were a number of instances that were referred to explicitly in meta code, and these have been given explicit names.

Removes the unused Lean.Elab.mkFreshInstanceName along with the Command state's nextInstIdx.

Fixes #2343

[leanprover-community-mathlib4-bot]

• 💥 Mathlib branch lean-pr-testing-3089 build failed against this PR. (2023-12-18 04:51:26) View Log
• 🟡 Mathlib branch lean-pr-testing-3089 build this PR didn't complete normally. (2023-12-18 05:08:35) View Log
• 💥 Mathlib branch lean-pr-testing-3089 build failed against this PR. (2023-12-18 05:55:13) View Log
• 🟡 Mathlib branch lean-pr-testing-3089 build this PR didn't complete normally. (2023-12-20 20:07:13) View Log
• ❌ Mathlib branch lean-pr-testing-3089 built against this PR, but linting failed. (2024-03-31 01:16:24) View Log
• ❌ Mathlib branch lean-pr-testing-3089 built against this PR, but linting failed. (2024-03-31 03:51:29) View Log
• ❌ Mathlib branch lean-pr-testing-3089 built against this PR, but testing failed. (2024-03-31 04:42:56) View Log
• ✅ Mathlib branch lean-pr-testing-3089 has successfully built against this PR. (2024-03-31 05:55:16) View Log
• ✅ Mathlib branch lean-pr-testing-3089 has successfully built against this PR. (2024-03-31 07:10:22) View Log
• ✅ Mathlib branch lean-pr-testing-3089 has successfully built against this PR. (2024-03-31 21:53:10) View Log
• ❌ Mathlib branch lean-pr-testing-3089 built against this PR, but linting failed. (2024-04-02 18:44:00) View Log
• ❌ Mathlib branch lean-pr-testing-3089 built against this PR, but linting failed. (2024-04-02 19:30:43) View Log
• ✅ Mathlib branch lean-pr-testing-3089 has successfully built against this PR. (2024-04-02 21:33:03) View Log
• ✅ Mathlib branch lean-pr-testing-3089 has successfully built against this PR. (2024-04-02 22:40:21) View Log
• ✅ Mathlib branch lean-pr-testing-3089 has successfully built against this PR. (2024-04-03 01:48:36) View Log

[semorrison]

I've rebased this onto nightly-with-mathlib to see if we can get a build.

[digama0]

Master seems to be broken, I think due to test changes from this PR

[kmill]

Fascinating, it was triggered by the stage0 update. Fixing the tests...