feat: `subsingleton` tactic

[kmill]

The subsingleton tactic tries to close equality goals by arguing that the underlying type is a subsingleton type. It might be via a Subsingleton instance (via Subsingleton.elim), but it also handles some cases where morally the types are subsingletons; for example, it can prove that two BEq instances are equal if they both have LawfulBEq instances. For heterogeneous equality, it tries the HEq version of proof irrelevance.

This tactic avoids the issue where

example (α : Sort _) (x y : α) : x = y := by apply Subsingleton.elim

is a "proof" that every type is trivial. Changing this to by subsingleton prevents it from assigning the universe level metavariable in Sort _ to 0.

This tactic can accept a list of instances subsingleton [inst1, inst2, ...] to do something like have := inst1; have := inst2; ...; subsingleton, but it elaborates them in a lenient way (like simp arguments), and they can even be universe polymorphic. For example, subsingleton [CharP.CharOne.subsingleton] is allowed even though the type of CharP.CharOne.subsingleton is Subsingleton ?R with a number of pending instance problems.

This PR also eliminates a number of uses of Subsingleton.elim, either by switching a congr to congr! or by using this new tactic.

---

[kmill]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6ac7cfe8196ae9566da618dadca3b2ca15e25241. There were no significant changes against commit 335470e523bfe84aa288da3cd9e487906c6b37e6.

[github-actions[bot]]

PR summary 3861d3dfbb

Import changes

No significant changes to the import graph

---

Declarations diff

+ Lean.MVarId.subsingleton + Lean.Meta.mkSubsingleton + Lean.Meta.synthSubsingletonInst + elabSubsingletonInsts + fdef + instance (α : Sort _) (x y : α) : Decidable (x = y) := isTrue (Subsingleton.elim _ _) + instance (α : Sort _) (x y : α) : Decidable (x = y) := isTrue (by subsingleton)

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>

[kim-em]

bors merge

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[sgouezel]

bors r-

[mathlib-bors[bot]]

Canceled.

[sgouezel]

Can you merge master, fix the build, and send it back to bors? bors d+

[mathlib-bors[bot]]

:v: kmill can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kmill]

bors r+

[kmill]

bors r-

[mathlib-bors[bot]]

Canceled.

[kmill]

bors r+

[mathlib-bors[bot]]

This PR was included in a batch that was canceled, it will be automatically retried

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style