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

88 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2024, Problem 5

Turbo the snail plays a game on a board with $2024$ rows and $2023$ columns. There are hidden monsters in $2022$ of the cells. Initially, Turbo does not know where any of the monsters are, but he knows that there is exactly one monster in each row except the first row and the last row, and that each column contains at most one monster.

Turbo makes a series of attempts to go from the first row to the last row. On each attempt, he chooses to start on any cell in the first row, then repeatedly moves to an adjacent cell sharing a common side. (He is allowed to return to a previously visited cell.) If he reaches a cell with a monster, his attempt ends and he is transported back to the first row to start a new attempt. The monsters do not move, and Turbo remembers whether or not each cell he has visited contains a monster. If he reaches any cell in the last row, his attempt ends and the game is over.

Determine the minimum value of $n$ for which Turbo has a strategy that guarantees reaching the last row on the $n$th attempt or earlier, regardless of the locations of the monsters.

Imports (8)

Imported by 1 file

Compfiles.lean

abbrev Imo2024P5.Cell A cell on the board for the game line 55 source
Source documentation
A cell on the board for the game.

no axioms what this means
Statement uses: Nat
Proof uses: Prod, Fin, HAdd.hAdd, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
abbrev Cell (N : ℕ) : Type := Fin (N + 2) × Fin (N + 1)
```
abbrev Imo2024P5.InteriorRow A row that is neither the first nor the last (and thus contains a monster) line 58 source
Source documentation
A row that is neither the first nor the last (and thus contains a monster).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Fin, HAdd.hAdd, OfNat.ofNat, Set.Icc, Fin.mk
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
abbrev InteriorRow (N : ℕ) : Type := (Set.Icc 1 ⟨N, by lia⟩ : Set (Fin (N + 2)))
```
abbrev Imo2024P5.MonsterData Data for valid positions of the monsters line 61 source
Source documentation
Data for valid positions of the monsters.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Function.Embedding, Imo2024P5.InteriorRow, Fin, HAdd.hAdd, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
abbrev MonsterData (N : ℕ) : Type := InteriorRow N ↪ Fin (N + 1)
```
Mentions: Imo2024P5.InteriorRow
def Imo2024P5.MonsterData.monsterCells The cells with monsters as a Set, given an injection from rows to columns line 64 source
Source documentation
The cells with monsters as a Set, given an injection from rows to columns.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.MonsterData, Set, Imo2024P5.Cell
Proof uses: Set.range, Imo2024P5.InteriorRow, Prod.mk, Fin, HAdd.hAdd, OfNat.ofNat, Membership.mem, Set.Icc, Fin.mk
12 instances, coercions and auxiliary constants left out.
```
def MonsterData.monsterCells (m : MonsterData N) :
    Set (Cell N) :=
…
```
Mentions: Imo2024P5.MonsterData, Imo2024P5.Cell
def Imo2024P5.Adjacent Whether two cells are adjacent line 69 source
Source documentation
Whether two cells are adjacent.

no axioms what this means
Statement uses: Nat, Imo2024P5.Cell
Proof uses: Eq, HAdd.hAdd, Nat.dist, OfNat.ofNat, Prod.fst, Fin, Prod.snd
4 instances, coercions and auxiliary constants left out.
```
def Adjacent (x y : Cell N) : Prop :=
…
```
Mentions: Imo2024P5.Cell
structure Imo2024P5.Path A valid path from the first to the last row line 73 source
Source documentation
A valid path from the first to the last row.

standard axioms: propext what this means
Statement uses: Nat
```
structure Path (N : ℕ) where
…
```
def Imo2024P5.Path.firstMonster The first monster on a path, or none line 82 source
Source documentation
The first monster on a path, or none.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Path, Imo2024P5.MonsterData, Option, Imo2024P5.Cell
Proof uses: Decidable, Classical.propDecidable, List.find?, Decidable.decide, Membership.mem, Set, Imo2024P5.MonsterData.monsterCells, Imo2024P5.Path.cells
1 instances, coercions and auxiliary constants left out.
```
noncomputable def Path.firstMonster (p : Path N) (m : MonsterData N) : Option (Cell N) :=
…
```
Mentions: Imo2024P5.Path, Imo2024P5.MonsterData, Imo2024P5.Cell
abbrev Imo2024P5.Strategy A strategy, given the results of initial attempts, returns a path for the next attempt line 87 source
Source documentation
A strategy, given the results of initial attempts, returns a path for the next attempt.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: Fin, Option, Imo2024P5.Cell, Imo2024P5.Path
```
abbrev Strategy (N : ℕ) : Type := ⦃k : ℕ⦄ → (Fin k → Option (Cell N)) → Path N
```
Mentions: Imo2024P5.Cell, Imo2024P5.Path
def Imo2024P5.Strategy.play Playing a strategy, k attempts line 90 source
Source documentation
Playing a strategy, k attempts.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy, Imo2024P5.MonsterData, Fin, Option, Imo2024P5.Cell
2 instances, coercions and auxiliary constants left out.
```
noncomputable def Strategy.play (s : Strategy N) (m : MonsterData N) :
    (k : ℕ) → Fin k → Option (Cell N)
| 0 => Fin.elim0
| k + 1 => Fin.snoc (s.play m k) ((s (s.play m k)).firstMonster m)

