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

47 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1990, Problem 5

Given an initial integer n₀ > 1, two players A and B choose integers n₁, n₂, n₃, ... alternately according to the following rules:

Knowing n₂ₖ, A chooses any integer n₂ₖ₊₁ such that n₂ₖ ≤ n₂ₖ₊₁ ≤ n₂ₖ².

Knowing n₂ₖ₊₁, B chooses any integer n₂ₖ₊₂ such that n₂ₖ₊₁/n₂ₖ₊₂ = p^r for some prime p and integer r ≥ 1.

Player A wins the game by choosing the number 1990; player B wins by choosing the number 1.

For which n₀ does (a) A have a winning strategy? (b) B have a winning strategy? (c) neither player have a winning strategy?

Formalization notes

The proof follows a solution sketch after kalva.

Imports (5)

Imported by 1 file

Compfiles.lean

def Imo1990P5.AMove A legal move of player A: from the number n just chosen by B (or the initial number n₀), A may choose any m with n ≤ m ≤ n ^ 2 (A wins by choosing 1990) line 46 source
Source documentation
A legal move of player A: from the number n just chosen by B (or the initial number n₀), A may choose any m with n ≤ m ≤ n ^ 2 (A wins by choosing 1990).

standard axioms: propext what this means
Statement uses: Nat
Proof uses: And, LE.le, HPow.hPow, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.
```
@[reducible] def AMove (n m : ℕ) : Prop := n ≤ m ∧ m ≤ n ^ 2
```
def Imo1990P5.BMove A legal move of player B: from the number m just chosen by A, B may choose any m' such that m / m' is a prime power p ^ r with r ≥ 1 (B wins by choosing 1) line 50 source
Source documentation
A legal move of player B: from the number m just chosen by A, B may choose any m' such that m / m' is a prime power p ^ r with r ≥ 1 (B wins by choosing 1).

standard axioms: propext what this means
Statement uses: Nat
Proof uses: Exists, And, Nat.Prime, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HPow.hPow
8 instances, coercions and auxiliary constants left out.
```
@[reducible] def BMove (m m' : ℕ) : Prop := ∃ p r : ℕ, p.Prime ∧ 0 < r ∧ m = m' * p ^ r
```
inductive Imo1990P5.AWins AWins n: it is A's turn and the current number is n (the initial position has n = n₀), and A has a winning strategy line 57 source
Source documentation
AWins n: it is A's turn and the current number is n (the initial position has n = n₀), and A has a winning strategy. A either wins immediately by choosing 1990 (a legal move from n), or chooses a legal move m from which B cannot win (B wins by choosing 1) and such that every legal answer of B is again a winning position for A.

