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

138 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2022, Problem 6

Let n be a positive integer. A Nordic square is an n×n board containing all the integers from 1 to n² so that each cell contains exactly one number. Two different cells are considered adjacent if they share a common side. Every cell that is adjacent only to cells containing larger numbers is called a valley. An uphill path is a sequence of one or more cells such that:

(1) the first cell in the sequence is a valley, (2) each subsequent cell in the sequence is adjacent to the previous cell, and (3) the numbers written in the cells in the sequence are in increasing order.

Find, as a function of n, the smallest possible total number of uphill paths in a Nordic square.

Imports (11)

Imported by 1 file

Compfiles.lean

abbrev Imo2022P6.Cell A cell of the board line 54 source
Source documentation
A cell of the board.

no axioms what this means
Statement uses: Nat
Proof uses: Prod, Fin
```
abbrev Cell (n : ℕ) : Type := Fin n × Fin n
```
abbrev Imo2022P6.NordicSquare A Nordic square line 57 source
Source documentation
A Nordic square.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Equiv, Imo2022P6.Cell, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow
9 instances, coercions and auxiliary constants left out.
```
abbrev NordicSquare (n : ℕ) : Type := Cell n ≃ Finset.Icc 1 (n ^ 2)
```
Mentions: Imo2022P6.Cell
def Imo2022P6.Adjacent Whether two cells are adjacent line 60 source
Source documentation
Whether two cells are adjacent.

no axioms what this means
Statement uses: Nat, Imo2022P6.Cell
Proof uses: Eq, HAdd.hAdd, Nat.dist, Prod.fst, Fin, Prod.snd, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def Adjacent {n : ℕ} (x y : Cell n) : Prop :=
…
```
Mentions: Imo2022P6.Cell
def Imo2022P6.NordicSquare.Valley The definition of a valley from the problem line 64 source
Source documentation
The definition of a valley from the problem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell
Proof uses: Imo2022P6.Adjacent, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype
14 instances, coercions and auxiliary constants left out.
```
def NordicSquare.Valley {n : ℕ} (ns : NordicSquare n) (c : Cell n) : Prop :=
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell
structure Imo2022P6.NordicSquare.UphillPath The definition of an uphill path from the problem line 68 source
Source documentation
The definition of an uphill path from the problem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare
```
structure NordicSquare.UphillPath {n : ℕ} (ns : NordicSquare n) where
…
```
Mentions: Imo2022P6.NordicSquare
theorem Imo2022P6.Adjacent.symm Adjacency is symmetric line 79 source
Source documentation
Adjacency is symmetric.

standard axioms: propext what this means
Statement uses: Nat, Imo2022P6.Cell, Imo2022P6.Adjacent
Proof uses: id, Eq.mpr, Eq, HAdd.hAdd, Nat.dist, Prod.fst, Fin, Prod.snd, OfNat.ofNat, congrArg, Nat.dist_comm
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem Adjacent.symm {n : ℕ} {x y : Cell n} (h : Adjacent x y) : Adjacent y x := by
…
```
Mentions: Imo2022P6.Cell, h, Imo2022P6.Adjacent
instance Imo2022P6.(instance at line 85) line 85 source
Source documentation
Adjacency is decidable.
```
instance {n : ℕ} (x y : Cell n) : Decidable (Adjacent x y) :=
…
```
Mentions: Imo2022P6.Cell, Imo2022P6.Adjacent
theorem Imo2022P6.Adjacent.ne Adjacent cells are distinct line 89 source
Source documentation
Adjacent cells are distinct.

standard axioms: propext what this means
Statement uses: Nat, Imo2022P6.Cell, Imo2022P6.Adjacent, Ne
Proof uses: Eq, False, False.elim, Eq.mp, Eq.trans, HAdd.hAdd, Nat.dist, Prod.fst, Fin, Prod.snd, OfNat.ofNat, congrFun', congrArg, congr, Nat.dist_self, add_zero
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem Adjacent.ne {n : ℕ} {x y : Cell n} (h : Adjacent x y) : x ≠ y := by
…
```
Mentions: Imo2022P6.Cell, h, Imo2022P6.Adjacent
theorem Imo2022P6.NordicSquare.value_ne_of_adjacent Adjacent cells have different values line 94 source
Source documentation
Adjacent cells have different values.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.Adjacent, Ne, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype
Proof uses: Eq, Imo2022P6.Adjacent.ne, Equiv.injective, Subtype.ext, Equiv
26 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.value_ne_of_adjacent {n : ℕ} (ns : NordicSquare n) {x y : Cell n}
    (h : Adjacent x y) : (ns x : ℕ) ≠ (ns y : ℕ) := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, h, Imo2022P6.Adjacent
