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

67 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2016, Problem 6

Integers n and k are given, with n ≥ k ≥ 2. You play the following game against an evil wizard. The wizard has 2n cards; for each i = 1, ..., n, there are two cards labeled i. Initially, the wizard places all cards face down in a row, in unknown order. You may repeatedly make moves of the following form: you point to any k of the cards. The wizard then turns those cards face up. If any two of the cards match, the game is over and you win. Otherwise, you must look away, while the wizard arbitrarily permutes the k chosen cards and then turns them back face-down. Then, it is your turn again.

We say this game is winnable if there exist some positive integer m and some strategy that is guaranteed to win in at most m moves, no matter how the wizard responds. For which values of n and k is the game winnable?

Imports (5)

Imported by 1 file

Compfiles.lean

abbrev Usa2016P6.Arrangement An arrangement of the 2n cards: the label shown at each position line 43 source
Source documentation
An arrangement of the 2n cards: the label shown at each position.

no axioms what this means
Statement uses: Nat
Proof uses: Fin, HMul.hMul, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
abbrev Arrangement (n : ℕ) := Fin (2 * n) → Fin n
```
def Usa2016P6.Arrangement.Valid An arrangement is valid when each of the n labels appears exactly twice line 46 source
Source documentation
An arrangement is valid when each of the n labels appears exactly twice.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Arrangement
Proof uses: Fin, Eq, Finset.card, HMul.hMul, OfNat.ofNat, Finset.filter, Finset.univ
5 instances, coercions and auxiliary constants left out.
```
def Arrangement.Valid {n : ℕ} (a : Arrangement n) : Prop :=
…
```
Mentions: Usa2016P6.Arrangement
abbrev Usa2016P6.Observation An observation made by the player: the set of queried positions, together with the labels that were revealed (none outside the queried set) line 51 source
Source documentation
An observation made by the player: the set of queried positions, together with the labels that were revealed (none outside the queried set).

standard axioms: Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Prod, Finset, Fin, HMul.hMul, OfNat.ofNat, Option
3 instances, coercions and auxiliary constants left out.
```
abbrev Observation (n : ℕ) := Finset (Fin (2 * n)) × (Fin (2 * n) → Option (Fin n))
```
abbrev Usa2016P6.Strategy A player strategy: from the list of past observations, choose the next set of positions to query line 55 source
Source documentation
A player strategy: from the list of past observations, choose the next set of positions to query.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat
Proof uses: List, Usa2016P6.Observation, Finset, Fin, HMul.hMul, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
abbrev Strategy (n : ℕ) := List (Observation n) → Finset (Fin (2 * n))
```
Mentions: Usa2016P6.Observation
def Usa2016P6.Strategy.Valid A strategy is valid for the parameter k if it always queries exactly k cards line 59 source
Source documentation
A strategy is valid for the parameter k if it always queries exactly k cards.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy
Proof uses: List, Usa2016P6.Observation, Eq, Finset.card, Fin, HMul.hMul, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
def Strategy.Valid {n : ℕ} (σ : Strategy n) (k : ℕ) : Prop :=
…
```
Mentions: Usa2016P6.Strategy
def Usa2016P6.reveal The revealed labels, hidden (none) outside the queried set line 63 source
Source documentation
The revealed labels, hidden (none) outside the queried set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Arrangement, Finset, Fin, HMul.hMul, OfNat.ofNat, Option
Proof uses: ite, Membership.mem, Option.some, Option.none
10 instances, coercions and auxiliary constants left out.
```
def reveal {n : ℕ} (a : Arrangement n) (Q : Finset (Fin (2 * n))) :
    Fin (2 * n) → Option (Fin n) :=
…
```
Mentions: Usa2016P6.Arrangement
structure Usa2016P6.Wizard A wizard: an initial arrangement of the cards, and a way to permute the queried cards after each unsuccessful query line 69 source
Source documentation
A wizard: an initial arrangement of the cards, and a way to permute the queried cards after each unsuccessful query.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat
```
structure Wizard (n : ℕ) where
…
```
def Usa2016P6.Wizard.Valid A wizard plays legitimately if the initial arrangement has two cards of each label and each permutation only moves the currently queried cards line 75 source
Source documentation
A wizard plays legitimately if the initial arrangement has two cards of each label and each permutation only moves the currently queried cards.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Wizard
Proof uses: And, Usa2016P6.Arrangement.Valid, Usa2016P6.Wizard.init, List, Usa2016P6.Observation, Finset, Fin, HMul.hMul, OfNat.ofNat, Not, Membership.mem, Eq, Equiv.Perm, Usa2016P6.Wizard.perm
8 instances, coercions and auxiliary constants left out.
```
def Wizard.Valid {n : ℕ} (W : Wizard n) : Prop :=
…
```
Mentions: Usa2016P6.Wizard
structure Usa2016P6.PlayState The state of play: the current arrangement, the past observations, and whether the player has already won line 80 source
Source documentation
The state of play: the current arrangement, the past observations, and whether the player has already won.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat
```
structure PlayState (n : ℕ) where
…
```
def Usa2016P6.step One round of the game line 86 source
Source documentation
One round of the game.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Wizard, Usa2016P6.PlayState
Proof uses: ite, Eq, Bool, Usa2016P6.PlayState.won, Bool.true, Finset, Fin, HMul.hMul, OfNat.ofNat, Usa2016P6.PlayState.hist, Finset.card, Finset.image, Usa2016P6.PlayState.arr, Usa2016P6.PlayState.mk, Function.comp, Equiv.Perm, Usa2016P6.Wizard.perm, HAppend.hAppend, List, Usa2016P6.Observation and 7 more
11 instances, coercions and auxiliary constants left out.
```
def step {n : ℕ} (σ : Strategy n) (W : Wizard n) (s : PlayState n) : PlayState n :=
…
```
Mentions: Usa2016P6.Strategy, Usa2016P6.Wizard, Usa2016P6.PlayState
def Usa2016P6.play The state after m rounds of play line 97 source
Source documentation
The state after m rounds of play.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Wizard, Usa2016P6.PlayState
2 instances, coercions and auxiliary constants left out.
```
def play {n : ℕ} (σ : Strategy n) (W : Wizard n) : ℕ → PlayState n
  | 0 => { arr := W.init, hist := [], won := false }
