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

55 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1999, Problem 5

The Y2K Game is played on a 1 × 2000 grid as follows. Two players in turn write either an S or an O in an empty square. The first player who produces three consecutive boxes that spell SOS wins. If all boxes are filled without producing SOS then the game is a draw. Show that the second player has a winning strategy.

Imports (5)

Imported by 1 file

Compfiles.lean

inductive Usa1999P5.Piece The two letters that can be written in a square line 35 source
Source documentation
The two letters that can be written in a square.

no axioms what this means

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
inductive Piece | S | O
  deriving DecidableEq, Inhabited
```
Mentions: S
instance Usa1999P5.(instance at line 38) line 38 source
abbrev Usa1999P5.Board The board: square i contains b i for i < 2000; anything outside is irrelevant line 43 source
Source documentation
The board: square i contains b i for i < 2000; anything outside is irrelevant.

no axioms what this means
Proof uses: Nat, Option, Usa1999P5.Piece
```
abbrev Board := ℕ → Option Piece
```
Mentions: Usa1999P5.Piece
def Usa1999P5.BOK Well-formed board: nothing written outside the 2000 squares line 46 source
Source documentation
Well-formed board: nothing written outside the 2000 squares.

no axioms what this means
Statement uses: Usa1999P5.Board
Proof uses: Nat, LE.le, OfNat.ofNat, Eq, Option, Usa1999P5.Piece, Option.none
2 instances, coercions and auxiliary constants left out.
```
def BOK (b : Board) : Prop := ∀ i, 2000 ≤ i → b i = none
```
Mentions: Usa1999P5.Board
def Usa1999P5.HasSOS The board contains three consecutive squares spelling S O S line 49 source
Source documentation
The board contains three consecutive squares spelling S O S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board
Proof uses: Exists, Nat, And, Membership.mem, Finset, Finset.range, OfNat.ofNat, Eq, Option, Usa1999P5.Piece, Option.some, Usa1999P5.Piece.S, HAdd.hAdd, Usa1999P5.Piece.O
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def HasSOS (b : Board) : Prop :=
…
```
Mentions: Usa1999P5.Board
instance Usa1999P5.(instance at line 53) line 53 source
def Usa1999P5.HasThreat The player to move can win immediately: some legal move produces SOS line 57 source
Source documentation
The player to move can win immediately: some legal move produces SOS.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board
Proof uses: Exists, Nat, And, Membership.mem, Finset, Finset.range, OfNat.ofNat, Usa1999P5.Piece, Eq, Option, Option.none, Usa1999P5.HasSOS, Function.update, Option.some
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def HasThreat (b : Board) : Prop :=
…
```
Mentions: Usa1999P5.Board
instance Usa1999P5.(instance at line 61) line 61 source
def Usa1999P5.ThreatFree No immediate winning move is available line 65 source
Source documentation
No immediate winning move is available.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board
Proof uses: Not, Usa1999P5.HasThreat
```
def ThreatFree (b : Board) : Prop := ¬ HasThreat b
```
Mentions: Usa1999P5.Board, Usa1999P5.HasThreat
def Usa1999P5.IsLosing A losing square: an empty square such that playing either letter there allows the opponent to win on the following move line 69 source
Source documentation
A losing square: an empty square such that playing either letter there allows the opponent to win on the following move.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Nat
Proof uses: And, Eq, Option, Usa1999P5.Piece, Option.none, Usa1999P5.HasThreat, Function.update, Option.some
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def IsLosing (b : Board) (x : ℕ) : Prop :=
…
```
Mentions: Usa1999P5.Board
instance Usa1999P5.(instance at line 72) line 72 source
def Usa1999P5.TrapAt A "trap": the pattern S _ _ S with both middle squares empty line 77 source
Source documentation
A "trap": the pattern S _ _ S with both middle squares empty. Its two middle squares will turn out to be exactly the losing squares.

