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

22 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1975, Problem 5

A pack of n cards, including three aces, is well shuffled. Cards are turned over in turn. Show that the expected number of cards that must be turned over to reach the second ace is (n+1)/2.

Formalization notes

We model the well-shuffled pack by the set of positions occupied by the three aces, which is uniformly distributed over the 3-element subsets of {1, ..., n}. The number of cards that must be turned over to reach the second ace is then the middle (second-smallest) of the three ace positions, and the expected number of cards is the average of this quantity over all 3-element subsets.

Imports (12)

Imported by 1 file

Compfiles.lean

def Usa1975P5.aceSets The sample space: the 3-element subsets of the positions {1, ..., n}; each such subset records the positions of the three aces in the pack line 49 source
Source documentation
The sample space: the 3-element subsets of the positions {1, ..., n}; each such subset records the positions of the three aces in the pack.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: Finset.powersetCard, OfNat.ofNat, Finset.Icc
3 instances, coercions and auxiliary constants left out.
```
def aceSets (n : ℕ) : Finset (Finset ℕ) := (Icc 1 n).powersetCard 3
```
def Usa1975P5.reflect Reflection of the pack about its middle: the card in position x of a pack of n cards moves to position n + 1 - x line 53 source
Source documentation
Reflection of the pack about its middle: the card in position x of a pack of n cards moves to position n + 1 - x.

no axioms what this means
Statement uses: Nat
Proof uses: HSub.hSub, HAdd.hAdd, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def reflect (n x : ℕ) : ℕ := n + 1 - x
```
def Usa1975P5.minD The minimum of a set of naturals, defaulting to 0 for the empty set line 56 source
Source documentation
The minimum of a set of naturals, defaulting to 0 for the empty set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: WithTop.untopD, OfNat.ofNat, Finset.min
2 instances, coercions and auxiliary constants left out.
```
def minD (S : Finset ℕ) : ℕ := (S.min).untopD 0
```
Mentions: S
def Usa1975P5.maxD The maximum of a set of naturals, defaulting to 0 for the empty set line 59 source
Source documentation
The maximum of a set of naturals, defaulting to 0 for the empty set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: WithBot.unbotD, OfNat.ofNat, Finset.max
2 instances, coercions and auxiliary constants left out.
```
def maxD (S : Finset ℕ) : ℕ := (S.max).unbotD 0
```
Mentions: S
def Usa1975P5.mid The middle element of a 3-element set of natural numbers, computed as the sum minus the minimum minus the maximum line 64 source
Source documentation
The middle element of a 3-element set of natural numbers, computed as the sum minus the minimum minus the maximum. When S is the set of ace positions, this is the number of cards turned over to reach the second ace.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Int
Proof uses: HSub.hSub, Finset.sum, Usa1975P5.minD, Usa1975P5.maxD
5 instances, coercions and auxiliary constants left out.
```
def mid (S : Finset ℕ) : ℤ :=
…
```
Mentions: S
lemma Usa1975P5.card_aceSets line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Finset, Usa1975P5.aceSets, Nat.choose, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.powersetCard, Finset.Icc, Finset.card_powersetCard, HSub.hSub, HAdd.hAdd, Nat.card_Icc, add_tsub_cancel_right, eq_self
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1975P5.nonempty_of_mem_aceSets line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Membership.mem, Usa1975P5.aceSets, Finset.Nonempty
Proof uses: Eq, Finset.card, OfNat.ofNat, And.right, LE.le, Finset.Icc, Iff.mp, Finset.powersetCard, And, Finset.mem_powersetCard, LT.lt, Finset.card_pos
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1975P5.reflect_mem A card in position x ∈ {1, ..., n} reflects to a position in {1, ..., n} line 78 source
Source documentation
A card in position x ∈ {1, ..., n} reflects to a position in {1, ..., n}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Usa1975P5.reflect
Proof uses: Eq.mpr, And, LE.le, id, Eq, congrArg, propext, Finset.mem_Icc, Eq.mp
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma reflect_mem {n x : ℕ} (hx : x ∈ Icc 1 n) : reflect n x ∈ Icc 1 n := by
…
```
Mentions: Usa1975P5.reflect
lemma Usa1975P5.reflect_injOn Reflection is injective on positions that are at most n line 84 source
Source documentation
Reflection is injective on positions that are at most n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.InjOn, Usa1975P5.reflect, Set.ofPred, LE.le
Proof uses: Membership.mem, Set, Eq
4 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma reflect_injOn (n : ℕ) : Set.InjOn (reflect n) {x | x ≤ n} := by
…
```
Mentions: Usa1975P5.reflect
lemma Usa1975P5.reflect_reflect Reflection is an involution on positions that are at most n line 91 source
Source documentation
Reflection is an involution on positions that are at most n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Eq, Usa1975P5.reflect
Proof uses: id
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma reflect_reflect {n x : ℕ} (hx : x ≤ n) : reflect n (reflect n x) = x := by
…
```
Mentions: Usa1975P5.reflect
lemma Usa1975P5.min_image_reflect The minimum of the reflected set is the reflection of the maximum line 96 source
Source documentation
The minimum of the reflected set is the reflection of the maximum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, LE.le, Finset.Icc, OfNat.ofNat, Finset.Nonempty, Eq, Int, Usa1975P5.minD, Finset.image, Usa1975P5.reflect, HSub.hSub, HAdd.hAdd, Usa1975P5.maxD
Proof uses: Iff.mpr, Finset.image_nonempty, Membership.mem, Finset.max', Finset.max'_mem, And.right, Iff.mp, And, Finset.mem_Icc, Finset.min', le_antisymm, Finset.min'_le, Exists, Finset.mem_image, Exists.intro, And.intro, rfl, Finset.le_min', Finset.le_max', id and 46 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma min_image_reflect {n : ℕ} {S : Finset ℕ} (hsub : S ⊆ Icc 1 n) (hne : S.Nonempty) :
    (minD (S.image (reflect n)) : ℤ) = (n : ℤ) + 1 - (maxD S : ℤ) := by
