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

7 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1984, Problem 4

A maths exam has two papers, each with at least one question and 28 questions in total. Each pupil attempted 7 questions. Each pair of questions was attempted by just two pupils. Show that one pupil attempted either nil or at least 4 questions in the first paper.

Imports (9)

Imported by 1 file

Compfiles.lean

lemma Usa1984P4.sum_ite_erase Number of ordered pairs (q₁, q₂) with q₂ ∈ s and q₁ ≠ q₂, for a fixed question q₁, expressed as a sum of indicators over all questions line 55 source
Source documentation
Number of ordered pairs (q₁, q₂) with q₂ ∈ s and q₁ ≠ q₂, for a fixed question q₁, expressed as a sum of indicators over all questions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Fin, OfNat.ofNat, Nat, Eq, Finset.sum, Finset.univ, ite, And, Membership.mem, Ne, HSub.hSub, Finset.card
Proof uses: dite, Eq.mpr, id, congrArg, ite_eq_left, Finset.filter, Finset.erase, Finset.ext, Iff, congr, Eq.trans, True, congrFun', true_and, Iff.intro, And.intro, Ne.symm, And.right, And.left, Eq.symm and 6 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma sum_ite_erase (s : Finset (Fin 28)) (q1 : Fin 28) :
    ∑ q2 : Fin 28, (if q1 ∈ s ∧ q2 ∈ s ∧ q1 ≠ q2 then (1 : ℕ) else 0)
      = if q1 ∈ s then s.card - 1 else 0 := by
…
```
lemma Usa1984P4.card_ordered_pairs The number of ordered pairs of distinct questions in s, written as a double sum of indicators over all questions line 76 source
Source documentation
The number of ordered pairs of distinct questions in s, written as a double sum of indicators over all questions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Fin, OfNat.ofNat, Nat, Eq, Finset.sum, Finset.univ, ite, And, Membership.mem, Ne, HMul.hMul, Finset.card, HSub.hSub
Proof uses: Eq.mpr, id, congrArg, Finset.sum_congr, rfl, Usa1984P4.sum_ite_erase, Inter.inter, Finset.sum_ite_mem, Finset.univ_inter, HSMul.hSMul, Finset.sum_const, smul_eq_mul, Eq.refl
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma card_ordered_pairs (s : Finset (Fin 28)) :
    ∑ q1 : Fin 28, ∑ q2 : Fin 28, (if q1 ∈ s ∧ q2 ∈ s ∧ q1 ≠ q2 then (1 : ℕ) else 0)
      = s.card * (s.card - 1) := by
…
```
lemma Usa1984P4.sum_pupils_pair For fixed questions q₁ ≠ q₂, the number of pupils that attempted both is 2, expressed as a sum of indicators over all pupils line 84 source
Source documentation
For fixed questions q₁ ≠ q₂, the number of pupils that attempted both is 2, expressed as a sum of indicators over all pupils.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Finset, Fin, OfNat.ofNat, Nat, Ne, Eq, Finset.card, Finset.filter, And, Membership.mem, Finset.univ, Finset.sum, ite
Proof uses: dite, Eq.mpr, id, congrArg, ite_eq_left, Finset.ext, Iff, congr, Eq.trans, True, congrFun', true_and, Iff.intro, And.intro, And.left, And.right, Eq.symm, Finset.card_filter, Eq.refl, Not and 4 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma sum_pupils_pair {Pupil : Type} [Fintype Pupil] (attempt : Pupil → Finset (Fin 28))
    (hpair : ∀ q1 q2 : Fin 28, q1 ≠ q2 →
      (Finset.univ.filter fun p ↦ q1 ∈ attempt p ∧ q2 ∈ attempt p).card = 2)
    (q1 q2 : Fin 28) :
    (∑ p : Pupil, if q1 ∈ attempt p ∧ q2 ∈ attempt p ∧ q1 ≠ q2 then (1 : ℕ) else 0)
      = if q1 ≠ q2 then 2 else 0 := by