standard axioms: propext what this means
Statement uses: Nat
```
inductive AWins : ℕ → Prop
  | win (n : ℕ) (h : AMove n 1990) : AWins n
  | move (n m : ℕ) (h₁ : AMove n m) (h₂ : ¬ BMove m 1)
      (h₃ : ∀ m', BMove m m' → AWins m') : AWins n

/-- `BWins m`: it is B's turn and the current number is `m`, and B has a winning
strategy. B either wins immediately by choosing 1, or chooses a legal move `m' ≠ 1`
from which A cannot win (A wins by choosing 1990) and such that every legal answer
of A is again a winning position for B. -/
```
Mentions: h, Imo1990P5.AMove, Imo1990P5.BMove, Imo1990P5.BWins, answer
inductive Imo1990P5.BWins BWins m: it is B's turn and the current number is m, and B has a winning strategy line 66 source
Source documentation
BWins m: it is B's turn and the current number is m, and B has a winning strategy. B either wins immediately by choosing 1, or chooses a legal move m' ≠ 1 from which A cannot win (A wins by choosing 1990) and such that every legal answer of A is again a winning position for B.

standard axioms: propext what this means
Statement uses: Nat
```
inductive BWins : ℕ → Prop
  | one (m : ℕ) (h : BMove m 1) : BWins m
  | move (m m' : ℕ) (h : BMove m m') (h₁ : m' ≠ 1)
      (h₂ : ∀ m'', AMove m' m'' → m'' ≠ 1990)
      (h₃ : ∀ m'', AMove m' m'' → BWins m'') : BWins m

/-- `BWinsStart n`: B has a winning strategy from the initial position with `n₀ = n`
(it is A's turn): whatever legal first move `m` A makes, it is not 1990 and B wins
from `m`. -/
```
Mentions: h, Imo1990P5.BMove, Imo1990P5.AMove, Imo1990P5.BWinsStart
def Imo1990P5.BWinsStart BWinsStart n: B has a winning strategy from the initial position with n₀ = n (it is A's turn): whatever legal first move m A makes, it is not 1990 and B wins from m line 75 source
Source documentation
BWinsStart n: B has a winning strategy from the initial position with n₀ = n (it is A's turn): whatever legal first move m A makes, it is not 1990 and B wins from m.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: Imo1990P5.AMove, And, Ne, OfNat.ofNat, Imo1990P5.BWins
1 instances, coercions and auxiliary constants left out.
```
def BWinsStart (n : ℕ) : Prop := ∀ m, AMove n m → m ≠ 1990 ∧ BWins m
…
```
Mentions: Imo1990P5.AMove, Imo1990P5.BWins
theorem Imo1990P5.bmove_one_iff_isPrimePow B can win from the move m (by choosing 1) iff m is a prime power line 80 source
Source documentation
B can win from the move m (by choosing 1) iff m is a prime power.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Imo1990P5.BMove, OfNat.ofNat, IsPrimePow
Proof uses: Iff.intro, Exists, And, Nat.Prime, LT.lt, Eq, HMul.hMul, HPow.hPow, Iff.mpr, isPrimePow_nat_iff, Exists.intro, And.intro, Eq.mpr, id, congrArg, one_mul, Eq.refl, Eq.mp, propext
18 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem bmove_one_iff_isPrimePow {m : ℕ} : BMove m 1 ↔ IsPrimePow m := by
…
```
Mentions: Imo1990P5.BMove
theorem Imo1990P5.not_isPrimePow_of_dvd_of_dvd A number divisible by two distinct primes is not a prime power line 90 source
Source documentation
A number divisible by two distinct primes is not a prime power.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Ne, Dvd.dvd, Not, IsPrimePow
Proof uses: Eq.mpr, Exists, And, LT.lt, OfNat.ofNat, Eq, HPow.hPow, id, congrArg, propext, isPrimePow_nat_iff, False, Nat.Prime.dvd_of_dvd_pow, Eq.mp, Eq.symm, Iff.mp, Nat.prime_dvd_prime_iff_eq, Eq.trans
12 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem not_isPrimePow_of_dvd_of_dvd {m a b : ℕ} (ha : a.Prime) (hb : b.Prime)
    (hab : a ≠ b) (ham : a ∣ m) (hbm : b ∣ m) : ¬ IsPrimePow m := by
…
```
def Imo1990P5.bResponses The legal responses available to B after A chooses m line 103 source
Source documentation
The legal responses available to B after A chooses m. Keeping only divisors whose complementary factor is a prime power avoids reasoning about impossible moves.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: Finset.filter, IsPrimePow, HDiv.hDiv, Nat.divisors
4 instances, coercions and auxiliary constants left out.
```
def bResponses (m : ℕ) : Finset ℕ :=
…
```
theorem Imo1990P5.bmove_iff_mem_bResponses line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Iff, Imo1990P5.BMove, Membership.mem, Finset, Imo1990P5.bResponses
Proof uses: Eq.mpr, Finset.filter, IsPrimePow, HDiv.hDiv, Nat.divisors, id, Eq, congrArg, Imo1990P5.bResponses.eq_1, And, propext, Finset.mem_filter, Dvd.dvd, Nat.mem_divisors, Iff.intro, Exists, Nat.Prime, LT.lt, HMul.hMul, HPow.hPow and 15 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.not_bmove_one_of_not_mem line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Not, Membership.mem, Finset, Imo1990P5.bResponses, Imo1990P5.BMove
Proof uses: Iff.mp, Imo1990P5.bmove_iff_mem_bResponses
6 instances, coercions and auxiliary constants left out.
theorem Imo1990P5.bResponses_30 line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Finset, Nat, Imo1990P5.bResponses, OfNat.ofNat, Insert.insert, Singleton.singleton
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.bResponses_60 line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Finset, Nat, Imo1990P5.bResponses, OfNat.ofNat, Insert.insert, Singleton.singleton
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.bResponses_140 line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Finset, Nat, Imo1990P5.bResponses, OfNat.ofNat, Insert.insert, Singleton.singleton
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.bResponses_280 line 128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Finset, Nat, Imo1990P5.bResponses, OfNat.ofNat, Insert.insert, Singleton.singleton
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.bResponses_504 line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Finset, Nat, Imo1990P5.bResponses, OfNat.ofNat, Insert.insert, Singleton.singleton
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.bResponses_1991 line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Finset, Nat, Imo1990P5.bResponses, OfNat.ofNat, Insert.insert, Singleton.singleton
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo1990P5.trap The finite trap used for the drawn starting positions line 134 source
Source documentation
The finite trap used for the drawn starting positions.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton
4 instances, coercions and auxiliary constants left out.
```
def trap : Finset ℕ := {30, 60, 140, 280, 504}
```
lemma Imo1990P5.ne_zero_of_mem_trap line 136 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Imo1990P5.trap, Ne, OfNat.ofNat
Proof uses: List, List.Mem, Eq, List.insert, List.cons, List.nil, HEq, Insert.insert, Singleton.singleton, Eq.mp, congrArg, Imo1990P5.trap.eq_1, List.Mem.head, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, eq_of_heq and 5 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1990P5.one_not_mem_bResponses_of_mem_trap line 140 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Imo1990P5.trap, Not, Imo1990P5.bResponses, OfNat.ofNat
Proof uses: List, List.Mem, Eq, List.insert, List.cons, List.nil, HEq, Insert.insert, Singleton.singleton, Eq.mp, congrArg, Imo1990P5.trap.eq_1, List.Mem.head, of_eq_true, Eq.trans, False, True, Or, congrFun', Imo1990P5.bResponses_30 and 14 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1990P5.return_to_trap Whatever B plays from a trap number, A can legally return to that same number line 147 source
Source documentation
Whatever B plays from a trap number, A can legally return to that same number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Imo1990P5.trap, Imo1990P5.bResponses, Imo1990P5.AMove
Proof uses: List, List.Mem, Eq, List.insert, OfNat.ofNat, List.cons, List.nil, HEq, Insert.insert, Singleton.singleton, Eq.mp, congrArg, Imo1990P5.trap.eq_1, List.Mem.head, Imo1990P5.bResponses_30, of_decide_eq_true, LE.le, HPow.hPow, id, Bool and 13 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma return_to_trap {m m' : ℕ} (hm : m ∈ trap) (hm' : m' ∈ bResponses m) :
    AMove m' m := by
…
```
Mentions: Imo1990P5.trap, Imo1990P5.bResponses, Imo1990P5.AMove
theorem Imo1990P5.aw_45_1990 line 165 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo1990P5.AWins
Proof uses: Imo1990P5.AWins.win, And.intro, HPow.hPow, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 68 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.aw_23_44 line 169 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo1990P5.AWins
Proof uses: Imo1990P5.AWins.move, And.intro, HPow.hPow, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 104 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.aw_17_22 line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo1990P5.AWins
Proof uses: Imo1990P5.AWins.move, And.intro, HPow.hPow, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 105 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.aw_12_16 line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo1990P5.AWins
Proof uses: Imo1990P5.AWins.move, And.intro, HPow.hPow, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 106 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.aw_8_11 line 201 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo1990P5.AWins
Proof uses: Imo1990P5.AWins.move, And.intro, HPow.hPow, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 106 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.aw_1991 line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1990P5.AWins, OfNat.ofNat, Nat
Proof uses: Imo1990P5.AWins.move, And.intro, LE.le, HPow.hPow, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Imo1990P5.not_bmove_one_of_not_mem, Ne, of_eq_true, Not, Membership.mem, Finset, Imo1990P5.bResponses, Eq.trans, False and 29 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.exists_interval For n ≥ 1992 there is an exponent r ≥ 1 with 11 ^ r * 181 < n ≤ 11 ^ (r + 1) * 181, i.e. the intervals (11^r·181, 11^(r+1)·181] cover [1992, ∞) line 226 source
Source documentation
For n ≥ 1992 there is an exponent r ≥ 1 with 11 ^ r * 181 < n ≤ 11 ^ (r + 1) * 181, i.e. the intervals (11^r·181, 11^(r+1)·181] cover [1992, ∞).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, And, LT.lt, HMul.hMul, HPow.hPow, HAdd.hAdd
Proof uses: Exists.intro, le_trans, LT.lt.le, Nat.lt_pow_self, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Nat.pow_le_pow_right, GT.gt, Nat.le_mul_of_pos_right, Nat.find, Decidable.byContradiction, Not, Nat.find_spec, Eq.mp, congrArg and 10 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
theorem exists_interval {n : ℕ} (h : 1992 ≤ n) :
    ∃ r, 1 ≤ r ∧ 11 ^ r * 181 < n ∧ n ≤ 11 ^ (r + 1) * 181 := by
…
```
Mentions: h
theorem Imo1990P5.aw_big line 247 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Imo1990P5.AWins
Proof uses: And, HMul.hMul, HPow.hPow, HAdd.hAdd, Exists, Imo1990P5.exists_interval, Imo1990P5.AWins.move, And.intro, Trans.trans, Eq, Eq.symm, pow_one, Nat.pow_le_pow_right, of_decide_eq_true, GT.gt, id, Bool, Decidable.decide, Bool.true, Eq.refl and 78 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 121 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.awins_of_ge_8 A wins from every n ≥ 8 line 345 source
Source documentation
A wins from every n ≥ 8.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo1990P5.AWins
Proof uses: Nat.strong_induction_on, LT.lt, dite, Imo1990P5.aw_big, Not, Or, And, Eq, Imo1990P5.aw_8_11, Imo1990P5.aw_12_16, And.left, And.right, Imo1990P5.aw_17_22, Imo1990P5.aw_23_44, Imo1990P5.aw_45_1990, Imo1990P5.aw_1991, Eq.symm
9 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
theorem awins_of_ge_8 (n : ℕ) : 8 ≤ n → AWins n := by
…
```
Mentions: Imo1990P5.AWins
theorem Imo1990P5.escape_le49 From any non-prime-power m ∈ [2, 49], B has a legal move into [2, 7] line 364 source
Source documentation
From any non-prime-power m ∈ [2, 49], B has a legal move into [2, 7].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Not, IsPrimePow, Exists, And, Imo1990P5.BMove
Proof uses: dite, absurd, Iff.mpr, Nat.Prime, LT.lt, Eq, HPow.hPow, isPrimePow_nat_iff, Exists.intro, And.intro, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, of_decide_eq_true and 12 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 291 steps (first 200 of 291)
Open to load the checked before-and-after goal states.
```
theorem escape_le49 {m : ℕ} (h₁ : 2 ≤ m) (h₂ : m ≤ 49) (h₃ : ¬ IsPrimePow m) :
    ∃ m', BMove m m' ∧ 2 ≤ m' ∧ m' ≤ 7 := by
…
```
Mentions: Imo1990P5.BMove
theorem Imo1990P5.awins_ge line 416 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1990P5.AWins, Or, Eq, OfNat.ofNat, LE.le
Proof uses: Imo1990P5.AWins.rec, Imo1990P5.AMove, HPow.hPow, Or.inr, Decidable.byContradiction, Not, Trans.trans, Nat.pow_le_pow_left, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Imo1990P5.BMove, dite, Or.inl, Eq.mpr, Eq.mp, Eq.trans and 26 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.awins_not_bwinsstart line 448 source
standard axioms: propext what this means
Statement uses: Nat, Imo1990P5.AWins, Imo1990P5.BWinsStart, False
Proof uses: Imo1990P5.AWins.rec, Imo1990P5.AMove, OfNat.ofNat, And.left, Ne, Imo1990P5.BWins, rfl, Not, Imo1990P5.BMove, And.right, Eq, HEq, Imo1990P5.BWins.one, Imo1990P5.BWins.move, And.intro, Eq.refl, HEq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.bw_pp line 463 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, IsPrimePow, Imo1990P5.BWins
Proof uses: Exists, And, Nat.Prime, LT.lt, OfNat.ofNat, Eq, HPow.hPow, Eq.mp, congrArg, propext, isPrimePow_nat_iff, Imo1990P5.BWins.one, Exists.intro, HMul.hMul, And.intro, Eq.mpr, id, one_mul, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.bw_le_11 line 469 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo1990P5.BWins
Proof uses: dite, Imo1990P5.bw_pp, Iff.mpr, IsPrimePow, Exists, And, Nat.Prime, LT.lt, Eq, HPow.hPow, isPrimePow_nat_iff, Exists.intro, And.intro, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl and 23 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 103 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.bw_le_19 line 500 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo1990P5.BWins
Proof uses: dite, Imo1990P5.bw_pp, Iff.mpr, IsPrimePow, Exists, And, Nat.Prime, LT.lt, Eq, HPow.hPow, isPrimePow_nat_iff, Exists.intro, And.intro, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl and 24 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 175 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.bw_le_29 line 557 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo1990P5.BWins
Proof uses: dite, Imo1990P5.bw_pp, Iff.mpr, IsPrimePow, Exists, And, Nat.Prime, LT.lt, Eq, HPow.hPow, isPrimePow_nat_iff, Exists.intro, And.intro, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl and 25 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 309 steps (first 200 of 309)
Open to load the checked before-and-after goal states.
theorem Imo1990P5.bwinsstart_2 line 660 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1990P5.BWinsStart, OfNat.ofNat, Nat
Proof uses: Imo1990P5.AMove, And, Ne, Imo1990P5.BWins, LE.le, HPow.hPow, le_trans, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, And.intro, Imo1990P5.bw_le_11
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.bwinsstart_3 line 665 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1990P5.BWinsStart, OfNat.ofNat, Nat
Proof uses: Imo1990P5.AMove, And, Ne, Imo1990P5.BWins, LE.le, HPow.hPow, le_trans, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, And.intro, Imo1990P5.bw_le_11
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.bwinsstart_4 line 670 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1990P5.BWinsStart, OfNat.ofNat, Nat
Proof uses: Imo1990P5.AMove, And, Ne, Imo1990P5.BWins, LE.le, HPow.hPow, le_trans, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, And.intro, Imo1990P5.bw_le_19
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.bwinsstart_5 line 675 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1990P5.BWinsStart, OfNat.ofNat, Nat
Proof uses: Imo1990P5.AMove, And, Ne, Imo1990P5.BWins, LE.le, HPow.hPow, le_trans, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, And.intro, Imo1990P5.bw_le_29
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.not_bwins_trap B has no winning strategy from a trap number: A can always restore it line 683 source
Source documentation
B has no winning strategy from a trap number: A can always restore it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1990P5.BWins, Not, Membership.mem, Finset, Imo1990P5.trap
Proof uses: Imo1990P5.BWins.rec, Imo1990P5.BMove, OfNat.ofNat, Imo1990P5.one_not_mem_bResponses_of_mem_trap, Iff.mp, Imo1990P5.bResponses, Imo1990P5.bmove_iff_mem_bResponses, Imo1990P5.ne_zero_of_mem_trap, Ne, Imo1990P5.AMove, Imo1990P5.return_to_trap
5 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem not_bwins_trap {m : ℕ} (h : BWins m) : m ∉ trap := by
…
```
Mentions: h, Imo1990P5.BWins, Imo1990P5.trap
theorem Imo1990P5.not_bwinsstart_6 line 694 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Imo1990P5.BWinsStart, OfNat.ofNat, Nat
Proof uses: Ne, Imo1990P5.BWins, And, False, And.intro, LE.le, HPow.hPow, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Imo1990P5.not_bwins_trap, Membership.mem, Finset, Imo1990P5.trap
13 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo1990P5.not_bwinsstart_7 line 699 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Imo1990P5.BWinsStart, OfNat.ofNat, Nat
Proof uses: Ne, Imo1990P5.BWins, And, False, And.intro, LE.le, HPow.hPow, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Imo1990P5.not_bwins_trap, Membership.mem, Finset, Imo1990P5.trap
13 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
determine Imo1990P5.aWinsSet line 706 source
no axioms what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, LE.le, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
determine Imo1990P5.bWinsSet line 708 source
standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton
4 instances, coercions and auxiliary constants left out.
determine Imo1990P5.drawSet line 710 source
standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton
4 instances, coercions and auxiliary constants left out.
problem Imo1990P5.imo1990_p5 line 712 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, And, Iff, Imo1990P5.AWins, Membership.mem, Set, Imo1990P5.aWinsSet, Imo1990P5.BWinsStart, Finset, Imo1990P5.bWinsSet, Not, Imo1990P5.drawSet
Proof uses: And.intro, Iff.intro, Eq, Or, Imo1990P5.awins_ge, False.elim, Imo1990P5.awins_of_ge_8, dite, Imo1990P5.awins_not_bwinsstart, absurd, Imo1990P5.not_bwinsstart_7, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_not_le_left, Nat.rawCast, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Imo1990P5.not_bwinsstart_6 and 23 more
26 instances, coercions and auxiliary constants left out.

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