theorem Imo2022P6.NordicSquare.exists_smaller_neighbor In a Nordic square, any non-valley cell has an adjacent cell with a smaller value line 103 source
Source documentation
In a Nordic square, any non-valley cell has an adjacent cell with a smaller value.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, Not, Imo2022P6.NordicSquare.Valley, Exists, And, Imo2022P6.Adjacent, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype
Proof uses: LE.le, Eq.mp, Eq.trans, congrArg, funext, propext, exists_prop_congr, Iff.of_eq, Eq.refl, Exists.intro, And.intro, lt_of_le_of_ne, Ne.symm, Imo2022P6.NordicSquare.value_ne_of_adjacent
37 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.exists_smaller_neighbor {n : ℕ} (ns : NordicSquare n) {c : Cell n}
    (h : ¬ ns.Valley c) : ∃ c' : Cell n, Adjacent c c' ∧ (ns c' : ℕ) < (ns c : ℕ) := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, h, Imo2022P6.Adjacent
theorem Imo2022P6.NordicSquare.valley_of_no_smaller_neighbor A cell with no smaller-valued adjacent cell is a valley line 110 source
Source documentation
A cell with no smaller-valued adjacent cell is a valley.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, Not, Exists, And, Imo2022P6.Adjacent, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype, Imo2022P6.NordicSquare.Valley
Proof uses: Decidable.byContradiction, Exists.intro, And.intro, lt_of_le_of_ne, Iff.mp, LE.le, not_lt, Ne.symm, Imo2022P6.NordicSquare.value_ne_of_adjacent
35 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.valley_of_no_smaller_neighbor {n : ℕ} (ns : NordicSquare n) {c : Cell n}
    (h : ¬ ∃ c' : Cell n, Adjacent c c' ∧ (ns c' : ℕ) < (ns c : ℕ)) : ns.Valley c := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, h, Imo2022P6.Adjacent
def Imo2022P6.NordicSquare.pathTo The path from a valley to a given cell, following decreasing values line 119 source
Source documentation
The path from a valley to a given cell, following decreasing values. This is defined by well-founded recursion on the value of the cell.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, List
Proof uses: WellFounded.Nat.fix, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype, InvImage, LT.lt, dite, Exists, And, Imo2022P6.Adjacent, Fin, Classical.choose, HAppend.hAppend, List.cons, List.nil, Not
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def NordicSquare.pathTo {n : ℕ} (ns : NordicSquare n) (c : Cell n) : List (Cell n) :=
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell
theorem Imo2022P6.NordicSquare.pathTo_ne_nil line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, Ne, List, Imo2022P6.NordicSquare.pathTo, List.nil
Proof uses: Eq.mpr, dite, Exists, And, Imo2022P6.Adjacent, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype, Fin, Classical.choose, HAppend.hAppend, List.cons, Not, id, Eq, congrArg and 13 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2022P6.NordicSquare.pathTo_props The defining property of pathTo: it is an uphill path ending at c line 135 source
Source documentation
The defining property of pathTo: it is an uphill path ending at c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, And, Eq, Option, List.head?, Imo2022P6.NordicSquare.pathTo, Option.some, Imo2022P6.NordicSquare.Valley, List.IsChain, Imo2022P6.Adjacent, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype, List.getLast?
Proof uses: Imo2022P6.NordicSquare.pathTo.induct, Exists, Classical.choose, Classical.choose_spec, Eq.mpr, dite, List, Fin, HAppend.hAppend, List.cons, List.nil, Not, id, congrArg, Imo2022P6.NordicSquare.pathTo.eq_1, dite_eq_left, And.intro, List.head, Imo2022P6.NordicSquare.pathTo_ne_nil, List.head?_eq_some_head and 25 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.pathTo_props {n : ℕ} (ns : NordicSquare n) (c : Cell n) :
    (∀ v, (pathTo ns c).head? = some v → ns.Valley v) ∧
    (pathTo ns c).IsChain Adjacent ∧
    (pathTo ns c).IsChain (fun x y ↦ (ns x : ℕ) < (ns y : ℕ)) ∧
    (pathTo ns c).getLast? = some c := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.NordicSquare.pathTo, Imo2022P6.Adjacent
def Imo2022P6.NordicSquare.uphillPathTo pathTo packaged as an uphill path line 179 source
Source documentation
pathTo packaged as an uphill path.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.NordicSquare.UphillPath
Proof uses: Imo2022P6.NordicSquare.UphillPath.mk, Imo2022P6.NordicSquare.pathTo, Imo2022P6.NordicSquare.pathTo_ne_nil
3 instances, coercions and auxiliary constants left out.
```
noncomputable def NordicSquare.uphillPathTo {n : ℕ} (ns : NordicSquare n) (c : Cell n) :
    ns.UphillPath where
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell
theorem Imo2022P6.NordicSquare.uphillPathTo_getLast? line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, Eq, Option, List.getLast?, Imo2022P6.NordicSquare.UphillPath.cells, Imo2022P6.NordicSquare.uphillPathTo, Option.some
Proof uses: And.right, List.IsChain, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype, Imo2022P6.NordicSquare.pathTo, Imo2022P6.Adjacent, And, List.head?, Imo2022P6.NordicSquare.Valley, Imo2022P6.NordicSquare.pathTo_props
14 instances, coercions and auxiliary constants left out.
def Imo2022P6.NordicSquare.minCell The cell with value 1 line 192 source
Source documentation
The cell with value 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, HAdd.hAdd, OfNat.ofNat, Imo2022P6.Cell
Proof uses: Equiv, Subtype, Membership.mem, Finset, Finset.Icc, HPow.hPow, Equiv.symm, Subtype.mk
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def NordicSquare.minCell {n : ℕ} (ns : NordicSquare (n + 1)) : Cell (n + 1) :=
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell
theorem Imo2022P6.NordicSquare.minCell_value line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, HAdd.hAdd, OfNat.ofNat, Eq, Membership.mem, Finset, Finset.Icc, HPow.hPow, Imo2022P6.Cell, Subtype, Imo2022P6.NordicSquare.minCell
Proof uses: Eq.mpr, Equiv, Equiv.symm, Subtype.mk, id, congrArg, Imo2022P6.NordicSquare.minCell.eq_1, Equiv.apply_symm_apply, Eq.refl
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2022P6.NordicSquare.minCell_valley line 199 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, HAdd.hAdd, OfNat.ofNat, Imo2022P6.NordicSquare.Valley, Imo2022P6.NordicSquare.minCell
Proof uses: Imo2022P6.Cell, Imo2022P6.Adjacent, Eq.mpr, LT.lt, Membership.mem, Finset, Finset.Icc, HPow.hPow, Subtype, id, Eq, congrArg, Imo2022P6.NordicSquare.minCell_value, LE.le, And.left, Iff.mp, And, Finset.mem_Icc, Subtype.property, Ne and 7 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Imo2022P6.NordicSquare.trivialPath The trivial uphill path consisting of just the minimum cell line 213 source
Source documentation
The trivial uphill path consisting of just the minimum cell.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, HAdd.hAdd, OfNat.ofNat, Imo2022P6.NordicSquare.UphillPath
Proof uses: Imo2022P6.NordicSquare.UphillPath.mk, List.cons, Imo2022P6.Cell, Imo2022P6.NordicSquare.minCell, List.nil
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def NordicSquare.trivialPath {n : ℕ} (ns : NordicSquare (n + 1)) : ns.UphillPath where
…
```
Mentions: Imo2022P6.NordicSquare
def Imo2022P6.NordicSquare.gapPath Given adjacent cells a, b, the uphill path ending with the edge {a,b} (obtained by extending the path to the smaller-valued cell by the larger one) line 222 source
Source documentation
Given adjacent cells a, b, the uphill path ending with the edge {a,b} (obtained by extending the path to the smaller-valued cell by the larger one).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.Adjacent, Imo2022P6.NordicSquare.UphillPath
Proof uses: dite, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype, Imo2022P6.NordicSquare.UphillPath.mk, HAppend.hAppend, List, Imo2022P6.NordicSquare.pathTo, List.cons, List.nil, Not
25 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
noncomputable def NordicSquare.gapPath {n : ℕ} (ns : NordicSquare n) (a b : Cell n)
    (hab : Adjacent a b) : ns.UphillPath :=
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.Adjacent
theorem Imo2022P6.NordicSquare.gapPath_cells line 265 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.Adjacent, Eq, List, Imo2022P6.NordicSquare.UphillPath.cells, Imo2022P6.NordicSquare.gapPath, ite, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype, HAppend.hAppend, Imo2022P6.NordicSquare.pathTo, List.cons, List.nil
Proof uses: id, Decidable, dite, Imo2022P6.NordicSquare.UphillPath, Imo2022P6.NordicSquare.UphillPath.mk, Not, Eq.mpr, congr, congrArg, dite_eq_right, ite_eq_right, Eq.refl, dite_eq_left, ite_eq_left
43 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2022P6.NordicSquare.gapPath_length line 272 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.Adjacent, LE.le, OfNat.ofNat, List.length, Imo2022P6.NordicSquare.UphillPath.cells, Imo2022P6.NordicSquare.gapPath
Proof uses: Eq.mpr, ite, List, LT.lt, Membership.mem, Finset, Finset.Icc, HPow.hPow, Subtype, HAppend.hAppend, Imo2022P6.NordicSquare.pathTo, List.cons, List.nil, id, Eq, congrArg, Imo2022P6.NordicSquare.gapPath_cells, Decidable, Not, ite_eq_right and 9 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Imo2022P6.UphillPath.lastTwo The last two cells of an uphill path, as a pair (second-to-last, last), with junk value for the second-to-last cell if the path has length 1 line 285 source
Source documentation
The last two cells of an uphill path, as a pair (second-to-last, last), with junk value for the second-to-last cell if the path has length 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, HAdd.hAdd, OfNat.ofNat, Imo2022P6.NordicSquare.UphillPath, Prod, Imo2022P6.Cell
Proof uses: Prod.mk, List.getD, Imo2022P6.NordicSquare.UphillPath.cells, HSub.hSub, List.length, Fin, Fin.mk, List.getLast
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def UphillPath.lastTwo {n : ℕ} {ns : NordicSquare (n + 1)} (p : ns.UphillPath) :
    Cell (n + 1) × Cell (n + 1) :=
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell
theorem Imo2022P6.NordicSquare.gapPath_lastTwo The last two cells of gapPath a b are the two cells, smaller-valued first line 291 source
Source documentation
The last two cells of gapPath a b are the two cells, smaller-valued first.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, HAdd.hAdd, OfNat.ofNat, Imo2022P6.Cell, Imo2022P6.Adjacent, Eq, Prod, Imo2022P6.UphillPath.lastTwo, Imo2022P6.NordicSquare.gapPath, ite, LT.lt, Membership.mem, Finset, Finset.Icc, HPow.hPow, Subtype, Prod.mk
Proof uses: id, Eq.mpr, List.getD, Imo2022P6.NordicSquare.UphillPath.cells, HSub.hSub, List.length, Fin, Fin.mk, List.getLast, List, HAppend.hAppend, Imo2022P6.NordicSquare.pathTo, List.cons, List.nil, Ne, Imo2022P6.NordicSquare.gapPath_cells, congrFun', congrArg, congr, List.getLast.congr_simp and 34 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.gapPath_lastTwo {n : ℕ} (ns : NordicSquare (n + 1)) (a b : Cell (n + 1))
    (hab : Adjacent a b) :
    UphillPath.lastTwo (gapPath ns a b hab) =
      if (ns a : ℕ) < (ns b : ℕ) then (a, b) else (b, a) := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.Adjacent, Imo2022P6.UphillPath.lastTwo, Imo2022P6.NordicSquare.gapPath
inductive Imo2022P6.GapDir A direction for a gap between two adjacent cells line 328 source
Source documentation
A direction for a gap between two adjacent cells.

no axioms what this means
```
inductive GapDir : Type
  | horiz : GapDir
  | vert : GapDir

/-- The ordered pair of cells of a gap: for `horiz`, `(i, j), (i, j+1)`;
for `vert`, `(j, i), (j+1, i)`. -/
```
def Imo2022P6.gapPair The ordered pair of cells of a gap: for horiz, (i, j), (i, j+1); for vert, (j, i), (j+1, i) line 334 source
Source documentation
The ordered pair of cells of a gap: for horiz, (i, j), (i, j+1); for vert, (j, i), (j+1, i).

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.GapDir, Prod, Fin, HAdd.hAdd, OfNat.ofNat, Imo2022P6.Cell
Proof uses: Imo2022P6.gapPair.match_1, Unit, Prod.mk, Prod.fst, Fin.mk, Prod.snd
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def gapPair {n : ℕ} (d : GapDir) (g : Fin (n + 1) × Fin n) : Cell (n + 1) × Cell (n + 1) :=
…
```
Mentions: Imo2022P6.GapDir, Imo2022P6.Cell
theorem Imo2022P6.gapPair_adjacent line 339 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.GapDir, Prod, Fin, HAdd.hAdd, OfNat.ofNat, Imo2022P6.Adjacent, Prod.fst, Imo2022P6.Cell, Imo2022P6.gapPair, Prod.snd
Proof uses: Eq, Imo2022P6.GapDir.horiz, of_eq_true, Nat.dist, Eq.trans, True, congrFun', congrArg, congr, HSub.hSub, tsub_self, add_zero, Nat.sub_eq_zero_of_le, LE.le, add_tsub_cancel_left, zero_add, eq_self, Eq.symm, Imo2022P6.GapDir.vert, Eq.refl
43 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2022P6.gapPair_injective The unordered pair of cells of a gap determines the gap line 344 source
Source documentation
The unordered pair of cells of a gap determines the gap.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.GapDir, Prod, Fin, HAdd.hAdd, OfNat.ofNat, Or, Eq, Imo2022P6.Cell, Imo2022P6.gapPair, Prod.swap, And
Proof uses: Imo2022P6.GapDir.horiz, And.intro, rfl, Prod.ext, Fin.ext, Prod.fst, Prod.snd, Eq.mp, congr, congrArg, Eq.trans, Prod.mk, Fin.mk, Prod.mk.injEq, Decidable.byContradiction, Not, Eq.symm, Imo2022P6.GapDir.vert, False.elim, False and 1 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem gapPair_injective {n : ℕ} (d₁ d₂ : GapDir) (g₁ g₂ : Fin (n + 1) × Fin n)
    (h : gapPair d₁ g₁ = gapPair d₂ g₂ ∨ gapPair d₁ g₁ = (gapPair d₂ g₂).swap) :
    d₁ = d₂ ∧ g₁ = g₂ := by
…
```
Mentions: Imo2022P6.GapDir, h, Imo2022P6.gapPair
def Imo2022P6.gapPathInj The injection from gaps (plus a point for the trivial path) to uphill paths line 355 source
Source documentation
The injection from gaps (plus a point for the trivial path) to uphill paths.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, HAdd.hAdd, OfNat.ofNat, Sum, Prod, Imo2022P6.GapDir, Fin, Unit, Imo2022P6.NordicSquare.UphillPath
Proof uses: Imo2022P6.gapPathInj.match_1, Imo2022P6.NordicSquare.gapPath, Prod.fst, Imo2022P6.Cell, Imo2022P6.gapPair, Prod.snd, Imo2022P6.gapPair_adjacent, Imo2022P6.NordicSquare.trivialPath
6 instances, coercions and auxiliary constants left out.
```
noncomputable def gapPathInj {n : ℕ} (ns : NordicSquare (n + 1)) :
    (GapDir × (Fin (n + 1) × Fin n)) ⊕ Unit → ns.UphillPath
  | .inl (d, g) => NordicSquare.gapPath ns (gapPair d g).1 (gapPair d g).2 (gapPair_adjacent _ _)
  | .inr () => NordicSquare.trivialPath ns
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.GapDir, Imo2022P6.NordicSquare.gapPath, Imo2022P6.gapPair, Imo2022P6.gapPair_adjacent, Imo2022P6.NordicSquare.trivialPath
theorem Imo2022P6.gapPathInj_injective line 360 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, HAdd.hAdd, OfNat.ofNat, Function.Injective, Sum, Prod, Imo2022P6.GapDir, Fin, Unit, Imo2022P6.NordicSquare.UphillPath, Imo2022P6.gapPathInj
Proof uses: Eq, Sum.inl, Prod.mk, Imo2022P6.Cell, Imo2022P6.UphillPath.lastTwo, congrArg, LT.lt, Membership.mem, Finset, Finset.Icc, HPow.hPow, Subtype, Prod.fst, Imo2022P6.gapPair, Prod.snd, Decidable, Not, And, Iff.mp, Prod.ext_iff and 22 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
def Imo2022P6.gapDirEquivFin2 GapDir is equivalent to Fin 2 line 402 source
Source documentation
GapDir is equivalent to Fin 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv, Imo2022P6.GapDir, Fin, OfNat.ofNat, Nat
Proof uses: Equiv.mk, Imo2022P6.gapPair.match_1, Unit, Fin.mk, ite, Eq, Imo2022P6.GapDir.horiz, Imo2022P6.GapDir.vert
9 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
def gapDirEquivFin2 : GapDir ≃ Fin 2 where
…
```
Mentions: Imo2022P6.GapDir
instance Imo2022P6.(instance at line 409) line 409 source
Source documentation
GapDir is a finite type.
```
instance : Fintype GapDir := Fintype.ofEquiv (Fin 2) gapDirEquivFin2.symm
```
Mentions: Imo2022P6.GapDir
theorem Imo2022P6.mk_gaps The number of gaps (plus one for the trivial path) as a cardinal line 412 source
Source documentation
The number of gaps (plus one for the trivial path) as a cardinal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Cardinal, Cardinal.mk, Sum, Prod, Imo2022P6.GapDir, Fin, HAdd.hAdd, OfNat.ofNat, Unit, HMul.hMul
Proof uses: Eq.mpr, Cardinal.lift, id, congrArg, Cardinal.mk_sum, Cardinal.mk_unit, Cardinal.mk_prod, Cardinal.mk_fin, Nonempty, Equiv, propext, Cardinal.mk_eq_nat_iff, Nonempty.intro, Imo2022P6.gapDirEquivFin2, congrFun', congr, Eq.trans, Cardinal.lift_id, Eq.symm, Nat.cast_one and 1 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem mk_gaps (n : ℕ) :
    (#(GapDir × (Fin (n + 1) × Fin n) ⊕ Unit) : Cardinal) =
      ((2 * ((n + 1) * n) + 1 : ℕ) : Cardinal) := by
…
```
Mentions: Imo2022P6.GapDir
theorem Imo2022P6.answer_eq The answer expressed as 2 * ((n+1) * n) + 1 line 425 source
Source documentation
The answer expressed as 2 * ((n+1) * n) + 1.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow
Proof uses: Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.pow_nat, Mathlib.Tactic.Ring.Common.coeff_one, Mathlib.Tactic.Ring.Common.pow_one_cast_of_isNat, Mathlib.Meta.NormNum.IsNat.mk and 21 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem answer_eq (n : ℕ) : 2 * (n + 1) ^ 2 - 2 * (n + 1) + 1 = 2 * ((n + 1) * n) + 1 := by
…
```
theorem Imo2022P6.lower_bound Lower bound: every Nordic square on an (n+1) × (n+1) board has at least 2 * ((n+1) * n) + 1 uphill paths line 431 source
Source documentation
Lower bound: every Nordic square on an (n+1) × (n+1) board has at least 2 * ((n+1) * n) + 1 uphill paths.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, HAdd.hAdd, OfNat.ofNat, LE.le, Cardinal, HMul.hMul, Cardinal.mk, Imo2022P6.NordicSquare.UphillPath
Proof uses: Sum, Prod, Imo2022P6.GapDir, Fin, Unit, Cardinal.mk_le_of_injective, Imo2022P6.gapPathInj, Imo2022P6.gapPathInj_injective, Eq.mp, congrArg, Imo2022P6.mk_gaps
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem lower_bound {n : ℕ} (ns : NordicSquare (n + 1)) :
    ((2 * ((n + 1) * n) + 1 : ℕ) : Cardinal) ≤ #ns.UphillPath := by
…
```
Mentions: Imo2022P6.NordicSquare
theorem Imo2022P6.lower_bound' Lower bound (general form): every Nordic square on an m × m board has at least 2 * (m * (m - 1)) + 1 uphill paths line 439 source
Source documentation
Lower bound (general form): every Nordic square on an m × m board has at least 2 * (m * (m - 1)) + 1 uphill paths.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.NordicSquare, Cardinal, HAdd.hAdd, HMul.hMul, HSub.hSub, Cardinal.mk, Imo2022P6.NordicSquare.UphillPath
Proof uses: Eq, Exists, Exists.intro, Eq.symm, Nat.sub_add_cancel, Eq.mpr, id, congrFun', congrArg, Eq.trans, congr, add_tsub_cancel_right, Nat.mul_assoc, Nat.cast_add, Nat.cast_mul, Nat.cast_one, Eq.mp, Imo2022P6.lower_bound
57 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem lower_bound' {m : ℕ} (hm : 1 ≤ m) (ns : NordicSquare m) :
    ((2 * ((m - 1) + 1) * (m - 1) + 1 : ℕ) : Cardinal) ≤ #ns.UphillPath := by
…
```
Mentions: Imo2022P6.NordicSquare
theorem Imo2022P6.NordicSquare.UphillPath.ext Two uphill paths with the same cells are equal line 445 source
Source documentation
Two uphill paths with the same cells are equal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.NordicSquare.UphillPath, Eq, List, Imo2022P6.Cell, Imo2022P6.NordicSquare.UphillPath.cells
Proof uses: Ne, List.nil, Imo2022P6.NordicSquare.Valley, List.head, List.IsChain, Imo2022P6.Adjacent, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype, Imo2022P6.NordicSquare.UphillPath.mk, Eq.rec, Eq.refl, Eq.symm
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.UphillPath.ext {n : ℕ} {ns : NordicSquare n} {p q : ns.UphillPath}
    (h : p.cells = q.cells) : p = q := by
…
```
Mentions: Imo2022P6.NordicSquare, h
theorem Imo2022P6.NordicSquare.isChain_nodup An increasing chain of cells has no duplicates line 450 source
Source documentation
An increasing chain of cells has no duplicates.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, List, Imo2022P6.Cell, List.IsChain, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype, List.Nodup
Proof uses: List.rec, List.nil, List.nodup_nil, List.cons, Option, List.head?, And, Eq.mp, congrArg, propext, List.isChain_cons, Eq.mpr, Not, id, Eq, List.nodup_cons, And.intro, List.IsChain.rel_cons, Iff.mpr, False.elim and 1 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.isChain_nodup {n : ℕ} (ns : NordicSquare n) (l : List (Cell n))
    (h : l.IsChain fun x y ↦ (ns x : ℕ) < (ns y : ℕ)) : l.Nodup := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, h
theorem Imo2022P6.NordicSquare.uphillPath_length_le The list of cells of an uphill path has length at most the number of cells line 464 source
Source documentation
The list of cells of an uphill path has length at most the number of cells.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.NordicSquare.UphillPath, LE.le, List.length, Imo2022P6.Cell, Imo2022P6.NordicSquare.UphillPath.cells, HPow.hPow, OfNat.ofNat
Proof uses: List.Nodup, Imo2022P6.NordicSquare.isChain_nodup, Imo2022P6.NordicSquare.UphillPath.increasing, Fintype.card, Fin, List.Nodup.length_le_card, Eq.mp, HMul.hMul, congrArg, Eq.symm, pow_two, Fintype.card_fin, Prod, Fintype.card_prod
19 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.uphillPath_length_le {n : ℕ} (ns : NordicSquare n) (p : ns.UphillPath) :
    p.cells.length ≤ n ^ 2 := by
…
```
Mentions: Imo2022P6.NordicSquare
instance Imo2022P6.finiteBoundedList Bounded-length lists over a finite type form a finite type line 472 source
Source documentation
Bounded-length lists over a finite type form a finite type.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finite, Nat, Subtype, List, LE.le, List.length
Proof uses: Finite.of_injective, Fin, Option, GetElem?.getElem?, LT.lt, Eq, Subtype.ext, List.ext_getElem?, dite, congrFun, Fin.mk, Not, Eq.mpr, Option.none, id, congrArg, Iff.mpr, List.getElem?_eq_none_iff, le_trans, Subtype.property and 2 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
instance finiteBoundedList (α : Type*) [Finite α] (k : ℕ) :
    Finite {l : List α // l.length ≤ k} :=
…
```
instance Imo2022P6.(instance at line 488) line 488 source
Source documentation
There are finitely many uphill paths.
```
instance (n : ℕ) (ns : NordicSquare n) : Finite ns.UphillPath :=
…
```
Mentions: Imo2022P6.NordicSquare
instance Imo2022P6.(instance at line 496) line 496 source
theorem Imo2022P6.mk_uphillPath The cardinal of the type of uphill paths as a natural line 499 source
Source documentation
The cardinal of the type of uphill paths as a natural.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Eq, Cardinal, Cardinal.mk, Imo2022P6.NordicSquare.UphillPath, Nat.card
Proof uses: Eq.symm, Nat.cast_card
5 instances, coercions and auxiliary constants left out.
```
theorem mk_uphillPath (n : ℕ) (ns : NordicSquare n) :
    #ns.UphillPath = (Nat.card ns.UphillPath : Cardinal) := Nat.cast_card.symm
```
Mentions: Imo2022P6.NordicSquare
def Imo2022P6.NordicSquare.UphillPath.dropLast The dropLast of an uphill path of length at least 2 is an uphill path line 503 source
Source documentation
The dropLast of an uphill path of length at least 2 is an uphill path.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.NordicSquare.UphillPath, LE.le, OfNat.ofNat, List.length, Imo2022P6.Cell, Imo2022P6.NordicSquare.UphillPath.cells
Proof uses: Imo2022P6.NordicSquare.UphillPath.mk, List.dropLast
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def NordicSquare.UphillPath.dropLast {n : ℕ} {ns : NordicSquare n} (p : ns.UphillPath)
    (h : 2 ≤ p.cells.length) : ns.UphillPath where
…
```
Mentions: Imo2022P6.NordicSquare, h
theorem Imo2022P6.NordicSquare.UphillPath.dropLast_getLast The last cell of the dropLast of a path of length ≥ 2 is its second-to-last cell line 516 source
Source documentation
The last cell of the dropLast of a path of length ≥ 2 is its second-to-last cell.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.NordicSquare.UphillPath, LE.le, OfNat.ofNat, List.length, Imo2022P6.Cell, Imo2022P6.NordicSquare.UphillPath.cells, Eq, List.getLast, Imo2022P6.NordicSquare.UphillPath.dropLast, Imo2022P6.NordicSquare.UphillPath.nonempty, GetElem.getElem, List, LT.lt, HSub.hSub
Proof uses: List.getLast_dropLast
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.UphillPath.dropLast_getLast {n : ℕ} {ns : NordicSquare n}
    (p : ns.UphillPath) (h : 2 ≤ p.cells.length) :
    (p.dropLast h).cells.getLast (p.dropLast h).nonempty =
      p.cells[p.cells.length - 2]'(by omega) := by
…
```
Mentions: Imo2022P6.NordicSquare, h
theorem Imo2022P6.NordicSquare.UphillPath.penultimate_props The penultimate and last cells of a path of length ≥ 2 are adjacent, with the value of the penultimate one smaller line 524 source
Source documentation
The penultimate and last cells of a path of length ≥ 2 are adjacent, with the value of the penultimate one smaller.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.NordicSquare.UphillPath, LE.le, OfNat.ofNat, List.length, Imo2022P6.Cell, Imo2022P6.NordicSquare.UphillPath.cells, And, Imo2022P6.Adjacent, List.getLast, Imo2022P6.NordicSquare.UphillPath.dropLast, Imo2022P6.NordicSquare.UphillPath.nonempty, LT.lt, Membership.mem, Finset, Finset.Icc, HPow.hPow, Subtype
Proof uses: Ne, List, List.dropLast, List.nil, Eq.mpr, id, Eq, congrArg, propext, List.ne_nil_iff_length_pos, HSub.hSub, List.length_dropLast, Decidable.byContradiction, Not, And.intro, List.IsChain.rel_getLast_dropLast, Imo2022P6.NordicSquare.UphillPath.adjacent, Imo2022P6.NordicSquare.UphillPath.increasing
34 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.UphillPath.penultimate_props {n : ℕ} {ns : NordicSquare n}
    (p : ns.UphillPath) (h : 2 ≤ p.cells.length) :
    Adjacent ((p.dropLast h).cells.getLast (p.dropLast h).nonempty) (p.cells.getLast p.nonempty) ∧
      (ns ((p.dropLast h).cells.getLast (p.dropLast h).nonempty) : ℕ) <
        (ns (p.cells.getLast p.nonempty) : ℕ) := by
…
```
Mentions: Imo2022P6.NordicSquare, h, Imo2022P6.Adjacent
def Imo2022P6.NordicSquare.Hill A "hill" in a Nordic square: a cell adjacent only to cells with smaller values line 535 source
Source documentation
A "hill" in a Nordic square: a cell adjacent only to cells with smaller values.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell
Proof uses: Imo2022P6.Adjacent, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype
14 instances, coercions and auxiliary constants left out.
```
def NordicSquare.Hill {n : ℕ} (ns : NordicSquare n) (c : Cell n) : Prop :=
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell
instance Imo2022P6.(instance at line 539) line 539 source
Source documentation
Valley and Hill are decidable.
```
instance {n : ℕ} (ns : NordicSquare n) (c : Cell n) : Decidable (ns.Valley c) :=
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell
instance Imo2022P6.(instance at line 543) line 543 source
Source documentation
Hills are decidable.
```
instance {n : ℕ} (ns : NordicSquare n) (c : Cell n) : Decidable (ns.Hill c) :=
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell
theorem Imo2022P6.NordicSquare.no_smaller_of_valley A valley has no smaller-valued neighbor line 547 source
Source documentation
A valley has no smaller-valued neighbor.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.NordicSquare.Valley, Not, Exists, And, Imo2022P6.Adjacent, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype
Proof uses: False
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.no_smaller_of_valley {n : ℕ} (ns : NordicSquare n) {c : Cell n}
    (h : ns.Valley c) : ¬ ∃ c', Adjacent c c' ∧ (ns c' : ℕ) < (ns c : ℕ) := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, h, Imo2022P6.Adjacent
theorem Imo2022P6.NordicSquare.not_hill_of_exists_larger A valley is not a hill when it has a neighbor line 554 source
Source documentation
A valley is not a hill when it has a neighbor.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, Exists, And, Imo2022P6.Adjacent, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype, Not, Imo2022P6.NordicSquare.Hill
31 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.not_hill_of_exists_larger {n : ℕ} (ns : NordicSquare n) {c : Cell n}
    (h : ∃ c', Adjacent c c' ∧ (ns c : ℕ) < (ns c' : ℕ)) : ¬ ns.Hill c := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, h, Imo2022P6.Adjacent
theorem Imo2022P6.NordicSquare.not_valley_of_exists_smaller A cell with a smaller-valued neighbor is not a valley line 562 source
Source documentation
A cell with a smaller-valued neighbor is not a valley.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, Exists, And, Imo2022P6.Adjacent, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype, Not, Imo2022P6.NordicSquare.Valley
31 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.not_valley_of_exists_smaller {n : ℕ} (ns : NordicSquare n) {c : Cell n}
    (h : ∃ c', Adjacent c c' ∧ (ns c' : ℕ) < (ns c : ℕ)) : ¬ ns.Valley c := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, h, Imo2022P6.Adjacent
structure Imo2022P6.NordicSquare.Good The properties of a Nordic square implying the minimal number of uphill paths line 570 source
Source documentation
The properties of a Nordic square implying the minimal number of uphill paths.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare
```
structure NordicSquare.Good {n : ℕ} (ns : NordicSquare n) : Prop where
…
```
Mentions: Imo2022P6.NordicSquare
theorem Imo2022P6.NordicSquare.cells_eq_pathTo_of_good In a good square, any uphill path ending at a non-hill cell c equals pathTo ns c line 580 source
Source documentation
In a good square, any uphill path ending at a non-hill cell c equals pathTo ns c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.NordicSquare.Good, Imo2022P6.Cell, Not, Imo2022P6.NordicSquare.Hill, Imo2022P6.NordicSquare.UphillPath, Eq, List.getLast, Imo2022P6.NordicSquare.UphillPath.cells, Imo2022P6.NordicSquare.UphillPath.nonempty, List, Imo2022P6.NordicSquare.pathTo
Proof uses: Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype, Nat.strong_induction_on, LT.lt, dite, List.length, List.cons, List.nil, Exists, Iff.mp, List.length_eq_one_iff, Eq.mp, congrFun', congrArg, List.getLast.congr_simp, Imo2022P6.NordicSquare.Valley and 37 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.cells_eq_pathTo_of_good {n : ℕ} (ns : NordicSquare n) (hg : ns.Good)
    (c : Cell n) (hc : ¬ ns.Hill c) (p : ns.UphillPath)
    (hlast : p.cells.getLast p.nonempty = c) : p.cells = pathTo ns c := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.NordicSquare.pathTo
theorem Imo2022P6.NordicSquare.countTo_eq_one_of_not_hill The fiber of uphill paths ending at a non-hill cell has cardinality 1 line 637 source
Source documentation
The fiber of uphill paths ending at a non-hill cell has cardinality 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.NordicSquare.Good, Imo2022P6.Cell, Not, Imo2022P6.NordicSquare.Hill, Eq, Nat.card, Subtype, Imo2022P6.NordicSquare.UphillPath, List.getLast, Imo2022P6.NordicSquare.UphillPath.cells, Imo2022P6.NordicSquare.UphillPath.nonempty, OfNat.ofNat
Proof uses: Subsingleton, Subsingleton.intro, Subtype.ext, Imo2022P6.NordicSquare.UphillPath.ext, Eq.mpr, List, Imo2022P6.NordicSquare.pathTo, id, congrArg, Imo2022P6.NordicSquare.cells_eq_pathTo_of_good, Subtype.property, Eq.refl, Nonempty, Nonempty.intro, Subtype.mk, Imo2022P6.NordicSquare.uphillPathTo, Iff.mpr, Option, List.getLast?, Option.some and 3 more
2 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.countTo_eq_one_of_not_hill {n : ℕ} (ns : NordicSquare n) (hg : ns.Good)
    (c : Cell n) (hc : ¬ ns.Hill c) :
    Nat.card {p : ns.UphillPath // p.cells.getLast p.nonempty = c} = 1 := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell
def Imo2022P6.cellDegree The degree of a cell: the number of cells adjacent to it line 652 source
Source documentation
The degree of a cell: the number of cells adjacent to it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.Cell
Proof uses: Finset.card, Finset.filter, Imo2022P6.Adjacent, Finset.univ, Fin
3 instances, coercions and auxiliary constants left out.
```
def cellDegree {n : ℕ} (c : Cell n) : ℕ := (Finset.univ.filter fun c' ↦ Adjacent c' c).card
```
Mentions: Imo2022P6.Cell, Imo2022P6.Adjacent
theorem Imo2022P6.NordicSquare.length_ge_two_of_getLast_hill A path ending at a hill (which has a neighbor) has length at least 2 line 655 source
Source documentation
A path ending at a hill (which has a neighbor) has length at least 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.NordicSquare.Hill, Exists, Imo2022P6.Adjacent, Subtype, Imo2022P6.NordicSquare.UphillPath, Eq, List.getLast, Imo2022P6.NordicSquare.UphillPath.cells, Imo2022P6.NordicSquare.UphillPath.nonempty, LE.le, OfNat.ofNat, List.length
Proof uses: Ne, List, List.nil, Decidable.byContradiction, Not, Eq.mp, LT.lt, congrArg, propext, List.ne_nil_iff_length_pos, List.cons, False, Iff.mp, List.length_eq_one_iff, Subtype.property, congrFun', List.getLast.congr_simp, Imo2022P6.NordicSquare.Valley, List.head, Imo2022P6.NordicSquare.UphillPath.first_valley and 7 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.length_ge_two_of_getLast_hill {n : ℕ} (ns : NordicSquare n)
    (h : Cell n) (hh : ns.Hill h) (hnb : ∃ c', Adjacent h c')
    (p : {p : ns.UphillPath // p.cells.getLast p.nonempty = h}) : 2 ≤ p.1.cells.length := by
…
```
Mentions: Imo2022P6.NordicSquare, h, Imo2022P6.Cell, Imo2022P6.Adjacent
def Imo2022P6.NordicSquare.hillFiberEquiv The fiber of uphill paths ending at a hill is equivalent to its set of neighbors line 678 source
Source documentation
The fiber of uphill paths ending at a hill is equivalent to its set of neighbors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.NordicSquare.Good, Imo2022P6.Cell, Imo2022P6.NordicSquare.Hill, Exists, Imo2022P6.Adjacent, Equiv, Subtype, Imo2022P6.NordicSquare.UphillPath, Eq, List.getLast, Imo2022P6.NordicSquare.UphillPath.cells, Imo2022P6.NordicSquare.UphillPath.nonempty
Proof uses: Equiv.mk, Subtype.mk, Imo2022P6.NordicSquare.UphillPath.dropLast, Imo2022P6.NordicSquare.length_ge_two_of_getLast_hill, Imo2022P6.NordicSquare.gapPath
7 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
```
noncomputable def NordicSquare.hillFiberEquiv {n : ℕ} (ns : NordicSquare n) (hg : ns.Good)
    (h : Cell n) (hh : ns.Hill h) (hnb : ∃ c', Adjacent h c') :
    {p : ns.UphillPath // p.cells.getLast p.nonempty = h} ≃ {c' : Cell n // Adjacent c' h} where
…
```
Mentions: Imo2022P6.NordicSquare, h, Imo2022P6.Cell, Imo2022P6.Adjacent
theorem Imo2022P6.NordicSquare.countTo_eq_degree_of_hill The fiber of uphill paths ending at a hill has cardinality its degree line 738 source
Source documentation
The fiber of uphill paths ending at a hill has cardinality its degree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.NordicSquare.Good, Imo2022P6.Cell, Imo2022P6.NordicSquare.Hill, Exists, Imo2022P6.Adjacent, Eq, Nat.card, Subtype, Imo2022P6.NordicSquare.UphillPath, List.getLast, Imo2022P6.NordicSquare.UphillPath.cells, Imo2022P6.NordicSquare.UphillPath.nonempty, Imo2022P6.cellDegree
Proof uses: Nat.card_congr, Imo2022P6.NordicSquare.hillFiberEquiv, Eq.mpr, id, congrArg, Fintype.card, Fin, Nat.card_eq_fintype_card, Finset.card, Finset.filter, Finset.univ, Fintype.card_subtype, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.countTo_eq_degree_of_hill {n : ℕ} (ns : NordicSquare n) (hg : ns.Good)
    (h : Cell n) (hh : ns.Hill h) (hnb : ∃ c', Adjacent h c') :
    Nat.card {p : ns.UphillPath // p.cells.getLast p.nonempty = h} = cellDegree h := by
…
```
Mentions: Imo2022P6.NordicSquare, h, Imo2022P6.Cell, Imo2022P6.Adjacent, Imo2022P6.cellDegree
def Imo2022P6.gapCells Cells of a gap on an n × n board (ordered by position) line 748 source
Source documentation
Cells of a gap on an n × n board (ordered by position).

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.GapDir, Prod, Fin, HSub.hSub, OfNat.ofNat, Imo2022P6.Cell
Proof uses: Imo2022P6.gapPair.match_1, Unit, Prod.mk, Prod.fst, Fin.mk, Prod.snd, HAdd.hAdd
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def gapCells {n : ℕ} (d : GapDir) (g : Fin n × Fin (n - 1)) : Cell n × Cell n :=
…
```
Mentions: Imo2022P6.GapDir, Imo2022P6.Cell
theorem Imo2022P6.gapCells_adjacent line 753 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.GapDir, Prod, Fin, HSub.hSub, OfNat.ofNat, Imo2022P6.Adjacent, Prod.fst, Imo2022P6.Cell, Imo2022P6.gapCells, Prod.snd
Proof uses: Eq, Imo2022P6.GapDir.horiz, of_eq_true, HAdd.hAdd, Nat.dist, Eq.trans, True, congrFun', congrArg, congr, tsub_self, add_zero, Nat.sub_eq_zero_of_le, LE.le, add_tsub_cancel_left, zero_add, eq_self, Eq.symm, Imo2022P6.GapDir.vert, Eq.refl
43 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2022P6.Adjacent.dist The arithmetic content of adjacency, unpacked line 758 source
Source documentation
The arithmetic content of adjacency, unpacked.

no axioms what this means
Statement uses: Nat, Imo2022P6.Cell, Imo2022P6.Adjacent, Eq, HAdd.hAdd, HSub.hSub, Prod.fst, Fin, Prod.snd, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem Adjacent.dist {n : ℕ} {x y : Cell n} (h : Adjacent x y) :
    (x.1.1 - y.1.1 + (y.1.1 - x.1.1)) + (x.2.1 - y.2.1 + (y.2.1 - x.2.1)) = 1 := by
…
```
Mentions: Imo2022P6.Cell, h, Imo2022P6.Adjacent
def Imo2022P6.gapOfPair The gap determined by an ordered pair of adjacent cells line 765 source
Source documentation
The gap determined by an ordered pair of adjacent cells.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2022P6.Cell, Imo2022P6.Adjacent, Prod.fst, Prod.snd, Imo2022P6.GapDir, Fin, HSub.hSub, OfNat.ofNat
Proof uses: dite, Eq, Prod.mk, Imo2022P6.GapDir.horiz, Fin.mk, Min.min, Not, Imo2022P6.GapDir.vert
11 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
noncomputable def gapOfPair {n : ℕ} (cc : Cell n × Cell n) (h : Adjacent cc.1 cc.2) :
    GapDir × (Fin n × Fin (n - 1)) :=
…
```
Mentions: Imo2022P6.Cell, h, Imo2022P6.Adjacent, Imo2022P6.GapDir
theorem Imo2022P6.gapOfPair_swap gapOfPair is invariant under swapping the two cells line 783 source
Source documentation
gapOfPair is invariant under swapping the two cells.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2022P6.Cell, Imo2022P6.Adjacent, Prod.fst, Prod.snd, Eq, Imo2022P6.GapDir, Fin, HSub.hSub, OfNat.ofNat, Imo2022P6.gapOfPair, Prod.swap, Imo2022P6.Adjacent.symm
Proof uses: id, dite, Prod.mk, Imo2022P6.GapDir.horiz, Fin.mk, Min.min, Not, Imo2022P6.GapDir.vert, Eq.mpr, congrArg, dite_eq_left, Eq.symm, And, True, LT.lt, Eq.refl, Eq.trans, Prod.mk.injEq, congr, eq_self and 12 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
theorem gapOfPair_swap {n : ℕ} (cc : Cell n × Cell n) (h : Adjacent cc.1 cc.2) :
    gapOfPair cc.swap h.symm = gapOfPair cc h := by
…
```
Mentions: Imo2022P6.Cell, h, Imo2022P6.Adjacent, Imo2022P6.gapOfPair
theorem Imo2022P6.gapOfPair_eq_horiz In the horizontal case, gapOfPair is the horizontal gap of the two cells line 803 source
Source documentation
In the horizontal case, gapOfPair is the horizontal gap of the two cells.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2022P6.Cell, Imo2022P6.Adjacent, Prod.fst, Prod.snd, Eq, Fin, Imo2022P6.GapDir, HSub.hSub, OfNat.ofNat, Imo2022P6.gapOfPair, Prod.mk, Imo2022P6.GapDir.horiz, Fin.mk, Min.min
Proof uses: id, Eq.mpr, dite, Not, Imo2022P6.GapDir.vert, congrArg, dite_eq_left, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem gapOfPair_eq_horiz {n : ℕ} (cc : Cell n × Cell n) (h : Adjacent cc.1 cc.2)
    (h1 : cc.1.1 = cc.2.1) :
    gapOfPair cc h = (.horiz, (cc.1.1, ⟨min cc.1.2.1 cc.2.2.1, by
      have _hdist := h.dist
…
```
Mentions: Imo2022P6.Cell, h, Imo2022P6.Adjacent, Imo2022P6.gapOfPair
theorem Imo2022P6.gapOfPair_eq_vert In the vertical case, gapOfPair is the vertical gap of the two cells line 815 source
Source documentation
In the vertical case, gapOfPair is the vertical gap of the two cells.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2022P6.Cell, Imo2022P6.Adjacent, Prod.fst, Prod.snd, Not, Eq, Fin, Imo2022P6.GapDir, HSub.hSub, OfNat.ofNat, Imo2022P6.gapOfPair, Prod.mk, Imo2022P6.GapDir.vert, Fin.mk, Min.min
Proof uses: id, Eq.mpr, dite, Imo2022P6.GapDir.horiz, congrArg, dite_eq_right, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem gapOfPair_eq_vert {n : ℕ} (cc : Cell n × Cell n) (h : Adjacent cc.1 cc.2)
    (h1 : ¬ cc.1.1 = cc.2.1) :
    gapOfPair cc h = (.vert, (cc.1.2, ⟨min cc.1.1.1 cc.2.1.1, by
      have _hdist := h.dist
…
```
Mentions: Imo2022P6.Cell, h, Imo2022P6.Adjacent, Imo2022P6.gapOfPair
theorem Imo2022P6.gapCells_gapOfPair The two cells of gapOfPair cc are exactly the two cells of cc (in some order) line 827 source
Source documentation
The two cells of gapOfPair cc are exactly the two cells of cc (in some order).

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Prod, Imo2022P6.Cell, Imo2022P6.Adjacent, Prod.fst, Prod.snd, Or, Eq, Imo2022P6.gapCells, Imo2022P6.GapDir, Fin, HSub.hSub, OfNat.ofNat, Imo2022P6.gapOfPair, Prod.swap
Proof uses: dite, Eq.mpr, Prod.mk, Imo2022P6.GapDir.horiz, Fin.mk, Min.min, id, congrArg, Imo2022P6.gapOfPair_eq_horiz, HAdd.hAdd, Imo2022P6.Adjacent.dist, LT.lt, Fin.isLt, LE.le, Or.inl, Iff.mpr, And, Prod.ext_iff, And.intro, rfl and 9 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
theorem gapCells_gapOfPair {n : ℕ} (cc : Cell n × Cell n) (h : Adjacent cc.1 cc.2) :
    gapCells (gapOfPair cc h).1 (gapOfPair cc h).2 = cc ∨
      gapCells (gapOfPair cc h).1 (gapOfPair cc h).2 = cc.swap := by
…
```
Mentions: Imo2022P6.Cell, h, Imo2022P6.Adjacent, Imo2022P6.gapCells, Imo2022P6.gapOfPair
theorem Imo2022P6.gapOfPair_gapCells The gap of the cells of a gap is the gap itself line 883 source
Source documentation
The gap of the cells of a gap is the gap itself.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.GapDir, Prod, Fin, HSub.hSub, OfNat.ofNat, Eq, Imo2022P6.gapOfPair, Imo2022P6.gapCells, Imo2022P6.gapCells_adjacent, Prod.mk
Proof uses: Imo2022P6.GapDir.horiz, of_eq_true, Eq.trans, True, congrFun', congrArg, dite, Prod.fst, Imo2022P6.Cell, Prod.snd, Fin.mk, Min.min, Not, Imo2022P6.GapDir.vert, eq_self, dite_eq_left_of_eq_true, Fin.mk.congr_simp, inf_of_le_left, HAdd.hAdd, LE.le and 6 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem gapOfPair_gapCells {n : ℕ} (d : GapDir) (g : Fin n × Fin (n - 1)) :
    gapOfPair (gapCells d g) (gapCells_adjacent d g) = (d, g) := by
…
```
Mentions: Imo2022P6.GapDir, Imo2022P6.gapOfPair, Imo2022P6.gapCells, Imo2022P6.gapCells_adjacent
def Imo2022P6.decPairOfGap The decreasing orientation of the cells of a gap line 894 source
Source documentation
The decreasing orientation of the cells of a gap.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Imo2022P6.GapDir, Prod, Fin, HSub.hSub, OfNat.ofNat, Subtype, Imo2022P6.Cell, And, Imo2022P6.Adjacent, Prod.fst, Prod.snd, LT.lt, Membership.mem, Finset, Finset.Icc, HPow.hPow
Proof uses: dite, Imo2022P6.gapCells, Subtype.mk, Prod.mk, Not
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def decPairOfGap {n : ℕ} (ns : NordicSquare n) (d : GapDir)
    (g : Fin n × Fin (n - 1)) :
    {cc : Cell n × Cell n // Adjacent cc.1 cc.2 ∧ (ns cc.2 : ℕ) < (ns cc.1 : ℕ)} :=
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.GapDir, Imo2022P6.Cell, Imo2022P6.Adjacent
def Imo2022P6.decPairEquivGaps The decreasing-adjacent-pairs are equivalent to the gaps line 906 source
Source documentation
The decreasing-adjacent-pairs are equivalent to the gaps.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Equiv, Subtype, Prod, Imo2022P6.Cell, And, Imo2022P6.Adjacent, Prod.fst, Prod.snd, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Imo2022P6.GapDir, Fin, HSub.hSub
Proof uses: Equiv.mk, Imo2022P6.gapOfPair, Imo2022P6.decPairOfGap
35 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
noncomputable def decPairEquivGaps {n : ℕ} (ns : NordicSquare n) :
    {cc : Cell n × Cell n // Adjacent cc.1 cc.2 ∧ (ns cc.2 : ℕ) < (ns cc.1 : ℕ)} ≃
      GapDir × (Fin n × Fin (n - 1)) where
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.Adjacent, Imo2022P6.GapDir
theorem Imo2022P6.card_decPair The number of decreasing adjacent pairs is the number of gaps line 938 source
Source documentation
The number of decreasing adjacent pairs is the number of gaps.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Eq, Fintype.card, Subtype, Prod, Imo2022P6.Cell, And, Imo2022P6.Adjacent, Prod.fst, Prod.snd, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Fin, HMul.hMul, HSub.hSub
Proof uses: Imo2022P6.GapDir, Fintype.card_congr, Imo2022P6.decPairEquivGaps, Eq.mpr, id, congrArg, Fintype.card_prod, Fintype.card_fin, Eq.symm, Imo2022P6.gapDirEquivFin2, Eq.refl
49 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem card_decPair {n : ℕ} (ns : NordicSquare n) :
    Fintype.card {cc : Cell n × Cell n // Adjacent cc.1 cc.2 ∧ (ns cc.2 : ℕ) < (ns cc.1 : ℕ)} =
      2 * (n * (n - 1)) := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.Adjacent
theorem Imo2022P6.exists_adjacent Every cell on a board of side at least 2 has an adjacent cell line 949 source
Source documentation
Every cell on a board of side at least 2 has an adjacent cell.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.Cell, Exists, Imo2022P6.Adjacent
Proof uses: Fin, dite, Prod.mk, Eq, Exists.intro, Fin.mk, Decidable.byContradiction, LT.lt, Not, Fin.ext, of_eq_true, Eq.trans, True, congrFun', congrArg, eq_self, Eq.mpr, id, HAdd.hAdd, Nat.dist and 11 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem exists_adjacent {n : ℕ} (hn : 2 ≤ n) (c : Cell n) : ∃ c', Adjacent c c' := by
…
```
Mentions: Imo2022P6.Cell, Imo2022P6.Adjacent
theorem Imo2022P6.sum_smaller_eq_gaps The total number of "smaller neighbor" incidences equals the number of gaps line 962 source
Source documentation
The total number of "smaller neighbor" incidences equals the number of gaps.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Eq, Finset.sum, Imo2022P6.Cell, Finset.univ, Fin, Finset.card, Finset.filter, And, Imo2022P6.Adjacent, LT.lt, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HPow.hPow, Subtype, HMul.hMul, HSub.hSub
Proof uses: ite, Eq.mpr, id, congrArg, Finset.card_filter, Eq.refl, Finset.sum_congr, rfl, Prod, SProd.sprod, Prod.fst, Prod.snd, Eq.symm, Finset.sum_product', Finset.univ_product_univ, Fintype.card, Fintype.card_subtype, Imo2022P6.card_decPair
50 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem sum_smaller_eq_gaps {n : ℕ} (ns : NordicSquare n) :
    (∑ c : Cell n, (Finset.univ.filter fun c' ↦ Adjacent c c' ∧ (ns c' : ℕ) < (ns c : ℕ)).card) =
      2 * (n * (n - 1)) := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell, Imo2022P6.Adjacent
theorem Imo2022P6.NordicSquare.card_eq_sum_countTo The number of uphill paths as a sum over the last cell line 975 source
Source documentation
The number of uphill paths as a sum over the last cell.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.NordicSquare, Eq, Nat.card, Imo2022P6.NordicSquare.UphillPath, Finset.sum, Imo2022P6.Cell, Finset.univ, Fin, Subtype, List.getLast, Imo2022P6.NordicSquare.UphillPath.cells, Imo2022P6.NordicSquare.UphillPath.nonempty
Proof uses: Fintype.card, Nat.card_eq_fintype_card, Eq.mpr, Sigma, id, congrArg, Eq.symm, Fintype.card_sigma, Fintype.card_congr, Equiv.symm, Equiv.sigmaFiberEquiv, Finset.sum_congr, rfl, Finset, Membership.mem
13 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.card_eq_sum_countTo {n : ℕ} (ns : NordicSquare n) :
    Nat.card ns.UphillPath =
      ∑ c : Cell n, Nat.card {p : ns.UphillPath // p.cells.getLast p.nonempty = c} := by
…
```
Mentions: Imo2022P6.NordicSquare, Imo2022P6.Cell
theorem Imo2022P6.NordicSquare.good_count Counting theorem: a good Nordic square on an n × n board (with n ≥ 2) has exactly 2 * n * (n - 1) + 1 uphill paths line 989 source
Source documentation
Counting theorem: a good Nordic square on an n × n board (with n ≥ 2) has exactly 2 * n * (n - 1) + 1 uphill paths.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.NordicSquare, Imo2022P6.NordicSquare.Good, Eq, Nat.card, Imo2022P6.NordicSquare.UphillPath, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: Imo2022P6.Cell, And, Imo2022P6.NordicSquare.Valley, ExistsUnique, Imo2022P6.NordicSquare.Good.valley_unique, Not, Imo2022P6.NordicSquare.Hill, Imo2022P6.Adjacent, Exists, Imo2022P6.exists_adjacent, LT.lt, Membership.mem, Finset, Finset.Icc, HPow.hPow, Subtype, Finset.card, Finset.filter, Finset.univ, Fin and 55 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
```
theorem NordicSquare.good_count {n : ℕ} (hn : 2 ≤ n) (ns : NordicSquare n) (hg : ns.Good) :
    Nat.card ns.UphillPath = 2 * n * (n - 1) + 1 := by
…
```
Mentions: Imo2022P6.NordicSquare
theorem Imo2022P6.nat_card_uphillPath_one The number of uphill paths on a 1×1 board is 1 line 1059 source
Source documentation
The number of uphill paths on a 1×1 board is 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2022P6.NordicSquare, OfNat.ofNat, Nat, Eq, Nat.card, Imo2022P6.NordicSquare.UphillPath
Proof uses: Subsingleton, Imo2022P6.Cell, Subsingleton.intro, Fin, Prod.mk, of_eq_true, Prod, Eq.trans, And, True, Prod.mk.injEq, congr, congrArg, Fin.val_eq_zero, eq_self, and_self, Imo2022P6.NordicSquare.UphillPath.ext, List.length, Imo2022P6.NordicSquare.UphillPath.cells, List.Nodup and 30 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
theorem nat_card_uphillPath_one (ns : NordicSquare 1) : Nat.card ns.UphillPath = 1 := by
…
```
Mentions: Imo2022P6.NordicSquare
def Imo2022P6.pOffset The column offset of the construction (handles the case m % 3 = 1) line 1087 source
Source documentation
The column offset of the construction (handles the case m % 3 = 1).

no axioms what this means
Statement uses: Nat
Proof uses: ite, Eq, HMod.hMod, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def pOffset (m : ℕ) : ℕ := if m % 3 = 1 then 1 else 0
```
def Imo2022P6.isTreeJ Whether a cell with pattern-column residue jm6 = j % 6 and row r is a tree cell of the construction (its complement are the hills) line 1091 source
Source documentation
Whether a cell with pattern-column residue jm6 = j % 6 and row r is a tree cell of the construction (its complement are the hills).

no axioms what this means
Statement uses: Nat, Bool
Proof uses: ite, Eq, OfNat.ofNat, Bool.true, Decidable.decide, GE.ge, Or, HMod.hMod
7 instances, coercions and auxiliary constants left out.
```
def isTreeJ (jm6 : ℕ) (r : ℕ) : Bool :=
…
```
def Imo2022P6.isTree Whether a cell of the board is a tree cell of the construction line 1098 source
Source documentation
Whether a cell of the board is a tree cell of the construction.

no axioms what this means
Statement uses: Nat, Prod, Fin, Bool
Proof uses: Imo2022P6.isTreeJ, HMod.hMod, HAdd.hAdd, Prod.snd, Imo2022P6.pOffset, OfNat.ofNat, Prod.fst
6 instances, coercions and auxiliary constants left out.
```
def isTree (m : ℕ) (x : Fin m × Fin m) : Bool :=
…
```
def Imo2022P6.cspos The position of column-in-strip cs within its row in the strip order line 1102 source
Source documentation
The position of column-in-strip cs within its row in the strip order.

no axioms what this means
Statement uses: Nat
Proof uses: ite, Eq, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
```
def cspos (cs : ℕ) : ℕ := if cs = 1 then 0 else if cs = 0 then 1 else 2
```
theorem Imo2022P6.cspos_le cspos is at most 2 line 1105 source
Source documentation
cspos is at most 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Imo2022P6.cspos, OfNat.ofNat
Proof uses: dite, Eq, of_eq_true, Eq.trans, True, congrFun', congrArg, ite_eq_left_of_eq_true, ite, eq_self, Not, ite_eq_right_of_eq_false, False, eq_false
25 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem cspos_le (cs : ℕ) : cspos cs ≤ 2 := by
…
```
Mentions: Imo2022P6.cspos
theorem Imo2022P6.cspos_injective cspos is injective on {0, 1, 2} line 1109 source
Source documentation
cspos is injective on {0, 1, 2}.

standard axioms: propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Imo2022P6.cspos
Proof uses: dite, ite, of_eq_true, eq_self, Eq.symm, le_antisymm, Nat.rawCast, Mathlib.Tactic.IntervalCases.of_le_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Not, False.elim, Eq.mp, False, Eq.trans, congr, congrArg, ite_eq_right_of_eq_false, ite_eq_left_of_eq_true and 2 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem cspos_injective {a b : ℕ} (ha : a ≤ 2) (hb : b ≤ 2) (h : cspos a = cspos b) : a = b := by
…
```
Mentions: h, Imo2022P6.cspos
def Imo2022P6.subKey The within-strip order key of a cell (pattern column j, row r) line 1114 source
Source documentation
The within-strip order key of a cell (pattern column j, row r).

no axioms what this means
Statement uses: Nat
Proof uses: ite, Eq, HMod.hMod, HDiv.hDiv, OfNat.ofNat, HAdd.hAdd, HMul.hMul, HSub.hSub, Imo2022P6.cspos
12 instances, coercions and auxiliary constants left out.
```
def subKey (_m : ℕ) (j : ℕ) (r : ℕ) : ℕ :=
…
```
theorem Imo2022P6.subKey_lt The within-strip key is less than 3 * m line 1124 source
Source documentation
The within-strip key is less than 3 * m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, LE.le, OfNat.ofNat, Imo2022P6.subKey, HMul.hMul
Proof uses: id, dite, ite, Eq, HMod.hMod, HDiv.hDiv, HAdd.hAdd, HSub.hSub, Imo2022P6.cspos, Eq.mpr, congrArg, ite_eq_left, Nat.mod_lt, Decidable.byContradiction, Not, ite_eq_right, Imo2022P6.cspos_le, Decidable, congrFun'
29 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
theorem subKey_lt {m j r : ℕ} (hr : r < m) (hm : 2 ≤ m) : subKey m j r < 3 * m := by
…
```
Mentions: Imo2022P6.subKey
def Imo2022P6.keyFn The key function of the construction: tree cells come first (in strip order), then the hills (in column-major order) line 1150 source
Source documentation
The key function of the construction: tree cells come first (in strip order), then the hills (in column-major order).

no axioms what this means
Statement uses: Nat, Prod, Fin
Proof uses: ite, Eq, Bool, Imo2022P6.isTree, Bool.true, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HDiv.hDiv, Prod.snd, Imo2022P6.pOffset, Imo2022P6.subKey, Prod.fst
9 instances, coercions and auxiliary constants left out.
```
def keyFn (m : ℕ) (x : Fin m × Fin m) : ℕ :=
…
```
theorem Imo2022P6.keyFn_tree_lt The tree key is less than m * m + 3 * m line 1155 source
Source documentation
The tree key is less than m * m + 3 * m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Prod, Fin, Eq, Bool, Imo2022P6.isTree, Bool.true, LT.lt, Imo2022P6.keyFn, HAdd.hAdd, HMul.hMul
Proof uses: id, Eq.mpr, ite, HDiv.hDiv, Prod.snd, Imo2022P6.pOffset, Imo2022P6.subKey, Prod.fst, congrArg, ite_eq_left, Imo2022P6.subKey_lt, Fin.isLt, Nat.div_le_div_right, HMod.hMod, Decidable, Not, congrFun', ite_eq_right, Decidable.byContradiction, Nat.div_add_mod and 21 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem keyFn_tree_lt {m : ℕ} (hm : 2 ≤ m) (x : Fin m × Fin m) (hT : isTree m x = true) :
    keyFn m x < m * m + 3 * m := by
…
```
Mentions: Imo2022P6.isTree, Imo2022P6.keyFn
theorem Imo2022P6.subKey_inj The subKey determines the row (within a strip, for tree cells) line 1174 source
Source documentation
The subKey determines the row (within a strip, for tree cells).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo2022P6.subKey
Proof uses: dite, HMod.hMod, HDiv.hDiv, OfNat.ofNat, Eq.trans, Eq.symm, Not, LE.le, Imo2022P6.cspos, Imo2022P6.cspos_le, LT.lt, Nat.mod_lt, Decidable.byContradiction, Eq.mp, ite, HAdd.hAdd, HMul.hMul, HSub.hSub, congrArg, Decidable and 5 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 111 steps
Open to load the checked before-and-after goal states.
```
theorem subKey_inj {m j r₁ r₂ : ℕ} (h : subKey m j r₁ = subKey m j r₂) : r₁ = r₂ := by
…
```
Mentions: h, Imo2022P6.subKey
theorem Imo2022P6.subKey_inj_both The subKey of a tree cell determines its row and column-in-strip jointly line 1248 source
Source documentation
The subKey of a tree cell determines its row and column-in-strip jointly.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HDiv.hDiv, OfNat.ofNat, Bool, Imo2022P6.isTreeJ, HMod.hMod, Bool.true, Imo2022P6.subKey, And
Proof uses: LT.lt, Nat.mod_lt, Decidable.byContradiction, Not, LE.le, Imo2022P6.cspos, Imo2022P6.cspos_le, dite, And.intro, Eq.trans, Eq.symm, Eq.mp, ite, HAdd.hAdd, HMul.hMul, HSub.hSub, congrArg, Decidable, ite_eq_left, congrFun' and 16 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 116 steps
Open to load the checked before-and-after goal states.
```
theorem subKey_inj_both {m j₁ j₂ r₁ r₂ : ℕ} (hs : j₁ / 3 = j₂ / 3)
    (hT1 : isTreeJ (j₁ % 6) r₁ = true) (hT2 : isTreeJ (j₂ % 6) r₂ = true)
    (h : subKey m j₁ r₁ = subKey m j₂ r₂) : r₁ = r₂ ∧ j₁ % 3 = j₂ % 3 := by
…
```
Mentions: Imo2022P6.isTreeJ, h, Imo2022P6.subKey
theorem Imo2022P6.keyFn_injective The key function is injective line 1326 source
Source documentation
The key function is injective.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Function.Injective, Prod, Fin, Imo2022P6.keyFn
Proof uses: Eq, dite, Bool, Imo2022P6.isTree, Bool.true, LT.lt, HMul.hMul, Decidable.byContradiction, Not, Imo2022P6.subKey, HAdd.hAdd, Prod.snd, Imo2022P6.pOffset, Prod.fst, Imo2022P6.subKey_lt, Fin.isLt, HDiv.hDiv, congrArg, Eq.mp, ite and 18 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
```
theorem keyFn_injective {m : ℕ} (hm : 2 ≤ m) : Function.Injective (keyFn m) := by
…
```
Mentions: Imo2022P6.keyFn
def Imo2022P6.cellOrder The linear order on cells induced by the key function line 1372 source
Source documentation
The linear order on cells induced by the key function.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LinearOrder, Prod, Fin
Proof uses: LinearOrder.lift', Imo2022P6.keyFn, Imo2022P6.keyFn_injective
5 instances, coercions and auxiliary constants left out.
```
@[reducible] noncomputable def cellOrder (m : ℕ) (hm : 2 ≤ m) : LinearOrder (Fin m × Fin m) :=
…
```
def Imo2022P6.OrderedCell The cell type equipped with the key order (a synonym to avoid instance clashes) line 1376 source
Source documentation
The cell type equipped with the key order (a synonym to avoid instance clashes).

no axioms what this means
Statement uses: Nat
Proof uses: Prod, Fin
```
def OrderedCell (m : ℕ) := Fin m × Fin m
```
instance Imo2022P6.(instance at line 1378) line 1378 source
instance Imo2022P6.(instance at line 1380) line 1380 source
def Imo2022P6.OrderedCell.of The identity map from cells to ordered cells line 1383 source
Source documentation
The identity map from cells to ordered cells.

no axioms what this means
Statement uses: Nat, Equiv, Imo2022P6.Cell, Imo2022P6.OrderedCell
Proof uses: Equiv.refl
```
def OrderedCell.of {m : ℕ} : Cell m ≃ OrderedCell m := Equiv.refl _
```
Mentions: Imo2022P6.Cell, Imo2022P6.OrderedCell
theorem Imo2022P6.keyFn_injective' The key function is injective for all m line 1386 source
Source documentation
The key function is injective for all m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Function.Injective, Prod, Fin, Imo2022P6.keyFn
Proof uses: LT.lt, OfNat.ofNat, GE.ge, Or, Nat.lt_or_ge, dite, LE.le, Function.injective_of_subsingleton, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Not, Nat.zero_le, Imo2022P6.keyFn_injective
12 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem keyFn_injective' (m : ℕ) : Function.Injective (keyFn m) := by
…
```
Mentions: Imo2022P6.keyFn
instance Imo2022P6.OrderedCell.instLinearOrder The linear order on ordered cells given by the key function line 1392 source
Source documentation
The linear order on ordered cells given by the key function.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LinearOrder, Imo2022P6.OrderedCell
Proof uses: LinearOrder.lift', Imo2022P6.keyFn, Imo2022P6.keyFn_injective'
1 instances, coercions and auxiliary constants left out.
```
noncomputable instance OrderedCell.instLinearOrder {m : ℕ} : LinearOrder (OrderedCell m) :=
…
```
Mentions: Imo2022P6.OrderedCell
def Imo2022P6.nsOfIso The order isomorphism between all cells (with the key order) and Fin (m ^ 2) line 1396 source
Source documentation
The order isomorphism between all cells (with the key order) and Fin (m ^ 2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, OrderIso, Subtype, Imo2022P6.OrderedCell, Membership.mem, Finset, Finset.univ, Fin, HPow.hPow
Proof uses: Eq, Finset.card, OrderIso.symm, Finset.orderIsoOfFin
37 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
noncomputable def nsOfIso {m : ℕ} (_hm : 2 ≤ m) :
    ↥(Finset.univ : Finset (OrderedCell m)) ≃o Fin (m ^ 2) := by
…
```
Mentions: Imo2022P6.OrderedCell
def Imo2022P6.nsOf The constructed Nordic square: values are positions in the key order plus one line 1405 source
Source documentation
The constructed Nordic square: values are positions in the key order plus one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.NordicSquare
Proof uses: Equiv.mk, Imo2022P6.Cell, Subtype, Membership.mem, Finset, Finset.Icc, HPow.hPow, Subtype.mk, HAdd.hAdd, OrderIso, Imo2022P6.OrderedCell, Finset.univ, Fin, Imo2022P6.nsOfIso, Equiv, Imo2022P6.OrderedCell.of, OrderIso.symm, Fin.mk, HSub.hSub
37 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
noncomputable def nsOf {m : ℕ} (hm : 2 ≤ m) : NordicSquare m := by
…
```
Mentions: Imo2022P6.NordicSquare
theorem Imo2022P6.nsOf_lt_iff Comparison of values in the constructed square is comparison of keys line 1435 source
Source documentation
Comparison of values in the constructed square is comparison of keys.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Prod, Fin, Iff, LT.lt, Membership.mem, Finset, Finset.Icc, HPow.hPow, Imo2022P6.NordicSquare, Imo2022P6.Cell, Subtype, Imo2022P6.nsOf, Imo2022P6.keyFn
Proof uses: Eq, HAdd.hAdd, OrderIso, Imo2022P6.OrderedCell, Finset.univ, Imo2022P6.nsOfIso, Subtype.mk, Equiv, Imo2022P6.OrderedCell.of, Finset.mem_univ, rfl, Eq.mpr, id, congrArg, propext, Nat.add_lt_add_iff_right, OrderIso.lt_iff_lt, Iff.rfl
48 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem nsOf_lt_iff {m : ℕ} (hm : 2 ≤ m) (c c' : Fin m × Fin m) :
    (nsOf hm c : ℕ) < (nsOf hm c' : ℕ) ↔ keyFn m c < keyFn m c' := by
…
```
Mentions: Imo2022P6.nsOf, Imo2022P6.keyFn
lemma Imo2022P6.isTreeJ_true_iff Characterization of tree cells by column residue and row line 1446 source
Source documentation
Characterization of tree cells by column residue and row.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Iff, Eq, Bool, Imo2022P6.isTreeJ, Bool.true, Or, And, GE.ge, HMod.hMod
Proof uses: id, dite, ite, Decidable.decide, Eq.mpr, congrArg, ite_eq_left, iff_of_true, rfl, Or.inl, Not, ite_eq_right, decide_eq_true_eq, Iff.intro, Or.inr, And.intro, Decidable.byContradiction, HEq, Eq.refl, HEq.refl
30 instances, coercions and auxiliary constants left out.

Tactic trace: 66 steps
Open to load the checked before-and-after goal states.
```
lemma isTreeJ_true_iff {c r : ℕ} (hc : c < 6) :
    isTreeJ c r = true ↔
      c = 1 ∨ (c = 4 ∧ r ≥ 1) ∨ ((c = 0 ∨ c = 2) ∧ r % 2 = 0) ∨
        ((c = 3 ∨ c = 5) ∧ (r % 2 = 1 ∨ r = 0)) := by
…
```
Mentions: Imo2022P6.isTreeJ
def Imo2022P6.rootCell The root cell of the construction (its global key minimum) line 1490 source
Source documentation
The root cell of the construction (its global key minimum).

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.Cell
Proof uses: Prod.mk, Fin, Fin.mk
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def rootCell (m : ℕ) (hm : 2 ≤ m) : Cell m := (⟨0, by omega⟩, ⟨0, by omega⟩)
```
Mentions: Imo2022P6.Cell
theorem Imo2022P6.rootCell_isTree line 1492 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Bool, Imo2022P6.isTree, Imo2022P6.rootCell, Bool.true
Proof uses: id, Imo2022P6.isTreeJ, HMod.hMod, HAdd.hAdd, Prod.snd, Fin, Imo2022P6.pOffset, Prod.fst, ite, Decidable.decide, GE.ge, Or, Decidable, Prod.mk, Fin.mk, Not, Eq.mpr, congrFun', congrArg, ite_congr and 17 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2022P6.rootCell_key_min line 1496 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.Cell, Ne, Imo2022P6.rootCell, LT.lt, Imo2022P6.keyFn
Proof uses: Imo2022P6.pOffset, id, Eq, HMod.hMod, Decidable, ite, Not, Eq.mpr, congrFun', congrArg, ite_eq_right, Decidable.byContradiction, ite_eq_left, Bool, Imo2022P6.isTree, Bool.true, Imo2022P6.rootCell_isTree, Prod.fst, Fin, rfl and 28 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
theorem Imo2022P6.tree_key_lt_hill line 1548 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.Cell, Eq, Bool, Imo2022P6.isTree, Bool.true, Bool.false, LT.lt, Imo2022P6.keyFn
Proof uses: HAdd.hAdd, HMul.hMul, Imo2022P6.keyFn_tree_lt, Not, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, False, True, Bool.false_eq_true, not_false_eq_true, ite, HDiv.hDiv, Prod.snd, Fin, Imo2022P6.pOffset, Imo2022P6.subKey, Prod.fst and 4 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P6.keyFn_lt_of_strip_lt A tree cell in an earlier strip has a smaller key line 1560 source
Source documentation
A tree cell in an earlier strip has a smaller key.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.Cell, Eq, Bool, Imo2022P6.isTree, Bool.true, HAdd.hAdd, Prod.snd, Fin, Imo2022P6.pOffset, LT.lt, HDiv.hDiv, Prod.fst, Imo2022P6.keyFn
Proof uses: id, Eq.mpr, ite, HMul.hMul, Imo2022P6.subKey, congrArg, ite_eq_left, Imo2022P6.subKey_lt, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, 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.symm, Mathlib.Tactic.Ring.Common.add_mul and 15 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma keyFn_lt_of_strip_lt {m : ℕ} (hm : 2 ≤ m) (jy jx : ℕ) {y : Cell m}
    (hyT : isTree m y = true) {x : Cell m} (hxT : isTree m x = true)
    (hjy : y.2.1 + pOffset m = jy) (hjx : x.2.1 + pOffset m = jx)
    (hst : jy / 3 < jx / 3) (hry : y.1.1 < m) :
    keyFn m y < keyFn m x := by
…
```
Mentions: Imo2022P6.Cell, Imo2022P6.isTree, Imo2022P6.pOffset, Imo2022P6.keyFn
lemma Imo2022P6.cspos_zero line 1573 source
no axioms what this means
Statement uses: Eq, Nat, Imo2022P6.cspos, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P6.cspos_one cspos at 1 line 1576 source
Source documentation
cspos at 1.

no axioms what this means
Statement uses: Eq, Nat, Imo2022P6.cspos, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma cspos_one : cspos 1 = 0 := by decide
```
Mentions: Imo2022P6.cspos
lemma Imo2022P6.cspos_two cspos at 2 line 1579 source
Source documentation
cspos at 2.

no axioms what this means
Statement uses: Eq, Nat, Imo2022P6.cspos, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma cspos_two : cspos 2 = 2 := by decide
```
Mentions: Imo2022P6.cspos
lemma Imo2022P6.isTreeJ_zero_zero line 1581 source
no axioms what this means
Statement uses: Eq, Bool, Imo2022P6.isTreeJ, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P6.isTreeJ_one line 1583 source
no axioms what this means
Statement uses: Nat, Eq, Bool, Imo2022P6.isTreeJ, OfNat.ofNat, Bool.true
Proof uses: id, Eq.mpr, ite, Decidable.decide, GE.ge, Or, HMod.hMod, congrArg, ite_eq_left, rfl, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P6.isTreeJ_two_zero line 1587 source
no axioms what this means
Statement uses: Eq, Bool, Imo2022P6.isTreeJ, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P6.isTreeJ_three_zero line 1589 source
no axioms what this means
Statement uses: Eq, Bool, Imo2022P6.isTreeJ, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P6.isTreeJ_three_one line 1591 source
no axioms what this means
Statement uses: Eq, Bool, Imo2022P6.isTreeJ, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P6.isTreeJ_four line 1593 source
standard axioms: propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Bool, Imo2022P6.isTreeJ, Bool.true
Proof uses: id, Eq.mpr, ite, Decidable.decide, GE.ge, Or, HMod.hMod, congrArg, ite_eq_right, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool.false, ite_eq_left, rfl, decide_eq_true_eq
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P6.isTreeJ_five_zero line 1598 source
no axioms what this means
Statement uses: Eq, Bool, Imo2022P6.isTreeJ, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P6.isTreeJ_five_one line 1600 source
no axioms what this means
Statement uses: Eq, Bool, Imo2022P6.isTreeJ, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P6.subKey_even_zero subKey at row 0 of an even strip line 1603 source
Source documentation
subKey at row 0 of an even strip.

no axioms what this means
Statement uses: Nat, Eq, HMod.hMod, HDiv.hDiv, OfNat.ofNat, Imo2022P6.subKey
Proof uses: id, Eq.mpr, ite, HAdd.hAdd, HMul.hMul, HSub.hSub, Imo2022P6.cspos, congrArg, ite_eq_left, rfl, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma subKey_even_zero {m j : ℕ} (hj : (j / 3) % 2 = 0) : subKey m j 0 = j % 3 := by
…
```
Mentions: Imo2022P6.subKey
lemma Imo2022P6.subKey_even_of_ne_zero subKey at a positive row of an even strip line 1608 source
Source documentation
subKey at a positive row of an even strip.

no axioms what this means
Statement uses: Nat, Eq, HMod.hMod, HDiv.hDiv, OfNat.ofNat, Ne, Imo2022P6.subKey, HAdd.hAdd, HMul.hMul, HSub.hSub, Imo2022P6.cspos
Proof uses: id, Eq.mpr, ite, congrArg, ite_eq_left, ite_eq_right, Eq.refl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma subKey_even_of_ne_zero {m j r : ℕ} (hj : (j / 3) % 2 = 0) (hr : r ≠ 0) :
    subKey m j r = 3 + 3 * (r - 1) + cspos (j % 3) := by
…
```
Mentions: Imo2022P6.subKey, Imo2022P6.cspos
lemma Imo2022P6.subKey_odd_zero subKey at row 0 of an odd strip line 1614 source
Source documentation
subKey at row 0 of an odd strip.

no axioms what this means
Statement uses: Nat, Ne, HMod.hMod, HDiv.hDiv, OfNat.ofNat, Eq, Imo2022P6.subKey, ite
Proof uses: id, Eq.mpr, HAdd.hAdd, HMul.hMul, HSub.hSub, Imo2022P6.cspos, congrArg, ite_eq_right, ite_eq_left, rfl, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma subKey_odd_zero {m j : ℕ} (hj : (j / 3) % 2 ≠ 0) :
    subKey m j 0 = (if j % 3 = 0 then 0 else 4) := by
…
```
Mentions: Imo2022P6.subKey
lemma Imo2022P6.subKey_odd_one subKey at row 1 of an odd strip line 1620 source
Source documentation
subKey at row 1 of an odd strip.

standard axioms: propext what this means
Statement uses: Nat, Ne, HMod.hMod, HDiv.hDiv, OfNat.ofNat, Eq, Imo2022P6.subKey, HAdd.hAdd
Proof uses: id, Eq.mpr, ite, HMul.hMul, HSub.hSub, Imo2022P6.cspos, congrArg, ite_eq_right, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, ite_eq_left, rfl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma subKey_odd_one {m j : ℕ} (hj : (j / 3) % 2 ≠ 0) :
    subKey m j 1 = 1 + j % 3 := by
…
```
Mentions: Imo2022P6.subKey
lemma Imo2022P6.subKey_odd_of_ge_two subKey at a row ≥ 2 of an odd strip line 1626 source
Source documentation
subKey at a row ≥ 2 of an odd strip.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Ne, HMod.hMod, HDiv.hDiv, OfNat.ofNat, LE.le, Eq, Imo2022P6.subKey, HAdd.hAdd, HMul.hMul, HSub.hSub, Imo2022P6.cspos
Proof uses: id, Eq.mpr, ite, congrArg, ite_eq_right, Eq.refl
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma subKey_odd_of_ge_two {m j r : ℕ} (hj : (j / 3) % 2 ≠ 0) (hr : 2 ≤ r) :
    subKey m j r = 5 + 3 * (r - 2) + cspos (j % 3) := by
…
```
Mentions: Imo2022P6.subKey, Imo2022P6.cspos
lemma Imo2022P6.keyFn_lt_of_same_strip Between two tree cells in the same strip, the key order is the subKey order line 1632 source
Source documentation
Between two tree cells in the same strip, the key order is the subKey order.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.Cell, Eq, Bool, Imo2022P6.isTree, Bool.true, HAdd.hAdd, Prod.snd, Fin, Imo2022P6.pOffset, HDiv.hDiv, OfNat.ofNat, LT.lt, Imo2022P6.subKey, Prod.fst, Imo2022P6.keyFn
Proof uses: id, Eq.mpr, ite, HMul.hMul, congrArg, ite_eq_left, Decidable.byContradiction, Not
19 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma keyFn_lt_of_same_strip {m : ℕ} (jy jx : ℕ) {y : Cell m}
    (hyT : isTree m y = true) {x : Cell m} (hxT : isTree m x = true)
    (hjy : y.2.1 + pOffset m = jy) (hjx : x.2.1 + pOffset m = jx)
    (hst : jy / 3 = jx / 3) (hsub : subKey m jy y.1.1 < subKey m jx x.1.1) :
    keyFn m y < keyFn m x := by
…
```
Mentions: Imo2022P6.Cell, Imo2022P6.isTree, Imo2022P6.pOffset, Imo2022P6.subKey, Imo2022P6.keyFn
theorem Imo2022P6.parent_exists A tree cell in an earlier strip has a smaller key line 1642 source
Source documentation
A tree cell in an earlier strip has a smaller key.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.Cell, Eq, Bool, Imo2022P6.isTree, Bool.true, Ne, Imo2022P6.rootCell, Exists, And, Imo2022P6.Adjacent, LT.lt, Imo2022P6.keyFn
Proof uses: Fin, Prod.mk, Fin.isLt, Imo2022P6.pOffset, id, HMod.hMod, Decidable, ite, Not, Eq.mpr, congrFun', congrArg, ite_eq_right, Decidable.byContradiction, ite_eq_left, HAdd.hAdd, rfl, Imo2022P6.isTreeJ, False, Fin.mk and 63 more
142 instances, coercions and auxiliary constants left out.

Tactic trace: 495 steps (first 200 of 495)
Open to load the checked before-and-after goal states.
```
theorem parent_exists {m : ℕ} (hm : 2 ≤ m) (x : Cell m)
    (hx : isTree m x = true) (hx0 : x ≠ rootCell m hm) :
    ∃ y : Cell m, Adjacent x y ∧ isTree m y = true ∧ keyFn m y < keyFn m x := by
…
```
Mentions: Imo2022P6.Cell, Imo2022P6.isTree, Imo2022P6.rootCell, Imo2022P6.Adjacent, Imo2022P6.keyFn
theorem Imo2022P6.keyFn_tree_eq line 1957 source
no axioms what this means
Statement uses: Nat, Imo2022P6.Cell, Eq, Bool, Imo2022P6.isTree, Bool.true, Imo2022P6.keyFn, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HDiv.hDiv, Prod.snd, Fin, Imo2022P6.pOffset, Imo2022P6.subKey, Prod.fst
Proof uses: id, Eq.mpr, ite, congrArg, ite_eq_left, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2022P6.subKey_even_pos subKey in an even strip, row 0 line 1964 source
Source documentation
subKey in an even strip, row 0.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, HDiv.hDiv, OfNat.ofNat, LE.le, Imo2022P6.subKey, HAdd.hAdd, HMul.hMul, HSub.hSub, Imo2022P6.cspos
Proof uses: id, Eq.mpr, ite, congrArg, ite_eq_left, ite_eq_right, Eq.refl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem subKey_even_pos {m j r : ℕ} (hs : (j / 3) % 2 = 0) (hr : 1 ≤ r) :
    subKey m j r = 3 + 3 * (r - 1) + cspos (j % 3) := by
…
```
Mentions: Imo2022P6.subKey, Imo2022P6.cspos
theorem Imo2022P6.rule_down If the tree cell y directly below the tree cell x has smaller key, then x has pattern column 5 (mod 6) and row 0 line 1972 source
Source documentation
If the tree cell y directly below the tree cell x has smaller key, then x has pattern column 5 (mod 6) and row 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.Cell, Eq, Bool, Imo2022P6.isTree, Bool.true, Prod.snd, Fin, Prod.fst, HAdd.hAdd, LT.lt, Imo2022P6.keyFn, And, HMod.hMod, Imo2022P6.pOffset
Proof uses: Imo2022P6.subKey, Decidable.byContradiction, Not, Eq.mp, HMul.hMul, HDiv.hDiv, congrArg, Imo2022P6.keyFn_tree_eq, Nat.mod_lt, Imo2022P6.cspos, Imo2022P6.cspos_le, dite, Imo2022P6.isTreeJ, HSub.hSub, Imo2022P6.subKey_even_pos, Imo2022P6.subKey_even_zero, Eq.symm, Eq.refl, ite, ite_eq_left and 19 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
```
theorem rule_down {m : ℕ} (_hm : 2 ≤ m) (x y : Cell m)
    (hx : isTree m x = true) (hy : isTree m y = true)
    (hcol : y.2.1 = x.2.1) (hrow : y.1.1 = x.1.1 + 1)
    (hyk : keyFn m y < keyFn m x) :
    (x.2.1 + pOffset m) % 6 = 5 ∧ x.1.1 = 0 := by
…
```
Mentions: Imo2022P6.Cell, Imo2022P6.isTree, Imo2022P6.keyFn, Imo2022P6.pOffset
theorem Imo2022P6.rule_up Documented declaration: rule_up line 2019 source
Source documentation
If the tree cell y directly above the tree cell x has smaller key, then x has pattern column 1 (mod 6) with a positive row, or pattern column 3 and row 1, or pattern column 4 and row at least 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.Cell, Eq, Bool, Imo2022P6.isTree, Bool.true, Prod.snd, Fin, HAdd.hAdd, Prod.fst, LT.lt, Imo2022P6.keyFn, Or, And, HMod.hMod, Imo2022P6.pOffset
Proof uses: HSub.hSub, Decidable.byContradiction, Not, Imo2022P6.subKey, Eq.mp, HMul.hMul, HDiv.hDiv, congrArg, Imo2022P6.keyFn_tree_eq, dite, Imo2022P6.isTreeJ, Eq.trans, Decidable.decide, congrFun', ite, GE.ge, ite_eq_right_of_eq_false, ite_eq_left_of_eq_true, True, False and 22 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
theorem rule_up {m : ℕ} (_hm : 2 ≤ m) (x y : Cell m)
    (hx : isTree m x = true) (hy : isTree m y = true)
    (hcol : y.2.1 = x.2.1) (hrow : y.1.1 + 1 = x.1.1)
    (hyk : keyFn m y < keyFn m x) :
    (x.2.1 + pOffset m) % 6 = 1 ∧ 1 ≤ x.1.1 ∨
      (x.2.1 + pOffset m) % 6 = 3 ∧ x.1.1 = 1 ∨
        (x.2.1 + pOffset m) % 6 = 4 ∧ 2 ≤ x.1.1 := by
…
```
Mentions: Imo2022P6.Cell, Imo2022P6.isTree, Imo2022P6.keyFn, Imo2022P6.pOffset
theorem Imo2022P6.rule_left If the tree cell y directly left of the tree cell x has smaller key, then the pattern column and row of x satisfy one of six mutually exclusive signatures line 2070 source
Source documentation
If the tree cell y directly left of the tree cell x has smaller key, then the pattern column and row of x satisfy one of six mutually exclusive signatures.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.Cell, Eq, Bool, Imo2022P6.isTree, Bool.true, Prod.fst, Fin, HAdd.hAdd, Prod.snd, LT.lt, Imo2022P6.keyFn, Or, And, HMod.hMod, Imo2022P6.pOffset
Proof uses: Decidable.byContradiction, Not, Eq.refl, dite, HDiv.hDiv, Or.inl, And.intro, Eq.mp, Imo2022P6.isTreeJ, Eq.trans, Decidable.decide, congrFun', congrArg, ite, GE.ge, ite_eq_right_of_eq_false, ite_eq_left_of_eq_true, True, False, congr and 27 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 111 steps
Open to load the checked before-and-after goal states.
```
theorem rule_left {m : ℕ} (_hm : 2 ≤ m) (x y : Cell m)
    (hx : isTree m x = true) (hy : isTree m y = true)
    (hrow : y.1.1 = x.1.1) (hcol : y.2.1 + 1 = x.2.1)
    (hyk : keyFn m y < keyFn m x) :
    (x.2.1 + pOffset m) % 6 = 0 ∧ x.1.1 = 0 ∨
      (x.2.1 + pOffset m) % 6 = 3 ∧ x.1.1 = 0 ∨
        (x.2.1 + pOffset m) % 6 = 1 ∧ x.1.1 = 0 ∨
          (x.2.1 + pOffset m) % 6 = 2 ∨
            (x.2.1 + pOffset m) % 6 = 4 ∧ x.1.1 = 1 ∨
              (x.2.1 + pOffset m) % 6 = 5 ∧ 1 ≤ x.1.1 := by
…
```
Mentions: Imo2022P6.Cell, Imo2022P6.isTree, Imo2022P6.keyFn, Imo2022P6.pOffset
theorem Imo2022P6.rule_right If the tree cell y directly right of the tree cell x has smaller key, then x has pattern column 0 (mod 6) and row at least 2, or pattern column 3 and row at least 3 line 2152 source
Source documentation
If the tree cell y directly right of the tree cell x has smaller key, then x has pattern column 0 (mod 6) and row at least 2, or pattern column 3 and row at least 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.Cell, Eq, Bool, Imo2022P6.isTree, Bool.true, Prod.fst, Fin, Prod.snd, HAdd.hAdd, LT.lt, Imo2022P6.keyFn, Or, And, HMod.hMod, Imo2022P6.pOffset
Proof uses: Fin.isLt, Decidable.byContradiction, Not, Eq.refl, dite, HDiv.hDiv, Imo2022P6.subKey, Eq.mp, HMul.hMul, congrArg, Imo2022P6.keyFn_tree_eq, Imo2022P6.isTreeJ, Imo2022P6.subKey_even_zero, Eq.symm, Or.inl, And.intro, Eq.trans, Decidable.decide, congrFun', ite and 50 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 121 steps
Open to load the checked before-and-after goal states.
```
theorem rule_right {m : ℕ} (hm : 2 ≤ m) (x y : Cell m)
    (hx : isTree m x = true) (hy : isTree m y = true)
    (hrow : y.1.1 = x.1.1) (hcol : y.2.1 = x.2.1 + 1)
    (hyk : keyFn m y < keyFn m x) :
    (x.2.1 + pOffset m) % 6 = 0 ∧ 2 ≤ x.1.1 ∨
      (x.2.1 + pOffset m) % 6 = 3 ∧ 3 ≤ x.1.1 := by
…
```
Mentions: Imo2022P6.Cell, Imo2022P6.isTree, Imo2022P6.keyFn, Imo2022P6.pOffset
theorem Imo2022P6.adjacent_dir Two adjacent cells differ by one in exactly one coordinate line 2241 source
Source documentation
Two adjacent cells differ by one in exactly one coordinate.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.Cell, Imo2022P6.Adjacent, Or, And, Eq, Prod.fst, Fin, Prod.snd, HAdd.hAdd, OfNat.ofNat
Proof uses: HSub.hSub, Imo2022P6.Adjacent.dist, Decidable.byContradiction, Not
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem adjacent_dir {n : ℕ} {x y : Cell n} (h : Adjacent x y) :
    (x.1.1 = y.1.1 ∧ x.2.1 = y.2.1 + 1) ∨ (x.1.1 = y.1.1 ∧ y.2.1 = x.2.1 + 1) ∨
      (x.2.1 = y.2.1 ∧ x.1.1 = y.1.1 + 1) ∨ (x.2.1 = y.2.1 ∧ y.1.1 = x.1.1 + 1) := by
…
```
Mentions: Imo2022P6.Cell, h, Imo2022P6.Adjacent
theorem Imo2022P6.smaller_neighbor_unique line 2248 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.Cell, Eq, Bool, Imo2022P6.isTree, Bool.true, Imo2022P6.Adjacent, LT.lt, Imo2022P6.keyFn
Proof uses: Or, And, Prod.fst, Fin, Prod.snd, HAdd.hAdd, Imo2022P6.adjacent_dir, Prod.ext, Fin.ext, Decidable.byContradiction, Not, False.elim, HMod.hMod, Imo2022P6.pOffset, Imo2022P6.rule_left, Eq.symm, Imo2022P6.rule_right, Imo2022P6.rule_up, Imo2022P6.rule_down
32 instances, coercions and auxiliary constants left out.

Tactic trace: 80 steps
Open to load the checked before-and-after goal states.
theorem Imo2022P6.hill_neighbor_tree line 2309 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P6.Cell, Eq, Bool, Imo2022P6.isTree, Bool.false, Imo2022P6.Adjacent, Bool.true
Proof uses: HAdd.hAdd, HSub.hSub, Prod.fst, Fin, Prod.snd, OfNat.ofNat, Imo2022P6.Adjacent.dist, id, LT.lt, HMod.hMod, Imo2022P6.pOffset, Nat.mod_lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Eq.mpr, Imo2022P6.isTreeJ, Or, And, GE.ge and 7 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem Imo2022P6.tree_not_hill line 2322 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2022P6.Cell, Eq, Bool, Imo2022P6.isTree, Bool.true, Exists, And, Imo2022P6.Adjacent, LT.lt, Imo2022P6.keyFn
Proof uses: Fin, Prod.mk, Fin.isLt, Or, Imo2022P6.pOffset, dite, HMod.hMod, of_eq_true, Eq.trans, False, True, congr, congrArg, congrFun', ite_eq_left_of_eq_true, eq_self, or_true, Not, ite_eq_right_of_eq_false, eq_false and 47 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 495 steps (first 200 of 495)
Open to load the checked before-and-after goal states.
theorem Imo2022P6.nordicSquare_good Documented declaration: nordicSquare_good line 2671 source
Source documentation
The construction (the strip pattern from the official IMO 2022 solution, as drawn in Evan Chen's IMO 2022 Solution Notes): for every m ≥ 2 there is a "good" Nordic square on the m × m board (exactly one valley, every non-hill cell has exactly one smaller-valued neighbor, hills are pairwise non-adjacent), which therefore has exactly 2 * m * (m - 1) + 1 uphill paths.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Imo2022P6.NordicSquare, Imo2022P6.NordicSquare.Good
Proof uses: Exists.intro, Imo2022P6.nsOf, Eq, Bool, Imo2022P6.isTree, Imo2022P6.rootCell, Bool.true, Imo2022P6.rootCell_isTree, Imo2022P6.Cell, Iff, Imo2022P6.NordicSquare.Hill, Bool.false, Iff.intro, Decidable.byContradiction, Not, And, Imo2022P6.Adjacent, LT.lt, Imo2022P6.keyFn, False and 35 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 70 steps
Open to load the checked before-and-after goal states.
```
theorem nordicSquare_good (m : ℕ) (hm : 2 ≤ m) : ∃ ns : NordicSquare m, ns.Good := by
…
```
Mentions: Imo2022P6.NordicSquare
determine Imo2022P6.answer line 2739 source
standard axioms: propext what this means
Statement uses: PNat, Nat
Proof uses: HAdd.hAdd, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow
12 instances, coercions and auxiliary constants left out.
theorem Imo2022P6.answer_val The answer expressed as 2 * n * (n - 1) + 1 line 2742 source
Source documentation
The answer expressed as 2 * n * (n - 1) + 1.

standard axioms: Quot.sound, propext what this means
Statement uses: PNat, Eq, Nat, Imo2022P6.answer, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HSub.hSub
Proof uses: Eq.symm, Nat.succ, Nat.sub_add_cancel, PNat.pos, Eq.mpr, HPow.hPow, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Imo2022P6.answer.eq_1, Imo2022P6.answer_eq, Nat.mul_assoc
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem answer_val (n : ℕ+) : answer n = 2 * (n : ℕ) * ((n : ℕ) - 1) + 1 := by
…
```
Mentions: Imo2022P6.answer
problem Imo2022P6.imo2022_p6 line 2747 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, IsLeast, Nat, Set.ofPred, Exists, Imo2022P6.NordicSquare, Eq, Cardinal, Cardinal.mk, Imo2022P6.NordicSquare.UphillPath, Imo2022P6.answer
Proof uses: And.intro, Membership.mem, Set, lowerBounds, dite, OfNat.ofNat, Subtype.ext, LT.lt, Eq.mpr, id, congrArg, rfl, Exists.intro, Equiv.mk, Imo2022P6.Cell, Subtype, Finset, Finset.Icc, HPow.hPow, Subtype.mk and 46 more
77 instances, coercions and auxiliary constants left out.

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