/-- The predicate for a strategy winning within the given number of attempts. -/
```
Mentions: Imo2024P5.Strategy, Imo2024P5.MonsterData, Imo2024P5.Cell
def Imo2024P5.Strategy.WinsIn The predicate for a strategy winning within the given number of attempts line 96 source
Source documentation
The predicate for a strategy winning within the given number of attempts.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy, Imo2024P5.MonsterData
Proof uses: Membership.mem, Option, Imo2024P5.Cell, Set, Set.range, Fin, Imo2024P5.Strategy.play, Option.none
1 instances, coercions and auxiliary constants left out.
```
def Strategy.WinsIn (s : Strategy N) (m : MonsterData N) (k : ℕ) : Prop :=
…
```
Mentions: Imo2024P5.Strategy, Imo2024P5.MonsterData
def Imo2024P5.Strategy.ForcesWinIn Whether a strategy forces a win within the given number of attempts line 100 source
Source documentation
Whether a strategy forces a win within the given number of attempts.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy
Proof uses: Imo2024P5.MonsterData, Imo2024P5.Strategy.WinsIn
```
def Strategy.ForcesWinIn (s : Strategy N) (k : ℕ) : Prop :=
…
```
Mentions: Imo2024P5.Strategy
def Imo2024P5.Cell.reflect Reflecting a cell of the board (swapping left and right sides of the board) line 120 source
Source documentation
Reflecting a cell of the board (swapping left and right sides of the board).

no axioms what this means
Statement uses: Nat, Imo2024P5.Cell
Proof uses: Prod.mk, Fin, HAdd.hAdd, OfNat.ofNat, Prod.fst, Fin.rev, Prod.snd
3 instances, coercions and auxiliary constants left out.
```
def Cell.reflect (c : Cell N) : Cell N := (c.1, c.2.rev)
```
Mentions: Imo2024P5.Cell
def Imo2024P5.row1 The row 1, in the form required for MonsterData line 125 source
Source documentation
The row 1, in the form required for MonsterData.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.InteriorRow
Proof uses: Subtype.mk, Fin, HAdd.hAdd, Membership.mem, Set, Set.Icc, Fin.mk
13 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
@[expose] def row1 (hN : 2 ≤ N) : InteriorRow N :=
…
```
Mentions: Imo2024P5.InteriorRow
lemma Imo2024P5.coe_coe_row1 line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, HAdd.hAdd, Fin, Membership.mem, Set, Set.Icc, Fin.mk, Imo2024P5.row1
Proof uses: rfl
24 instances, coercions and auxiliary constants left out.
def Imo2024P5.row2 The row 2, in the form required for MonsterData line 135 source
Source documentation
The row 2, in the form required for MonsterData.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.InteriorRow
Proof uses: Subtype.mk, Fin, HAdd.hAdd, Membership.mem, Set, Set.Icc, Fin.mk
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def row2 (hN : 2 ≤ N) : InteriorRow N :=
…
```
Mentions: Imo2024P5.InteriorRow
def Imo2024P5.MonsterData.reflect Reflecting monster data line 141 source
Source documentation
Reflecting monster data.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.MonsterData
Proof uses: Function.Embedding.mk, Imo2024P5.InteriorRow, Fin, HAdd.hAdd, OfNat.ofNat, Function.comp, Fin.rev
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def MonsterData.reflect (m : MonsterData N) : MonsterData N where
…
```
Mentions: Imo2024P5.MonsterData
lemma Imo2024P5.MonsterData.reflect_reflect line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.MonsterData, Eq, Imo2024P5.MonsterData.reflect
Proof uses: Function.Embedding.ext, Imo2024P5.InteriorRow, Fin, HAdd.hAdd, OfNat.ofNat, Fin.rev_rev
5 instances, coercions and auxiliary constants left out.
lemma Imo2024P5.MonsterData.apply_row1_ne_zero_of_apply_row1_eq_N line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.MonsterData, Eq, HAdd.hAdd, Imo2024P5.InteriorRow, Fin, Imo2024P5.row1, Ne
Proof uses: Eq.mpr, id, congrArg, Eq.symm, propext, Fin.val_ne_iff, Fin.val_zero
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.MonsterData.reflect_apply_row1_eq_zero_of_apply_row1_eq_N line 153 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.MonsterData, Eq, HAdd.hAdd, Imo2024P5.InteriorRow, Fin, Imo2024P5.row1, Imo2024P5.MonsterData.reflect
Proof uses: Fin.rev, rfl, Eq.mpr, id, congrArg, Fin.last, Eq.symm, Fin.rev_last, propext, Fin.rev_inj, Fin.ext_iff, Fin.val_last
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.MonsterData.not_mem_monsterCells_of_fst_eq_zero line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.MonsterData, Imo2024P5.Cell, Eq, Fin, HAdd.hAdd, OfNat.ofNat, Prod.fst, Not, Membership.mem, Set, Imo2024P5.MonsterData.monsterCells
Proof uses: of_eq_true, Eq.trans, False, True, congrArg, Set.range, Imo2024P5.InteriorRow, Prod.mk, Set.Icc, Fin.mk, Exists, And, Subtype.mk, Prod.snd, funext, Prod, congrFun', Subtype, LE.le, Iff.mpr and 7 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.MonsterData.le_N_of_mem_monsterCells line 163 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.MonsterData, Imo2024P5.Cell, Membership.mem, Set, Imo2024P5.MonsterData.monsterCells, LE.le, HAdd.hAdd, OfNat.ofNat, Prod.fst, Fin
Proof uses: Exists, And, Fin.mk, Eq, Prod.mk, Imo2024P5.InteriorRow, Subtype.mk, Set.Icc, Iff.mpr, Iff.of_eq, Eq.mp, Eq.trans, Set.range, Subtype, congrArg, funext, propext, exists_prop_congr, Eq.refl, And.intro and 1 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.MonsterData.mk_mem_monsterCells_iff_of_le line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.MonsterData, Fin, HAdd.hAdd, OfNat.ofNat, LE.le, Fin.mk, Iff, Membership.mem, Prod, Set, Imo2024P5.Cell, Imo2024P5.MonsterData.monsterCells, Prod.mk, Eq, Imo2024P5.InteriorRow, Subtype.mk, Set.Icc, And.intro
Proof uses: Eq.mpr, Exists, And, id, congrFun', congrArg, Eq.trans, Set.range, funext, Prod.mk.injEq, Iff.intro, Eq.refl, Exists.intro, rfl
35 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.MonsterData.mem_monsterCells_iff_of_le line 180 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.MonsterData, Imo2024P5.Cell, LE.le, Fin, HAdd.hAdd, OfNat.ofNat, Prod.fst, Fin.mk, Iff, Membership.mem, Set, Imo2024P5.MonsterData.monsterCells, Eq, Imo2024P5.InteriorRow, Subtype.mk, Set.Icc, And.intro, Prod.snd
Proof uses: Imo2024P5.MonsterData.mk_mem_monsterCells_iff_of_le
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.MonsterData.mk_mem_monsterCells_iff line 185 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.MonsterData, Fin, HAdd.hAdd, OfNat.ofNat, Iff, Membership.mem, Prod, Set, Imo2024P5.Cell, Imo2024P5.MonsterData.monsterCells, Prod.mk, Exists, LE.le, Fin.mk, Eq, Imo2024P5.InteriorRow, Subtype.mk, Set.Icc, And.intro
Proof uses: Iff.intro, And, Eq.mp, Prod.mk.injEq, Exists.intro, rfl, Iff.mpr, Prod.fst, Prod.snd, Imo2024P5.MonsterData.mem_monsterCells_iff_of_le
36 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Path.exists_mem_le_fst line 196 source
standard axioms: propext what this means
Statement uses: Nat, Imo2024P5.Path, Fin, HAdd.hAdd, OfNat.ofNat, Exists, Imo2024P5.Cell, And, Membership.mem, List, Imo2024P5.Path.cells, LE.le, Prod.fst
Proof uses: Exists.intro, List.getLast, Imo2024P5.Path.nonempty, And.intro, List.getLast_mem, Eq.mpr, Fin.last, id, Eq, congrArg, Imo2024P5.Path.last_last_row, Fin.le_last
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2024P5.Path.findFstEq The first path element whose row is at least r line 202 source
Source documentation
The first path element whose row is at least r. Since rows change by at most one on each move and the path starts in row 0, this is in fact on row r: see Path.findFstEq_fst.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Path, Fin, HAdd.hAdd, OfNat.ofNat, Imo2024P5.Cell
Proof uses: Option.get, List.find?, Decidable.decide, LE.le, Prod.fst, Imo2024P5.Path.cells
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def Path.findFstEq (p : Path N) (r : Fin (N + 2)) : Cell N :=
…
```
Mentions: Imo2024P5.Path, Imo2024P5.Cell
lemma Imo2024P5.Path.find_eq_some_findFstEq line 206 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Path, Fin, HAdd.hAdd, OfNat.ofNat, Eq, Option, Imo2024P5.Cell, List.find?, Decidable.decide, LE.le, Prod.fst, Imo2024P5.Path.cells, Option.some, Imo2024P5.Path.findFstEq
Proof uses: Eq.mpr, Exists, Bool, Option.isSome, Bool.true, Option.get, id, congrArg, propext, Option.eq_some_iff_get_eq, Exists.intro, rfl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Path.findFstEq_mem_cells line 211 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Path, Fin, HAdd.hAdd, OfNat.ofNat, Membership.mem, Imo2024P5.Cell, List, Imo2024P5.Path.cells, Imo2024P5.Path.findFstEq
Proof uses: List.mem_of_find?_eq_some, Decidable.decide, LE.le, Prod.fst, Imo2024P5.Path.find_eq_some_findFstEq
9 instances, coercions and auxiliary constants left out.
lemma Imo2024P5.Path.findFstEq_fst_and_sub_one_mem Documented declaration: findFstEq_fst_and_sub_one_mem line 217 source
Source documentation
findFstEq r lies on row r exactly, and the cell just before it on the path lies on row r - 1 in the same column: the cell before the first row-≥ r cell has row < r, and adjacency forces both rows.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Path, Fin, HAdd.hAdd, OfNat.ofNat, Ne, And, Eq, Prod.fst, Imo2024P5.Path.findFstEq, Membership.mem, Prod, List, Imo2024P5.Cell, Imo2024P5.Path.cells, Prod.mk, Fin.mk, HSub.hSub, Prod.snd
Proof uses: id, LE.le, Exists, Option.get, List.find?, Decidable.decide, Imo2024P5.Path.exists_mem_le_fst, List.nil, List.head, List.getLast, Fin.last, List.IsChain, Imo2024P5.Adjacent, Imo2024P5.Path.mk, Bool, Bool.true, Exists.intro, And.intro, Eq.mpr, decide_eq_true_eq and 59 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
lemma Path.findFstEq_fst_and_sub_one_mem (p : Path N) {r : Fin (N + 2)} (hr : r ≠ 0) :
    (p.findFstEq r).1 = r ∧ (⟨(r : ℕ) - 1, by lia⟩, (p.findFstEq r).2) ∈ p.cells := by
…
```
Mentions: Imo2024P5.Path
lemma Imo2024P5.Path.findFstEq_fst line 249 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Path, Fin, HAdd.hAdd, OfNat.ofNat, Eq, Prod.fst, Imo2024P5.Path.findFstEq
Proof uses: Ne, Or, eq_or_ne, Imo2024P5.Cell, Exists, List, Imo2024P5.Path.cells, List.cons, List.exists_cons_of_ne_nil, Imo2024P5.Path.nonempty, List.head, Imo2024P5.Path.head_first_row, Eq.mp, congrFun', congrArg, List.head.congr_simp, Eq.symm, Option, List.find?, Decidable.decide and 22 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Path.findFstEq_fst_sub_one_mem line 260 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Path, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Membership.mem, Prod, List, Imo2024P5.Cell, Imo2024P5.Path.cells, Prod.mk, Fin.mk, HSub.hSub, Prod.snd, Imo2024P5.Path.findFstEq
Proof uses: And.right, Eq, Prod.fst, Imo2024P5.Path.findFstEq_fst_and_sub_one_mem
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Path.firstMonster_isSome line 264 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Path, Imo2024P5.MonsterData, Iff, Eq, Bool, Option.isSome, Imo2024P5.Cell, Imo2024P5.Path.firstMonster, Bool.true, Exists, And, Membership.mem, List, Imo2024P5.Path.cells, Set, Imo2024P5.MonsterData.monsterCells
Proof uses: Eq.mpr, List.find?, Decidable.decide, Classical.propDecidable, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Option, funext, propext, of_eq_true, Eq.trans, True, congrArg, decide_eq_true_eq, iff_self, List.find?_isSome
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Path.firstMonster_none_or_some line 269 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Path, Imo2024P5.MonsterData, Imo2024P5.Cell, Membership.mem, List, Imo2024P5.Path.cells, Or, Not, Set, Imo2024P5.MonsterData.monsterCells, Eq, Option, Imo2024P5.Path.firstMonster, Option.none, Option.some
Proof uses: dite, Or.inl, Exists, Eq.mp, Ne, congrArg, propext, Option.ne_none_iff_exists', Eq.symm, ne_eq, List.mem_of_find?_eq_some, Decidable.decide, Classical.propDecidable, Bool, Bool.true, List.find?_some, Or.resolve_left, Iff.mpr, Classical.not_not, decide_eq_true_eq and 3 more
6 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Path.firstMonster_eq_of_findFstEq_mem line 284 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Path, Imo2024P5.MonsterData, Membership.mem, Imo2024P5.Cell, Set, Imo2024P5.MonsterData.monsterCells, Imo2024P5.Path.findFstEq, OfNat.ofNat, Fin, HAdd.hAdd, Eq, Option, Imo2024P5.Path.firstMonster, Option.some
Proof uses: Exists, And, List, Imo2024P5.Path.cells, Bool, Decidable.decide, LE.le, Prod.fst, Bool.true, Eq.mpr, Prod.mk, id, Eq.trans, congrArg, funext, decide_eq_true_eq, Prod, Eq.mp, Imo2024P5.Path.exists_mem_le_fst, Ne and 37 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Path.mem_of_firstMonster_eq_some line 309 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Path, Imo2024P5.MonsterData, Imo2024P5.Cell, Eq, Option, Imo2024P5.Path.firstMonster, Option.some, And, Membership.mem, List, Imo2024P5.Path.cells, Set, Imo2024P5.MonsterData.monsterCells
Proof uses: List.mem_of_find?_eq_some, Decidable.decide, Classical.propDecidable, Bool, Bool.true, List.find?_some, And.intro, Eq.mp, decide_eq_true_eq
4 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Imo2024P5.Path.ofFn Convert a function giving the cells of a path to a Path line 318 source
Source documentation
Convert a function giving the cells of a path to a Path.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo2024P5.Cell, Ne, OfNat.ofNat, Eq, HAdd.hAdd, Prod.fst, Fin.mk, Nat.pos_of_ne_zero, HSub.hSub, Nat.sub_one_lt, Nat.lt_add_one, LT.lt, Imo2024P5.Adjacent, Nat.lt_of_succ_lt, Imo2024P5.Path
Proof uses: Imo2024P5.Path.mk, List.ofFn
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
@[expose] def Path.ofFn {m : ℕ} (f : Fin m → Cell N) (hm : m ≠ 0)
    (hf : (f ⟨0, Nat.pos_of_ne_zero hm⟩).1 = 0)
    (hl : (f ⟨m - 1, Nat.sub_one_lt hm⟩).1 = ⟨N + 1, Nat.lt_add_one _⟩)
    (ha : ∀ (i : ℕ) (hi : i + 1 < m), Adjacent (f ⟨i, Nat.lt_of_succ_lt hi⟩) (f ⟨i + 1, hi⟩)) :
    Path N where
