`Compfiles/Usa2014P4.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 2014, Problem 4

Let k be a positive integer. Two players A and B play a game on an infinite grid of regular hexagons. Initially all the grid cells are empty. Then the players alternately take turns with A moving first. In her move, A may choose two adjacent hexagons in the grid which are empty and place a counter in both of them. In his move, B may choose any counter on the board and remove it. If at any time there are k consecutive grid cells in a line all of which contain a counter, A wins. Find the minimum value of k for which A cannot win in a finite number of moves, or prove that no such minimum value exists.

Imports (8)

Imported by 1 file

Compfiles.lean

abbrev Usa2014P4.Cell A cell of the hexagonal grid, given in axial coordinates line 38 source
Source documentation
A cell of the hexagonal grid, given in axial coordinates.

no axioms what this means
Proof uses: Prod, Int
```
abbrev Cell := ℤ × ℤ
```
def Usa2014P4.offsets The six unit steps between adjacent cells of the grid line 41 source
Source documentation
The six unit steps between adjacent cells of the grid.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Usa2014P4.Cell
Proof uses: Insert.insert, Prod, Int, Prod.mk, OfNat.ofNat, Neg.neg, Singleton.singleton
6 instances, coercions and auxiliary constants left out.
```
def offsets : Finset Cell := {(1, 0), (-1, 0), (0, 1), (0, -1), (1, -1), (-1, 1)}
```
Mentions: Usa2014P4.Cell
def Usa2014P4.Adj Two cells are adjacent when their difference is one of the six unit steps line 44 source
Source documentation
Two cells are adjacent when their difference is one of the six unit steps.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2014P4.Cell
Proof uses: Membership.mem, Prod, Int, Finset, Usa2014P4.offsets, Prod.mk, HSub.hSub, Prod.fst, Prod.snd
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def Adj (c d : Cell) : Prop := (d.1 - c.1, d.2 - c.2) ∈ offsets
```
Mentions: Usa2014P4.Cell, Usa2014P4.offsets
instance Usa2014P4.(instance at line 46) line 46 source
def Usa2014P4.Dirs The three (undirected) line directions of the grid line 51 source
Source documentation
The three (undirected) line directions of the grid.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Usa2014P4.Cell
Proof uses: Insert.insert, Prod, Int, Prod.mk, OfNat.ofNat, Singleton.singleton, Neg.neg
6 instances, coercions and auxiliary constants left out.
```
def Dirs : Finset Cell := {(1, 0), (0, 1), (1, -1)}
```
Mentions: Usa2014P4.Cell
def Usa2014P4.step The cell reached from p by making i steps in direction d line 54 source
Source documentation
The cell reached from p by making i steps in direction d.

no axioms what this means
Statement uses: Usa2014P4.Cell, Nat
Proof uses: Prod.mk, Int, HAdd.hAdd, Prod.fst, HMul.hMul, Prod.snd
6 instances, coercions and auxiliary constants left out.
```
def step (p : Cell) (d : Cell) (i : ℕ) : Cell := (p.1 + (i : ℤ) * d.1, p.2 + (i : ℤ) * d.2)
```
Mentions: Usa2014P4.Cell
def Usa2014P4.Winning A has won on the board s: some line of k consecutive cells all carry a counter line 58 source
Source documentation
A has won on the board s: some line of k consecutive cells all carry a counter.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2014P4.Cell
Proof uses: Exists, And, Membership.mem, Usa2014P4.Dirs, LT.lt, Usa2014P4.step
3 instances, coercions and auxiliary constants left out.
```
def Winning (k : ℕ) (s : Finset Cell) : Prop :=
…
```
Mentions: Usa2014P4.Cell
def Usa2014P4.AMove A move of player A: place counters on two empty adjacent cells line 62 source
Source documentation
A move of player A: place counters on two empty adjacent cells.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa2014P4.Cell
Proof uses: Exists, And, Ne, Usa2014P4.Adj, Not, Membership.mem, Eq, Insert.insert, Int
5 instances, coercions and auxiliary constants left out.
```
def AMove (s s' : Finset Cell) : Prop :=
…
```
Mentions: Usa2014P4.Cell
def Usa2014P4.BMove A move of player B: remove one counter from the board line 66 source
Source documentation
A move of player B: remove one counter from the board.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa2014P4.Cell
Proof uses: Exists, And, Membership.mem, Eq, Finset.erase, Int
4 instances, coercions and auxiliary constants left out.
```
def BMove (s t : Finset Cell) : Prop := ∃ c ∈ s, t = s.erase c
```
Mentions: Usa2014P4.Cell
inductive Usa2014P4.AForce AForce k s means that from the board s, with A to move, A can force a win in finitely many moves regardless of how B plays line 72 source
Source documentation
AForce k s means that from the board s, with A to move, A can force a win in finitely many moves regardless of how B plays. Since the witness is an inductive tree covering all of B's responses, every play following the strategy ends in a win after finitely many moves.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2014P4.Cell
```
inductive AForce (k : ℕ) : Finset Cell → Prop
  | of_win {s s'} : AMove s s' → Winning k s' → AForce k s
  | of_step {s s'} : AMove s s' → (∀ t, BMove s' t → AForce k t) → AForce k s

/-- `A` can win the game with parameter `k` in finitely many moves. -/
```
Mentions: Usa2014P4.Cell, Usa2014P4.AMove, Usa2014P4.Winning, Usa2014P4.BMove
def Usa2014P4.ACanWin A can win the game with parameter k in finitely many moves line 77 source
Source documentation
A can win the game with parameter k in finitely many moves.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Usa2014P4.AForce, EmptyCollection.emptyCollection, Finset, Usa2014P4.Cell
1 instances, coercions and auxiliary constants left out.
```
def ACanWin (k : ℕ) : Prop := AForce k ∅
…
```
Mentions: Usa2014P4.AForce
def Usa2014P4.shaded The shading of the grid used in B's defense strategy for k = 6: every third cell is shaded line 85 source
Source documentation
The shading of the grid used in B's defense strategy for k = 6: every third cell is shaded.

