[Merged by Bors] - feat(archive/100-theorems-list/73_ascending_descending_sequences): Erdős–Szekeres

[b-mehta]

Prove the Erdős-Szekeres theorem on ascending or descending sequences

---

Can probably be golfed, but crossing another one off the Freek list

[robertylewis]

My worry, just glancing at this, is that the proof will be hard to maintain. It's a very long proof with few intermediate statements and no comments explaining the proof sketch. Do you think you could split this up a bit more? Or at the very least add comments inside the proof so readers have some landmarks?

[b-mehta]

I don't think it'd be possible to split the proof up, but it should be very easy to add a sketch at the top and comments during the proof, I'll do that.

[bryangingechen]

The Wikipedia proof you refer to uses the pigeonhole principle. Do we have a reasonable API for making arguments with it in mathlib yet? cf. #2272.

[b-mehta]

No, but this argument uses a very basic version which is basically just the cardinality of the image of an injective function

[semorrison]

I don't think it'd be possible to split the proof up, but it should be very easy to add a sketch at the top and comments during the proof, I'll do that.

I think it should be straightforward to split up. Essentially every let, have and suffices you have in the proof could be a separate declaration. That said, the fact it looks straightforward to split up perhaps contradicts what Rob says about the proof having few intermediate statements, so I'm left a little uncertain how valuable it is to split up. Probably it would end up better.

[semorrison]

I think still to do:

1. move injective_of_lt_imp_ne to order.basic
2. see how @robertylewis feels about the length of the proof. I think it could be both easier to read and maintain if split across half a dozen declarations, but only slightly, and I think this is a pretty robust proof already with good use of let, have, suffices. (If I'd written it I definitely would have done it with many declarations, fwiw.)

[robertylewis]

2. see how @robertylewis feels about the length of the proof.

The comments help a lot, thanks.

My biggest worry is the long all_goals call beginning at line 106. It's a fairly long block, without milestones, and working on multiple goals at once without closing them is a recipe for confusion.

I didn't look at it in an editor and can't judge very well from the script (which is a minor warning sign itself), but maybe it would be possible to break the all_goals script into a separate lemma?

[b-mehta]

My biggest worry is the long all_goals call beginning at line 106. It's a fairly long block, without milestones, and working on multiple goals at once without closing them is a recipe for confusion.

This block does close the two goals it's working on - should I add a comment to make that more clear?

[robertylewis]

Sure, thanks.

[bryangingechen]

Just some final cosmetic suggestions. Everything else looks good to me!

bors d+

[bors]

✌️ b-mehta can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[b-mehta]

bors r+

[bors]

Build failed:

• Build mathlib

[bryangingechen]

Oh, the latest commit on this branch might fail to build because we haven't merged master into this branch yet. I'm betting the merge commit will build though:
bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Lint mathlib
• Build mathlib
• Run tests and docs