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

34 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1993, Problem 3

On an infinite chessboard a game is played as follows. At the start n² pieces are arranged in an n × n block of adjoining squares, one piece on each square. A move in the game is a jump in a horizontal or vertical direction over an adjacent occupied square to an unoccupied square immediately beyond. The piece which has been jumped over is removed. Find those values of n for which the game can end with only one piece remaining on the board.

Imports (2)

Imported by 1 file

Compfiles.lean

abbrev Imo1993P3.dirs The four unit directions in which a jump is allowed line 31 source
Source documentation
The four unit directions in which a jump is allowed.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: Insert.insert, Prod.mk, OfNat.ofNat, Neg.neg, Singleton.singleton
6 instances, coercions and auxiliary constants left out.
```
abbrev dirs : Finset (ℤ × ℤ) := {(1, 0), (-1, 0), (0, 1), (0, -1)}
```
def Imo1993P3.initPos The initial position: an n × n block of occupied squares line 34 source
Source documentation
The initial position: an n × n block of occupied squares.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Int
Proof uses: SProd.sprod, Finset.Ico, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.
```
noncomputable def initPos (n : ℕ) : Finset (ℤ × ℤ) := Ico 0 (n : ℤ) ×ˢ Ico 0 (n : ℤ)
```
lemma Imo1993P3.mem_initPos line 36 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Int, Iff, Membership.mem, Finset, Imo1993P3.initPos, And, LE.le, OfNat.ofNat, Prod.fst, LT.lt, Prod.snd
Proof uses: Eq.mpr, id, Eq, congrFun', congrArg, Eq.trans, SProd.sprod, Finset.Ico, congr
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo1993P3.IsMove A single move: the piece at c jumps over the adjacent piece at c + d onto the empty square c + d + d; the jumped-over piece is removed line 43 source
Source documentation
A single move: the piece at c jumps over the adjacent piece at c + d onto the empty square c + d + d; the jumped-over piece is removed.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: Exists, Subtype, Membership.mem, Imo1993P3.dirs, And, HAdd.hAdd, Not, Eq, Insert.insert, Finset.erase
9 instances, coercions and auxiliary constants left out.
```
def IsMove (s s' : Finset (ℤ × ℤ)) : Prop :=
…
```
def Imo1993P3.Solvable The game is solvable for n if the n × n block can be reduced to a single piece, i.e. a one-piece position is reachable from the initial position by a sequence of moves line 49 source
Source documentation
The game is solvable for n if the n × n block can be reduced to a single piece, i.e. a one-piece position is reachable from the initial position by a sequence of moves.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Exists, Prod, Int, Relation.ReflTransGen, Finset, Imo1993P3.IsMove, Imo1993P3.initPos, Singleton.singleton
1 instances, coercions and auxiliary constants left out.
```
def Solvable (n : ℕ) : Prop := ∃ c : ℤ × ℤ, Relation.ReflTransGen IsMove (initPos n) {c}
```
Mentions: Imo1993P3.IsMove, Imo1993P3.initPos
determine Imo1993P3.SolutionSet line 51 source
no axioms what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, And, LT.lt, OfNat.ofNat, Not, Dvd.dvd
3 instances, coercions and auxiliary constants left out.
def Imo1993P3.g1 Weight functions on the exponents: cells with (i + j) % 3 = r get weight 1 for the two classes in question and 0 for the remaining one line 59 source
Source documentation
Weight functions on the exponents: cells with (i + j) % 3 = r get weight 1 for the two classes in question and 0 for the remaining one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, ZMod, OfNat.ofNat, Nat
Proof uses: ite, Eq, HMod.hMod
20 instances, coercions and auxiliary constants left out.
```
def g1 (k : ℤ) : ZMod 2 := if k % 3 = 2 then 0 else 1
```
def Imo1993P3.g2 line 61 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, ZMod, OfNat.ofNat, Nat
Proof uses: ite, Eq, HMod.hMod
20 instances, coercions and auxiliary constants left out.
def Imo1993P3.Wt The total weight of a position line 64 source
Source documentation
The total weight of a position.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, ZMod, OfNat.ofNat, Nat, Finset, Prod
Proof uses: Finset.sum, HAdd.hAdd, Prod.fst, Prod.snd
10 instances, coercions and auxiliary constants left out.
```
def Wt (g : ℤ → ZMod 2) (s : Finset (ℤ × ℤ)) : ZMod 2 := ∑ c ∈ s, g (c.1 + c.2)
```
lemma Imo1993P3.g1_sum3 line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, ZMod, OfNat.ofNat, Nat, HAdd.hAdd, Imo1993P3.g1
Proof uses: HMod.hMod, Or, Eq.mpr, ite, id, congrFun', congrArg, congr, ite_congr, Eq.refl, Not, Eq.trans, Mathlib.Meta.NormNum.instAtLeastTwo, ite_eq_right_of_eq_false, eq_false, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Bool, Bool.false, Mathlib.Meta.NormNum.instAddMonoidWithOne and 17 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P3.g2_sum3 line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, ZMod, OfNat.ofNat, Nat, HAdd.hAdd, Imo1993P3.g2
Proof uses: HMod.hMod, Or, Eq.mpr, ite, True, id, congrFun', congrArg, congr, ite_congr, Eq.trans, eq_self, Eq.refl, Not, Mathlib.Meta.NormNum.instAtLeastTwo, ite_eq_left_of_eq_true, eq_true, True.intro, ite_eq_right_of_eq_false, eq_false and 17 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P3.Wt_move A move changes the weight by g x + g (x+δ) + g (x+2δ) = 0 line 79 source
Source documentation
A move changes the weight by g x + g (x+δ) + g (x+2δ) = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, ZMod, OfNat.ofNat, Nat, Eq, HAdd.hAdd, Finset, Prod, Imo1993P3.IsMove, Imo1993P3.Wt
Proof uses: Exists, Subtype, Membership.mem, Imo1993P3.dirs, And, Not, Insert.insert, Finset.erase, Prod.mk, Subtype.mk, id, Or, Neg.neg, Eq.mp, Eq.trans, Singleton.singleton, congr, congrArg, Prod.mk.injEq, of_eq_true and 88 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma Wt_move {g : ℤ → ZMod 2} (hg : ∀ t : ℤ, g t + g (t + 1) + g (t + 2) = 0)
    {s s' : Finset (ℤ × ℤ)} (h : IsMove s s') : Wt g s' = Wt g s := by