no axioms what this means
Statement uses: Usa2014P4.Cell
Proof uses: Eq, Int, HMod.hMod, HSub.hSub, Prod.fst, Prod.snd, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def shaded (c : Cell) : Prop := (c.1 - c.2) % 3 = 0
```
Mentions: Usa2014P4.Cell
lemma Usa2014P4.mem_offsets Membership in offsets as an explicit case distinction line 88 source
Source documentation
Membership in offsets as an explicit case distinction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2014P4.Cell, Iff, Membership.mem, Finset, Usa2014P4.offsets, Or, Eq, Prod.mk, Int, OfNat.ofNat, Neg.neg
Proof uses: id, of_eq_true, Insert.insert, Prod, Singleton.singleton, Eq.trans, True, congrFun', congrArg, iff_self
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma mem_offsets {v : Cell} :
    v ∈ offsets ↔ v = (1, 0) ∨ v = (-1, 0) ∨ v = (0, 1) ∨ v = (0, -1) ∨
      v = (1, -1) ∨ v = (-1, 1) := by
…
```
Mentions: Usa2014P4.Cell, Usa2014P4.offsets
lemma Usa2014P4.mem_Dirs Membership in Dirs as an explicit case distinction line 95 source
Source documentation
Membership in Dirs as an explicit case distinction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2014P4.Cell, Iff, Membership.mem, Finset, Usa2014P4.Dirs, Or, Eq, Prod.mk, Int, OfNat.ofNat, Neg.neg
Proof uses: id, of_eq_true, Insert.insert, Prod, Singleton.singleton, Eq.trans, True, congrFun', congrArg, iff_self
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma mem_Dirs {v : Cell} : v ∈ Dirs ↔ v = (1, 0) ∨ v = (0, 1) ∨ v = (1, -1) := by
…
```
Mentions: Usa2014P4.Cell, Usa2014P4.Dirs
lemma Usa2014P4.adj_not_both_shaded Adjacent cells are never both shaded: adjacent cells have different colors line 100 source
Source documentation
Adjacent cells are never both shaded: adjacent cells have different colors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2014P4.Cell, Usa2014P4.Adj, Not, And, Usa2014P4.shaded
Proof uses: id, Eq, Prod.mk, Int, HSub.hSub, Prod.fst, Prod.snd, OfNat.ofNat, Or, Neg.neg, HMod.hMod, Eq.mp, Membership.mem, Finset, Usa2014P4.offsets, congrArg, propext, Usa2014P4.mem_offsets, Iff.mp, Prod and 1 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma adj_not_both_shaded {c d : Cell} (h : Adj c d) : ¬ (shaded c ∧ shaded d) := by
…
```
Mentions: Usa2014P4.Cell, h, Usa2014P4.Adj, Usa2014P4.shaded
lemma Usa2014P4.step_eq_of_eq The cells of a line are distinct line 105 source
Source documentation
The cells of a line are distinct.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2014P4.Cell, Membership.mem, Finset, Usa2014P4.Dirs, Nat, Eq, Usa2014P4.step
Proof uses: Prod.mk, Int, OfNat.ofNat, Or, Neg.neg, Eq.mp, congrArg, propext, Usa2014P4.mem_Dirs, HAdd.hAdd, Prod.fst, HMul.hMul, Prod.snd, of_eq_true, Eq.trans, True, congrFun', id, And, congr and 11 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma step_eq_of_eq {d : Cell} (hd : d ∈ Dirs) (p : Cell) {i j : ℕ}
    (h : step p d i = step p d j) : i = j := by
