`Compfiles/Imo2009P6.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

20 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2009, Problem 6

Let a₁, a₂, ..., aₙ be distinct positive integers and let M be a set of n - 1 positive integers not containing s = a₁ + a₂ + ... + aₙ. A grasshopper is to jump along the real axis, starting at the point 0 and making n jumps to the right with lengths a₁, a₂, ..., aₙ in some order. Prove that the order can be chosen in such a way that the grasshopper never lands on any point in M.

Imports (3)

Imported by 1 file

Compfiles.lean

lemma Imo2009P6.lemma1 line 34 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Exists, Equiv.Perm, LE.le
Proof uses: Exists.intro, Tuple.sort, Tuple.monotone_sort
11 instances, coercions and auxiliary constants left out.
lemma Imo2009P6.lemma2 line 39 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Function.Injective, Exists, Equiv.Perm, LT.lt, Function.comp
Proof uses: LE.le, Imo2009P6.lemma1, Exists.intro, Ne, ne_of_lt, le_of_lt, Eq, Eq.mp, congrArg, propext, EmbeddingLike.apply_eq_iff_eq, lt_of_le_of_ne
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Imo2009P6.embedFinLE line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Function.Embedding, Fin
Proof uses: Function.Embedding.mk, Fin.mk
5 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
abbrev Imo2009P6.extendPerm line 58 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, LE.le
Proof uses: dite, LT.lt, Fin.mk, Not, Function.Injective, Equiv.ofBijective
11 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Imo2009P6.extendPerm_apply_of_lt line 75 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, LE.le, LT.lt, Eq, Imo2009P6.extendPerm, Fin.mk
Proof uses: of_eq_true, Eq.trans, eq_true, True, congrFun', congrArg, Equiv, Equiv.ofBijective, dite, Not, Equiv.ofBijective_apply, dite_eq_left_of_eq_true, eq_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2009P6.extendPerm_apply_of_not_lt line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, LE.le, Not, LT.lt, Eq, Imo2009P6.extendPerm
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Equiv, Equiv.ofBijective, dite, Fin.mk, Equiv.ofBijective_apply, dite_eq_right_of_eq_false, eq_false, eq_self
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2009P6.filter_le_last line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, HSub.hSub, OfNat.ofNat, Finset, Finset.filter, LE.le, Finset.univ
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, id, congrArg, propext, Finset.mem_filter, Iff.intro, And.left, And.intro, Finset.mem_univ, Decidable.byContradiction, Not
19 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2009P6.prefix_last_perm line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Nat, Fin, Equiv.Perm, Eq, HSub.hSub, OfNat.ofNat, Finset.sum, Finset.filter, LE.le, Finset.univ
Proof uses: Eq.mpr, id, congrArg, Finset, Imo2009P6.filter_le_last, Equiv.sum_comp
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2009P6.sum_init line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Nat, Fin, Eq, Finset.sum, HSub.hSub, OfNat.ofNat, Finset.univ, Fin.mk, Finset.filter, LT.lt
Proof uses: Function.Embedding, Imo2009P6.embedFinLE, Nat.sub_le, Finset, Finset.map, Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, And, id, congrArg, propext, Finset.mem_map, Finset.mem_filter, Iff.intro, Eq.trans, True, congrFun' and 13 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Imo2009P6.sum_init_of_eq line 121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Nat, Eq, HSub.hSub, OfNat.ofNat, Fin, Finset.sum, Finset.univ, Fin.mk, Finset.filter, LT.lt
Proof uses: Eq.rec, Eq.symm, Imo2009P6.sum_init
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2009P6.sum_init_add_last line 128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Nat, Fin, Eq, HSub.hSub, OfNat.ofNat, Finset.sum, Finset.univ, HAdd.hAdd, Fin.mk
Proof uses: Finset.erase, Finset.sum_erase_add, of_eq_true, Membership.mem, Finset, Finset.filter, LT.lt, Finset.ext, Eq.mpr, Iff, And, Ne, id, congrArg, propext, Finset.mem_erase, Finset.mem_filter, Iff.intro, And.intro, Fin.ext and 5 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma Imo2009P6.init_injective line 157 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Function.Injective, HSub.hSub, OfNat.ofNat, Fin.mk
Proof uses: Eq, Decidable.byContradiction, LT.lt, Not, congrArg, Fin.eq_of_val_eq
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2009P6.init_pos line 163 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, LT.lt, OfNat.ofNat, HSub.hSub, Fin.mk
Proof uses: Decidable.byContradiction, Not
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2009P6.init_sorted line 168 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, LT.lt, HSub.hSub, OfNat.ofNat, Fin.mk
Proof uses: Decidable.byContradiction, Not
17 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2009P6.embedFinLE_map_Iic The image of the prefix {j ≤ i'} of Fin m under embedFinLE is the prefix {j ≤ i} of Fin n, provided i lies in the small range line 176 source
Source comment
The image of the prefix `{j ≤ i'}` of `Fin m` under `embedFinLE` is the prefix `{j ≤ i}` of `Fin n`, provided `i` lies in the small range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Fin, LT.lt, Eq, Finset, Finset.map, Imo2009P6.embedFinLE, Finset.filter, Fin.mk, Finset.univ
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, And, Function.Embedding, id, congrArg, propext, Finset.mem_map, Finset.mem_filter, Iff.intro, Eq.trans, True, congrFun', true_and, Eq.symm, Eq.mp, Exists.intro and 6 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma embedFinLE_map_Iic {m n : ℕ} (hmn : m ≤ n) (i : Fin n) (hi : i.val < m) :
    (Finset.univ.filter (· ≤ (⟨i.val, hi⟩ : Fin m))).map (embedFinLE hmn) =
      Finset.univ.filter (· ≤ i) := by
…
```
Mentions: Imo2009P6.embedFinLE
lemma Imo2009P6.embedFinLE_map_Iio The image of {j : Fin m | j.val < c} under embedFinLE is the prefix {j ≤ ⟨c⟩} of Fin n with the point ⟨c⟩ removed line 196 source
Source comment
The image of `{j : Fin m | j.val < c}` under `embedFinLE` is the prefix `{j ≤ ⟨c⟩}` of `Fin n` with the point `⟨c⟩` removed.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, LT.lt, Eq, Finset, Fin, Finset.map, Imo2009P6.embedFinLE, Finset.filter, Finset.univ, Finset.erase, Fin.mk
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, And, Function.Embedding, id, congrArg, propext, Finset.mem_map, Ne, Finset.mem_erase, Iff.intro, Eq.symm, Eq.refl, And.intro, Eq.mp, Eq.trans, True and 10 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma embedFinLE_map_Iio {m n : ℕ} (hmn : m ≤ n) (c : ℕ) (hcm : c ≤ m) (hcn : c < n) :
    (Finset.univ.filter (fun j : Fin m => j.val < c)).map (embedFinLE hmn) =
      (Finset.univ.filter (fun j : Fin n => j ≤ ⟨c, hcn⟩)).erase ⟨c, hcn⟩ := by
…
```
Mentions: Imo2009P6.embedFinLE
lemma Imo2009P6.prefix_extendPerm line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Nat, Fin, Equiv.Perm, LE.le, LT.lt, Eq, Finset.sum, Finset.filter, Finset.univ, Imo2009P6.extendPerm, Fin.mk
Proof uses: Function.Embedding, Imo2009P6.embedFinLE, Finset, Finset.map, Imo2009P6.embedFinLE_map_Iic, Eq.mpr, id, congrArg, Eq.symm, Finset.sum_map, Finset.sum_congr, rfl, Membership.mem, Fin.isLt, Imo2009P6.extendPerm_apply_of_lt, of_eq_true, Eq.trans, Fin.mk.congr_simp, congrFun', Function.Embedding.mk and 3 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem Imo2009P6.imo2009_p6_aux1 line 244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Int, Function.Injective, Finset, Membership.mem, LE.le, Finset.card, HSub.hSub, Not, Finset.sum, Finset.univ, Exists, Equiv.Perm, Finset.filter
Proof uses: Nat.strongRecOn, dite, And, Classical.propDecidable, Ne, Eq, Insert.insert, Singleton.singleton, Or, Eq.mp, Eq.trans, congrArg, Eq.symm, of_eq_true, True, congrFun', HAdd.hAdd, Finset.card_insert_of_notMem, False, eq_false and 138 more
171 instances, coercions and auxiliary constants left out.

Tactic trace: 724 steps (first 200 of 724)
Open to load the checked before-and-after goal states.
theorem Imo2009P6.imo2009_p6_aux2 The problem with an additional assumption that a is sorted line 927 source
Source comment
The problem with an additional assumption that a is sorted.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Int, Function.Injective, Finset, Membership.mem, Eq, Finset.card, HSub.hSub, Not, Finset.sum, Finset.univ, Exists, Equiv.Perm, Finset.filter, LE.le
Proof uses: Eq.le, Imo2009P6.imo2009_p6_aux1
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem imo2009_p6_aux2 (n : ℕ) (hn : 0 < n)
    (a : Fin n → ℤ)
    (ainj : a.Injective)
    (apos : ∀ i, 0 < a i)
    (asorted : ∀ i j, i < j → a i < a j)
    (M : Finset ℤ)
    (Mpos : ∀ m ∈ M, 0 < m)
    (Mcard : M.card = n - 1)
    (hM : ∑ i, a i ∉ M)
    : ∃ p : Equiv.Perm (Fin n),
          ∀ i : Fin n, ∑ j ∈ Finset.univ.filter (· ≤ i), a (p j) ∉ M := by
…
```
problem Imo2009P6.imo2009_p6 line 943 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Int, Function.Injective, Finset, Membership.mem, Eq, Finset.card, HSub.hSub, Not, Finset.sum, Finset.univ, Exists, Equiv.Perm, Finset.filter, LE.le
Proof uses: Function.comp, Imo2009P6.lemma2, Iff.mpr, Equiv, Equiv.injective_comp, Equiv.invFun, Function.Bijective, of_eq_true, Equiv.symm, Eq.trans, Multiset, Multiset.map, Finset.val, True, congrFun', congrArg, Multiset.map_univ_val_equiv, eq_self, Equiv.right_inv, Equiv.toFun and 17 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.