Commit 2023-09-27 06:47 7a2b5b8e
View on Github →refactor: Change OrderBot ext lemma to Subsingleton (#7376)
This ext lemma had no assumption, so it can be turned into a Subsingleton instance.
Note that in Lean 3, subsingleton instances were a performance concern for simp. This concern is gone in Lean 4.