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

9 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2011, Problem 6

Imports (6)

Imported by 1 file

Compfiles.lean

lemma Usa2011P6.sum_card_filter_comm Documented declaration: sum_card_filter_comm line 39 source
Source documentation
Double counting: for a predicate p on t × u, the sum over a ∈ u of the number of indices i ∈ t satisfying p i a equals the sum over i ∈ t of the number of elements a ∈ u satisfying p i a.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Decidable, Eq, Nat, Finset.sum, Finset.card, Finset.filter
Proof uses: Eq.mpr, ite, OfNat.ofNat, id, congr, congrArg, Finset.sum_congr, Eq.refl, Membership.mem, Finset.card_filter, Finset.sum_comm
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma sum_card_filter_comm {ι α : Type*} {t : Finset ι} {u : Finset α}
    (p : ι → α → Prop) [∀ i a, Decidable (p i a)] :
    ∑ a ∈ u, (t.filter fun i ↦ p i a).card = ∑ i ∈ t, (u.filter fun a ↦ p i a).card := by
…
```
lemma Usa2011P6.card_powersetCard_filter_mem Documented declaration: card_powersetCard_filter_mem line 48 source
Source documentation
There are exactly 45 three-element subsets of an 11-element set containing a given element i: erasing i puts them in bijection with the 2-element subsets of the remaining 10 elements, and Nat.choose 10 2 = 45.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, Finset.card, Finset, Finset.filter, Membership.mem, Finset.powersetCard, Finset.univ
Proof uses: Finset.erase, Finset.card_bij', Insert.insert, And, LE.le, Eq.mp, congrArg, propext, Finset.mem_powersetCard, Finset.mem_filter, Eq.mpr, id, And.intro, Finset.erase_subset_erase, HSub.hSub, Finset.card_erase_of_mem, Eq.refl, Not, Finset.notMem_erase, Finset.insert_subset and 19 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma card_powersetCard_filter_mem (i : Fin 11) :
    (((Finset.univ : Finset (Fin 11)).powersetCard 3).filter fun T ↦ i ∈ T).card = 45 := by
…
```
lemma Usa2011P6.card_powersetCard_filter_mem₂ Documented declaration: card_powersetCard_filter_mem₂ line 80 source
Source documentation
There are exactly 9 three-element subsets of an 11-element set containing two given distinct elements i and j: erasing both puts them in bijection with the 1-element subsets of the remaining 9 elements, and Nat.choose 9 1 = 9.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Eq, Finset.card, Finset, Finset.filter, And, Membership.mem, Finset.powersetCard, Finset.univ
Proof uses: Finset.erase, Finset.card_bij', Insert.insert, LE.le, Eq.mp, congrArg, propext, Finset.mem_powersetCard, Finset.mem_filter, Iff.mpr, Finset.mem_erase, And.intro, Ne.symm, Eq.mpr, id, Finset.erase_subset_erase, HSub.hSub, Finset.card_erase_of_mem, Eq.refl, Not and 27 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma card_powersetCard_filter_mem₂ {i j : Fin 11} (hij : i ≠ j) :
    (((Finset.univ : Finset (Fin 11)).powersetCard 3).filter fun T ↦ i ∈ T ∧ j ∈ T).card
      = 9 := by
…
```
lemma Usa2011P6.sum_multiplicity The sum of the multiplicities of the elements of the union equals the sum of the sizes of the eleven sets, 11 * 45 = 495 line 128 source
Source documentation
The sum of the multiplicities of the elements of the union equals the sum of the sizes of the eleven sets, 11 * 45 = 495.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Fin, OfNat.ofNat, Nat, Finset, Eq, Finset.card, Finset.sum, Finset.biUnion, Finset.univ, Finset.filter, Membership.mem
Proof uses: Eq.mpr, id, congrArg, rfl, LE.le, Iff.mpr, Exists, And, Finset.mem_biUnion, Exists.intro, And.intro, Finset.mem_univ, Finset.filter_mem_eq_of_subset, Trans.trans, Usa2011P6.sum_card_filter_comm, Finset.sum_congr, Eq.refl, HMul.hMul, Finset.sum_const_nat, Fintype.card and 2 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma sum_multiplicity {α : Type*} [DecidableEq α] (As : Fin 11 → Finset α)
    (hcard : ∀ i, (As i).card = 45) :
    ∑ a ∈ Finset.univ.biUnion As, (Finset.univ.filter fun i ↦ a ∈ As i).card = 495 := by
…
```
lemma Usa2011P6.sum_inter_card The sum of the intersection sizes over all ordered pairs of indices equals 11 * 45 + 11 * 10 * 9 = 1485 line 146 source
Source documentation
The sum of the intersection sizes over all ordered pairs of indices equals 11 * 45 + 11 * 10 * 9 = 1485.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Fin, OfNat.ofNat, Nat, Finset, Eq, Finset.card, Ne, Inter.inter, Finset.sum, Prod, SProd.sprod, Finset.univ, Prod.fst, Prod.snd
Proof uses: Finset.diag, Membership.mem, Eq.mpr, id, congrArg, Eq.symm, And.right, Eq.mp, And, propext, Finset.mem_diag, Finset.inter_self, Eq.refl, HMul.hMul, Finset.sum_const_nat, Finset.diag_card, Fintype.card, Finset.card_univ, Fintype.card_fin, Finset.offDiag and 9 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma sum_inter_card {α : Type*} [DecidableEq α] (As : Fin 11 → Finset α)
    (hcard : ∀ i, (As i).card = 45)
    (hinter : ∀ i j, i ≠ j → (As i ∩ As j).card = 9) :
    ∑ ij ∈ (Finset.univ : Finset (Fin 11)) ×ˢ Finset.univ, (As ij.1 ∩ As ij.2).card
      = 1485 := by
