Advice on preparing a PR to `lean4`

Stream: lean4

[Wrenna Robson]

I have this draft PR, lean4#12166. I think this makes a genuine improvement to Core in that it removes an unecessary dependence of a key theorem characterising List.Pairwise that then naturally allows for some missing (arguably, existent downstream) theorems about List.Nodup.

However I am consious that standards for core are very high and I don't want to just submit this and hope it is good enough for maintainers to seriously review. I was wondering if I can get some advice on if there are any obvious pitfalls that I ought to avoid, or simple improvements I can make?

[Markus Himmel]

If you've read through https://github.com/leanprover/lean4/blob/master/doc/std/style.md and https://github.com/leanprover/lean4/blob/master/doc/std/naming.md, don't be afraid to mark your PR as ready for review. The kinds of standard library PRs that are least likely to be accepted are those that increase the maintenance burden or that include significant design work that hasn't been cleared with a maintainer beforehand, but from a quick look your PR just seems to add a bunch of lemmas which are clearly desirable, so I'm looking forward to merging it.

[Wrenna Robson]

@Markus Himmel Thank you. Having given them a re-read, and also made some improvements (unrelated), I have opened it for review.