…
```
Mentions: Usa2016P6.Strategy, Usa2016P6.Wizard, Usa2016P6.PlayState
def Usa2016P6.Winnable The game is winnable if some valid strategy guarantees a win within m moves against every legitimate wizard line 103 source
Source documentation
The game is winnable if some valid strategy guarantees a win within m moves against every legitimate wizard.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Exists, And, GE.ge, OfNat.ofNat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, Usa2016P6.Wizard, Usa2016P6.Wizard.Valid, Eq, Bool, Usa2016P6.PlayState.won, Usa2016P6.play, Bool.true
2 instances, coercions and auxiliary constants left out.
```
def Winnable (n k : ℕ) : Prop :=
…
```
lemma Usa2016P6.play_succ line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Wizard, Eq, Usa2016P6.PlayState, Usa2016P6.play, HAdd.hAdd, OfNat.ofNat, Usa2016P6.step
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma Usa2016P6.step_of_won line 111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Wizard, Usa2016P6.PlayState, Eq, Bool, Usa2016P6.PlayState.won, Bool.true, Usa2016P6.step
Proof uses: id, Eq.mpr, ite, Finset, Fin, HMul.hMul, OfNat.ofNat, Usa2016P6.PlayState.hist, Finset.card, Finset.image, Usa2016P6.PlayState.arr, Usa2016P6.PlayState.mk, Function.comp, Equiv.Perm, Usa2016P6.Wizard.perm, HAppend.hAppend, List, Usa2016P6.Observation, Prod, Option and 8 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P6.won_mono line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Wizard, Eq, Bool, Usa2016P6.PlayState.won, Usa2016P6.play, Bool.true, LE.le
Proof uses: Nat.le.rec, Nat.le, Eq.mpr, Nat.succ, Usa2016P6.step, id, congrArg, Usa2016P6.PlayState, HAdd.hAdd, OfNat.ofNat, Usa2016P6.play_succ, Usa2016P6.step_of_won, Eq.refl
5 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P6.image_eq_of_perm_fix line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Equiv.Perm, Finset, Not, Membership.mem, Eq, Finset.image
Proof uses: Finset.ext, Eq.mpr, Iff, Exists, And, id, congrFun', congrArg, Iff.intro, Decidable.byContradiction, Equiv.injective, Eq.mp, Exists.intro, Equiv, Equiv.symm, And.intro, Eq.symm, Equiv.apply_symm_apply
15 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
def Usa2016P6.obsValues The labels revealed in an observation on a given set of positions line 142 source
Source documentation
The labels revealed in an observation on a given set of positions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Observation, Finset, Fin, HMul.hMul, OfNat.ofNat
Proof uses: Finset.biUnion, Option.toFinset, Prod.snd, Option
7 instances, coercions and auxiliary constants left out.
```
def obsValues {n : ℕ} (o : Observation n) (s : Finset (Fin (2 * n))) : Finset (Fin n) :=
…
```
Mentions: Usa2016P6.Observation
lemma Usa2016P6.obsValues_eq_image line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Arrangement, Finset, Fin, HMul.hMul, OfNat.ofNat, LE.le, Eq, Usa2016P6.obsValues, Prod.mk, Option, Usa2016P6.reveal, Finset.image
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, And, Option.some, id, congr, congrArg, Eq.trans, Finset.biUnion, Option.toFinset, funext, Iff.intro, Exists.intro, And.intro, Option.some.inj, Eq.mp, ite and 4 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def Usa2016P6.window The window of k consecutive positions starting at j (the empty set if it does not fit) line 160 source
Source documentation
The window of k consecutive positions starting at j (the empty set if it does not fit).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, HMul.hMul, OfNat.ofNat
Proof uses: dite, LE.le, HAdd.hAdd, Finset.image, Subtype, Membership.mem, Finset.range, Usa2016P6.window.match_1, Fin.mk, Finset.attach, Not, EmptyCollection.emptyCollection
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def window (n k j : ℕ) : Finset (Fin (2 * n)) :=
…
```
lemma Usa2016P6.card_window line 165 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Eq, Finset.card, Fin, Usa2016P6.window
Proof uses: Eq.mpr, dite, Finset, Finset.image, Subtype, Membership.mem, Finset.range, Usa2016P6.window.match_1, Fin.mk, Finset.attach, Not, EmptyCollection.emptyCollection, id, congrArg, Usa2016P6.window.eq_1, dite_eq_left, Finset.card_image_of_injOn, Set, Subtype.mk, Eq.mp and 4 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P6.mem_window line 173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Fin, Iff, Membership.mem, Finset, Usa2016P6.window, And, LT.lt
Proof uses: Eq.mpr, dite, Finset.image, Subtype, Finset.range, Usa2016P6.window.match_1, Fin.mk, Finset.attach, Not, EmptyCollection.emptyCollection, id, Eq, congrArg, Usa2016P6.window.eq_1, dite_eq_left, Exists, Subtype.mk, Iff.mpr, Iff.of_eq, Eq.refl and 14 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
def Usa2016P6.midWindow The k - 1 positions strictly between i and i + k (the empty set if they do not fit) line 188 source
Source documentation
The k - 1 positions strictly between i and i + k (the empty set if they do not fit).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, HMul.hMul, OfNat.ofNat
Proof uses: dite, LE.le, HAdd.hAdd, Finset.image, Subtype, Membership.mem, Finset.range, HSub.hSub, Usa2016P6.midWindow.match_1, Fin.mk, Finset.attach, Not, EmptyCollection.emptyCollection
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def midWindow (n k i : ℕ) : Finset (Fin (2 * n)) :=
…
```
lemma Usa2016P6.card_midWindow line 194 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Eq, Finset.card, Fin, Usa2016P6.midWindow, HSub.hSub
Proof uses: Eq.mpr, dite, Finset, Finset.image, Subtype, Membership.mem, Finset.range, Usa2016P6.midWindow.match_1, Fin.mk, Finset.attach, Not, EmptyCollection.emptyCollection, id, congrArg, Usa2016P6.midWindow.eq_1, dite_eq_left, Finset.card_image_of_injOn, Set, Subtype.mk, Eq.mp and 4 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P6.mem_midWindow line 202 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Fin, Iff, Membership.mem, Finset, Usa2016P6.midWindow, And, LT.lt
Proof uses: Eq.mpr, dite, Finset.image, Subtype, Finset.range, HSub.hSub, Usa2016P6.midWindow.match_1, Fin.mk, Finset.attach, Not, EmptyCollection.emptyCollection, id, Eq, congrArg, Usa2016P6.midWindow.eq_1, dite_eq_left, Exists, Subtype.mk, Iff.mpr, Iff.of_eq and 14 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P6.midWindow_subset_window line 215 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset, Fin, Usa2016P6.midWindow, Usa2016P6.window
Proof uses: Membership.mem, Eq.mpr, And, LT.lt, id, Eq, congrArg, propext, Usa2016P6.mem_window, Eq.mp, Usa2016P6.mem_midWindow
20 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P6.midWindow_subset_window_succ line 222 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset, Fin, Usa2016P6.midWindow, Usa2016P6.window
Proof uses: Membership.mem, Eq.mpr, And, LT.lt, id, Eq, congrArg, propext, Usa2016P6.mem_window, Eq.mp, Usa2016P6.mem_midWindow
20 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Usa2016P6.labelAt The label the player can deduce at position i, computed from observations i and i + 1 (junk value 0 when those observations are not available) line 231 source
Source documentation
The label the player can deduce at position i, computed from observations i and i + 1 (junk value 0 when those observations are not available).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, List, Usa2016P6.Observation, Fin
Proof uses: dite, And, LT.lt, HAdd.hAdd, OfNat.ofNat, List.length, LE.le, HMul.hMul, Finset, Usa2016P6.obsValues, List.get, Fin.mk, Usa2016P6.window, Usa2016P6.midWindow, Finset.Nonempty, SDiff.sdiff, Exists.choose, Membership.mem, Not
22 instances, coercions and auxiliary constants left out.
```
noncomputable def labelAt (n k : ℕ) [NeZero n] (hist : List (Observation n)) (i : ℕ) :
    Fin n :=
