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

75 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2012, Problem 3

The liar's guessing game is a game played between two players A and B. The rules of the game depend on two fixed positive integers k and n which are known to both players.

At the start of the game A chooses integers x and N with 1 ≤ x ≤ N. Player A keeps x secret, and truthfully tells N to player B. Player B now tries to obtain information about x by asking player A questions as follows: each question consists of B specifying an arbitrary set S of positive integers (possibly one specified in some previous question), and asking A whether x belongs to S. Player B may ask as many questions as he wishes. After each question, player A must immediately answer it with yes or no, but is allowed to lie as many times as she wants; the only restriction is that, among any k + 1 consecutive answers, at least one answer must be truthful.

After B has asked as many questions as he wants, he must specify a set X of at most n positive integers. If x belongs to X, then B wins; otherwise, he loses. Prove that:

(a) If n ≥ 2^k, then B can guarantee a win.

(b) For all sufficiently large k, there exists an integer n ≥ (1.99)^k such that B cannot guarantee a win.

Imports (5)

Imported by 1 file

Compfiles.lean

inductive Imo2012P3.Move A move of player B: either stop and guess a set X, or ask whether x ∈ S line 61 source
Source documentation
A move of player B: either stop and guess a set X, or ask whether x ∈ S.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat
```
inductive Move (N : ℕ) where
…
```
structure Imo2012P3.Strategy A strategy for player B: from the list of answers so far (in chronological order), decide the next move line 67 source
Source documentation
A strategy for player B: from the list of answers so far (in chronological order), decide the next move.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat
```
structure Strategy (N : ℕ) where
…
```
def Imo2012P3.hist The answer history after t questions, when player A answers according to ans line 72 source
Source documentation
The answer history after t questions, when player A answers according to ans.