…
```
Mentions: h, Imo1993P3.IsMove, Imo1993P3.Wt
lemma Imo1993P3.Wt_reachable line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, ZMod, OfNat.ofNat, Nat, Eq, HAdd.hAdd, Finset, Prod, Relation.ReflTransGen, Imo1993P3.IsMove, Imo1993P3.Wt
Proof uses: Relation.ReflTransGen.rec, Eq.refl, Eq.trans, Eq.symm, Imo1993P3.Wt_move
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P3.gsum_interval The sum of a period-3 weight with zero triple-sum over 3m consecutive integers is zero line 117 source
Source documentation
The sum of a period-3 weight with zero triple-sum over 3m consecutive integers is zero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, ZMod, OfNat.ofNat, Nat, Eq, HAdd.hAdd, Finset.sum, Finset.Ico, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.sum_congr, EmptyCollection.emptyCollection, Finset, CharP.cast_eq_zero, MulZeroClass.mul_zero, add_zero, Finset.Ico_eq_empty_of_le, LE.le, Membership.mem, Eq.refl, eq_self, Eq.mpr, id, Nat.cast_add and 41 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma gsum_interval {g : ℤ → ZMod 2} (hg : ∀ t : ℤ, g t + g (t + 1) + g (t + 2) = 0)
    (a : ℤ) (m : ℕ) : ∑ k ∈ Finset.Ico a (a + 3 * (m : ℤ)), g k = 0 := by
…
```
lemma Imo1993P3.Wt_init The weight of the initial 3m × 3m block is zero line 142 source
Source documentation
The weight of the initial 3m × 3m block is zero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, ZMod, OfNat.ofNat, Nat, Eq, HAdd.hAdd, Imo1993P3.Wt, Imo1993P3.initPos, HMul.hMul
Proof uses: Eq.mpr, id, congrFun', congrArg, Nat.cast_mul, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_mul and 23 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma Wt_init {g : ℤ → ZMod 2} (hg : ∀ t : ℤ, g t + g (t + 1) + g (t + 2) = 0) (m : ℕ) :
    Wt g (initPos (3 * m)) = 0 := by
