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

36 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2022, Problem 3

Let k be a positive integer and let S be a finite set of odd prime integers. Prove that there is at most one way (up to rotation and reflection) to place the elements of S around a circle such that the product of any two neighbors is of the form x² + x + k for some positive integer x.

(formalization note: S is assumed to be nonempty; the statement would be false for S = ∅ because the rotations are indexed by the empty type Fin #S.)

Imports (7)

Imported by 1 file

Compfiles.lean

def Imo2022P3.Condition The condition of the problem on a placement of numbers round a circle line 44 source
Source documentation
The condition of the problem on a placement of numbers round a circle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Equiv, Fin, Finset.card, Subtype, Membership.mem
Proof uses: NeZero, Exists, And, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HPow.hPow
23 instances, coercions and auxiliary constants left out.
```
def Condition (k : ℕ) (S : Finset ℕ) (p : Fin #S ≃ S) : Prop :=
…
```
Mentions: S
def Imo2022P3.good Auxiliary condition: m * n is of the form x ^ 2 + x + k for a nonnegative integer x line 53 source
Source documentation
Auxiliary condition: m * n is of the form x ^ 2 + x + k for a nonnegative integer x. The problem uses positive x, but uniqueness of placements for the weaker (nonnegative) condition implies uniqueness for the stronger one.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: Exists, Eq, HMul.hMul, HAdd.hAdd, HPow.hPow, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
```
def good (k m n : ℕ) : Prop := ∃ x : ℕ, m * n = x ^ 2 + x + k
```
lemma Imo2022P3.lt_of_good_of_lt A product below M ^ 2 that is good forces the witness x to be below M line 56 source
Source documentation
A product below M ^ 2 that is good forces the witness x to be below M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LT.lt, Eq, HMul.hMul, HAdd.hAdd, HPow.hPow, OfNat.ofNat
Proof uses: Nat.Prime.pos, Nat.mul_lt_mul_of_pos_left, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos and 69 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma lt_of_good_of_lt {k M q x : ℕ} (hM : Nat.Prime M) (hq : q < M)
    (hx : M * q = x ^ 2 + x + k) : x < M := by
…
```
lemma Imo2022P3.add_eq_of_dvd_of_dvd Two distinct roots of T ^ 2 + T + k below the prime M sum to M - 1 line 63 source
Source documentation
Two distinct roots of T ^ 2 + T + k below the prime M sum to M - 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LT.lt, Ne, Dvd.dvd, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Eq
Proof uses: Nat.Prime.pos, Fact, Fact.mk, ZMod, Iff.mpr, ZMod.natCast_eq_zero_iff, Eq.mp, congrFun', congrArg, Eq.trans, Nat.cast_add, Nat.cast_pow, HMul.hMul, HSub.hSub, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.add_eq_eq, Eq.symm, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr and 79 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
```
lemma add_eq_of_dvd_of_dvd {k M x y : ℕ} (hM : Nat.Prime M) (hxM : x < M) (hyM : y < M)
    (hxy : x ≠ y) (hx : M ∣ x ^ 2 + x + k) (hy : M ∣ y ^ 2 + y + k) :
    x + y + 1 = M := by
…
```
lemma Imo2022P3.dvd_sub_of_good_of_good Vieta for the two roots: their product is congruent to k modulo M line 106 source
Source documentation
Vieta for the two roots: their product is congruent to k modulo M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LT.lt, Ne, Eq, HMul.hMul, HAdd.hAdd, HPow.hPow, OfNat.ofNat, And, Dvd.dvd, Int, HSub.hSub
Proof uses: Nat.Prime.pos, Fact, Fact.mk, Imo2022P3.lt_of_good_of_lt, False, Eq.mpr, id, congrArg, Eq.refl, Nat.eq_of_mul_eq_mul_left, Imo2022P3.add_eq_of_dvd_of_dvd, Exists.intro, Eq.symm, And.intro, ZMod, Iff.mpr, ZMod.natCast_eq_zero_iff, Eq.mp, congrFun', Eq.trans and 64 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma dvd_sub_of_good_of_good {k M q r x y : ℕ} (hM : Nat.Prime M)
    (hq : q < M) (hr : r < M) (hqr : q ≠ r)
    (hx : M * q = x ^ 2 + x + k) (hy : M * r = y ^ 2 + y + k) :
    x + y + 1 = M ∧ (M : ℤ) ∣ (x * y : ℤ) - k := by
…
```
lemma Imo2022P3.good_of_good_of_good The key multiplicativity lemma (Chen's Claim 2): if the prime M has two distinct smaller good partners q and r, then q * r is itself good line 141 source
Source documentation
The key multiplicativity lemma (Chen's Claim 2): if the prime M has two distinct smaller good partners q and r, then q * r is itself good.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LT.lt, Ne, Imo2022P3.good
Proof uses: Eq, HMul.hMul, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Dvd.dvd, Int, HSub.hSub, And, Imo2022P3.dvd_sub_of_good_of_good, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_zero, Nat.Prime.pos, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr and 83 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
```
lemma good_of_good_of_good {k M q r : ℕ} (hM : Nat.Prime M) (hq : q < M) (hr : r < M)
    (hqr : q ≠ r) (h1 : good k M q) (h2 : good k M r) : good k q r := by
…
```
Mentions: Imo2022P3.good
lemma Imo2022P3.card_roots_le_two A quadratic has at most two roots below a prime M: the set T of solutions x < M to M ∣ x ^ 2 + x + k has at most two elements line 180 source
Source documentation
A quadratic has at most two roots below a prime M: the set T of solutions x < M to M ∣ x ^ 2 + x + k has at most two elements.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Finset, Membership.mem, LT.lt, Dvd.dvd, HAdd.hAdd, HPow.hPow, OfNat.ofNat, LE.le, Finset.card
Proof uses: dite, Finset.Nonempty, Finset.erase, Finset.min', Eq, rfl, Eq.mp, congrArg, Finset.min'_mem, Finset.mem_of_mem_erase, Ne, Finset.min'_erase_ne_self, Insert.insert, Singleton.singleton, Decidable.byContradiction, Not, And.left, And, Eq.trans, Or and 23 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma card_roots_le_two {k M : ℕ} (hM : Nat.Prime M) (T : Finset ℕ)
    (hT1 : ∀ x ∈ T, x < M) (hT2 : ∀ x ∈ T, M ∣ x ^ 2 + x + k) : T.card ≤ 2 := by
…
```
lemma Imo2022P3.card_good_le_two Chen's Claim 1: a prime M has at most two good partners below it inside any set of smaller numbers line 220 source
Source documentation
Chen's Claim 1: a prime M has at most two good partners below it inside any set of smaller numbers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Finset, DecidablePred, Imo2022P3.good, Membership.mem, LT.lt, LE.le, Finset.card, Finset.filter, OfNat.ofNat
Proof uses: dite, Exists.choose, Eq, HMul.hMul, HAdd.hAdd, HPow.hPow, Not, rfl, And.right, Eq.mp, And, congrArg, propext, Finset.mem_filter, Exists.choose_spec, Eq.mpr, id, congrFun', congr, Eq.trans and 18 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma card_good_le_two {k M : ℕ} (hM : Nat.Prime M) (S : Finset ℕ)
    [DecidablePred (good k M)] (hSM : ∀ q ∈ S, q < M) :
    (S.filter (good k M ·)).card ≤ 2 := by
…
```
Mentions: S, Imo2022P3.good
lemma Imo2022P3.good_comm good is symmetric in the two factors line 248 source
Source documentation
good is symmetric in the two factors.

standard axioms: propext what this means
Statement uses: Nat, Imo2022P3.good
Proof uses: Eq, HMul.hMul, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Exists.intro, Eq.mpr, id, congrArg, mul_comm
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma good_comm {k m n : ℕ} (h : good k m n) : good k n m := by
…
```
Mentions: h, Imo2022P3.good
lemma Imo2022P3.zmod_inj Injectivity of the ZMod n cast on Fin n line 253 source
Source documentation
Injectivity of the ZMod n cast on Fin n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, ZMod
Proof uses: Fin.ext, Nat.ModEq.eq_of_lt_of_lt, Eq.mp, Nat.ModEq, congrArg, propext, ZMod.natCast_eq_natCast_iff, Fin.isLt
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma zmod_inj {n : ℕ} {a b : Fin n} (h : (a.val : ZMod n) = b.val) : a = b := by
…
```
Mentions: h
lemma Imo2022P3.zmod_add The ZMod n cast of a sum in Fin n line 258 source
Source documentation
The ZMod n cast of a sum in Fin n.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, ZMod, HAdd.hAdd
Proof uses: Eq.mpr, HMod.hMod, id, congrArg, Fin.val_add, ZMod.natCast_mod, Nat.cast_add, Eq.refl
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma zmod_add {n : ℕ} (a b : Fin n) : ((a + b).val : ZMod n) = a.val + b.val := by
…
```
lemma Imo2022P3.zmod_one The ZMod n cast of 1 : Fin n line 262 source
Source documentation
The ZMod n cast of 1 : Fin n.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, Eq, ZMod, OfNat.ofNat, Fin
Proof uses: Eq.mpr, HMod.hMod, id, congrArg, Fin.val_one', ZMod.natCast_mod, Nat.cast_one, Eq.refl
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma zmod_one {n : ℕ} [NeZero n] : ((1 : Fin n).val : ZMod n) = 1 := by
…
```
lemma Imo2022P3.zmod_rev The ZMod n cast of Fin.rev line 266 source
Source documentation
The ZMod n cast of Fin.rev.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, Eq, ZMod, Fin.rev, HSub.hSub, Neg.neg, OfNat.ofNat
Proof uses: HAdd.hAdd, rfl, LE.le, Fin.isLt, Eq.mpr, id, congrArg, Nat.cast_sub, ZMod.natCast_self, congrFun', Eq.trans, Nat.cast_add, Nat.cast_one, Mathlib.Tactic.Ring.of_eq, Int.rawCast, inferInstance, Ring, Int.negOfNat, HMul.hMul, HPow.hPow and 25 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma zmod_rev {n : ℕ} [NeZero n] (j : Fin n) :
    ((Fin.rev j).val : ZMod n) = -1 - j.val := by
…
```
def Imo2022P3.succPerm The successor permutation of a placement: sends each element to its clockwise neighbor line 276 source
Source documentation
The successor permutation of a placement: sends each element to its clockwise neighbor.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Equiv, Fin, Finset.card, Subtype, Membership.mem, Equiv.Perm
Proof uses: Equiv.trans, Equiv.symm, finRotate
4 instances, coercions and auxiliary constants left out.
```
def succPerm {S : Finset ℕ} (p : Fin #S ≃ S) : Equiv.Perm S :=
…
```
Mentions: S
lemma Imo2022P3.succPerm_apply line 279 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, NeZero, Finset.card, Equiv, Fin, Subtype, Membership.mem, Eq, Equiv.Perm, Imo2022P3.succPerm, HAdd.hAdd, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, Fin.neZero, True, congrFun', congrArg, Equiv.trans, Equiv.symm, finRotate, Equiv.symm_apply_apply, finRotate_apply, eq_self
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2022P3.ValidPerm Validity of a permutation of S: every element has a good product with its successor line 285 source
Source documentation
Validity of a permutation of S: every element has a good product with its successor.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Equiv.Perm, Subtype, Membership.mem
Proof uses: Imo2022P3.good
8 instances, coercions and auxiliary constants left out.
```
def ValidPerm (k : ℕ) {S : Finset ℕ} (σ : Equiv.Perm S) : Prop :=
…
```
Mentions: S
def Imo2022P3.ConnectedP Connectivity of a permutation of S: it is a single cycle line 289 source
Source documentation
Connectivity of a permutation of S: it is a single cycle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Equiv.Perm, Subtype, Membership.mem
Proof uses: Exists, Eq, Nat.iterate
7 instances, coercions and auxiliary constants left out.
```
def ConnectedP {S : Finset ℕ} (σ : Equiv.Perm S) : Prop :=
…
```
Mentions: S
lemma Imo2022P3.validPerm_succPerm line 292 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, NeZero, Finset.card, Equiv, Fin, Subtype, Membership.mem, Imo2022P3.good, HAdd.hAdd, OfNat.ofNat, Imo2022P3.ValidPerm, Imo2022P3.succPerm
Proof uses: Eq, Equiv.Perm, Equiv.symm, of_eq_true, Eq.trans, Fin.neZero, True, congrFun', congrArg, Equiv.trans, finRotate, finRotate_apply, eq_self, Eq.mpr, id, Eq.mp, Equiv.apply_symm_apply
22 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P3.iterate_conj Iteration of a conjugated map line 301 source
Source documentation
Iteration of a conjugated map.

standard axioms: Quot.sound, propext what this means
Statement uses: Equiv, Nat, Eq, Nat.iterate, Function.comp, Equiv.symm
Proof uses: Nat.recAux, funext, OfNat.ofNat, of_eq_true, Eq.trans, True, congrArg, congrFun', CompTriple.comp_eq, id, Equiv.apply_symm_apply, eq_self, Eq.mpr, HAdd.hAdd, Nat.succ, Function.iterate_succ', Equiv.symm_apply_apply, Function.iterate_succ_apply', Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma iterate_conj {α β : Type*} (c : α ≃ β) (τ : α → α) (m : ℕ) :
    (⇑c ∘ τ ∘ ⇑c.symm)^[m] = ⇑c ∘ τ^[m] ∘ ⇑c.symm := by
…
```
lemma Imo2022P3.iterate_finRotate line 313 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, Eq, Nat.iterate, Equiv.Perm, finRotate, HAdd.hAdd, Fin.NatCast.instNatCast
Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congrArg, Fin.instAddMonoidWithOne, Nat.cast_zero, add_zero, eq_self, Eq.mpr, id, Nat.succ, Function.iterate_succ_apply', Fin.neZero, finRotate_apply, Imo2022P3.zmod_inj, ZMod, congr, Imo2022P3.zmod_add and 15 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P3.succPerm_iterate line 323 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, NeZero, Finset.card, Equiv, Fin, Subtype, Membership.mem, Eq, Nat.iterate, Equiv.Perm, Imo2022P3.succPerm, HAdd.hAdd, Fin.NatCast.instNatCast
Proof uses: Function.comp, finRotate, Equiv.symm, funext, of_eq_true, Eq.trans, OfNat.ofNat, Fin.neZero, True, congr, congrArg, Equiv.trans, finRotate_apply, eq_self, Eq.mpr, id, Imo2022P3.iterate_conj, congrFun', Equiv.symm_apply_apply, Imo2022P3.iterate_finRotate and 1 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P3.connectedP_succPerm line 336 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Finset.Nonempty, Equiv, Fin, Finset.card, Subtype, Membership.mem, Imo2022P3.ConnectedP, Imo2022P3.succPerm
Proof uses: NeZero, NeZero.mk, LT.lt.ne', OfNat.ofNat, Iff.mpr, LT.lt, Finset.card_pos, Equiv.symm, Eq, Equiv.apply_symm_apply, Exists.intro, Nat.iterate, Equiv.Perm, ZMod.val, HSub.hSub, ZMod, Eq.mpr, id, congrArg, Eq.symm and 47 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P3.zmod_eq_of_add_key A permutation of Fin n commuting with + 1 is a rotation line 352 source
Source documentation
A permutation of Fin n commuting with + 1 is a rotation.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, Equiv.Perm, Fin, Eq, HAdd.hAdd, OfNat.ofNat, ZMod
Proof uses: Nat.succ, Exists, Nat.exists_eq_succ_of_ne_zero, NeZero.ne, Fin.induction, of_eq_true, Eq.trans, True, congrArg, Nat.cast_zero, add_zero, eq_self, Fin.castSucc, Eq.mpr, Fin.succ, id, Eq.symm, Fin.coeSucc_eq_succ, congr, Imo2022P3.zmod_add and 16 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma zmod_eq_of_add_key {n : ℕ} [NeZero n] (g : Equiv.Perm (Fin n))
    (key : ∀ j : Fin n, g (j + 1) = g j + 1) (j : Fin n) :
    ((g j).val : ZMod n) = ((g 0).val : ZMod n) + j.val := by
…
```
lemma Imo2022P3.zmod_eq_of_sub_key A permutation of Fin n anti-commuting with + 1 is a reflection line 364 source
Source documentation
A permutation of Fin n anti-commuting with + 1 is a reflection.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, Equiv.Perm, Fin, Eq, HAdd.hAdd, OfNat.ofNat, ZMod, HSub.hSub
Proof uses: Nat.succ, Exists, Nat.exists_eq_succ_of_ne_zero, NeZero.ne, Fin.induction, of_eq_true, Eq.trans, True, congrArg, Nat.cast_zero, sub_zero, eq_self, Fin.castSucc, Eq.mpr, id, Eq.refl, Mathlib.Tactic.LinearCombination.eq_of_eq, Eq.mp, Imo2022P3.zmod_one, Imo2022P3.zmod_add and 42 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma zmod_eq_of_sub_key {n : ℕ} [NeZero n] (g : Equiv.Perm (Fin n))
    (key : ∀ j : Fin n, g (j + 1) + 1 = g j) (j : Fin n) :
    ((g j).val : ZMod n) = ((g 0).val : ZMod n) - j.val := by
…
```
lemma Imo2022P3.rot_of_succPerm_eq If two placements have the same successor permutation, they differ by a rotation line 384 source
Source documentation
If two placements have the same successor permutation, they differ by a rotation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Finset.Nonempty, Equiv, Fin, Finset.card, Subtype, Membership.mem, Eq, Equiv.Perm, Imo2022P3.succPerm, Exists, HAdd.hAdd
Proof uses: NeZero, NeZero.mk, LT.lt.ne', OfNat.ofNat, Iff.mpr, LT.lt, Finset.card_pos, Equiv.trans, Equiv.symm, rfl, Equiv.injective, of_eq_true, Eq.trans, True, congrFun', congrArg, Equiv.apply_symm_apply, eq_self, Imo2022P3.succPerm_apply, Eq.mp and 20 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma rot_of_succPerm_eq {S : Finset ℕ} (hne : S.Nonempty) {p₁ p₂ : Fin #S ≃ S}
    (h : succPerm p₁ = succPerm p₂) :
    ∃ i, ∀ j, p₂ j = p₁ (j + i) := by
…
```
Mentions: S, h, Imo2022P3.succPerm
lemma Imo2022P3.ref_of_succPerm_eq If the successor permutation of one placement is the inverse of the other's, they differ by a reflection composed with a rotation line 408 source
Source documentation
If the successor permutation of one placement is the inverse of the other's, they differ by a reflection composed with a rotation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Finset.Nonempty, Equiv, Fin, Finset.card, Subtype, Membership.mem, Eq, Equiv.Perm, Imo2022P3.succPerm, Inv.inv, Exists, HAdd.hAdd, Fin.rev
Proof uses: NeZero, NeZero.mk, LT.lt.ne', OfNat.ofNat, Iff.mpr, LT.lt, Finset.card_pos, Equiv.trans, Equiv.symm, rfl, Equiv.injective, Eq.symm, Imo2022P3.succPerm_apply, of_eq_true, Eq.trans, True, congrFun', congrArg, Equiv.apply_symm_apply, eq_self and 47 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma ref_of_succPerm_eq {S : Finset ℕ} (hne : S.Nonempty) {p₁ p₂ : Fin #S ≃ S}
    (h : succPerm p₁ = (succPerm p₂)⁻¹) :
    ∃ i, ∀ j, p₂ j = p₁ (Fin.rev j + i) := by
…
```
Mentions: S, h, Imo2022P3.succPerm
def Imo2022P3.delPerm Deleting M from a permutation: the short-circuited permutation on S.erase M, sending the predecessor of M to the successor of M line 436 source
Source documentation
Deleting M from a permutation: the short-circuited permutation on S.erase M, sending the predecessor of M to the successor of M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Equiv.Perm, Subtype, Membership.mem, Ne, Finset.erase
Proof uses: ite, Eq, Subtype.mk, Function.Injective, Equiv.ofBijective
19 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
noncomputable def delPerm {S : Finset ℕ} (τ : Equiv.Perm S) (M : S) (hrM : τ M ≠ M) :
    Equiv.Perm (S.erase M) :=
…
```
Mentions: S
lemma Imo2022P3.delPerm_val The computation rule for delPerm line 483 source
Source documentation
The computation rule for delPerm.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Equiv.Perm, Subtype, Membership.mem, Ne, Finset.erase, Eq, Imo2022P3.delPerm, ite, Subtype.mk, Finset.mem_of_mem_erase, Subtype.property
Proof uses: id, Eq.mpr, Function.Injective, Equiv.ofBijective, congrArg, Equiv, Equiv.ofBijective_apply, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma delPerm_val {S : Finset ℕ} {τ : Equiv.Perm S} {M : S} {hrM : τ M ≠ M}
    (s : S.erase M) :
    (delPerm τ M hrM s).1
      = if τ ⟨s.1, Finset.mem_of_mem_erase s.2⟩ = M then (τ M).1
        else (τ ⟨s.1, Finset.mem_of_mem_erase s.2⟩).1 := by
…
```
Mentions: S, Imo2022P3.delPerm
lemma Imo2022P3.validPerm_delPerm The deleted permutation stays valid: the one new edge is good by good_of_good_of_good line 493 source
Source documentation
The deleted permutation stays valid: the one new edge is good by good_of_good_of_good.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Equiv.Perm, Subtype, Membership.mem, Ne, Imo2022P3.ValidPerm, Nat.Prime, LT.lt, Inv.inv, Imo2022P3.good, Finset.erase, Imo2022P3.delPerm
Proof uses: Eq.mpr, ite, Eq, Subtype.mk, Finset.mem_of_mem_erase, Subtype.property, id, congrArg, Imo2022P3.delPerm_val, dite, ite_eq_left, Eq.symm, Equiv, Equiv.symm, Equiv.apply_symm_apply, Equiv.injective, Iff.mp, Subtype.mk_eq_mk, Imo2022P3.good_of_good_of_good, Subtype.ext and 2 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma validPerm_delPerm {k : ℕ} {S : Finset ℕ} {τ : Equiv.Perm S} {M : S}
    {hrM : τ M ≠ M} (hv : ValidPerm k τ)
    (hMprime : Nat.Prime M.1)
    (hq : (τ⁻¹ M).1 < M.1) (hr : (τ M).1 < M.1) (hqr : τ⁻¹ M ≠ τ M)
    (hgq : good k M.1 (τ⁻¹ M).1) (hgr : good k M.1 (τ M).1) :
    ValidPerm k (delPerm τ M hrM) := by
…
```
Mentions: S, Imo2022P3.ValidPerm, Imo2022P3.good, Imo2022P3.delPerm
lemma Imo2022P3.connectedP_delPerm The deleted permutation stays connected (the "skip M" argument) line 516 source
Source documentation
The deleted permutation stays connected (the "skip M" argument).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Equiv.Perm, Subtype, Membership.mem, Ne, Imo2022P3.ConnectedP, Finset.erase, Imo2022P3.delPerm
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, LE.le, OfNat.ofNat, LT.lt, Nat.iterate, Subtype.mk, Finset.mem_of_mem_erase, Subtype.property, Exists, Nat.recAux, Exists.intro, HAdd.hAdd, Eq.symm, Nat.succ, Function.iterate_succ_apply', Iff.mpr and 22 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
lemma connectedP_delPerm {S : Finset ℕ} {τ : Equiv.Perm S} {M : S}
    {hrM : τ M ≠ M} (hc : ConnectedP τ) :
    ConnectedP (delPerm τ M hrM) := by
…
```
Mentions: S, Imo2022P3.ConnectedP, Imo2022P3.delPerm
lemma Imo2022P3.not_connectedP_of_orbit_subset If an orbit stays inside a set missing an element, the permutation is not connected line 612 source
Source documentation
If an orbit stays inside a set missing an element, the permutation is not connected.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Equiv.Perm, Subtype, Membership.mem, Imo2022P3.ConnectedP, Nat.iterate, Not, False
Proof uses: Eq, Exists, Eq.rec
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma not_connectedP_of_orbit_subset {S : Finset ℕ} {σ : Equiv.Perm S} (hc : ConnectedP σ)
    {x : S} {T : Finset S} (hT : ∀ m, σ^[m] x ∈ T) {y : S} (hy : y ∉ T) : False := by
…
```
Mentions: S, Imo2022P3.ConnectedP
lemma Imo2022P3.validPerm_inv Validity passes to the inverse permutation line 618 source
Source documentation
Validity passes to the inverse permutation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Equiv.Perm, Subtype, Membership.mem, Imo2022P3.ValidPerm, Inv.inv
Proof uses: Imo2022P3.good, Eq, Equiv.apply_symm_apply, Imo2022P3.good_comm, Eq.mp, congrArg
10 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma validPerm_inv {k : ℕ} {S : Finset ℕ} {σ : Equiv.Perm S} (hv : ValidPerm k σ) :
    ValidPerm k σ⁻¹ := by
…
```
Mentions: S, Imo2022P3.ValidPerm
lemma Imo2022P3.connectedP_inv Connectivity passes to the inverse permutation line 627 source
Source documentation
Connectivity passes to the inverse permutation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Equiv.Perm, Subtype, Membership.mem, Imo2022P3.ConnectedP, Inv.inv
Proof uses: Iff, Eq, Nat.iterate, Nat.recAux, Iff.intro, OfNat.ofNat, Eq.symm, Eq.mpr, HAdd.hAdd, id, congrArg, Nat.succ, Function.iterate_succ_apply', Equiv.Perm.inv_eq_iff_eq, propext, Function.iterate_succ_apply, Iff.rfl, Exists, Exists.intro, Iff.mpr
13 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma connectedP_inv {S : Finset ℕ} {σ : Equiv.Perm S} (hc : ConnectedP σ) :
    ConnectedP σ⁻¹ := by
…
```
Mentions: S, Imo2022P3.ConnectedP
lemma Imo2022P3.ne_of_connectedP A connected permutation on at least two elements has no fixed point line 645 source
Source documentation
A connected permutation on at least two elements has no fixed point.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Equiv.Perm, Subtype, Membership.mem, Imo2022P3.ConnectedP, LE.le, OfNat.ofNat, Finset.card, Ne
Proof uses: Eq, Exists, False, Finset.Nonempty, Finset.erase, Iff.mp, LT.lt, Finset.card_pos, Eq.mpr, HSub.hSub, id, congrArg, Finset.card_erase_of_mem, Subtype.property, Exists.intro, Subtype.mk, Finset.mem_of_mem_erase, And.left, And, Finset.mem_erase and 5 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma ne_of_connectedP {S : Finset ℕ} {σ : Equiv.Perm S} (hc : ConnectedP σ)
    (h : 2 ≤ #S) (s : S) : σ s ≠ s := by
…
```
Mentions: S, Imo2022P3.ConnectedP, h
lemma Imo2022P3.perm_unique The core uniqueness statement: two valid connected permutations of S are equal or inverse to each other line 663 source
Source documentation
The core uniqueness statement: two valid connected permutations of S are equal or inverse to each other. Proved by strong induction on #S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Eq, Finset.card, LE.le, OfNat.ofNat, Membership.mem, And, Odd, Nat.Prime, Equiv.Perm, Subtype, Imo2022P3.ValidPerm, Imo2022P3.ConnectedP, Or, Inv.inv
Proof uses: Nat.strong_induction_on, LT.lt, dite, Singleton.singleton, Exists, Iff.mp, Finset.card_eq_one, Or.inl, Equiv.Perm.ext, Subtype.ext, Subtype.mk, Finset.mem_singleton_self, Finset.mem_singleton, Subtype.property, Eq.mpr, id, congrArg, Eq.refl, Eq.symm, Not and 72 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 431 steps (first 200 of 431)
Open to load the checked before-and-after goal states.
```
lemma perm_unique {k : ℕ} (n : ℕ) :
    ∀ (S : Finset ℕ) (_ : #S = n) (_ : 1 ≤ #S) (_ : ∀ p ∈ S, Odd p ∧ Nat.Prime p)
    (σ₁ σ₂ : Equiv.Perm S), ValidPerm k σ₁ → ValidPerm k σ₂ →
    ConnectedP σ₁ → ConnectedP σ₂ → σ₁ = σ₂ ∨ σ₁ = σ₂⁻¹ := by
…
```
Mentions: S, Imo2022P3.ValidPerm, Imo2022P3.ConnectedP
problem Imo2022P3.imo2023_p3 line 1074 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Finset.Nonempty, Membership.mem, And, Odd, Nat.Prime, Equiv, Fin, Finset.card, Subtype, Imo2022P3.Condition, Or, Exists, Eq, HAdd.hAdd, Fin.rev
Proof uses: NeZero, NeZero.mk, LT.lt.ne', Iff.mpr, Finset.card_pos, Imo2022P3.good, HMul.hMul, HPow.hPow, Exists.intro, Equiv.Perm, Imo2022P3.succPerm, Inv.inv, Imo2022P3.perm_unique, rfl, Imo2022P3.validPerm_succPerm, Imo2022P3.connectedP_succPerm, Or.inl, Imo2022P3.rot_of_succPerm_eq, Or.inr, Imo2022P3.ref_of_succPerm_eq
36 instances, coercions and auxiliary constants left out.

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