`Compfiles/Usa2022P1.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 2022, Problem 1

Let a and b be positive integers. The cells of an (a+b+1) × (a+b+1) grid are colored amber and bronze such that there are at least a² + ab - b amber cells and at least b² + ab - a bronze cells. Prove that it is possible to choose a amber cells and b bronze cells such that no two of the a + b chosen cells lie in the same row or column.

Imports (13)

Imported by 1 file

Compfiles.lean

abbrev Usa2022P1.Cell line 40 source
no axioms what this means
Statement uses: Nat
Proof uses: Prod, Fin
def Usa2022P1.colorCount line 42 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2022P1.Cell, Fin, OfNat.ofNat, Equiv.Perm
Proof uses: Finset.card, Finset.filter, Eq, Prod.mk, Finset.univ
7 instances, coercions and auxiliary constants left out.
def Usa2022P1.rowsToCells line 45 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Finset, Usa2022P1.Cell
Proof uses: Finset.map, Function.Embedding.mk, Prod.mk
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P1.rowsToCells_card line 51 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Finset, Eq, Finset.card, Usa2022P1.Cell, Usa2022P1.rowsToCells
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.card_map, Function.Embedding.mk, Prod.mk, eq_self
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P1.mem_rowsToCells line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Finset, Usa2022P1.Cell, Iff, Membership.mem, Usa2022P1.rowsToCells, Exists, And, Eq, Prod.mk
Proof uses: Iff.intro, Function.Embedding, Function.Embedding.mk, Eq.mp, Finset.map, congrArg, propext, Finset.mem_map, Usa2022P1.rowsToCells.eq_1, Exists.intro, And.intro, Eq.symm, of_eq_true, Eq.trans, True, eq_true
16 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P1.rowsToCells_color line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2022P1.Cell, Fin, OfNat.ofNat, Equiv.Perm, Finset, Membership.mem, Eq, Prod.mk, Usa2022P1.rowsToCells
Proof uses: And, Exists, Eq.mp, congrArg, propext, Usa2022P1.mem_rowsToCells, Eq.symm
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P1.rowsToCells_no_conflict line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Finset, Usa2022P1.Cell, Membership.mem, Union.union, Usa2022P1.rowsToCells, Ne, And, Prod.fst, Prod.snd
Proof uses: Exists, Eq, Prod.mk, Or, Eq.mp, congrArg, propext, Finset.mem_union, Usa2022P1.mem_rowsToCells, Exists.intro, And.intro, of_eq_true, Eq.trans, True, congrFun', Prod, congr, eq_self, Equiv.injective, Eq.symm
17 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P1.color_ne_zero_iff_eq_one line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Iff, Ne, Eq
Proof uses: List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, of_eq_true, Eq.trans, False, True, congr, congrArg and 15 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P1.colorCount_zero_add_one line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2022P1.Cell, Fin, OfNat.ofNat, Equiv.Perm, Eq, HAdd.hAdd, Usa2022P1.colorCount
Proof uses: Eq.mpr, Finset.card, Finset.filter, Prod.mk, Finset.univ, id, congrArg, Usa2022P1.colorCount.eq_1, Finset, Not, Finset.ext, of_eq_true, Iff, Membership.mem, Eq.trans, True, congr, And, congrFun', true_and and 7 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P1.colorCount_one_le_iff line 121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2022P1.Cell, Fin, OfNat.ofNat, Equiv.Perm, LE.le, Iff, Usa2022P1.colorCount, HSub.hSub
Proof uses: Iff.intro, Eq, HAdd.hAdd, Usa2022P1.colorCount_zero_add_one
16 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P1.colorCount_swap_le_add_two Adjacent permutations in the transposition graph differ in at most two rows line 133 source
Source comment
Adjacent permutations in the transposition graph differ in at most two rows.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2022P1.Cell, Fin, OfNat.ofNat, Equiv.Perm, LE.le, Usa2022P1.colorCount, HMul.hMul, Equiv.swap, HAdd.hAdd
Proof uses: id, Finset, Finset.filter, Eq, Prod.mk, Finset.univ, Union.union, Insert.insert, Singleton.singleton, Membership.mem, dite, of_eq_true, Eq.trans, Or, True, congr, congrArg, Finset.union_insert, Finset.union_singleton, eq_self and 18 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma colorCount_swap_le_add_two
    (color : Cell N → Fin 2) (p : Equiv.Perm (Fin N)) (x y : Fin N) :
    colorCount color 0 (p * Equiv.swap x y) ≤ colorCount color 0 p + 2 := by
…
```
Mentions: Usa2022P1.Cell, Usa2022P1.colorCount
lemma Usa2022P1.colorCount_swap_ge_sub_two line 157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2022P1.Cell, Fin, OfNat.ofNat, Equiv.Perm, LE.le, Usa2022P1.colorCount, HAdd.hAdd, HMul.hMul, Equiv.swap
Proof uses: Eq.mp, congrFun', congrArg, Eq.trans, mul_assoc, Equiv.swap_mul_self, mul_one, Usa2022P1.colorCount_swap_le_add_two
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P1.exists_transversal_with_exact_or_succ_color_count Walking from a color-rich transversal to a color-poor one gives count a or a+1 line 164 source
Source comment
Walking from a color-rich transversal to a color-poor one gives count a or a+1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2022P1.Cell, Fin, OfNat.ofNat, Equiv.Perm, LE.le, Usa2022P1.colorCount, HAdd.hAdd, Exists, Or, Eq
Proof uses: HMul.hMul, Equiv, Equiv.symm, Equiv.Perm.ext, Fin.ext, of_eq_true, Eq.trans, True, congrFun', congrArg, Equiv.apply_symm_apply, eq_self, Eq.mpr, id, GE.ge, Equiv.Perm.swap_induction_on', Exists.intro, Eq.mp, mul_one, Ne and 5 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma exists_transversal_with_exact_or_succ_color_count
    (color : Cell N → Fin 2) (a : ℕ) (p q : Equiv.Perm (Fin N))
    (hp : a ≤ colorCount color 0 p)
    (hq : colorCount color 0 q ≤ a + 1) :
    ∃ r : Equiv.Perm (Fin N), colorCount color 0 r = a ∨ colorCount color 0 r = a + 1 := by