no axioms what this means
Statement uses: Usa1999P5.Board, Nat
Proof uses: And, Eq, Option, Usa1999P5.Piece, Option.some, Usa1999P5.Piece.S, HAdd.hAdd, OfNat.ofNat, Option.none
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def TrapAt (b : Board) (a : ℕ) : Prop :=
…
```
Mentions: Usa1999P5.Board
instance Usa1999P5.(instance at line 80) line 80 source
def Usa1999P5.HasTrap The board contains a trap line 84 source
Source documentation
The board contains a trap.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board
Proof uses: Exists, Nat, And, Membership.mem, Finset, Finset.range, OfNat.ofNat, Usa1999P5.TrapAt
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def HasTrap (b : Board) : Prop := ∃ a ∈ Finset.range 1997, TrapAt b a
```
Mentions: Usa1999P5.Board, Usa1999P5.TrapAt
instance Usa1999P5.(instance at line 86) line 86 source
def Usa1999P5.empties The empty squares of the board line 90 source
Source documentation
The empty squares of the board.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Finset, Nat
Proof uses: Finset.filter, Eq, Option, Usa1999P5.Piece, Option.none, Finset.range, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
```
def empties (b : Board) : Finset ℕ := (Finset.range 2000).filter fun i => b i = none
```
Mentions: Usa1999P5.Board
def Usa1999P5.letters The occupied squares of the board line 93 source
Source documentation
The occupied squares of the board.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Finset, Nat
Proof uses: Finset.filter, Ne, Option, Usa1999P5.Piece, Option.none, Eq, Finset.range, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
def letters (b : Board) : Finset ℕ := (Finset.range 2000).filter fun i => b i ≠ none
```
Mentions: Usa1999P5.Board
def Usa1999P5.losing The losing squares of the board line 96 source
Source documentation
The losing squares of the board.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Finset, Nat
Proof uses: Finset.filter, Usa1999P5.IsLosing, Finset.range, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
```
def losing (b : Board) : Finset ℕ := (Finset.range 2000).filter fun i => IsLosing b i
```
Mentions: Usa1999P5.Board, Usa1999P5.IsLosing
def Usa1999P5.trapEnds The left ends of traps on the board line 99 source
Source documentation
The left ends of traps on the board.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Finset, Nat
Proof uses: Finset.filter, Usa1999P5.TrapAt, Finset.range, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
```
def trapEnds (b : Board) : Finset ℕ := (Finset.range 1997).filter fun a => TrapAt b a
```
Mentions: Usa1999P5.Board, Usa1999P5.TrapAt
inductive Usa1999P5.Outcome The outcome of a game: first player wins, second player wins, or draw line 102 source
Source documentation
The outcome of a game: first player wins, second player wins, or draw.

no axioms what this means
```
inductive Outcome | p1 | p2 | draw
  deriving DecidableEq

/-- A strategy chooses a square and a letter given a board. -/
```
abbrev Usa1999P5.Strategy A strategy chooses a square and a letter given a board line 106 source
Source documentation
A strategy chooses a square and a letter given a board.

no axioms what this means
Proof uses: Usa1999P5.Board, Prod, Nat, Usa1999P5.Piece
```
abbrev Strategy := Board → ℕ × Piece
```
Mentions: Usa1999P5.Board, Usa1999P5.Piece
def Usa1999P5.play Playing out the game with two strategies; fuel bounds the number of moves (2001 always suffices) line 111 source
Source documentation
Playing out the game with two strategies; fuel bounds the number of moves (2001 always suffices). true means it is the first player's turn. An illegal move (off the board or onto an occupied square) loses immediately.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa1999P5.Strategy, Usa1999P5.Board, Bool, Usa1999P5.Outcome
2 instances, coercions and auxiliary constants left out.
```
def play : ℕ → Strategy → Strategy → Board → Bool → Outcome
  | 0, _, _, _, _ => .draw
  | fuel + 1, σ₁, σ₂, b, true =>
      if HasSOS b then .p2
      else if empties b = ∅ then .draw
      else if (σ₁ b).1 < 2000 ∧ b (σ₁ b).1 = none
      then play fuel σ₁ σ₂ (Function.update b (σ₁ b).1 (some (σ₁ b).2)) false
      else .p2
  | fuel + 1, σ₁, σ₂, b, false =>
      if HasSOS b then .p1
      else if empties b = ∅ then .draw
      else if (σ₂ b).1 < 2000 ∧ b (σ₂ b).1 = none