…
```
Mentions: Imo1993P3.Wt, Imo1993P3.initPos
lemma Imo1993P3.not_solvable_of_three_dvd If 3 ∣ n the game cannot end with one piece: the two weights of the initial block are (0, 0), but the weights of a single piece are never (0, 0) line 156 source
Source documentation
If 3 ∣ n the game cannot end with one piece: the two weights of the initial block are (0, 0), but the weights of a single piece are never (0, 0).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, OfNat.ofNat, Not, Imo1993P3.Solvable
Proof uses: Eq, HMul.hMul, Prod, Int, Relation.ReflTransGen, Finset, Imo1993P3.IsMove, Imo1993P3.initPos, Singleton.singleton, False, ZMod, Imo1993P3.Wt, Imo1993P3.g1, Imo1993P3.Wt_reachable, Imo1993P3.g1_sum3, Imo1993P3.g2, Imo1993P3.g2_sum3, HMod.hMod, HAdd.hAdd, Prod.fst and 26 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma not_solvable_of_three_dvd {n : ℕ} (h3 : 3 ∣ n) : ¬ Solvable n := by
…
```
Mentions: Imo1993P3.Solvable
lemma Imo1993P3.unit_facts Arithmetic facts about two perpendicular unit directions line 175 source
Source documentation
Arithmetic facts about two perpendicular unit directions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Membership.mem, Finset, Imo1993P3.dirs, Eq, HAdd.hAdd, HMul.hMul, Prod.fst, Prod.snd, OfNat.ofNat, And, Or, Ne, Not, Neg.neg
Proof uses: Prod.mk, Eq.mp, Eq.trans, Insert.insert, Singleton.singleton, congrArg, False.elim, False, congrFun', congr, mul_one, MulZeroClass.mul_zero, add_zero, Nat, Eq.symm, mul_neg, of_eq_true, True, not_false_eq_true, eq_self and 7 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma unit_facts {u w : ℤ × ℤ} (hu : u ∈ dirs) (hw : w ∈ dirs)
    (hperp : u.1 * w.1 + u.2 * w.2 = 0) :
    (u.1 ≠ 0 ∨ u.2 ≠ 0) ∧ (w.1 ≠ 0 ∨ w.2 ≠ 0) ∧ ¬ (u.1 = w.1 ∧ u.2 = w.2) ∧
      ¬ (u.1 = -w.1 ∧ u.2 = -w.2) ∧ ¬ (u.1 + u.1 = w.1 ∧ u.2 + u.2 = w.2) ∧
      ¬ (u.1 + u.1 = -w.1 ∧ u.2 + u.2 = -w.2) := by