…
```
Mentions: S, Usa1975P5.minD, Usa1975P5.reflect, Usa1975P5.maxD
lemma Usa1975P5.max_image_reflect The maximum of the reflected set is the reflection of the minimum line 119 source
Source documentation
The maximum of the reflected set is the reflection of the minimum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, LE.le, Finset.Icc, OfNat.ofNat, Finset.Nonempty, Eq, Int, Usa1975P5.maxD, Finset.image, Usa1975P5.reflect, HSub.hSub, HAdd.hAdd, Usa1975P5.minD
Proof uses: Iff.mpr, Finset.image_nonempty, Membership.mem, Finset.min', Finset.min'_mem, And.right, Iff.mp, And, Finset.mem_Icc, Finset.max', le_antisymm, Finset.max'_le, Exists, Finset.mem_image, Finset.min'_le, id, Finset.le_max', Exists.intro, And.intro, rfl and 46 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma max_image_reflect {n : ℕ} {S : Finset ℕ} (hsub : S ⊆ Icc 1 n) (hne : S.Nonempty) :
    (maxD (S.image (reflect n)) : ℤ) = (n : ℤ) + 1 - (minD S : ℤ) := by
…
```
Mentions: S, Usa1975P5.maxD, Usa1975P5.reflect, Usa1975P5.minD
lemma Usa1975P5.sum_image_reflect The sum of the reflected set is 3 * (n + 1) minus the sum of the set line 142 source
Source documentation
The sum of the reflected set is 3 * (n + 1) minus the sum of the set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, LE.le, Finset.Icc, OfNat.ofNat, Eq, Finset.card, Int, Finset.sum, Finset.image, Usa1975P5.reflect, HSub.hSub, HMul.hMul, HAdd.hAdd
Proof uses: Set.InjOn, Set.InjOn.mono, Nat.le, Membership.mem, Set, And.right, Iff.mp, And, Finset.mem_Icc, Usa1975P5.reflect_injOn, id, Eq.mpr, congrArg, Nat.cast_sub, congrFun', Eq.trans, Nat.cast_add, Nat.cast_one, Mathlib.Tactic.Ring.of_eq, Nat.rawCast and 41 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma sum_image_reflect {n : ℕ} {S : Finset ℕ} (hsub : S ⊆ Icc 1 n) (hcard : S.card = 3) :
    (∑ y ∈ S.image (reflect n), (y : ℤ)) = 3 * ((n : ℤ) + 1) - ∑ x ∈ S, (x : ℤ) := by
