`Compfiles/Imo2017P5.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

8 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2017, Problem 5

Fix N ≥ 1. A collection of N (N + 1) soccer players of distinct heights stand in a row. Sir Alex wishes to remove N (N − 1) players from this row to obtain a new row of 2N players in which the following N conditions hold: no one stands between the two tallest players, no one stands between the third and fourth tallest players, ..., no one stands between the two shortest players. Prove that this is possible.

Imports (9)

Imported by 1 file

Compfiles.lean

def Imo2017P5.prepend Prepend the kept pair s₀ < t₀ in front of the inductively chosen subsequence g line 53 source
Source documentation
Prepend the kept pair s₀ < t₀ in front of the inductively chosen subsequence g.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OrderEmbedding, HMul.hMul, OfNat.ofNat, HAdd.hAdd
Proof uses: dite, Eq, Not, Fin.mk, HSub.hSub
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def prepend (N M : ℕ) (s₀ t₀ : Fin M) (g : Fin (2 * N) ↪o Fin M) (x : Fin (2 * N + 2)) :
    Fin M :=
…
```
theorem Imo2017P5.prepend_zero line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OrderEmbedding, HMul.hMul, OfNat.ofNat, LT.lt, HAdd.hAdd, Eq, Imo2017P5.prepend, Fin.mk
Proof uses: id, dite_eq_left, rfl, Not, dite, HSub.hSub
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2017P5.prepend_one line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OrderEmbedding, HMul.hMul, OfNat.ofNat, LT.lt, HAdd.hAdd, Eq, Imo2017P5.prepend, Fin.mk
Proof uses: id, Eq.mpr, dite, Not, HSub.hSub, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, congrArg, dite_eq_right, dite_eq_left, rfl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2017P5.prepend_two line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OrderEmbedding, HMul.hMul, OfNat.ofNat, HAdd.hAdd, LE.le, Eq, Imo2017P5.prepend, Fin.mk, HSub.hSub
Proof uses: id, Eq.mpr, dite, Not, congrArg, dite_eq_right, Eq.refl
30 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Imo2017P5.prepend_strictMono line 75 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, LT.lt, OrderEmbedding, HMul.hMul, OfNat.ofNat, StrictMono, HAdd.hAdd, Imo2017P5.prepend
Proof uses: Fin.mk, dite, Eq, Eq.mpr, id, congrArg, Imo2017P5.prepend_zero, Imo2017P5.prepend_one, Eq.symm, Not, LE.le, HSub.hSub, Imo2017P5.prepend_two, lt_trans, False.elim, OrderEmbedding.strictMono
38 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
theorem Imo2017P5.aux Evan Chen's scan argument, by induction on the number of colours line 111 source
Source documentation
Evan Chen's scan argument, by induction on the number of colours.
Given a row of M people coloured by c : Fin M → Fin N, every colour appearing at least N + 1 times, one can select a subsequence of 2N people containing exactly two people of each colour, and such that the two people of any given colour stand next to each other in the subsequence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, LE.le, HAdd.hAdd, OfNat.ofNat, Finset.card, Finset.filter, Eq, Finset.univ, Exists, OrderEmbedding, HMul.hMul, And, Or
Proof uses: Nat.recAux, Exists.intro, OrderEmbedding.ofStrictMono, Fin.elim0, LT.lt, And.intro, Trans.trans, Finset.card_le_card, Finset.filter_subset, of_eq_true, Eq.trans, True, congrFun', congrArg, Fintype.card_fin, eq_self, Membership.mem, Finset, Ne, Fin.castLE and 83 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 316 steps (first 200 of 316)
Open to load the checked before-and-after goal states.
```
theorem aux : ∀ (N M : ℕ) (c : Fin M → Fin N),
    (∀ k, N + 1 ≤ (univ.filter fun i ↦ c i = k).card) →
    ∃ f : Fin (2 * N) ↪o Fin M,
      (∀ k, (univ.filter fun i ↦ c (f i) = k).card = 2) ∧
      ∀ i j, c (f i) = c (f j) → i = j ∨ i.val + 1 = j.val ∨ j.val + 1 = i.val := by
…
```
Mentions: f
theorem Imo2017P5.main_aux Colouring by height: c i is the index of the block of N + 1 consecutive height ranks containing the player at position i line 387 source
Source documentation
Colouring by height: c i is the index of the block of N + 1 consecutive height ranks containing the player at position i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HMul.hMul, HAdd.hAdd, Function.Injective, Exists, OrderEmbedding, Eq, Finset.card, Finset.filter, GT.gt, Finset.univ, Or
Proof uses: LT.lt, Finset.card_lt_card, Eq.mpr, Finset, And, Membership.mem, Not, id, congrArg, propext, Finset.filter_ssubset, Exists.intro, And.intro, Finset.mem_univ, of_eq_true, Eq.trans, False, True, not_false_eq_true, Eq.mp and 100 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 216 steps (first 200 of 216)
Open to load the checked before-and-after goal states.
```
theorem main_aux (N : ℕ) (_hN : 1 ≤ N) (a : Fin (N * (N + 1)) → ℕ)
    (ha : Function.Injective a) :
    ∃ f : Fin (2 * N) ↪o Fin (N * (N + 1)), ∀ k : Fin N, ∀ i j : Fin (2 * N),
      (univ.filter fun t ↦ a (f t) > a (f i)).card = 2 * k.val →
      (univ.filter fun t ↦ a (f t) > a (f j)).card = 2 * k.val + 1 →
      i.val + 1 = j.val ∨ j.val + 1 = i.val := by
…
```
Mentions: f
problem Imo2017P5.imo2017_p5 line 623 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HMul.hMul, HAdd.hAdd, Function.Injective, Exists, OrderEmbedding, Eq, Finset.card, Finset.filter, GT.gt, Finset.univ, Or
Proof uses: Imo2017P5.main_aux
19 instances, coercions and auxiliary constants left out.