…
```
Mentions: Usa2022P1.Cell, Usa2022P1.colorCount
def Usa2022P1.neighborCols Columns containing a good cell in one of the rows in R line 198 source
Source documentation
Columns containing a good cell in one of the rows in R.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2022P1.Cell, DecidablePred, Finset, Fin
Proof uses: Finset.filter, Exists, And, Membership.mem, Prod.mk, Finset.univ
7 instances, coercions and auxiliary constants left out.
```
def neighborCols (good : Cell N → Prop) [DecidablePred good]
    (R : Finset (Fin N)) : Finset (Fin N) :=
…
```
Mentions: Usa2022P1.Cell
def Usa2022P1.dummyCols The dummy columns used to turn "at least k real matches" into a full matching line 203 source
Source documentation
The dummy columns used to turn "at least k real matches" into a full matching.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Sum, Fin, HSub.hSub
Proof uses: Finset.map, Function.Embedding.inr, Finset.univ
5 instances, coercions and auxiliary constants left out.
```
def dummyCols (N k : ℕ) : Finset (Fin N ⊕ Fin (N - k)) :=
…
```
def Usa2022P1.hallTargets Hall targets for row r: good real columns, plus all dummy columns line 207 source
Source documentation
Hall targets for row r: good real columns, plus all dummy columns.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2022P1.Cell, DecidablePred, Fin, Finset, Sum, HSub.hSub
Proof uses: Finset.disjSum, Finset.filter, Prod.mk, Finset.univ
5 instances, coercions and auxiliary constants left out.
```
def hallTargets (good : Cell N → Prop) [DecidablePred good]
    (k : ℕ) (r : Fin N) : Finset (Fin N ⊕ Fin (N - k)) :=