…
```
Mentions: Usa2014P4.Cell, Usa2014P4.Dirs, h, Usa2014P4.step
lemma Usa2014P4.two_shaded_of_line Any six consecutive cells in a line contain two distinct shaded cells line 111 source
Source documentation
Any six consecutive cells in a line contain two distinct shaded cells.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2014P4.Cell, Membership.mem, Finset, Usa2014P4.Dirs, Exists, Nat, And, LT.lt, OfNat.ofNat, Usa2014P4.shaded, Usa2014P4.step, Ne
Proof uses: Or, Eq, Int, HSub.hSub, Prod.fst, Prod.snd, Neg.neg, Prod.mk, Eq.mp, congrArg, propext, Usa2014P4.mem_Dirs, of_eq_true, Eq.trans, True, False, congr, eq_true, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.instAddMonoidWithOne and 65 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma two_shaded_of_line {d : Cell} (hd : d ∈ Dirs) (p : Cell) :
    ∃ i j : ℕ, i < 6 ∧ j < 6 ∧
      shaded (step p d i) ∧ shaded (step p d j) ∧ step p d i ≠ step p d j := by
…
```
Mentions: Usa2014P4.Cell, Usa2014P4.Dirs, Usa2014P4.shaded, Usa2014P4.step
theorem Usa2014P4.not_ACanWin_six Player B has a strategy preventing A from ever getting six consecutive cells in a line: B always removes a counter on a shaded cell line 134 source
Source documentation
Player B has a strategy preventing A from ever getting six consecutive cells in a line: B always removes a counter on a shaded cell.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Usa2014P4.ACanWin, OfNat.ofNat, Nat
Proof uses: Finset, Usa2014P4.Cell, Usa2014P4.AForce, Membership.mem, Usa2014P4.shaded, False, Usa2014P4.AForce.rec, Usa2014P4.AMove, Usa2014P4.Winning, Exists, And, Ne, Usa2014P4.Adj, Eq, Insert.insert, Int, Usa2014P4.Dirs, LT.lt, Usa2014P4.step, Usa2014P4.two_shaded_of_line and 35 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 85 steps
Open to load the checked before-and-after goal states.
```
theorem not_ACanWin_six : ¬ ACanWin 6 := by
…
```
Mentions: Usa2014P4.ACanWin
lemma Usa2014P4.winning_of_neg A line traversed in the opposite direction is still a line line 202 source
Source documentation
A line traversed in the opposite direction is still a line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2014P4.Cell, Membership.mem, Usa2014P4.Dirs, LT.lt, Usa2014P4.step, Neg.neg, Int, Usa2014P4.Winning
Proof uses: Nat.casesAuxOn, OfNat.ofNat, Exists.intro, And, Exists, And.intro, HAdd.hAdd, Eq, Prod.mk, Prod.fst, Prod.snd, rfl, HSub.hSub, Eq.mpr, id, congrArg, Prod, propext, Prod.ext_iff, HMul.hMul and 39 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma winning_of_neg {k : ℕ} {s : Finset Cell} {d : Cell} (hd : d ∈ Dirs) {p : Cell}
    (h : ∀ i : ℕ, i < k → step p (-d) i ∈ s) : Winning k s := by
…
```
Mentions: Usa2014P4.Cell, Usa2014P4.Dirs, h, Usa2014P4.step, Usa2014P4.Winning
lemma Usa2014P4.AForce_image Generic transport of AForce along a map preserving the game structure line 217 source
Source documentation
Generic transport of AForce along a map preserving the game structure.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2014P4.Cell, Function.Injective, Iff, Usa2014P4.Adj, Finset, Usa2014P4.Winning, Finset.image, Int, Usa2014P4.AForce
Proof uses: Usa2014P4.AForce.rec, Usa2014P4.AMove, Exists, And, Ne, Not, Membership.mem, Eq, Insert.insert, Exists.intro, And.intro, Iff.mpr, False, Iff.mp, Finset.mem_image, Eq.rec, rfl, Usa2014P4.AForce.of_win, Eq.mpr, id and 20 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
lemma AForce_image {k : ℕ} {φ : Cell → Cell} (hφ : Function.Injective φ)
    (hφ_adj : ∀ c d, Adj (φ c) (φ d) ↔ Adj c d)
    (hφ_win : ∀ s, Winning k s → Winning k (s.image φ))
    {s : Finset Cell} (h : AForce k s) : AForce k (s.image φ) := by
…
```
Mentions: Usa2014P4.Cell, Usa2014P4.Adj, Usa2014P4.Winning, h, Usa2014P4.AForce
def Usa2014P4.rot Rotation by 60 degrees about the origin line 260 source
Source documentation
Rotation by 60 degrees about the origin.

