mathlib3

b95b8c7a - chore(*): restore `subsingleton` instances and remove hacks (#16046)

chore(*): restore `subsingleton` instances and remove hacks (#16046) #### Background The `simp` tactic used to [look for subsingleton instances excessively](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223034551), so every subsingleton/unique instances added to mathlib could slow down `simp` performance; in fact, removing some subsingleton instances locally led to such speedup that three hacks #5779, #5878 and #6639 along this line have been merged into mathlib. Since the problem was discovered, new subsingleton instances were mostly turned into lemma/defs, with a reference to gh-6025 that @eric-wieser created to track them and a notice to restore them as instances once safe to do so. This bad behavior of `simp` was finally fixed in [lean#665](https://github.com/leanprover-community/lean/pull/665) by @gebner in January 2022, so it is now safe to remove the hacks and restore the instances. In fact, the hack #5878 was already removed in [#13127](https://github.com/leanprover-community/mathlib/commit/c7626b7dfe2bf35b48cf43178a32d74f5dbf8b3f#diff-02976f8e19552b3c7ea070e30761e4e99f1333085cc5bb94fa170861c6ed27bcL497). I [measured the difference in performance](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/293228091) from removing one of the remaining hacks and it was negligible. Therefore, in this PR, we: + Remove both hacks remaining; + Turn all would-be instances that mention gh-6025 into actual global instances; + Golf proofs that explicitly invoked these instances previously; + Remove `local attribute [instance]` lines that were added when these instances were needed. Closes #6025.