…
```
lemma Usa2011P6.sum_sq_multiplicity_eq The sum of the squares of the multiplicities equals the sum of the intersection sizes over all ordered pairs of indices line 170 source
Source documentation
The sum of the squares of the multiplicities equals the sum of the intersection sizes over all ordered pairs of indices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Fin, OfNat.ofNat, Nat, Finset, Eq, Finset.sum, Finset.biUnion, Finset.univ, HPow.hPow, Finset.card, Finset.filter, Membership.mem, Prod, SProd.sprod, Inter.inter, Prod.fst, Prod.snd
Proof uses: Eq.mpr, id, congrArg, rfl, And, Finset.ext, Iff, congr, Iff.intro, And.intro, Iff.mpr, Exists, Finset.mem_biUnion, Exists.intro, Finset.mem_univ, of_eq_true, Prod.mk, Eq.trans, True, congrFun' and 10 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma sum_sq_multiplicity_eq {α : Type*} [DecidableEq α] (As : Fin 11 → Finset α) :
    ∑ a ∈ Finset.univ.biUnion As, (Finset.univ.filter fun i ↦ a ∈ As i).card ^ 2
      = ∑ ij ∈ (Finset.univ : Finset (Fin 11)) ×ˢ Finset.univ,
          (As ij.1 ∩ As ij.2).card := by
…
```
lemma Usa2011P6.sum_sq_multiplicity The sum of the squares of the multiplicities equals 11 * 45 + 11 * 10 * 9 = 1485 line 203 source
Source documentation
The sum of the squares of the multiplicities equals 11 * 45 + 11 * 10 * 9 = 1485.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Fin, OfNat.ofNat, Nat, Finset, Eq, Finset.card, Ne, Inter.inter, Finset.sum, Finset.biUnion, Finset.univ, HPow.hPow, Finset.filter, Membership.mem
Proof uses: Eq.trans, Prod, SProd.sprod, Prod.fst, Prod.snd, Usa2011P6.sum_sq_multiplicity_eq, Usa2011P6.sum_inter_card
23 instances, coercions and auxiliary constants left out.
```
lemma sum_sq_multiplicity {α : Type*} [DecidableEq α] (As : Fin 11 → Finset α)
    (hcard : ∀ i, (As i).card = 45)
    (hinter : ∀ i j, i ≠ j → (As i ∩ As j).card = 9) :
    ∑ a ∈ Finset.univ.biUnion As, (Finset.univ.filter fun i ↦ a ∈ As i).card ^ 2
      = 1485 :=
…
```
problem Usa2011P6.usa2011_p6 line 212 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Fin, OfNat.ofNat, Nat, Eq, Finset.card, LE.le, Ne, Inter.inter, Finset.biUnion, Finset.univ
Proof uses: Int, Finset.sum, Finset.filter, Membership.mem, cast, Eq.symm, Eq.trans, congrFun', congrArg, Usa2011P6.sum_multiplicity, HPow.hPow, Finset.sum_congr, Eq.refl, Usa2011P6.sum_sq_multiplicity, HMul.hMul, Finset.sum_mul_sq_le_sq_mul_sq, Eq.mp, congr, mul_one, HSMul.hSMul and 14 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
problem Usa2011P6.usa2011_p6_sharp line 240 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Finset, Sum, Fin, OfNat.ofNat, Nat, And, Eq, Finset.card, LE.le, Ne, Inter.inter, Finset.biUnion, Finset.univ
Proof uses: Finset.powersetCard, rfl, Union.union, Finset.image, Sum.inl, Sum.inr, Finset.filter, Membership.mem, Exists.intro, And.intro, Disjoint, Eq.mpr, Not, id, congrArg, propext, Finset.disjoint_left, False, Iff.mp, Finset.mem_image and 39 more
32 instances, coercions and auxiliary constants left out.

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