…
```
Mentions: Usa2016P6.Observation
def Usa2016P6.posOf The position in the row corresponding to a deduced-label index line 240 source
Source documentation
The position in the row corresponding to a deduced-label index.

no axioms what this means
Statement uses: Nat, Fin, HSub.hSub, HMul.hMul, OfNat.ofNat
Proof uses: Fin.mk
12 instances, coercions and auxiliary constants left out.
```
def posOf (n k : ℕ) (p : Fin (2 * n - k)) : Fin (2 * n) :=
…
```
lemma Usa2016P6.posOf_val line 243 source
no axioms what this means
Statement uses: Nat, Fin, HSub.hSub, HMul.hMul, OfNat.ofNat, Eq, Usa2016P6.posOf
Proof uses: rfl
12 instances, coercions and auxiliary constants left out.
lemma Usa2016P6.posOf_ne line 245 source
no axioms what this means
Statement uses: Nat, Fin, HSub.hSub, HMul.hMul, OfNat.ofNat, Ne, Usa2016P6.posOf
Proof uses: Eq, Fin.ext, congrArg, Eq.mp, Usa2016P6.posOf_val
11 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P6.pairSet_exists line 253 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HSub.hSub, HMul.hMul, Ne, Exists, Finset, And, Eq, Finset.card, Membership.mem, Usa2016P6.posOf
Proof uses: SDiff.sdiff, Finset.univ, Insert.insert, Singleton.singleton, Finset.exists_subset_card_eq, Eq.mpr, Inter.inter, id, congrArg, Finset.card_sdiff, Fintype.card, Finset.card_univ, Fintype.card_fin, Finset.inter_univ, HAdd.hAdd, Finset.card_insert_of_notMem, Not, Usa2016P6.posOf_ne, Finset.card_singleton, Disjoint and 13 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
def Usa2016P6.pairSet A set of k positions containing the two given (distinct) positions line 274 source
Source documentation
A set of k positions containing the two given (distinct) positions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HSub.hSub, HMul.hMul, Ne, Finset
Proof uses: Exists.choose, And, Eq, Finset.card, Membership.mem, Usa2016P6.posOf, Usa2016P6.pairSet_exists
14 instances, coercions and auxiliary constants left out.
```
noncomputable def pairSet (n k : ℕ) (hk : 2 ≤ k) (hkn : k ≤ n)
    (p q : Fin (2 * n - k)) (hpq : p ≠ q) : Finset (Fin (2 * n)) :=
