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

USA Mathematical Olympiad 2007, Problem 3

Let S be a set containing n² + n − 1 elements. Suppose that the n-element subsets of S are partitioned into two classes. Prove that there are at least n pairwise disjoint sets in the same class.

Imports (4)

Imported by 1 file

Compfiles.lean

lemma Usa2007P3.exists_disjoint_family Any finite set S with k * n ≤ S.card contains k pairwise disjoint n-element subsets (here 1 ≤ n) line 34 source
Source documentation
Any finite set S with k * n ≤ S.card contains k pairwise disjoint n-element subsets (here 1 ≤ n).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Nat, LE.le, OfNat.ofNat, Finset, HMul.hMul, Finset.card, Exists, And, Eq, Membership.mem, Set.PairwiseDisjoint, id
Proof uses: Nat.recAux, Exists.intro, EmptyCollection.emptyCollection, And.intro, Finset.card_empty, False.elim, Finset.notMem_empty, of_eq_true, Eq.trans, Set, True, congrFun', congrArg, Finset.coe_empty, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr and 47 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
lemma exists_disjoint_family {n : ℕ} (hn : 1 ≤ n) :
    ∀ k : ℕ, ∀ S : Finset α, k * n ≤ S.card →
      ∃ F : Finset (Finset α), F.card = k ∧ (∀ A ∈ F, A ⊆ S ∧ A.card = n) ∧
        (F : Set (Finset α)).PairwiseDisjoint id := by
…
```
Mentions: S
lemma Usa2007P3.color_eq Documented declaration: color_eq line 79 source
Source documentation
If every (n+1)-element subset U of S is monochromatic (i.e. all of its n-element subsets have the same color), then all n-element subsets of S have the same color: any two n-element sets can be joined by a chain in which consecutive sets differ in exactly one element, so induction on the size of the symmetric difference applies.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Bool, Nat, LE.le, Eq, Finset.card, HAdd.hAdd, OfNat.ofNat, SDiff.sdiff
Proof uses: Nat.recAux, Eq.mpr, EmptyCollection.emptyCollection, id, congrArg, Eq.symm, propext, Finset.sdiff_eq_empty_iff_subset, Finset.card_eq_zero, Nat.eq_zero_of_le_zero, Finset.eq_of_subset_of_card_le, Eq.refl, dite, Not, Membership.mem, Finset.Nonempty, LT.lt, Finset.card_pos, Nat.succ_pos, HSub.hSub and 25 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
```
lemma color_eq (col : Finset α → Bool) {n : ℕ} {S : Finset α}
    (H : ∀ U : Finset α, U ⊆ S → U.card = n + 1 →
      ∀ A B : Finset α, A ⊆ U → B ⊆ U → A.card = n → B.card = n → col A = col B) :
    ∀ m : ℕ, ∀ A B : Finset α, A ⊆ S → B ⊆ S → A.card = n → B.card = n →
      (A \ B).card ≤ m → col A = col B := by
…
```
Mentions: S
lemma Usa2007P3.main Documented declaration: main line 138 source
Source documentation
The strengthened statement, proved by induction on k: if S has k * (n + 1) - 1 elements and the n-element subsets of S are two-colored (by col), then one can find k pairwise disjoint n-element subsets of S having the same color.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Bool, Nat, LE.le, OfNat.ofNat, Eq, Finset.card, HSub.hSub, HMul.hMul, HAdd.hAdd, Exists, And, Membership.mem, Set.PairwiseDisjoint, id
Proof uses: Nat.recAux, Exists.intro, EmptyCollection.emptyCollection, And.intro, Nat.zero_le, False.elim, Finset.notMem_empty, of_eq_true, Eq.trans, Set, True, congrFun', congrArg, Finset.coe_empty, Bool.true, Classical.byContradiction, Not, SDiff.sdiff, Eq.mpr, Finset.card_sdiff_of_subset and 59 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 75 steps
Open to load the checked before-and-after goal states.
```
lemma main (col : Finset α → Bool) {n : ℕ} (hn : 1 ≤ n) :
    ∀ k : ℕ, ∀ S : Finset α, S.card = k * (n + 1) - 1 →
      ∃ F : Finset (Finset α), k ≤ F.card ∧ (∀ A ∈ F, A ⊆ S ∧ A.card = n) ∧
        (F : Set (Finset α)).PairwiseDisjoint id ∧ ∃ b : Bool, ∀ A ∈ F, col A = b := by
…
```
Mentions: S
problem Usa2007P3.usa2007_p3 line 218 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, DecidableEq, Finset, Eq, Finset.card, HSub.hSub, HAdd.hAdd, HPow.hPow, Bool, Exists, And, LE.le, Membership.mem, Set.PairwiseDisjoint, id
Proof uses: HMul.hMul, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_mul and 15 more
44 instances, coercions and auxiliary constants left out.

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