…
```
Mentions: Imo1993P3.dirs
lemma Imo1993P3.purge Documented declaration: purge line 189 source
Source documentation
The key purge: three consecutive pieces p, p + u, p + u + u in a line can be removed from the board (everything else unchanged) using a catalyst piece at p + w provided the square p - w is empty. The sequence is: p + w jumps over p to p - w; p + u + u jumps over p + u to p; p - w jumps over p to p + w.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo1993P3.dirs, Eq, HAdd.hAdd, HMul.hMul, Prod.fst, Prod.snd, OfNat.ofNat, Not, HSub.hSub, Relation.ReflTransGen, Imo1993P3.IsMove, SDiff.sdiff, Insert.insert, Singleton.singleton
Proof uses: Or, Ne, And, Neg.neg, Imo1993P3.unit_facts, Prod.mk, And.intro, Eq.mpr, id, congrArg, Finset.erase, Exists.intro, Exists, Subtype, Subtype.mk, Eq.trans, Eq.mp, of_eq_true, False, True and 38 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 125 steps
Open to load the checked before-and-after goal states.
```
lemma purge {s : Finset (ℤ × ℤ)} {p u w : ℤ × ℤ}
    (hu : u ∈ dirs) (hw : w ∈ dirs) (hperp : u.1 * w.1 + u.2 * w.2 = 0)
    (hp : p ∈ s) (hpu : p + u ∈ s) (hp2 : p + u + u ∈ s) (hpw : p + w ∈ s)
    (hnw : p - w ∉ s) :
    Relation.ReflTransGen IsMove s (s \ {p, p + u, p + u + u}) := by
…
```
Mentions: Imo1993P3.dirs, Imo1993P3.IsMove
def Imo1993P3.stateA After clearing k columns of the top strip: the board below row n plus columns k, k+1, ... of the whole square line 334 source
Source documentation
After clearing k columns of the top strip: the board below row n plus columns k, k+1, ... of the whole square.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Int
Proof uses: Finset.filter, Or, LT.lt, Prod.snd, LE.le, Prod.fst, Imo1993P3.initPos, HAdd.hAdd, OfNat.ofNat
10 instances, coercions and auxiliary constants left out.
```
noncomputable def stateA (n k : ℕ) : Finset (ℤ × ℤ) :=
…
```
def Imo1993P3.stateB After clearing k rows of the right strip line 338 source
Source documentation
After clearing k rows of the right strip.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Int
Proof uses: Finset.filter, Or, And, LT.lt, Prod.fst, Prod.snd, LE.le, HSub.hSub, HAdd.hAdd, OfNat.ofNat, Imo1993P3.initPos
15 instances, coercions and auxiliary constants left out.
```
noncomputable def stateB (n k : ℕ) : Finset (ℤ × ℤ) :=
…
```
def Imo1993P3.stateC After clearing the bottom of column n + 2 as well line 343 source
Source documentation
After clearing the bottom of column n + 2 as well.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Int
Proof uses: Finset.filter, Or, And, LT.lt, Prod.fst, Prod.snd, LE.le, HAdd.hAdd, OfNat.ofNat, Imo1993P3.initPos
13 instances, coercions and auxiliary constants left out.
```
noncomputable def stateC (n : ℕ) : Finset (ℤ × ℤ) :=
…
```
def Imo1993P3.stateD After clearing the bottom of columns n + 1, n + 2 line 348 source
Source documentation
After clearing the bottom of columns n + 1, n + 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Int
Proof uses: Finset.filter, Or, And, LT.lt, Prod.fst, Prod.snd, Eq, LE.le, OfNat.ofNat, Imo1993P3.initPos, HAdd.hAdd
13 instances, coercions and auxiliary constants left out.
```
noncomputable def stateD (n : ℕ) : Finset (ℤ × ℤ) :=
…
```
lemma Imo1993P3.phase1_step One step of phase 1: purge the vertical triple in column k of the top strip, using the piece at (k+1, n) as catalyst line 354 source
Source documentation
One step of phase 1: purge the vertical triple in column k of the top strip, using the piece at (k+1, n) as catalyst.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Relation.ReflTransGen, Finset, Prod, Int, Imo1993P3.IsMove, Imo1993P3.stateA, HAdd.hAdd, OfNat.ofNat
Proof uses: SDiff.sdiff, Insert.insert, Prod.mk, Singleton.singleton, Imo1993P3.purge, of_decide_eq_true, Membership.mem, Imo1993P3.dirs, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, HMul.hMul, Prod.fst, Prod.snd, Eq.mpr, And, LE.le and 12 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma phase1_step (n k : ℕ) (hk : k < n) :
    Relation.ReflTransGen IsMove (stateA n k) (stateA n (k + 1)) := by
…
```
Mentions: Imo1993P3.IsMove, Imo1993P3.stateA
lemma Imo1993P3.phase1 Phase 1: clear the top strip, one column at a time line 370 source
Source documentation
Phase 1: clear the top strip, one column at a time.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Relation.ReflTransGen, Finset, Prod, Int, Imo1993P3.IsMove, Imo1993P3.initPos, HAdd.hAdd, OfNat.ofNat, Imo1993P3.stateA
Proof uses: Nat.recAux, Eq.mpr, id, Eq, congrArg, Finset.ext, Iff, Membership.mem, Prod.mk, And, LT.lt, Or, congr, Eq.trans, Finset.filter, Prod.snd, Prod.fst, congrFun', Relation.ReflTransGen.refl, Relation.ReflTransGen.trans and 2 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma phase1 (n : ℕ) (k : ℕ) (hk : k ≤ n) :
    Relation.ReflTransGen IsMove (initPos (n + 3)) (stateA n k) := by
