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

61 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2004, Problem 4

Alice and Bob play a game on a 6 by 6 grid. On his turn, a player chooses a rational number not yet appearing in the grid and writes it in an empty square of the grid. Alice goes first and then the players alternate. When all squares have numbers written in them, in each row, the square with the greatest number in that row is colored black. Alice wins if he can then draw a line from the top of the grid to the bottom of the grid that stays in black squares, and Bob wins if he can't. (If two squares share a vertex, Alice can draw a line from one to the other that stays in those two squares.) Find, with proof, a winning strategy for one of the players.

Imports (9)

Imported by 1 file

Compfiles.lean

abbrev Usa2004P4.Cell A cell of the 6×6 grid: (row, column), both in Fin 6 line 45 source
Source documentation
A cell of the 6×6 grid: (row, column), both in Fin 6. Row 0 is the top row of the grid and row 5 the bottom row.

no axioms what this means
Proof uses: Prod, Fin, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
```
abbrev Cell : Type := Fin 6 × Fin 6
…
```
def Usa2004P4.colMate The pairing of columns: each column is paired with the column three places away line 52 source
Source documentation
The pairing of columns: each column is paired with the column three places away.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat
Proof uses: Fin.mk, ite, LT.lt, HAdd.hAdd, HSub.hSub
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def colMate (j : Fin 6) : Fin 6 :=
…
```
def Usa2004P4.mate The pairing of the cells of the first two rows: the cell (0, j) is paired with (1, colMate j) and vice versa; all other cells are paired with themselves line 59 source
Source documentation
The pairing of the cells of the first two rows: the cell (0, j) is paired with (1, colMate j) and vice versa; all other cells are paired with themselves. Paired cells are in different rows and three columns apart, so they do not even share a vertex.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell
Proof uses: ite, Eq, Fin, OfNat.ofNat, Nat, Prod.fst, Prod.mk, Usa2004P4.colMate, Prod.snd
4 instances, coercions and auxiliary constants left out.
```
def mate (c : Cell) : Cell :=
…
```
Mentions: Usa2004P4.Cell
lemma Usa2004P4.colMate_colMate line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, Usa2004P4.colMate
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.colMate_dist line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, Nat.dist, Usa2004P4.colMate
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.mate_mate line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Eq, Usa2004P4.mate
Proof uses: of_decide_eq_true, Fin, OfNat.ofNat, Nat, id, Bool, Decidable.decide, Bool.true, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.mate_ne line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Ne, Usa2004P4.mate
Proof uses: of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.mate_val_le line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Usa2004P4.mate
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.mate_val_eq_of0 line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Eq, Nat, OfNat.ofNat, Prod.fst, Fin, Usa2004P4.mate
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.mate_val_eq_of1 line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Eq, Nat, OfNat.ofNat, Prod.fst, Fin, Usa2004P4.mate
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.mate_of_ge2 line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Eq, Usa2004P4.mate
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.mate_snd_dist line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Eq, Nat.dist, Prod.snd, Usa2004P4.mate
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.mate_fst_ne_iff line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Iff, Ne, Eq, Usa2004P4.mate
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.mate_fst_eq_iff line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Iff, Eq, Usa2004P4.mate
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.mate_fst_ne_self line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Ne, Usa2004P4.mate
Proof uses: of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.mate_inj line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Usa2004P4.Cell, Usa2004P4.mate
Proof uses: Eq, congrArg, Eq.mp, Usa2004P4.mate_mate

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Usa2004P4.Adj Two cells are adjacent if their squares share a vertex (Chebyshev distance at most 1) line 98 source
Source documentation
Two cells are adjacent if their squares share a vertex (Chebyshev distance at most 1).

no axioms what this means
Statement uses: Usa2004P4.Cell
Proof uses: And, LE.le, Nat, Nat.dist, OfNat.ofNat, Prod.fst, Fin, Prod.snd
3 instances, coercions and auxiliary constants left out.
```
def Adj (x y : Cell) : Prop := Nat.dist x.1.1 y.1.1 ≤ 1 ∧ Nat.dist x.2.1 y.2.1 ≤ 1
```
Mentions: Usa2004P4.Cell
def Usa2004P4.IsBlack A cell is black if it contains the greatest number in its row line 101 source
Source documentation
A cell is black if it contains the greatest number in its row.

no axioms what this means
Statement uses: Usa2004P4.Cell, Rat
Proof uses: Eq, Fin, OfNat.ofNat, Nat, Prod.fst, LE.le
2 instances, coercions and auxiliary constants left out.
```
def IsBlack (f : Cell → ℚ) (c : Cell) : Prop := ∀ d : Cell, d.1 = c.1 → f d ≤ f c
```
Mentions: f, Usa2004P4.Cell
def Usa2004P4.AliceWins Alice wins a finished board: there is a chain of black cells, consecutive cells sharing a vertex, from the top row to the bottom row line 105 source
Source documentation
Alice wins a finished board: there is a chain of black cells, consecutive cells sharing a vertex, from the top row to the bottom row.

no axioms what this means
Statement uses: Usa2004P4.Cell, Rat
Proof uses: Exists, And, Eq, Nat, OfNat.ofNat, Prod.fst, Fin, Usa2004P4.IsBlack, Relation.ReflTransGen, Usa2004P4.Adj
2 instances, coercions and auxiliary constants left out.
```
def AliceWins (f : Cell → ℚ) : Prop :=
…
```
Mentions: f, Usa2004P4.Cell
lemma Usa2004P4.IsBlack.unique The black cell of a row is unique (for an injective filling) line 112 source
Source documentation
The black cell of a row is unique (for an injective filling).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Rat, Function.Injective, Usa2004P4.IsBlack, Eq, Fin, OfNat.ofNat, Nat, Prod.fst
Proof uses: LE.le, Eq.symm, le_antisymm
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma IsBlack.unique {f : Cell → ℚ} (hinj : Function.Injective f) {x y : Cell}
    (hx : IsBlack f x) (hy : IsBlack f y) (h : x.1 = y.1) : x = y := by
…
```
Mentions: f, Usa2004P4.Cell, Usa2004P4.IsBlack, h
lemma Usa2004P4.exists_isBlack Every row has a black cell line 119 source
Source documentation
Every row has a black cell.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Rat, Fin, OfNat.ofNat, Nat, Exists, And, Eq, Prod.fst, Usa2004P4.IsBlack
Proof uses: Finset.Nonempty, Finset.filter, Finset.univ, Exists.intro, Membership.mem, Finset, Prod.mk, of_eq_true, Eq.trans, True, congr, congrArg, eq_self, and_self, LE.le, Finset.exists_max_image, And.intro, Eq.mp, congrFun', true_and
22 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma exists_isBlack (f : Cell → ℚ) (r : Fin 6) : ∃ c : Cell, c.1 = r ∧ IsBlack f c := by
…
```
Mentions: f, Usa2004P4.Cell, Usa2004P4.IsBlack
lemma Usa2004P4.not_aliceWins Documented declaration: not_aliceWins line 129 source
Source documentation
The key endgame lemma: if the black cell of row 1 is the mate of the black cell of row 0, then the two black cells are three columns apart, so no black chain can leave row 0, and Alice cannot win.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Rat, Function.Injective, Eq, Nat, OfNat.ofNat, Prod.fst, Fin, Usa2004P4.IsBlack, Usa2004P4.mate, Not, Usa2004P4.AliceWins
Proof uses: Exists, And, Relation.ReflTransGen, Usa2004P4.Adj, False, Relation.ReflTransGen.rec, LE.le, Nat.dist, And.left, Prod.snd, Eq.mp, congrArg, Nat.dist_zero_left, Or, Iff.mp, Nat.le_one_iff_eq_zero_or_eq_one, False.elim, Usa2004P4.mate_val_eq_of0, Fin.ext, Eq.mpr and 5 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma not_aliceWins (f : Cell → ℚ) (hinj : Function.Injective f)
    (c : Cell) (hc0 : c.1.1 = 0) (hc : IsBlack f c) (hm : IsBlack f (mate c)) :
    ¬ AliceWins f := by
…
```
Mentions: f, Usa2004P4.Cell, Usa2004P4.IsBlack, Usa2004P4.mate, Usa2004P4.AliceWins
lemma Usa2004P4.exists_fresh_rat_avoiding There is always a rational number outside any finite set line 165 source
Source documentation
There is always a rational number outside any finite set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Rat, Exists, Not, Membership.mem
Proof uses: Finset.exists_notMem
15 instances, coercions and auxiliary constants left out.
```
lemma exists_fresh_rat_avoiding (F : Finset ℚ) : ∃ w : ℚ, w ∉ F :=
…
```
lemma Usa2004P4.exists_rat_between_avoiding Documented declaration: exists_rat_between_avoiding line 171 source
Source documentation
Given finite sets L, U of rationals with everything in L smaller than everything in U, there is a rational number strictly between the two sets that moreover avoids a third finite set F.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Rat, Membership.mem, LT.lt, Exists, And, Not
Proof uses: Set, Set.Ioo, Set.Infinite.exists_notMem_finset, Set.Ioo_infinite, Exists.intro, And.intro, Eq, EmptyCollection.emptyCollection, Finset.Nonempty, Or, Finset.eq_empty_or_nonempty, Usa2004P4.exists_fresh_rat_avoiding, absurd, Eq.rec, Finset.notMem_empty, HSub.hSub, Finset.min', OfNat.ofNat, lt_of_not_ge, LE.le and 58 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma exists_rat_between_avoiding (L U F : Finset ℚ)
    (h : ∀ a ∈ L, ∀ b ∈ U, a < b) :
    ∃ w : ℚ, (∀ a ∈ L, a < w) ∧ (∀ b ∈ U, w < b) ∧ w ∉ F := by
