Junyan Xu

Yes the branch is deleted but the PR is still there (check the bottom of the PR for the deletion message; good hygiene automated by bors!).

I'll update the PR title/description since only one new lemma is added.

Actually bors will add my name because of my commits in the merged branch; so we'd better remove the coauthor message to avoid duplication.

> Actually bors will add my name because of my commits in the merged branch You can see that already happened in the squashed merge commit: https://github.com/leanprover-community/mathlib/pull/15721/commits/06d609d486920e3ac964fa4a8ab59dca40eae73b

> I mentioned this on the other PR, but I think the real reason for making this into an instance is that the problem was specifically about `subsingleton`, and this...

Maybe @eric-wieser can explain since he made the decision at [#9124](https://github.com/leanprover-community/mathlib/pull/9124#discussion_r706016081). I've personally been [hit by this issue](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/subsingleton.20instance.20makes.20a.20structure.20timeout); if adding an instance causes a timeout then you'd definitely change it...

What would it take to re-evaluate the decision? Any performance metric readily available? Build time depends a lot on which files are touched and resources on the machines. Randomly sample...

Oh I see there are plenty of methods for performance testing in the [original thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout), which I haven't looked into before.

Thanks to @sgouezel who pointed out on Zulip that the subsingleton issue was fixed by [lean#665](https://github.com/leanprover-community/lean/pull/665).

> So we can just make everything into an instance again, right? I think so and you are welcome to submit a PR removing those gh-6025 references and hacks as...