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

77 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2025, Problem 6

Let m and n be positive integers with m ≥ n. There are m cupcakes of different flavors arranged around a circle and n people who like cupcakes. Each person assigns a nonnegative real number score to each cupcake, depending on how much they like the cupcake. Suppose that for each person P, it is possible to partition the circle of m cupcakes into n groups of consecutive cupcakes so that the sum of P's scores of the cupcakes in each group is at least 1. Prove that it is possible to distribute the m cupcakes to the n people so that each person P receives cupcakes of total score at least 1 with respect to P.

Imports (12)

Imported by 1 file

Compfiles.lean

def Usa2025P6.arcSet An arc of length l starting at c on the circle ZMod m line 49 source
Source documentation
An arc of length l starting at c on the circle ZMod m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ZMod, Finset
Proof uses: Finset.image, HAdd.hAdd, Finset.range
12 instances, coercions and auxiliary constants left out.
```
def arcSet {m : ℕ} (c : ZMod m) (l : ℕ) : Finset (ZMod m) :=
…
```
structure Usa2025P6.CirclePartition A partition of the circle ZMod m into k consecutive nonempty arcs, described by a basepoint and the list of arc lengths line 55 source
Source documentation
A partition of the circle ZMod m into k consecutive nonempty arcs, described by a basepoint and the list of arc lengths.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
```
structure CirclePartition (m k : ℕ) where
…
```
def Usa2025P6.CirclePartition.off The offset of arc i: total length of the preceding arcs line 67 source
Source documentation
The offset of arc i: total length of the preceding arcs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, Fin
Proof uses: Finset.sum, Finset.filter, LT.lt, Finset.univ, Usa2025P6.CirclePartition.len
4 instances, coercions and auxiliary constants left out.
```
def off (i : Fin k) : ℕ := ∑ j ∈ Finset.univ.filter (· < i), P.len j
```
def Usa2025P6.CirclePartition.start The starting point of arc i line 70 source
Source documentation
The starting point of arc i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, Fin, ZMod
Proof uses: HAdd.hAdd, Usa2025P6.CirclePartition.base, Usa2025P6.CirclePartition.off
11 instances, coercions and auxiliary constants left out.
```
def start (i : Fin k) : ZMod m := P.base + (P.off i : ZMod m)
```
def Usa2025P6.CirclePartition.arcOf The i-th arc as a finset line 73 source
Source documentation
The i-th arc as a finset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, Fin, Finset, ZMod
Proof uses: Usa2025P6.arcSet, Usa2025P6.CirclePartition.start, Usa2025P6.CirclePartition.len
```
def arcOf (i : Fin k) : Finset (ZMod m) := arcSet (P.start i) (P.len i)
…
```
Mentions: Usa2025P6.arcSet
lemma Usa2025P6.CirclePartition.mem_arcSet line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ZMod, Iff, Membership.mem, Finset, Usa2025P6.arcSet, Exists, And, LT.lt, Eq, HAdd.hAdd
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.image, Finset.range, funext, iff_self
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.natCast_injective_of_lt line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LT.lt, Eq, ZMod
Proof uses: Nat.ModEq.eq_of_lt_of_lt, Eq.mp, Nat.ModEq, congrArg, propext, ZMod.natCast_eq_natCast_iff
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.arcSet_card line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, LE.le, Eq, Finset.card, Usa2025P6.arcSet
Proof uses: Eq.mpr, Finset.image, HAdd.hAdd, Finset.range, id, congrArg, Finset, Usa2025P6.arcSet.eq_1, Finset.card_image_of_injOn, Membership.mem, Set, Usa2025P6.CirclePartition.natCast_injective_of_lt, Eq.mp, LT.lt, propext, Finset.mem_range, Finset.mem_coe, Finset.card_range, Eq.refl
30 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.sum_arcSet line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, LE.le, Real, Eq, Finset.sum, Usa2025P6.arcSet, Finset.range, HAdd.hAdd
Proof uses: Eq.mpr, Finset.image, id, congrArg, Finset, Usa2025P6.arcSet.eq_1, Finset.sum_image, Membership.mem, Set, Usa2025P6.CirclePartition.natCast_injective_of_lt, Eq.mp, LT.lt, propext, Finset.mem_range, Finset.mem_coe, Eq.refl
43 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.arcSet_univ line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, Eq, Finset, Usa2025P6.arcSet, Finset.univ
Proof uses: Finset.eq_univ_of_card, Eq.mpr, Finset.card, Fintype.card, id, congrArg, Usa2025P6.CirclePartition.arcSet_card, le_rfl, ZMod.card, Eq.refl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.k_pos line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat
Proof uses: Decidable.byContradiction, Not, Eq, Nat.eq_zero_of_le_zero, Eq.mp, LE.le, Finset, Fin, Finset.univ, EmptyCollection.emptyCollection, Eq.mpr, id, congrArg, Finset.univ_eq_empty, Finset.sum, Usa2025P6.CirclePartition.len, Usa2025P6.CirclePartition.len_sum, Finset.sum_empty
20 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def Usa2025P6.CirclePartition.offExt Periodic extension of the offsets: the total length of the first a arcs (going around the circle repeatedly) line 127 source
Source documentation
Periodic extension of the offsets: the total length of the first a arcs (going around the circle repeatedly).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat
Proof uses: Finset.sum, Finset.range, Usa2025P6.CirclePartition.len, Fin.mk, HMod.hMod, Nat.mod_lt
7 instances, coercions and auxiliary constants left out.
```
def offExt (hk : 0 < k) (a : ℕ) : ℕ :=
…
```
lemma Usa2025P6.CirclePartition.len_congr Helper: evaluating the periodic length at an explicitly given index line 132 source
Source documentation
Helper: evaluating the periodic length at an explicitly given index.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Fin, Eq, HMod.hMod, Usa2025P6.CirclePartition.len, Fin.mk, Nat.mod_lt
Proof uses: congr_arg, Fin.ext
10 instances, coercions and auxiliary constants left out.
```
lemma len_congr (hk : 0 < k) {a : ℕ} {j : Fin k} (h : a % k = j.val) :
    P.len ⟨a % k, Nat.mod_lt a hk⟩ = P.len j :=
…
```
Mentions: h
lemma Usa2025P6.CirclePartition.offExt_zero line 136 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Eq, Usa2025P6.CirclePartition.offExt
Proof uses: of_eq_true, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.offExt_succ line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Eq, Usa2025P6.CirclePartition.offExt, HAdd.hAdd, Usa2025P6.CirclePartition.len, Fin.mk, HMod.hMod, Nat.mod_lt
Proof uses: of_eq_true, Finset.sum, Finset.range, Eq.trans, True, congrFun', congrArg, Finset.sum_range_succ, eq_self
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.off_eq_offExt line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Fin, Eq, Usa2025P6.CirclePartition.off, Usa2025P6.CirclePartition.offExt
Proof uses: Eq.mpr, Finset.sum, Finset.filter, Finset.univ, Usa2025P6.CirclePartition.len, id, congrArg, Usa2025P6.CirclePartition.off.eq_1, Finset.range, Fin.mk, HMod.hMod, Nat.mod_lt, Usa2025P6.CirclePartition.offExt.eq_1, Finset.sum_bij, Membership.mem, Finset, propext, Finset.mem_range, And.right, Eq.mp and 13 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.offExt_k line 161 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Eq, Usa2025P6.CirclePartition.offExt
Proof uses: Finset.sum, Finset.range, Usa2025P6.CirclePartition.len, Fin.mk, HMod.hMod, Nat.mod_lt, Fin, Finset.univ, Eq.mpr, id, congrArg, Eq.symm, Fin.sum_univ_eq_sum_range, Finset.sum_congr, rfl, Finset, Membership.mem, Usa2025P6.CirclePartition.len_congr, Nat.mod_eq_of_lt, Fin.isLt and 3 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.offExt_add_period line 169 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Eq, Usa2025P6.CirclePartition.offExt, HAdd.hAdd
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, Usa2025P6.CirclePartition.offExt.congr_simp, Eq.refl, zero_add, Usa2025P6.CirclePartition.offExt_k, congrFun', Usa2025P6.CirclePartition.offExt_zero, eq_self, Usa2025P6.CirclePartition.len, Fin.mk, HMod.hMod, Nat.mod_lt, Usa2025P6.CirclePartition.len_congr, Nat.add_mod_right, Eq.mpr and 14 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.offExt_mono line 179 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, LE.le, Usa2025P6.CirclePartition.offExt
Proof uses: Eq, HAdd.hAdd, Exists, Nat.exists_eq_add_of_le, Nat.recAux, of_eq_true, Eq.trans, True, congrArg, Usa2025P6.CirclePartition.offExt.congr_simp, Eq.refl, add_zero, Eq.mpr, Nat.succ, id, Nat.add_succ, Usa2025P6.CirclePartition.len, Fin.mk, HMod.hMod, Nat.mod_lt and 3 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.offExt_lt_succ line 188 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Usa2025P6.CirclePartition.offExt, HAdd.hAdd
Proof uses: Eq.mpr, Usa2025P6.CirclePartition.len, Fin.mk, HMod.hMod, Nat.mod_lt, id, Eq, congrArg, Usa2025P6.CirclePartition.offExt_succ, LE.le, Usa2025P6.CirclePartition.len_pos
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Usa2025P6.CirclePartition.perW The periodic weight function on ℕ associated to a score function line 194 source
Source documentation
The periodic weight function on ℕ associated to a score function.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, ZMod, Real
Proof uses: HAdd.hAdd, Usa2025P6.CirclePartition.base
11 instances, coercions and auxiliary constants left out.
```
def perW (w : ZMod m → ℝ) (t : ℕ) : ℝ := w (P.base + (t : ZMod m))
```
lemma Usa2025P6.CirclePartition.perW_periodic line 196 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, ZMod, Real, Eq, Usa2025P6.CirclePartition.perW, HAdd.hAdd
Proof uses: Eq.mpr, Usa2025P6.CirclePartition.base, id, congrArg, Usa2025P6.CirclePartition.perW.eq_1, Nat.cast_add, OfNat.ofNat, ZMod.natCast_self, add_zero, Eq.refl
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.offExt_succ_fin line 199 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Fin, Eq, Usa2025P6.CirclePartition.offExt, HAdd.hAdd, Usa2025P6.CirclePartition.off, Usa2025P6.CirclePartition.len
Proof uses: Eq.mpr, Fin.mk, HMod.hMod, Nat.mod_lt, id, congrArg, Usa2025P6.CirclePartition.offExt_succ, Usa2025P6.CirclePartition.off_eq_offExt, HAdd, Eq.rec, Eq.refl, Usa2025P6.CirclePartition.len_congr, Nat.mod_eq_of_lt, Fin.isLt
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.off_add_len_le line 205 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Fin, LE.le, HAdd.hAdd, Usa2025P6.CirclePartition.off, Usa2025P6.CirclePartition.len
Proof uses: Eq.mpr, Usa2025P6.CirclePartition.offExt, id, Eq, congrArg, Eq.symm, Usa2025P6.CirclePartition.offExt_succ_fin, Nat.succ, Usa2025P6.CirclePartition.offExt_mono, Fin.isLt, Eq.mp, Usa2025P6.CirclePartition.offExt_k
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.len_le line 210 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Fin, LE.le, Usa2025P6.CirclePartition.len
Proof uses: le_trans, HAdd.hAdd, Usa2025P6.CirclePartition.off, Nat.le_add_left, Usa2025P6.CirclePartition.off_add_len_le
8 instances, coercions and auxiliary constants left out.
lemma Usa2025P6.CirclePartition.offExt_strictMono line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, StrictMono, Usa2025P6.CirclePartition.offExt
Proof uses: Eq, HAdd.hAdd, Exists, Nat.exists_eq_add_of_lt, Usa2025P6.CirclePartition.offExt_lt_succ, Nat.recAux, Eq.mpr, id, Eq.trans, congrArg, Usa2025P6.CirclePartition.offExt.congr_simp, Eq.refl, congrFun', add_zero, Eq.mp, congr, Eq.symm
16 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.off_le_off line 226 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Fin, LE.le, Usa2025P6.CirclePartition.off
Proof uses: Eq.mpr, Usa2025P6.CirclePartition.offExt, id, Eq, congrArg, Usa2025P6.CirclePartition.off_eq_offExt, Usa2025P6.CirclePartition.offExt_mono, Eq.mp, propext, Fin.le_def
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.off_add_len_le_off line 230 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Fin, LE.le, HAdd.hAdd, Usa2025P6.CirclePartition.off, Usa2025P6.CirclePartition.len
Proof uses: Eq.mpr, Usa2025P6.CirclePartition.offExt, id, Eq, congrArg, Eq.symm, Usa2025P6.CirclePartition.offExt_succ_fin, Usa2025P6.CirclePartition.offExt_mono, Eq.mp, propext, Fin.le_def
14 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.exists_Ico_of_mono Every position in [0, m) lies in a unique arc interval; existence part line 236 source
Source documentation
Every position in [0, m) lies in a unique arc interval; existence part.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Exists, And, HAdd.hAdd
Proof uses: Nat.recAux, dite, Exists.intro, And.intro, Nat.lt_succ_of_lt, Not, Nat.lt_succ_self
16 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma exists_Ico_of_mono {off : ℕ → ℕ} {K p : ℕ} (h0 : off 0 ≤ p) (hp : p < off K) :
    ∃ j < K, off j ≤ p ∧ p < off (j + 1) := by
