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
```lean
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.

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
```lean
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.

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
```lean
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.

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
```lean
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.

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
```lean
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.

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
```lean
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.

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
```lean
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.