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

15 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1986, Problem 2

Five professors attended a lecture. Each fell asleep just twice. For each pair there was a moment when both were asleep. Show that there was a moment when three of them were asleep.

Imports (7)

Imported by 1 file

Compfiles.lean

def Usa1986P2.Asleep Each professor p : Fin 5 takes two naps, and nap k : Fin 2 of professor p is the closed interval [s p k, e p k] line 34 source
Source documentation
Each professor p : Fin 5 takes two naps, and nap k : Fin 2 of professor p is the closed interval [s p k, e p k]. Professor p is asleep at time t if t belongs to one of these two nap intervals.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real
Proof uses: Exists, And, LE.le
3 instances, coercions and auxiliary constants left out.
```
def Asleep (s e : Fin 5 → Fin 2 → ℝ) (p : Fin 5) (t : ℝ) : Prop :=
…
```
def Usa1986P2.pairs The ten pairs of professors, as the 2-element subsets of Fin 5 line 40 source
Source documentation
The ten pairs of professors, as the 2-element subsets of Fin 5.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Fin, OfNat.ofNat, Nat
Proof uses: Finset.powersetCard, Finset.univ
3 instances, coercions and auxiliary constants left out.
```
def pairs : Finset (Finset (Fin 5)) := Finset.powersetCard 2 Finset.univ
```
abbrev Usa1986P2.PairSet The type of pairs of professors line 43 source
Source documentation
The type of pairs of professors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Subtype, Finset, Fin, OfNat.ofNat, Nat, Membership.mem, Usa1986P2.pairs
3 instances, coercions and auxiliary constants left out.
```
abbrev PairSet := { A : Finset (Fin 5) // A ∈ pairs }
…
```
Mentions: Usa1986P2.pairs
def Usa1986P2.cands Candidate "first moments" for a set A of professors: nap-start times of members of A at which every member of A is asleep line 50 source
Source documentation
Candidate "first moments" for a set A of professors: nap-start times of members of A at which every member of A is asleep.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Finset
Proof uses: Finset.filter, Membership.mem, Usa1986P2.Asleep, Classical.propDecidable, Finset.biUnion, Finset.image, Finset.univ
10 instances, coercions and auxiliary constants left out.
```
noncomputable def cands (s e : Fin 5 → Fin 2 → ℝ) (A : Finset (Fin 5)) : Finset ℝ :=
…
```
lemma Usa1986P2.mem_cands Membership in cands: a nap-start time of a member of A at which every member of A is asleep line 56 source
Source documentation
Membership in cands: a nap-start time of a member of A at which every member of A is asleep.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Finset, Iff, Membership.mem, Usa1986P2.cands, And, Exists, Eq, Usa1986P2.Asleep
Proof uses: id, of_eq_true, Finset.filter, Classical.propDecidable, Finset.biUnion, Finset.image, Finset.univ, Eq.trans, True, congrFun', congrArg, funext, true_and, iff_self
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma mem_cands {A : Finset (Fin 5)} {u : ℝ} :
    u ∈ cands s e A ↔
      (∃ p ∈ A, ∃ k : Fin 2, s p k = u) ∧ ∀ p ∈ A, Asleep s e p u := by
…
```
Mentions: Usa1986P2.cands, Usa1986P2.Asleep
lemma Usa1986P2.exists_mem_cands_le Documented declaration: exists_mem_cands_le line 66 source
Source documentation
If all members of a nonempty set A of professors are asleep at time t, then some nap-start time u ≤ t of a member of A is already a moment when all members of A are asleep.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Finset, Finset.Nonempty, Membership.mem, Usa1986P2.Asleep, Exists, And, Usa1986P2.cands, LE.le
Proof uses: Subtype, Subtype.property, Finset.attach, Finset.exists_max_image, Iff.mpr, Finset.attach_nonempty_iff, Exists.intro, And.intro, Eq, Usa1986P2.mem_cands, rfl, Subtype.mk, Finset.mem_attach, LE.le.trans, And.left, And.right, Classical.choose, Classical.choose_spec
19 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma exists_mem_cands_le {A : Finset (Fin 5)} (hA : A.Nonempty) {t : ℝ}
    (ht : ∀ p ∈ A, Asleep s e p t) : ∃ u ∈ cands s e A, u ≤ t := by
…
```
Mentions: Usa1986P2.Asleep, Usa1986P2.cands
def Usa1986P2.f The first moment at which all members of A are simultaneously asleep line 76 source
Source documentation
The first moment at which all members of A are simultaneously asleep.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Finset, Finset.Nonempty, Usa1986P2.cands
Proof uses: Finset.min'
3 instances, coercions and auxiliary constants left out.
```
noncomputable def f (s e : Fin 5 → Fin 2 → ℝ) (A : Finset (Fin 5))
    (h : (cands s e A).Nonempty) : ℝ := (cands s e A).min' h
```
Mentions: h, Usa1986P2.cands
lemma Usa1986P2.f_asleep All members of A are asleep at the first common moment line 80 source
Source documentation
All members of A are asleep at the first common moment.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Finset, Finset.Nonempty, Usa1986P2.cands, Membership.mem, Usa1986P2.Asleep, Usa1986P2.f
Proof uses: Finset.min', Finset.min'_mem, And.right, Exists, And, Eq, Iff.mp, Usa1986P2.mem_cands
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma f_asleep {A : Finset (Fin 5)} {h : (cands s e A).Nonempty} :
    ∀ p ∈ A, Asleep s e p (f s e A h) := by