no axioms what this means
Statement uses: Usa2014P4.Cell
Proof uses: Prod.mk, Int, Neg.neg, Prod.snd, HAdd.hAdd, Prod.fst
3 instances, coercions and auxiliary constants left out.
```
def rot (c : Cell) : Cell := (-c.2, c.1 + c.2)
```
Mentions: Usa2014P4.Cell
lemma Usa2014P4.rot_injective line 262 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Usa2014P4.Cell, Usa2014P4.rot
Proof uses: Eq, Int, Prod.fst, Prod.mk, Neg.neg, Prod.snd, HAdd.hAdd, And, Eq.mp, Prod, congrArg, propext, Prod.ext_iff, Prod.ext
6 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2014P4.adj_rot line 271 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2014P4.Cell, Iff, Usa2014P4.Adj, Usa2014P4.rot
Proof uses: Eq, Finset, Finset.image, Int, Usa2014P4.offsets, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Prod, Prod.mk, HSub.hSub, Prod.fst, Prod.snd, Eq.mpr, And, congrArg, propext and 45 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Usa2014P4.step_rot line 287 source
standard axioms: Quot.sound, propext what this means
Statement uses: Usa2014P4.Cell, Nat, Eq, Usa2014P4.step, Usa2014P4.rot
Proof uses: Eq.mpr, And, Int, Prod.fst, Prod.snd, id, congrArg, Prod, propext, Prod.ext_iff, Prod.mk, HAdd.hAdd, HMul.hMul, And.intro, Neg.neg, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance and 32 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2014P4.winning_rot line 290 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2014P4.Cell, Usa2014P4.Winning, Finset.image, Int, Usa2014P4.rot
Proof uses: And, Membership.mem, Usa2014P4.Dirs, Exists, LT.lt, Usa2014P4.step, Eq, Prod.mk, OfNat.ofNat, Or, Neg.neg, Eq.mp, congrArg, propext, Usa2014P4.mem_Dirs, Exists.intro, And.intro, of_eq_true, Insert.insert, Prod and 27 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma Usa2014P4.AForce_image_rot line 309 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2014P4.Cell, Usa2014P4.AForce, Finset.image, Int, Usa2014P4.rot
Proof uses: Usa2014P4.AForce_image, Usa2014P4.rot_injective, Usa2014P4.adj_rot, Usa2014P4.Winning, Usa2014P4.winning_rot
2 instances, coercions and auxiliary constants left out.
lemma Usa2014P4.AForce_image_rotpow Rotation by an arbitrary multiple of 60 degrees line 314 source
Source documentation
Rotation by an arbitrary multiple of 60 degrees.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2014P4.Cell, Usa2014P4.AForce, Finset.image, Int, Nat.iterate, Usa2014P4.rot
Proof uses: Nat.recAux, Eq.mpr, OfNat.ofNat, id, Eq, congrArg, Finset.image_id, HAdd.hAdd, Function.comp, Nat.succ, Function.iterate_succ', Eq.symm, Finset.image_image, Usa2014P4.AForce_image_rot
7 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma AForce_image_rotpow {k : ℕ} {s : Finset Cell} (j : ℕ) (h : AForce k s) :
    AForce k (s.image (rot^[j])) := by