…
```
Mentions: S, Usa1975P5.reflect
lemma Usa1975P5.mid_image_reflect Reflecting every position turns the middle element m into n + 1 - m: this is the heart of the reflection argument line 161 source
Source documentation
Reflecting every position turns the middle element m into n + 1 - m: this is the heart of the reflection argument.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Membership.mem, Usa1975P5.aceSets, Eq, Int, Usa1975P5.mid, Finset.image, Usa1975P5.reflect, HSub.hSub, HAdd.hAdd, OfNat.ofNat
Proof uses: LE.le, Finset.Icc, Finset.card, And, Iff.mp, Finset.powersetCard, Finset.mem_powersetCard, Finset.Nonempty, Usa1975P5.nonempty_of_mem_aceSets, id, Eq.mpr, Finset.sum, Usa1975P5.minD, Usa1975P5.maxD, HMul.hMul, congrArg, Usa1975P5.sum_image_reflect, Usa1975P5.min_image_reflect, Usa1975P5.max_image_reflect, Mathlib.Tactic.Ring.of_eq and 42 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma mid_image_reflect {n : ℕ} {S : Finset ℕ} (hS : S ∈ aceSets n) :
    mid (S.image (reflect n)) = (n : ℤ) + 1 - mid S := by
…
```
Mentions: S, Usa1975P5.aceSets, Usa1975P5.mid, Usa1975P5.reflect
lemma Usa1975P5.image_mem_aceSets Reflecting the positions of the aces yields another valid set of positions line 170 source
Source documentation
Reflecting the positions of the aces yields another valid set of positions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Membership.mem, Usa1975P5.aceSets, Finset.image, Usa1975P5.reflect
Proof uses: LE.le, Finset.Icc, OfNat.ofNat, Eq, Finset.card, And, Iff.mp, Finset.powersetCard, Finset.mem_powersetCard, id, Eq.mpr, congrArg, propext, And.intro, Exists, Finset.mem_image, Usa1975P5.reflect_mem, Finset.card_image_of_injOn, Set.InjOn.mono, Nat.le and 4 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma image_mem_aceSets {n : ℕ} {S : Finset ℕ} (hS : S ∈ aceSets n) :
    S.image (reflect n) ∈ aceSets n := by
…
```
Mentions: S, Usa1975P5.aceSets, Usa1975P5.reflect
lemma Usa1975P5.image_image_reflect Reflection of position sets is an involution on the sample space line 184 source
Source documentation
Reflection of position sets is an involution on the sample space.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Membership.mem, Usa1975P5.aceSets, Eq, Finset.image, Usa1975P5.reflect
Proof uses: LE.le, Finset.Icc, OfNat.ofNat, Finset.card, And, Iff.mp, Finset.powersetCard, Finset.mem_powersetCard, Eq.mpr, Function.comp, id, congrArg, Finset.image_image, Trans.simple, Finset.image_congr, Set, Usa1975P5.reflect_reflect, And.right, Finset.mem_Icc, Finset.image_id'
16 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma image_image_reflect {n : ℕ} {S : Finset ℕ} (hS : S ∈ aceSets n) :
    (S.image (reflect n)).image (reflect n) = S := by
…
```
Mentions: S, Usa1975P5.aceSets, Usa1975P5.reflect
lemma Usa1975P5.image_reflect_injOn Reflection of position sets is injective on the sample space line 193 source
Source documentation
Reflection of position sets is injective on the sample space.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.InjOn, Finset, Finset.image, Usa1975P5.reflect, Usa1975P5.aceSets
Proof uses: Membership.mem, Set, Eq, id, Usa1975P5.image_image_reflect, Eq.symm, Eq.mp, congrArg
7 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma image_reflect_injOn (n : ℕ) :
    Set.InjOn (fun S : Finset ℕ => S.image (reflect n)) (aceSets n) := by
