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

19 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2002, Problem 1

Let n be a positive integer. Let T be the set of points (x, y) in the plane where x and y are non-negative integers and x + y < n. Each point of T is coloured red or blue, subject to the following condition: if a point (x, y) is red, then so are all points (x', y') of T with x' ≤ x and y' ≤ y. Let A be the number of ways of choosing n blue points with distinct x-coordinates, and let B be the number of ways of choosing n blue points with distinct y-coordinates. Prove that A = B.

Imports (2)

Imported by 1 file

Compfiles.lean

inductive Imo2002P1.Color line 32 source
no axioms what this means

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance Imo2002P1.(instance at line 37) line 37 source
def Imo2002P1.T The points (x, y) with nonnegative integer coordinates and x + y < n line 42 source
Source documentation
The points (x, y) with nonnegative integer coordinates and x + y < n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod
Proof uses: Finset.filter, LT.lt, HAdd.hAdd, Prod.fst, Prod.snd, SProd.sprod, Finset.range
5 instances, coercions and auxiliary constants left out.
```
def T (n : ℕ) : Finset (ℕ × ℕ) :=
…
```
def Imo2002P1.ChoiceCount The sets of n blue points in T whose coordinates are distinct in the dimension selected by coord line 47 source
Source documentation
The sets of n blue points in T whose coordinates are distinct in the dimension selected by coord.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2002P1.Color
Proof uses: Finset.card, Finset, Finset.filter, And, Membership.mem, Eq, Imo2002P1.Color.blue, Finset.powersetCard, Imo2002P1.T
8 instances, coercions and auxiliary constants left out.
```
def ChoiceCount (n : ℕ) (color : ℕ × ℕ → Color) (coord : ℕ × ℕ → ℕ) : ℕ :=
…
```
Mentions: Imo2002P1.Color
lemma Imo2002P1.color_eq_blue_iff line 54 source
standard axioms: propext what this means
Statement uses: Imo2002P1.Color, Iff, Eq, Imo2002P1.Color.blue, Not, Imo2002P1.Color.red
Proof uses: of_eq_true, Eq.trans, False, True, congr, congrArg, eq_false', False.elim, noConfusion_of_Nat, Imo2002P1.Color.ctorIdx, eq_self, not_true_eq_false, iff_self, Eq.symm, not_false_eq_true, Eq.refl
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2002P1.downward_closed_iff_lt_card A downward-closed finite set of naturals is an initial segment line 58 source
Source documentation
A downward-closed finite set of naturals is an initial segment.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, LE.le, Membership.mem, Iff, LT.lt, Finset.card
Proof uses: Iff.intro, Finset.range, HAdd.hAdd, OfNat.ofNat, Eq.mp, congrArg, propext, Finset.mem_range, Finset.card_le_card, Finset.card_range, Decidable.byContradiction, Not, Eq.mpr, id, Eq
21 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma downward_closed_iff_lt_card {S : Finset ℕ}
    (h : ∀ a b, a ≤ b → b ∈ S → a ∈ S) (y : ℕ) : y ∈ S ↔ y < S.card := by