no axioms what this means
Statement uses: Nat, Bool, List
2 instances, coercions and auxiliary constants left out.
```
def hist (ans : ℕ → Bool) : ℕ → List Bool
  | 0 => []
  | t + 1 => hist ans t ++ [ans t]

/-- The `i`-th answer is truthful for the secret `x`: it matches the truth value
of `x ∈ S`, where `S` is the question B asked at that point. (If B guessed instead
of asking, the answer is vacuously truthful.) -/
```
Mentions: answer, S
def Imo2012P3.TruthfulAt The i-th answer is truthful for the secret x: it matches the truth value of x ∈ S, where S is the question B asked at that point line 79 source
Source documentation
The i-th answer is truthful for the secret x: it matches the truth value of x ∈ S, where S is the question B asked at that point. (If B guessed instead of asking, the answer is vacuously truthful.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, Fin, Bool
Proof uses: Finset, Eq, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.hist, Imo2012P3.Move.ask, Iff, Membership.mem, Bool.true
2 instances, coercions and auxiliary constants left out.
```
def TruthfulAt {N : ℕ} (σ : Strategy N) (x : Fin N) (ans : ℕ → Bool) (i : ℕ) : Prop :=
…
```
Mentions: Imo2012P3.Strategy
def Imo2012P3.ConsistentUpTo The play is consistent with the secret x up to time T: among any k + 1 consecutive answers within the first T, at least one is truthful line 84 source
Source documentation
The play is consistent with the secret x up to time T: among any k + 1 consecutive answers within the first T, at least one is truthful.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, Fin, Bool
Proof uses: LE.le, HAdd.hAdd, OfNat.ofNat, Exists, And, Imo2012P3.TruthfulAt
4 instances, coercions and auxiliary constants left out.
```
def ConsistentUpTo (k : ℕ) {N : ℕ} (σ : Strategy N) (x : Fin N) (ans : ℕ → Bool)
    (T : ℕ) : Prop :=
…
```
Mentions: Imo2012P3.Strategy
def Imo2012P3.GuaranteesWin Player B's strategy σ guarantees a win if 1 line 93 source
Source documentation
Player B's strategy σ guarantees a win if
1. against any answer sequence that stays consistent with x forever, B eventually stops and guesses, and
2. whenever B guesses X at time T and the answers given so far are consistent with x, then x ∈ X and X has at most n elements.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy
Proof uses: And, Fin, Bool, Imo2012P3.ConsistentUpTo, Exists, Finset, Eq, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.hist, Imo2012P3.Move.guess, Membership.mem, LE.le, Finset.card
3 instances, coercions and auxiliary constants left out.
```
def GuaranteesWin (k n : ℕ) {N : ℕ} (σ : Strategy N) : Prop :=
…
```
Mentions: Imo2012P3.Strategy
def Imo2012P3.BobWins Player B can guarantee a win with parameters k, n when player A's bound is N line 102 source
Source documentation
Player B can guarantee a win with parameters k, n when player A's bound is N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Exists, Imo2012P3.Strategy, Imo2012P3.GuaranteesWin
```
def BobWins (k n N : ℕ) : Prop :=
…
```
def Imo2012P3.weightBase The base of the weights used by A's counter-strategy line 127 source
Source documentation
The base of the weights used by A's counter-strategy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: OfScientific.ofScientific, Bool.true
2 instances, coercions and auxiliary constants left out.
```
def weightBase : ℝ := 1.998
```
lemma Imo2012P3.one_lt_weightBase line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LT.lt, Real, OfNat.ofNat, Imo2012P3.weightBase
Proof uses: of_eq_true, Eq.trans, HDiv.hDiv, Mathlib.Meta.NormNum.instAtLeastTwo, True, congrArg, Mathlib.Meta.NormNum.IsNNRat.to_eq, OfScientific.ofScientific, Bool.true, Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true, Mathlib.Meta.NormNum.isNNRat_nnratCast, NNRat.divNat, HPow.hPow, Nat, Mathlib.Meta.NormNum.isNNRat_divNat, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run and 14 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2012P3.alicePlay A's counterplay against σ: after each answer she records, for every candidate, the length of its current run of consecutive lies line 136 source
Source documentation
A's counterplay against σ: after each answer she records, for every candidate, the length of its current run of consecutive lies. Given a question, she chooses the side with smaller total weight as the "bad set" and answers that x lies on the other side. The third component is the answer given at that step. (Once B guesses, the streaks are frozen and the answers are junk.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, Prod, Fin, List, Bool
2 instances, coercions and auxiliary constants left out.
```
def alicePlay (σ : Strategy N) : ℕ → (Fin N → ℕ) × List Bool × Bool
  | 0 => (fun _ => 0, [], true)
  | t + 1 =>
    match σ.move (alicePlay σ t).2.1 with
    | Move.guess _ => ((alicePlay σ t).1, (alicePlay σ t).2.1 ++ [true], true)
    | Move.ask S =>
      if ∑ x ∈ S, weightBase ^ ((alicePlay σ t).1 x) ≤
          ∑ x ∈ Sᶜ, weightBase ^ ((alicePlay σ t).1 x) then
        (fun x => if x ∈ S then (alicePlay σ t).1 x + 1 else 0,
          (alicePlay σ t).2.1 ++ [false], false)
      else
        (fun x => if x ∉ S then (alicePlay σ t).1 x + 1 else 0,
…
```
Mentions: Imo2012P3.Strategy, S, Imo2012P3.weightBase
def Imo2012P3.aliceStreak The streak (length of the current run of consecutive lies) of each candidate after t answers of A's counterplay line 152 source
Source documentation
The streak (length of the current run of consecutive lies) of each candidate after t answers of A's counterplay.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, Fin
Proof uses: Prod.fst, Prod, List, Bool, Imo2012P3.alicePlay
```
def aliceStreak (σ : Strategy N) (t : ℕ) : Fin N → ℕ := (alicePlay σ t).1
```
Mentions: Imo2012P3.Strategy, Imo2012P3.alicePlay
def Imo2012P3.aliceHist The answer history of A's counterplay after t steps line 155 source
Source documentation
The answer history of A's counterplay after t steps.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, List, Bool
Proof uses: Prod.fst, Prod.snd, Fin, Prod, Imo2012P3.alicePlay
```
def aliceHist (σ : Strategy N) (t : ℕ) : List Bool := (alicePlay σ t).2.1
```
Mentions: Imo2012P3.Strategy, Imo2012P3.alicePlay
def Imo2012P3.aliceAns The t-th answer of A's counterplay line 158 source
Source documentation
The t-th answer of A's counterplay.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, Bool
Proof uses: Prod.snd, List, Fin, Prod, Imo2012P3.alicePlay, HAdd.hAdd, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
def aliceAns (σ : Strategy N) (t : ℕ) : Bool := (alicePlay σ (t + 1)).2.2
```
Mentions: Imo2012P3.Strategy, Imo2012P3.alicePlay
def Imo2012P3.aliceWeight The total weight after t answers line 161 source
Source documentation
The total weight after t answers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, Real
Proof uses: Finset.sum, Fin, Finset.univ, HPow.hPow, Imo2012P3.weightBase, Imo2012P3.aliceStreak
6 instances, coercions and auxiliary constants left out.
```
def aliceWeight (σ : Strategy N) (t : ℕ) : ℝ := ∑ x, weightBase ^ (aliceStreak σ t x)
```
Mentions: Imo2012P3.Strategy, Imo2012P3.weightBase, Imo2012P3.aliceStreak
lemma Imo2012P3.alicePlay_guess line 163 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, Finset, Fin, Eq, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.aliceHist, Imo2012P3.Move.guess, Prod, List, Bool, Imo2012P3.alicePlay, HAdd.hAdd, OfNat.ofNat, Prod.mk, Imo2012P3.aliceStreak, HAppend.hAppend, List.cons, Bool.true and 1 more
Proof uses: Prod.fst, Prod.snd, Eq.mpr, Imo2012P3.alicePlay.match_1, ite, LE.le, Real, Finset.sum, HPow.hPow, Imo2012P3.weightBase, Compl.compl, Membership.mem, Bool.false, Not, id, Eq.rec, Eq.refl, Eq.trans, Nat.succ, congrArg and 1 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.aliceStreak_guess line 171 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, Finset, Fin, Eq, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.aliceHist, Imo2012P3.Move.guess, Imo2012P3.aliceStreak, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, Prod.fst, Prod, List, Bool, Imo2012P3.alicePlay, id, congrArg, rfl, Prod.mk, HAppend.hAppend, List.cons, Bool.true, List.nil, Imo2012P3.alicePlay_guess, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.alicePlay_ask line 176 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, Finset, Fin, Eq, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.aliceHist, Imo2012P3.Move.ask, Prod, List, Bool, Imo2012P3.alicePlay, HAdd.hAdd, OfNat.ofNat, ite, LE.le, Real, Finset.sum, HPow.hPow and 11 more
Proof uses: Prod.fst, Prod.snd, Eq.mpr, Imo2012P3.alicePlay.match_1, id, Eq.rec, Eq.refl, Eq.trans, Nat.succ, congrArg, Imo2012P3.alicePlay.eq_2
40 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.aliceHist_succ line 190 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, Eq, List, Bool, Imo2012P3.aliceHist, HAdd.hAdd, OfNat.ofNat, HAppend.hAppend, List.cons, Imo2012P3.aliceAns, List.nil
Proof uses: Imo2012P3.Move, Imo2012P3.Strategy.move, Finset, Fin, Imo2012P3.Move.guess, Eq.mpr, Prod.fst, Prod.snd, Prod, Imo2012P3.alicePlay, id, congrArg, rfl, Prod.mk, Imo2012P3.aliceStreak, Bool.true, Imo2012P3.alicePlay_guess, Eq.refl, Eq.symm, Imo2012P3.Move.ask and 16 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.aliceHist_eq_hist line 201 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, Eq, List, Bool, Imo2012P3.aliceHist, Imo2012P3.hist, Imo2012P3.aliceAns
Proof uses: Nat.recAux, Eq.refl, OfNat.ofNat, Eq.mpr, HAdd.hAdd, HAppend.hAppend, List.cons, List.nil, id, congrArg, Nat.succ, Imo2012P3.hist.eq_2, Eq.symm, Imo2012P3.aliceHist_succ
5 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.aliceWeight_step_ask At an ask-step, the new total weight is at most weightBase / 2 times the old weight plus N line 209 source
Source documentation
At an ask-step, the new total weight is at most weightBase / 2 times the old weight plus N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, Finset, Fin, Eq, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.aliceHist, Imo2012P3.Move.ask, LE.le, Real, Imo2012P3.aliceWeight, HAdd.hAdd, OfNat.ofNat, HMul.hMul, HDiv.hDiv, Imo2012P3.weightBase
Proof uses: le_of_lt, of_eq_true, LT.lt, Eq.trans, Mathlib.Meta.NormNum.instAtLeastTwo, True, congrArg, Mathlib.Meta.NormNum.IsNNRat.to_eq, OfScientific.ofScientific, Bool.true, Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true, Mathlib.Meta.NormNum.isNNRat_nnratCast, NNRat.divNat, HPow.hPow, Mathlib.Meta.NormNum.isNNRat_divNat, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run and 124 more
153 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
lemma aliceWeight_step_ask {σ : Strategy N} {t : ℕ} {S : Finset (Fin N)}
    (h : σ.move (aliceHist σ t) = Move.ask S) :
    aliceWeight σ (t + 1) ≤ weightBase / 2 * aliceWeight σ t + N := by
…
```
Mentions: Imo2012P3.Strategy, S, h, Imo2012P3.aliceHist, Imo2012P3.aliceWeight, Imo2012P3.weightBase
lemma Imo2012P3.aliceWeight_le The total weight never exceeds 1000 * N line 267 source
Source documentation
The total weight never exceeds 1000 * N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, LE.le, Real, Imo2012P3.aliceWeight, HMul.hMul, OfNat.ofNat
Proof uses: Nat.recAux, Eq, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.sum, Fin, Finset.univ, HPow.hPow, Imo2012P3.weightBase, Imo2012P3.aliceStreak, HSMul.hSMul, Finset.card, funext, pow_zero, Finset.sum_const, Fintype.card_fin, nsmul_eq_mul and 127 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma aliceWeight_le (σ : Strategy N) (t : ℕ) : aliceWeight σ t ≤ 1000 * N := by
…
```
Mentions: Imo2012P3.Strategy, Imo2012P3.aliceWeight
lemma Imo2012P3.aliceStreak_le No candidate's streak ever reaches k + 1, once 1000 * N < (1.998) ^ (k+1) line 289 source
Source documentation
No candidate's streak ever reaches k + 1, once 1000 * N < (1.998) ^ (k+1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, LT.lt, Real, HMul.hMul, OfNat.ofNat, HPow.hPow, Imo2012P3.weightBase, HAdd.hAdd, Fin, LE.le, Imo2012P3.aliceStreak
Proof uses: Decidable.byContradiction, Not, Imo2012P3.aliceWeight, Finset.single_le_sum, Finset.univ, Membership.mem, Finset, pow_nonneg, of_eq_true, Eq.trans, HDiv.hDiv, Mathlib.Meta.NormNum.instAtLeastTwo, True, congrArg, Mathlib.Meta.NormNum.IsNNRat.to_eq, OfScientific.ofScientific, Bool.true, Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true, Mathlib.Meta.NormNum.isNNRat_nnratCast, NNRat.divNat and 86 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma aliceStreak_le (σ : Strategy N) {k : ℕ} (hWt : 1000 * (N : ℝ) < weightBase ^ (k + 1))
    (x : Fin N) (t : ℕ) :
    aliceStreak σ t x ≤ k := by
…
```
Mentions: Imo2012P3.Strategy, Imo2012P3.weightBase, Imo2012P3.aliceStreak
lemma Imo2012P3.alice_lie_streak If A's i-th answer is a lie for x, then x's streak increases by one line 303 source
Source documentation
If A's i-th answer is a lie for x, then x's streak increases by one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, Fin, Not, Imo2012P3.TruthfulAt, Imo2012P3.aliceAns, Eq, Imo2012P3.aliceStreak, HAdd.hAdd, OfNat.ofNat
Proof uses: Finset, And, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.aliceHist, Imo2012P3.Move.ask, Or, Membership.mem, Ne, Bool, Bool.true, Exists, Eq.mp, Iff, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, Imo2012P3.hist, List and 39 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma alice_lie_streak {σ : Strategy N} {x : Fin N} {i : ℕ}
    (h : ¬ TruthfulAt σ x (aliceAns σ) i) :
    aliceStreak σ (i + 1) x = aliceStreak σ i x + 1 := by
…
```
Mentions: Imo2012P3.Strategy, h, Imo2012P3.TruthfulAt, Imo2012P3.aliceAns, Imo2012P3.aliceStreak
lemma Imo2012P3.alice_consistent A's answer sequence is consistent with every candidate at all times: among any k + 1 consecutive answers, at least one is truthful for x line 339 source
Source documentation
A's answer sequence is consistent with every candidate at all times: among any k + 1 consecutive answers, at least one is truthful for x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy, LT.lt, Real, HMul.hMul, OfNat.ofNat, HPow.hPow, Imo2012P3.weightBase, HAdd.hAdd, Fin, Imo2012P3.ConsistentUpTo, Imo2012P3.aliceAns
Proof uses: LE.le, Classical.byContradiction, Exists, And, Imo2012P3.TruthfulAt, Not, Imo2012P3.aliceStreak, Nat.recAux, of_eq_true, Eq.trans, True, implies_congr, Function.swap, congr, congrArg, add_zero, congrFun', Eq.mp, binderNameHint, forall_congr and 8 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma alice_consistent (σ : Strategy N) {k : ℕ}
    (hWt : 1000 * (N : ℝ) < weightBase ^ (k + 1))
    (x : Fin N) (T : ℕ) :
    ConsistentUpTo k σ x (aliceAns σ) T := by
…
```
Mentions: Imo2012P3.Strategy, Imo2012P3.weightBase, Imo2012P3.ConsistentUpTo, Imo2012P3.aliceAns
lemma Imo2012P3.aliceWeightBase_bound The weight bound needed at N = n + 1 where n = ⌈(1.99) ^ k⌉ line 363 source
Source documentation
The weight bound needed at N = n + 1 where n = ⌈(1.99) ^ k⌉.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Nat.ceil, Real, HPow.hPow, OfScientific.ofScientific, Bool.true, LT.lt, HMul.hMul, OfNat.ofNat, HAdd.hAdd, Imo2012P3.weightBase
Proof uses: LE.le, le_of_lt, pow_pos, Mathlib.Meta.Positivity.pos_of_isNNRat, Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true, Mathlib.Meta.NormNum.isNNRat_nnratCast, NNRat.divNat, Mathlib.Meta.NormNum.isNNRat_divNat, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit0, Mathlib.Meta.NormNum.isNNRat_div, NNRat, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_natCast and 102 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma aliceWeightBase_bound {k n : ℕ} (hn : n = ⌈(1.99 : ℝ) ^ k⌉₊)
    (h1000 : 1000 * ((1.99 : ℝ) ^ k + 2) < weightBase ^ (k + 1)) :
    1000 * ((n + 1 : ℕ) : ℝ) < weightBase ^ (k + 1) := by
…
```
Mentions: Imo2012P3.weightBase
lemma Imo2012P3.not_bobWins Under the weight bound, B has no winning strategy: A's counterplay is consistent with every candidate at all times, so B can never stop with a correct guess of size at most n line 378 source
Source documentation
Under the weight bound, B has no winning strategy: A's counterplay is consistent with every candidate at all times, so B can never stop with a correct guess of size at most n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Real, HMul.hMul, OfNat.ofNat, HAdd.hAdd, HPow.hPow, Imo2012P3.weightBase, LE.le, Not, Imo2012P3.BobWins
Proof uses: Imo2012P3.Strategy, Imo2012P3.GuaranteesWin, False, Fin, Bool, Imo2012P3.ConsistentUpTo, Exists, Finset, Eq, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.hist, Imo2012P3.Move.guess, And, Membership.mem, Finset.card, Imo2012P3.aliceAns, Imo2012P3.alice_consistent, Fin.mk, Finset.univ and 8 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma not_bobWins {k n : ℕ} (hWt : 1000 * ((n + 1 : ℕ) : ℝ) < weightBase ^ (k + 1))
    (hN : 1 ≤ n + 1) :
    ¬ BobWins k n (n + 1) := by
…
```
Mentions: Imo2012P3.weightBase, Imo2012P3.BobWins
lemma Imo2012P3.one_le_pow_199 Helper: 1 ≤ (1.99) ^ k line 394 source
Source documentation
Helper: 1 ≤ (1.99) ^ k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, OfNat.ofNat, HPow.hPow, OfScientific.ofScientific, Bool.true
Proof uses: Nat.recAux, Mathlib.Meta.NormNum.isRat_le_true, Int.ofNat, Mathlib.Meta.NormNum.IsNNRat.to_isRat, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_pow, Eq.refl, Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true, Mathlib.Meta.NormNum.isNNRat_nnratCast, NNRat.divNat, Mathlib.Meta.NormNum.isNNRat_divNat, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit0, Mathlib.Meta.NormNum.isNNRat_div, NNRat, Mathlib.Meta.NormNum.isNNRat_mul and 14 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma one_le_pow_199 (k : ℕ) : (1 : ℝ) ≤ 1.99 ^ k := by
…
```
lemma Imo2012P3.exists_eventually_large For all sufficiently large k, 1000 * ((1.99) ^ k + 2) < (1.998) ^ (k + 1) line 402 source
Source documentation
For all sufficiently large k, 1000 * ((1.99) ^ k + 2) < (1.998) ^ (k + 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Nat, GE.ge, LT.lt, Real, HMul.hMul, OfNat.ofNat, HAdd.hAdd, HPow.hPow, OfScientific.ofScientific, Bool.true, Imo2012P3.weightBase
Proof uses: HDiv.hDiv, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true, Mathlib.Meta.NormNum.isNNRat_nnratCast, NNRat.divNat, Mathlib.Meta.NormNum.isNNRat_divNat, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit1, NNRat, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNNRat_inv_pos and 144 more
187 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma exists_eventually_large :
    ∃ k₀ : ℕ, ∀ k ≥ k₀, 1000 * ((1.99 : ℝ) ^ k + 2) < weightBase ^ (k + 1) := by
…
```
Mentions: Imo2012P3.weightBase
inductive Imo2012P3.BobPhase Documented declaration: BobPhase line 452 source
Source documentation
Bob's phase within the current elimination round: either probing with the singleton question (j consecutive "no" answers so far), or asking the bit questions after a "yes" (the probe phase took j answers, and bs are the bit answers so far).

no axioms what this means
```
inductive BobPhase where
…
```
structure Imo2012P3.BobState Bob's state: his current candidate pool together with the progress in the current elimination round line 458 source
Source documentation
Bob's state: his current candidate pool together with the progress in the current elimination round.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat
```
structure BobState (N : ℕ) where
…
```
lemma Imo2012P3.bobState_ext_iff line 462 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.BobState, Finset, Fin, Imo2012P3.BobPhase, Iff, Eq, Imo2012P3.BobState.mk, And, Imo2012P3.BobState.pool, Imo2012P3.BobState.phase
Proof uses: Iff.intro, Eq.mpr, id, congrArg, And.intro, rfl, of_eq_true, Eq.trans, True, congrFun', congr, eq_self, Eq.symm, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def Imo2012P3.BobPhase.answers The number of answers given so far in the current round line 473 source
Source documentation
The number of answers given so far in the current round.

no axioms what this means
Statement uses: Imo2012P3.BobPhase, Nat
Proof uses: Imo2012P3.BobPhase.answers.match_1, List, Bool, HAdd.hAdd, List.length
2 instances, coercions and auxiliary constants left out.
```
def BobPhase.answers : BobPhase → ℕ
  | probe j => j
  | bits j bs => j + bs.length

/-- An embedding of the `2 ^ k` bit patterns into the pool. -/
```
Mentions: Imo2012P3.BobPhase
def Imo2012P3.bobEmbedding An embedding of the 2 ^ k bit patterns into the pool line 478 source
Source documentation
An embedding of the 2 ^ k bit patterns into the pool.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HPow.hPow, OfNat.ofNat, Finset.card, Function.Embedding, Bool, Subtype, Membership.mem
Proof uses: Eq, Fintype.card, Function.Embedding.trans, Equiv.toEmbedding, Equiv.trans, Fintype.equivFin, finCongr, Fin.castLEEmb, RelEmbedding.toEmbedding, OrderIso.toOrderEmbedding, Finset.orderIsoOfFin
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def bobEmbedding (P : Finset (Fin N)) (h : 2 ^ k ≤ P.card) :
    (Fin k → Bool) ↪ P :=
…
```
Mentions: P, h
lemma Imo2012P3.bobEmbedding_mem line 485 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HPow.hPow, OfNat.ofNat, Finset.card, Bool, Membership.mem, Function.Embedding, Subtype, Imo2012P3.bobEmbedding
Proof uses: Subtype.property
21 instances, coercions and auxiliary constants left out.
lemma Imo2012P3.exists_special There is an element of the pool outside the image of the bit patterns line 490 source
Source documentation
There is an element of the pool outside the image of the bit patterns.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card, Exists, And, Membership.mem, Bool, Ne, Function.Embedding, Subtype, Imo2012P3.bobEmbedding
Proof uses: LT.lt, Finset.image, Finset.univ, Eq.mpr, id, Eq, congrArg, Finset.card_image_of_injective, Function.Embedding.injective, Subtype.coe_injective, Fintype.card, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, Fintype.card_fin, Decidable.byContradiction, Not, Eq.mp, Eq.trans, binderNameHint and 12 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma exists_special (P : Finset (Fin N)) (h : 2 ^ k + 1 ≤ P.card) :
    ∃ s ∈ P, ∀ p : Fin k → Bool, (bobEmbedding P (by lia) p : Fin N) ≠ s := by
…
```
Mentions: P, h, Imo2012P3.bobEmbedding
def Imo2012P3.bobSpecial The distinguished candidate asked about in the probe phase: an element of the pool outside the image of the bit patterns line 511 source
Source documentation
The distinguished candidate asked about in the probe phase: an element of the pool outside the image of the bit patterns.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card
Proof uses: Exists.choose, And, Membership.mem, Bool, Ne, Function.Embedding, Subtype, Imo2012P3.bobEmbedding, Imo2012P3.exists_special
22 instances, coercions and auxiliary constants left out.
```
noncomputable def bobSpecial (P : Finset (Fin N)) (h : 2 ^ k + 1 ≤ P.card) : Fin N :=
…
```
Mentions: P, h
lemma Imo2012P3.bobSpecial_mem line 514 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card, Membership.mem, Imo2012P3.bobSpecial
Proof uses: And.left, Exists.choose, And, Bool, Ne, Function.Embedding, Subtype, Imo2012P3.bobEmbedding, Imo2012P3.exists_special, Exists.choose_spec
24 instances, coercions and auxiliary constants left out.
lemma Imo2012P3.bobSpecial_ne_embedding line 517 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card, Bool, Ne, Membership.mem, Function.Embedding, Subtype, Imo2012P3.bobEmbedding, Imo2012P3.bobSpecial
Proof uses: And.right, Exists.choose, And, Imo2012P3.exists_special, Exists.choose_spec
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bobSpecial_congr line 522 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Eq, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card, Imo2012P3.bobSpecial, Eq.rec
Proof uses: Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bobEmbedding_congr line 527 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Eq, LE.le, HPow.hPow, OfNat.ofNat, Finset.card, Bool, Membership.mem, Function.Embedding, Subtype, Imo2012P3.bobEmbedding, Eq.rec
Proof uses: Eq.refl
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2012P3.bitQuestion The set of candidates whose i-th bit is 1 line 534 source
Source documentation
The set of candidates whose i-th bit is 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HPow.hPow, OfNat.ofNat, Finset.card
Proof uses: Finset.image, Bool, Membership.mem, Function.Embedding, Subtype, Imo2012P3.bobEmbedding, Finset.filter, Eq, Bool.true, Finset.univ
22 instances, coercions and auxiliary constants left out.
```
noncomputable def bitQuestion (P : Finset (Fin N)) (h : 2 ^ k ≤ P.card) (i : Fin k) :
    Finset (Fin N) :=
…
```
Mentions: P, h
lemma Imo2012P3.mem_bitQuestion line 539 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HPow.hPow, OfNat.ofNat, Finset.card, Bool, Iff, Membership.mem, Imo2012P3.bitQuestion, Function.Embedding, Subtype, Imo2012P3.bobEmbedding, Eq, Bool.true
Proof uses: Iff.intro, And, Finset.filter, Finset.univ, Exists, Eq.mp, Finset.image, congrArg, propext, Finset.mem_image, Imo2012P3.bitQuestion.eq_1, Function.Embedding.injective, Subtype.coe_injective, And.right, Finset.mem_filter, Eq.mpr, id, Exists.intro, And.intro, Iff.mpr and 2 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
def Imo2012P3.bobQuestion Bob's question in a given phase: the singleton {special} when probing, the |bs|-th bit question in the bit phase line 556 source
Source documentation
Bob's question in a given phase: the singleton {special} when probing, the |bs|-th bit question in the bit phase.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card, Imo2012P3.BobPhase
Proof uses: Imo2012P3.BobPhase.answers.match_1, Singleton.singleton, Imo2012P3.bobSpecial, List, Bool, dite, LT.lt, List.length, Imo2012P3.bitQuestion, Fin.mk, Not, EmptyCollection.emptyCollection
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def bobQuestion (P : Finset (Fin N)) (h : 2 ^ k + 1 ≤ P.card) :
    BobPhase → Finset (Fin N)
  | BobPhase.probe _ => {bobSpecial P h}
  | BobPhase.bits _ bs =>
    if hb : bs.length < k then bitQuestion P (by lia) ⟨bs.length, hb⟩ else ∅
```
Mentions: P, h, Imo2012P3.BobPhase, Imo2012P3.bobSpecial, Imo2012P3.bitQuestion
lemma Imo2012P3.bobQuestion_probe line 562 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card, Eq, Imo2012P3.bobQuestion, Imo2012P3.BobPhase.probe, Singleton.singleton, Imo2012P3.bobSpecial
Proof uses: rfl
17 instances, coercions and auxiliary constants left out.
lemma Imo2012P3.bobQuestion_bits line 565 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card, List, Bool, LT.lt, List.length, Eq, Imo2012P3.bobQuestion, Imo2012P3.BobPhase.bits, Imo2012P3.bitQuestion, Fin.mk
Proof uses: id, dite_eq_left, Not, EmptyCollection.emptyCollection
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Imo2012P3.bobStepPhase One round-step of Bob's state machine, in the case 2 ^ k < P.card line 572 source
Source documentation
One round-step of Bob's state machine, in the case 2 ^ k < P.card.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card, Imo2012P3.BobPhase, Bool, Imo2012P3.BobState
Proof uses: Imo2012P3.BobPhase.answers.match_1, Imo2012P3.bobStepPhase.match_1, Unit, Imo2012P3.BobState.mk, Imo2012P3.BobPhase.bits, List.nil, ite, Eq, Finset.erase, Imo2012P3.bobSpecial, Imo2012P3.BobPhase.probe, List, HAppend.hAppend, List.cons, dite, List.length, Membership.mem, Function.Embedding, Subtype, Imo2012P3.bobEmbedding and 4 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def bobStepPhase (P : Finset (Fin N)) (h : 2 ^ k + 1 ≤ P.card)
    (ph : BobPhase) (a : Bool) : BobState N :=
…
```
Mentions: P, h, Imo2012P3.BobPhase, Imo2012P3.BobState
def Imo2012P3.bobStep One step of Bob's state machine line 590 source
Source documentation
One step of Bob's state machine. If the pool is already small enough, the state is frozen.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.BobState, Bool
Proof uses: dite, LE.le, Finset.card, Fin, Imo2012P3.BobState.pool, HPow.hPow, OfNat.ofNat, Not, Imo2012P3.bobStepPhase, Imo2012P3.BobState.phase
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def bobStep (k : ℕ) (s : BobState N) (a : Bool) : BobState N :=
…
```
Mentions: Imo2012P3.BobState
def Imo2012P3.bobStrategy Bob's winning strategy for part (a) line 595 source
Source documentation
Bob's winning strategy for part (a).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.Strategy
Proof uses: Imo2012P3.Strategy.mk, List, Bool, Imo2012P3.BobState, List.foldl, Imo2012P3.bobStep, Imo2012P3.BobState.mk, Finset.univ, Fin, Imo2012P3.BobPhase.probe, OfNat.ofNat, dite, Imo2012P3.Move, LE.le, Finset.card, Imo2012P3.BobState.pool, HPow.hPow, Imo2012P3.Move.guess, Not, Imo2012P3.Move.ask and 2 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def bobStrategy (k : ℕ) : Strategy N where
…
```
Mentions: Imo2012P3.Strategy
def Imo2012P3.bobStateOf Bob's state after processing the first t answers line 602 source
Source documentation
Bob's state after processing the first t answers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Imo2012P3.BobState
Proof uses: List.foldl, Imo2012P3.bobStep, Imo2012P3.BobState.mk, Finset.univ, Fin, Imo2012P3.BobPhase.probe, OfNat.ofNat, Imo2012P3.hist
2 instances, coercions and auxiliary constants left out.
```
def bobStateOf (N k : ℕ) (ans : ℕ → Bool) (t : ℕ) : BobState N :=
…
```
Mentions: Imo2012P3.BobState
lemma Imo2012P3.bobStateOf_zero line 605 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Eq, Imo2012P3.BobState, Imo2012P3.bobStateOf, OfNat.ofNat, Imo2012P3.BobState.mk, Finset.univ, Fin, Imo2012P3.BobPhase.probe
Proof uses: rfl
3 instances, coercions and auxiliary constants left out.
lemma Imo2012P3.bobStateOf_succ line 608 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Eq, Imo2012P3.BobState, Imo2012P3.bobStateOf, HAdd.hAdd, OfNat.ofNat, Imo2012P3.bobStep
Proof uses: id, Eq.mpr, List.foldl, Imo2012P3.BobState.mk, Finset.univ, Fin, Imo2012P3.BobPhase.probe, HAppend.hAppend, List, Imo2012P3.hist, List.cons, List.nil, congrArg, List.foldl_append, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bobStep_frozen line 614 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.BobState, LE.le, Finset.card, Fin, Imo2012P3.BobState.pool, HPow.hPow, OfNat.ofNat, Bool, Eq, Imo2012P3.bobStep
Proof uses: id, dite_eq_left, Not, Imo2012P3.bobStepPhase, Imo2012P3.BobState.phase
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bobStep_active line 619 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2012P3.BobState, Not, LE.le, Finset.card, Fin, Imo2012P3.BobState.pool, HPow.hPow, OfNat.ofNat, Bool, Eq, Imo2012P3.bobStep, Imo2012P3.bobStepPhase, Imo2012P3.BobState.phase
Proof uses: id, dite_eq_right
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bobStepPhase_probe_true line 624 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card, Eq, Imo2012P3.BobState, Imo2012P3.bobStepPhase, Imo2012P3.BobPhase.probe, Bool.true, Imo2012P3.BobState.mk, Imo2012P3.BobPhase.bits, List.nil, Bool
Proof uses: rfl
16 instances, coercions and auxiliary constants left out.
lemma Imo2012P3.bobStepPhase_probe_false_eq line 627 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card, Eq, Imo2012P3.BobState, Imo2012P3.bobStepPhase, Imo2012P3.BobPhase.probe, Bool.false, Imo2012P3.BobState.mk, Finset.erase, Imo2012P3.bobSpecial
Proof uses: id, Eq.mpr, ite, congrArg, ite_eq_left, Eq.refl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bobStepPhase_probe_false_lt line 635 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card, Ne, Eq, Imo2012P3.BobState, Imo2012P3.bobStepPhase, Imo2012P3.BobPhase.probe, Bool.false, Imo2012P3.BobState.mk
Proof uses: id, Eq.mpr, ite, Finset.erase, Imo2012P3.bobSpecial, congrArg, ite_eq_right, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bobStepPhase_bits_complete line 642 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card, List, Bool, Eq, List.length, HAppend.hAppend, List.cons, List.nil, Imo2012P3.BobState, Imo2012P3.bobStepPhase, Imo2012P3.BobPhase.bits, Imo2012P3.BobState.mk, Finset.erase and 10 more
Proof uses: id, Imo2012P3.BobPhase.answers.match_1, Imo2012P3.BobPhase, Imo2012P3.bobStepPhase.match_1, Unit, ite, Imo2012P3.bobSpecial, dite, Not, Eq.mpr, congrArg, dite_eq_left, Eq.refl
42 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bobStepPhase_bits_cont line 651 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Finset.card, List, Bool, Ne, List.length, HAppend.hAppend, List.cons, List.nil, Eq, Imo2012P3.BobState, Imo2012P3.bobStepPhase, Imo2012P3.BobPhase.bits, Imo2012P3.BobState.mk
Proof uses: id, Imo2012P3.BobPhase.answers.match_1, Imo2012P3.BobPhase, Imo2012P3.bobStepPhase.match_1, Unit, ite, Finset.erase, Imo2012P3.bobSpecial, Imo2012P3.BobPhase.probe, dite, Membership.mem, Function.Embedding, Subtype, Imo2012P3.bobEmbedding, Bool.not, List.get, Fin.mk, Not, Eq.mpr, congrArg and 2 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bobStrategy_move_guess line 658 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, LE.le, Finset.card, Fin, Imo2012P3.BobState.pool, Imo2012P3.bobStateOf, HPow.hPow, OfNat.ofNat, Eq, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.bobStrategy, Imo2012P3.hist, Imo2012P3.Move.guess
Proof uses: List.foldl, Imo2012P3.BobState, Imo2012P3.bobStep, Imo2012P3.BobState.mk, Finset.univ, Imo2012P3.BobPhase.probe, id, dite, Not, Imo2012P3.Move.ask, Imo2012P3.bobQuestion, Imo2012P3.BobState.phase, dite_eq_left
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bobStrategy_move_ask line 669 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Not, LE.le, Finset.card, Fin, Imo2012P3.BobState.pool, Imo2012P3.bobStateOf, HPow.hPow, OfNat.ofNat, Eq, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.bobStrategy, Imo2012P3.hist, Imo2012P3.Move.ask, Imo2012P3.bobQuestion, Imo2012P3.BobState.phase
Proof uses: List.foldl, Imo2012P3.BobState, Imo2012P3.bobStep, Imo2012P3.BobState.mk, Finset.univ, Imo2012P3.BobPhase.probe, id, dite, Imo2012P3.Move.guess, dite_eq_right
17 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bobStrategy_move_ask_probe line 682 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Eq, Imo2012P3.BobPhase, Imo2012P3.BobState.phase, Imo2012P3.bobStateOf, Imo2012P3.BobPhase.probe, Not, LE.le, Finset.card, Fin, Imo2012P3.BobState.pool, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.bobStrategy, Imo2012P3.hist, Imo2012P3.Move.ask and 3 more
Proof uses: Eq.mpr, Imo2012P3.bobQuestion, id, congrArg, Imo2012P3.bobStrategy_move_ask, Imo2012P3.bobQuestion_probe, Eq.refl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bobStrategy_move_ask_bits line 690 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, List, Eq, Imo2012P3.BobPhase, Imo2012P3.BobState.phase, Imo2012P3.bobStateOf, Imo2012P3.BobPhase.bits, Not, LE.le, Finset.card, Fin, Imo2012P3.BobState.pool, HPow.hPow, OfNat.ofNat, List.length, LT.lt, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.bobStrategy and 4 more
Proof uses: Eq.mpr, id, congrArg, Imo2012P3.bobQuestion, Imo2012P3.bobStrategy_move_ask, Finset, Imo2012P3.bobQuestion_bits, Fin.ext, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bob_answers_le line 702 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, LE.le, Imo2012P3.BobPhase.answers, Imo2012P3.BobState.phase, Imo2012P3.bobStateOf
Proof uses: Nat.recAux, le_refl, OfNat.ofNat, Eq.mpr, HAdd.hAdd, Imo2012P3.bobStep, id, Eq, congrArg, Imo2012P3.BobState, Imo2012P3.bobStateOf_succ, dite, Finset.card, Fin, Imo2012P3.BobState.pool, HPow.hPow, Imo2012P3.bobStep_frozen, le_trans, Nat.le_succ, Not and 37 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bob_phase_inv line 740 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Bool, Imo2012P3.BobPhase.answers.match_1, Imo2012P3.BobPhase, Imo2012P3.BobState.phase, Imo2012P3.bobStateOf, List, And, HAdd.hAdd, LT.lt, List.length
Proof uses: Nat.recAux, Nat.zero_le, Eq.mpr, Imo2012P3.bobStep, id, Eq, congrArg, Imo2012P3.BobState, Imo2012P3.bobStateOf_succ, dite, Finset.card, Fin, Imo2012P3.BobState.pool, HPow.hPow, Imo2012P3.bobStep_frozen, Not, Imo2012P3.bobStepPhase, Imo2012P3.bobStep_active, Imo2012P3.BobPhase.probe, Eq.mp and 29 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
lemma Imo2012P3.bob_backward_probe Backward step, probe phase with j ≥ 1 line 783 source
Source documentation
Backward step, probe phase with j ≥ 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Finset, Fin, Eq, Imo2012P3.BobState, Imo2012P3.bobStateOf, HAdd.hAdd, OfNat.ofNat, Imo2012P3.BobState.mk, Imo2012P3.BobPhase.probe, Not, LE.le, Finset.card, HPow.hPow, And, HSub.hSub, Bool.false
Proof uses: Imo2012P3.bobStep, Eq.mpr, id, congrArg, Eq.symm, Imo2012P3.bobStateOf_succ, dite, Imo2012P3.BobState.pool, absurd, Eq.mp, Imo2012P3.bobStep_frozen, Imo2012P3.BobPhase, Imo2012P3.BobState.phase, Finset.erase, Imo2012P3.bobSpecial, HEq, Imo2012P3.bobStepPhase, Imo2012P3.bobStepPhase_probe_false_eq, Imo2012P3.bobStep_active, Eq.refl and 29 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma bob_backward_probe {ans : ℕ → Bool} {t : ℕ} {P : Finset (Fin N)} {j : ℕ}
    (h : bobStateOf N k ans (t + 1) = ⟨P, BobPhase.probe j⟩)
    (hcard : ¬ P.card ≤ 2 ^ k) (hj : 1 ≤ j) :
    bobStateOf N k ans t = ⟨P, BobPhase.probe (j - 1)⟩ ∧ ans t = false := by
…
```
Mentions: P, h, Imo2012P3.bobStateOf
lemma Imo2012P3.bob_backward_bits_nil Backward step, bit phase with no bit answers yet line 824 source
Source documentation
Backward step, bit phase with no bit answers yet.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Finset, Fin, Eq, Imo2012P3.BobState, Imo2012P3.bobStateOf, HAdd.hAdd, OfNat.ofNat, Imo2012P3.BobState.mk, Imo2012P3.BobPhase.bits, List.nil, Not, LE.le, Finset.card, HPow.hPow, And, Imo2012P3.BobPhase.probe, HSub.hSub, Bool.true
Proof uses: Imo2012P3.bobStep, Eq.mpr, id, congrArg, Eq.symm, Imo2012P3.bobStateOf_succ, dite, Imo2012P3.BobState.pool, absurd, Eq.mp, Imo2012P3.bobStep_frozen, Imo2012P3.BobPhase, Imo2012P3.BobState.phase, Bool.false, Finset.erase, Imo2012P3.bobSpecial, HEq, Imo2012P3.bobStepPhase, Imo2012P3.bobStepPhase_probe_false_eq, Imo2012P3.bobStep_active and 36 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
lemma bob_backward_bits_nil {ans : ℕ → Bool} {t : ℕ} {P : Finset (Fin N)} {j : ℕ}
    (h : bobStateOf N k ans (t + 1) = ⟨P, BobPhase.bits j []⟩)
    (hcard : ¬ P.card ≤ 2 ^ k) :
    bobStateOf N k ans t = ⟨P, BobPhase.probe (j - 1)⟩ ∧ ans t = true := by
…
```
Mentions: P, h, Imo2012P3.bobStateOf
lemma Imo2012P3.bob_backward_bits_snoc Backward step, bit phase with at least one bit answer line 866 source
Source documentation
Backward step, bit phase with at least one bit answer.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Finset, Fin, List, Eq, Imo2012P3.BobState, Imo2012P3.bobStateOf, HAdd.hAdd, OfNat.ofNat, Imo2012P3.BobState.mk, Imo2012P3.BobPhase.bits, HAppend.hAppend, List.cons, List.nil, Not, LE.le, Finset.card, HPow.hPow, And
Proof uses: Imo2012P3.bobStep, Eq.mpr, id, congrArg, Eq.symm, Imo2012P3.bobStateOf_succ, dite, Imo2012P3.BobState.pool, absurd, Eq.mp, Imo2012P3.bobStep_frozen, Imo2012P3.BobPhase, Imo2012P3.BobState.phase, Imo2012P3.BobPhase.probe, Bool.false, Finset.erase, Imo2012P3.bobSpecial, HEq, Imo2012P3.bobStepPhase, Imo2012P3.bobStepPhase_probe_false_eq and 39 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
```
lemma bob_backward_bits_snoc {ans : ℕ → Bool} {t : ℕ} {P : Finset (Fin N)} {j : ℕ}
    {bs : List Bool} {b : Bool}
    (h : bobStateOf N k ans (t + 1) = ⟨P, BobPhase.bits j (bs ++ [b])⟩)
    (hcard : ¬ P.card ≤ 2 ^ k) :
    bobStateOf N k ans t = ⟨P, BobPhase.bits j bs⟩ ∧ ans t = b := by
…
```
Mentions: P, h, Imo2012P3.bobStateOf
lemma Imo2012P3.bob_backward_probe_chain Iterated backward step through a probe phase line 916 source
Source documentation
Iterated backward step through a probe phase.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Finset, Fin, Eq, Imo2012P3.BobState, Imo2012P3.bobStateOf, Imo2012P3.BobState.mk, Imo2012P3.BobPhase.probe, Not, LE.le, Finset.card, HPow.hPow, OfNat.ofNat, And, HSub.hSub, Bool.false
Proof uses: Nat.recAux, And.intro, Eq.mpr, id, congr, congrArg, tsub_zero, Imo2012P3.BobPhase, absurd, HAdd.hAdd, Imo2012P3.bob_backward_probe, Eq.symm, And.left, And.right
26 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma bob_backward_probe_chain {ans : ℕ → Bool} {t : ℕ} {P : Finset (Fin N)} {j i : ℕ}
    (h : bobStateOf N k ans t = ⟨P, BobPhase.probe j⟩)
    (hcard : ¬ P.card ≤ 2 ^ k) (hi : i ≤ j) (ht : j ≤ t) :
    bobStateOf N k ans (t - i) = ⟨P, BobPhase.probe (j - i)⟩ ∧
      (1 ≤ i → ans (t - i) = false) := by
…
```
Mentions: P, h, Imo2012P3.bobStateOf
lemma Imo2012P3.bob_backward_bits_chain Iterated backward step through a bit phase line 932 source
Source documentation
Iterated backward step through a bit phase.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Finset, Fin, List, Eq, Imo2012P3.BobState, Imo2012P3.bobStateOf, Imo2012P3.BobState.mk, Imo2012P3.BobPhase.bits, Not, LE.le, Finset.card, HPow.hPow, OfNat.ofNat, List.length, HAdd.hAdd, And, HSub.hSub, List.take and 2 more
Proof uses: Nat.recAux, And.intro, Eq.mpr, id, congr, congrArg, tsub_zero, Imo2012P3.BobPhase, Eq.trans, congrFun', List.take_length, absurd, rfl, HAppend.hAppend, List.cons, List.nil, Option.toList, GetElem?.getElem?, List.take_add_one, Option.some and 7 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma bob_backward_bits_chain {ans : ℕ → Bool} {t : ℕ} {P : Finset (Fin N)} {j : ℕ}
    {bs : List Bool} {i : ℕ}
    (h : bobStateOf N k ans t = ⟨P, BobPhase.bits j bs⟩)
    (hcard : ¬ P.card ≤ 2 ^ k) (hi : i ≤ bs.length) (ht : bs.length + 1 ≤ t + 1) :
    bobStateOf N k ans (t - i) = ⟨P, BobPhase.bits j (bs.take (bs.length - i))⟩ ∧
      ((hi1 : 1 ≤ i) → ans (t - i) = bs[bs.length - i]'(by lia)) := by
…
```
Mentions: P, h, Imo2012P3.bobStateOf
lemma Imo2012P3.bob_measure The termination measure: while the pool has more than 2 ^ k elements, t is bounded by (2k+1) * (eliminated so far) + (answers in current round) line 958 source
Source documentation
The termination measure: while the pool has more than 2 ^ k elements, t is bounded by (2k+1) * (eliminated so far) + (answers in current round).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Bool, Not, Finset.card, Fin, Imo2012P3.BobState.pool, Imo2012P3.bobStateOf, HPow.hPow, HAdd.hAdd, HMul.hMul, HSub.hSub, Imo2012P3.BobPhase.answers, Imo2012P3.BobState.phase
Proof uses: Nat.recAux, of_eq_true, Eq.trans, Imo2012P3.BobPhase.probe, True, congrArg, congrFun', Fintype.card_fin, tsub_self, MulZeroClass.mul_zero, zero_add, Eq.mpr, Imo2012P3.bobStep, id, Eq, Imo2012P3.BobState, Imo2012P3.bobStateOf_succ, dite, absurd, Eq.mp and 46 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
lemma bob_measure (hk : 1 ≤ k) (ans : ℕ → Bool) (t : ℕ)
    (hcard : ¬ (bobStateOf N k ans t).pool.card ≤ 2 ^ k) :
    t ≤ (2 * k + 1) * (N - (bobStateOf N k ans t).pool.card) +
      (bobStateOf N k ans t).phase.answers := by
…
```
Mentions: Imo2012P3.bobStateOf
lemma Imo2012P3.bob_terminates B's strategy always stops: the pool shrinks by one every 2k + 1 answers line 1038 source
Source documentation
B's strategy always stops: the pool shrinks by one every 2k + 1 answers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Bool, Exists, Finset, Fin, Eq, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.bobStrategy, Imo2012P3.hist, Imo2012P3.Move.guess
Proof uses: Classical.byContradiction, Not, Finset.card, Imo2012P3.BobState.pool, Imo2012P3.bobStateOf, HPow.hPow, Eq.mp, Ne, Eq.trans, binderNameHint, forall_congr, Imo2012P3.bobStrategy_move_guess, HAdd.hAdd, HMul.hMul, HSub.hSub, Imo2012P3.BobPhase.answers, Imo2012P3.BobState.phase, Imo2012P3.bob_measure, card_finset_fin_le, Imo2012P3.BobPhase.answers.match_1 and 14 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma bob_terminates (hk : 1 ≤ k) (ans : ℕ → Bool) :
    ∃ T X, (bobStrategy (N := N) k).move (hist ans T) = Move.guess X := by
…
```
Mentions: Imo2012P3.bobStrategy, Imo2012P3.hist
lemma Imo2012P3.bob_mem_pool The pool invariant: if the answers are consistent with x up to time t, then x is still in Bob's pool line 1074 source
Source documentation
The pool invariant: if the answers are consistent with x up to time t, then x is still in Bob's pool.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Bool, Imo2012P3.ConsistentUpTo, Imo2012P3.bobStrategy, Membership.mem, Finset, Imo2012P3.BobState.pool, Imo2012P3.bobStateOf
Proof uses: Nat.recAux, Finset.mem_univ, HAdd.hAdd, Eq.mpr, Imo2012P3.bobStep, id, Eq, congrArg, Imo2012P3.BobState, Imo2012P3.bobStateOf_succ, dite, Finset.card, HPow.hPow, Imo2012P3.bobStep_frozen, Not, Imo2012P3.bobStepPhase, Imo2012P3.BobState.phase, Imo2012P3.bobStep_active, Imo2012P3.BobPhase, Imo2012P3.BobPhase.probe and 91 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 188 steps
Open to load the checked before-and-after goal states.
```
lemma bob_mem_pool (hk : 1 ≤ k) {x : Fin N} {ans : ℕ → Bool} {t : ℕ}
    (hcons : ConsistentUpTo k (bobStrategy k) x ans t) :
    x ∈ (bobStateOf N k ans t).pool := by
…
```
Mentions: Imo2012P3.ConsistentUpTo, Imo2012P3.bobStrategy, Imo2012P3.bobStateOf, pool
lemma Imo2012P3.bob_guaranteesWin B's strategy guarantees a win when n ≥ 2 ^ k line 1257 source
Source documentation
B's strategy guarantees a win when n ≥ 2 ^ k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HPow.hPow, Imo2012P3.GuaranteesWin, Imo2012P3.bobStrategy
Proof uses: And.intro, Fin, Bool, Imo2012P3.ConsistentUpTo, Exists, Finset, Eq, Imo2012P3.Move, Imo2012P3.Strategy.move, Imo2012P3.hist, Imo2012P3.Move.guess, And, Membership.mem, Finset.card, Imo2012P3.bob_terminates, dite, Imo2012P3.BobState.pool, Imo2012P3.bobStateOf, Imo2012P3.Move.guess.inj, Eq.mp and 18 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma bob_guaranteesWin (n : ℕ) (hk : 1 ≤ k) (hn : 2 ^ k ≤ n) :
    GuaranteesWin k n (bobStrategy (N := N) k) := by
…
```
Mentions: Imo2012P3.GuaranteesWin, Imo2012P3.bobStrategy
problem Imo2012P3.imo2012_p3_part_a line 1274 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HPow.hPow, Imo2012P3.BobWins
Proof uses: Exists.intro, Imo2012P3.Strategy, Imo2012P3.GuaranteesWin, Imo2012P3.bobStrategy, Imo2012P3.bob_guaranteesWin
12 instances, coercions and auxiliary constants left out.
problem Imo2012P3.imo2012_p3_part_b line 1278 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Nat, GE.ge, And, LE.le, Real, HPow.hPow, OfScientific.ofScientific, Bool.true, Not, Imo2012P3.BobWins, HAdd.hAdd, OfNat.ofNat
Proof uses: LT.lt, HMul.hMul, Imo2012P3.weightBase, Imo2012P3.exists_eventually_large, Exists.intro, Nat.ceil, And.intro, Nat.le_ceil, Imo2012P3.not_bobWins, Imo2012P3.aliceWeightBase_bound, rfl
41 instances, coercions and auxiliary constants left out.

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