…
```
Mentions: h
structure Usa2004P4.Play A play of the game: the sequence of 36 moves, each a cell together with the rational number written in it line 210 source
Source documentation
A play of the game: the sequence of 36 moves, each a cell together with the rational number written in it. Alice makes the moves 0, 2, ..., 34 and Bob the moves 1, 3, ..., 35. The legality conditions are that all cells played are distinct (a player must write in an empty square) and that all numbers played are distinct (a player must choose a rational not yet appearing in the grid).

no axioms what this means
```
structure Play where
…
```
def Usa2004P4.prefBoard The board after the first n moves of a play line 216 source
Source documentation
The board after the first n moves of a play.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Nat, Usa2004P4.Cell, Option, Rat
Proof uses: dite, Exists, Fin, OfNat.ofNat, And, LT.lt, Eq, Prod.fst, Usa2004P4.Play.moves, Option.some, Prod.snd, Exists.choose, Not, Option.none
8 instances, coercions and auxiliary constants left out.
```
noncomputable def prefBoard (p : Play) (n : ℕ) : Cell → Option ℚ :=
…
```
Mentions: Usa2004P4.Play, Usa2004P4.Cell
def Usa2004P4.finalBoard The final board of a play: after 36 moves every cell is filled (see prefBoard_finalBoard), and this is the number written in each cell line 223 source
Source documentation
The final board of a play: after 36 moves every cell is filled (see prefBoard_finalBoard), and this is the number written in each cell.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Usa2004P4.Cell, Rat
Proof uses: Option.getD, Usa2004P4.prefBoard, OfNat.ofNat, Nat
2 instances, coercions and auxiliary constants left out.
```
noncomputable def finalBoard (p : Play) : Cell → ℚ :=
…
```
Mentions: Usa2004P4.Play, Usa2004P4.Cell
def Usa2004P4.FollowsStrategy A play follows Bob's strategy σ if each of Bob's moves (the odd-numbered moves) is the move prescribed by σ on the current board line 228 source
Source documentation
A play follows Bob's strategy σ if each of Bob's moves (the odd-numbered moves) is the move prescribed by σ on the current board.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat, Prod, Usa2004P4.Play
Proof uses: Fin, OfNat.ofNat, Nat, Odd, Eq, Usa2004P4.Play.moves, Usa2004P4.prefBoard
3 instances, coercions and auxiliary constants left out.
```
def FollowsStrategy (σ : (Cell → Option ℚ) → Cell × ℚ) (p : Play) : Prop :=
…
```
Mentions: Usa2004P4.Cell, Usa2004P4.Play
lemma Usa2004P4.prefBoard_zero line 233 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Usa2004P4.Cell, Eq, Option, Rat, Usa2004P4.prefBoard, OfNat.ofNat, Nat, Option.none
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, dite_eq_right_of_eq_false, Exists, Fin, And, LT.lt, Prod.fst, Usa2004P4.Play.moves, Option.some, Prod.snd, Exists.choose, Not, False, funext, false_and, eq_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.prefBoard_eq_some line 236 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Nat, Usa2004P4.Cell, Rat, Iff, Eq, Option, Usa2004P4.prefBoard, Option.some, Exists, Fin, OfNat.ofNat, And, LT.lt, Prod, Usa2004P4.Play.moves, Prod.mk
Proof uses: id, dite, Prod.fst, Prod.snd, Exists.choose, Not, Option.none, Eq.mpr, congrArg, dite_eq_left, Iff.intro, Exists.intro, And.intro, And.left, Exists.choose_spec, Prod.ext, And.right, Option.some.inj, Usa2004P4.Play.cell_inj, of_eq_true and 7 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.prefBoard_eq_none line 254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Nat, Usa2004P4.Cell, Iff, Eq, Option, Rat, Usa2004P4.prefBoard, Option.none, Fin, OfNat.ofNat, LT.lt, Ne, Prod.fst, Usa2004P4.Play.moves
Proof uses: Iff.intro, Option.some, Prod.snd, Iff.mpr, Exists, And, Prod, Prod.mk, Usa2004P4.prefBoard_eq_some, Exists.intro, And.intro, Prod.ext, rfl, False, Eq.mp, congrArg, Eq.refl, Eq.symm, Iff.mp, absurd
11 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.prefBoard_succ line 269 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Nat, LT.lt, OfNat.ofNat, Eq, Usa2004P4.Cell, Option, Rat, Usa2004P4.prefBoard, HAdd.hAdd, Function.update, Fin, Prod.fst, Usa2004P4.Play.moves, Fin.mk, Option.some, Prod.snd
Proof uses: funext, dite, Eq.mpr, id, congrArg, Function.update_self, Iff.mpr, Exists, And, Prod, Prod.mk, Usa2004P4.prefBoard_eq_some, Exists.intro, And.intro, Nat.lt_succ_self, rfl, Eq.symm, Not, Function.update_of_ne, Option.none and 9 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.prefBoard_apply_self line 300 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Nat, LT.lt, OfNat.ofNat, Eq, Option, Rat, Usa2004P4.prefBoard, Prod.fst, Usa2004P4.Cell, Usa2004P4.Play.moves, Fin.mk, Option.none
Proof uses: Eq.mpr, Fin, Ne, id, congrArg, propext, Usa2004P4.prefBoard_eq_none, Usa2004P4.Play.cell_inj, Iff.mp, Fin.ext_iff
6 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.prefBoard_inj line 308 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Nat, Usa2004P4.Cell, Rat, Eq, Option, Usa2004P4.prefBoard, Option.some
Proof uses: Fin, OfNat.ofNat, And, LT.lt, Prod, Usa2004P4.Play.moves, Prod.mk, Exists, Iff.mp, Usa2004P4.prefBoard_eq_some, Prod.snd, Eq.mpr, id, congrArg, Eq.refl, Usa2004P4.Play.val_inj, Prod.fst, Eq.symm
5 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def Usa2004P4.filled The set of cells filled after the first n moves of a play line 320 source
Source documentation
The set of cells filled after the first n moves of a play.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Nat, LE.le, OfNat.ofNat, Finset, Usa2004P4.Cell
Proof uses: Finset.image, Fin, Prod.fst, Rat, Usa2004P4.Play.moves, Fin.castLE, Finset.univ
7 instances, coercions and auxiliary constants left out.
```
def filled (p : Play) (n : ℕ) (hn : n ≤ 36) : Finset Cell :=
…
```
Mentions: Usa2004P4.Play, Usa2004P4.Cell
lemma Usa2004P4.filled_cell_inj line 323 source
standard axioms: propext what this means
Statement uses: Usa2004P4.Play, Nat, LE.le, OfNat.ofNat, Function.Injective, Fin, Usa2004P4.Cell, Prod.fst, Rat, Usa2004P4.Play.moves, Fin.castLE
Proof uses: Eq, Usa2004P4.Play.cell_inj, Eq.mp, congrArg, propext, Fin.castLE_inj
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.card_filled line 329 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Nat, LE.le, OfNat.ofNat, Eq, Finset.card, Usa2004P4.Cell, Usa2004P4.filled
Proof uses: Eq.mpr, Finset.image, Fin, Prod.fst, Rat, Usa2004P4.Play.moves, Fin.castLE, Finset.univ, id, congrArg, Finset, Usa2004P4.filled.eq_1, Finset.card_image_of_injOn, Function.Injective.injOn, Usa2004P4.filled_cell_inj, Fintype.card, Finset.card_univ, Fintype.card_fin, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.mem_filled line 333 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Nat, LE.le, OfNat.ofNat, Usa2004P4.Cell, Iff, Membership.mem, Finset, Usa2004P4.filled, Ne, Option, Rat, Usa2004P4.prefBoard, Option.none
Proof uses: Iff.intro, Fin, And, Finset.univ, Eq, Prod.fst, Usa2004P4.Play.moves, Fin.castLE, Exists, Iff.mp, Finset.image, Finset.mem_image, Eq.mp, LT.lt, congrArg, propext, Usa2004P4.prefBoard_eq_none, Fin.isLt, absurd, Eq.symm and 14 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.prefBoard_36_isSome line 352 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Usa2004P4.Cell, Eq, Bool, Option.isSome, Rat, Usa2004P4.prefBoard, OfNat.ofNat, Nat, Bool.true
Proof uses: Function.Bijective, Fin, Prod.fst, Usa2004P4.Play.moves, Eq.mpr, And, Function.Injective, Fintype.card, id, congrArg, propext, Fintype.bijective_iff_injective_and_card, And.intro, Usa2004P4.Play.cell_inj, of_decide_eq_true, Decidable.decide, Eq.refl, Exists, And.right, Function.Surjective and 13 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.prefBoard_finalBoard line 360 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Usa2004P4.Cell, Eq, Option, Rat, Usa2004P4.prefBoard, OfNat.ofNat, Nat, Option.some, Usa2004P4.finalBoard
Proof uses: Exists, Iff.mp, Bool, Option.isSome, Bool.true, Option.isSome_iff_exists, Usa2004P4.prefBoard_36_isSome, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', Option.getD, eq_self
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.finalBoard_inj line 365 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Function.Injective, Usa2004P4.Cell, Rat, Usa2004P4.finalBoard
Proof uses: Eq, Option, Usa2004P4.prefBoard, OfNat.ofNat, Nat, Option.some, Eq.rec, Usa2004P4.prefBoard_finalBoard, Eq.symm, Usa2004P4.prefBoard_inj
1 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.even_card_of_mate_closed A set of cells of the first two rows closed under the pairing has even cardinality: it is a union of pairs {c, mate c} line 374 source
Source documentation
A set of cells of the first two rows closed under the pairing has even cardinality: it is a union of pairs {c, mate c}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa2004P4.Cell, Membership.mem, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Usa2004P4.mate, Even, Finset.card
Proof uses: Finset.filter, Eq, rfl, Union.union, Finset.image, Finset.ext, Eq.mpr, Iff, Or, And, Exists, id, congrArg, Eq.trans, congrFun', congr, funext, Iff.intro, Or.inl, And.intro and 20 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
lemma even_card_of_mate_closed (S : Finset Cell)
    (hsub : ∀ c ∈ S, c.1.1 ≤ 1)
    (hclosed : ∀ c ∈ S, mate c ∈ S) : Even S.card := by
…
```
Mentions: S, Usa2004P4.Cell, Usa2004P4.mate
lemma Usa2004P4.orderIso_update Updating two order-isomorphic functions at a fresh point with values occupying the same relative position preserves the order-isomorphism line 407 source
Source documentation
Updating two order-isomorphic functions at a fresh point with values occupying the same relative position preserves the order-isomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Rat, Set, Not, Membership.mem, Iff, LT.lt, And, Ne, Union.union, Singleton.singleton, Function.update
Proof uses: Eq.mpr, id, Eq, congrArg, Function.update_of_ne, ne_of_mem_of_not_mem, Function.update_self, Iff.intro, And.left, Decidable.byContradiction, lt_of_le_of_ne, Eq.mp, LE.le, propext, not_lt, Ne.symm, absurd, False, not_lt_of_gt, And.right and 1 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma orderIso_update {ι : Type*} [DecidableEq ι] (A B : ι → ℚ) (S : Set ι) (x : ι)
    (vx w : ℚ) (hx : x ∉ S)
    (hiso : ∀ c ∈ S, ∀ d ∈ S, (A c < A d ↔ B c < B d))
    (hnew : ∀ z ∈ S, (A z < vx → B z < w) ∧ (vx < A z → w < B z))
    (hA : ∀ z ∈ S, A z ≠ vx) :
    ∀ c ∈ S ∪ {x}, ∀ d ∈ S ∪ {x},
      (Function.update A x vx c < Function.update A x vx d ↔
       Function.update B x w c < Function.update B x w d) := by