…
```
lemma Usa1984P4.sum_two_distinct For a fixed question q₁, the number of questions q₂ ≠ q₁ is 27, so summing the constant 2 over them gives 54 line 110 source
Source documentation
For a fixed question q₁, the number of questions q₂ ≠ q₁ is 27, so summing the constant 2 over them gives 54.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, Finset.sum, Finset.univ, ite, Ne
Proof uses: Finset, Finset.filter, Finset.erase, Finset.filter_ne, Eq.mpr, id, congrArg, Eq.symm, Finset.sum_filter, HSMul.hSMul, Finset.card, Finset.sum_const, HSub.hSub, Finset.card_erase_of_mem, Finset.mem_univ, Fintype.card, Finset.card_univ, Fintype.card_fin, HMul.hMul, smul_eq_mul and 1 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma sum_two_distinct (q1 : Fin 28) :
    ∑ q2 : Fin 28, (if q1 ≠ q2 then (2 : ℕ) else 0) = 54 := by
…
```
lemma Usa1984P4.card_pupils Double counting ordered pairs of distinct questions attempted by the same pupil shows there are 36 pupils line 120 source
Source documentation
Double counting ordered pairs of distinct questions attempted by the same pupil shows there are 36 pupils.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Finset, Fin, OfNat.ofNat, Nat, Eq, Finset.card, Ne, Finset.filter, And, Membership.mem, Finset.univ, Fintype.card
Proof uses: Finset.sum, ite, HMul.hMul, Eq.mpr, HSub.hSub, id, congrArg, Finset.sum_congr, rfl, Usa1984P4.card_ordered_pairs, Eq.refl, HSMul.hSMul, Finset.sum_const, Finset.card_univ, smul_eq_mul, Eq.symm, Finset.sum_comm_cycle, Usa1984P4.sum_pupils_pair, Usa1984P4.sum_two_distinct, Fintype.card_fin and 1 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma card_pupils {Pupil : Type} [Fintype Pupil] (attempt : Pupil → Finset (Fin 28))
    (hattempt : ∀ p, (attempt p).card = 7)
    (hpair : ∀ q1 q2 : Fin 28, q1 ≠ q2 →
      (Finset.univ.filter fun p ↦ q1 ∈ attempt p ∧ q2 ∈ attempt p).card = 2) :
    Fintype.card Pupil = 36 := by
…
```
lemma Usa1984P4.card_attempters Double counting the pairs (p, q₂) with q and q₂ both attempted by p shows every question was attempted by exactly 9 pupils line 149 source
Source documentation
Double counting the pairs (p, q₂) with q and q₂ both attempted by p shows every question was attempted by exactly 9 pupils.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Finset, Fin, OfNat.ofNat, Nat, Eq, Finset.card, Ne, Finset.filter, And, Membership.mem, Finset.univ
Proof uses: Finset.sum, ite, HMul.hMul, Eq.mpr, HSub.hSub, id, congrArg, Finset.sum_congr, rfl, Usa1984P4.sum_ite_erase, Eq.refl, Eq.symm, Finset.sum_filter, HSMul.hSMul, Finset.sum_const, smul_eq_mul, Finset.sum_comm, Usa1984P4.sum_pupils_pair, Usa1984P4.sum_two_distinct, Eq.mp
29 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma card_attempters {Pupil : Type} [Fintype Pupil] (attempt : Pupil → Finset (Fin 28))
    (hattempt : ∀ p, (attempt p).card = 7)
    (hpair : ∀ q1 q2 : Fin 28, q1 ≠ q2 →
      (Finset.univ.filter fun p ↦ q1 ∈ attempt p ∧ q2 ∈ attempt p).card = 2)
    (q : Fin 28) :
    (Finset.univ.filter fun p ↦ q ∈ attempt p).card = 9 := by
…
```
problem Usa1984P4.usa1984_p4 line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Finset, Fin, OfNat.ofNat, Nat, Eq, Finset.card, Ne, Finset.filter, And, Membership.mem, Finset.univ, Finset.Nonempty, SDiff.sdiff, Exists, Or, Inter.inter, LE.le
Proof uses: Decidable.byContradiction, Not, Iff.mpr, Nat.one_le_iff_ne_zero, And.left, LT.lt, Eq.mp, Eq.trans, binderNameHint, forall_congr, congrArg, And.right, Fintype.card, Usa1984P4.card_pupils, Finset.card_pos, Finset.sum, HMul.hMul, ite, Eq.mpr, id and 130 more
164 instances, coercions and auxiliary constants left out.

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