…
```
Mentions: S, h
def Imo2002P1.blueCol The blue points in column x line 81 source
Source documentation
The blue points in column x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2002P1.Color, Finset
Proof uses: Finset.filter, Eq, Prod.mk, Imo2002P1.Color.blue, Finset.range, HSub.hSub
3 instances, coercions and auxiliary constants left out.
```
def blueCol (n : ℕ) (color : ℕ × ℕ → Color) (x : ℕ) : Finset ℕ :=
…
```
Mentions: Imo2002P1.Color
def Imo2002P1.redCol The number of red points in column x line 85 source
Source documentation
The number of red points in column x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2002P1.Color
Proof uses: Finset.card, Finset.filter, Eq, Prod.mk, Imo2002P1.Color.red, Finset.range, HSub.hSub
3 instances, coercions and auxiliary constants left out.
```
def redCol (n : ℕ) (color : ℕ × ℕ → Color) (x : ℕ) : ℕ :=
…
```
Mentions: Imo2002P1.Color
lemma Imo2002P1.card_blueCol line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2002P1.Color, Eq, Finset.card, Imo2002P1.blueCol, HSub.hSub, Imo2002P1.redCol
Proof uses: Finset, SDiff.sdiff, Finset.range, Finset.filter, Prod.mk, Imo2002P1.Color.red, Eq.mpr, Imo2002P1.Color.blue, id, congrArg, Imo2002P1.blueCol.eq_1, Not, Eq.symm, Finset.filter_not, Finset.filter_congr, Membership.mem, Imo2002P1.color_eq_blue_iff, Inter.inter, Finset.card_sdiff, Iff.mpr and 6 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2002P1.redCol_le line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2002P1.Color, LE.le, Imo2002P1.redCol, HSub.hSub
Proof uses: le_trans, Finset.card, Finset.range, Finset.card_filter_le, Eq, Prod.mk, Imo2002P1.Color.red, Eq.le, Finset.card_range
7 instances, coercions and auxiliary constants left out.
lemma Imo2002P1.red_iff line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2002P1.Color, LE.le, LT.lt, HAdd.hAdd, Eq, Prod.mk, Imo2002P1.Color.red, Iff, Imo2002P1.redCol
Proof uses: Membership.mem, Finset, Finset.filter, Finset.range, HSub.hSub, Eq.mpr, And, id, congrArg, propext, Finset.mem_filter, Finset.mem_range, And.intro, Eq.mp, le_rfl, And.right, Finset.card, Imo2002P1.redCol.eq_1, Eq.symm, Imo2002P1.downward_closed_iff_lt_card and 1 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2002P1.redCol_antitone line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2002P1.Color, LE.le, LT.lt, HAdd.hAdd, Eq, Prod.mk, Imo2002P1.Color.red, Antitone, Imo2002P1.redCol
Proof uses: antitone_nat_of_succ_le, Finset.card_le_card, Finset.filter, OfNat.ofNat, Finset.range, HSub.hSub, Membership.mem, Finset, Eq.mpr, And, id, congrArg, propext, Finset.mem_filter, Finset.mem_range, And.intro, Eq.mp, le_rfl, And.right
19 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2002P1.redCol_swap The red count in row y is the number of columns whose red count exceeds y line 127 source
Source documentation
The red count in row y is the number of columns whose red count exceeds y.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2002P1.Color, LE.le, LT.lt, HAdd.hAdd, Eq, Prod.mk, Imo2002P1.Color.red, Imo2002P1.redCol, Prod.swap, Finset.card, Finset.filter, Finset.range
Proof uses: Eq.mpr, HSub.hSub, id, congrArg, Imo2002P1.redCol.eq_1, Finset, Eq.rec, Eq.refl, Finset.ext, Iff, Membership.mem, And, propext, Finset.mem_filter, Finset.mem_range, Iff.intro, And.intro, Iff.mp, Imo2002P1.red_iff, Imo2002P1.redCol_le and 1 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma redCol_swap (y : ℕ) :
    redCol n (fun p ↦ color p.swap) y =
      ((Finset.range n).filter fun x ↦ y < redCol n color x).card := by
…
```
Mentions: Imo2002P1.redCol
lemma Imo2002P1.key_prod Documented declaration: key_prod line 149 source
Source documentation
The heart of the solution: if f is an antitone "red column count" function fitting under the staircase, then the product of blue column counts equals the product of blue row counts, where row red counts are given by the conjugate partition. Induction on ∑ f, recoloring one corner red point at a time.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Finset.range, Antitone, LE.le, HSub.hSub, Finset.prod, Finset.card, Finset.filter, LT.lt
Proof uses: Nat.strong_induction_on, OfNat.ofNat, GT.gt, Or, Nat.eq_zero_or_pos, Membership.mem, Finset, Finset.single_le_sum, Nat.zero_le, Eq.mpr, id, congrArg, EmptyCollection.emptyCollection, Finset.filter_false_of_mem, Not, Finset.card_empty, Finset.prod_congr, rfl, Eq.refl, Eq.symm and 48 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 174 steps
Open to load the checked before-and-after goal states.
```
lemma key_prod (n : ℕ) : ∀ N : ℕ, ∀ f : ℕ → ℕ, (∑ x ∈ Finset.range n, f x = N) →
    Antitone f → (∀ x, f x ≤ n - x) →
    ∏ x ∈ Finset.range n, (n - x - f x) =
      ∏ y ∈ Finset.range n, (n - y - ((Finset.range n).filter fun x ↦ y < f x).card) := by
…
```
Mentions: f
lemma Imo2002P1.image_fst_eq line 306 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2002P1.Color, Finset, Membership.mem, Finset.filter, And, Eq, Imo2002P1.Color.blue, Prod.fst, Finset.powersetCard, Imo2002P1.T, Finset.image, Finset.range
Proof uses: LE.le, Finset.card, Eq.mp, congrArg, propext, Finset.mem_powersetCard, Finset.mem_filter, Finset.eq_of_subset_of_card_le, Exists, Finset.mem_image, Iff.mpr, LT.lt, Finset.mem_range, Prod.snd, HAdd.hAdd, Eq.trans, SProd.sprod, congrFun', congr, Eq.mpr and 4 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2002P1.exists_unique_fst line 322 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2002P1.Color, Finset, Membership.mem, Finset.filter, And, Eq, Imo2002P1.Color.blue, Prod.fst, Finset.powersetCard, Imo2002P1.T, Finset.range, ExistsUnique
Proof uses: Finset.image, Imo2002P1.image_fst_eq, Eq.mp, congrArg, propext, Finset.mem_filter, Eq.mpr, id, Exists, Finset.mem_image, Exists.intro, And.intro, Eq.refl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2002P1.choiceCount_fst A choice of n blue points with distinct x-coordinates amounts to a choice of one blue point in each column line 337 source
Source documentation
A choice of n blue points with distinct x-coordinates amounts to a choice of one blue point in each column.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2002P1.Color, Eq, Imo2002P1.ChoiceCount, Prod.fst, Finset.prod, Finset.range, Finset.card, Imo2002P1.blueCol
Proof uses: Eq.mpr, Finset, Finset.filter, And, Membership.mem, Imo2002P1.Color.blue, Finset.powersetCard, Imo2002P1.T, id, congrArg, Imo2002P1.ChoiceCount.eq_1, Finset.pi, Eq.symm, Finset.card_pi, Finset.card_bij', Prod.snd, Finset.choose, Imo2002P1.exists_unique_fst, Finset.image, Subtype and 44 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 95 steps
Open to load the checked before-and-after goal states.
```
lemma choiceCount_fst (n : ℕ) (color : ℕ × ℕ → Color) :
    ChoiceCount n color Prod.fst = ∏ x ∈ Finset.range n, (blueCol n color x).card := by
…
```
Mentions: Imo2002P1.Color, Imo2002P1.ChoiceCount, Imo2002P1.blueCol
lemma Imo2002P1.choiceCount_snd Reflecting across the diagonal swaps the roles of the two coordinates line 434 source
Source documentation
Reflecting across the diagonal swaps the roles of the two coordinates.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2002P1.Color, Eq, Imo2002P1.ChoiceCount, Prod.snd, Prod.swap, Prod.fst
Proof uses: Eq.mpr, Finset.card, Finset, Finset.filter, And, Membership.mem, Imo2002P1.Color.blue, Finset.powersetCard, Imo2002P1.T, id, congrArg, Imo2002P1.ChoiceCount.eq_1, Finset.card_bij', Finset.image, propext, Finset.mem_filter, LE.le, Finset.mem_powersetCard, Eq.mp, And.intro and 22 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
```
lemma choiceCount_snd (n : ℕ) (color : ℕ × ℕ → Color) :
    ChoiceCount n color Prod.snd = ChoiceCount n (fun p ↦ color p.swap) Prod.fst := by
…
```
Mentions: Imo2002P1.Color, Imo2002P1.ChoiceCount
problem Imo2002P1.imo2002_p1 line 493 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Prod, Imo2002P1.Color, LE.le, HAdd.hAdd, Eq, Prod.mk, Imo2002P1.Color.red, Imo2002P1.ChoiceCount, Prod.fst, Prod.snd
Proof uses: Prod.swap, Eq.mpr, Finset.prod, Finset.range, Finset.card, Imo2002P1.blueCol, id, congrArg, Imo2002P1.choiceCount_fst, Imo2002P1.choiceCount_snd, Membership.mem, Finset, HSub.hSub, Imo2002P1.redCol, Imo2002P1.card_blueCol, Finset.filter, Imo2002P1.redCol_swap, Eq.refl, Finset.prod_congr, rfl and 4 more
18 instances, coercions and auxiliary constants left out.

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