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

5 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1979, Problem 5

X has n members. Given n+1 subsets of X, each with 3 members, show that we can always find two which have just one member in common.

Imports (5)

Imported by 1 file

Compfiles.lean

theorem Usa1979P5.card_inter_eq_two_of_good Documented declaration: card_inter_eq_two_of_good line 35 source
Source documentation
If two distinct members s, t of a "good" family (no two sets share exactly one element) each have three elements and intersect nontrivially, then they share exactly two elements.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Membership.mem, Ne, Nat, Finset.card, Inter.inter, OfNat.ofNat, Eq, LT.lt
Proof uses: LE.le, Trans.trans, Finset.card_le_card, Finset.inter_subset_right, Finset.eq_of_subset_of_card_le, Eq.rec, Finset.inter_subset_left, Eq.symm
18 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem card_inter_eq_two_of_good {α : Type*} [DecidableEq α] {S : Finset (Finset α)}
    (hgood : ∀ s ∈ S, ∀ t ∈ S, s ≠ t → (s ∩ t).card ≠ 1)
    {s t : Finset α} (hs : s ∈ S) (ht : t ∈ S) (hne : s ≠ t)
    (hs3 : s.card = 3) (ht3 : t.card = 3) (hpos : 0 < (s ∩ t).card) :
    (s ∩ t).card = 2 := by
…
```
Mentions: S
theorem Usa1979P5.mem_third_of_inter If u, v = {w, x, y} are members of a "good" family, w ∈ u ∩ v and x ∉ u, then y ∈ u: otherwise u ∩ v = {w} would be a singleton intersection line 54 source
Source documentation
If u, v = {w, x, y} are members of a "good" family, w ∈ u ∩ v and x ∉ u, then y ∈ u: otherwise u ∩ v = {w} would be a singleton intersection.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Membership.mem, Ne, Nat, Finset.card, Inter.inter, OfNat.ofNat, Not, Eq, Insert.insert, Singleton.singleton
Proof uses: Decidable.byContradiction, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, Or, True, congr, eq_self, true_or, or_true, Eq.mp, Eq.symm, LE.le, And.right, And, propext, Finset.mem_inter, Finset.mem_singleton_self and 8 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
theorem mem_third_of_inter {α : Type*} [DecidableEq α] {S : Finset (Finset α)}
    (hgood : ∀ s ∈ S, ∀ t ∈ S, s ≠ t → (s ∩ t).card ≠ 1)
    {u v : Finset α} {w x y : α}
    (hu : u ∈ S) (hv : v ∈ S) (hw : w ∈ u ∩ v) (hx : x ∉ u) (hv_eq : v = {w, x, y}) :
    y ∈ u := by
…
```
Mentions: S
theorem Usa1979P5.sum_card_filter_eq_three_mul Double counting of the incidences between X and a family of 3-element subsets of X line 80 source
Source documentation
Double counting of the incidences between X and a family of 3-element subsets of X.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Membership.mem, LE.le, Eq, Nat, Finset.card, OfNat.ofNat, Finset.sum, Finset.filter, HMul.hMul
Proof uses: ite, Finset.card_filter, Eq.mpr, id, congrArg, Finset.sum_congr, rfl, Finset.sum_comm, Eq.symm, Inter.inter, Finset.filter_mem_eq_inter, Iff.mpr, Finset.inter_eq_right, HSMul.hSMul, Finset.sum_const, smul_eq_mul, mul_comm, Eq.refl
31 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem sum_card_filter_eq_three_mul {α : Type*} [DecidableEq α]
    {X : Finset α} {S : Finset (Finset α)}
    (hsub : ∀ s ∈ S, s ⊆ X) (hcard : ∀ s ∈ S, s.card = 3) :
    ∑ x ∈ X, (S.filter (fun s ↦ x ∈ s)).card = 3 * S.card := by
…
```
Mentions: S
theorem Usa1979P5.card_le_of_good Main step: a "good" family of 3-element subsets of an n-element set has at most n members line 97 source
Source documentation
Main step: a "good" family of 3-element subsets of an n-element set has at most n members. Proved by strong induction on n, following the informal argument for USAMO 1979 problem 5.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Nat, Finset, Eq, Finset.card, Membership.mem, LE.le, OfNat.ofNat, Ne, Inter.inter
Proof uses: Nat.strongRecOn, LT.lt, dite, Exists, And, Finset.filter, rfl, Iff, Eq.mpr, id, congrArg, Finset.mem_filter, Eq.mp, Finset.Nonempty, Iff.mp, Finset.card_pos, And.left, And.right, Finset.erase, HSub.hSub and 85 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 366 steps (first 200 of 366)
Open to load the checked before-and-after goal states.
```
theorem card_le_of_good {α : Type*} [DecidableEq α] :
    ∀ n : ℕ, ∀ (X : Finset α) (S : Finset (Finset α)),
    X.card = n → (∀ s ∈ S, s ⊆ X) → (∀ s ∈ S, s.card = 3) →
    (∀ s ∈ S, ∀ t ∈ S, s ≠ t → (s ∩ t).card ≠ 1) → S.card ≤ n := by
…
```
Mentions: S
problem Usa1979P5.usa1979_p5 line 449 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Nat, Finset, Eq, Finset.card, HAdd.hAdd, OfNat.ofNat, Membership.mem, LE.le, Exists, And, Ne, Inter.inter
Proof uses: Decidable.byContradiction, Not, Usa1979P5.card_le_of_good, Eq.mp, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl
26 instances, coercions and auxiliary constants left out.

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