…
```
lemma Usa2016P6.pairSet_card line 278 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HSub.hSub, HMul.hMul, Ne, Eq, Finset.card, Usa2016P6.pairSet
Proof uses: And.left, Exists.choose, Finset, And, Membership.mem, Usa2016P6.posOf, Usa2016P6.pairSet_exists, Exists.choose_spec
14 instances, coercions and auxiliary constants left out.
lemma Usa2016P6.posOf_mem_pairSet line 282 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HSub.hSub, HMul.hMul, Ne, Membership.mem, Finset, Usa2016P6.pairSet, Usa2016P6.posOf
Proof uses: And.left, Exists.choose, And, Eq, Finset.card, Usa2016P6.pairSet_exists, And.right, Exists.choose_spec
16 instances, coercions and auxiliary constants left out.
lemma Usa2016P6.posOf_mem_pairSet' line 286 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HSub.hSub, HMul.hMul, Ne, Membership.mem, Finset, Usa2016P6.pairSet, Usa2016P6.posOf
Proof uses: And.right, Exists.choose, And, Eq, Finset.card, Usa2016P6.pairSet_exists, Exists.choose_spec
16 instances, coercions and auxiliary constants left out.
def Usa2016P6.winStrat The winning strategy: slide a window of k positions across the row, then query two positions that are known to carry the same label line 292 source
Source documentation
The winning strategy: slide a window of k positions across the row, then query two positions that are known to carry the same label.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LE.le, OfNat.ofNat, Usa2016P6.Strategy
Proof uses: List, Usa2016P6.Observation, ite, Finset, Fin, HMul.hMul, HAdd.hAdd, List.length, Usa2016P6.window, dite, Exists, HSub.hSub, And, Ne, Eq, Usa2016P6.labelAt, Usa2016P6.pairSet, Exists.choose, Not
22 instances, coercions and auxiliary constants left out.
```
noncomputable def winStrat (n k : ℕ) [NeZero n] (hk : 2 ≤ k) (hkn : k ≤ n) :
    Strategy n :=
…
```
Mentions: Usa2016P6.Strategy
lemma Usa2016P6.winStrat_valid line 302 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LE.le, OfNat.ofNat, Usa2016P6.Strategy.Valid, Usa2016P6.winStrat
Proof uses: List, Usa2016P6.Observation, id, Eq, Finset.card, Fin, HMul.hMul, HAdd.hAdd, List.length, Decidable, ite, Finset, Usa2016P6.window, dite, Exists, HSub.hSub, And, Ne, Usa2016P6.labelAt, Usa2016P6.pairSet and 11 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
abbrev Usa2016P6.slideStrat The winning strategy specialized to k < n line 313 source
Source documentation
The winning strategy specialized to k < n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LE.le, OfNat.ofNat, LT.lt, Usa2016P6.Strategy
Proof uses: Usa2016P6.winStrat, le_of_lt
11 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev slideStrat (n k : ℕ) [NeZero n] (hk : 2 ≤ k) (hkn : k < n) : Strategy n :=
…
```
Mentions: Usa2016P6.Strategy
lemma Usa2016P6.step_apply_of_not_won line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Wizard, Usa2016P6.PlayState, Not, Eq, Bool, Usa2016P6.PlayState.won, Bool.true, Usa2016P6.step, ite, Finset.card, Fin, Finset.image, HMul.hMul, OfNat.ofNat, Usa2016P6.PlayState.arr, Usa2016P6.PlayState.hist, Usa2016P6.PlayState.mk, Function.comp and 13 more
Proof uses: id, Eq.mpr, congrArg, ite_eq_right, Eq.refl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P6.slideStrat_of_lt line 326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LE.le, OfNat.ofNat, LT.lt, List, Usa2016P6.Observation, HAdd.hAdd, List.length, HMul.hMul, Eq, Finset, Fin, Usa2016P6.slideStrat, Usa2016P6.window
Proof uses: id, Eq.mpr, ite, dite, Exists, HSub.hSub, And, Ne, Usa2016P6.labelAt, Usa2016P6.pairSet, le_of_lt, Exists.choose, Not, congrArg, ite_eq_left, Eq.refl
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P6.slideStrat_of_ge line 332 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LE.le, OfNat.ofNat, LT.lt, List, Usa2016P6.Observation, HMul.hMul, HAdd.hAdd, List.length, Exists, Fin, HSub.hSub, And, Ne, Eq, Usa2016P6.labelAt, Finset, Usa2016P6.slideStrat, Usa2016P6.pairSet and 4 more
Proof uses: id, Eq.mpr, ite, Usa2016P6.window, dite, Not, congrArg, ite_eq_right, dite_eq_left, Eq.refl
34 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P6.slide_play_facts Facts about the play of the sliding strategy, while no win has occurred line 343 source
Source documentation
Facts about the play of the sliding strategy, while no win has occurred.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LE.le, OfNat.ofNat, LT.lt, Usa2016P6.Wizard, Usa2016P6.Wizard.Valid, Not, Eq, Bool, Usa2016P6.PlayState.won, Usa2016P6.play, Usa2016P6.slideStrat, HAdd.hAdd, HSub.hSub, HMul.hMul, Bool.true, And, Bool.false, List.length and 15 more
Proof uses: Nat.recAux, And.intro, rfl, Iff.mp, Ne, Bool.eq_false_iff, Usa2016P6.slideStrat_of_lt, Eq.mpr, id, congrArg, Eq.mp, Decidable.byContradiction, Usa2016P6.card_window, Usa2016P6.step, Usa2016P6.PlayState, Usa2016P6.play_succ, ite, Usa2016P6.PlayState.mk, Function.comp, Equiv.Perm and 25 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
```
lemma slide_play_facts {n k : ℕ} [NeZero n] (hk : 2 ≤ k) (hkn : k < n)
    (W : Wizard n) (_hW : W.Valid)
    (hM : ¬ (play (slideStrat n k hk hkn) W (2 * n - k + 1)).won)
    (j : ℕ) (hj : j ≤ 2 * n - k + 1) :
    (play (slideStrat n k hk hkn) W j).won = false ∧
    ((play (slideStrat n k hk hkn) W j).hist).length = j ∧
    (∀ i (_hi : i < j), ((play (slideStrat n k hk hkn) W j).hist)[i]? =
      some (window n k i, reveal ((play (slideStrat n k hk hkn) W i).arr) (window n k i))) ∧
    (∀ j' (_hj' : j' < j),
      ((window n k j').image (play (slideStrat n k hk hkn) W j').arr).card = k) := by
…
```
Mentions: Usa2016P6.Wizard, Usa2016P6.play, Usa2016P6.slideStrat, Usa2016P6.window, Usa2016P6.reveal
lemma Usa2016P6.slide_arr_step The arrangement one step later, while no win has occurred line 399 source
Source documentation
The arrangement one step later, while no win has occurred.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LE.le, OfNat.ofNat, LT.lt, Usa2016P6.Wizard, Usa2016P6.Wizard.Valid, Not, Eq, Bool, Usa2016P6.PlayState.won, Usa2016P6.play, Usa2016P6.slideStrat, HAdd.hAdd, HSub.hSub, HMul.hMul, Bool.true, Usa2016P6.Arrangement, Usa2016P6.PlayState.arr, Function.comp and 5 more
Proof uses: Bool.false, And.left, And, List.length, Usa2016P6.Observation, Option, GetElem?.getElem?, List, Option.some, Prod, Finset, Prod.mk, Usa2016P6.reveal, Finset.card, Finset.image, Usa2016P6.slide_play_facts, And.right, Nat.lt_succ_self, Usa2016P6.slideStrat_of_lt, Eq.mpr and 18 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma slide_arr_step {n k : ℕ} [NeZero n] (hk : 2 ≤ k) (hkn : k < n)
    (W : Wizard n) (hW : W.Valid)
    (hM : ¬ (play (slideStrat n k hk hkn) W (2 * n - k + 1)).won)
    (j : ℕ) (hj : j < 2 * n - k + 1) :
    (play (slideStrat n k hk hkn) W (j + 1)).arr =
      (play (slideStrat n k hk hkn) W j).arr ∘
        W.perm (play (slideStrat n k hk hkn) W j).hist (window n k j) := by
