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

17 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1988, Problem 2

Let n be a positive integer and let A₁, A₂, ..., A₂ₙ₊₁ be subsets of a set B. Suppose that

(i) each Aᵢ has exactly 2n elements, (ii) each intersection Aᵢ ∩ Aⱼ (i ≠ j) contains exactly one element, and (iii) every element of B belongs to at least two of the Aᵢ.

For which values of n can one assign to every element of B one of the numbers 0 and 1 in such a way that each Aᵢ has exactly n elements assigned 0?

Imports (2)

Imported by 1 file

Compfiles.lean

determine Imo1988P2.SolutionSet line 34 source
no axioms what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, And, LT.lt, OfNat.ofNat, Even
3 instances, coercions and auxiliary constants left out.
lemma Imo1988P2.double_count Counting the pairs (a, b) with a ∈ s, b ∈ t and r a b, fiberwise in either order line 40 source
Source documentation
Counting the pairs (a, b) with a ∈ s, b ∈ t and r a b, fiberwise in either order.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Decidable, Eq, Nat, Finset.sum, Finset.card, Finset.filter
Proof uses: Eq.mpr, ite, OfNat.ofNat, id, congr, congrArg, Finset.sum_congr, Eq.refl, Membership.mem, Finset.card_filter, Finset.sum_comm
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma double_count {α β : Type*} (s : Finset α) (t : Finset β) (r : α → β → Prop)
    [∀ a b, Decidable (r a b)] :
    ∑ a ∈ s, (t.filter (fun b ↦ r a b)).card =
      ∑ b ∈ t, (s.filter (fun a ↦ r a b)).card := by
…
```
lemma Imo1988P2.all_eq_one If finitely many terms, each at least 1, sum to the number of terms, then every term equals 1 line 49 source
Source documentation
If finitely many terms, each at least 1, sum to the number of terms, then every term equals 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Membership.mem, LE.le, OfNat.ofNat, Eq, Finset.sum, Finset.card
Proof uses: Eq.mpr, id, congrArg, HMul.hMul, Finset.sum_const_nat, rfl, mul_one, Eq.refl, Eq.symm, Iff.mp, Finset.sum_eq_sum_iff_of_le
19 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma all_eq_one {α : Type*} {s : Finset α} {g : α → ℕ}
    (h1 : ∀ a ∈ s, 1 ≤ g a) (h2 : ∑ a ∈ s, g a = s.card) :
    ∀ a ∈ s, g a = 1 := by
…
```
lemma Imo1988P2.other_unique Under the problem's hypotheses, every element of A i lies in exactly one set A j with j ≠ i line 63 source
Source documentation
Under the problem's hypotheses, every element of A i lies in exactly one set A j with j ≠ i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidableEq, Fin, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset, Eq, Finset.card, Ne, Inter.inter, LE.le, Finset.filter, Membership.mem, Finset.univ, Finset.erase
Proof uses: Imo1988P2.all_eq_one, HSub.hSub, Eq.mpr, id, congrArg, Finset.filter_erase, Finset.pred_card_le_card_erase, Finset.sum, Imo1988P2.double_count, Finset.filter_mem_eq_inter, Ne.symm, And.left, Iff.mp, And, Finset.mem_erase, Finset.sum_const_nat, mul_one, Finset.card_erase_of_mem, Finset.mem_univ, Fintype.card and 2 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma other_unique
    (hcard : ∀ i, (A i).card = 2 * n)
    (hint : ∀ i j, i ≠ j → (A i ∩ A j).card = 1)
    (hcov : ∀ b : B, 2 ≤ (Finset.univ.filter (fun i ↦ b ∈ A i)).card)
    {i : Fin (2 * n + 1)} {b : B} (hb : b ∈ A i) :
    ((Finset.univ.erase i).filter (fun j ↦ b ∈ A j)).card = 1 := by