…
```
Mentions: Usa2014P4.Cell, h, Usa2014P4.AForce, Usa2014P4.rot
def Usa2014P4.transl Translation by a fixed cell line 323 source
Source documentation
Translation by a fixed cell.

no axioms what this means
Statement uses: Usa2014P4.Cell
Proof uses: Prod.mk, Int, HAdd.hAdd, Prod.fst, Prod.snd
2 instances, coercions and auxiliary constants left out.
```
def transl (t : Cell) (c : Cell) : Cell := (c.1 + t.1, c.2 + t.2)
```
Mentions: Usa2014P4.Cell
lemma Usa2014P4.transl_injective line 325 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2014P4.Cell, Function.Injective, Usa2014P4.transl
Proof uses: Eq, Eq.mpr, And, Int, Prod.fst, Prod.snd, id, congrArg, Prod, propext, Prod.ext_iff, Eq.mp, Prod.mk, HAdd.hAdd
3 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2014P4.adj_transl line 331 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2014P4.Cell, Iff, Usa2014P4.Adj, Usa2014P4.transl
Proof uses: Eq, Prod, Int, Prod.mk, HSub.hSub, Prod.fst, Prod.snd, Eq.mpr, And, id, congrArg, propext, Prod.ext_iff, And.intro, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat, Nat.rawCast and 34 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2014P4.step_transl line 338 source
standard axioms: propext what this means
Statement uses: Usa2014P4.Cell, Nat, Eq, Usa2014P4.step, Usa2014P4.transl
Proof uses: Eq.mpr, And, Int, Prod.fst, Prod.snd, id, congrArg, Prod, propext, Prod.ext_iff, Prod.mk, HAdd.hAdd, HMul.hMul, And.intro, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, OfNat.ofNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf and 17 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2014P4.winning_transl line 341 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2014P4.Cell, Finset, Usa2014P4.Winning, Finset.image, Int, Usa2014P4.transl
Proof uses: And, Membership.mem, Usa2014P4.Dirs, Exists, LT.lt, Usa2014P4.step, Exists.intro, And.intro, Eq.mpr, id, Eq, congrArg, Usa2014P4.step_transl, Finset.mem_image_of_mem
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2014P4.AForce_image_transl line 347 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2014P4.Cell, Finset, Usa2014P4.AForce, Finset.image, Int, Usa2014P4.transl
Proof uses: Usa2014P4.AForce_image, Usa2014P4.transl_injective, Usa2014P4.adj_transl, Usa2014P4.Winning, Usa2014P4.winning_transl
2 instances, coercions and auxiliary constants left out.
def Usa2014P4.mirror The point reflection swapping the two distinguished cells x₀ = (1, 0) and y₀ = (4, 0) of the strategy below line 353 source
Source documentation
The point reflection swapping the two distinguished cells x₀ = (1, 0) and y₀ = (4, 0) of the strategy below.

no axioms what this means
Statement uses: Usa2014P4.Cell
Proof uses: Prod.mk, Int, HSub.hSub, OfNat.ofNat, Prod.fst, Neg.neg, Prod.snd
4 instances, coercions and auxiliary constants left out.
```
def mirror (c : Cell) : Cell := (5 - c.1, -c.2)
```
Mentions: Usa2014P4.Cell
lemma Usa2014P4.mirror_injective line 355 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Usa2014P4.Cell, Usa2014P4.mirror
Proof uses: Eq, Eq.mpr, And, Int, Prod.fst, Prod.snd, id, congrArg, Prod, propext, Prod.ext_iff, Eq.mp, Prod.mk, HSub.hSub, OfNat.ofNat, Neg.neg
5 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2014P4.adj_mirror line 361 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2014P4.Cell, Iff, Usa2014P4.Adj, Usa2014P4.mirror
Proof uses: Eq, Finset, Prod, Int, Finset.image, Prod.mk, Neg.neg, Prod.fst, Prod.snd, Usa2014P4.offsets, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, HSub.hSub, Eq.mpr, And, congrArg and 50 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Usa2014P4.winning_mirror line 381 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2014P4.Cell, Usa2014P4.Winning, Finset.image, Int, Usa2014P4.mirror
Proof uses: And, Membership.mem, Usa2014P4.Dirs, Exists, LT.lt, Usa2014P4.step, Usa2014P4.winning_of_neg, Eq, Neg.neg, Prod.mk, Prod.fst, Prod.snd, rfl, Eq.mpr, id, congrArg, Prod, propext, Prod.ext_iff, HAdd.hAdd and 43 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Usa2014P4.AForce_image_mirror line 394 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2014P4.Cell, Usa2014P4.AForce, Finset.image, Int, Usa2014P4.mirror
Proof uses: Usa2014P4.AForce_image, Usa2014P4.mirror_injective, Usa2014P4.adj_mirror, Usa2014P4.Winning, Usa2014P4.winning_mirror
2 instances, coercions and auxiliary constants left out.
def Usa2014P4.x₀ The first distinguished cell of the strategy line 408 source
Source documentation
The first distinguished cell of the strategy.

no axioms what this means
Statement uses: Usa2014P4.Cell
Proof uses: Prod.mk, Int, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
def x₀ : Cell := (1, 0)
```
Mentions: Usa2014P4.Cell
def Usa2014P4.y₀ The second distinguished cell of the strategy line 411 source
Source documentation
The second distinguished cell of the strategy.