…
```
Mentions: Usa2016P6.Wizard, Usa2016P6.play, Usa2016P6.slideStrat, Usa2016P6.window
lemma Usa2016P6.slide_arr_frozen Once determined, the label at position x never changes again line 421 source
Source documentation
Once determined, the label at position x never changes again.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LE.le, OfNat.ofNat, LT.lt, Usa2016P6.Wizard, Usa2016P6.Wizard.Valid, Not, Eq, Bool, Usa2016P6.PlayState.won, Usa2016P6.play, Usa2016P6.slideStrat, HAdd.hAdd, HSub.hSub, HMul.hMul, Bool.true, Fin, Usa2016P6.PlayState.arr
Proof uses: Nat.le.rec, Eq.refl, Nat.le, Nat.succ, Eq.mpr, id, congrArg, Nat.succ_eq_add_one, Usa2016P6.Arrangement, Function.comp, Equiv.Perm, Usa2016P6.Wizard.perm, Usa2016P6.PlayState.hist, Usa2016P6.window, Usa2016P6.slide_arr_step, Eq.mp, And.right, Usa2016P6.Arrangement.Valid, Usa2016P6.Wizard.init, List and 7 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma slide_arr_frozen {n k : ℕ} [NeZero n] (hk : 2 ≤ k) (hkn : k < n)
    (W : Wizard n) (hW : W.Valid)
    (hM : ¬ (play (slideStrat n k hk hkn) W (2 * n - k + 1)).won)
    (x : Fin (2 * n)) (hx : x.val < 2 * n - k)
    (j : ℕ) (hj1 : x.val + 1 ≤ j) (hj2 : j ≤ 2 * n - k + 1) :
    (play (slideStrat n k hk hkn) W j).arr x =
      (play (slideStrat n k hk hkn) W (x.val + 1)).arr x := by
…
```
Mentions: Usa2016P6.Wizard, Usa2016P6.play, Usa2016P6.slideStrat
lemma Usa2016P6.slide_labelAt_eq The label computed from the observations is the actual label line 446 source
Source documentation
The label computed from the observations is the actual label.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LE.le, OfNat.ofNat, LT.lt, Usa2016P6.Wizard, Usa2016P6.Wizard.Valid, Not, Eq, Bool, Usa2016P6.PlayState.won, Usa2016P6.play, Usa2016P6.slideStrat, HAdd.hAdd, HSub.hSub, HMul.hMul, Bool.true, Fin, Usa2016P6.labelAt, Usa2016P6.PlayState.hist and 1 more
Proof uses: Bool.false, And, List.length, Usa2016P6.Observation, Option, GetElem?.getElem?, List, Option.some, Prod, Finset, Prod.mk, Usa2016P6.window, Usa2016P6.reveal, Finset.card, Finset.image, Usa2016P6.slide_play_facts, le_refl, Eq.mpr, id, congrArg and 58 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 74 steps
Open to load the checked before-and-after goal states.
```
lemma slide_labelAt_eq {n k : ℕ} [NeZero n] (hk : 2 ≤ k) (hkn : k < n)
    (W : Wizard n) (hW : W.Valid)
    (hM : ¬ (play (slideStrat n k hk hkn) W (2 * n - k + 1)).won)
    (x : Fin (2 * n)) (hx : x.val < 2 * n - k) :
    labelAt n k ((play (slideStrat n k hk hkn) W (2 * n - k + 1)).hist) x.val =
      (play (slideStrat n k hk hkn) W (x.val + 1)).arr x := by
…
```
Mentions: Usa2016P6.Wizard, Usa2016P6.play, Usa2016P6.slideStrat, Usa2016P6.labelAt
lemma Usa2016P6.slideStrat_wins The sliding strategy wins within 2n - k + 2 moves line 543 source
Source documentation
The sliding strategy wins within 2n - k + 2 moves.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LE.le, OfNat.ofNat, LT.lt, Usa2016P6.Wizard, Usa2016P6.Wizard.Valid, Eq, Bool, Usa2016P6.PlayState.won, Usa2016P6.play, Usa2016P6.slideStrat, HAdd.hAdd, HSub.hSub, HMul.hMul, Bool.true
Proof uses: dite, Usa2016P6.won_mono, Not, List.length, Usa2016P6.Observation, Usa2016P6.PlayState.hist, And.left, And, Option, GetElem?.getElem?, List, Option.some, Prod, Finset, Fin, Prod.mk, Usa2016P6.window, Usa2016P6.reveal, Usa2016P6.PlayState.arr, Finset.card and 50 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
```
lemma slideStrat_wins {n k : ℕ} [NeZero n] (hk : 2 ≤ k) (hkn : k < n)
    (W : Wizard n) (hW : W.Valid) :
    (play (slideStrat n k hk hkn) W (2 * n - k + 2)).won := by
…
```
Mentions: Usa2016P6.Wizard, Usa2016P6.play, Usa2016P6.slideStrat
lemma Usa2016P6.exists_perm_injOn line 608 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Eq, Finset.card, Finset.filter, Finset.univ, Finset, Set.InjOn, Exists, Equiv.Perm, And, Not, Membership.mem, Function.comp
Proof uses: Fintype.card, Fintype.card_fin, Eq.mpr, id, congrArg, Finset.card_univ, Eq.refl, Finset.image, Finset.eq_univ_of_card, Eq.trans, Iff.mpr, Finset.card_image_iff, Eq.symm, Compl.compl, propext, Finset.eq_univ_iff_forall, Finset.mem_univ, Iff.mp, Finset.mem_image, LT.lt and 54 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 206 steps (first 200 of 206)
Open to load the checked before-and-after goal states.
def Usa2016P6.initEquiv₁ The equivalence between the first query and the labels line 804 source
Source documentation
The equivalence between the first query and the labels.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, Equiv, Subtype, Fin, HMul.hMul, OfNat.ofNat, Membership.mem, Finset, List.nil, Usa2016P6.Observation
Proof uses: Fintype.equivOfCardEq
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def initEquiv₁ {n : ℕ} (σ : Strategy n) (hσ : σ.Valid n) : ↥(σ []) ≃ Fin n :=
…
```
Mentions: Usa2016P6.Strategy
def Usa2016P6.initEquiv₂ The equivalence between the complement of the first query and the labels line 808 source
Source documentation
The equivalence between the complement of the first query and the labels.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, Equiv, Subtype, Fin, HMul.hMul, OfNat.ofNat, Membership.mem, Finset, Compl.compl, List.nil, Usa2016P6.Observation
Proof uses: Fintype.equivOfCardEq
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def initEquiv₂ {n : ℕ} (σ : Strategy n) (hσ : σ.Valid n) : ↥(σ [])ᶜ ≃ Fin n :=
…
```
Mentions: Usa2016P6.Strategy
def Usa2016P6.initArr The wizard's initial arrangement: a bijection of each of σ [] and its complement onto the labels line 814 source
Source documentation
The wizard's initial arrangement: a bijection of each of σ [] and its complement onto the labels.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, Usa2016P6.Arrangement
Proof uses: Fin, HMul.hMul, OfNat.ofNat, dite, Membership.mem, Finset, List.nil, Usa2016P6.Observation, Equiv, Subtype, Usa2016P6.initEquiv₁, Subtype.mk, Not, Compl.compl, Usa2016P6.initEquiv₂
14 instances, coercions and auxiliary constants left out.
```
noncomputable def initArr {n : ℕ} (σ : Strategy n) (hσ : σ.Valid n) : Arrangement n :=
…
```
Mentions: Usa2016P6.Strategy, Usa2016P6.Arrangement
lemma Usa2016P6.initArr_apply_of_mem line 817 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, Fin, HMul.hMul, OfNat.ofNat, Membership.mem, Finset, List.nil, Usa2016P6.Observation, Eq, Usa2016P6.initArr, Equiv, Subtype, Usa2016P6.initEquiv₁, Subtype.mk
Proof uses: dite_eq_left, Not, Compl.compl, Usa2016P6.initEquiv₂
22 instances, coercions and auxiliary constants left out.
lemma Usa2016P6.initArr_apply_of_notMem line 820 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, Fin, HMul.hMul, OfNat.ofNat, Not, Membership.mem, Finset, List.nil, Usa2016P6.Observation, Eq, Usa2016P6.initArr, Equiv, Subtype, Compl.compl, Usa2016P6.initEquiv₂, Subtype.mk, Iff.mpr, Finset.mem_compl
Proof uses: dite_eq_right, Usa2016P6.initEquiv₁
26 instances, coercions and auxiliary constants left out.
lemma Usa2016P6.initArr_valid line 823 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, Usa2016P6.Arrangement.Valid, Usa2016P6.initArr
Proof uses: Fin, Eq, Finset, HMul.hMul, OfNat.ofNat, Finset.filter, Finset.univ, Insert.insert, Membership.mem, List.nil, Usa2016P6.Observation, Equiv, Subtype, Equiv.symm, Usa2016P6.initEquiv₁, Singleton.singleton, Compl.compl, Usa2016P6.initEquiv₂, Finset.ext, Eq.mpr and 35 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P6.initArr_injOn line 864 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, And, Set.InjOn, Fin, HMul.hMul, OfNat.ofNat, Usa2016P6.initArr, Finset, List.nil, Usa2016P6.Observation, Compl.compl
Proof uses: And.intro, Membership.mem, Set, Eq, congrArg, Subtype, Subtype.mk, Iff.mp, Finset.mem_coe, Equiv.injective, Usa2016P6.initEquiv₁, Eq.mp, Equiv, Usa2016P6.initArr_apply_of_mem, Iff.mpr, Not, Finset.mem_compl, Usa2016P6.initEquiv₂, Usa2016P6.initArr_apply_of_notMem
24 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def Usa2016P6.permOf The permutation the wizard uses in response to the query σ l: it keeps the next query free of matches line 877 source
Source documentation
The permutation the wizard uses in response to the query σ l: it keeps the next query free of matches.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, List, Usa2016P6.Observation, Usa2016P6.Arrangement, Equiv.Perm, Fin, HMul.hMul, OfNat.ofNat
Proof uses: dite, Exists, And, Not, Membership.mem, Finset, Eq, Set.InjOn, Function.comp, HAppend.hAppend, Prod, Option, List.cons, Prod.mk, Usa2016P6.reveal, List.nil, Exists.choose
26 instances, coercions and auxiliary constants left out.
```
noncomputable def permOf {n : ℕ} (σ : Strategy n) (_hσ : σ.Valid n)
    (l : List (Observation n)) (a : Arrangement n) : Equiv.Perm (Fin (2 * n)) :=
…
```
Mentions: Usa2016P6.Strategy, Usa2016P6.Observation, Usa2016P6.Arrangement
def Usa2016P6.wizArrAux Auxiliary for wizArr, recursing on the reversed history line 885 source
Source documentation
Auxiliary for wizArr, recursing on the reversed history.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, List, Usa2016P6.Observation, Usa2016P6.Arrangement
2 instances, coercions and auxiliary constants left out.
```
noncomputable def wizArrAux {n : ℕ} (σ : Strategy n) (hσ : σ.Valid n) :
    List (Observation n) → Arrangement n
  | [] => initArr σ hσ
  | _ :: r => wizArrAux σ hσ r ∘ permOf σ hσ r.reverse (wizArrAux σ hσ r)

/-- The arrangement after the given history, when the wizard plays `permOf`. -/
```
Mentions: Usa2016P6.Strategy, Usa2016P6.Observation, Usa2016P6.Arrangement, Usa2016P6.initArr, Usa2016P6.permOf
def Usa2016P6.wizArr The arrangement after the given history, when the wizard plays permOf line 891 source
Source documentation
The arrangement after the given history, when the wizard plays permOf.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, List, Usa2016P6.Observation, Usa2016P6.Arrangement
Proof uses: Usa2016P6.wizArrAux, List.reverse
```
noncomputable def wizArr {n : ℕ} (σ : Strategy n) (hσ : σ.Valid n)
    (l : List (Observation n)) : Arrangement n :=
…
```
Mentions: Usa2016P6.Strategy, Usa2016P6.Observation, Usa2016P6.Arrangement
lemma Usa2016P6.wizArr_nil line 895 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, Eq, Usa2016P6.Arrangement, Usa2016P6.wizArr, List.nil, Usa2016P6.Observation, Usa2016P6.initArr
Proof uses: rfl
lemma Usa2016P6.wizArr_append line 898 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, List, Usa2016P6.Observation, Eq, Usa2016P6.Arrangement, Usa2016P6.wizArr, HAppend.hAppend, List.cons, List.nil, Function.comp, Fin, HMul.hMul, OfNat.ofNat, Equiv.Perm, Usa2016P6.permOf
Proof uses: of_eq_true, Usa2016P6.wizArrAux, List.reverse, Eq.trans, True, congrFun', congrArg, List.reverse_append, List.reverse_singleton, Usa2016P6.wizArrAux.eq_2, Usa2016P6.permOf.congr_simp, Eq.refl, List.reverse_reverse, eq_self
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Usa2016P6.evasiveWizard The wizard that evades the player forever when k = n line 905 source
Source documentation
The wizard that evades the player forever when k = n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, Usa2016P6.Wizard
Proof uses: Usa2016P6.Wizard.mk, Usa2016P6.initArr, List, Usa2016P6.Observation, Finset, Fin, HMul.hMul, OfNat.ofNat, ite, Equiv.Perm, Eq, Usa2016P6.permOf, Usa2016P6.wizArr
7 instances, coercions and auxiliary constants left out.
```
noncomputable def evasiveWizard {n : ℕ} (σ : Strategy n) (hσ : σ.Valid n) : Wizard n where
…
```
Mentions: Usa2016P6.Strategy, Usa2016P6.Wizard
lemma Usa2016P6.evasiveWizard_valid line 909 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, Usa2016P6.Wizard.Valid, Usa2016P6.evasiveWizard
Proof uses: And.intro, Usa2016P6.Arrangement.Valid, Usa2016P6.Wizard.init, List, Usa2016P6.Observation, Finset, Fin, HMul.hMul, OfNat.ofNat, Not, Membership.mem, Eq, Equiv.Perm, Usa2016P6.Wizard.perm, Usa2016P6.initArr_valid, id, Decidable, ite, Usa2016P6.permOf, Usa2016P6.wizArr and 24 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
def Usa2016P6.evasiveHist The history after j rounds against the evasive wizard line 926 source
Source documentation
The history after j rounds against the evasive wizard.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, List, Usa2016P6.Observation
2 instances, coercions and auxiliary constants left out.
```
noncomputable def evasiveHist {n : ℕ} (σ : Strategy n) (hσ : σ.Valid n) :
    ℕ → List (Observation n)
  | 0 => []
  | j + 1 => evasiveHist σ hσ j ++
      [(σ (evasiveHist σ hσ j), reveal (wizArr σ hσ (evasiveHist σ hσ j))
        (σ (evasiveHist σ hσ j)))]

/-- The invariant maintained by the evasive wizard: the current arrangement is
valid, and injective both on the last query and on the next query. -/
```
Mentions: Usa2016P6.Strategy, Usa2016P6.Observation, Usa2016P6.reveal, Usa2016P6.wizArr
lemma Usa2016P6.evasive_inv The invariant maintained by the evasive wizard: the current arrangement is valid, and injective both on the last query and on the next query line 935 source
Source documentation
The invariant maintained by the evasive wizard: the current arrangement is valid, and injective both on the last query and on the next query.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, And, Usa2016P6.Arrangement.Valid, Usa2016P6.wizArr, Usa2016P6.evasiveHist, Set.InjOn, Fin, HMul.hMul, OfNat.ofNat, Finset, List.dropLast, Usa2016P6.Observation
Proof uses: Nat.recAux, And.intro, Usa2016P6.initArr_valid, And.left, Usa2016P6.initArr, List.nil, Compl.compl, Usa2016P6.initArr_injOn, HAdd.hAdd, List, Eq, rfl, Usa2016P6.Arrangement, HAppend.hAppend, Prod, Option, List.cons, Prod.mk, Usa2016P6.reveal, Function.comp and 51 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
lemma evasive_inv {n : ℕ} (σ : Strategy n) (hσ : σ.Valid n) (j : ℕ) :
    (wizArr σ hσ (evasiveHist σ hσ j)).Valid ∧
    Set.InjOn (wizArr σ hσ (evasiveHist σ hσ j)) ↑(σ ((evasiveHist σ hσ j).dropLast)) ∧
    Set.InjOn (wizArr σ hσ (evasiveHist σ hσ j)) ↑(σ (evasiveHist σ hσ j)) := by