…
```
Mentions: Usa1999P5.Strategy, Usa1999P5.Board, Usa1999P5.Outcome, Usa1999P5.HasSOS, Usa1999P5.empties
lemma Usa1999P5.mem_empties line 128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Nat, Iff, Membership.mem, Finset, Usa1999P5.empties, And, LT.lt, OfNat.ofNat, Eq, Option, Usa1999P5.Piece, Option.none
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.filter, Finset.range, iff_self
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1999P5.mem_letters line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Nat, Iff, Membership.mem, Finset, Usa1999P5.letters, And, LT.lt, OfNat.ofNat, Ne, Option, Usa1999P5.Piece, Option.none
Proof uses: of_eq_true, Not, Eq, Eq.trans, True, congrFun', congrArg, Finset.range, Finset.filter, Finset.filter_congr, Iff.of_eq, Eq.refl, iff_self
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1999P5.letters_update_card line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Nat, LT.lt, OfNat.ofNat, Eq, Option, Usa1999P5.Piece, Option.none, Finset.card, Usa1999P5.letters, Function.update, Option.some, HAdd.hAdd
Proof uses: Finset, Insert.insert, Finset.ext, Eq.mpr, Iff, Membership.mem, And, Ne, Or, id, congr, congrArg, Eq.trans, Finset.filter, Finset.range, congrFun', dite, of_eq_true, True, eq_true and 22 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Usa1999P5.empties_update_card line 146 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Nat, LT.lt, OfNat.ofNat, Eq, Option, Usa1999P5.Piece, Option.none, Finset.card, Usa1999P5.empties, Function.update, Option.some, HSub.hSub
Proof uses: Finset, Finset.erase, Finset.ext, Eq.mpr, Iff, Membership.mem, And, Ne, id, congr, congrArg, Eq.trans, Finset.filter, Finset.range, congrFun', dite, of_eq_true, False, True, Function.update_self and 19 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Usa1999P5.empties_ne_empty line 157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Ne, Nat, Finset.card, Usa1999P5.empties, OfNat.ofNat, Finset, EmptyCollection.emptyCollection
Proof uses: Eq, False.elim, False, Eq.mp, Eq.trans, Not, True, congrArg, eq_self, not_true_eq_false
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1999P5.empties_card_pos line 160 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Ne, Finset, Nat, Usa1999P5.empties, EmptyCollection.emptyCollection, LT.lt, OfNat.ofNat, Finset.card
Proof uses: Iff.mpr, Finset.Nonempty, Finset.card_pos, Finset.nonempty_of_ne_empty
6 instances, coercions and auxiliary constants left out.
lemma Usa1999P5.three_le_card_letters_of_hasSOS A board with SOS has at least three occupied squares line 164 source
Source documentation
A board with SOS has at least three occupied squares.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.HasSOS, LE.le, Nat, OfNat.ofNat, Finset.card, Usa1999P5.letters
Proof uses: And, Membership.mem, Finset, Finset.range, Eq, Option, Usa1999P5.Piece, Option.some, Usa1999P5.Piece.S, HAdd.hAdd, Usa1999P5.Piece.O, Iff.mpr, LT.lt, Ne, Option.none, Usa1999P5.mem_letters, And.intro, Eq.mp, congrArg, propext and 21 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma three_le_card_letters_of_hasSOS {b : Board} (h : HasSOS b) : 3 ≤ (letters b).card := by
…
```
Mentions: Usa1999P5.Board, h, Usa1999P5.HasSOS, Usa1999P5.letters
lemma Usa1999P5.two_le_card_letters_of_hasTrap A board with a trap has at least two occupied squares line 180 source
Source documentation
A board with a trap has at least two occupied squares.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.HasTrap, LE.le, Nat, OfNat.ofNat, Finset.card, Usa1999P5.letters
Proof uses: And, Membership.mem, Finset, Finset.range, Usa1999P5.TrapAt, Eq, Option, Usa1999P5.Piece, Option.some, Usa1999P5.Piece.S, HAdd.hAdd, Option.none, Iff.mpr, LT.lt, Ne, Usa1999P5.mem_letters, And.intro, Eq.mp, congrArg, propext and 19 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma two_le_card_letters_of_hasTrap {b : Board} (h : HasTrap b) : 2 ≤ (letters b).card := by
…
```
Mentions: Usa1999P5.Board, h, Usa1999P5.HasTrap, Usa1999P5.letters
lemma Usa1999P5.not_hasSOS_update_of_threatFree On a threat-free board, no move can produce SOS (else that move would have won) line 194 source
Source documentation
On a threat-free board, no move can produce SOS (else that move would have won).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.ThreatFree, Nat, LT.lt, OfNat.ofNat, Eq, Option, Usa1999P5.Piece, Option.none, Not, Usa1999P5.HasSOS, Function.update, Option.some
Proof uses: Exists.intro, And, Membership.mem, Finset, Finset.range, Exists, And.intro, Iff.mpr, Finset.mem_range
8 instances, coercions and auxiliary constants left out.
```
lemma not_hasSOS_update_of_threatFree {b : Board} (hTF : ThreatFree b) {x : ℕ}
    (hx : x < 2000) (hxe : b x = none) (l : Piece) :
    ¬ HasSOS (Function.update b x (some l)) :=