…
```
Mentions: S
def Usa2004P4.Rows01Closed The board is closed under the pairing on the first two rows: a cell of the first two rows is filled iff its mate is filled line 447 source
Source documentation
The board is closed under the pairing on the first two rows: a cell of the first two rows is filled iff its mate is filled.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat
Proof uses: LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Iff, Eq, Option.none, Usa2004P4.mate
3 instances, coercions and auxiliary constants left out.
```
def Rows01Closed (b : Cell → Option ℚ) : Prop :=
…
```
Mentions: Usa2004P4.Cell
def Usa2004P4.SameRowIso The entries of each of the first two rows are ordered in the same way as the entries of the paired cells line 452 source
Source documentation
The entries of each of the first two rows are ordered in the same way as the entries of the paired cells.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat
Proof uses: Eq, Fin, OfNat.ofNat, Nat, Prod.fst, LE.le, Option.some, Usa2004P4.mate, Iff, LT.lt
4 instances, coercions and auxiliary constants left out.
```
def SameRowIso (b : Cell → Option ℚ) : Prop :=
…
```
Mentions: Usa2004P4.Cell
def Usa2004P4.Inv The invariant Bob maintains after each of his moves line 458 source
Source documentation
The invariant Bob maintains after each of his moves.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat
Proof uses: And, Usa2004P4.Rows01Closed, Usa2004P4.SameRowIso
```
def Inv (b : Cell → Option ℚ) : Prop := Rows01Closed b ∧ SameRowIso b
```
Mentions: Usa2004P4.Cell, Usa2004P4.Rows01Closed, Usa2004P4.SameRowIso
def Usa2004P4.GoodMateValue Documented declaration: GoodMateValue line 464 source
Source documentation
GoodMateValue b x vx w says that the number w is a legal and good answer for Bob in the mate of the cell x (which contains vx): it does not yet appear on the board, and it occupies the same position relative to the entries of the row of x as vx does relative to the entries of the paired cells.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat
Proof uses: And, Ne, Option.some, Eq, Fin, OfNat.ofNat, Nat, Prod.fst, Usa2004P4.mate, LT.lt
2 instances, coercions and auxiliary constants left out.
```
def GoodMateValue (b : Cell → Option ℚ) (x : Cell) (vx w : ℚ) : Prop :=
…
```
Mentions: Usa2004P4.Cell
lemma Usa2004P4.exists_GoodMateValue Documented declaration: exists_GoodMateValue line 472 source
Source documentation
A good value for Bob's answer exists: the constraints coming from entries below vx and those coming from entries above vx are consistent (by the order-isomorphism of the board before Alice's move), and ℚ is dense.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat, Usa2004P4.Inv, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Eq, Option.none, Function.update, Option.some, Exists, Usa2004P4.GoodMateValue
Proof uses: Eq.mpr, id, congrArg, rfl, Finset, Finset.image, Option.getD, Usa2004P4.mate, Finset.filter, And, Ne, LT.lt, Classical.propDecidable, Finset.univ, Membership.mem, Iff.mp, Finset.mem_image, Eq.mp, Finset.mem_filter, Function.update_of_ne and 16 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 92 steps
Open to load the checked before-and-after goal states.
```
lemma exists_GoodMateValue {b₀ b₁ : Cell → Option ℚ} (hinv : Inv b₀)
    {x : Cell} (hx01 : x.1.1 ≤ 1) (hx : b₀ x = none) {vx : ℚ}
    (hb₁ : b₁ = Function.update b₀ x (some vx)) :
    ∃ w, GoodMateValue b₁ x vx w := by