…
```
Mentions: Usa2016P6.Strategy, Usa2016P6.wizArr, Usa2016P6.evasiveHist
lemma Usa2016P6.evasive_play Playing against the evasive wizard, the player never wins line 979 source
Source documentation
Playing against the evasive wizard, the player never wins.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, Eq, Usa2016P6.PlayState, Usa2016P6.play, Usa2016P6.evasiveWizard, Usa2016P6.PlayState.mk, Usa2016P6.wizArr, Usa2016P6.evasiveHist, Bool.false
Proof uses: Nat.recAux, Eq.refl, OfNat.ofNat, Set.InjOn, Fin, HMul.hMul, Finset, And.right, List.dropLast, Usa2016P6.Observation, Usa2016P6.Arrangement.Valid, And, Usa2016P6.evasive_inv, Eq.mpr, HAdd.hAdd, Usa2016P6.step, id, congrArg, Usa2016P6.play_succ, ite and 33 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma evasive_play {n : ℕ} (σ : Strategy n) (hσ : σ.Valid n) (m : ℕ) :
    play σ (evasiveWizard σ hσ) m =
      { arr := wizArr σ hσ (evasiveHist σ hσ m)
…
```
Mentions: Usa2016P6.Strategy, Usa2016P6.play, Usa2016P6.evasiveWizard, Usa2016P6.wizArr, Usa2016P6.evasiveHist
lemma Usa2016P6.not_winnable_of_eq When k = n, no strategy can guarantee a win: the game is not winnable line 1000 source
Source documentation
When k = n, no strategy can guarantee a win: the game is not winnable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, Exists, Usa2016P6.Wizard, And, Usa2016P6.Wizard.Valid, Eq, Bool, Usa2016P6.PlayState.won, Usa2016P6.play, Bool.false
Proof uses: Exists.intro, Usa2016P6.evasiveWizard, And.intro, Usa2016P6.evasiveWizard_valid, Eq.mpr, Usa2016P6.PlayState.mk, Usa2016P6.wizArr, Usa2016P6.evasiveHist, id, congrArg, Usa2016P6.PlayState, Usa2016P6.evasive_play, Eq.refl

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma not_winnable_of_eq {n : ℕ} (σ : Strategy n) (hσ : σ.Valid n) :
    ∃ W : Wizard n, W.Valid ∧ ∀ m, (play σ W m).won = false :=
…
```
Mentions: Usa2016P6.Strategy, Usa2016P6.Wizard, Usa2016P6.play
determine Usa2016P6.answer line 1006 source
no axioms what this means
Statement uses: Nat
Proof uses: LT.lt
1 instances, coercions and auxiliary constants left out.
problem Usa2016P6.usa2016_p6 line 1008 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Iff, Usa2016P6.Winnable, Usa2016P6.answer
Proof uses: id, Iff.intro, LT.lt, And, GE.ge, Exists, Usa2016P6.Strategy, Usa2016P6.Strategy.Valid, Usa2016P6.Wizard, Usa2016P6.Wizard.Valid, Eq, Bool, Usa2016P6.PlayState.won, Usa2016P6.play, Bool.true, Decidable.byContradiction, Not, False, Bool.false, Usa2016P6.not_winnable_of_eq and 13 more
22 instances, coercions and auxiliary constants left out.

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