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

4 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2005, Problem 2

Let $a_1, a_2, \dots$ be a sequence of integers with infinitely many positive and negative terms. Suppose that for every positive integer $n$ the numbers $a_1, a_2, \dots, a_n$ leave $n$ different remainders upon division by $n$. Prove that every integer occurs exactly once in the sequence.

Imports (2)

Imported by 1 file

Compfiles.lean

lemma Imo2005P2.a_injective line 41 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, GT.gt, OfNat.ofNat, Eq, Finset.card, Finset.image, HMod.hMod, Finset.range, Function.Injective
Proof uses: Decidable.byContradiction, Not, HAdd.hAdd, Max.max, rfl, Set.InjOn, Finset, Finset.injOn_of_card_image_eq, Eq.mpr, id, congrArg, Finset.card_range, Eq.refl, Iff.mpr, Membership.mem, Set, Finset.mem_coe, LT.lt, Finset.mem_range, Nat.lt_succ_of_le and 2 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2005P2.abs_sub_lt Any two of the first n terms differ by less than n line 55 source
Source documentation
Any two of the first n terms differ by less than n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, GT.gt, OfNat.ofNat, Eq, Finset.card, Finset.image, HMod.hMod, Finset.range, LT.lt, abs, HSub.hSub
Proof uses: Ne, Or, eq_or_ne, Eq.mpr, id, congrFun', congrArg, Eq.trans, sub_self, abs_zero, cast, Eq.symm, Nat.cast_zero, Nat.zero_lt_of_lt, Decidable.byContradiction, Not, Int.natAbs, rfl, LE.le, Int.abs_eq_natAbs and 17 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma abs_sub_lt (a : ℕ → ℤ)
    (rem : ∀ n > 0, ((Finset.range n).image (fun i => a i % n)).card = n)
    {i j n : ℕ} (hi : i < n) (hj : j < n) : |a i - a j| < n := by
…
```
lemma Imo2005P2.mem_of_between The first n terms form a set of n consecutive integers, so any integer sandwiched between two of them is itself one of them line 77 source
Source documentation
The first n terms form a set of n consecutive integers, so any integer sandwiched between two of them is itself one of them.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, GT.gt, OfNat.ofNat, Eq, Finset.card, Finset.image, HMod.hMod, Finset.range, LT.lt, LE.le, Exists
Proof uses: Finset, rfl, Membership.mem, Iff.mpr, And, Finset.mem_image, Exists.intro, And.intro, Finset.mem_range, Finset.Nonempty, Eq.mpr, id, congrArg, Finset.card_image_of_injOn, Function.Injective.injOn, Imo2005P2.a_injective, Finset.card_range, Eq.refl, Finset.max', Iff.mp and 19 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma mem_of_between (a : ℕ → ℤ)
    (rem : ∀ n > 0, ((Finset.range n).image (fun i => a i % n)).card = n)
    {n : ℕ} {z : ℤ} {i j : ℕ} (hi : i < n) (hj : j < n)
    (hzi : z ≤ a i) (hjz : a j ≤ z) :
    ∃ k, a k = z := by
…
```
problem Imo2005P2.imo2005_p2 line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Set.Infinite, Set.ofPred, LT.lt, OfNat.ofNat, GT.gt, Eq, Finset.card, Finset.image, HMod.hMod, Finset.range, ExistsUnique
Proof uses: Exists, LE.le, Classical.byContradiction, Not, Set.Finite.subset, Set.preimage, Set.Ioo, Set.Finite.preimage, Function.Injective.injOn, Imo2005P2.a_injective, Set.finite_Ioo, Membership.mem, Set, Iff.mpr, Set.mem_preimage, And, Set.mem_Ioo, And.intro, Eq.mp, Eq.trans and 10 more
32 instances, coercions and auxiliary constants left out.

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