…
```
Mentions: f, Imo2024P5.Cell, Imo2024P5.Adjacent, Imo2024P5.Path
lemma Imo2024P5.Path.ofFn_cells line 332 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo2024P5.Cell, Ne, OfNat.ofNat, Eq, HAdd.hAdd, Prod.fst, Fin.mk, Nat.pos_of_ne_zero, HSub.hSub, Nat.sub_one_lt, Nat.lt_add_one, LT.lt, Imo2024P5.Adjacent, Nat.lt_of_succ_lt, List, Imo2024P5.Path.cells, Imo2024P5.Path.ofFn, List.ofFn
Proof uses: rfl
18 instances, coercions and auxiliary constants left out.
lemma Imo2024P5.Path.ofFn_firstMonster_eq_none line 339 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo2024P5.Cell, Ne, OfNat.ofNat, Eq, HAdd.hAdd, Prod.fst, Fin.mk, Nat.pos_of_ne_zero, HSub.hSub, Nat.sub_one_lt, Nat.lt_add_one, LT.lt, Imo2024P5.Adjacent, Nat.lt_of_succ_lt, Imo2024P5.MonsterData, Iff, Option, Imo2024P5.Path.firstMonster and 6 more
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, List.find?, Decidable.decide, Classical.propDecidable, List.ofFn, List, Bool, Bool.true, forall_congr, Exists, implies_congr, decide_eq_true_eq, iff_self
25 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2024P5.Path.reflect Reflecting a path line 345 source
Source documentation
Reflecting a path.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Path
Proof uses: Imo2024P5.Path.mk, List.map, Imo2024P5.Cell, Imo2024P5.Cell.reflect, Imo2024P5.Path.cells
4 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def Path.reflect (p : Path N) : Path N where
…
```
Mentions: Imo2024P5.Path
lemma Imo2024P5.Path.firstMonster_reflect line 360 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Path, Imo2024P5.MonsterData, Eq, Option, Imo2024P5.Cell, Imo2024P5.Path.firstMonster, Imo2024P5.Path.reflect, Imo2024P5.MonsterData.reflect, Option.map, Imo2024P5.Cell.reflect
Proof uses: Imo2024P5.InteriorRow, Fin, HAdd.hAdd, OfNat.ofNat, Fin.rev, rfl, id, List.find?, Decidable.decide, Membership.mem, Set, Imo2024P5.MonsterData.monsterCells, Classical.propDecidable, Imo2024P5.Path.cells, Eq.mpr, List.map, Function.comp, Bool, congrFun', congrArg and 15 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Strategy.play_comp_castLE line 377 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy, Imo2024P5.MonsterData, LE.le, Eq, Fin, Option, Imo2024P5.Cell, Function.comp, Imo2024P5.Strategy.play, Fin.castLE
Proof uses: Nat.le.rec, Eq.refl, Nat.le.refl, Nat.le, Eq.mpr, Nat.succ, Nat.le.step, id, congrArg, Eq.symm, Nat.le_succ, Nat.le_trans, Fin.castLE_comp_castLE, Function.comp_assoc, eq_of_heq, HEq, HEq.refl, HAdd.hAdd, OfNat.ofNat, Fin.snoc and 4 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Strategy.play_apply_of_le line 386 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy, Imo2024P5.MonsterData, LT.lt, LE.le, Eq, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Fin.mk, LT.lt.trans_le
Proof uses: Eq.mpr, Function.comp, Fin, Fin.castLE, id, congrArg, Eq.symm, Imo2024P5.Strategy.play_comp_castLE, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Strategy.play_zero line 391 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy, Imo2024P5.MonsterData, LT.lt, OfNat.ofNat, Eq, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Fin.mk, Imo2024P5.Path.firstMonster, Fin.elim0
Proof uses: LE.le, Eq.mpr, zero_lt_one, id, congrArg, LT.lt.trans_le, Imo2024P5.Strategy.play_apply_of_le, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Strategy.play_one_eq line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy, Imo2024P5.MonsterData, Eq, Fin, OfNat.ofNat, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Matrix.vecCons, Imo2024P5.Path.firstMonster, Fin.elim0, Matrix.vecEmpty
Proof uses: funext, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_refl, List.nil, Eq.refl, eq_of_heq, List.Mem.tail, False.elim, noConfusion_of_Nat, List.ctorIdx and 1 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Strategy.play_one line 403 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy, Imo2024P5.MonsterData, LT.lt, OfNat.ofNat, Eq, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Fin.mk, Imo2024P5.Path.firstMonster, Nat.succ, Matrix.vecCons, Fin.elim0, Matrix.vecEmpty
Proof uses: Eq.mpr, one_lt_two, id, congrArg, LT.lt.trans_le, Imo2024P5.Strategy.play_apply_of_le, Fin, Eq.symm, Imo2024P5.Strategy.play_one_eq, Eq.refl
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Strategy.play_two_eq line 408 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy, Imo2024P5.MonsterData, Eq, Fin, OfNat.ofNat, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Matrix.vecCons, Nat.succ, Imo2024P5.Path.firstMonster, Fin.elim0, Matrix.vecEmpty
Proof uses: funext, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Eq.refl, eq_of_heq, List.Mem.tail, id, Eq.mpr and 6 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Strategy.play_two line 418 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy, Imo2024P5.MonsterData, LT.lt, OfNat.ofNat, Eq, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Fin.mk, Imo2024P5.Path.firstMonster, Nat.succ, Matrix.vecCons, Fin.elim0, Matrix.vecEmpty
Proof uses: Eq.mpr, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, id, congrArg, LT.lt.trans_le, Imo2024P5.Strategy.play_apply_of_le, Fin, Eq.symm, Imo2024P5.Strategy.play_two_eq
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Strategy.WinsIn.mono line 424 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy, Imo2024P5.MonsterData, Imo2024P5.Strategy.WinsIn, LE.le
Proof uses: Set.mem_of_mem_of_subset, Option, Imo2024P5.Cell, Option.none, Set.range, Fin, Imo2024P5.Strategy.play, Eq.mpr, Set, Exists, Eq, Function.comp, id, congrArg, propext, Set.range_subset_range_iff_exists_comp, Exists.intro, Fin.castLE, Eq.symm, Imo2024P5.Strategy.play_comp_castLE
3 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Strategy.ForcesWinIn.mono line 430 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy, Imo2024P5.Strategy.ForcesWinIn, LE.le
Proof uses: Imo2024P5.MonsterData, Imo2024P5.Strategy.WinsIn.mono
2 instances, coercions and auxiliary constants left out.
def Imo2024P5.baseMonsterData An arbitrary choice of monster positions, which is modified to put selected monsters in desired places line 438 source
Source documentation
An arbitrary choice of monster positions, which is modified to put selected monsters in desired places.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.MonsterData
Proof uses: Function.Embedding.mk, Imo2024P5.InteriorRow, Fin, HAdd.hAdd, OfNat.ofNat, LE.le, Fin.mk
13 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def baseMonsterData (N : ℕ) : MonsterData N where
…
```
Mentions: Imo2024P5.MonsterData
def Imo2024P5.monsterData12 Positions for monsters with specified columns in the second and third rows (rows 1 and 2) line 447 source
Source documentation
Positions for monsters with specified columns in the second and third rows (rows 1 and 2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HAdd.hAdd, Imo2024P5.MonsterData
Proof uses: Function.Embedding.setValue, Imo2024P5.InteriorRow, Imo2024P5.baseMonsterData, Imo2024P5.row2, Membership.mem, Set, Set.Icc, Fin.mk, Function.Embedding, Imo2024P5.row1
18 instances, coercions and auxiliary constants left out.
```
def monsterData12 (hN : 2 ≤ N) (c₁ c₂ : Fin (N + 1)) : MonsterData N :=
…
```
Mentions: Imo2024P5.MonsterData
lemma Imo2024P5.monsterData12_apply_row2 line 450 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HAdd.hAdd, Ne, Eq, Imo2024P5.MonsterData, Imo2024P5.InteriorRow, Imo2024P5.monsterData12, Imo2024P5.row2
Proof uses: Eq.mpr, Function.Embedding.setValue, Imo2024P5.baseMonsterData, Membership.mem, Set, Set.Icc, Fin.mk, Function.Embedding, Imo2024P5.row1, id, congrArg, Function.Embedding.setValue_eq_of_ne, Function.Embedding.setValue_eq, Ne.symm
24 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.row1_mem_monsterCells_monsterData12 line 461 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HAdd.hAdd, Membership.mem, Prod, Set, Imo2024P5.Cell, Imo2024P5.MonsterData.monsterCells, Imo2024P5.monsterData12, Prod.mk
Proof uses: Set.mem_range_self, Imo2024P5.InteriorRow, Set.Icc, Fin.mk, Imo2024P5.MonsterData, Imo2024P5.row1
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.row2_mem_monsterCells_monsterData12 line 465 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HAdd.hAdd, Ne, Membership.mem, Prod, Set, Imo2024P5.Cell, Imo2024P5.MonsterData.monsterCells, Imo2024P5.monsterData12, Prod.mk, Fin.mk
Proof uses: Eq.mpr, Set.range, Imo2024P5.InteriorRow, Set.Icc, Imo2024P5.MonsterData, Imo2024P5.row2, eq_of_heq, outParam, Membership, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, LT.lt, Subtype, Fin.isLt, Imo2024P5.monsterData12_apply_row2, Set.mem_range_self
25 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Strategy.not_forcesWinIn_two line 470 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy, LE.le, OfNat.ofNat, Not, Imo2024P5.Strategy.ForcesWinIn
Proof uses: NeZero, NeZero.mk, LT.lt, Nat.pos_of_neZero, Eq.mpr, Exists, Imo2024P5.MonsterData, Fin, Eq, Bool, Option.isSome, Imo2024P5.Cell, Imo2024P5.Strategy.play, Bool.true, id, Eq.trans, Option, Option.none, congrArg, forall_congr and 68 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.Strategy.ForcesWinIn.three_le line 501 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P5.Strategy, Imo2024P5.Strategy.ForcesWinIn, LE.le, OfNat.ofNat
Proof uses: Decidable.byContradiction, Not, Imo2024P5.Strategy.not_forcesWinIn_two, Imo2024P5.Strategy.ForcesWinIn.mono
6 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Imo2024P5.fn0 The first attempt in a winning strategy, as a function: first pass along the second row to locate the monster there line 510 source
Source documentation
The first attempt in a winning strategy, as a function: first pass along the second row to locate the monster there.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Imo2024P5.Cell
Proof uses: ite, Eq, Prod.mk, dite, LT.lt, Fin.mk, HSub.hSub, Not
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def fn0 (N : ℕ) : Fin (2 * N + 2) → Cell N :=
…
```
Mentions: Imo2024P5.Cell
lemma Imo2024P5.injective_fn0 line 515 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Function.Injective, Fin, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Imo2024P5.Cell, Imo2024P5.fn0
Proof uses: Eq, LT.lt, Fin.mk, Eq.mpr, ite, Prod.mk, dite, HSub.hSub, Eq.mpr_prop, Eq.refl, Not, Eq.mpr_not, id, implies_congr, congr, congrArg, ite_congr, Prod, dite_congr, congrFun' and 17 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Imo2024P5.path0 The first attempt in a winning strategy, as a Path line 521 source
Source documentation
The first attempt in a winning strategy, as a Path.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.Path
Proof uses: Imo2024P5.Path.ofFn, HAdd.hAdd, HMul.hMul, Imo2024P5.fn0
12 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
def path0 (hN : 2 ≤ N) : Path N := Path.ofFn (fn0 N) (by lia) (by simp [fn0])
…
```
Mentions: Imo2024P5.Path, Imo2024P5.Path.ofFn, Imo2024P5.fn0
def Imo2024P5.fn1OfNotEdge The second attempt in a winning strategy, as a function, if the monster in the second row is not at an edge: pass to the left of that monster then along its column line 530 source
Source documentation
The second attempt in a winning strategy, as a function, if the monster in the second row is not at an edge: pass to the left of that monster then along its column.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Imo2024P5.Cell
Proof uses: dite, LE.le, Prod.mk, Fin.mk, HSub.hSub, Not
19 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def fn1OfNotEdge {c₁ : Fin (N + 1)} (hc₁ : c₁ ≠ 0) : Fin (N + 3) → Cell N :=
…
```
Mentions: Imo2024P5.Cell
def Imo2024P5.path1OfNotEdge The second attempt in a winning strategy, as a function, if the monster in the second row is not at an edge line 536 source
Source documentation
The second attempt in a winning strategy, as a function, if the monster in the second row is not at an edge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Imo2024P5.Path
Proof uses: Imo2024P5.Path.ofFn, Imo2024P5.fn1OfNotEdge
15 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
def path1OfNotEdge {c₁ : Fin (N + 1)} (hc₁ : c₁ ≠ 0) : Path N := Path.ofFn (fn1OfNotEdge hc₁)
…
```
Mentions: Imo2024P5.Path, Imo2024P5.Path.ofFn, Imo2024P5.fn1OfNotEdge
def Imo2024P5.fn2OfNotEdge The third attempt in a winning strategy, as a function, if the monster in the second row is not at an edge: pass to the right of that monster then along its column line 548 source
Source documentation
The third attempt in a winning strategy, as a function, if the monster in the second row is not at an edge: pass to the right of that monster then along its column.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Imo2024P5.Cell
Proof uses: dite, LE.le, Prod.mk, Fin.mk, Not, HSub.hSub
15 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def fn2OfNotEdge {c₁ : Fin (N + 1)} (hc₁ : (c₁ : ℕ) ≠ N) : Fin (N + 3) → Cell N :=
…
```
Mentions: Imo2024P5.Cell
def Imo2024P5.path2OfNotEdge The third attempt in a winning strategy, as a function, if the monster in the second row is not at an edge line 554 source
Source documentation
The third attempt in a winning strategy, as a function, if the monster in the second row is not at an edge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Imo2024P5.Path
Proof uses: Imo2024P5.Path.ofFn, Imo2024P5.fn2OfNotEdge
12 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
def path2OfNotEdge {c₁ : Fin (N + 1)} (hc₁ : (c₁ : ℕ) ≠ N) : Path N := Path.ofFn (fn2OfNotEdge hc₁)
…
```
Mentions: Imo2024P5.Path, Imo2024P5.Path.ofFn, Imo2024P5.fn2OfNotEdge
def Imo2024P5.fn1OfEdge0 Documented declaration: fn1OfEdge0 line 565 source
Source documentation
The second attempt in a winning strategy, as a function, if the monster in the second row is at the left edge: zigzag across the board so that, if we encounter a monster, we have a third path we know will not encounter a monster.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Imo2024P5.Cell
Proof uses: dite, Eq, Prod.mk, Fin.mk, Not, HDiv.hDiv
18 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def fn1OfEdge0 (N : ℕ) : Fin (2 * N + 1) → Cell N :=
…
```
Mentions: Imo2024P5.Cell
def Imo2024P5.path1OfEdge0 The second attempt in a winning strategy, as a Path, if the monster in the second row is at the left edge line 571 source
Source documentation
The second attempt in a winning strategy, as a Path, if the monster in the second row is at the left edge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.Path
Proof uses: Imo2024P5.Path.ofFn, HAdd.hAdd, HMul.hMul, Imo2024P5.fn1OfEdge0
12 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
def path1OfEdge0 (hN : 2 ≤ N) : Path N := Path.ofFn (fn1OfEdge0 N) (by lia)
…
```
Mentions: Imo2024P5.Path, Imo2024P5.Path.ofFn, Imo2024P5.fn1OfEdge0
def Imo2024P5.path1OfEdgeN The second attempt in a winning strategy, as a Path, if the monster in the second row is at the right edge line 581 source
Source documentation
The second attempt in a winning strategy, as a Path, if the monster in the second row is at the right edge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.Path
Proof uses: Imo2024P5.Path.reflect, Imo2024P5.path1OfEdge0
4 instances, coercions and auxiliary constants left out.
```
def path1OfEdgeN (hN : 2 ≤ N) : Path N := (path1OfEdge0 hN).reflect
```
Mentions: Imo2024P5.Path, Imo2024P5.path1OfEdge0
def Imo2024P5.fn2OfEdge0 Documented declaration: fn2OfEdge0 line 587 source
Source documentation
The third attempt in a winning strategy, as a function, if the monster in the second row is at the left edge and the second (zigzag) attempt encountered a monster: on the row before the monster was encountered, move to the following row one place earlier, proceed to the left edge and then along that column.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, LE.le, HSub.hSub, HMul.hMul, Imo2024P5.Cell
Proof uses: dite, LT.lt, Prod.mk, Fin.mk, HDiv.hDiv, Not
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def fn2OfEdge0 {r : Fin (N + 2)} (hr : (r : ℕ) ≤ N) : Fin (N + 2 * r - 1) → Cell N :=
…
```
Mentions: Imo2024P5.Cell
lemma Imo2024P5.fn2OfEdge0_apply_eq_fn1OfEdge0_apply_of_lt line 593 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, LE.le, LT.lt, HMul.hMul, Eq, Imo2024P5.Cell, Imo2024P5.fn2OfEdge0, Fin.mk, HSub.hSub, Imo2024P5.fn1OfEdge0
Proof uses: Eq.mpr, dite, Prod.mk, Not, HDiv.hDiv, id, congrArg, congrFun', dite_eq_left, And, Eq.trans, Prod, Prod.fst, Prod.snd, congr, dite_eq_right, of_eq_true, eq_self
43 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def Imo2024P5.path2OfEdge0 The third attempt in a winning strategy, as a Path, if the monster in the second row is at the left edge and the second (zigzag) attempt encountered a monster line 600 source
Source documentation
The third attempt in a winning strategy, as a Path, if the monster in the second row is at the left edge and the second (zigzag) attempt encountered a monster.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HAdd.hAdd, Imo2024P5.Path
Proof uses: Imo2024P5.Path.ofFn, HSub.hSub, HMul.hMul, Imo2024P5.fn2OfEdge0
18 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
def path2OfEdge0 (hN : 2 ≤ N) {r : Fin (N + 2)} (hr2 : 2 ≤ (r : ℕ)) (hrN : (r : ℕ) ≤ N) : Path N :=
…
```
Mentions: Imo2024P5.Path
def Imo2024P5.path2OfEdge0Def Documented declaration: path2OfEdge0Def line 613 source
Source documentation
The third attempt in a winning strategy, as a Path, if the monster in the second row is at the left edge and the second (zigzag) attempt encountered a monster, version that works with junk values of r for convenience in defining the strategy before needing to prove things about exactly where it can encounter monsters.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HAdd.hAdd, Imo2024P5.Path
Proof uses: dite, And, Imo2024P5.path2OfEdge0, Not, Fin.mk
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def path2OfEdge0Def (hN : 2 ≤ N) (r : Fin (N + 2)) : Path N :=
…
```
Mentions: Imo2024P5.Path
def Imo2024P5.path2OfEdgeNDef The third attempt in a winning strategy, as a Path, if the monster in the second row is at the right edge and the second (zigzag) attempt encountered a monster line 619 source
Source documentation
The third attempt in a winning strategy, as a Path, if the monster in the second row is at the right edge and the second (zigzag) attempt encountered a monster.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HAdd.hAdd, Imo2024P5.Path
Proof uses: Imo2024P5.Path.reflect, Imo2024P5.path2OfEdge0Def
8 instances, coercions and auxiliary constants left out.
```
def path2OfEdgeNDef (hN : 2 ≤ N) (r : Fin (N + 2)) : Path N :=
…
```
Mentions: Imo2024P5.Path
def Imo2024P5.path1 The second attempt in a winning strategy, given the column of the monster in the second row, as a Path line 624 source
Source documentation
The second attempt in a winning strategy, given the column of the monster in the second row, as a Path.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HAdd.hAdd, Imo2024P5.Path
Proof uses: dite, Eq, Imo2024P5.path1OfEdge0, Not, ite, Imo2024P5.path1OfEdgeN, Imo2024P5.path1OfNotEdge
13 instances, coercions and auxiliary constants left out.
```
def path1 (hN : 2 ≤ N) (c₁ : Fin (N + 1)) : Path N :=
…
```
Mentions: Imo2024P5.Path
def Imo2024P5.path2 The third attempt in a winning strategy, given the column of the monster in the second row and the row of the monster (if any) found in the second attempt, as a Path line 631 source
Source documentation
The third attempt in a winning strategy, given the column of the monster in the second row and the row of the monster (if any) found in the second attempt, as a Path.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HAdd.hAdd, Imo2024P5.Path
Proof uses: ite, Eq, Imo2024P5.path2OfEdge0Def, dite, Imo2024P5.path2OfEdgeNDef, Not, Imo2024P5.path2OfNotEdge
13 instances, coercions and auxiliary constants left out.
```
def path2 (hN : 2 ≤ N) (c₁ : Fin (N + 1)) (r : Fin (N + 2)) : Path N :=
…
```
Mentions: Imo2024P5.Path
def Imo2024P5.winningStrategy A strategy that wins in three attempts line 637 source
Source documentation
A strategy that wins in three attempts.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.Strategy
Proof uses: Fin, Option, Imo2024P5.Cell, Imo2024P5.Path, Unit, Imo2024P5.path0, Imo2024P5.path1, Prod.snd, HAdd.hAdd, Option.getD, Imo2024P5.path2, Prod.fst
14 instances, coercions and auxiliary constants left out.
```
def winningStrategy (hN : 2 ≤ N) : Strategy N
  | 0 => fun _ ↦ path0 hN
  | 1 => fun r => path1 hN ((r 0).getD 0).2
  | _ + 2 => fun r => path2 hN ((r 0).getD 0).2 ((r 1).getD 0).1
```
Mentions: Imo2024P5.Strategy, Imo2024P5.path0, Imo2024P5.path1, Imo2024P5.path2
lemma Imo2024P5.path0_firstMonster_eq_apply_row1 line 642 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.MonsterData, Eq, Option, Imo2024P5.Cell, Imo2024P5.Path.firstMonster, Imo2024P5.path0, Option.some, Prod, Fin, HAdd.hAdd, Prod.mk, Imo2024P5.InteriorRow, Imo2024P5.row1
Proof uses: id, Imo2024P5.Path.ofFn, HMul.hMul, Imo2024P5.fn0, List.find?, Decidable.decide, Membership.mem, Set, Imo2024P5.MonsterData.monsterCells, Classical.propDecidable, Imo2024P5.Path.cells, Fin.mk, Eq.mpr, ite, dite, LT.lt, HSub.hSub, Eq.mpr_prop, Eq.refl, Not and 64 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.winningStrategy_play_one line 671 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.MonsterData, Eq, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Imo2024P5.winningStrategy, Fin.mk, Imo2024P5.Path.firstMonster, Imo2024P5.path1, Imo2024P5.InteriorRow, Fin, HAdd.hAdd, Imo2024P5.row1
Proof uses: Eq.mpr, Nat.succ, Matrix.vecCons, Fin.elim0, Matrix.vecEmpty, id, congrFun', congrArg, Imo2024P5.Strategy.play_one, Prod.snd, Option.getD, Imo2024P5.path0, Option.some, Prod, Prod.mk, Imo2024P5.Path, Imo2024P5.path1.congr_simp, Imo2024P5.path0_firstMonster_eq_apply_row1, Eq.refl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.winningStrategy_play_two line 677 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.MonsterData, Eq, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Imo2024P5.winningStrategy, Fin.mk, Imo2024P5.Path.firstMonster, Imo2024P5.path2, Imo2024P5.InteriorRow, Fin, HAdd.hAdd, Imo2024P5.row1, Prod.fst, Option.getD, Imo2024P5.path1
Proof uses: Eq.mpr, Nat.succ, Matrix.vecCons, Fin.elim0, Matrix.vecEmpty, id, congrFun', congrArg, Imo2024P5.Strategy.play_two, Prod.snd, Imo2024P5.path0, Option.some, Prod, Prod.mk, Imo2024P5.Path, Imo2024P5.path2.congr_simp, congr, Imo2024P5.path0_firstMonster_eq_apply_row1, Imo2024P5.path1.congr_simp, Eq.refl
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.path1_firstMonster_of_not_edge line 684 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.MonsterData, Ne, Fin, HAdd.hAdd, Imo2024P5.InteriorRow, Imo2024P5.row1, Or, Eq, Option, Imo2024P5.Cell, Imo2024P5.Path.firstMonster, Imo2024P5.path1, Option.none, Option.some, Prod, Prod.mk, Fin.mk and 1 more
Proof uses: Imo2024P5.Path.firstMonster_none_or_some, Membership.mem, List, Imo2024P5.Path.cells, Imo2024P5.fn1OfNotEdge, of_eq_false, eq_false, Exists, Not, Set, Imo2024P5.MonsterData.monsterCells, Eq.mp, Eq.trans, List.ofFn, congrFun', congrArg, Imo2024P5.Path, Imo2024P5.Path.ofFn, dite, Imo2024P5.path1OfEdge0 and 44 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.path2_firstMonster_of_not_edge line 711 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.MonsterData, Ne, Fin, HAdd.hAdd, Imo2024P5.InteriorRow, Imo2024P5.row1, Or, Eq, Option, Imo2024P5.Cell, Imo2024P5.Path.firstMonster, Imo2024P5.path2, Option.none, Option.some, Prod, Prod.mk, Fin.mk
Proof uses: Imo2024P5.Path.firstMonster_none_or_some, Membership.mem, List, Imo2024P5.Path.cells, Imo2024P5.fn2OfNotEdge, of_eq_false, eq_false, Exists, Not, Set, Imo2024P5.MonsterData.monsterCells, Eq.mp, Eq.trans, List.ofFn, congrFun', congrArg, Imo2024P5.Path, Imo2024P5.Path.ofFn, ite, Imo2024P5.path2OfEdge0Def and 44 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.winningStrategy_play_one_eq_none_or_play_two_eq_none_of_not_edge line 737 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.MonsterData, Ne, Fin, HAdd.hAdd, Imo2024P5.InteriorRow, Imo2024P5.row1, Or, Eq, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Imo2024P5.winningStrategy, Fin.mk, Option.none
Proof uses: Eq.mpr, Imo2024P5.Path.firstMonster, Imo2024P5.path1, id, congrArg, Imo2024P5.winningStrategy_play_one, Imo2024P5.path2, Prod.fst, Option.getD, Imo2024P5.winningStrategy_play_two, Option.some, Prod, Prod.mk, HSub.hSub, Imo2024P5.path1_firstMonster_of_not_edge, Or.inl, Or.inr, Imo2024P5.path2_firstMonster_of_not_edge, Membership.mem, Set and 25 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.path2OfEdge0_firstMonster_eq_none_of_path1OfEdge0_firstMonster_eq_some line 758 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.Cell, HAdd.hAdd, Prod.fst, Fin, Imo2024P5.MonsterData, Eq, Imo2024P5.InteriorRow, Imo2024P5.row1, Option, Imo2024P5.Path.firstMonster, Imo2024P5.path1OfEdge0, Option.some, Imo2024P5.path2OfEdge0, Option.none
Proof uses: Eq.mpr, Imo2024P5.Path.ofFn, HSub.hSub, HMul.hMul, Imo2024P5.fn2OfEdge0, id, congrArg, Imo2024P5.Path, Not, Membership.mem, Set, Imo2024P5.MonsterData.monsterCells, propext, Imo2024P5.Path.ofFn_firstMonster_eq_none, Exists, And, Imo2024P5.fn1OfEdge0, LT.lt, Eq.mp, Bool and 48 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.winningStrategy_play_one_eq_none_or_play_two_eq_none_of_edge_zero line 799 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.MonsterData, Eq, Fin, HAdd.hAdd, Imo2024P5.InteriorRow, Imo2024P5.row1, Or, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Imo2024P5.winningStrategy, Fin.mk, Option.none
Proof uses: Eq.mpr, Not, id, congrArg, propext, Classical.or_iff_not_imp_left, Option.some, Exists, Eq.mp, Ne, Option.ne_none_iff_exists, Eq.symm, ne_eq, Imo2024P5.Path.firstMonster, Imo2024P5.path2, Prod.fst, Option.getD, Imo2024P5.path1, Imo2024P5.winningStrategy_play_two, Imo2024P5.winningStrategy_play_one and 55 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.winningStrategy_play_one_two_of_edge_N line 838 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.MonsterData, Eq, HAdd.hAdd, Imo2024P5.InteriorRow, Fin, Imo2024P5.row1, And, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Imo2024P5.winningStrategy, Fin.mk, Option.map, Imo2024P5.Cell.reflect, Imo2024P5.MonsterData.reflect
Proof uses: Ne, Imo2024P5.MonsterData.apply_row1_ne_zero_of_apply_row1_eq_N, Imo2024P5.MonsterData.reflect_apply_row1_eq_zero_of_apply_row1_eq_N, And.intro, Eq.mpr, Imo2024P5.Path.firstMonster, Imo2024P5.path1, id, congr, congrArg, Imo2024P5.winningStrategy_play_one, dite, Imo2024P5.Path, Imo2024P5.path1OfEdge0, Not, ite, Imo2024P5.path1OfEdgeN, Imo2024P5.path1OfNotEdge, Imo2024P5.Path.reflect, congrFun' and 35 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.winningStrategy_play_one_eq_none_or_play_two_eq_none_of_edge_N line 861 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.MonsterData, Eq, HAdd.hAdd, Imo2024P5.InteriorRow, Fin, Imo2024P5.row1, Or, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Imo2024P5.winningStrategy, Fin.mk, Option.none
Proof uses: Option.map, Imo2024P5.Cell.reflect, Imo2024P5.MonsterData.reflect, And, Imo2024P5.winningStrategy_play_one_two_of_edge_N, Eq.mpr, id, congrFun', congrArg, congr, Imo2024P5.MonsterData.reflect_apply_row1_eq_zero_of_apply_row1_eq_N, Imo2024P5.winningStrategy_play_one_eq_none_or_play_two_eq_none_of_edge_zero
23 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.winningStrategy_play_one_eq_none_or_play_two_eq_none line 871 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.MonsterData, Or, Eq, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Imo2024P5.winningStrategy, Fin.mk, Option.none
Proof uses: dite, Fin, HAdd.hAdd, Imo2024P5.InteriorRow, Imo2024P5.row1, Imo2024P5.winningStrategy_play_one_eq_none_or_play_two_eq_none_of_edge_zero, Not, Imo2024P5.winningStrategy_play_one_eq_none_or_play_two_eq_none_of_edge_N, Imo2024P5.winningStrategy_play_one_eq_none_or_play_two_eq_none_of_not_edge
18 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P5.winningStrategy_forcesWinIn_three line 880 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P5.Strategy.ForcesWinIn, Imo2024P5.winningStrategy
Proof uses: Imo2024P5.MonsterData, Eq, Option, Imo2024P5.Cell, Imo2024P5.Strategy.play, Fin.mk, Option.none, Or, Imo2024P5.Strategy.WinsIn, Imo2024P5.winningStrategy_play_one_eq_none_or_play_two_eq_none, Exists.intro, Fin, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false
13 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
determine Imo2024P5.answer line 889 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Imo2024P5.imo2024_p5 line 891 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Exists, Imo2024P5.Strategy, OfNat.ofNat, Imo2024P5.Strategy.ForcesWinIn, Imo2024P5.answer
Proof uses: id, Eq.mpr, And, Membership.mem, Set, lowerBounds, LE.le, Eq, congrArg, congr, forall_congr, implies_congr, Eq.refl, And.intro, Exists.intro, Imo2024P5.winningStrategy, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Bool, Bool.true and 2 more
15 instances, coercions and auxiliary constants left out.

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