…
```
Mentions: Imo1993P3.IsMove, Imo1993P3.initPos, Imo1993P3.stateA
lemma Imo1993P3.phase2a_step One step of phase 2a: purge the horizontal triple in row n + 2 - k of the right strip, using the piece at (n, n + 1 - k) as catalyst line 382 source
Source documentation
One step of phase 2a: purge the horizontal triple in row n + 2 - k of the right strip, using the piece at (n, n + 1 - k) as catalyst.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Relation.ReflTransGen, Finset, Prod, Int, Imo1993P3.IsMove, Imo1993P3.stateB, HAdd.hAdd, OfNat.ofNat
Proof uses: SDiff.sdiff, Insert.insert, Prod.mk, HSub.hSub, Singleton.singleton, Imo1993P3.purge, Neg.neg, of_decide_eq_true, Membership.mem, Imo1993P3.dirs, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, HMul.hMul, Prod.fst, Prod.snd, Eq.mpr and 12 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma phase2a_step (n k : ℕ) (hk : k < n) :
    Relation.ReflTransGen IsMove (stateB n k) (stateB n (k + 1)) := by
…
```
Mentions: Imo1993P3.IsMove, Imo1993P3.stateB
lemma Imo1993P3.phase2a Phase 2a: clear the right strip rows from top to bottom, down to row 3 line 399 source
Source documentation
Phase 2a: clear the right strip rows from top to bottom, down to row 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Relation.ReflTransGen, Finset, Prod, Int, Imo1993P3.IsMove, Imo1993P3.initPos, HAdd.hAdd, OfNat.ofNat, Imo1993P3.stateB
Proof uses: Nat.recAux, Eq.mpr, Imo1993P3.stateA, id, Eq, congrArg, Finset.ext, Iff, Membership.mem, Prod.mk, And, LT.lt, Or, HSub.hSub, congr, Eq.trans, Finset.filter, Prod.fst, Prod.snd, congrFun' and 5 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma phase2a (n : ℕ) (k : ℕ) (hk : k ≤ n) :
    Relation.ReflTransGen IsMove (initPos (n + 3)) (stateB n k) := by