no axioms what this means
Statement uses: Usa2014P4.Cell
Proof uses: Prod.mk, Int, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
def y₀ : Cell := (4, 0)
```
Mentions: Usa2014P4.Cell
def Usa2014P4.xSlots The neighbor slots of x₀ (other than (0, 0) and the central cell (2, 0)) that the strategy fills one by one line 415 source
Source documentation
The neighbor slots of x₀ (other than (0, 0) and the central cell (2, 0)) that the strategy fills one by one.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Usa2014P4.Cell
Proof uses: Insert.insert, Prod, Int, Prod.mk, OfNat.ofNat, Neg.neg, Singleton.singleton
6 instances, coercions and auxiliary constants left out.
```
def xSlots : Finset Cell := {(1, 1), (0, 1), (1, -1), (2, -1)}
```
Mentions: Usa2014P4.Cell
def Usa2014P4.ySlots The neighbor slots of y₀ (other than (5, 0) and the central cell (3, 0)) that the strategy fills one by one line 419 source
Source documentation
The neighbor slots of y₀ (other than (5, 0) and the central cell (3, 0)) that the strategy fills one by one.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Usa2014P4.Cell
Proof uses: Insert.insert, Prod, Int, Prod.mk, OfNat.ofNat, Neg.neg, Singleton.singleton
6 instances, coercions and auxiliary constants left out.
```
def ySlots : Finset Cell := {(4, 1), (3, 1), (4, -1), (5, -1)}
```
Mentions: Usa2014P4.Cell
lemma Usa2014P4.winning_row0 Five consecutive cells on the first axis give a win line 422 source
Source documentation
Five consecutive cells on the first axis give a win.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Finset, Usa2014P4.Cell, Membership.mem, Prod, Prod.mk, OfNat.ofNat, HAdd.hAdd, Usa2014P4.Winning, Nat
Proof uses: Exists.intro, And, Usa2014P4.Dirs, Exists, LT.lt, Usa2014P4.step, And.intro, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, dite, LE.le, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right and 20 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma winning_row0 (a : ℤ) {t : Finset Cell}
    (h0 : (a, 0) ∈ t) (h1 : (a + 1, 0) ∈ t) (h2 : (a + 2, 0) ∈ t)
    (h3 : (a + 3, 0) ∈ t) (h4 : (a + 4, 0) ∈ t) : Winning 5 t := by
…
```
Mentions: Usa2014P4.Cell, Usa2014P4.Winning
lemma Usa2014P4.winning_diag The diagonal line through (1, 1) in direction (1, -1) line 435 source
Source documentation
The diagonal line through (1, 1) in direction (1, -1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa2014P4.Cell, Membership.mem, Prod, Int, Prod.mk, OfNat.ofNat, Neg.neg, Usa2014P4.Winning, Nat
Proof uses: Exists.intro, And, Usa2014P4.Dirs, Exists, LT.lt, Usa2014P4.step, And.intro, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, dite, LE.le, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right and 5 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma winning_diag {t : Finset Cell}
    (h0 : (1, 1) ∈ t) (h1 : (2, 0) ∈ t) (h2 : (3, -1) ∈ t)
    (h3 : (4, -2) ∈ t) (h4 : (5, -3) ∈ t) : Winning 5 t := by
…
```
Mentions: Usa2014P4.Cell, Usa2014P4.Winning
lemma Usa2014P4.win_now0 Completing the first five cells of row 0 wins immediately line 447 source
Source documentation
Completing the first five cells of row 0 wins immediately.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa2014P4.Cell, Not, Membership.mem, Prod, Int, Prod.mk, OfNat.ofNat, Usa2014P4.x₀, Usa2014P4.y₀, Usa2014P4.AForce, Nat
Proof uses: Usa2014P4.AForce.of_win, Insert.insert, Exists.intro, Exists, And, Ne, Usa2014P4.Adj, Eq, And.intro, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, rfl, Usa2014P4.winning_row0, Finset.mem_insert_of_mem, HAdd.hAdd, Finset.mem_insert_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma win_now0 {s : Finset Cell} (h2 : (2, 0) ∉ s) (h3 : (3, 0) ∉ s)
    (h0 : (0, 0) ∈ s) (h1 : x₀ ∈ s) (h4 : y₀ ∈ s) : AForce 5 s := by
…
```
Mentions: Usa2014P4.Cell, Usa2014P4.x₀, Usa2014P4.y₀, Usa2014P4.AForce
lemma Usa2014P4.win_now1 Completing the cells (1, 0) to (5, 0) of row 0 wins immediately line 459 source
Source documentation
Completing the cells (1, 0) to (5, 0) of row 0 wins immediately.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa2014P4.Cell, Not, Membership.mem, Prod, Int, Prod.mk, OfNat.ofNat, Usa2014P4.x₀, Usa2014P4.y₀, Usa2014P4.AForce, Nat
Proof uses: Usa2014P4.AForce.of_win, Insert.insert, Exists.intro, Exists, And, Ne, Usa2014P4.Adj, Eq, And.intro, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, rfl, Usa2014P4.winning_row0, Finset.mem_insert_of_mem, Finset.mem_insert_self, HAdd.hAdd
15 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma win_now1 {s : Finset Cell} (h2 : (2, 0) ∉ s) (h3 : (3, 0) ∉ s)
    (h1 : x₀ ∈ s) (h4 : y₀ ∈ s) (h5 : (5, 0) ∈ s) : AForce 5 s := by
…
```
Mentions: Usa2014P4.Cell, Usa2014P4.x₀, Usa2014P4.y₀, Usa2014P4.AForce
lemma Usa2014P4.endgame_x_Bturn The endgame position with x₀ completely surrounded and filled: whatever counter B removes, A wins line 472 source
Source documentation
The endgame position with x₀ completely surrounded and filled: whatever counter B removes, A wins.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa2014P4.Cell, LE.le, Usa2014P4.ySlots, Usa2014P4.BMove, Union.union, Int, Insert.insert, Prod, Prod.mk, OfNat.ofNat, Singleton.singleton, Usa2014P4.xSlots, Usa2014P4.x₀, Usa2014P4.y₀, Usa2014P4.AForce, Nat
Proof uses: And, Membership.mem, Eq, Finset.erase, Eq.mpr, id, congrArg, rfl, of_eq_true, Eq.trans, Or, True, congrFun', Finset.insert_union, Finset.union_insert, Finset.union_assoc, Finset.union_singleton, False, congr, Prod.mk.injEq and 50 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 354 steps (first 200 of 354)
Open to load the checked before-and-after goal states.
```
lemma endgame_x_Bturn (Ny : Finset Cell) (hNy : Ny ⊆ ySlots) :
    ∀ t, BMove ({(0, 0), (5, 0)} ∪ xSlots ∪ Ny ∪ {(2, 0), x₀, y₀}) t → AForce 5 t := by
…
```
Mentions: Usa2014P4.Cell, Usa2014P4.ySlots, Usa2014P4.BMove, Usa2014P4.xSlots, Usa2014P4.x₀, Usa2014P4.y₀, Usa2014P4.AForce
lemma Usa2014P4.endgame_y_Bturn The mirrored endgame with y₀ completely surrounded and filled line 767 source
Source documentation
The mirrored endgame with y₀ completely surrounded and filled.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa2014P4.Cell, LE.le, Usa2014P4.xSlots, Usa2014P4.BMove, Union.union, Int, Insert.insert, Prod, Prod.mk, OfNat.ofNat, Singleton.singleton, Usa2014P4.ySlots, Usa2014P4.x₀, Usa2014P4.y₀, Usa2014P4.AForce, Nat
Proof uses: And, Membership.mem, Eq, Finset.erase, Usa2014P4.mirror, id, Eq.mpr, HSub.hSub, Prod.fst, Neg.neg, Prod.snd, congrArg, propext, Prod.ext_iff, And.intro, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat.rawCast and 49 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma endgame_y_Bturn (Nx : Finset Cell) (hNx : Nx ⊆ xSlots) :
    ∀ t, BMove ({(0, 0), (5, 0)} ∪ ySlots ∪ Nx ∪ {(3, 0), x₀, y₀}) t → AForce 5 t := by
…
```
Mentions: Usa2014P4.Cell, Usa2014P4.xSlots, Usa2014P4.BMove, Usa2014P4.ySlots, Usa2014P4.x₀, Usa2014P4.y₀, Usa2014P4.AForce
lemma Usa2014P4.midphase The midgame invariant: with (0, 0) and (5, 0) occupied, exactly one of x₀, y₀ missing, and the filled neighbor slots Nx ⊆ xSlots, Ny ⊆ ySlots, A can force a win line 801 source
Source documentation
The midgame invariant: with (0, 0) and (5, 0) occupied, exactly one of x₀, y₀ missing, and the filled neighbor slots Nx ⊆ xSlots, Ny ⊆ ySlots, A can force a win. A replaces the missing distinguished cell and fills one more of its neighbor slots each round; B must remove one of the two distinguished cells every round, so eventually one of them is completely surrounded and the endgame lemmas apply.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2014P4.Cell, Eq, HAdd.hAdd, HSub.hSub, Finset.card, Usa2014P4.xSlots, Usa2014P4.ySlots, LE.le, Or, Singleton.singleton, Usa2014P4.x₀, Usa2014P4.y₀, Usa2014P4.AForce, OfNat.ofNat, Union.union, Int, Insert.insert, Prod and 1 more
Proof uses: Nat.strong_induction_on, LT.lt, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Finset.card_le_card, dite, Not, Membership.mem, Ne, of_eq_true, Eq.trans, False, True, congrArg, congrFun', Finset.insert_union and 72 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 490 steps (first 200 of 490)
Open to load the checked before-and-after goal states.
```
lemma midphase : ∀ n : ℕ, ∀ Nx Ny P : Finset Cell,
    (xSlots.card - Nx.card) + (ySlots.card - Ny.card) = n →
    Nx ⊆ xSlots → Ny ⊆ ySlots → (P = {x₀} ∨ P = {y₀}) →
    AForce 5 ({(0, 0), (5, 0)} ∪ Nx ∪ Ny ∪ P) := by
…
```
Mentions: P, Usa2014P4.Cell, Usa2014P4.xSlots, Usa2014P4.ySlots, Usa2014P4.x₀, Usa2014P4.y₀, Usa2014P4.AForce
lemma Usa2014P4.canonical_pair With counters on two adjacent cells of a line, A places the mirror pair two spaces down the same line, reaching the midgame invariant line 1170 source
Source documentation
With counters on two adjacent cells of a line, A places the mirror pair two spaces down the same line, reaching the midgame invariant.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2014P4.AForce, OfNat.ofNat, Nat, Insert.insert, Prod, Int, Finset, Usa2014P4.Cell, Prod.mk, Singleton.singleton
Proof uses: Usa2014P4.AMove, Exists.intro, Exists, And, Ne, Usa2014P4.Adj, Not, Membership.mem, Eq, And.intro, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Usa2014P4.AForce.of_step, Usa2014P4.BMove, Finset.erase, Or and 22 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
lemma canonical_pair : AForce 5 ({(0, 0), (1, 0)}) := by
…
```
Mentions: Usa2014P4.AForce
lemma Usa2014P4.adjacent_pair With two counters on adjacent cells, A wins (transport of the canonical configuration along a grid symmetry) line 1201 source
Source documentation
With two counters on adjacent cells, A wins (transport of the canonical configuration along a grid symmetry).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2014P4.Cell, Ne, Usa2014P4.Adj, Usa2014P4.AForce, OfNat.ofNat, Nat, Insert.insert, Finset, Int, Singleton.singleton
Proof uses: Exists, Eq, Nat.iterate, Usa2014P4.rot, Prod.mk, HSub.hSub, Prod.fst, Prod.snd, Or, Neg.neg, Eq.mp, Membership.mem, Usa2014P4.offsets, congrArg, propext, Usa2014P4.mem_offsets, Exists.intro, Eq.symm, Eq.mpr, id and 54 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma adjacent_pair {P Q : Cell} (_hne : P ≠ Q) (hadj : Adj P Q) :
    AForce 5 ({P, Q}) := by
…
```
Mentions: P, Usa2014P4.Cell, Usa2014P4.Adj, Usa2014P4.AForce
theorem Usa2014P4.ACanWin_five A wins for k = 5, following the official solution: after two rounds a pair of adjacent counters remains, from which the strategy above wins line 1230 source
Source documentation
A wins for k = 5, following the official solution: after two rounds a pair of adjacent counters remains, from which the strategy above wins.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2014P4.ACanWin, OfNat.ofNat, Nat
Proof uses: id, Usa2014P4.AForce.of_step, EmptyCollection.emptyCollection, Finset, Usa2014P4.Cell, Insert.insert, Prod, Int, Prod.mk, Singleton.singleton, Exists.intro, Exists, And, Ne, Usa2014P4.Adj, Not, Membership.mem, Eq, And.intro, of_decide_eq_true and 16 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 87 steps
Open to load the checked before-and-after goal states.
```
theorem ACanWin_five : ACanWin 5 := by
…
```
Mentions: Usa2014P4.ACanWin
lemma Usa2014P4.AForce_mono If A can force a win with target l, A can also force a win with any smaller target k ≤ l (a line of l consecutive cells contains a line of k) line 1283 source
Source documentation
If A can force a win with target l, A can also force a win with any smaller target k ≤ l (a line of l consecutive cells contains a line of k).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Finset, Usa2014P4.Cell, Usa2014P4.AForce
Proof uses: Usa2014P4.AForce.rec, Usa2014P4.AMove, Usa2014P4.Winning, And, Membership.mem, Usa2014P4.Dirs, Exists, LT.lt, Usa2014P4.step, Usa2014P4.AForce.of_win, Exists.intro, And.intro, Usa2014P4.BMove, Usa2014P4.AForce.of_step
8 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma AForce_mono {k l : ℕ} (hkl : k ≤ l) {s : Finset Cell} (h : AForce l s) :
    AForce k s := by
…
```
Mentions: Usa2014P4.Cell, h, Usa2014P4.AForce
determine Usa2014P4.solution line 1294 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Usa2014P4.usa2014_p4 line 1296 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, And, LT.lt, OfNat.ofNat, Not, Usa2014P4.ACanWin, Usa2014P4.solution
Proof uses: And.intro, Membership.mem, Set, lowerBounds, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Usa2014P4.not_ACanWin_six, LE.le, id, Decidable.byContradiction, Usa2014P4.AForce_mono, Eq.mp, EmptyCollection.emptyCollection, Finset, Usa2014P4.Cell, Usa2014P4.ACanWin_five
24 instances, coercions and auxiliary constants left out.

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