…
```
lemma Imo1988P2.pair_eq The pair of indices of the sets containing a common element b of A i and A j line 91 source
Source documentation
The pair of indices of the sets containing a common element b of A i and A j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidableEq, Fin, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset, Eq, Finset.card, Ne, Inter.inter, LE.le, Finset.filter, Membership.mem, Finset.univ, Insert.insert, Singleton.singleton
Proof uses: Finset.erase, Eq.mpr, id, congrArg, Eq.symm, Finset.filter_erase, Imo1988P2.other_unique, Iff.mpr, And, Finset.mem_filter, And.intro, Finset.mem_univ, HSub.hSub, Finset.card_erase_of_mem, LT.lt, Finset.Nonempty, Finset.card_pos, Exists.intro, Or, Eq.mp and 5 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma pair_eq
    (hcard : ∀ i, (A i).card = 2 * n)
    (hint : ∀ i j, i ≠ j → (A i ∩ A j).card = 1)
    (hcov : ∀ b : B, 2 ≤ (Finset.univ.filter (fun i ↦ b ∈ A i)).card)
    {i j : Fin (2 * n + 1)} {b : B} (hbi : b ∈ A i) (hbj : b ∈ A j) (hij : i ≠ j) :
    Finset.univ.filter (fun k ↦ b ∈ A k) = {i, j} := by
…
```
def Imo1988P2.colour Colour an edge e = {p, q} of the complete graph on Fin (K + 1) with 0 iff the difference of its endpoints, in one of the two directions, lies in [1, m] line 121 source
Source documentation
Colour an edge e = {p, q} of the complete graph on Fin (K + 1) with 0 iff the difference of its endpoints, in one of the two directions, lies in [1, m].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, HAdd.hAdd, OfNat.ofNat
Proof uses: ite, Exists, And, Membership.mem, Finset.Icc, HSub.hSub
20 instances, coercions and auxiliary constants left out.
```
def colour {K : ℕ} (m : ℕ) (e : Finset (Fin (K + 1))) : Fin 2 :=
…
```
lemma Imo1988P2.colour_eq_zero_iff line 124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, HAdd.hAdd, OfNat.ofNat, Iff, Eq, Imo1988P2.colour, Exists, And, Membership.mem, Finset.Icc, HSub.hSub
Proof uses: id, Decidable, ite, Not, Eq.mpr, congrFun', congrArg, ite_eq_right, iff_of_false, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, ite_eq_left, iff_of_true, rfl
32 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo1988P2.colour_pair_eq_zero_iff line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Iff, Eq, Imo1988P2.colour, Insert.insert, Finset, Singleton.singleton, Or, Membership.mem, Finset.Icc, HSub.hSub
Proof uses: Eq.mpr, Exists, And, id, congrArg, propext, Imo1988P2.colour_eq_zero_iff, Not, sub_self, of_eq_true, Eq.trans, False, True, LE.le, congr, and_true, not_false_eq_true, Iff.intro, Eq.mp, absurd and 7 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma Imo1988P2.count_good Documented declaration: count_good line 157 source
Source documentation
At each vertex i of the complete graph on Fin (2 * n + 1) with n = 2 * m, exactly n of the 2 * n incident edges have a circular difference in [1, m]: measuring each neighbour j by (j - i).val identifies the good neighbours with [1, m] ∪ [2 * n + 1 - m, 2 * n].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMul.hMul, OfNat.ofNat, Fin, HAdd.hAdd, Finset.card, Finset.filter, Or, Membership.mem, Finset, Finset.Icc, HSub.hSub, Finset.erase, Finset.univ
Proof uses: And, LE.le, Finset.range, Finset.card_bij, Ne, Eq.mp, congrArg, propext, Finset.mem_erase, Finset.mem_filter, sub_ne_zero_of_ne, Iff.mp, Fin.val_inj, Eq.mpr, id, Fin.val_zero, Eq.refl, Neg.neg, ite, Fin.val_neg and 32 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 66 steps
Open to load the checked before-and-after goal states.
```
lemma count_good {n m : ℕ} (hm : n = 2 * m) (i : Fin (2 * n + 1)) :
    ((Finset.univ.erase i).filter
      (fun j ↦ (j - i).val ∈ Finset.Icc 1 m ∨ (i - j).val ∈ Finset.Icc 1 m)).card
      = n := by
…
```
lemma Imo1988P2.vertex_count With n = 2 * m, colouring each element by colour m of its index pair gives exactly n elements of colour 0 in each A i line 228 source
Source documentation
With n = 2 * m, colouring each element by colour m of its index pair gives exactly n elements of colour 0 in each A i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidableEq, Fin, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset, Eq, Finset.card, Ne, Inter.inter, LE.le, Finset.filter, Membership.mem, Finset.univ, Imo1988P2.colour
Proof uses: Finset.sum, Finset.erase, Imo1988P2.double_count, Imo1988P2.other_unique, And.left, Iff.mp, And, Finset.mem_filter, ite, Or, Finset.Icc, HSub.hSub, Ne.symm, Finset.mem_erase, Singleton.singleton, Exists, Finset.card_eq_one, Eq.mpr, id, congrArg and 31 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma vertex_count {m : ℕ} (hm : n = 2 * m)
    (hcard : ∀ i, (A i).card = 2 * n)
    (hint : ∀ i j, i ≠ j → (A i ∩ A j).card = 1)
    (hcov : ∀ b : B, 2 ≤ (Finset.univ.filter (fun i ↦ b ∈ A i)).card)
    (i : Fin (2 * n + 1)) :
    ((A i).filter
      (fun b ↦ colour m (Finset.univ.filter (fun k ↦ b ∈ A k)) = 0)).card = n := by