…
```
Mentions: Imo1993P3.IsMove, Imo1993P3.initPos, Imo1993P3.stateB
lemma Imo1993P3.phase2b Phase 2b: clear the remaining 3 × 3 corner, finishing with a purge whose catalyst lies inside the target n × n block line 412 source
Source documentation
Phase 2b: clear the remaining 3 × 3 corner, finishing with a purge whose catalyst lies inside the target n × n block.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Relation.ReflTransGen, Finset, Prod, Int, Imo1993P3.IsMove, Imo1993P3.stateB, Imo1993P3.initPos
Proof uses: SDiff.sdiff, Insert.insert, Prod.mk, HAdd.hAdd, Singleton.singleton, Imo1993P3.purge, Neg.neg, of_decide_eq_true, Membership.mem, Imo1993P3.dirs, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, HMul.hMul, Prod.fst, Prod.snd, Eq.mpr and 20 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 55 steps
Open to load the checked before-and-after goal states.
```
lemma phase2b (n : ℕ) (hn : 1 ≤ n) : Relation.ReflTransGen IsMove (stateB n n) (initPos n) := by
…
```
Mentions: Imo1993P3.IsMove, Imo1993P3.stateB, Imo1993P3.initPos
lemma Imo1993P3.reduction Reduction: if the game is solvable for n ≥ 1, it is solvable for n + 3 line 449 source
Source documentation
Reduction: if the game is solvable for n ≥ 1, it is solvable for n + 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo1993P3.Solvable, HAdd.hAdd
Proof uses: Prod, Int, Relation.ReflTransGen, Finset, Imo1993P3.IsMove, Imo1993P3.initPos, Singleton.singleton, Exists.intro, Relation.ReflTransGen.trans, Imo1993P3.stateB, Imo1993P3.phase2a, le_rfl, Imo1993P3.phase2b
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma reduction (n : ℕ) (hn : 1 ≤ n) (h : Solvable n) : Solvable (n + 3) := by
…
```
Mentions: h, Imo1993P3.Solvable
lemma Imo1993P3.solvable_one The 1 × 1 board is trivially solved line 454 source
Source documentation
The 1 × 1 board is trivially solved.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1993P3.Solvable, OfNat.ofNat, Nat
Proof uses: Exists.intro, Prod, Int, Relation.ReflTransGen, Finset, Imo1993P3.IsMove, Imo1993P3.initPos, Singleton.singleton, Prod.mk, Eq.mpr, id, Eq, congrArg, Finset.ext, Iff, Membership.mem, And, LE.le, LT.lt, congr and 4 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma solvable_one : Solvable 1 := by
…
```
Mentions: Imo1993P3.Solvable
lemma Imo1993P3.solvable_two The 2 × 2 board is solved in three moves line 462 source
Source documentation
The 2 × 2 board is solved in three moves.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1993P3.Solvable, OfNat.ofNat, Nat
Proof uses: Exists.intro, Prod, Int, Relation.ReflTransGen, Finset, Imo1993P3.IsMove, Imo1993P3.initPos, Singleton.singleton, Prod.mk, Insert.insert, Finset.erase, Exists, Subtype, Membership.mem, Imo1993P3.dirs, And, HAdd.hAdd, Not, Eq, Subtype.mk and 27 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
```
lemma solvable_two : Solvable 2 := by
…
```
Mentions: Imo1993P3.Solvable
lemma Imo1993P3.solvable_three_mul_add_one line 508 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1993P3.Solvable, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Nat.recAux, Imo1993P3.solvable_one, Imo1993P3.reduction, Eq.mp, congrArg, Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, Eq.symm, Mathlib.Tactic.Ring.Common.add_mul and 13 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P3.solvable_three_mul_add_two line 516 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1993P3.Solvable, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Nat.recAux, Imo1993P3.solvable_two, Imo1993P3.reduction, Eq.mp, congrArg, Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, Eq.symm, Mathlib.Tactic.Ring.Common.add_mul and 13 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo1993P3.solvable_of_pos_not_three_dvd line 524 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Not, Dvd.dvd, Imo1993P3.Solvable
Proof uses: Or, Eq, HMod.hMod, HAdd.hAdd, HMul.hMul, HDiv.hDiv, Eq.mpr, id, congrArg, Imo1993P3.solvable_three_mul_add_one, Imo1993P3.solvable_three_mul_add_two
18 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
problem Imo1993P3.imo1993_p3 line 536 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Imo1993P3.Solvable, Membership.mem, Set, Imo1993P3.SolutionSet
Proof uses: id, Iff.intro, And, LT.lt, OfNat.ofNat, Not, Dvd.dvd, Imo1993P3.not_solvable_of_three_dvd, Decidable.byContradiction, False, Exists.intro, Eq, HMul.hMul, of_eq_true, Eq.trans, True, congrArg, MulZeroClass.mul_zero, eq_self, Eq.symm and 6 more
19 instances, coercions and auxiliary constants left out.

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