…
```
Mentions: Usa2004P4.Cell, Usa2004P4.Inv, Usa2004P4.GoodMateValue
def Usa2004P4.bobMateValue The number Bob writes in the mate of Alice's cell when he answers in the first two rows line 569 source
Source documentation
The number Bob writes in the mate of Alice's cell when he answers in the first two rows.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat
Proof uses: dite, Exists, Usa2004P4.GoodMateValue, Option.getD, OfNat.ofNat, Classical.propDecidable, Exists.choose, Not
1 instances, coercions and auxiliary constants left out.
```
noncomputable def bobMateValue (b : Cell → Option ℚ) (x : Cell) : ℚ :=
…
```
Mentions: Usa2004P4.Cell
def Usa2004P4.bobCell2 The cell Bob plays in when Alice plays in rows 3 to 6: some empty cell of rows 3 to 6 (one always exists at that point by a parity argument, see inv_prefBoard) line 574 source
Source documentation
The cell Bob plays in when Alice plays in rows 3 to 6: some empty cell of rows 3 to 6 (one always exists at that point by a parity argument, see inv_prefBoard).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat
Proof uses: dite, Exists, And, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Eq, Option.none, Exists.choose, Not, Prod.mk
11 instances, coercions and auxiliary constants left out.
```
noncomputable def bobCell2 (b : Cell → Option ℚ) : Cell :=
…
```
Mentions: Usa2004P4.Cell
def Usa2004P4.bobFreshValue A rational number not appearing on the board line 578 source
Source documentation
A rational number not appearing on the board.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat
Proof uses: Exists.choose, Not, Membership.mem, Finset, Finset.image, Option.getD, OfNat.ofNat, Finset.univ, Fin, Nat
8 instances, coercions and auxiliary constants left out.
```
noncomputable def bobFreshValue (b : Cell → Option ℚ) : ℚ :=
…
```
Mentions: Usa2004P4.Cell
lemma Usa2004P4.bobFreshValue_fresh line 581 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat, Ne, Option.some, Usa2004P4.bobFreshValue
Proof uses: Eq, Not, Membership.mem, Finset, Finset.image, Option.getD, OfNat.ofNat, Finset.univ, Fin, Nat, Exists.choose, Usa2004P4.exists_fresh_rat_avoiding, Exists.choose_spec, Iff.mpr, Exists, And, Finset.mem_image, Exists.intro, And.intro, Finset.mem_univ and 4 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def Usa2004P4.bobMove Documented declaration: bobMove line 593 source
Source documentation
Bob's strategy: if Alice just played in the first two rows, answer in the mate of her cell with a number preserving the order-isomorphism; otherwise play in any empty cell of rows 3 to 6 with a fresh number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat, Prod
Proof uses: dite, Exists, And, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Ne, Option.none, Eq, Usa2004P4.mate, Prod.mk, Exists.choose, Usa2004P4.bobMateValue, Not, Usa2004P4.bobCell2, Usa2004P4.bobFreshValue
10 instances, coercions and auxiliary constants left out.
```
noncomputable def bobMove (b : Cell → Option ℚ) : Cell × ℚ :=
…
```
Mentions: Usa2004P4.Cell
lemma Usa2004P4.bobMove_eq_mate line 598 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Ne, Option.none, Eq, Usa2004P4.mate, Prod, Usa2004P4.bobMove, Prod.mk, Usa2004P4.bobMateValue
Proof uses: Exists, And, Exists.intro, And.intro, id, Eq.mpr, dite, Exists.choose, Not, Usa2004P4.bobCell2, Usa2004P4.bobFreshValue, congrArg, dite_eq_left, And.left, Exists.choose_spec, And.right, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.bobMove_eq_rows2 line 610 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat, Not, Exists, And, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Ne, Option.none, Eq, Usa2004P4.mate, Prod, Usa2004P4.bobMove, Prod.mk, Usa2004P4.bobCell2, Usa2004P4.bobFreshValue
Proof uses: id, Eq.mpr, dite, Exists.choose, Usa2004P4.bobMateValue, congrArg, dite_eq_right, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.bobCell2_spec line 616 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat, Exists, And, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Eq, Option.none, Usa2004P4.bobCell2
Proof uses: id, Eq.mpr, dite, Exists.choose, Not, Prod.mk, congrArg, dite_eq_left, Exists.choose_spec
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.goodMateValue_bobMateValue line 623 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat, Eq, Option.some, Exists, Usa2004P4.GoodMateValue, Usa2004P4.bobMateValue
Proof uses: Option.getD, OfNat.ofNat, Eq.mpr, id, congrArg, Eq.refl, dite, Classical.propDecidable, Exists.choose, Not, dite_eq_left, Exists.choose_spec
1 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2004P4.inv_update_rows2 The invariant is preserved when Alice plays in rows 3 to 6 and Bob answers in rows 3 to 6 (the first two rows are untouched) line 633 source
Source documentation
The invariant is preserved when Alice plays in rows 3 to 6 and Bob answers in rows 3 to 6 (the first two rows are untouched).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat, Usa2004P4.Inv, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Eq, Function.update, Option.some
Proof uses: And, Ne, Usa2004P4.mate, Usa2004P4.mate_val_le, And.intro, False, Eq.mp, congrArg, Usa2004P4.Rows01Closed, Usa2004P4.SameRowIso, Iff, Option.none, Eq.mpr, id, Function.update_of_ne, And.left, LT.lt, Eq.symm, And.right
15 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma inv_update_rows2 {b₀ b₁ b₂ : Cell → Option ℚ} (hinv : Inv b₀)
    {x c₂ : Cell} (hx2 : 2 ≤ x.1.1) (hc₂2 : 2 ≤ c₂.1.1) {vx w₂ : ℚ}
    (hb₁ : b₁ = Function.update b₀ x (some vx))
    (hb₂ : b₂ = Function.update b₁ c₂ (some w₂)) :
    Inv b₂ := by
…
```
Mentions: Usa2004P4.Cell, Usa2004P4.Inv
lemma Usa2004P4.inv_update_mate The invariant is preserved when Alice plays in the first two rows and Bob answers in the mate of her cell with a good value line 663 source
Source documentation
The invariant is preserved when Alice plays in the first two rows and Bob answers in the mate of her cell with a good value.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Cell, Option, Rat, Usa2004P4.Inv, LE.le, Nat, OfNat.ofNat, Prod.fst, Fin, Eq, Option.none, Function.update, Option.some, Usa2004P4.mate, Usa2004P4.GoodMateValue
Proof uses: Ne, Ne.symm, Usa2004P4.mate_ne, Iff.mp, And.left, Usa2004P4.Rows01Closed, Usa2004P4.SameRowIso, And.intro, dite, Iff, Eq.mpr, id, congrArg, Function.update_of_ne, Function.update_self, iff_of_false, Option.some_ne_none, Not, Usa2004P4.mate_mate, Eq.symm and 35 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 288 steps (first 200 of 288)
Open to load the checked before-and-after goal states.
```
lemma inv_update_mate {b₀ b₁ b₂ : Cell → Option ℚ} (hinv : Inv b₀)
    {x : Cell} (hx01 : x.1.1 ≤ 1) (hx : b₀ x = none) {vx w : ℚ}
    (hb₁ : b₁ = Function.update b₀ x (some vx))
    (hb₂ : b₂ = Function.update b₁ (mate x) (some w))
    (hinj : ∀ c d : Cell, ∀ v : ℚ, b₁ c = some v → b₁ d = some v → c = d)
    (hw : GoodMateValue b₁ x vx w) :
    Inv b₂ := by
…
```
Mentions: Usa2004P4.Cell, Usa2004P4.Inv, Usa2004P4.mate, Usa2004P4.GoodMateValue
lemma Usa2004P4.inv_prefBoard Bob's invariant holds after each of his moves in every play that follows his strategy line 956 source
Source documentation
Bob's invariant holds after each of his moves in every play that follows his strategy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2004P4.Play, Usa2004P4.FollowsStrategy, Usa2004P4.bobMove, Nat, LE.le, OfNat.ofNat, Usa2004P4.Inv, Usa2004P4.prefBoard, HMul.hMul
Proof uses: Nat.recAux, And.intro, Usa2004P4.Rows01Closed, Usa2004P4.SameRowIso, Usa2004P4.Cell, Prod.fst, Fin, Eq.mpr, Iff, Eq, Option, Rat, Option.none, Usa2004P4.mate, id, congrArg, Usa2004P4.prefBoard_zero, Iff.rfl, Option.some, LT.lt and 87 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 179 steps
Open to load the checked before-and-after goal states.
```
lemma inv_prefBoard (p : Play) (hp : FollowsStrategy bobMove p) :
    ∀ m : ℕ, m ≤ 18 → Inv (prefBoard p (2 * m)) := by
…
```
Mentions: Usa2004P4.Play, Usa2004P4.FollowsStrategy, Usa2004P4.bobMove, Usa2004P4.Inv, Usa2004P4.prefBoard
problem Usa2004P4.usa2004_p4 USAMO 2004, Problem 4 line 1137 source
Source documentation
USAMO 2004, Problem 4. Bob (the second player) has a winning strategy: whenever the play follows Bob's strategy σ of answering a move in the first two rows by a suitable number in the paired cell (and playing anywhere in rows 3 to 6 otherwise), the final board has no black path from the top row to the bottom row, so Alice cannot win.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Usa2004P4.Cell, Option, Rat, Prod, Usa2004P4.Play, Usa2004P4.FollowsStrategy, Not, Usa2004P4.AliceWins, Usa2004P4.finalBoard
Proof uses: Exists.intro, Usa2004P4.bobMove, Usa2004P4.Inv, Usa2004P4.prefBoard, HMul.hMul, Nat, OfNat.ofNat, Usa2004P4.inv_prefBoard, le_rfl, Function.Injective, Usa2004P4.finalBoard_inj, And, Eq, Fin, Prod.fst, Usa2004P4.IsBlack, Usa2004P4.exists_isBlack, congrArg, Usa2004P4.mate, Usa2004P4.mate_val_eq_of0 and 21 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
problem usa2004_p4 :
    ∃ σ : (Cell → Option ℚ) → Cell × ℚ,
      ∀ p : Play, FollowsStrategy σ p → ¬ AliceWins (finalBoard p) := by
…
```
Mentions: Usa2004P4.Cell, Usa2004P4.Play, Usa2004P4.FollowsStrategy, Usa2004P4.AliceWins, Usa2004P4.finalBoard