…
```
Mentions: h, Usa1986P2.cands, Usa1986P2.Asleep, Usa1986P2.f
lemma Usa1986P2.f_mem The first common moment is a nap-start time of some member of A line 86 source
Source documentation
The first common moment is a nap-start time of some member of A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Finset, Finset.Nonempty, Usa1986P2.cands, Exists, And, Membership.mem, Eq, Usa1986P2.f
Proof uses: Finset.min', Finset.min'_mem, And.left, Usa1986P2.Asleep, Iff.mp, Usa1986P2.mem_cands, Exists.intro, And.intro, Eq.symm
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma f_mem {A : Finset (Fin 5)} {h : (cands s e A).Nonempty} :
    ∃ p ∈ A, ∃ k : Fin 2, f s e A h = s p k := by
…
```
Mentions: h, Usa1986P2.cands, Usa1986P2.f
lemma Usa1986P2.f_le The first common moment is at most any moment at which all members of A are asleep line 94 source
Source documentation
The first common moment is at most any moment at which all members of A are asleep.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Finset, Finset.Nonempty, Usa1986P2.cands, Membership.mem, Usa1986P2.Asleep, LE.le, Usa1986P2.f
Proof uses: And, Exists, Usa1986P2.exists_mem_cands_le, LE.le.trans, Finset.min', Exists.intro, Finset.min'_le
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma f_le {A : Finset (Fin 5)} (hA : A.Nonempty) {h : (cands s e A).Nonempty}
    {t : ℝ} (ht : ∀ p ∈ A, Asleep s e p t) : f s e A h ≤ t := by
…
```
Mentions: h, Usa1986P2.cands, Usa1986P2.Asleep, Usa1986P2.f
lemma Usa1986P2.cands_nonempty Pairs of professors have candidate first moments line 100 source
Source documentation
Pairs of professors have candidate first moments.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Ne, Exists, And, Usa1986P2.Asleep, Finset, Eq, Finset.card, Finset.Nonempty, Usa1986P2.cands
Proof uses: Insert.insert, Singleton.singleton, Iff.mp, Finset.card_eq_two, Membership.mem, Or, Eq.mp, congrArg, propext, Finset.mem_singleton, Finset.mem_insert, LE.le, Usa1986P2.exists_mem_cands_le, Exists.intro, Finset.mem_insert_self, Eq.symm
12 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma cands_nonempty
    (hsleep : ∀ p q : Fin 5, p ≠ q → ∃ t, Asleep s e p t ∧ Asleep s e q t)
    {A : Finset (Fin 5)} (hA : A.card = 2) : (cands s e A).Nonempty := by
…
```
Mentions: Usa1986P2.Asleep, Usa1986P2.cands
def Usa1986P2.F The first moment when both members of a pair A are asleep line 115 source
Source documentation
The first moment when both members of a pair A are asleep.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Ne, Exists, And, Usa1986P2.Asleep, Usa1986P2.PairSet
Proof uses: Usa1986P2.f, Finset, Membership.mem, Usa1986P2.pairs
6 instances, coercions and auxiliary constants left out.
```
noncomputable def F
    (hsleep : ∀ p q : Fin 5, p ≠ q → ∃ t, Asleep s e p t ∧ Asleep s e q t)
    (A : PairSet) : ℝ :=
…
```
Mentions: Usa1986P2.Asleep, Usa1986P2.PairSet
lemma Usa1986P2.F_asleep Both members of a pair are asleep at the pair's first common moment line 121 source
Source documentation
Both members of a pair are asleep at the pair's first common moment.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Ne, Exists, And, Usa1986P2.Asleep, Usa1986P2.PairSet, Membership.mem, Finset, Usa1986P2.pairs, Usa1986P2.F
Proof uses: Usa1986P2.f_asleep
9 instances, coercions and auxiliary constants left out.
```
lemma F_asleep
    (hsleep : ∀ p q : Fin 5, p ≠ q → ∃ t, Asleep s e p t ∧ Asleep s e q t)
    (A : PairSet) {p : Fin 5} (hp : p ∈ A.1) : Asleep s e p (F hsleep A) :=
…
```
Mentions: Usa1986P2.Asleep, Usa1986P2.PairSet, Usa1986P2.F
lemma Usa1986P2.F_mem A pair's first common moment is a falling-asleep event: it is the start time of a nap of one of the two members line 128 source
Source documentation
A pair's first common moment is a falling-asleep event: it is the start time of a nap of one of the two members.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Ne, Exists, And, Usa1986P2.Asleep, Usa1986P2.PairSet, Membership.mem, Finset, Usa1986P2.pairs, Eq, Usa1986P2.F
Proof uses: Usa1986P2.f_mem
9 instances, coercions and auxiliary constants left out.
```
lemma F_mem
    (hsleep : ∀ p q : Fin 5, p ≠ q → ∃ t, Asleep s e p t ∧ Asleep s e q t)
    (A : PairSet) : ∃ p ∈ A.1, ∃ k : Fin 2, F hsleep A = s p k :=
…
```
Mentions: Usa1986P2.Asleep, Usa1986P2.PairSet, Usa1986P2.F
problem Usa1986P2.usa1986_p2 line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Ne, Exists, And, Usa1986P2.Asleep
Proof uses: Eq, Finset.card, Finset, Usa1986P2.pairs, Eq.mpr, Finset.powersetCard, Finset.univ, id, congrArg, Usa1986P2.pairs.eq_1, Nat.choose, Finset.card_powersetCard, Fintype.card, Finset.card_univ, Fintype.card_fin, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl and 78 more
52 instances, coercions and auxiliary constants left out.

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