…
```
Mentions: Usa2022P1.Cell
lemma Usa2022P1.line_count_le_of_hall_failure If Hall fails on rows R, then the rows outside R together with the neighboring columns of R form at most k - 1 covering lines line 215 source
Source documentation
If Hall fails on rows R, then the rows outside R together with the neighboring columns of R form at most k - 1 covering lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2022P1.Cell, DecidablePred, Finset, Fin, LT.lt, Finset.card, Sum, HSub.hSub, Finset.biUnion, Usa2022P1.hallTargets, LE.le, HAdd.hAdd, SDiff.sdiff, Finset.univ, Usa2022P1.neighborCols, OfNat.ofNat
Proof uses: Finset.Nonempty, Iff.mp, Finset.card_pos, Eq.mp, Fintype.card, congrArg, Fintype.card_fin, Finset.card_le_univ, Usa2022P1.dummyCols, Membership.mem, Eq.mpr, Exists, And, id, Eq, propext, Finset.mem_biUnion, Function.Embedding, Function.Embedding.inr, Finset.map and 31 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma line_count_le_of_hall_failure
    (good : Cell N → Prop) [DecidablePred good] {k : ℕ} {R : Finset (Fin N)}
    (hfail : (R.biUnion (hallTargets good k)).card < R.card) :
    ((univ : Finset (Fin N)) \ R).card + (neighborCols good R).card ≤ k - 1 := by
…
```
Mentions: Usa2022P1.Cell, Usa2022P1.hallTargets, Usa2022P1.neighborCols
lemma Usa2022P1.good_cells_card_le_of_neighbor_line_count Any good cells covered by at most k - 1 rows/columns number at most (k - 1) * N line 272 source
Source documentation
Any good cells covered by at most k - 1 rows/columns number at most (k - 1) * N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2022P1.Cell, DecidablePred, Finset, Fin, LE.le, HAdd.hAdd, Finset.card, SDiff.sdiff, Finset.univ, Usa2022P1.neighborCols, HSub.hSub, OfNat.ofNat, Finset.filter, HMul.hMul
Proof uses: Union.union, SProd.sprod, Prod, Membership.mem, Prod.mk, dite, Eq.mpr, Exists, And, id, Eq, Eq.trans, True, congrFun', congrArg, true_and, Exists.intro, And.intro, Eq.mp, of_eq_true and 42 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma good_cells_card_le_of_neighbor_line_count
    (good : Cell N → Prop) [DecidablePred good] {k : ℕ} (R : Finset (Fin N))
    (hline : ((univ : Finset (Fin N)) \ R).card + (neighborCols good R).card ≤ k - 1) :
    (univ.filter good).card ≤ (k - 1) * N := by
…
```
Mentions: Usa2022P1.Cell, Usa2022P1.neighborCols
lemma Usa2022P1.exists_transversal_with_many_good_cells Hall step: more than (k-1)N good cells force a transversal with k good cells line 308 source
Source comment
Hall step: more than (k-1)N good cells force a transversal with k good cells.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2022P1.Cell, DecidablePred, LE.le, LT.lt, HMul.hMul, HSub.hSub, OfNat.ofNat, Finset.card, Finset.filter, Finset.univ, Fin, Exists, Equiv.Perm, Prod.mk
Proof uses: Finset, Sum, Usa2022P1.dummyCols, Usa2022P1.hallTargets, Finset.biUnion, Decidable.byContradiction, Not, Nat.lt_of_not_ge, HAdd.hAdd, SDiff.sdiff, Usa2022P1.neighborCols, Usa2022P1.line_count_le_of_hall_failure, Usa2022P1.good_cells_card_le_of_neighbor_line_count, not_lt_of_ge, And, Function.Injective, Membership.mem, Iff.mp, Finset.all_card_le_biUnion_card_iff_existsInjective', Eq and 47 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 60 steps
Open to load the checked before-and-after goal states.
```
lemma exists_transversal_with_many_good_cells
    (good : Cell N → Prop) [DecidablePred good] {k : ℕ}
    (hkN : k ≤ N)
    (hcard : (k - 1) * N < (univ.filter good).card) :
    ∃ p : Equiv.Perm (Fin N),
      k ≤ (univ.filter fun r : Fin N => good (r, p r)).card := by