…
```
Mentions: Usa2025P6.CirclePartition.off
def Usa2025P6.CirclePartition.pos The position of a point relative to the basepoint line 247 source
Source documentation
The position of a point relative to the basepoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, ZMod
Proof uses: ZMod.val, HSub.hSub, Usa2025P6.CirclePartition.base
7 instances, coercions and auxiliary constants left out.
```
def pos (x : ZMod m) : ℕ := (x - P.base).val
```
lemma Usa2025P6.CirclePartition.base_add_pos line 249 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, NeZero, ZMod, Eq, HAdd.hAdd, Usa2025P6.CirclePartition.base, Usa2025P6.CirclePartition.pos
Proof uses: Eq.mpr, ZMod.val, HSub.hSub, id, congrArg, Usa2025P6.CirclePartition.pos.eq_1, ZMod.cast, ZMod.natCast_val, ZMod.cast_id
31 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.pos_start_add line 254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, NeZero, Fin, Usa2025P6.CirclePartition.len, Eq, Usa2025P6.CirclePartition.pos, HAdd.hAdd, ZMod, Usa2025P6.CirclePartition.start, Usa2025P6.CirclePartition.off
Proof uses: HSub.hSub, Usa2025P6.CirclePartition.base, Eq.mpr, id, congrArg, Usa2025P6.CirclePartition.start.eq_1, Nat.cast_add, ZMod.val, Usa2025P6.CirclePartition.pos.eq_1, HMod.hMod, ZMod.val_natCast, Nat.mod_eq_of_lt, LE.le, Usa2025P6.CirclePartition.off_add_len_le, Eq.refl
44 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.arcOf_cover line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, NeZero, ZMod, Exists, Fin, Membership.mem, Finset, Usa2025P6.CirclePartition.arcOf
Proof uses: And, LE.le, Usa2025P6.CirclePartition.offExt, Usa2025P6.CirclePartition.pos, HAdd.hAdd, Usa2025P6.CirclePartition.exists_Ico_of_mono, Eq.mpr, id, Eq, congrArg, Usa2025P6.CirclePartition.offExt_zero, Nat.zero_le, Usa2025P6.CirclePartition.offExt_k, ZMod.val_lt, HSub.hSub, Usa2025P6.CirclePartition.base, Usa2025P6.CirclePartition.off, Fin.mk, Usa2025P6.CirclePartition.off_eq_offExt, Usa2025P6.CirclePartition.len and 15 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.arcOf_disjoint line 282 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, NeZero, Fin, Ne, Disjoint, Finset, ZMod, Usa2025P6.CirclePartition.arcOf
Proof uses: Eq.mpr, Membership.mem, Not, id, Eq, congrArg, propext, Finset.disjoint_left, And, Usa2025P6.CirclePartition.len, HAdd.hAdd, Usa2025P6.CirclePartition.start, Exists, False, Eq.mp, Usa2025P6.arcSet, Usa2025P6.CirclePartition.mem_arcSet, Usa2025P6.CirclePartition.arcOf.eq_1, Usa2025P6.CirclePartition.pos, Usa2025P6.CirclePartition.off and 10 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.perW_sum_shift line 304 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, ZMod, Real, Eq, Finset.sum, Finset.Ico, HAdd.hAdd, Usa2025P6.CirclePartition.perW
Proof uses: Finset.sum_bij, Membership.mem, Finset, HSub.hSub, Eq.mpr, And, LE.le, LT.lt, id, Eq.mp, Exists.intro, Exists, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, Usa2025P6.CirclePartition.perW_periodic
22 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.perW_sum_period line 321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, ZMod, Real, Eq, Finset.sum, Finset.Ico, HAdd.hAdd, HMul.hMul, Usa2025P6.CirclePartition.perW
Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, Finset.sum_congr, congr, Finset, MulZeroClass.zero_mul, add_zero, Membership.mem, Eq.refl, eq_self, Eq.mpr, id, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast and 21 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.offExt_add_mul_period line 330 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Eq, Usa2025P6.CirclePartition.offExt, HAdd.hAdd, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, Usa2025P6.CirclePartition.offExt.congr_simp, Eq.refl, MulZeroClass.zero_mul, add_zero, eq_self, Eq.mpr, id, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm and 17 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.offExt_eq_off_add_div line 338 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Fin, Eq, HMod.hMod, Usa2025P6.CirclePartition.offExt, HAdd.hAdd, Usa2025P6.CirclePartition.off, HMul.hMul, HDiv.hDiv
Proof uses: Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, Nat.mod_add_div, Nat.mul_comm, Usa2025P6.CirclePartition.offExt_add_mul_period, Usa2025P6.CirclePartition.off_eq_offExt, Iff.mpr, Nat.add_right_cancel_iff
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.sum_arcOf line 344 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, NeZero, Fin, ZMod, Real, Eq, Finset.sum, Usa2025P6.CirclePartition.arcOf, Finset.Ico, Usa2025P6.CirclePartition.off, HAdd.hAdd, Usa2025P6.CirclePartition.len, Usa2025P6.CirclePartition.perW
Proof uses: Eq.mpr, Usa2025P6.arcSet, Usa2025P6.CirclePartition.start, id, congrArg, Finset, Usa2025P6.CirclePartition.arcOf.eq_1, Finset.range, Usa2025P6.CirclePartition.sum_arcSet, Usa2025P6.CirclePartition.len_le, HSub.hSub, Finset.sum_Ico_eq_sum_range, Nat.add_sub_cancel_left, Finset.sum_congr, rfl, Membership.mem, Usa2025P6.CirclePartition.base, Usa2025P6.CirclePartition.perW.eq_1, Usa2025P6.CirclePartition.start.eq_1, Nat.cast_add and 3 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.sum_arcOf_ext line 352 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, NeZero, Fin, Eq, HMod.hMod, ZMod, Real, Finset.sum, Finset.Ico, Usa2025P6.CirclePartition.offExt, HAdd.hAdd, Usa2025P6.CirclePartition.len, Usa2025P6.CirclePartition.perW, Usa2025P6.CirclePartition.arcOf
Proof uses: Eq.mpr, Usa2025P6.CirclePartition.off, HMul.hMul, HDiv.hDiv, id, congrArg, Usa2025P6.CirclePartition.offExt_eq_off_add_div, Usa2025P6.CirclePartition.perW_sum_period, Usa2025P6.CirclePartition.sum_arcOf, Eq.refl
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.perW_sum_nonneg line 358 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, ZMod, Real, LE.le, OfNat.ofNat, Finset.sum, Finset.Ico, Usa2025P6.CirclePartition.perW
Proof uses: Finset.sum_nonneg, Membership.mem, Finset, HAdd.hAdd, Usa2025P6.CirclePartition.base
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.perW_sum_mono line 364 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, ZMod, Real, LE.le, OfNat.ofNat, Finset.sum, Finset.Ico, Usa2025P6.CirclePartition.perW
Proof uses: Finset.sum_le_sum_of_subset_of_nonneg, Finset.Ico_subset_Ico, Membership.mem, Finset, Not, HAdd.hAdd, Usa2025P6.CirclePartition.base
30 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.exists_gap line 382 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, ZMod, Ne, Finset.univ, Exists, And, LE.le, OfNat.ofNat, Not, Membership.mem, HAdd.hAdd
Proof uses: Finset.exists_of_ssubset, Iff.mpr, LT.lt, Finset.ssubset_univ_iff, dite, Eq, Exists.intro, And.intro, Nat.pos_of_ne_zero, NeZero.ne, le_rfl, Eq.mpr, id, congrArg, Eq.symm, ZMod.natCast_self, add_zero, ZMod.val, HSub.hSub, Eq.mp and 10 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
def Usa2025P6.CirclePartition.gapSize The distance to the next point outside D (a positive number of steps) line 400 source
Source documentation
The distance to the next point outside D (a positive number of steps).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, ZMod, Ne, Finset.univ
Proof uses: Nat.find, And, LE.le, OfNat.ofNat, Not, Membership.mem, HAdd.hAdd, Usa2025P6.CirclePartition.exists_gap
26 instances, coercions and auxiliary constants left out.
```
noncomputable def gapSize (D : Finset (ZMod m)) (hD : D ≠ Finset.univ) (x : ZMod m) : ℕ :=
…
```
lemma Usa2025P6.CirclePartition.gapSize_spec line 403 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, ZMod, Ne, Finset.univ, And, LE.le, OfNat.ofNat, Usa2025P6.CirclePartition.gapSize, Not, Membership.mem, HAdd.hAdd
Proof uses: Nat.find_spec, Usa2025P6.CirclePartition.exists_gap
41 instances, coercions and auxiliary constants left out.
lemma Usa2025P6.CirclePartition.gapSize_mem line 407 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, ZMod, Ne, Finset.univ, LE.le, OfNat.ofNat, LT.lt, Usa2025P6.CirclePartition.gapSize, Membership.mem, HAdd.hAdd
Proof uses: Not, And, Nat.find_min, Usa2025P6.CirclePartition.exists_gap, Usa2025P6.CirclePartition.gapSize_spec, Decidable.byContradiction, And.intro
44 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Usa2025P6.CirclePartition.nextD The successor of x in the circle with D deleted line 415 source
Source documentation
The successor of x in the circle with D deleted.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, ZMod, Ne, Finset.univ
Proof uses: HAdd.hAdd, Usa2025P6.CirclePartition.gapSize
17 instances, coercions and auxiliary constants left out.
```
noncomputable def nextD (D : Finset (ZMod m)) (hD : D ≠ Finset.univ) (x : ZMod m) : ZMod m :=
…
```
lemma Usa2025P6.CirclePartition.nextD_notMem line 418 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, ZMod, Ne, Finset.univ, Not, Membership.mem, Usa2025P6.CirclePartition.nextD
Proof uses: And.right, LE.le, Usa2025P6.CirclePartition.gapSize, HAdd.hAdd, OfNat.ofNat, And, Usa2025P6.CirclePartition.gapSize_spec
23 instances, coercions and auxiliary constants left out.
lemma Usa2025P6.CirclePartition.nextD_ne_univ line 422 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, ZMod, Ne, Finset.univ, Eq, Usa2025P6.CirclePartition.nextD, HAdd.hAdd, Usa2025P6.CirclePartition.gapSize
Proof uses: rfl
17 instances, coercions and auxiliary constants left out.
structure Usa2025P6.CirclePartition.CircleEmb A circular embedding: an enumeration of the complement of D that respects the successor structure of the circle line 429 source
Source documentation
A circular embedding: an enumeration of the complement of D that respects the successor structure of the circle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, ZMod, Ne, Finset.univ
3 instances, coercions and auxiliary constants left out.
```
structure CircleEmb {m : ℕ} [NeZero m] {m' : ℕ} [NeZero m']
    (D : Finset (ZMod m)) (hD : D ≠ Finset.univ) (φ : ZMod m' → ZMod m) : Prop where
…
```
lemma Usa2025P6.CirclePartition.CircleEmb.congr_D line 436 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, ZMod, Ne, Finset.univ, Eq, Usa2025P6.CirclePartition.CircleEmb
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Usa2025P6.CirclePartition.skipMap The enumeration of the complement of an arc, starting right after the arc line 444 source
Source documentation
The enumeration of the complement of an arc, starting right after the arc.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, ZMod, HSub.hSub
Proof uses: HAdd.hAdd, ZMod.val
15 instances, coercions and auxiliary constants left out.
```
def skipMap {m : ℕ} (a₀ : ZMod m) (l : ℕ) (i : ZMod (m - l)) : ZMod m :=
…
```
lemma Usa2025P6.CirclePartition.skipMap_injective line 451 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, HSub.hSub, LE.le, Function.Injective, Usa2025P6.CirclePartition.skipMap
Proof uses: Eq, ZMod.val, Usa2025P6.CirclePartition.natCast_injective_of_lt, LT.lt, ZMod.val_lt, Eq.mp, HAdd.hAdd, congrArg, propext, add_left_cancel_iff, Usa2025P6.CirclePartition.skipMap.eq_1, ZMod.val_injective
28 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.skipMap_notMem line 459 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, HSub.hSub, LE.le, Not, Membership.mem, Finset, Usa2025P6.arcSet, Usa2025P6.CirclePartition.skipMap
Proof uses: Eq.mpr, Exists, And, LT.lt, Eq, HAdd.hAdd, id, congrArg, propext, Usa2025P6.CirclePartition.mem_arcSet, False, ZMod.val, Nat.cast_add, Eq.mp, add_left_cancel_iff, add_assoc, Usa2025P6.CirclePartition.skipMap.eq_1, Usa2025P6.CirclePartition.natCast_injective_of_lt, ZMod.val_lt
40 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.skipMap_cover line 471 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, HSub.hSub, LE.le, Not, Membership.mem, Finset, Usa2025P6.arcSet, Exists, Eq, Usa2025P6.CirclePartition.skipMap
Proof uses: HAdd.hAdd, ZMod.val, Eq.mpr, ZMod.cast, id, congrArg, ZMod.natCast_val, ZMod.cast_id, add_comm, sub_add_cancel, Eq.refl, dite, rfl, LT.lt, ZMod.val_lt, Exists.intro, HMod.hMod, ZMod.val_natCast, Nat.mod_eq_of_lt, Eq.mp and 10 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.skipMap_add line 494 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, ZMod, HSub.hSub, Eq, HAdd.hAdd, Usa2025P6.CirclePartition.skipMap, ZMod.val
Proof uses: Eq.mpr, id, congrArg, Usa2025P6.CirclePartition.skipMap.eq_1, Nat.cast_add
32 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.skipMap_eq line 500 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, ZMod, HSub.hSub, Eq, Usa2025P6.CirclePartition.skipMap, HAdd.hAdd, ZMod.val
Proof uses: Eq.mpr, id, congrArg, Usa2025P6.CirclePartition.skipMap.eq_1, Nat.cast_add, add_assoc, Eq.refl
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.mem_arcSet_iff line 505 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ZMod, LE.le, Iff, Membership.mem, Finset, Usa2025P6.arcSet, HAdd.hAdd, LT.lt, HMod.hMod
Proof uses: Eq.mpr, Exists, And, Eq, id, congrArg, propext, Usa2025P6.CirclePartition.mem_arcSet, Iff.intro, Eq.mp, Nat.ModEq, ZMod.natCast_eq_natCast_iff, add_left_cancel_iff, Eq.symm, Nat.mod_eq_of_lt, Exists.intro, And.intro, Nat.mod_modEq
44 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.skipMap_next line 520 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, HSub.hSub, LE.le, Ne, Finset, Usa2025P6.arcSet, Finset.univ, Eq, Usa2025P6.CirclePartition.skipMap, HAdd.hAdd, OfNat.ofNat, Usa2025P6.CirclePartition.nextD
Proof uses: LT.lt, Decidable.byContradiction, Not, Eq.mp, congrArg, Nat.le_antisymm, Usa2025P6.CirclePartition.arcSet_univ, ZMod.val, ZMod.val_lt, of_eq_true, Eq.trans, True, Nat.cast_one, eq_self, dite, Membership.mem, Eq.mpr, id, Usa2025P6.CirclePartition.skipMap_add, HMod.hMod and 28 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 77 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.circleEmb_skipMap The circular embedding given by skipping a single arc line 583 source
Source documentation
The circular embedding given by skipping a single arc.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, HSub.hSub, LE.le, Ne, Finset, Usa2025P6.arcSet, Finset.univ, Usa2025P6.CirclePartition.CircleEmb, Usa2025P6.CirclePartition.skipMap
Proof uses: Usa2025P6.CirclePartition.CircleEmb.mk, Usa2025P6.CirclePartition.skipMap_injective, Usa2025P6.CirclePartition.skipMap_next, Usa2025P6.CirclePartition.skipMap_notMem, Not, Membership.mem, Usa2025P6.CirclePartition.skipMap_cover
14 instances, coercions and auxiliary constants left out.
```
lemma circleEmb_skipMap [NeZero (m - l)] (hl : l ≤ m) (hlD : arcSet a₀ l ≠ Finset.univ) :
    CircleEmb (arcSet a₀ l) hlD (skipMap a₀ l) where
…
```
Mentions: Usa2025P6.arcSet, Usa2025P6.CirclePartition.CircleEmb, Usa2025P6.CirclePartition.skipMap
lemma Usa2025P6.CirclePartition.mem_image_skipMap line 591 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, Finset, HSub.hSub, LE.le, Iff, Membership.mem, Finset.image, Usa2025P6.CirclePartition.skipMap
Proof uses: Eq.mpr, Exists, And, Eq, id, congrArg, propext, Finset.mem_image, Iff.intro, Eq.symm, Usa2025P6.CirclePartition.skipMap_injective, Exists.intro, And.intro, rfl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.skipMap_nextD The intertwining lemma: skipping an arc commutes with the deleted successor line 603 source
Source documentation
The intertwining lemma: skipping an arc commutes with the deleted successor.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, HSub.hSub, LE.le, Finset, Ne, Finset.univ, Union.union, Usa2025P6.arcSet, Finset.image, Usa2025P6.CirclePartition.skipMap, Eq, Usa2025P6.CirclePartition.nextD
Proof uses: LT.lt, ZMod.val, ZMod.val_lt, And, OfNat.ofNat, Usa2025P6.CirclePartition.gapSize, Not, Membership.mem, HAdd.hAdd, Usa2025P6.CirclePartition.gapSize_spec, rfl, Eq.mpr, Or, id, congrArg, propext, Finset.mem_union, And.intro, Usa2025P6.CirclePartition.skipMap_notMem, Usa2025P6.CirclePartition.mem_image_skipMap and 38 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 111 steps
Open to load the checked before-and-after goal states.
```
lemma skipMap_nextD [NeZero (m - l)] (hl : l ≤ m)
    (D₂ : Finset (ZMod (m - l))) (hD₂ : D₂ ≠ Finset.univ)
    (hD : arcSet a₀ l ∪ D₂.image (skipMap a₀ l) ≠ Finset.univ)
    (x : ZMod (m - l)) :
    skipMap a₀ l (nextD D₂ hD₂ x) =
      nextD (arcSet a₀ l ∪ D₂.image (skipMap a₀ l)) hD (skipMap a₀ l x) := by
…
```
Mentions: Usa2025P6.arcSet, Usa2025P6.CirclePartition.skipMap, Usa2025P6.CirclePartition.nextD
lemma Usa2025P6.CirclePartition.circleEmb_comp_skipMap Composition of a circular embedding with skipMap line 704 source
Source documentation
Composition of a circular embedding with skipMap.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, HSub.hSub, LE.le, Finset, Ne, Finset.univ, Usa2025P6.CirclePartition.CircleEmb, Union.union, Usa2025P6.arcSet, Finset.image, Usa2025P6.CirclePartition.skipMap, Function.comp
Proof uses: Usa2025P6.CirclePartition.CircleEmb.mk, Function.Injective.comp, Usa2025P6.CirclePartition.skipMap_injective, Usa2025P6.CirclePartition.CircleEmb.inj, Eq.mpr, Eq, HAdd.hAdd, OfNat.ofNat, Usa2025P6.CirclePartition.nextD, id, congrArg, Function.comp_apply, Usa2025P6.CirclePartition.CircleEmb.next, Usa2025P6.CirclePartition.skipMap_nextD, Not, Membership.mem, Or, propext, Finset.mem_union, And and 14 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma circleEmb_comp_skipMap {m : ℕ} [NeZero m] {a₀ : ZMod m} {l : ℕ} [NeZero (m - l)]
    (hl : l ≤ m) {m₂ : ℕ} [NeZero m₂] (D₂ : Finset (ZMod (m - l))) (hD₂ : D₂ ≠ Finset.univ)
    (ψ : ZMod m₂ → ZMod (m - l)) (hψ : CircleEmb D₂ hD₂ ψ)
    (hD : arcSet a₀ l ∪ D₂.image (skipMap a₀ l) ≠ Finset.univ) :
    CircleEmb (arcSet a₀ l ∪ D₂.image (skipMap a₀ l)) hD ((skipMap a₀ l) ∘ ψ) where
…
```
Mentions: Usa2025P6.CirclePartition.CircleEmb, Usa2025P6.arcSet, Usa2025P6.CirclePartition.skipMap
lemma Usa2025P6.CirclePartition.circleEmb_factor Factorization of a circular embedding through skipMap line 731 source
Source documentation
Factorization of a circular embedding through skipMap.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, HSub.hSub, LE.le, Finset, Ne, Finset.univ, Eq, Union.union, Usa2025P6.arcSet, Finset.image, Usa2025P6.CirclePartition.skipMap, Usa2025P6.CirclePartition.CircleEmb, Exists, And, Function.comp
Proof uses: Eq.rec, Membership.mem, Set, Set.range, Not, Usa2025P6.CirclePartition.CircleEmb.notMem, Usa2025P6.CirclePartition.skipMap_cover, And.left, Eq.mp, Or, congrArg, propext, Finset.mem_union, Function.Injective, Usa2025P6.CirclePartition.CircleEmb.inj, Eq.mpr, id, Eq.symm, Eq.refl, Exists.intro and 15 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
lemma circleEmb_factor {m : ℕ} [NeZero m] {m' : ℕ} [NeZero m'] {a₀ : ZMod m} {l : ℕ}
    [NeZero (m - l)] (hl : l ≤ m)
    (D₂ : Finset (ZMod (m - l))) (hD₂ : D₂ ≠ Finset.univ)
    (D : Finset (ZMod m)) (hD : D ≠ Finset.univ)
    (hDeq : D = arcSet a₀ l ∪ D₂.image (skipMap a₀ l))
    (φ : ZMod m' → ZMod m) (hφ : CircleEmb D hD φ) :
    ∃ φ' : ZMod m' → ZMod (m - l), (skipMap a₀ l ∘ φ') = φ ∧ CircleEmb D₂ hD₂ φ' := by
…
```
Mentions: Usa2025P6.arcSet, Usa2025P6.CirclePartition.skipMap, Usa2025P6.CirclePartition.CircleEmb
lemma Usa2025P6.CirclePartition.transport_arc Transport of an arc disjoint from the skipped arc into the smaller circle line 778 source
Source documentation
Transport of an arc disjoint from the skipped arc into the smaller circle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, HSub.hSub, LE.le, OfNat.ofNat, Disjoint, Finset, Usa2025P6.arcSet, Exists, And, Eq, Finset.image, Usa2025P6.CirclePartition.skipMap, Real, Finset.sum
Proof uses: LT.lt, ZMod.val, ZMod.val_lt, HAdd.hAdd, Eq.mpr, ZMod.cast, id, congrArg, ZMod.natCast_val, ZMod.cast_id, add_comm, sub_add_cancel, Eq.refl, Not, Membership.mem, propext, Usa2025P6.CirclePartition.mem_arcSet, Exists.intro, And.intro, of_eq_true and 30 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 78 steps
Open to load the checked before-and-after goal states.
```
lemma transport_arc {m : ℕ} [NeZero m] {a₀ : ZMod m} {l : ℕ} [NeZero (m - l)]
    (hl1 : 1 ≤ l) (hl : l ≤ m) {c : ZMod m} {l₁ : ℕ} (hl₁ : 1 ≤ l₁)
    (hdisj : Disjoint (arcSet a₀ l) (arcSet c l₁)) :
    ∃ v : ZMod (m - l), l₁ ≤ m - l ∧
      (arcSet v l₁).image (skipMap a₀ l) = arcSet c l₁ ∧
      (∀ w : ZMod m → ℝ, ∑ x ∈ arcSet c l₁, w x = ∑ y ∈ arcSet v l₁, w (skipMap a₀ l y)) := by
…
```
Mentions: Usa2025P6.arcSet, Usa2025P6.CirclePartition.skipMap
lemma Usa2025P6.CirclePartition.surgeryMany Surgery: deleting a family of disjoint arcs yields a circular embedding of the complement, built by composing skipMaps line 850 source
Source documentation
Surgery: deleting a family of disjoint arcs yields a circular embedding of the complement, built by composing skipMaps.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, ZMod, LE.le, OfNat.ofNat, Ne, Disjoint, Finset, Usa2025P6.arcSet, Finset.biUnion, Finset.univ, Exists, And, Usa2025P6.CirclePartition.CircleEmb, Eq, HSub.hSub, Finset.sum
Proof uses: Nat.recAux, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.univ_eq_empty, eq_self, Ne.symm, Finset.Nonempty.ne_empty, Finset.univ_nonempty, HAdd.hAdd, id, Usa2025P6.CirclePartition.nextD, Usa2025P6.CirclePartition.gapSize, le_antisymm, Nat.find_min', Not, Membership.mem and 62 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 99 steps
Open to load the checked before-and-after goal states.
```
lemma surgeryMany {t : ℕ} :
    ∀ {m : ℕ} [NeZero m] (ca : Fin t → ZMod m) (la : Fin t → ℕ)
    (_hla1 : ∀ s, 1 ≤ la s) (_hlam : ∀ s, la s ≤ m)
    (_hdij : ∀ s₁ s₂, s₁ ≠ s₂ → Disjoint (arcSet (ca s₁) (la s₁)) (arcSet (ca s₂) (la s₂)))
    (hD : (Finset.univ.biUnion fun s => arcSet (ca s) (la s)) ≠ Finset.univ),
    ∃ (m' : ℕ) (_ : NeZero m') (φ : ZMod m' → ZMod m),
      CircleEmb (Finset.univ.biUnion fun s => arcSet (ca s) (la s)) hD φ ∧
      m' = m - ∑ s, la s := by
…
```
Mentions: Usa2025P6.arcSet, Usa2025P6.CirclePartition.CircleEmb
lemma Usa2025P6.CirclePartition.off_zero line 960 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Eq, Usa2025P6.CirclePartition.off, Fin.mk
Proof uses: Eq.mpr, Finset.sum, Fin, Finset.filter, Finset.univ, Usa2025P6.CirclePartition.len, id, congrArg, Usa2025P6.CirclePartition.off.eq_1, EmptyCollection.emptyCollection, Finset, Iff.mpr, Membership.mem, Not, Finset.filter_eq_empty_iff, Finset.sum_empty, Eq.refl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.off_succ line 965 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2025P6.CirclePartition, Fin, LT.lt, HAdd.hAdd, OfNat.ofNat, Eq, Usa2025P6.CirclePartition.off, Fin.mk, Usa2025P6.CirclePartition.len
Proof uses: Eq.mpr, Finset.sum, Finset.filter, Finset.univ, id, congrArg, Usa2025P6.CirclePartition.off.eq_1, Finset, Union.union, Singleton.singleton, Finset.ext, Iff, Membership.mem, Or, congr, Eq.trans, And, congrFun', Finset.filter_congr, Iff.of_eq and 16 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.mergeOne The single-arc merge lemma: deleting an arc of value < 1 from the circle yields a smaller circle with a partition into k - 1 arcs of value ≥ 1 line 990 source
Source documentation
The single-arc merge lemma: deleting an arc of value < 1 from the circle yields a smaller circle with a partition into k - 1 arcs of value ≥ 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, LE.le, ZMod, Real, Fin, Finset.sum, Usa2025P6.CirclePartition.arcOf, Usa2025P6.arcSet, Exists, HSub.hSub, Function.comp, Usa2025P6.CirclePartition.skipMap
Proof uses: Decidable.byContradiction, Not, Finset.univ, Fin.mk, le_trans, Finset.sum_le_sum_of_subset_of_nonneg, Finset.subset_univ, Membership.mem, Finset, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring and 152 more
184 instances, coercions and auxiliary constants left out.

Tactic trace: 347 steps (first 200 of 347)
Open to load the checked before-and-after goal states.
```
lemma mergeOne {m k : ℕ} [NeZero m] (P : CirclePartition m k) (hk : 0 < k) (hk2 : 2 ≤ k)
    (w : ZMod m → ℝ) (hnn : ∀ x, 0 ≤ w x)
    (hval : ∀ i, 1 ≤ ∑ x ∈ P.arcOf i, w x)
    {a₀ : ZMod m} {l : ℕ} (hl1 : 1 ≤ l) (hlm : l ≤ m)
    (hA : ∑ x ∈ arcSet a₀ l, w x < 1) :
    ∃ (P' : CirclePartition (m - l) (k - 1)),
      (∀ i, 1 ≤ ∑ x ∈ P'.arcOf i, (w ∘ skipMap a₀ l) x) := by
…
```
Mentions: P, Usa2025P6.CirclePartition, Usa2025P6.arcSet, Usa2025P6.CirclePartition.skipMap
def Usa2025P6.CirclePartition.cast Reindexing a circular partition along an equality of the number of arcs line 1355 source
Source documentation
Reindexing a circular partition along an equality of the number of arcs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2025P6.CirclePartition
Proof uses: Usa2025P6.CirclePartition.mk, Usa2025P6.CirclePartition.base, Fin, Usa2025P6.CirclePartition.len, Fin.cast, Eq.symm
2 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def cast {m a b : ℕ} (h : a = b) (P : CirclePartition m a) :
    CirclePartition m b where
…
```
Mentions: h, P, Usa2025P6.CirclePartition
lemma Usa2025P6.CirclePartition.circlePartition_cast_len line 1365 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2025P6.CirclePartition, Fin, Usa2025P6.CirclePartition.len, Usa2025P6.CirclePartition.cast, Fin.cast, Eq.symm
Proof uses: rfl
lemma Usa2025P6.CirclePartition.circlePartition_cast_off line 1368 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2025P6.CirclePartition, Fin, Usa2025P6.CirclePartition.off, Usa2025P6.CirclePartition.cast, Fin.cast, Eq.symm
Proof uses: Eq.rec, Eq.mpr, Eq.refl, id, congrArg, congrFun, Fin.cast_refl, Finset.sum, Finset.filter, LT.lt, Finset.univ, Usa2025P6.CirclePartition.len, Usa2025P6.CirclePartition.off.eq_1, Finset.sum_congr, rfl, Finset, Membership.mem
6 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.circlePartition_cast_arcOf line 1377 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2025P6.CirclePartition, Fin, Finset, ZMod, Usa2025P6.CirclePartition.arcOf, Usa2025P6.CirclePartition.cast, Fin.cast, Eq.symm
Proof uses: Usa2025P6.CirclePartition.start, Eq.mpr, HAdd.hAdd, Usa2025P6.CirclePartition.base, Usa2025P6.CirclePartition.off, id, congrArg, Usa2025P6.CirclePartition.start.eq_1, Usa2025P6.CirclePartition.circlePartition_cast_off, Eq.refl, Usa2025P6.arcSet, Usa2025P6.CirclePartition.len, Usa2025P6.CirclePartition.arcOf.eq_1, Usa2025P6.CirclePartition.circlePartition_cast_len
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2025P6.CirclePartition.mergeValues The multi-arc merge lemma: deleting t disjoint arcs, each of value < 1, yields a smaller circle with a partition into k - t arcs of value ≥ 1 line 1386 source
Source documentation
The multi-arc merge lemma: deleting t disjoint arcs, each of value < 1, yields a smaller circle with a partition into k - t arcs of value ≥ 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Usa2025P6.CirclePartition, LT.lt, OfNat.ofNat, Fin, ZMod, Real, LE.le, Finset.sum, Usa2025P6.CirclePartition.arcOf, Ne, Disjoint, Finset, Usa2025P6.arcSet, Finset.biUnion, Finset.univ, Usa2025P6.CirclePartition.CircleEmb, Exists, HSub.hSub and 1 more
Proof uses: Nat.recAux, Eq, Nat.sub_zero, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.univ_eq_empty, eq_self, Ne.symm, Finset.Nonempty.ne_empty, Finset.univ_nonempty, Usa2025P6.CirclePartition.CircleEmb.congr_D, HAdd.hAdd, Usa2025P6.CirclePartition.nextD, Usa2025P6.CirclePartition.CircleEmb.next, Usa2025P6.CirclePartition.gapSize, le_antisymm and 155 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 165 steps
Open to load the checked before-and-after goal states.
```
lemma mergeValues {t : ℕ} :
    ∀ {m k : ℕ} [NeZero m] (P : CirclePartition m k) (_hk : 0 < k)
    (ca : Fin t → ZMod m) (la : Fin t → ℕ) (w : ZMod m → ℝ)
    (_hnn : ∀ x, 0 ≤ w x) (_hval : ∀ i, 1 ≤ ∑ x ∈ P.arcOf i, w x)
    (_hla1 : ∀ s, 1 ≤ la s) (_hlam : ∀ s, la s ≤ m)
    (_hdij : ∀ s₁ s₂, s₁ ≠ s₂ → Disjoint (arcSet (ca s₁) (la s₁)) (arcSet (ca s₂) (la s₂)))
    (_harcval : ∀ s, ∑ x ∈ arcSet (ca s) (la s), w x < 1)
    (_htk : t < k)
    {m' : ℕ} [NeZero m'] (φ : ZMod m' → ZMod m)
    {hD : (Finset.univ.biUnion fun s => arcSet (ca s) (la s)) ≠ Finset.univ}
    (_hφ : CircleEmb _ hD φ),
    ∃ P' : CirclePartition m' (k - t), ∀ i, 1 ≤ ∑ x ∈ P'.arcOf i, (w ∘ φ) x := by
…
```
Mentions: P, Usa2025P6.CirclePartition, Usa2025P6.arcSet, Usa2025P6.CirclePartition.CircleEmb
theorem Usa2025P6.CirclePartition.hall_deficiency line 1569 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, DecidableRel, Exists, Finset, And, Membership.mem, Eq, Finset.card, Not
Proof uses: Finset.filter, Finset.univ, rfl, Int, HSub.hSub, Finset.biUnion, LE.le, Finset.exists_max_image, Exists.intro, EmptyCollection.emptyCollection, Finset.mem_univ, OfNat.ofNat, LT.lt, Or, le_or_gt, Eq.mp, congrArg, cast, Function.Injective, Iff.mp and 57 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 134 steps
Open to load the checked before-and-after goal states.
theorem Usa2025P6.CirclePartition.usa2025_p6_main The main theorem: USAMO 2025 Problem 6 line 1719 source
Source documentation
The main theorem: USAMO 2025 Problem 6.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, NeZero, LE.le, Fin, ZMod, Real, Exists, Usa2025P6.CirclePartition, Finset.sum, Usa2025P6.CirclePartition.arcOf, Finset.filter, Eq, Finset.univ
Proof uses: Nat.strong_induction_on, Nat.succ, Or, Nat.eq_or_lt_of_le, Fin.mk, Usa2025P6.CirclePartition.len, Usa2025P6.CirclePartition.len_sum, Eq.mp, congrArg, Fin.sum_univ_one, Finset, Eq.mpr, Usa2025P6.arcSet, Usa2025P6.CirclePartition.start, id, Usa2025P6.CirclePartition.arcOf.eq_1, Usa2025P6.CirclePartition.arcSet_univ, Eq.refl, Exists.intro, Subsingleton.elim and 105 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 277 steps (first 200 of 277)
Open to load the checked before-and-after goal states.
```
theorem usa2025_p6_main (N : ℕ) (hN : 0 < N) : ∀ (m : ℕ) [NeZero m] (_hmn : N ≤ m)
    (like : Fin N → ZMod m → ℝ) (_hnn : ∀ p c, 0 ≤ like p c)
    (_hpart : ∀ p, ∃ P : CirclePartition m N, ∀ i, 1 ≤ ∑ x ∈ P.arcOf i, like p x),
    ∃ a : ZMod m → Fin N, ∀ p, 1 ≤ ∑ c ∈ Finset.univ.filter (a · = p), like p c := by
…
```
Mentions: P, Usa2025P6.CirclePartition
problem Usa2025P6.usa2025_p6 The USAMO 2025 Problem 6: distributing cupcakes to people so that everybody gets total score at least one in their own ranking line 1994 source
Source documentation
The USAMO 2025 Problem 6: distributing cupcakes to people so that everybody gets total score at least one in their own ranking.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LT.lt, OfNat.ofNat, LE.le, Fin, ZMod, Real, Exists, Usa2025P6.CirclePartition, Finset.sum, Usa2025P6.CirclePartition.arcOf, Finset.filter, Eq, Finset.univ
Proof uses: Usa2025P6.CirclePartition.usa2025_p6_main
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
problem usa2025_p6 {m n : ℕ} [NeZero m] (_hm : 0 < m) (hn : 0 < n) (hmn : n ≤ m)
    (like : Fin n → ZMod m → ℝ) (hnn : ∀ p c, 0 ≤ like p c)
    (hpart : ∀ p, ∃ P : CirclePartition m n, ∀ i, 1 ≤ ∑ x ∈ P.arcOf i, like p x) :
    ∃ a : ZMod m → Fin n, ∀ p, 1 ≤ ∑ c ∈ Finset.univ.filter (a · = p), like p c := by
…
```
Mentions: P, Usa2025P6.CirclePartition