…
```
Mentions: Imo1988P2.colour
abbrev Imo1988P2.Edges The edges of the complete graph on Fin N: two-element subsets line 273 source
Source documentation
The edges of the complete graph on Fin N: two-element subsets.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Subtype, Finset, Fin, Eq, Finset.card, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
abbrev Edges (N : ℕ) : Type := {e : Finset (Fin N) // e.card = 2}
```
def Imo1988P2.edgeSets The set of edges incident to the vertex i line 276 source
Source documentation
The set of edges incident to the vertex i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, Imo1988P2.Edges
Proof uses: Finset.filter, Membership.mem, Eq, Finset.card, OfNat.ofNat, Finset.univ
10 instances, coercions and auxiliary constants left out.
```
def edgeSets (N : ℕ) (i : Fin N) : Finset (Edges N) :=
…
```
Mentions: Imo1988P2.Edges
lemma Imo1988P2.mem_edgeSets line 279 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo1988P2.Edges, Iff, Membership.mem, Finset, Imo1988P2.edgeSets, Eq, Finset.card, OfNat.ofNat
Proof uses: Eq.mpr, Finset.filter, Finset.univ, id, congrArg, Imo1988P2.edgeSets.eq_1, And, propext, Finset.mem_filter, and_iff_right, Finset.mem_univ
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1988P2.edgeSets_card line 284 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset.card, Imo1988P2.Edges, Imo1988P2.edgeSets, HSub.hSub, OfNat.ofNat
Proof uses: Finset.erase, Finset.univ, Finset.card_bij, Membership.mem, Finset, Subtype.mk, Insert.insert, Singleton.singleton, Iff.mpr, Ne, Finset.card_pair_eq_two_iff, Ne.symm, And.left, Iff.mp, And, Finset.mem_erase, Imo1988P2.mem_edgeSets, Finset.mem_insert_self, congrArg, Subtype and 24 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma Imo1988P2.edgeSets_inter line 312 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Ne, Eq, Finset, Imo1988P2.Edges, Inter.inter, Finset.card, OfNat.ofNat, Imo1988P2.edgeSets, Singleton.singleton, Subtype.mk, Insert.insert, Iff.mpr, Finset.card_pair_eq_two_iff
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, id, congrArg, propext, Finset.mem_inter, Finset.mem_singleton, Imo1988P2.mem_edgeSets, Iff.intro, LE.le, Finset.insert_subset, Finset.singleton_subset_iff, Subtype.prop, le_of_eq, Eq.symm, Subtype.ext, Finset.eq_of_subset_of_card_le and 4 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Imo1988P2.edgeSets_cov line 329 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1988P2.Edges, Eq, Finset.card, Fin, Finset.filter, Membership.mem, Finset, Imo1988P2.edgeSets, OfNat.ofNat, Finset.univ
Proof uses: Finset.ext, Eq.mpr, Iff, And, id, congrArg, propext, Finset.mem_filter, Imo1988P2.mem_edgeSets, and_iff_right, Finset.mem_univ, Subtype.prop, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
problem Imo1988P2.imo1988_p2 line 339 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Membership.mem, Set, Imo1988P2.SolutionSet, And, LT.lt, OfNat.ofNat, DecidableEq, Fin, HAdd.hAdd, HMul.hMul, Finset, Eq, Finset.card, Ne, Inter.inter, LE.le, Finset.filter, Finset.univ and 1 more
Proof uses: Iff.intro, Even, And.intro, Exists.intro, Imo1988P2.colour, Imo1988P2.vertex_count, Imo1988P2.Edges, Imo1988P2.edgeSets, Eq.mpr, HSub.hSub, id, congrArg, Imo1988P2.edgeSets_card, Singleton.singleton, Subtype.mk, Insert.insert, Iff.mpr, Finset.card_pair_eq_two_iff, Imo1988P2.edgeSets_inter, Finset.card_singleton and 21 more
49 instances, coercions and auxiliary constants left out.

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