…
```
Mentions: S, Usa1975P5.reflect, Usa1975P5.aceSets
lemma Usa1975P5.image_reflect_aceSets Reflecting the position sets permutes the sample space line 204 source
Source documentation
Reflecting the position sets permutes the sample space.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Finset.image, Usa1975P5.reflect, Usa1975P5.aceSets
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, And, id, congrFun', congrArg, Iff.intro, Usa1975P5.image_mem_aceSets, Exists.intro, And.intro, Usa1975P5.image_image_reflect
10 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma image_reflect_aceSets (n : ℕ) :
    (aceSets n).image (fun S => S.image (reflect n)) = aceSets n := by
…
```
Mentions: Usa1975P5.aceSets, S, Usa1975P5.reflect
lemma Usa1975P5.sum_mid_image_reflect Reindexing the sum over the sample space by reflection line 215 source
Source documentation
Reindexing the sum over the sample space by reflection.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Finset.sum, Finset, Usa1975P5.aceSets, Usa1975P5.mid, Finset.image, Usa1975P5.reflect
Proof uses: Eq.symm, Finset.sum_image, Usa1975P5.image_reflect_injOn, Eq.mp, congrArg, Usa1975P5.image_reflect_aceSets
5 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma sum_mid_image_reflect (n : ℕ) :
    ∑ S ∈ aceSets n, mid (S.image (reflect n)) = ∑ S ∈ aceSets n, mid S := by
…
```
Mentions: S, Usa1975P5.aceSets, Usa1975P5.mid, Usa1975P5.reflect
lemma Usa1975P5.two_mul_sum_mid Twice the total of the middle positions equals (n + 1) times the number of position sets: the average middle position is (n + 1) / 2 line 223 source
Source documentation
Twice the total of the middle positions equals (n + 1) times the number of position sets: the average middle position is (n + 1) / 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, HMul.hMul, OfNat.ofNat, Finset.sum, Finset, Usa1975P5.aceSets, Usa1975P5.mid, Nat.choose, HAdd.hAdd
Proof uses: Finset.image, Usa1975P5.reflect, Membership.mem, Eq.mpr, HSub.hSub, id, congrArg, Usa1975P5.mid_image_reflect, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl and 31 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma two_mul_sum_mid (n : ℕ) :
    2 * (∑ S ∈ aceSets n, mid S) = (n.choose 3 : ℤ) * (n + 1) := by
…
```
Mentions: S, Usa1975P5.aceSets, Usa1975P5.mid
determine Usa1975P5.expected The expected number of cards that must be turned over to reach the second ace line 238 source
Source documentation
The expected number of cards that must be turned over to reach the second ace.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
determine expected (n : ℕ) : ℚ := (n + 1) / 2
```
problem Usa1975P5.usa1975_p5 line 240 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Rat, HDiv.hDiv, Finset.sum, Finset, Usa1975P5.aceSets, Usa1975P5.mid, Nat.choose, Usa1975P5.expected
Proof uses: HMul.hMul, HAdd.hAdd, Int, congrArg, Usa1975P5.two_mul_sum_mid, Eq.mp, congr, Eq.trans, Int.cast_mul, Int.cast_ofNat, Int.cast_sum, Int.cast_natCast, Int.cast_add, Int.cast_one, Ne, cast, Not, Eq.symm, Nat.cast_zero, LT.lt.ne' and 78 more
126 instances, coercions and auxiliary constants left out.

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