Commit 2024-07-01 20:25 5f0c6af8

feat: subsingleton tactic (#12525) 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.