…
```
Mentions: Usa1999P5.Board, Usa1999P5.ThreatFree, Usa1999P5.Piece, Usa1999P5.HasSOS
lemma Usa1999P5.bOK_update line 199 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.BOK, Nat, LT.lt, OfNat.ofNat, Usa1999P5.Piece, Function.update, Option, Option.some
Proof uses: LE.le, Ne, Eq.mpr, Eq, Option.none, id, congrArg, Function.update_of_ne
8 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa1999P5.threat_shapes The shape of any immediate win created by playing letter l₀ at square x of a threat-free board line 209 source
Source documentation
The shape of any immediate win created by playing letter l₀ at square x of a threat-free board. The six alternatives correspond to the opponent's possible winning replies; the first two are the replies to an O, the other four to an S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.ThreatFree, Nat, LT.lt, OfNat.ofNat, Eq, Option, Usa1999P5.Piece, Option.none, Usa1999P5.HasThreat, Function.update, Option.some, Or, And, Usa1999P5.Piece.O, LE.le, HSub.hSub, HAdd.hAdd, Usa1999P5.Piece.S
Proof uses: Membership.mem, Finset, Finset.range, Exists, Usa1999P5.HasSOS, Decidable.byContradiction, Not, Ne, False, Eq.mp, Eq.trans, congrArg, Usa1999P5.not_hasSOS_update_of_threatFree, Exists.intro, And.intro, Iff.mpr, Finset.mem_range, propext, Function.update_of_ne, Option.some.inj and 14 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 254 steps (first 200 of 254)
Open to load the checked before-and-after goal states.
```
lemma threat_shapes {b : Board} (hTF : ThreatFree b) {x : ℕ}
    (hx : x < 2000) (hxe : b x = none) {l₀ : Piece}
    (h : HasThreat (Function.update b x (some l₀))) :
    (l₀ = Piece.O ∧ 1 ≤ x ∧ b (x - 1) = none ∧ b (x + 1) = some Piece.S) ∨
    (l₀ = Piece.O ∧ 1 ≤ x ∧ b (x + 1) = none ∧ b (x - 1) = some Piece.S) ∨
    (l₀ = Piece.S ∧ b (x + 2) = some Piece.S ∧ b (x + 1) = none) ∨
    (l₀ = Piece.S ∧ 2 ≤ x ∧ b (x - 2) = some Piece.S ∧ b (x - 1) = none) ∨
    (l₀ = Piece.S ∧ 2 ≤ x ∧ b (x - 1) = some Piece.O ∧ b (x - 2) = none) ∨
    (l₀ = Piece.S ∧ b (x + 1) = some Piece.O ∧ b (x + 2) = none) := by
…
```
Mentions: Usa1999P5.Board, Usa1999P5.ThreatFree, Usa1999P5.Piece, h, Usa1999P5.HasThreat
lemma Usa1999P5.trap_middle The middle squares of a trap are losing squares line 420 source
Source documentation
The middle squares of a trap are losing squares.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Nat, LT.lt, OfNat.ofNat, Usa1999P5.TrapAt, And, Usa1999P5.IsLosing, HAdd.hAdd
Proof uses: Eq, Option, Usa1999P5.Piece, Option.some, Usa1999P5.Piece.S, Option.none, And.intro, Usa1999P5.HasThreat, Function.update, Exists.intro, Membership.mem, Finset, Finset.range, Exists, Usa1999P5.HasSOS, Iff.mpr, Finset.mem_range, Usa1999P5.Piece.O, Eq.mpr, id and 5 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 84 steps
Open to load the checked before-and-after goal states.
```
lemma trap_middle {b : Board} {a : ℕ} (ha : a < 1997) (h : TrapAt b a) :
    IsLosing b (a + 1) ∧ IsLosing b (a + 2) := by
