Closing obsolete PRs

Stream: mathlib4

[Michael Rothgang]

Every now and then, I stumble across some PR that is now obsolete. (Usually via some Github search that is not #queue.) I'm inclined to comment (why they're superseded, thanking the author for their contribution) and close them; any objections if I do so?
Would a dedicated thread for recording such PRs be useful, as a "triage paper trail", so to say?

[Patrick Massot]

I think you should ask in the reviewer stream first. There may be a complicated history.

[Kim Morrison]

But yes, I think we are unnecessarily allergic to closing old obsolete stuff, and I think it would be good if we improved processes so reviewers agreed on when closing was appropriate, and then did it more!

[Richard Osborn]

They can always be re-opened as well.