…
```
Mentions: Usa2022P1.Cell
lemma Usa2022P1.exists_intermediate_transversal_of_card_bounds The density hypotheses give a transversal with exactly a or a+1 amber cells line 385 source
Source documentation
The density hypotheses give a transversal with exactly a or a+1 amber cells.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Usa2022P1.Cell, HAdd.hAdd, Fin, LE.le, HSub.hSub, HPow.hPow, HMul.hMul, Fintype.card, Subtype, Eq, Exists, Equiv.Perm, Or, Usa2022P1.colorCount
Proof uses: Finset.card, Finset.filter, Finset.univ, Eq.mpr, id, Eq.mp, Eq.trans, congrArg, Fintype.card_subtype, Nat.casesAuxOn, Nat.succ, Nat.le, HEq, False.elim, Nat.le.refl, noConfusion_of_Nat, Nat.ctorIdx, Nat.le.step, Eq.refl, HEq.refl and 51 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma exists_intermediate_transversal_of_card_bounds
    (a b : ℕ)
    (ha : 0 < a)
    (hb : 0 < b)
    (color : Cell (a + b + 1) → Fin 2)
    (c0 : a ^ 2 + a * b - b ≤ Fintype.card {s // color s = 0})
    (c1 : b ^ 2 + a * b - a ≤ Fintype.card {s // color s = 1}) :
    ∃ p : Equiv.Perm (Fin (a + b + 1)),
      colorCount color 0 p = a ∨ colorCount color 0 p = a + 1 := by
…
```
Mentions: Usa2022P1.Cell, Usa2022P1.colorCount
lemma Usa2022P1.exists_cells_of_intermediate_transversal A transversal with a or a+1 amber cells contains the required amber/bronze choices line 442 source
Source documentation
A transversal with a or a+1 amber cells contains the required amber/bronze choices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2022P1.Cell, HAdd.hAdd, OfNat.ofNat, Fin, Equiv.Perm, Or, Eq, Usa2022P1.colorCount, Exists, Finset, And, Finset.card, Membership.mem, Union.union, Ne, Prod.fst, Prod.snd
Proof uses: Finset.filter, Prod.mk, Finset.univ, id, Usa2022P1.colorCount_zero_add_one, LE.le, Finset.exists_subset_card_eq, Exists.intro, Usa2022P1.rowsToCells, And.intro, of_eq_true, Eq.trans, True, congrFun', congrArg, Usa2022P1.rowsToCells_card, eq_self, Usa2022P1.rowsToCells_color, Eq.mp, true_and and 1 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
```
lemma exists_cells_of_intermediate_transversal
    {a b : ℕ}
    (color : Cell (a + b + 1) → Fin 2)
    (p : Equiv.Perm (Fin (a + b + 1)))
    (hp : colorCount color 0 p = a ∨ colorCount color 0 p = a + 1) :
    ∃ A B : Finset (Cell (a + b + 1)),
      A.card = a ∧ B.card = b ∧
      (∀ x ∈ A, color x = 0) ∧
      (∀ y ∈ B, color y = 1) ∧
      ∀ x ∈ A ∪ B, ∀ y ∈ A ∪ B, x ≠ y → x.fst ≠ y.fst ∧ x.snd ≠ y.snd := by
…
```
Mentions: Usa2022P1.Cell, Usa2022P1.colorCount
problem Usa2022P1.usa2022_p1 line 493 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Prod, Fin, HAdd.hAdd, LE.le, HSub.hSub, HPow.hPow, HMul.hMul, Fintype.card, Subtype, Eq, Exists, Finset, And, Finset.card, Membership.mem, Union.union, Ne and 2 more
Proof uses: Equiv.Perm, Or, Usa2022P1.colorCount, Usa2022P1.exists_intermediate_transversal_of_card_bounds, Usa2022P1.exists_cells_of_intermediate_transversal
47 instances, coercions and auxiliary constants left out.

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