…
```
Mentions: Usa1999P5.Board, h, Usa1999P5.TrapAt, Usa1999P5.IsLosing
lemma Usa1999P5.losing_char A losing square of a threat-free board is the middle of a trap line 470 source
Source documentation
A losing square of a threat-free board is the middle of a trap.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.BOK, Usa1999P5.ThreatFree, Nat, LT.lt, OfNat.ofNat, Usa1999P5.IsLosing, Or, And, LE.le, Usa1999P5.TrapAt, HSub.hSub
Proof uses: Eq, Option, Usa1999P5.Piece, Option.none, Usa1999P5.HasThreat, Function.update, Option.some, Usa1999P5.Piece.O, HAdd.hAdd, Usa1999P5.Piece.S, Usa1999P5.threat_shapes, Or.inl, And.right, Or.inr, absurd, And.left, of_eq_true, Not, Eq.trans, False and 14 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 94 steps
Open to load the checked before-and-after goal states.
```
lemma losing_char {b : Board} (hBOK : BOK b) (hTF : ThreatFree b) {x : ℕ}
    (hx : x < 2000) (hL : IsLosing b x) :
    (2 ≤ x ∧ x ≤ 1998 ∧ TrapAt b (x - 2)) ∨ (1 ≤ x ∧ x ≤ 1997 ∧ TrapAt b (x - 1)) := by
…
```
Mentions: Usa1999P5.Board, Usa1999P5.BOK, Usa1999P5.ThreatFree, Usa1999P5.IsLosing, Usa1999P5.TrapAt
lemma Usa1999P5.trap_disjoint Middle pairs of distinct traps are disjoint line 531 source
Source documentation
Middle pairs of distinct traps are disjoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Nat, Usa1999P5.TrapAt, Ne, Disjoint, Finset, Insert.insert, HAdd.hAdd, OfNat.ofNat, Singleton.singleton
Proof uses: Eq.mpr, Membership.mem, Not, id, Eq, congrArg, propext, Finset.disjoint_left, Option, Usa1999P5.Piece, Option.some, Usa1999P5.Piece.S, And, Option.none, False, Or, Eq.mp, Eq.trans, False.elim, eq_false' and 3 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma trap_disjoint {b : Board} {a c : ℕ}
    (haT : TrapAt b a) (hcT : TrapAt b c) (hne : a ≠ c) :
    Disjoint ({a + 1, a + 2} : Finset ℕ) {c + 1, c + 2} := by
…
```
Mentions: Usa1999P5.Board, Usa1999P5.TrapAt
lemma Usa1999P5.mem_losing line 547 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Nat, Iff, Membership.mem, Finset, Usa1999P5.losing, And, LT.lt, OfNat.ofNat, Usa1999P5.IsLosing
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.filter, Finset.range, iff_self
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1999P5.mem_trapEnds line 550 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Nat, Iff, Membership.mem, Finset, Usa1999P5.trapEnds, And, LT.lt, OfNat.ofNat, Usa1999P5.TrapAt
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.filter, Finset.range, iff_self
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1999P5.losing_eq_biUnion The losing squares are exactly the middle squares of the traps line 554 source
Source documentation
The losing squares are exactly the middle squares of the traps.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.BOK, Usa1999P5.ThreatFree, Eq, Finset, Nat, Usa1999P5.losing, Finset.biUnion, Usa1999P5.trapEnds, Insert.insert, HAdd.hAdd, OfNat.ofNat, Singleton.singleton
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, LT.lt, Usa1999P5.IsLosing, Exists, Usa1999P5.TrapAt, Or, id, congr, congrArg, Eq.trans, funext, Iff.intro, LE.le, HSub.hSub, Usa1999P5.losing_char, Exists.intro and 5 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma losing_eq_biUnion {b : Board} (hBOK : BOK b) (hTF : ThreatFree b) :
    losing b = (trapEnds b).biUnion fun a => {a + 1, a + 2} := by
…
```
Mentions: Usa1999P5.Board, Usa1999P5.BOK, Usa1999P5.ThreatFree, Usa1999P5.losing, Usa1999P5.trapEnds
lemma Usa1999P5.even_card_losing Losing squares come in pairs, hence there is an even number of them line 571 source
Source documentation
Losing squares come in pairs, hence there is an even number of them.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.BOK, Usa1999P5.ThreatFree, Even, Nat, Finset.card, Usa1999P5.losing
Proof uses: Eq.mpr, Finset.biUnion, Usa1999P5.trapEnds, Insert.insert, Finset, HAdd.hAdd, OfNat.ofNat, Singleton.singleton, id, Eq, congrArg, Usa1999P5.losing_eq_biUnion, Finset.sum, Finset.card_biUnion, Membership.mem, Set, Ne, Function.onFun, Disjoint, Usa1999P5.trap_disjoint and 27 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma even_card_losing {b : Board} (hBOK : BOK b) (hTF : ThreatFree b) :
    Even (losing b).card := by
…
```
Mentions: Usa1999P5.Board, Usa1999P5.BOK, Usa1999P5.ThreatFree, Usa1999P5.losing
def Usa1999P5.SafeMove A safe move: a legal move that is not on a losing square and that creates neither SOS nor an immediate winning opportunity for the opponent line 586 source
Source documentation
A safe move: a legal move that is not on a losing square and that creates neither SOS nor an immediate winning opportunity for the opponent.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Nat, Usa1999P5.Piece
Proof uses: And, LT.lt, OfNat.ofNat, Eq, Option, Option.none, Not, Usa1999P5.IsLosing, Usa1999P5.HasThreat, Function.update, Option.some, Usa1999P5.HasSOS
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def SafeMove (b : Board) (x : ℕ) (l : Piece) : Prop :=
…
```
Mentions: Usa1999P5.Board, Usa1999P5.Piece
instance Usa1999P5.(instance at line 590) line 590 source
lemma Usa1999P5.exists_safe_move Documented declaration: exists_safe_move line 596 source
Source documentation
On a threat-free board with an odd number of empty squares, a safe move always exists: there are evenly many losing squares, so some empty square is not losing (this is the heart of the pairing argument).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.BOK, Usa1999P5.ThreatFree, Odd, Nat, Finset.card, Usa1999P5.empties, Exists, And, Membership.mem, Finset, Finset.range, OfNat.ofNat, Usa1999P5.Piece, Usa1999P5.SafeMove
Proof uses: LE.le, Usa1999P5.losing, Iff.mpr, LT.lt, Eq, Option, Option.none, Usa1999P5.mem_empties, And.intro, And.left, Usa1999P5.IsLosing, Eq.mp, congrArg, propext, Usa1999P5.mem_losing, Usa1999P5.HasThreat, Function.update, Option.some, And.right, Finset.card_le_card and 12 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma exists_safe_move {b : Board} (hBOK : BOK b) (hTF : ThreatFree b)
    (hodd : Odd (empties b).card) :
    ∃ x ∈ Finset.range 2000, ∃ l : Piece, SafeMove b x l := by
…
```
Mentions: Usa1999P5.Board, Usa1999P5.BOK, Usa1999P5.ThreatFree, Usa1999P5.empties, Usa1999P5.Piece, Usa1999P5.SafeMove
def Usa1999P5.SecondSetupOk A good second setup move: playing an S at t creates a trap without giving the opponent an immediate win line 620 source
Source documentation
A good second setup move: playing an S at t creates a trap without giving the opponent an immediate win.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Nat
Proof uses: And, Eq, Option, Usa1999P5.Piece, Option.none, Not, Usa1999P5.HasThreat, Function.update, Option.some, Usa1999P5.Piece.S, Usa1999P5.HasSOS, Usa1999P5.HasTrap
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def SecondSetupOk (b : Board) (t : ℕ) : Prop :=
…
```
Mentions: Usa1999P5.Board
instance Usa1999P5.(instance at line 625) line 625 source
def Usa1999P5.p2strat The second player's strategy line 629 source
Source documentation
The second player's strategy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Strategy
Proof uses: Usa1999P5.Board, dite, Prod, Nat, Usa1999P5.Piece, Usa1999P5.HasThreat, Prod.mk, Classical.choose, And, Membership.mem, Finset, Finset.range, OfNat.ofNat, Exists, Eq, Option, Option.none, Usa1999P5.HasSOS, Function.update, Option.some and 10 more
17 instances, coercions and auxiliary constants left out.
```
noncomputable def p2strat : Strategy := fun b =>
…
```
Mentions: Usa1999P5.Strategy
lemma Usa1999P5.p2strat_threat line 646 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.HasThreat, Exists, Nat, Usa1999P5.Piece, And, Eq, Prod.fst, Usa1999P5.p2strat, Prod.snd, LT.lt, OfNat.ofNat, Option, Option.none, Usa1999P5.HasSOS, Function.update, Option.some
Proof uses: id, Eq.mpr, dite, Prod, Prod.mk, Classical.choose, Membership.mem, Finset, Finset.range, Not, Usa1999P5.HasTrap, Usa1999P5.SafeMove, Usa1999P5.Piece.S, Finset.card, Usa1999P5.letters, ite, Singleton.singleton, Usa1999P5.SecondSetupOk, congrArg, dite_eq_left and 9 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa1999P5.p2strat_safe line 657 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.ThreatFree, Usa1999P5.HasTrap, Exists, Nat, And, Membership.mem, Finset, Finset.range, OfNat.ofNat, Usa1999P5.Piece, Usa1999P5.SafeMove, Eq, Prod.fst, Usa1999P5.p2strat, Prod.snd
Proof uses: id, Eq.mpr, dite, Prod, Usa1999P5.HasThreat, Prod.mk, Classical.choose, Option, Option.none, Usa1999P5.HasSOS, Function.update, Option.some, Not, Usa1999P5.Piece.S, Finset.card, Usa1999P5.letters, ite, LT.lt, Singleton.singleton, Usa1999P5.SecondSetupOk and 8 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa1999P5.p2strat_setup1 line 666 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.ThreatFree, Not, Usa1999P5.HasTrap, Eq, Nat, Finset.card, Usa1999P5.letters, OfNat.ofNat, Exists, And, Finset, Singleton.singleton, Prod.fst, Usa1999P5.Piece, Usa1999P5.p2strat, ite, LT.lt, Prod.snd, Usa1999P5.Piece.S
Proof uses: id, Eq.mpr, dite, Prod, Usa1999P5.HasThreat, Prod.mk, Classical.choose, Membership.mem, Finset.range, Option, Option.none, Usa1999P5.HasSOS, Function.update, Option.some, Usa1999P5.SafeMove, Usa1999P5.SecondSetupOk, congrArg, dite_eq_right, dite_eq_left, Exists.intro and 5 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1999P5.p2strat_setup2 line 674 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.ThreatFree, Not, Usa1999P5.HasTrap, Ne, Nat, Finset.card, Usa1999P5.letters, OfNat.ofNat, Exists, And, Membership.mem, Finset, Finset.range, Usa1999P5.SecondSetupOk, Eq, Prod.fst, Usa1999P5.Piece, Usa1999P5.p2strat, Prod.snd and 2 more
Proof uses: id, Eq.mpr, dite, Prod, Usa1999P5.HasThreat, Prod.mk, Classical.choose, Option, Option.none, Usa1999P5.HasSOS, Function.update, Option.some, Usa1999P5.SafeMove, ite, Singleton.singleton, congrArg, dite_eq_right, dite_eq_left, Exists.intro, And.intro 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.
def Usa1999P5.Inv Documented declaration: Inv line 687 source
Source documentation
The invariant maintained after each move of the second player: a threat-free board with a trap and no SOS, with the right parity of empty squares (t = true: first player to move).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Bool
Proof uses: And, Usa1999P5.BOK, Usa1999P5.ThreatFree, Not, Usa1999P5.HasSOS, Usa1999P5.HasTrap, ite, Eq, Bool.true, Even, Nat, Finset.card, Usa1999P5.empties, LE.le, OfNat.ofNat, Odd
5 instances, coercions and auxiliary constants left out.
```
def Inv (b : Board) (t : Bool) : Prop :=
…
```
Mentions: Usa1999P5.Board
lemma Usa1999P5.hasTrap_update A trap survives any move that avoids its middle squares (which are losing squares) line 693 source
Source documentation
A trap survives any move that avoids its middle squares (which are losing squares).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Board, Usa1999P5.HasTrap, Nat, LT.lt, OfNat.ofNat, Eq, Option, Usa1999P5.Piece, Option.none, Not, Usa1999P5.IsLosing, Function.update, Option.some
Proof uses: And, Membership.mem, Finset, Finset.range, Usa1999P5.TrapAt, HAdd.hAdd, Usa1999P5.trap_middle, Eq.mp, congrArg, propext, Finset.mem_range, Ne, And.left, Eq.symm, And.right, False.elim, False, Usa1999P5.Piece.S, eq_false', noConfusion_of_Nat and 8 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma hasTrap_update {b : Board} (hT : HasTrap b) {x : ℕ} (_hx : x < 2000) (hxe : b x = none)
    (hnl : ¬ IsLosing b x) (l : Piece) : HasTrap (Function.update b x (some l)) := by
…
```
Mentions: Usa1999P5.Board, Usa1999P5.HasTrap, Usa1999P5.IsLosing, Usa1999P5.Piece
lemma Usa1999P5.main_induction The heart of the argument: from an invariant position the second player wins line 716 source
Source documentation
The heart of the argument: from an invariant position the second player wins.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1999P5.Strategy, Nat, Usa1999P5.Board, Bool, LE.le, HAdd.hAdd, Finset.card, Usa1999P5.empties, OfNat.ofNat, Usa1999P5.Inv, Eq, Usa1999P5.Outcome, Usa1999P5.play, Usa1999P5.p2strat, Usa1999P5.Outcome.p2
Proof uses: Nat.recAux, Bool.false, Usa1999P5.BOK, And, Usa1999P5.ThreatFree, Not, Usa1999P5.HasSOS, Usa1999P5.HasTrap, ite, Bool.true, Even, Odd, Ne, Finset, EmptyCollection.emptyCollection, HMul.hMul, Usa1999P5.empties_ne_empty, Eq.mpr, Usa1999P5.Outcome.p1, Usa1999P5.Outcome.draw and 59 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 82 steps
Open to load the checked before-and-after goal states.
```
lemma main_induction (τ : Strategy) :
    ∀ fuel : ℕ, ∀ b : Board, ∀ t : Bool,
      (empties b).card + 1 ≤ fuel → Inv b t → play fuel τ p2strat b t = Outcome.p2 := by
…
```
Mentions: Usa1999P5.Strategy, Usa1999P5.Board, Usa1999P5.empties, Usa1999P5.Inv, Usa1999P5.play, Usa1999P5.p2strat
lemma Usa1999P5.exists_second_setup A good second setup move exists after the second player's first move, whatever the first player does (that is not immediately losing) line 798 source
Source documentation
A good second setup move exists after the second player's first move, whatever the first player does (that is not immediately losing).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa1999P5.Piece, LT.lt, OfNat.ofNat, Or, LE.le, HAdd.hAdd, Eq, Ne, Usa1999P5.ThreatFree, Function.update, Option, Option.none, Option.some, Usa1999P5.Piece.S, Exists, And, Membership.mem, Finset, Finset.range and 1 more
Proof uses: Eq.mpr, id, congrArg, rfl, Function.update_of_ne, Function.update_self, Eq.refl, Not, Usa1999P5.HasSOS, Usa1999P5.Piece.O, False, dite, Or.inl, Or.inr, False.elim, Eq.mp, Eq.trans, True, eq_self, not_true_eq_false and 19 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 197 steps
Open to load the checked before-and-after goal states.
```
lemma exists_second_setup {q p r : ℕ} {lq lr : Piece}
    (_hq : q < 2000) (hp : p < 2000) (_hr : r < 2000)
    (hpq : q + 500 ≤ p ∨ p + 500 ≤ q) (hp5 : p = 500 ∨ p = 1500)
    (hqr : q ≠ r) (hpr : p ≠ r)
    (hTF : ThreatFree (Function.update (Function.update
      (Function.update (fun _ => none) q (some lq)) p (some Piece.S)) r (some lr))) :
    ∃ t ∈ Finset.range 2000,
      SecondSetupOk (Function.update (Function.update
        (Function.update (fun _ => none) q (some lq)) p (some Piece.S)) r (some lr)) t := by
…
```
Mentions: Usa1999P5.Piece, Usa1999P5.ThreatFree, Usa1999P5.SecondSetupOk
problem Usa1999P5.usa1999_p5 line 932 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Usa1999P5.Strategy, Eq, Usa1999P5.Outcome, Usa1999P5.play, OfNat.ofNat, Nat, Option.none, Usa1999P5.Piece, Bool.true, Usa1999P5.Outcome.p2
Proof uses: Exists.intro, Usa1999P5.p2strat, Usa1999P5.BOK, LE.le, rfl, Option, Not, Usa1999P5.HasSOS, And, Membership.mem, Finset, Finset.range, Option.some, Usa1999P5.Piece.S, HAdd.hAdd, Usa1999P5.Piece.O, False, False.elim, Eq.mp, eq_false' and 95 more
90 instances, coercions and auxiliary constants left out.

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