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

242 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2026, Problem 3

Let n be a positive integer. Liu Bang and Xiang Yu have a stick of length 1 and want to divide it between themselves. Liu marks at most n points on the stick, and then Xiang marks at most n points on the stick. The marked points are distinct. Then, the stick is cut at all marked points, creating a number of pieces. Afterwards, they take turns claiming any unclaimed piece of the stick, with Liu going first. Each player's goal is to maximise the total length of their own pieces.

For each n, determine the largest value c such that Liu may guarantee a total length of at least c, regardless of Xiang's play.

Imports (6)

Imported by 1 file

Compfiles.lean

def Imo2026P3.pieceLengths The multiset of piece lengths obtained by cutting [0,1] at the points of a finite set S ⊆ (0,1) line 49 source
Source documentation
The multiset of piece lengths obtained by cutting [0,1] at the points of a finite set S ⊆ (0,1). We sort S ascending, prepend 0 and append 1, and take consecutive differences. The result is a list of |S| + 1 positive reals summing to 1 (when S ⊆ (0,1)).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, List
Proof uses: HAppend.hAppend, List.cons, OfNat.ofNat, Finset.sort, LE.le, List.nil, List.zipWith, HSub.hSub, List.tail
15 instances, coercions and auxiliary constants left out.
```
def pieceLengths (S : Finset ℝ) : List ℝ :=
…
```
Mentions: S
def Imo2026P3.firstPlayerShare The sum of the entries of a list L at the (0-indexed) even positions, after sorting L in non-increasing order line 57 source
Source documentation
The sum of the entries of a list L at the (0-indexed) even positions, after sorting L in non-increasing order. These are the entries in the 1st, 3rd, 5th, … positions of the sorted (decreasing) list, i.e. the pieces claimed by the first mover under the greedy claiming rule.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real
Proof uses: List.mergeSort, Decidable.decide, GE.ge, List.sum, List.map, Prod, Nat, Prod.fst, List.filter, Eq, HMod.hMod, Prod.snd, OfNat.ofNat, List.zipIdx
8 instances, coercions and auxiliary constants left out.
```
def firstPlayerShare (L : List ℝ) : ℝ :=
…
```
Mentions: Imo2026P3.L
def Imo2026P3.L L(A,B): Liu Bang's total length, given Liu Bang's marks A and Xiang Yu's marks B line 63 source
Source documentation
L(A,B): Liu Bang's total length, given Liu Bang's marks A and Xiang Yu's marks B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real
Proof uses: Imo2026P3.firstPlayerShare, Imo2026P3.pieceLengths, Union.union
2 instances, coercions and auxiliary constants left out.
```
def L (A B : Finset ℝ) : ℝ :=
…
```
def Imo2026P3.AdmissibleMark The set of admissible markings for a player: a finite subset of (0,1) of size at most n line 68 source
Source documentation
The set of admissible markings for a player: a finite subset of (0,1) of size at most n. We encode it as a Finset ℝ subject to the side conditions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Real
Proof uses: And, LE.le, Set, Set.Ioo, OfNat.ofNat, Finset.card
9 instances, coercions and auxiliary constants left out.
```
def AdmissibleMark (n : ℕ) (X : Finset ℝ) : Prop :=
…
```
def Imo2026P3.V The value Liu Bang can guarantee line 75 source
Source documentation
The value Liu Bang can guarantee.
V n is the supremum over Liu Bang's admissible markings A of the infimum, over Xiang Yu's admissible markings B disjoint from A, of L A B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: iSup, Subtype, Finset, Imo2026P3.AdmissibleMark, iInf, And, Disjoint, Imo2026P3.L
5 instances, coercions and auxiliary constants left out.
```
def V (n : ℕ) : ℝ :=
…
```
determine Imo2026P3.answer line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HDiv.hDiv, HPow.hPow, OfNat.ofNat, HSub.hSub, HAdd.hAdd
17 instances, coercions and auxiliary constants left out.
theorem Imo2026P3.pieceLengths_sum The piece lengths of an admissible cut set sum to 1 (the total stick length) line 93 source
Source documentation
The piece lengths of an admissible cut set sum to 1 (the total stick length).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, LE.le, Set, Set.Ioo, OfNat.ofNat, Eq, List.sum, Imo2026P3.pieceLengths
Proof uses: List, List.zipWith, HSub.hSub, List.tail, List.getLastD, List.headD, List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, List.map, List.zipWith_self, congrFun', funext, sub_self, List.map_nil, List.getLastD_eq_getLast? and 52 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem pieceLengths_sum (S : Finset ℝ) (_hS : ↑S ⊆ Set.Ioo (0 : ℝ) 1) :
    (pieceLengths S).sum = 1 := by
…
```
Mentions: S, Imo2026P3.pieceLengths
theorem Imo2026P3.pieceLengths_length There are |S| + 1 pieces line 122 source
Source documentation
There are |S| + 1 pieces.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, Eq, Nat, List.length, Imo2026P3.pieceLengths, HAdd.hAdd, Finset.card, OfNat.ofNat
Proof uses: List, List.zipWith, HSub.hSub, HAppend.hAppend, List.cons, Finset.sort, LE.le, List.nil, List.tail, rfl, Eq.mpr, id, congrArg, Min.min, List.length_zipWith, of_eq_true, Eq.trans, True, congrFun', congr and 5 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem pieceLengths_length (S : Finset ℝ) :
    (pieceLengths S).length = S.card + 1 := by
…
```
Mentions: S, Imo2026P3.pieceLengths
theorem Imo2026P3.L_mem_Icc Basic sanity bound: Liu Bang's share lies in [0, 1] for admissible cut sets (it is a subset-sum of the piece lengths, which are nonnegative and sum to 1) line 133 source
Source documentation
Basic sanity bound: Liu Bang's share lies in [0, 1] for admissible cut sets (it is a subset-sum of the piece lengths, which are nonnegative and sum to 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, LE.le, Set, Set.Ioo, OfNat.ofNat, Membership.mem, Set.Icc, Imo2026P3.L
Proof uses: Union.union, Eq.mpr, id, Eq, congrArg, Finset.coe_union, Set.union_subset, List, List.Pairwise, List.zipWith, HSub.hSub, HAppend.hAppend, List.cons, List.nil, List.tail, List.rec, Eq.mp, Eq.trans, Or, congrFun' and 48 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
theorem L_mem_Icc (A B : Finset ℝ)
    (hA : ↑A ⊆ Set.Ioo (0 : ℝ) 1) (hB : ↑B ⊆ Set.Ioo (0 : ℝ) 1) :
    L A B ∈ Set.Icc (0 : ℝ) 1 := by
…
```
Mentions: Imo2026P3.L
def Imo2026P3.interiorPartialSums line 202 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real
Proof uses: List.dropLast, List.tail, List.scanl, HAdd.hAdd, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
def Imo2026P3.cutsOfLengths line 205 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset
Proof uses: List.toFinset, Imo2026P3.interiorPartialSums
1 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.scanl_mem_ge line 208 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LE.le, OfNat.ofNat, List.scanl, HAdd.hAdd
Proof uses: List.rec, List.nil, le_rfl, Eq.symm, Eq.mp, Eq, Eq.trans, List.cons, congrFun', congrArg, List.scanl_nil, Or, Iff.mp, List.mem_cons, List.scanl_cons, List.mem_cons_self, List.mem_cons_of_mem, le_of_add_le_of_nonneg_left
21 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.pairwise_scanl_lt line 223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LT.lt, OfNat.ofNat, List.Pairwise, List.scanl, HAdd.hAdd
Proof uses: List.rec, List.nil, of_eq_true, Eq.trans, And, True, List.cons, congrArg, List.scanl_nil, congr, forall_congr, False, implies_congr, Eq.refl, implies_true, and_self, Eq.mpr, id, Eq, List.scanl_cons and 52 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.zipWith_scanl_tail line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, List.zipWith, HSub.hSub, List.scanl, HAdd.hAdd, List.tail
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congrFun', congrArg, List.cons, congr, List.scanl_nil, List.zipWith_nil_right, eq_self, Eq.mpr, id, List.scanl_cons, Eq.symm, Eq.refl, And, List.cons.injEq, And.intro and 34 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.scanl_zipWith_diff line 254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, List.scanl, HAdd.hAdd, List.zipWith, HSub.hSub, List.cons
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congrFun', congrArg, List.zipWith_nil_right, List.scanl_nil, eq_self, Eq.mpr, id, List.zipWith_cons_cons, List.scanl_cons, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, OfNat.ofNat and 29 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.zipWith_diff_pos_of_pairwise line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, List.Pairwise, LT.lt, Membership.mem, List.zipWith, HSub.hSub, List.tail, OfNat.ofNat
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, implies_congr, forall_congr, False, congrFun', congrArg, List.map, List.zipWith_self, funext, sub_self, List.map_nil, Eq.refl, implies_true, Eq, List.cons, And and 15 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.pieceLengths_pos line 281 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, LE.le, Set, Set.Ioo, OfNat.ofNat, Membership.mem, List, Imo2026P3.pieceLengths, LT.lt
Proof uses: Finset.sort, HAppend.hAppend, List.cons, List.nil, List.Pairwise, List.SortedLT.pairwise, Finset.sortedLT_sort, And.left, Iff.mp, Finset.mem_sort, And.right, id, Eq.mpr, And, Eq, congrArg, propext, List.pairwise_append, List.pairwise_cons, And.intro and 22 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.foldl_add_init line 304 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, List.foldl, HAdd.hAdd, List.sum
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congrArg, add_zero, eq_self, Eq.mpr, List.cons, id, List.foldl_cons, List.sum_cons, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, OfNat.ofNat, Mathlib.Tactic.Ring.Common.add_congr and 6 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.scanl_last_eq_sum line 312 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Ne, List.scanl, HAdd.hAdd, List.nil, Eq, List.getLast, List.sum
Proof uses: Eq.mpr, List.foldl, id, congrArg, List.getLast_scanl, Imo2026P3.foldl_add_init, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.interiorPartialSums_pairwise line 317 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LT.lt, OfNat.ofNat, List.Pairwise, Imo2026P3.interiorPartialSums
Proof uses: List.Pairwise.sublist, List.tail, List.scanl, HAdd.hAdd, List.dropLast_sublist, List.tail_sublist, Imo2026P3.pairwise_scanl_lt
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.sort_cutsOfLengths line 323 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LT.lt, OfNat.ofNat, Eq, Finset.sort, Imo2026P3.cutsOfLengths, LE.le, Imo2026P3.interiorPartialSums
Proof uses: Iff.mpr, List.toFinset, List.Pairwise, List.toFinset_sort, List.Pairwise.nodup, Imo2026P3.interiorPartialSums_pairwise, List.Pairwise.imp, LT.lt.le
24 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.boundaryList_eq_scanl line 329 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Ne, List.nil, Eq, List.sum, OfNat.ofNat, HAppend.hAppend, List.cons, Imo2026P3.interiorPartialSums, List.scanl, HAdd.hAdd
Proof uses: absurd, Eq.refl, Eq.symm, id, Eq.mpr, List.dropLast, List.tail, congrArg, List.scanl_cons, of_eq_true, Eq.trans, True, congrFun', zero_add, Not, False, not_false_eq_true, List.getLast, Imo2026P3.scanl_last_eq_sum, List.cons_append and 3 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.pieceLengths_cutsOfLengths line 349 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, Imo2026P3.pieceLengths, Imo2026P3.cutsOfLengths
Proof uses: id, Eq.mpr, HAppend.hAppend, List.cons, Finset.sort, LE.le, List.zipWith, HSub.hSub, List.tail, Imo2026P3.interiorPartialSums, congrArg, Imo2026P3.sort_cutsOfLengths, List.scanl, HAdd.hAdd, Imo2026P3.boundaryList_eq_scanl, Imo2026P3.zipWith_scanl_tail
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.interiorPartialSums_pieceLengths line 356 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, Eq, List, Imo2026P3.interiorPartialSums, Imo2026P3.pieceLengths, Finset.sort, LE.le
Proof uses: id, List.dropLast, List.tail, List.scanl, HAdd.hAdd, OfNat.ofNat, HAppend.hAppend, List.cons, List.nil, List.zipWith, HSub.hSub, Eq.mpr, congrArg, Imo2026P3.scanl_zipWith_diff, List.tail_cons, of_eq_true, Eq.trans, DecidableRel, IsTrans, Eq.refl and 11 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.cutsOfLengths_pieceLengths line 365 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, Eq, Imo2026P3.cutsOfLengths, Imo2026P3.pieceLengths
Proof uses: id, Eq.mpr, List.toFinset, Imo2026P3.interiorPartialSums, Finset.sort, LE.le, congrArg, List, Imo2026P3.interiorPartialSums_pieceLengths, Finset.sort_toFinset, 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 Imo2026P3.mem_interiorPartialSums_Ioo line 370 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, Imo2026P3.interiorPartialSums, Set, Set.Ioo
Proof uses: List.Pairwise, HAppend.hAppend, List.cons, Eq.mpr, List.scanl, HAdd.hAdd, id, congrArg, Imo2026P3.boundaryList_eq_scanl, Imo2026P3.pairwise_scanl_lt, And, Iff.mp, List.pairwise_append, And.left, List.pairwise_cons, List.mem_cons_of_mem, of_eq_true, Eq.trans, Or, True and 5 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.card_cutsOfLengths line 381 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, Nat, HAdd.hAdd, Finset.card, Imo2026P3.cutsOfLengths, List.length
Proof uses: id, Eq.mpr, List.toFinset, Imo2026P3.interiorPartialSums, congrArg, List.toFinset_card_of_nodup, List.Pairwise.nodup, Imo2026P3.interiorPartialSums_pairwise, List.dropLast, List.tail, List.scanl, HSub.hSub, List.length_dropLast, List.length_tail, List.length_scanl, Iff.mpr, List.length_pos_iff
22 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.admissible_cutsOfLengths line 391 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Real, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, LE.le, List.length, HAdd.hAdd, Imo2026P3.AdmissibleMark, Imo2026P3.cutsOfLengths
Proof uses: And.intro, Set, Finset, Set.Ioo, Finset.card, Imo2026P3.mem_interiorPartialSums_Ioo, Eq.mp, Imo2026P3.interiorPartialSums, congrFun', Set.ofPred, congrArg, List.coe_toFinset, Imo2026P3.card_cutsOfLengths
29 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.exists_reply_of_refinement line 401 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Real, List, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, LE.le, Imo2026P3.cutsOfLengths, HSub.hSub, Finset.card, Exists, And, Imo2026P3.AdmissibleMark, Disjoint, Imo2026P3.L and 1 more
Proof uses: SDiff.sdiff, Exists.intro, And.intro, Set, Set.Ioo, And.left, Not, Iff.mp, Finset.mem_sdiff, Imo2026P3.mem_interiorPartialSums_Ioo, Eq.mp, Imo2026P3.interiorPartialSums, Eq.mpr, HAdd.hAdd, id, Eq.trans, congrFun', congrArg, Inter.inter, Finset.card_sdiff and 9 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.exists_reply_of_refinement_length line 421 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Real, List, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, LE.le, Imo2026P3.cutsOfLengths, List.length, HAdd.hAdd, Finset.card, Exists, And, Imo2026P3.AdmissibleMark, Disjoint and 2 more
Proof uses: Imo2026P3.exists_reply_of_refinement, Imo2026P3.card_cutsOfLengths
30 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.exists_reply_of_piece_refinement line 430 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Real, List, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, LE.le, Imo2026P3.cutsOfLengths, Imo2026P3.pieceLengths, List.length, HAdd.hAdd, Finset.card, Exists, And, Imo2026P3.AdmissibleMark and 3 more
Proof uses: Imo2026P3.exists_reply_of_refinement_length, Eq.mp, congrFun', congrArg, Imo2026P3.cutsOfLengths_pieceLengths
29 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.surplus The "greedy surplus" of a list: sum of adjacent pair differences, plus the last entry if the length is odd line 447 source
Source documentation
The "greedy surplus" of a list: sum of adjacent pair differences, plus the last entry if the length is odd. For a decreasing list this equals 2 * (even-position sum) - (total sum).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real
2 instances, coercions and auxiliary constants left out.
```
def surplus : List ℝ → ℝ
  | [] => 0
  | [x] => x
  | x :: y :: t => (x - y) + surplus t

/-- The sum of entries at even (0-indexed) positions. -/
```
def Imo2026P3.evenSum The sum of entries at even (0-indexed) positions line 453 source
Source documentation
The sum of entries at even (0-indexed) positions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real
Proof uses: List.sum, List.map, Prod, Nat, Prod.fst, List.filter, Decidable.decide, Eq, HMod.hMod, Prod.snd, OfNat.ofNat, List.zipIdx
6 instances, coercions and auxiliary constants left out.
```
def evenSum (l : List ℝ) : ℝ :=
…
```
lemma Imo2026P3.evenSum_zipIdx_offset' line 456 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Nat, Eq, HMod.hMod, OfNat.ofNat, List.map, Prod, Prod.fst, List.filter, Decidable.decide, Prod.snd, List.zipIdx
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, List.map_nil, eq_self, Eq.mpr, List.cons, Prod.mk, HAdd.hAdd, id, List.zipIdx_cons, ite, Bool, Bool.true, List.filter_cons, dite and 15 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.evenSum_cons2 line 472 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, List, Eq, Imo2026P3.evenSum, List.cons, HAdd.hAdd
Proof uses: id, Eq.mpr, List.sum, List.map, Prod, Nat, Prod.fst, List.filter, Decidable.decide, HMod.hMod, Prod.snd, OfNat.ofNat, List.zipIdx, Prod.mk, congrArg, List.zipIdx_cons, ite, Bool, True, Bool.true and 23 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.evenSum_nil line 482 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, Imo2026P3.evenSum, List.nil, OfNat.ofNat
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.evenSum_singleton line 484 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Imo2026P3.evenSum, List.cons, List.nil
Proof uses: id, of_eq_true, List.sum, List.map, Prod, Nat, Prod.fst, List.filter, Decidable.decide, HMod.hMod, Prod.snd, OfNat.ofNat, List.zipIdx, Eq.trans, True, congrFun', congrArg, List, Prod.mk, HAdd.hAdd and 10 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.two_mul_evenSum_sub_sum For any list, 2 * evenSum - sum = surplus line 489 source
Source documentation
For any list, 2 * evenSum - sum = surplus. No sortedness needed.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, HSub.hSub, HMul.hMul, OfNat.ofNat, Nat, Imo2026P3.evenSum, List.sum, Imo2026P3.surplus
Proof uses: Imo2026P3.surplus.induct, of_eq_true, List.nil, Eq.trans, True, congrFun', congrArg, MulZeroClass.mul_zero, sub_self, eq_self, Eq.mpr, List.cons, id, congr, Imo2026P3.evenSum_singleton, add_zero, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat.rawCast and 60 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma two_mul_evenSum_sub_sum : ∀ l : List ℝ, 2 * evenSum l - l.sum = surplus l := by
…
```
Mentions: Imo2026P3.evenSum, Imo2026P3.surplus
lemma Imo2026P3.firstPlayerShare_eq_evenSum firstPlayerShare of a list equals evenSum of its decreasing sort line 500 source
Source documentation
firstPlayerShare of a list equals evenSum of its decreasing sort.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Imo2026P3.firstPlayerShare, Imo2026P3.evenSum, List.mergeSort, Decidable.decide, GE.ge
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
```
lemma firstPlayerShare_eq_evenSum (l : List ℝ) :
    firstPlayerShare l = evenSum (l.mergeSort (· ≥ ·)) := rfl
```
Mentions: Imo2026P3.firstPlayerShare, Imo2026P3.evenSum
lemma Imo2026P3.firstPlayerShare_congr firstPlayerShare is invariant under permutation: both mergeSorts are decreasing-sorted perms of each other, hence equal line 505 source
Source documentation
firstPlayerShare is invariant under permutation: both mergeSorts are decreasing-sorted perms of each other, hence equal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, List.Perm, Eq, Imo2026P3.firstPlayerShare
Proof uses: List.mergeSort, Decidable.decide, GE.ge, List.Perm.trans, List.mergeSort_perm, List.Perm.symm, List.Pairwise, List.pairwise_mergeSort', Eq.mpr, Imo2026P3.evenSum, id, congrArg, Imo2026P3.firstPlayerShare_eq_evenSum, List.Perm.eq_of_pairwise', Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma firstPlayerShare_congr {l₁ l₂ : List ℝ} (h : l₁.Perm l₂) :
    firstPlayerShare l₁ = firstPlayerShare l₂ := by
…
```
Mentions: h, Imo2026P3.firstPlayerShare
def Imo2026P3.pairDup line 518 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real
Proof uses: List.flatMap, List.cons, List.nil
lemma Imo2026P3.even_zip_sum_pairDup_aux line 520 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Nat, Eq, HMod.hMod, OfNat.ofNat, List.sum, List.map, Prod, Prod.fst, List.filter, Decidable.decide, Prod.snd, List.zipIdx, Imo2026P3.pairDup
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congrFun', congrArg, optParam, List.flatMap_nil, List.cons, List.map_nil, eq_self, HAdd.hAdd, Ne, Eq.mpr, List.flatMap, id, Prod.mk, List.flatMap_cons, List.filter_cons_of_pos and 13 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.even_zip_sum_pairDup line 533 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, List.sum, List.map, Prod, Nat, Prod.fst, List.filter, Decidable.decide, HMod.hMod, Prod.snd, OfNat.ofNat, List.zipIdx, Imo2026P3.pairDup
Proof uses: Imo2026P3.even_zip_sum_pairDup_aux, rfl
9 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.odd_zip_sum_pairDup_aux line 538 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Nat, Eq, HMod.hMod, OfNat.ofNat, List.sum, List.map, Prod, Prod.fst, List.filter, Decidable.decide, Prod.snd, List.zipIdx, Imo2026P3.pairDup
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congrFun', congrArg, optParam, List.flatMap_nil, List.cons, List.map_nil, eq_self, HAdd.hAdd, Eq.mpr, List.flatMap, id, Prod.mk, List.flatMap_cons, List.filter_cons_of_neg, Not and 11 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.zip_sum_pairDup_aux line 551 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Nat, Eq, List.sum, List.map, Prod, Prod.fst, List.filter, Decidable.decide, HMod.hMod, Prod.snd, OfNat.ofNat, List.zipIdx, Imo2026P3.pairDup
Proof uses: dite, Imo2026P3.even_zip_sum_pairDup_aux, Not, Imo2026P3.odd_zip_sum_pairDup_aux
13 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.length_pairDup line 559 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Nat, List.length, Imo2026P3.pairDup, HMul.hMul, OfNat.ofNat
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, List.flatMap_nil, List.cons, MulZeroClass.mul_zero, eq_self, Eq.mpr, id, Eq.refl, HAdd.hAdd, congrFun'
12 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.even_zip_sum_pairs_singleton_pairs line 567 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, List.sum, List.map, Prod, Nat, Prod.fst, List.filter, Decidable.decide, HMod.hMod, Prod.snd, OfNat.ofNat, List.zipIdx, HAppend.hAppend, Imo2026P3.pairDup, List.cons, HAdd.hAdd
Proof uses: Eq.mpr, List.length, id, congrArg, List.zipIdx_append, congrFun', Eq.trans, List.filter_append, List.map_append, List.sum_append, Imo2026P3.zip_sum_pairDup_aux, HMul.hMul, Imo2026P3.length_pairDup, Prod.mk, zero_add, List.filter_cons_of_pos, of_eq_true, Bool, Bool.true, True and 14 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.pairwise_pairDup line 580 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, List.Pairwise, GE.ge, Imo2026P3.pairDup
Proof uses: List.rec, List.nil, of_eq_true, Eq.trans, LE.le, True, congr, congrArg, funext, List.flatMap_nil, List.cons, Membership.mem, And, Exists, Eq.mp, Eq, Or, False, or_false, or_self and 12 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.firstPlayerShare_pairDup_of_pairwise line 602 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, List.Pairwise, GE.ge, Eq, Imo2026P3.firstPlayerShare, Imo2026P3.pairDup, List.sum
Proof uses: id, Eq.mpr, List.mergeSort, Decidable.decide, List.map, Prod, Nat, Prod.fst, List.filter, HMod.hMod, Prod.snd, OfNat.ofNat, List.zipIdx, congrArg, List.mergeSort_eq_self, Imo2026P3.pairwise_pairDup, Imo2026P3.even_zip_sum_pairDup
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.sum_pairDup line 608 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, List.sum, Imo2026P3.pairDup, HMul.hMul, OfNat.ofNat, Nat
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, List.flatMap_nil, List.cons, MulZeroClass.mul_zero, eq_self, Eq.mpr, id, Eq.refl, HAdd.hAdd, List.sum_cons, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr and 21 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.twice_firstPlayerShare_pairDup line 616 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, List.Pairwise, GE.ge, Eq, HMul.hMul, OfNat.ofNat, Nat, Imo2026P3.firstPlayerShare, Imo2026P3.pairDup, List.sum
Proof uses: Eq.mpr, id, congrArg, Imo2026P3.firstPlayerShare_pairDup_of_pairwise, Imo2026P3.sum_pairDup, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.firstPlayerShare_pairs_singleton_pairs line 620 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, List.Pairwise, GE.ge, HAppend.hAppend, Imo2026P3.pairDup, List.cons, Eq, Imo2026P3.firstPlayerShare, HAdd.hAdd, List.sum
Proof uses: id, Eq.mpr, List.mergeSort, Decidable.decide, List.map, Prod, Nat, Prod.fst, List.filter, HMod.hMod, Prod.snd, OfNat.ofNat, List.zipIdx, congrArg, List.mergeSort_eq_self, Imo2026P3.even_zip_sum_pairs_singleton_pairs
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.surplus_pairs_singleton_pairs line 627 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, List.Pairwise, GE.ge, HAppend.hAppend, Imo2026P3.pairDup, List.cons, Eq, HMul.hMul, OfNat.ofNat, Nat, Imo2026P3.firstPlayerShare, HAdd.hAdd, List.sum
Proof uses: Eq.mpr, id, congrArg, Imo2026P3.firstPlayerShare_pairs_singleton_pairs, List.sum_append, List.sum_cons, Imo2026P3.sum_pairDup, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_pf_add_lt and 13 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.geom_two Geometric sum of powers of two over range m line 641 source
Source documentation
Geometric sum of powers of two over range m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Finset.sum, Finset.range, HPow.hPow, OfNat.ofNat, HSub.hSub
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, congrFun', pow_zero, sub_self, eq_self, Eq.mpr, HAdd.hAdd, id, Finset.sum_range_succ, Mathlib.Tactic.Ring.of_eq, Int.rawCast, inferInstance, Ring, Int.negOfNat, HMul.hMul, Nat.rawCast and 42 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma geom_two (m : ℕ) : ∑ j ∈ range m, (2 : ℝ) ^ j = 2 ^ m - 1 := by
…
```
lemma Imo2026P3.pow_two_punch The discrete punchline: a signed sum of distinct powers of two, with at least one nonzero sign, has absolute value at least one line 650 source
Source documentation
The discrete punchline: a signed sum of distinct powers of two, with at least one nonzero sign, has absolute value at least one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nat, Function.Injective, Real, Or, Eq, OfNat.ofNat, Neg.neg, Exists, Ne, LE.le, abs, Finset.sum, Finset.univ, HMul.hMul, HPow.hPow
Proof uses: Finset, Finset.filter, rfl, Finset.Nonempty, Exists.intro, Membership.mem, Iff.mpr, And, Finset.mem_filter, And.intro, Finset.mem_univ, Finset.exists_max_image, And.right, Iff.mp, of_eq_true, Eq.trans, True, congrFun', congrArg, abs_one and 107 more
142 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
```
lemma pow_two_punch {ι : Type} [Fintype ι] [DecidableEq ι]
    (p : ι → ℕ) (hp : Function.Injective p)
    (s : ι → ℝ) (hs : ∀ i, s i = 1 ∨ s i = -1 ∨ s i = 0) (hne : ∃ i, s i ≠ 0) :
    1 ≤ |∑ i, s i * 2 ^ p i| := by
…
```
def Imo2026P3.codexDenom line 725 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HSub.hSub, HPow.hPow, OfNat.ofNat, HAdd.hAdd
14 instances, coercions and auxiliary constants left out.
def Imo2026P3.codexDyadicWeights line 727 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Real
Proof uses: List.map, HDiv.hDiv, HPow.hPow, OfNat.ofNat, Imo2026P3.codexDenom, List.range, HAdd.hAdd
13 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.codex_list_geom_two line 730 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, List.sum, List.map, HPow.hPow, OfNat.ofNat, List.range, HSub.hSub
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, List, List.nil, List.map_nil, congrFun', pow_zero, sub_self, eq_self, Eq.mpr, HAdd.hAdd, HAppend.hAppend, List.cons, id, Nat.succ, List.range_succ and 53 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.codex_sum_map_div line 739 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, List.sum, List.map, HDiv.hDiv
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, OfNat.ofNat, True, congr, congrArg, List.map_nil, zero_div, eq_self, Eq.mpr, List.cons, id, List.map_cons, HAdd.hAdd, List.sum_cons, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow and 29 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.codexDenom_pos line 747 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Real, OfNat.ofNat, Imo2026P3.codexDenom
Proof uses: id, HPow.hPow, HAdd.hAdd, one_lt_pow₀, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, lt_of_not_ge, HSub.hSub, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast and 52 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.codexDyadicWeights_pos line 753 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Membership.mem, List, Imo2026P3.codexDyadicWeights, LT.lt, OfNat.ofNat
Proof uses: And, HAdd.hAdd, Eq, HDiv.hDiv, HPow.hPow, Imo2026P3.codexDenom, Exists, Eq.mp, Eq.trans, List.map, List.range, congrArg, funext, congrFun', div_pos, pow_pos, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl and 4 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.codexDyadicWeights_length line 760 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List.length, Real, Imo2026P3.codexDyadicWeights, HAdd.hAdd, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, List.map, HDiv.hDiv, HPow.hPow, Imo2026P3.codexDenom, List.range, List.length_map, List.length_range, eq_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.codexDyadicWeights_ne_nil line 764 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, List, Real, Imo2026P3.codexDyadicWeights, List.nil
Proof uses: Eq, List.length, congrArg, False.elim, False, Eq.mp, HAdd.hAdd, OfNat.ofNat, Eq.trans, And, and_false, Imo2026P3.codexDyadicWeights_length
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.codexDyadicWeights_sum line 770 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, List.sum, Imo2026P3.codexDyadicWeights, OfNat.ofNat
Proof uses: id, Eq.mpr, List.map, HDiv.hDiv, HPow.hPow, Imo2026P3.codexDenom, List.range, HAdd.hAdd, congrArg, List, of_eq_true, Eq.trans, Membership.mem, Function.comp, True, List.map_map, forall_congr, LE.le, implies_congr, LT.lt and 8 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.codexLowerCuts line 779 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Real
Proof uses: Imo2026P3.cutsOfLengths, Imo2026P3.codexDyadicWeights
lemma Imo2026P3.codexLowerCuts_admissible line 782 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2026P3.AdmissibleMark, Imo2026P3.codexLowerCuts
Proof uses: Imo2026P3.admissible_cutsOfLengths, Imo2026P3.codexDyadicWeights, Imo2026P3.codexDyadicWeights_ne_nil, Imo2026P3.codexDyadicWeights_pos, Imo2026P3.codexDyadicWeights_sum, Eq.mpr, LE.le, List.length, Real, HAdd.hAdd, OfNat.ofNat, id, Eq, congrArg, Imo2026P3.codexDyadicWeights_length, le_refl
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.codexLowerCuts_pieces line 787 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List, Real, Imo2026P3.pieceLengths, Imo2026P3.codexLowerCuts, Imo2026P3.codexDyadicWeights
Proof uses: Imo2026P3.pieceLengths_cutsOfLengths, Imo2026P3.codexDyadicWeights_ne_nil, Imo2026P3.codexDyadicWeights_pos, Imo2026P3.codexDyadicWeights_sum

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.CodexMod3.incidence line 798 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, LinearMap, ZMod, OfNat.ofNat, Nat, RingHom.id
Proof uses: LinearMap.mk, AddHom.mk, HAdd.hAdd
30 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.CodexMod3.exists_mod3_kernel line 810 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, LT.lt, Nat, Fintype.card, Exists, ZMod, OfNat.ofNat, And, Ne, Eq, HAdd.hAdd
Proof uses: LinearMap, RingHom.id, Imo2026P3.CodexMod3.incidence, Module.finrank, Eq.mpr, id, congr, congrArg, Module.finrank_pi, Submodule, LinearMap.ker, Bot.bot, LinearMap.ker_ne_bot_of_finrank_lt, Membership.mem, Submodule.exists_mem_ne_zero_of_ne_bot, Exists.intro, And.intro, Iff.mp, LinearMap.mem_ker, congrFun
57 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.CodexMod3.sign3 line 826 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Real
Proof uses: ite, Eq, Neg.neg
20 instances, coercions and auxiliary constants left out.
theorem Imo2026P3.CodexMod3.sign3_cases line 829 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Or, Eq, Real, Imo2026P3.CodexMod3.sign3, Neg.neg
Proof uses: dite, of_eq_true, Eq.trans, True, False, congr, congrArg, congrFun', ite_eq_left_of_eq_true, ite, eq_self, or_self, or_false, Not, ite_eq_right_of_eq_false, true_or, or_true, eq_false
47 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.CodexMod3.sign3_ne_zero line 836 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Ne, Real, Imo2026P3.CodexMod3.sign3
Proof uses: Eq.mpr, ite, Eq, Neg.neg, id, congrFun', congrArg, Eq.trans, False, ite_congr, eq_false, Eq.refl, Not, ite_false, Decidable, ite_eq_right, Mathlib.Meta.NormNum.isInt_eq_false, Int.negOfNat, Int.ofNat, Mathlib.Meta.NormNum.isInt_neg and 9 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.CodexMod3.zmod3_cases line 840 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Or, Eq, Neg.neg
Proof uses: List, List.Mem, Fin, HAdd.hAdd, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Or.inl, rfl, eq_of_heq, List.Mem.tail and 14 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.CodexMod3.sign3_add_eq_zero line 850 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, HAdd.hAdd, Real, Imo2026P3.CodexMod3.sign3
Proof uses: Neg.neg, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, HSub.hSub, Mathlib.Tactic.Ring.Common.sub_congr, HMul.hMul, HPow.hPow, Nat.rawCast, 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_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero and 46 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.CodexMod3.exists_real_signing line 861 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, LT.lt, Nat, Fintype.card, Exists, Real, And, Or, Eq, OfNat.ofNat, Neg.neg, Ne, HAdd.hAdd
Proof uses: ZMod, Imo2026P3.CodexMod3.exists_mod3_kernel, Decidable.byContradiction, Not, funext, Eq.mp, Eq.trans, binderNameHint, forall_congr, Exists.intro, Imo2026P3.CodexMod3.sign3, And.intro, Imo2026P3.CodexMod3.sign3_cases, Imo2026P3.CodexMod3.sign3_ne_zero, Imo2026P3.CodexMod3.sign3_add_eq_zero
34 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.CodexMod3.exists_signed_edge_bound line 879 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Real, LT.lt, Nat, Fintype.card, Eq, Finset.sum, Finset.univ, HMul.hMul, HAdd.hAdd, Exists, And, Or, OfNat.ofNat, Neg.neg, Ne, LE.le, abs, HSub.hSub
Proof uses: Imo2026P3.CodexMod3.exists_real_signing, Exists.intro, And.intro, Eq.mpr, id, congrArg, Trans.trans, Lattice, AddGroup, Eq.rec, Eq.refl, Finset.sum_congr, rfl, Finset, Membership.mem, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq and 61 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.pairUp line 914 source
standard axioms: propext what this means
Statement uses: List, Prod
2 instances, coercions and auxiliary constants left out.
def Imo2026P3.unpaired line 918 source
no axioms what this means
Statement uses: List, Option
2 instances, coercions and auxiliary constants left out.
def Imo2026P3.unpair line 923 source
no axioms what this means
Statement uses: List, Prod
2 instances, coercions and auxiliary constants left out.
theorem Imo2026P3.unpair_pairUp_append_unpaired line 927 source
standard axioms: propext what this means
Statement uses: List, Eq, HAppend.hAppend, Imo2026P3.unpair, Imo2026P3.pairUp, Option.toList, Imo2026P3.unpaired
Proof uses: Imo2026P3.pairUp.induct, of_eq_true, List.cons, Eq.trans, True, congrFun', congrArg, Imo2026P3.unpair.eq_2, eq_self, False, List.nil, Imo2026P3.unpair.eq_1, List.append_nil, Eq.symm, False.elim, rfl, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.length_pairUp line 940 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Eq, Nat, List.length, Prod, Imo2026P3.pairUp, HDiv.hDiv, OfNat.ofNat
Proof uses: Imo2026P3.pairUp.induct, Eq.mpr, List.cons, HAdd.hAdd, id, congrFun', congrArg, False, List.nil, of_eq_true, Eq.trans, True, Nat.zero_div, eq_self, Eq.symm, zero_add, False.elim, rfl, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.unpaired_isSome_iff line 954 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Iff, Eq, Bool, Option.isSome, Imo2026P3.unpaired, Bool.true, Nat, HMod.hMod, List.length, OfNat.ofNat
Proof uses: Imo2026P3.pairUp.induct, Eq.mpr, List.cons, id, congrArg, Option, Imo2026P3.unpaired.eq_3, propext, False, List.nil, of_eq_true, Eq.trans, True, congr, Bool.false_eq_true, iff_self, Eq.symm, eq_self, congrFun', zero_add and 4 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.pairUp_sum line 970 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, List, Eq, List.sum, List.map, HAdd.hAdd, Prod, Prod.fst, Prod.snd, Imo2026P3.pairUp, Option.elim, Imo2026P3.unpaired, OfNat.ofNat
Proof uses: Imo2026P3.pairUp.induct, Eq.mpr, List.cons, id, congr, congrArg, Eq.trans, List.map_cons, congrFun', List.sum_map_add, Prod.mk, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm and 12 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.surplus_eq_pairUp line 984 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Imo2026P3.surplus, HAdd.hAdd, List.sum, List.map, Prod, HSub.hSub, Prod.fst, Prod.snd, Imo2026P3.pairUp, Option.getD, Imo2026P3.unpaired, OfNat.ofNat
Proof uses: Imo2026P3.pairUp.induct, Eq.mpr, List.cons, id, congr, congrArg, congrFun', List.map_cons, Prod.mk, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.sub_congr and 27 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.pairUp_rel line 998 source
standard axioms: Quot.sound, propext what this means
Statement uses: List, List.Pairwise, Prod, Membership.mem, Imo2026P3.pairUp, Prod.fst, Prod.snd
Proof uses: Imo2026P3.pairUp.induct, List.cons, Eq.mpr, Or, Eq, Prod.mk, id, forall_congr, implies_congr, Eq.refl, And.left, Eq.mp, And, congrArg, propext, List.pairwise_cons, of_eq_true, Eq.trans, True, congrFun' and 10 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.pairUp_map line 1015 source
standard axioms: propext what this means
Statement uses: List, Eq, Prod, Imo2026P3.pairUp, List.map, Prod.mk, Prod.fst, Prod.snd
Proof uses: Imo2026P3.pairUp.induct, of_eq_true, List.cons, Eq.trans, True, congr, congrArg, List.map_cons, Imo2026P3.pairUp.eq_1, eq_self, False, List.nil, List.map_nil, Imo2026P3.pairUp.eq_2, False.elim, noConfusion_of_Nat, List.ctorIdx, Eq.symm, HEq, eq_of_heq and 2 more
3 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.unpaired_map line 1028 source
standard axioms: propext what this means
Statement uses: List, Eq, Option, Imo2026P3.unpaired, List.map, Option.map
Proof uses: Imo2026P3.pairUp.induct, Eq.mpr, List.cons, id, congrFun', congrArg, Eq.trans, List.map_cons, Imo2026P3.unpaired.eq_3, False, List.nil, of_eq_true, Option.none, True, List.map_nil, Imo2026P3.unpaired.eq_1, eq_self, Eq.symm, Option.some, Imo2026P3.unpaired.eq_2 and 3 more
2 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.mem_of_unpaired_eq_some line 1041 source
standard axioms: propext what this means
Statement uses: List, Eq, Option, Imo2026P3.unpaired, Option.some, Membership.mem
Proof uses: Imo2026P3.pairUp.induct, List.cons, List.mem_cons_of_mem, False, List.nil, of_eq_true, Option.none, Eq.trans, True, implies_congr, eq_false', False.elim, noConfusion_of_Nat, Option.ctorIdx, Eq.symm, Or, congrFun', congrArg, Eq.mp, Option.some.injEq and 5 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.labelWeight line 1059 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Prod, Real
Proof uses: List.sum, List.map, Prod.fst, List.filter, Decidable.decide, Eq, Prod.snd
2 instances, coercions and auxiliary constants left out.
theorem Imo2026P3.labelWeight_cons line 1062 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Prod, Real, List, Eq, Imo2026P3.labelWeight, List.cons, HAdd.hAdd, ite, Prod.snd, Prod.fst, OfNat.ofNat
Proof uses: dite, of_eq_true, Eq.trans, List.sum, List.map, List.filter, Decidable.decide, True, congr, congrArg, List.filter_cons_of_pos, Bool, Bool.true, congrFun', Decidable.decide.congr_simp, eq_self, decide_true, List.map_cons, ite_eq_left_of_eq_true, Not and 9 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.labelWeight_perm line 1067 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Prod, Real, List.Perm, Eq, Imo2026P3.labelWeight
Proof uses: id, List.Perm.sum_eq, List.map, Prod.fst, List.filter, Decidable.decide, Prod.snd, List.Perm.map, List.Perm.filter
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.labelWeight_scale line 1072 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Real, List, Prod, Eq, Imo2026P3.labelWeight, List.map, Prod.mk, HMul.hMul, Prod.fst, Prod.snd
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, forall_congr, OfNat.ofNat, congr, congrArg, List.filter, Decidable.decide, List.sum, List.map_nil, MulZeroClass.mul_zero, eq_self, implies_true, Eq.mpr, List.cons, id, List.map_cons and 32 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.surplus_scale line 1083 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, List, Eq, Imo2026P3.surplus, List.map, HMul.hMul
Proof uses: Imo2026P3.surplus.induct, of_eq_true, List.nil, Eq.trans, OfNat.ofNat, True, congr, congrArg, List.map_nil, Imo2026P3.surplus.eq_1, MulZeroClass.mul_zero, eq_self, List.cons, congrFun', List.map_cons, Imo2026P3.surplus.eq_2, Eq.mpr, HAdd.hAdd, HSub.hSub, id and 40 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.sum_sign_labelWeight line 1091 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Real, List, Prod, Eq, Finset.sum, Finset.univ, HMul.hMul, Imo2026P3.labelWeight, List.sum, List.map, Prod.snd, Prod.fst
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, OfNat.ofNat, True, congr, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, List.filter, Decidable.decide, List.map_nil, MulZeroClass.mul_zero, Finset.sum_const_zero, eq_self, Trans.trans, List.cons and 18 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.fin_sum_get_map line 1117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, List, Eq, Finset.sum, Fin, List.length, Finset.univ, List.get, List.sum, List.map
Proof uses: Eq.mpr, List.ofFn, id, congrArg, Eq.symm, List.sum_ofFn, List.ofFn_getElem_eq_map
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.sum_sign_weight_pairUp line 1123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Real, List, Prod, Eq, Finset.sum, Finset.univ, HMul.hMul, Imo2026P3.labelWeight, HAdd.hAdd, List.sum, List.map, Prod.snd, Prod.fst, Imo2026P3.pairUp, Option.elim, Imo2026P3.unpaired, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Imo2026P3.sum_sign_labelWeight, Imo2026P3.pairUp_sum
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.abstract_even_lower line 1132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nat, Function.Injective, List, Prod, Real, List.Pairwise, GE.ge, Prod.fst, Eq, Option, Imo2026P3.unpaired, Option.none, LT.lt, List.length, HMul.hMul, OfNat.ofNat, Fintype.card, Imo2026P3.labelWeight and 4 more
Proof uses: Imo2026P3.pairUp, Fin, Prod.snd, List.get, Eq.mpr, id, congrFun', congrArg, Fintype.card_fin, HDiv.hDiv, Imo2026P3.length_pairUp, Finset.sum, Finset.univ, HAdd.hAdd, List.sum, Option.elim, Imo2026P3.sum_sign_weight_pairUp, Trans.trans, List.sum_map_add, Eq.mp and 37 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.abstract_lower line 1193 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nat, Function.Injective, List, Prod, Real, List.Pairwise, GE.ge, Prod.fst, Membership.mem, LE.le, OfNat.ofNat, LT.lt, List.length, HMul.hMul, Fintype.card, Eq, Imo2026P3.labelWeight, HPow.hPow and 2 more
Proof uses: Imo2026P3.pairUp, Fin, Prod.snd, List.get, Eq.mpr, id, congrFun', congrArg, Fintype.card_fin, HDiv.hDiv, Imo2026P3.length_pairUp, And, Or, Neg.neg, Exists, Ne, HAdd.hAdd, Imo2026P3.CodexMod3.exists_real_signing, Option.elim, Imo2026P3.unpaired and 108 more
133 instances, coercions and auxiliary constants left out.

Tactic trace: 75 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.sort_sublist_sort_of_subset line 1294 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, LE.le, List.Sublist, Finset.sort
Proof uses: List.sublist_of_subperm_of_sortedLE, List.subperm_of_subset, Finset.sort_nodup, Membership.mem, List, Eq.mpr, id, Eq, congrArg, propext, Finset.mem_sort, Eq.mp, List.Pairwise.sortedLE, Finset.pairwise_sort
23 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.taggedBlocks line 1304 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, List, Real, Prod
Proof uses: List.flatMap, List.map, Prod.mk, List.finRange
lemma Imo2026P3.labelWeight_append line 1307 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Prod, Real, Eq, Imo2026P3.labelWeight, HAppend.hAppend, HAdd.hAdd
Proof uses: of_eq_true, List.sum, List.map, Prod.fst, List.filter, Decidable.decide, Prod.snd, Eq.trans, True, congrFun', congrArg, List.filter_append, List.map_append, List.sum_append, OfNat.ofNat, 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 Imo2026P3.labelWeight_same_block line 1311 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Real, Eq, Imo2026P3.labelWeight, List.map, Prod, Prod.mk, ite, List.sum, OfNat.ofNat
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, Prod.fst, List.filter, Decidable.decide, Prod.snd, List.map_nil, ite_self, eq_self, Eq.mpr, List.cons, id, List.map_cons, HAdd.hAdd, Imo2026P3.labelWeight_cons and 8 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.labelWeight_flatMap_blocks line 1319 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Real, Eq, Imo2026P3.labelWeight, List.flatMap, Prod, List.map, Prod.mk, List.sum, ite, OfNat.ofNat
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, Prod.fst, List.filter, Decidable.decide, Prod.snd, List.flatMap_nil, List.map_nil, eq_self, Eq.mpr, List.cons, HAppend.hAppend, id, List.flatMap_cons, HAdd.hAdd and 5 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.labelWeight_taggedBlocks line 1329 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, List, Real, Eq, Imo2026P3.labelWeight, Imo2026P3.taggedBlocks, List.sum
Proof uses: Eq.mpr, List.flatMap, Prod, List.map, Prod.mk, List.finRange, id, congrArg, Imo2026P3.taggedBlocks.eq_1, ite, OfNat.ofNat, Imo2026P3.labelWeight_flatMap_blocks, Finset.sum, List.toFinset, Eq.symm, List.sum_toFinset, List.nodup_finRange, of_eq_true, Eq.trans, True and 10 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.intervalBlock line 1335 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Fin, List
Proof uses: List.map, HSub.hSub, HAdd.hAdd, OfNat.ofNat, List.range'
7 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.intervalBlock_sum line 1338 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Fin, LE.le, HAdd.hAdd, OfNat.ofNat, Eq, List.sum, Imo2026P3.intervalBlock, HSub.hSub
Proof uses: id, Eq.mpr, List.map, List.range', Finset.sum, List.toFinset, congrArg, Eq.symm, List.sum_toFinset, List.nodup_range', of_eq_true, LT.lt, optParam, Eq.trans, True, eq_self, Finset.Ico, Finset, List.toFinset_range'_1, Nat.add_sub_of_le and 1 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.blockIndices line 1346 source
no axioms what this means
Statement uses: Nat, List
Proof uses: List.flatMap, List.range', HSub.hSub, HAdd.hAdd, OfNat.ofNat, List.range
5 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.blockIndices_eq_range' line 1349 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Monotone, Eq, List, Imo2026P3.blockIndices, List.range', OfNat.ofNat, HSub.hSub
Proof uses: Nat.recAux, of_eq_true, Eq.trans, List.nil, True, congr, congrArg, List.flatMap_nil, HAdd.hAdd, congrFun', optParam, tsub_self, List.range'_zero, eq_self, Eq.mpr, List.flatMap, List.range, id, Imo2026P3.blockIndices.eq_1, HAppend.hAppend and 13 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.map_fst_tagged_intervalBlocks line 1372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Monotone, Eq, List, List.map, Prod, Fin, Prod.fst, Imo2026P3.taggedBlocks, Imo2026P3.intervalBlock, HSub.hSub, HAdd.hAdd, OfNat.ofNat, List.range'
Proof uses: id, List.flatMap, Prod.mk, List.finRange, Eq.mpr, congrArg, List.map_flatMap, Function.comp, congrFun', funext, Eq.trans, List.map_map, List.flatMap_map, Eq.refl, List.range, List.map_coe_finRange_eq_range, Eq.symm, Imo2026P3.blockIndices, Imo2026P3.blockIndices_eq_range'
15 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.indexedDiffs line 1394 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real
Proof uses: List.map, Nat, HSub.hSub, List.getD, HAdd.hAdd, OfNat.ofNat, List.range, List.length
8 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.indexedDiffs_getD line 1397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Nat, LT.lt, HSub.hSub, List.length, OfNat.ofNat, Eq, List.getD, Imo2026P3.indexedDiffs, HAdd.hAdd
Proof uses: of_eq_true, Eq.trans, True, congrArg, List.range, List.map, Option.getD, GetElem?.getElem?, congrFun', funext, congr, List.getD_eq_getElem?_getD, List.length_map, List.length_range, eq_true, Eq.mpr, GetElem.getElem, id, List.getD_eq_getElem, Eq.rec and 6 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.zipWith_tail_diff_eq_indexedDiffs line 1403 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, List.zipWith, HSub.hSub, List.tail, Imo2026P3.indexedDiffs
Proof uses: List.ext_getElem, of_eq_true, Nat, List.length, Eq.trans, OfNat.ofNat, True, congr, congrArg, Min.min, List.length_zipWith, List.length_tail, inf_of_le_right, LE.le, HAdd.hAdd, List.range, List.map, Option.getD, GetElem?.getElem?, LT.lt and 20 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.boundaryPoints line 1412 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, List
Proof uses: HAppend.hAppend, List.cons, OfNat.ofNat, Finset.sort, LE.le, List.nil
13 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.boundaryPoints_length line 1415 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, Eq, Nat, List.length, Imo2026P3.boundaryPoints, HAdd.hAdd, Finset.card, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HAppend.hAppend, List, Finset.sort, LE.le, List.cons, List.nil, List.length_append, congr, Finset.length_sort, zero_add, eq_self
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.boundaryPoints_pairwise line 1419 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, LE.le, Set, Set.Ioo, OfNat.ofNat, List.Pairwise, LT.lt, Imo2026P3.boundaryPoints
Proof uses: id, Eq.mpr, HAppend.hAppend, List, List.cons, Finset.sort, List.nil, And, Membership.mem, Eq, congrArg, propext, List.pairwise_append, List.pairwise_cons, And.intro, And.left, Iff.mp, Finset.mem_sort, List.SortedLT.pairwise, Finset.sortedLT_sort and 22 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.boundaryPoints_sublist line 1434 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, LE.le, List.Sublist, Imo2026P3.boundaryPoints
Proof uses: id, List.Sublist.cons_cons, HAppend.hAppend, List, Finset.sort, List.cons, OfNat.ofNat, List.nil, List.Sublist.append, Imo2026P3.sort_sublist_sort_of_subset, List.Sublist.refl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.pieceLengths_eq_indexedDiffs_boundaryPoints line 1439 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, Eq, List, Imo2026P3.pieceLengths, Imo2026P3.indexedDiffs, Imo2026P3.boundaryPoints
Proof uses: id, HAppend.hAppend, List.cons, OfNat.ofNat, Finset.sort, LE.le, List.nil, List.zipWith, HSub.hSub, List.tail, Imo2026P3.zipWith_tail_diff_eq_indexedDiffs
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.clippedEmbedding line 1444 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OrderEmbedding, Fin, HAdd.hAdd, OfNat.ofNat
Proof uses: Fin.mk, Min.min
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.clippedEmbedding_mono line 1447 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OrderEmbedding, Fin, HAdd.hAdd, OfNat.ofNat, Monotone, Imo2026P3.clippedEmbedding
Proof uses: LE.le, OrderEmbedding.monotone, Fin.mk, Min.min, Eq.mpr, id, Eq
18 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.clippedEmbedding_of_le line 1454 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OrderEmbedding, Fin, HAdd.hAdd, OfNat.ofNat, LE.le, Eq, Imo2026P3.clippedEmbedding, Fin.mk
Proof uses: of_eq_true, Eq.trans, Min.min, LT.lt, Nat.min_eq_left, True, congrFun', congrArg, Fin.mk.congr_simp, eq_self
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.exists_tagged_piece_refinement line 1459 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, LE.le, Set, Set.Ioo, OfNat.ofNat, Exists, List, Prod, Fin, HAdd.hAdd, Nat, Finset.card, And, Eq, List.map, Prod.fst, Imo2026P3.pieceLengths, Imo2026P3.labelWeight, List.getD
Proof uses: Imo2026P3.boundaryPoints, List.length, Imo2026P3.boundaryPoints_length, List.Sublist, Imo2026P3.boundaryPoints_sublist, OrderEmbedding, List.get, Eq.mp, congrArg, propext, List.sublist_iff_exists_fin_orderEmbedding_get_eq, RelEmbedding.trans, OrderIso.toOrderEmbedding, Fin.castOrderIso, Eq.symm, LT.lt, Eq.mpr, id, Fin.isLt, GetElem.getElem and 67 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 140 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.codexLowerCuts_card line 1575 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Real, Imo2026P3.codexLowerCuts
Proof uses: HAdd.hAdd, Imo2026P3.cutsOfLengths, Imo2026P3.codexDyadicWeights, OfNat.ofNat, List.length, Imo2026P3.card_cutsOfLengths, Imo2026P3.codexDyadicWeights_ne_nil, Imo2026P3.codexDyadicWeights_pos, Eq.mpr, id, Eq.mp, Eq.trans, congrArg, Imo2026P3.codexDyadicWeights_length
5 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.codexLowerCuts_piece_getD line 1582 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Eq, Real, List.getD, Imo2026P3.pieceLengths, Imo2026P3.codexLowerCuts, HDiv.hDiv, HPow.hPow, Imo2026P3.codexDenom
Proof uses: Eq.mpr, Imo2026P3.codexDyadicWeights, id, congrArg, List, Imo2026P3.codexLowerCuts_pieces, LT.lt, List.length, Imo2026P3.codexDyadicWeights_length, Fin.isLt, GetElem.getElem, List.getD_eq_getElem, of_eq_true, Eq.trans, True, congrFun', List.map, List.range, Eq.refl, Eq.rec and 4 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.codex_lower_bound_complete line 1592 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, Finset, Real, And, Imo2026P3.AdmissibleMark, Disjoint, LE.le, HDiv.hDiv, HPow.hPow, HSub.hSub, HAdd.hAdd, Imo2026P3.L
Proof uses: Imo2026P3.codexLowerCuts, Exists.intro, And.intro, Imo2026P3.codexLowerCuts_admissible, Union.union, Set, Set.Ioo, id, Eq.mpr, Eq, congrArg, Finset.coe_union, Set.union_subset, And.left, Finset.card, List, Prod, Fin, List.map, Prod.fst and 178 more
191 instances, coercions and auxiliary constants left out.

Tactic trace: 80 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.bisectLengths line 1689 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real
Proof uses: Imo2026P3.pairDup, List.map, HDiv.hDiv, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.bisectLengths_cons line 1692 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, List, Eq, Imo2026P3.bisectLengths, List.cons, HDiv.hDiv, OfNat.ofNat, Nat
Proof uses: rfl
8 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.bisectLengths_pos line 1695 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LT.lt, OfNat.ofNat, Imo2026P3.bisectLengths
Proof uses: And, Exists, Eq, HDiv.hDiv, List.cons, List.nil, Eq.mp, Eq.trans, List.flatMap, List.map, congrArg, funext, congrFun', Nat, Or, False, or_false, or_self, div_pos, Mathlib.Meta.NormNum.isNat_lt_true and 7 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.bisectLengths_sum line 1704 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, List.sum, Imo2026P3.bisectLengths
Proof uses: List.rec, of_eq_true, List.nil, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, List.flatMap, List.cons, List.map, HDiv.hDiv, List.map_nil, List.flatMap_nil, eq_self, Eq.mpr, Nat, id, Imo2026P3.bisectLengths_cons, HAdd.hAdd and 40 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.sum_map_half line 1711 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, List.sum, List.map, HDiv.hDiv, OfNat.ofNat, Nat
Proof uses: Imo2026P3.codex_sum_map_div
15 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.bisectLengths_length line 1714 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Nat, List.length, Imo2026P3.bisectLengths, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, Imo2026P3.pairDup, List.map, HDiv.hDiv, id, congrArg, Imo2026P3.bisectLengths.eq_1, Imo2026P3.length_pairDup, List.length_map, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.scanl_mem_bisectLengths line 1718 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, List.scanl, HAdd.hAdd, Imo2026P3.bisectLengths
Proof uses: List.rec, List.nil, Eq.mpr, Eq, id, Eq.trans, Or, List.cons, congrFun', congrArg, List.flatMap, List.map, HDiv.hDiv, OfNat.ofNat, List.map_nil, List.flatMap_nil, List.scanl_nil, False, or_false, Eq.mp and 50 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.mem_interiorPartialSums_of_mem_scanl_Ioo line 1732 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, List.scanl, HAdd.hAdd, Set, Set.Ioo, Imo2026P3.interiorPartialSums
Proof uses: List.cons, Or, Iff.mp, HAppend.hAppend, List.mem_append, Eq.mp, congrArg, Eq.symm, Imo2026P3.boundaryList_eq_scanl, List.mem_cons, False.elim, lt_irrefl, And.left, Eq.trans, False, or_false, And.right
27 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.cutsOfLengths_subset_bisectLengths line 1745 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, LE.le, Finset, Imo2026P3.cutsOfLengths, Imo2026P3.bisectLengths
Proof uses: Imo2026P3.interiorPartialSums, Eq.mp, Set, Set.Ioo, Imo2026P3.mem_interiorPartialSums_Ioo, List.tail, List.scanl, HAdd.hAdd, List.mem_of_mem_dropLast, List.mem_of_mem_tail, Imo2026P3.bisectLengths_pos, congrArg, False.elim, False, Imo2026P3.bisectLengths_sum, Eq.mpr, id, Eq.refl, Imo2026P3.scanl_mem_bisectLengths, Imo2026P3.mem_interiorPartialSums_of_mem_scanl_Ioo
35 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.firstPlayerShare_bisectLengths line 1766 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Imo2026P3.firstPlayerShare, Imo2026P3.bisectLengths, HDiv.hDiv, List.sum, OfNat.ofNat, Nat
Proof uses: List.map, List.mergeSort, Decidable.decide, GE.ge, List.Perm, List.Perm.symm, List.mergeSort_perm, Imo2026P3.pairDup, id, List.Perm.flatMap_right, List.cons, List.nil, Trans.trans, Imo2026P3.firstPlayerShare_congr, Imo2026P3.firstPlayerShare_pairDup_of_pairwise, List.pairwise_mergeSort', Eq.symm, List.Perm.sum_eq, Imo2026P3.sum_map_half
33 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.exists_bisect_reply line 1785 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Real, Imo2026P3.AdmissibleMark, LT.lt, Finset.card, Exists, And, Disjoint, Eq, Imo2026P3.L, HDiv.hDiv, OfNat.ofNat
Proof uses: List, Imo2026P3.pieceLengths, Ne, List.nil, List.length, congrArg, False.elim, False, Eq.mp, HAdd.hAdd, Eq.trans, EmptyCollection.emptyCollection, congr, and_false, Imo2026P3.pieceLengths_length, Membership.mem, Imo2026P3.pieceLengths_pos, And.left, LE.le, Set and 17 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.CodexClosePoints.zip_tail_rel line 1819 source
theorem Imo2026P3.CodexClosePoints.zip_tail_sum line 1833 source
theorem Imo2026P3.CodexClosePoints.exists_close_pair_of_finite line 1852 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Real, LE.le, Nat, OfNat.ofNat, Fintype.card, Exists, And, Ne, abs, HSub.hSub, HDiv.hDiv
Proof uses: dite, Function.Injective, LinearOrder, LinearOrder.lift', List, Finset.sort, Finset.univ, Eq, List.length, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.length_sort, DecidableRel, IsTrans, Eq.refl, Std.Antisymm, Std.Total and 141 more
192 instances, coercions and auxiliary constants left out.

Tactic trace: 74 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.CodexClosePoints.exists_disjoint_subset_sums_close line 1933 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Real, LE.le, Eq, Finset.sum, Finset.univ, Exists, Finset, And, Disjoint, Finset.Nonempty, Union.union, HSub.hSub, HDiv.hDiv, HPow.hPow
Proof uses: Fintype.card, Eq.mpr, id, congrArg, Eq.trans, Fintype.card_finset, Fintype.card_fin, Nat.le_pow, Finset.sum_nonneg, Membership.mem, Eq.symm, Finset.sum_le_univ_sum_of_nonneg, Ne, abs, Imo2026P3.CodexClosePoints.exists_close_pair_of_finite, Eq.mp, congrFun', Nat.cast_pow, SDiff.sdiff, disjoint_sdiff_sdiff and 96 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.subperm_perm_of_length_eq line 1986 source
standard axioms: propext what this means
Statement uses: List, List.Subperm, Eq, Nat, List.length, List.Perm
Proof uses: And, List.Sublist, Exists, Eq.mp, congrArg, propext, List.subperm_iff, Eq.mpr, id, List.Perm.length_eq, Eq.refl, List.Sublist.eq_of_length, congrFun'
2 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.finBlocks line 1999 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, List, Real
Proof uses: List.map, List.finRange
def Imo2026P3.flattenFinBlocks line 2002 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, List, Real
Proof uses: List.flatten, Imo2026P3.finBlocks
lemma Imo2026P3.map_fst_taggedBlocks_eq_flattenFinBlocks line 2005 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, List, Real, Eq, List.map, Prod, Prod.fst, Imo2026P3.taggedBlocks, Imo2026P3.flattenFinBlocks
Proof uses: id, List.flatMap, Prod.mk, List.finRange, List.flatten, Imo2026P3.finBlocks, Eq.mpr, congrArg, List.map_flatMap, List.flatMap_congr, Membership.mem, Function.comp, List.map_map, of_eq_true, Eq.trans, True, congrFun', congrFun, List.map_id_fun', eq_self
1 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.indexedDiffs_scanl line 2018 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Imo2026P3.indexedDiffs, List.scanl, HAdd.hAdd
Proof uses: Eq.mpr, List.zipWith, HSub.hSub, List.tail, id, congrArg, Eq.symm, Imo2026P3.zipWith_tail_diff_eq_indexedDiffs, Imo2026P3.zipWith_scanl_tail
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.map_sum_finBlocks_eq line 2023 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Fin, List.length, Eq, List.sum, List.get, List.map, Imo2026P3.finBlocks
Proof uses: id, Eq.mpr, List.finRange, Function.comp, congrArg, List.map_map, List.map_congr_left, Membership.mem, List.map_get_finRange
5 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.flattenFinBlocks_sum line 2036 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Fin, List.length, Eq, List.sum, List.get, Imo2026P3.flattenFinBlocks
Proof uses: id, Eq.mpr, List.flatten, Imo2026P3.finBlocks, List.map, congrArg, List.sum_flatten, Imo2026P3.map_sum_finBlocks_eq, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.flattenFinBlocks_pos line 2042 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, List, Real, Membership.mem, LT.lt, OfNat.ofNat, Imo2026P3.flattenFinBlocks
Proof uses: And, Exists, Eq, Eq.mp, Eq.trans, List.flatten, List.map, List.finRange, congrArg, funext, congrFun', True, true_and
14 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.flattenFinBlocks_ne_nil line 2051 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, List, Real, LT.lt, OfNat.ofNat, Ne, List.nil, Imo2026P3.flattenFinBlocks
Proof uses: Eq, Fin.mk, Membership.mem, Imo2026P3.finBlocks, of_eq_true, List.map, List.finRange, Eq.trans, Exists, And, True, congrArg, funext, congrFun', true_and, Iff.mp, List.flatten, List.flatten_eq_nil_iff, Eq.mpr, id and 1 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.scanl_blockSums_mem_flatten line 2062 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, List.scanl, HAdd.hAdd, List.map, List.sum, List.flatten
Proof uses: List.rec, List.nil, Eq.mpr, Eq, id, Eq.trans, Or, List.cons, congrFun', congrArg, List.scanl_nil, False, or_false, Eq.mp, List.map_nil, Iff.mp, List.mem_cons, List.scanl_cons, List.map_cons, HAppend.hAppend and 19 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.scanl_piece_mem_flattenFinBlocks line 2087 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Fin, List.length, Eq, List.sum, List.get, Membership.mem, List.scanl, HAdd.hAdd, OfNat.ofNat, Imo2026P3.flattenFinBlocks
Proof uses: List.map, Imo2026P3.finBlocks, Imo2026P3.map_sum_finBlocks_eq, Imo2026P3.scanl_blockSums_mem_flatten, Eq.mp, congrArg, Eq.symm
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.cutsOfLengths_subset_flattenFinBlocks line 2096 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, Fin, List.length, List.get, LE.le, Finset, Imo2026P3.cutsOfLengths, Imo2026P3.flattenFinBlocks
Proof uses: Imo2026P3.interiorPartialSums, Eq.mp, Set, Set.Ioo, Imo2026P3.mem_interiorPartialSums_Ioo, List.scanl, HAdd.hAdd, List.mem_of_mem_tail, List.mem_of_mem_dropLast, List.tail, Imo2026P3.scanl_piece_mem_flattenFinBlocks, Nat, Iff.mpr, List.length_pos_iff, Imo2026P3.flattenFinBlocks_ne_nil, Imo2026P3.flattenFinBlocks_pos, Eq.mpr, id, congrArg, Imo2026P3.flattenFinBlocks_sum and 2 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.commonAtoms line 2122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real
Proof uses: PSigma.mk
1 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.commonAtoms_spec line 2135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, And, Imo2026P3.commonAtoms, LE.le, Nat, List.length, HSub.hSub, HAdd.hAdd
Proof uses: PSigma.mk, PSigma
17 instances, coercions and auxiliary constants left out.

Tactic trace: 115 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.ScanRefines line 2238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real
Proof uses: Membership.mem, List.scanl, HAdd.hAdd
3 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.ScanRefines.cons_same line 2241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Imo2026P3.ScanRefines, List.cons
Proof uses: Membership.mem, List.scanl, HAdd.hAdd, Eq.mpr, id, Eq, congrArg, List.scanl_cons, Or, Iff.mp, List.mem_cons, Eq.mp, List.mem_cons_self, List.mem_cons_of_mem
5 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.ScanRefines.absorb_left line 2250 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, List, Imo2026P3.ScanRefines, List.cons, HAdd.hAdd
Proof uses: Membership.mem, List.scanl, Eq.mpr, id, Eq, congrArg, List.scanl_cons, Or, Iff.mp, List.mem_cons, Eq.mp, List.mem_cons_self, List.mem_cons_of_mem, congrFun', add_assoc
9 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.commonAtoms_scanRefines line 2263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, And, Imo2026P3.ScanRefines, Imo2026P3.commonAtoms
Proof uses: PSigma.mk, PSigma
11 instances, coercions and auxiliary constants left out.

Tactic trace: 79 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.scanl_sublist_of_scanRefines line 2346 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LT.lt, OfNat.ofNat, Imo2026P3.ScanRefines, List.Sublist, List.scanl, HAdd.hAdd
Proof uses: List.sublist_of_subperm_of_sortedLE, List.subperm_of_subset, List.Pairwise.nodup, Imo2026P3.pairwise_scanl_lt, List.Pairwise.sortedLE, List.Pairwise.imp, LE.le, LT.lt.le
16 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.exists_blocks_of_scanRefines line 2357 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, Imo2026P3.ScanRefines, Exists, Fin, List.length, And, Ne, List.nil, List.get, Imo2026P3.flattenFinBlocks
Proof uses: Nat, List.scanl, HAdd.hAdd, of_eq_true, Eq.trans, True, congrFun', congrArg, List.length_scanl, eq_self, List.Sublist, id, Imo2026P3.scanl_sublist_of_scanRefines, OrderEmbedding, Eq.mp, propext, List.sublist_iff_exists_fin_orderEmbedding_get_eq, RelEmbedding.trans, LE.le, OrderIso.toOrderEmbedding and 80 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 173 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.selectedList line 2497 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length
Proof uses: List.map, List.get, Finset.sort, LE.le
5 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.selectedList_length line 2500 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Eq, Nat, Imo2026P3.selectedList, Finset.card
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, List.map, List.get, Finset.sort, LE.le, List.length_map, Finset.length_sort, eq_self
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.selectedList_pos line 2504 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Membership.mem, LT.lt, OfNat.ofNat, Imo2026P3.selectedList
Proof uses: And, Finset.sort, LE.le, Eq, List.get, Exists, Eq.mp, List.get_mem
17 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.selectedList_sum line 2512 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Eq, List.sum, Imo2026P3.selectedList, Finset.sum, List.get
Proof uses: id, Eq.mpr, List.map, Finset.sort, LE.le, List.toFinset, congrArg, Eq.symm, List.sum_toFinset, Finset.sort_nodup, of_eq_true, Eq.trans, GetElem.getElem, Nat, LT.lt, Fin.isLt, True, congr, Finset.sum_congr, Finset.sort_toFinset and 3 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.selectedIndex line 2518 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Membership.mem, Imo2026P3.selectedList
Proof uses: Fin.cast, Finset.card, OrderIso, Subtype, OrderIso.symm, Finset.orderIsoOfFin, Subtype.mk
17 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.selectedList_get_orderEmb line 2523 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Finset.card, Eq, List.get, Imo2026P3.selectedList, Fin.cast, Eq.symm, Nat, Imo2026P3.selectedList_length, OrderEmbedding, Finset.orderEmbOfFin, rfl
Proof uses: id, Eq.mpr, List.map, Finset.sort, LE.le, GetElem.getElem, LT.lt, Fin.isLt, congrArg, List.get_eq_getElem, Eq.rec, List.length_map, congrFun', List.getElem_map, Fin.ext, Eq.refl
27 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.selectedList_get_selectedIndex line 2534 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Membership.mem, Eq, List.get, Imo2026P3.selectedList, Imo2026P3.selectedIndex
Proof uses: id, Eq.mpr, Fin.cast, Finset.card, OrderIso, Subtype, OrderIso.symm, Finset.orderIsoOfFin, Subtype.mk, OrderEmbedding, Finset.orderEmbOfFin, rfl, Nat, congrArg, Eq.symm, Imo2026P3.selectedList_length, Imo2026P3.selectedList_get_orderEmb, Fin.ext, OrderIso.apply_symm_apply, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.selectedIndex_orderEmb line 2544 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Finset.card, Eq, Imo2026P3.selectedList, Imo2026P3.selectedIndex, OrderEmbedding, Finset.orderEmbOfFin, rfl, Nat, Finset.orderEmbOfFin_mem, Fin.cast, Eq.symm, Imo2026P3.selectedList_length
Proof uses: id, Fin.ext, OrderIso, Subtype, Membership.mem, OrderIso.symm, Finset.orderIsoOfFin, Subtype.mk, Eq.mpr, congrArg, OrderIso.symm_apply_apply, 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 Imo2026P3.sort_eq_ofFn_orderEmb line 2553 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Eq, List, Finset.sort, LE.le, List.ofFn, Finset.card, OrderEmbedding, Finset.orderEmbOfFin, rfl
Proof uses: List.ext_getElem, of_eq_true, List.length, Eq.trans, True, congr, congrArg, Finset.length_sort, List.length_ofFn, eq_self, LT.lt, Eq.mpr, GetElem.getElem, Fin.mk, id, List.getElem_ofFn, Eq.symm, Eq.mp, Finset.orderEmbOfFin_apply
37 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.selectedBlockAt line 2561 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Imo2026P3.selectedList
Proof uses: dite, Membership.mem, Imo2026P3.selectedIndex, Not, List.nil
4 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.flatMap_sort_selectedBlockAt line 2566 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Imo2026P3.selectedList, Eq, List.flatMap, Imo2026P3.selectedBlockAt, Finset.sort, LE.le, Imo2026P3.flattenFinBlocks
Proof uses: Eq.mpr, List.ofFn, Finset.card, OrderEmbedding, Finset.orderEmbOfFin, rfl, Nat, id, congrArg, Imo2026P3.sort_eq_ofFn_orderEmb, List.flatten, List.map, Imo2026P3.finBlocks, List.finRange, Eq.symm, List.ofFn_eq_map, Fin.cast, Imo2026P3.selectedList_length, List.ofFn_comp', propext and 17 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.halfBlockAt line 2584 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Fin, List.length
Proof uses: List.cons, HDiv.hDiv, List.get, OfNat.ofNat, List.nil
6 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.flatMap_sort_halfBlockAt line 2587 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Eq, List.flatMap, Imo2026P3.halfBlockAt, Finset.sort, LE.le, Imo2026P3.bisectLengths, Imo2026P3.selectedList
Proof uses: id, List.rec, List.map, List.get, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, List.flatMap_nil, List.cons, HDiv.hDiv, OfNat.ofNat, List.map_nil, eq_self, GetElem.getElem, Nat, LT.lt, Fin.isLt and 5 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.assembleSelectedBlocks line 2596 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Imo2026P3.selectedList
Proof uses: dite, Membership.mem, Imo2026P3.selectedIndex, Not, List.cons, HDiv.hDiv, List.get, OfNat.ofNat, List.nil
10 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.assembleSelectedBlocks_ne_nil line 2603 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Imo2026P3.selectedList, Ne, List.nil, Imo2026P3.assembleSelectedBlocks
Proof uses: dite, Membership.mem, Eq.mpr, Not, Eq, Imo2026P3.selectedIndex, of_eq_true, eq_true, id, congrFun', congrArg, dite_eq_left_of_eq_true, List.cons, HDiv.hDiv, List.get, OfNat.ofNat, Eq.trans, GetElem.getElem, Nat, LT.lt and 10 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.assembleSelectedBlocks_pos line 2613 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Imo2026P3.selectedList, Membership.mem, LT.lt, OfNat.ofNat, Imo2026P3.assembleSelectedBlocks
Proof uses: dite, Imo2026P3.selectedIndex, Eq.mp, of_eq_true, eq_true, congrFun', congrArg, dite_eq_left_of_eq_true, Not, List.cons, HDiv.hDiv, List.get, List.nil, Eq, Nat, id, GetElem.getElem, Fin.isLt, Eq.trans, Or and 15 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.assembleSelectedBlocks_sum line 2627 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Imo2026P3.selectedList, Eq, List.sum, List.get, Imo2026P3.assembleSelectedBlocks
Proof uses: dite, Membership.mem, Eq.mpr, Imo2026P3.selectedIndex, Eq.mpr_prop, True, eq_true, True.intro, id, congrFun', congrArg, Eq.trans, Not, List.cons, HDiv.hDiv, OfNat.ofNat, List.nil, dite_congr, Eq.refl, dite_true and 12 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.cutsOfLengths_subset_assembleSelectedBlocks line 2638 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, Finset, Fin, List.length, Imo2026P3.selectedList, List.get, LE.le, Imo2026P3.cutsOfLengths, Imo2026P3.flattenFinBlocks, Imo2026P3.assembleSelectedBlocks
Proof uses: Imo2026P3.cutsOfLengths_subset_flattenFinBlocks, Imo2026P3.assembleSelectedBlocks_ne_nil, Imo2026P3.assembleSelectedBlocks_pos, Imo2026P3.assembleSelectedBlocks_sum
17 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.flatten_assembleSelectedBlocks_pos line 2651 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LT.lt, OfNat.ofNat, Finset, Fin, List.length, Imo2026P3.selectedList, Imo2026P3.flattenFinBlocks, Imo2026P3.assembleSelectedBlocks
Proof uses: Imo2026P3.flattenFinBlocks_pos, Imo2026P3.assembleSelectedBlocks_pos
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.flatten_assembleSelectedBlocks_sum line 2658 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Imo2026P3.selectedList, Eq, List.sum, List.get, Imo2026P3.flattenFinBlocks, Imo2026P3.assembleSelectedBlocks
Proof uses: Imo2026P3.flattenFinBlocks_sum, Imo2026P3.assembleSelectedBlocks_sum
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.assembleTwoSelectedBlocks line 2665 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Imo2026P3.selectedList
Proof uses: dite, Membership.mem, Imo2026P3.selectedIndex, Not, List.cons, HDiv.hDiv, List.get, OfNat.ofNat, List.nil
10 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.assembleTwoSelectedBlocks_ne_nil line 2674 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Imo2026P3.selectedList, Ne, List.nil, Imo2026P3.assembleTwoSelectedBlocks
Proof uses: dite, Membership.mem, Eq.mpr, Not, Eq, Imo2026P3.selectedIndex, of_eq_true, eq_true, id, congrFun', congrArg, dite_eq_left_of_eq_true, List.cons, HDiv.hDiv, List.get, OfNat.ofNat, Eq.trans, dite_eq_right_of_eq_false, eq_false, GetElem.getElem and 10 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.assembleTwoSelectedBlocks_pos line 2687 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Imo2026P3.selectedList, Membership.mem, LT.lt, OfNat.ofNat, Imo2026P3.assembleTwoSelectedBlocks
Proof uses: dite, Imo2026P3.selectedIndex, Eq.mp, of_eq_true, eq_true, congrFun', congrArg, dite_eq_left_of_eq_true, Not, List.cons, HDiv.hDiv, List.get, List.nil, Eq.trans, dite_eq_right_of_eq_false, eq_false, Eq, Nat, id, GetElem.getElem and 15 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.assembleTwoSelectedBlocks_sum line 2707 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Disjoint, Imo2026P3.selectedList, Eq, List.sum, List.get, Imo2026P3.assembleTwoSelectedBlocks
Proof uses: dite, Membership.mem, Eq.mpr, Imo2026P3.selectedIndex, Eq.mpr_prop, True, eq_true, True.intro, id, congrFun', congrArg, Eq.trans, Not, List.cons, HDiv.hDiv, OfNat.ofNat, List.nil, dite_congr, Eq.refl, dite_true and 14 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.cutsOfLengths_subset_assembleTwoSelectedBlocks line 2723 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, Finset, Fin, List.length, Disjoint, Imo2026P3.selectedList, List.get, LE.le, Imo2026P3.cutsOfLengths, Imo2026P3.flattenFinBlocks, Imo2026P3.assembleTwoSelectedBlocks
Proof uses: Imo2026P3.cutsOfLengths_subset_flattenFinBlocks, Imo2026P3.assembleTwoSelectedBlocks_ne_nil, Imo2026P3.assembleTwoSelectedBlocks_pos, Imo2026P3.assembleTwoSelectedBlocks_sum
20 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.exists_equal_subset_common_blocks line 2744 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LT.lt, OfNat.ofNat, Finset, Fin, List.length, Eq, List.sum, Imo2026P3.selectedList, Exists, And, LE.le, Nat, HSub.hSub, HAdd.hAdd, Finset.card, Ne, List.nil and 2 more
Proof uses: Imo2026P3.commonAtoms, Imo2026P3.selectedList_pos, id, Imo2026P3.commonAtoms_spec, Imo2026P3.ScanRefines, Imo2026P3.commonAtoms_scanRefines, Eq.symm, And.left, And.right, Eq.mpr, congrArg, Imo2026P3.exists_blocks_of_scanRefines, Exists.intro, And.intro, Eq.mp, congrFun', congr, Imo2026P3.selectedList_length
24 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.firstPlayerShare_pairDup_append_singleton line 2786 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Imo2026P3.firstPlayerShare, HAppend.hAppend, Imo2026P3.pairDup, List.cons, List.nil, HAdd.hAdd, List.sum
Proof uses: List.filter, Decidable.decide, LE.le, Bool.not, List.mergeSort, GE.ge, List.Perm, List.mergeSort_perm, List.filter_append_perm, List.Perm.trans, List.Perm.append, List.Pairwise, List.pairwise_mergeSort', Membership.mem, Iff.mp, List.Perm.mem_iff, And, Eq.mp, Eq.trans, Bool and 91 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.firstPlayerShare_pairDup line 2854 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Imo2026P3.firstPlayerShare, Imo2026P3.pairDup, List.sum
Proof uses: List.mergeSort, Decidable.decide, GE.ge, List.Perm, List.mergeSort_perm, id, List.Perm.flatMap_right, List.cons, List.nil, Trans.trans, Imo2026P3.firstPlayerShare_congr, List.Perm.symm, Imo2026P3.firstPlayerShare_pairDup_of_pairwise, List.pairwise_mergeSort', List.Perm.sum_eq
12 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.pairDup_perm_append_self line 2868 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, List.Perm, Imo2026P3.pairDup, HAppend.hAppend
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, List.flatMap_nil, List.cons, List.append_nil, id, List.Perm.cons, List.Perm.trans, List.append, List.Perm.symm, List.perm_middle
5 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.exists_crossing_decomposition line 2884 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LT.lt, OfNat.ofNat, LE.le, List.sum, Exists, And, Eq, HAppend.hAppend, List.cons, HAdd.hAdd
Proof uses: List.rec, List.nil, False.elim, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat and 49 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.exists_prefix_match_residual line 2911 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LT.lt, OfNat.ofNat, LE.le, List.sum, Exists, And, Eq, HAppend.hAppend, List.cons, HSub.hSub, HAdd.hAdd, List.nil
Proof uses: Imo2026P3.exists_crossing_decomposition, id, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 51 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.residualList line 2944 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, List
Proof uses: ite, Eq, OfNat.ofNat, List.nil, List.cons
3 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.residualList_sum line 2947 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, List.sum, Imo2026P3.residualList
Proof uses: dite, OfNat.ofNat, of_eq_true, Eq.trans, True, congr, congrArg, List, List.nil, ite_eq_left_of_eq_true, List.cons, congrFun', eq_self, Not, ite_eq_right_of_eq_false, eq_false, add_zero
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.residualList_length_le_one line 2950 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, Nat, List.length, Imo2026P3.residualList, OfNat.ofNat
Proof uses: dite, Eq, of_eq_true, Eq.trans, True, congrFun', congrArg, List, List.nil, ite_eq_left_of_eq_true, List.cons, eq_self, Not, ite_eq_right_of_eq_false, eq_false, zero_add
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.residualList_pos line 2953 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, Membership.mem, List, Imo2026P3.residualList, LT.lt
Proof uses: dite, Eq, False.elim, Eq.mp, False, Eq.trans, List.nil, congrFun', congrArg, ite_eq_left_of_eq_true, List.cons, True, eq_self, Not, lt_of_le_of_ne, Ne.symm, Or, ite_eq_right_of_eq_false, eq_false, or_false and 1 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.firstPlayerShare_pairDup_residualList line 2963 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Imo2026P3.firstPlayerShare, HAppend.hAppend, Imo2026P3.pairDup, Imo2026P3.residualList, HAdd.hAdd, List.sum
Proof uses: dite, OfNat.ofNat, Eq.mpr, id, congr, congrArg, Eq.trans, List.nil, ite_eq_left_of_eq_true, List.cons, eq_self, List.append_nil, add_zero, Imo2026P3.firstPlayerShare_pairDup, Eq.symm, Not, congrFun', ite_eq_right_of_eq_false, eq_false, Imo2026P3.firstPlayerShare_pairDup_append_singleton
15 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.prefixRefinementBlocks line 2971 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Fin, List.length, HAppend.hAppend, List.cons, List.nil
Proof uses: dite, LT.lt, Nat, Fin.mk, Not, Eq, Imo2026P3.residualList, HDiv.hDiv, List.get, OfNat.ofNat
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.prefixRefinementBlocks_ne_nil line 2982 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Fin, List.length, HAppend.hAppend, List.cons, List.nil, Ne, Imo2026P3.prefixRefinementBlocks
Proof uses: dite, LT.lt, Nat, Eq.mpr, Not, Eq, Fin.mk, of_eq_true, eq_true, id, congrFun', congrArg, dite_eq_left_of_eq_true, Imo2026P3.residualList, HDiv.hDiv, List.get, OfNat.ofNat, LE.le, Eq.trans, HAdd.hAdd and 18 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.prefixRefinementBlocks_pos line 2995 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Fin, List.length, HAppend.hAppend, List.cons, List.nil, Membership.mem, LT.lt, OfNat.ofNat, LE.le, Imo2026P3.prefixRefinementBlocks
Proof uses: dite, Nat, Fin.mk, Eq.mpr, id, Eq, Eq.trans, HAdd.hAdd, congrArg, List.length_append, zero_add, Eq.mp, of_eq_true, eq_true, congrFun', dite_eq_left_of_eq_true, Not, Imo2026P3.residualList, HDiv.hDiv, List.get and 26 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.prefixRefinementBlocks_sum line 3016 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, HAdd.hAdd, Fin, List.length, HAppend.hAppend, List.cons, List.nil, List.sum, List.get, Imo2026P3.prefixRefinementBlocks
Proof uses: dite, LT.lt, Nat, Eq.mpr, Fin.mk, Eq.mpr_prop, True, eq_true, True.intro, id, congrFun', congrArg, Eq.trans, Not, Imo2026P3.residualList, HDiv.hDiv, OfNat.ofNat, dite_congr, Eq.refl, dite_true and 24 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.appendToLast line 3040 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, List, Real
Proof uses: ite, Eq, Fin.last, HAppend.hAppend
9 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.ofFn_appendToLast line 3044 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, List, Real, Eq, List.ofFn, Imo2026P3.appendToLast, HAppend.hAppend, List.dropLast, List.cons, Fin.last, List.nil
Proof uses: Eq.mpr, List.concat, Fin.castSucc, id, congrArg, Nat.succ, List.ofFn_succ', propext, List.ofFn_inj, funext, of_eq_true, Eq.trans, True, congrFun', ite_eq_right_of_eq_false, eq_self, congr, ite_eq_left_of_eq_true, List.concat_eq_append, List.dropLast_append_of_ne_nil and 5 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.prefixFlattenBlocks line 3058 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Fin, HAdd.hAdd, Nat, List.length, OfNat.ofNat, HAppend.hAppend, List.cons
Proof uses: Eq, Fin.cast, Fin.append, Imo2026P3.appendToLast, Imo2026P3.residualList, HDiv.hDiv, List.get, List.nil
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.prefixRefinementBlocks_eq_prefixFlattenBlocks line 3070 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Fin, HAdd.hAdd, Nat, List.length, OfNat.ofNat, Eq, HAppend.hAppend, List.cons, Imo2026P3.prefixRefinementBlocks, List.nil, Fin.cast, Imo2026P3.prefixFlattenBlocks
Proof uses: funext, dite, LT.lt, Eq.mpr, Fin.mk, Eq.rec, of_eq_true, eq_true, LE.le, ite, Fin.castLT, Eq.mpr_prop, Fin.last, Imo2026P3.residualList, Not, HDiv.hDiv, GetElem.getElem, HSub.hSub, Fin.subNat, Eq.trans and 36 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 60 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.prefixFlattenBlocks_ne_nil line 3121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Fin, HAdd.hAdd, Nat, List.length, OfNat.ofNat, Ne, List.nil, HAppend.hAppend, List.cons, Imo2026P3.prefixFlattenBlocks
Proof uses: Eq.mpr, Imo2026P3.prefixRefinementBlocks, Fin.cast, id, Eq, congrArg, Eq.symm, Imo2026P3.prefixRefinementBlocks_eq_prefixFlattenBlocks, Imo2026P3.prefixRefinementBlocks_ne_nil, of_eq_true, Eq.trans, True, congrFun', List.length_append, zero_add, eq_self
14 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.prefixFlattenBlocks_pos line 3130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Fin, HAdd.hAdd, Nat, List.length, OfNat.ofNat, Membership.mem, HAppend.hAppend, List.cons, LT.lt, LE.le, Imo2026P3.prefixFlattenBlocks
Proof uses: Eq.mpr, Imo2026P3.prefixRefinementBlocks, List.nil, Fin.cast, id, Eq, congrArg, Eq.symm, Imo2026P3.prefixRefinementBlocks_eq_prefixFlattenBlocks, Imo2026P3.prefixRefinementBlocks_pos, of_eq_true, Eq.trans, True, congrFun', List.length_append, zero_add, eq_self
24 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.prefixFlattenBlocks_sum line 3141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, HAdd.hAdd, Fin, Nat, List.length, OfNat.ofNat, List.sum, List.get, HAppend.hAppend, List.cons, List.nil, Fin.cast, Imo2026P3.prefixFlattenBlocks
Proof uses: Eq.mpr, Imo2026P3.prefixRefinementBlocks, id, congrArg, Eq.symm, Imo2026P3.prefixRefinementBlocks_eq_prefixFlattenBlocks, Imo2026P3.prefixRefinementBlocks_sum, of_eq_true, Eq.trans, True, congrFun', List.length_append, zero_add, eq_self
20 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.finBlocks_prefixFlattenBlocks line 3154 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Fin, HAdd.hAdd, Nat, List.length, OfNat.ofNat, Eq, Imo2026P3.finBlocks, HAppend.hAppend, List.cons, Imo2026P3.prefixFlattenBlocks, List.ofFn, Imo2026P3.appendToLast, Imo2026P3.residualList, HDiv.hDiv, List.get, List.nil
Proof uses: id, Eq.mpr, List.map, List.finRange, congrArg, Eq.symm, List.ofFn_eq_map, congrFun', List.length_append, Fin.cast, List.ofFn_congr, List.ofFn_fin_append
25 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.flatten_ofFn_appendToLast line 3171 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, List, Real, Eq, List.flatten, List.ofFn, Imo2026P3.appendToLast, HAppend.hAppend
Proof uses: Eq.mpr, List.dropLast, List.cons, Fin.last, List.nil, id, congrArg, Imo2026P3.ofFn_appendToLast, List.flatten_append, List.flatten_singleton, Ne, of_eq_true, Eq.trans, Fin.succ, True, congrFun', List.ofFn_succ, Not, False, eq_false' and 14 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.flatten_map_halfBlock line 3189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, List.flatten, List.map, List.cons, HDiv.hDiv, OfNat.ofNat, Nat, List.nil, Imo2026P3.bisectLengths
Proof uses: List.rec, of_eq_true, Eq.trans, True, congr, congrArg, List.map_nil, List.flatMap, List.flatMap_nil, eq_self, HAppend.hAppend, List.map_cons, List.flatMap_cons
19 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.flattenFinBlocks_prefixFlattenBlocks line 3195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Fin, HAdd.hAdd, Nat, List.length, OfNat.ofNat, Eq, Imo2026P3.flattenFinBlocks, HAppend.hAppend, List.cons, Imo2026P3.prefixFlattenBlocks, Imo2026P3.residualList, Imo2026P3.bisectLengths
Proof uses: id, Eq.mpr, List.flatten, Imo2026P3.finBlocks, List.ofFn, Imo2026P3.appendToLast, HDiv.hDiv, List.get, List.nil, congrArg, Imo2026P3.finBlocks_prefixFlattenBlocks, List.flatten_append, Imo2026P3.flatten_ofFn_appendToLast, Eq.symm, List.map, List.finRange, List.ofFn_eq_map, Trans.trans, List.ofFn_comp', List.ofFn_get and 2 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.prefix_local_perm_pairs line 3220 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, List.Perm, HAppend.hAppend, Imo2026P3.residualList, Imo2026P3.bisectLengths, Imo2026P3.pairDup, List.map, HDiv.hDiv, OfNat.ofNat, Nat
Proof uses: Eq, Eq.refl, Eq.mpr, id, congrArg, List.perm_append_comm, congr, Eq.trans, congrFun', List.append_assoc, Eq.mp, List.Perm.append_left, List.Perm.append_right, List.Perm.symm, Imo2026P3.pairDup_perm_append_self, of_eq_true, List.flatMap, List.cons, List.nil, True and 6 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.firstPlayerShare_prefix_local line 3241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Imo2026P3.firstPlayerShare, HAppend.hAppend, Imo2026P3.residualList, Imo2026P3.bisectLengths, HAdd.hAdd, List.sum, HDiv.hDiv, OfNat.ofNat, Nat
Proof uses: Eq.mpr, Imo2026P3.pairDup, List.map, id, congrArg, Imo2026P3.firstPlayerShare_congr, Imo2026P3.prefix_local_perm_pairs, Imo2026P3.firstPlayerShare_pairDup_residualList, List.sum_append, Imo2026P3.sum_map_half, Eq.refl
35 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.prefix_local_length line 3248 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Nat, List.length, HAppend.hAppend, Imo2026P3.residualList, Imo2026P3.bisectLengths, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, List.length_append, congr, Imo2026P3.bisectLengths_length
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.prefix_local_length_le line 3254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Nat, LT.lt, OfNat.ofNat, HAdd.hAdd, LE.le, List.length, HSub.hSub, HAppend.hAppend, Imo2026P3.residualList, Imo2026P3.bisectLengths, HMul.hMul
Proof uses: Eq.mpr, id, Eq, congrArg, Imo2026P3.prefix_local_length, Imo2026P3.residualList_length_le_one
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.prefix_global_perm_pairs line 3262 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, List.Perm, HAppend.hAppend, Imo2026P3.residualList, Imo2026P3.bisectLengths, Imo2026P3.pairDup, List.map, HDiv.hDiv, OfNat.ofNat, Nat
Proof uses: List.Perm.append_right, Imo2026P3.prefix_local_perm_pairs, Eq, Eq.refl, Eq.mpr, id, congr, congrArg, List.append_assoc, List.Perm.append_left, List.perm_append_comm, of_eq_true, List.flatMap, List.cons, List.nil, Eq.trans, True, List.flatMap_append, eq_self, congrFun' and 4 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.firstPlayerShare_prefix_global line 3289 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Imo2026P3.firstPlayerShare, HAppend.hAppend, Imo2026P3.residualList, Imo2026P3.bisectLengths, HAdd.hAdd, List.sum, HDiv.hDiv, OfNat.ofNat, Nat
Proof uses: Eq.mpr, Imo2026P3.pairDup, List.map, id, congrArg, Imo2026P3.firstPlayerShare_congr, Imo2026P3.prefix_global_perm_pairs, Imo2026P3.firstPlayerShare_pairDup_residualList, List.sum_append, Imo2026P3.sum_map_half, Eq.refl
35 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.prefix_global_length line 3297 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Nat, List.length, HAppend.hAppend, Imo2026P3.residualList, Imo2026P3.bisectLengths, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, List.length_append, congr, Imo2026P3.bisectLengths_length
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2026P3.outsideIndices line 3309 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin
Proof uses: SDiff.sdiff, Finset.univ, Union.union
4 instances, coercions and auxiliary constants left out.
def Imo2026P3.groupedIndices line 3312 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, List
Proof uses: HAppend.hAppend, Finset.sort, LE.le, Imo2026P3.outsideIndices
7 instances, coercions and auxiliary constants left out.
lemma Imo2026P3.groupedIndices_nodup line 3315 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Disjoint, List.Nodup, Imo2026P3.groupedIndices
Proof uses: Finset.sort, LE.le, Finset.sort_nodup, Imo2026P3.outsideIndices, id, Eq.mpr, HAppend.hAppend, List, Eq, congrArg, List.append_assoc, List.Nodup.append, List.Disjoint, Membership.mem, Not, propext, List.disjoint_left, Iff.mp, Finset.mem_sort, And.right and 11 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.groupedIndices_length line 3339 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Disjoint, Eq, List.length, Imo2026P3.groupedIndices
Proof uses: List.Nodup, Imo2026P3.groupedIndices_nodup, Trans.trans, Finset.card, List.toFinset, Eq.symm, List.toFinset_card_of_nodup, Union.union, Imo2026P3.outsideIndices, Finset.univ, Finset.ext, Eq.mpr, Iff, Membership.mem, Or, And, Not, id, Eq.trans, True and 19 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.groupedIndices_perm_finRange line 3352 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Disjoint, List.Perm, Imo2026P3.groupedIndices, List.finRange
Proof uses: List.Subperm, List.subperm_of_subset, Imo2026P3.groupedIndices_nodup, Membership.mem, List, of_eq_true, Imo2026P3.subperm_perm_of_length_eq, Eq.mpr, Eq, List.length, id, congrArg, Imo2026P3.groupedIndices_length, List.length_finRange, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.flatten_assembleTwoSelectedBlocks_perm line 3362 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Disjoint, Imo2026P3.selectedList, List.Perm, Imo2026P3.flattenFinBlocks, Imo2026P3.assembleTwoSelectedBlocks, HAppend.hAppend, Imo2026P3.bisectLengths, Imo2026P3.outsideIndices
Proof uses: Eq, List.flatMap, Finset.sort, LE.le, Eq.mpr, Imo2026P3.selectedBlockAt, id, congrArg, Eq.symm, Imo2026P3.flatMap_sort_selectedBlockAt, List.flatMap_congr, Membership.mem, Iff.mp, Finset.mem_sort, of_eq_true, Eq.trans, Imo2026P3.selectedIndex, eq_true, True, congr and 40 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.flattenFinBlocks_cast line 3410 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Fin, List, Real, Imo2026P3.flattenFinBlocks, Fin.cast
Proof uses: Eq.rec, of_eq_true, eq_self

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
structure Imo2026P3.PositivePrefixData line 3417 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real
theorem Imo2026P3.exists_positive_prefix_data line 3441 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Membership.mem, LT.lt, OfNat.ofNat, List.sum, LE.le, Nonempty, Imo2026P3.PositivePrefixData
Proof uses: Exists, And, Eq, HAppend.hAppend, List.cons, HSub.hSub, HAdd.hAdd, List.nil, Imo2026P3.exists_prefix_match_residual, Imo2026P3.commonAtoms, Or, Iff.mp, List.mem_append, of_eq_true, Eq.trans, True, congr, congrArg, eq_true, true_or and 87 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.selected_partition_sum line 3541 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Disjoint, Eq, HAdd.hAdd, List.sum, Imo2026P3.selectedList, Imo2026P3.outsideIndices
Proof uses: List.Perm, List.map, List.get, Imo2026P3.groupedIndices, List.finRange, List.Perm.map, Imo2026P3.groupedIndices_perm_finRange, List.Perm.sum_eq, id, Eq.mp, Finset.sort, LE.le, congrArg, List.map_get_finRange, HAppend.hAppend, congrFun', Eq.trans, List.map_append, List.sum_append, OfNat.ofNat
29 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.selected_partition_length line 3551 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Finset, Fin, List.length, Disjoint, Eq, Nat, HAdd.hAdd, Imo2026P3.selectedList, Imo2026P3.outsideIndices
Proof uses: Imo2026P3.groupedIndices, List.finRange, List.Perm.length_eq, Imo2026P3.groupedIndices_perm_finRange, Eq.mpr, Finset.card, id, congrFun', congrArg, Eq.trans, congr, Imo2026P3.selectedList_length, Nat.add_assoc, Eq.mp, HAppend.hAppend, Finset.sort, LE.le, List.append_assoc, List.length_append, Finset.length_sort and 1 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.exists_positive_close_refinement line 3559 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, Finset, Fin, List.length, Disjoint, Imo2026P3.selectedList, LE.le, HSub.hSub, Exists, And, Imo2026P3.cutsOfLengths, Nat and 4 more
Proof uses: Imo2026P3.outsideIndices, Imo2026P3.selectedList_pos, id, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero and 126 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.flattenFinBlocks_singletons line 3639 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Eq, Imo2026P3.flattenFinBlocks, List.length, Fin, List.cons, List.get, List.nil
Proof uses: id, List.flatten, Imo2026P3.finBlocks, Eq.mpr, List.map, List.finRange, List.ofFn, congrArg, Eq.symm, List.ofFn_eq_map, Trans.trans, List.ofFn_comp', List.ofFn_get, Eq.refl, List.rec, of_eq_true, Eq.trans, True, congrFun', List.map_nil and 3 more
3 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.exists_singleton_close_refinement line 3654 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, Fin, List.length, LE.le, List.get, Exists, And, Finset, Imo2026P3.cutsOfLengths, Nat, HSub.hSub, HMul.hMul and 3 more
Proof uses: Singleton.singleton, EmptyCollection.emptyCollection, Imo2026P3.selectedList, Imo2026P3.outsideIndices, Disjoint, Finset.disjoint_empty_right, List.cons, of_eq_true, GetElem.getElem, Fin.isLt, Eq.trans, True, congrFun', congrArg, List.map, Finset.sort, Imo2026P3.selectedList.eq_1, Finset.sort_singleton, DecidableRel, IsTrans and 136 more
135 instances, coercions and auxiliary constants left out.

Tactic trace: 80 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.exists_close_refinement line 3752 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Real, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Eq, List.sum, Exists, And, LE.le, Finset, Imo2026P3.cutsOfLengths, Nat, List.length, HSub.hSub, HMul.hMul, Imo2026P3.firstPlayerShare, HDiv.hDiv and 2 more
Proof uses: Iff.mpr, List.length_pos_iff, Fin, List.get, LT.lt.le, List.get_mem, Finset.sum, Finset.univ, List.map, List.finRange, Eq.symm, of_eq_true, Eq.trans, True, congr, congrArg, List.map_get_finRange, GetElem.getElem, Fin.isLt, Finset.sum_congr and 95 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.upper_denom_pos line 3813 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Real, OfNat.ofNat, HSub.hSub, HPow.hPow, HAdd.hAdd
Proof uses: one_lt_pow₀, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, HMul.hMul, Int.rawCast, inferInstance, Ring and 49 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.upper_answer_identity line 3819 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, HSub.hSub, HPow.hPow
Proof uses: Ne, ne_of_gt, Imo2026P3.upper_denom_pos, HMul.hMul, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero and 89 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2026P3.half_le_upper_answer line 3828 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, HDiv.hDiv, OfNat.ofNat, HPow.hPow, HSub.hSub, HAdd.hAdd
Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, Imo2026P3.upper_answer_identity, LT.lt, Iff.mpr, one_div_pos, Imo2026P3.upper_denom_pos, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Inv.inv, Int.rawCast and 74 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.exists_hard_reply line 3835 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Real, Imo2026P3.AdmissibleMark, Eq, Finset.card, Exists, And, Disjoint, LE.le, Imo2026P3.L, HDiv.hDiv, HPow.hPow, OfNat.ofNat, HSub.hSub, HAdd.hAdd
Proof uses: List, Imo2026P3.pieceLengths, Ne, List.nil, List.length, congrArg, False.elim, False, Eq.mp, Eq.trans, EmptyCollection.emptyCollection, congr, and_false, Imo2026P3.pieceLengths_length, Membership.mem, LT.lt, Imo2026P3.pieceLengths_pos, And.left, Set, Set.Ioo and 14 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.codex_upper_bound_aux line 3863 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Real, Imo2026P3.AdmissibleMark, Exists, And, Disjoint, LE.le, Imo2026P3.L, HDiv.hDiv, HPow.hPow, HSub.hSub, HAdd.hAdd
Proof uses: dite, Finset.card, Eq, Imo2026P3.exists_bisect_reply, Exists.intro, And.intro, Eq.mpr, id, congrArg, Imo2026P3.half_le_upper_answer, Not, And.right, Set, Set.Ioo, Imo2026P3.exists_hard_reply
55 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem Imo2026P3.lower_bound_aux Auxiliary form of the lower bound, declared before V_eq so that the main reduction can refer to it line 3879 source
Source documentation
Auxiliary form of the lower bound, declared before V_eq so that the main reduction can refer to it. Its content is identical to lower_bound.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, Finset, Real, And, Imo2026P3.AdmissibleMark, Disjoint, LE.le, HDiv.hDiv, HPow.hPow, HSub.hSub, HAdd.hAdd, Imo2026P3.L
Proof uses: Imo2026P3.codex_lower_bound_complete
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem lower_bound_aux (n : ℕ) (hn : 0 < n) :
    ∃ A : Finset ℝ, AdmissibleMark n A ∧
      ∀ B : Finset ℝ, AdmissibleMark n B → Disjoint A B →
        (2 : ℝ) ^ n / ((2 : ℝ) ^ (n + 1) - 1) ≤ L A B := by
…
```
Mentions: Imo2026P3.AdmissibleMark, Imo2026P3.L
theorem Imo2026P3.upper_bound_aux Auxiliary form of the upper bound, declared before V_eq so that the main reduction can refer to it line 3887 source
Source documentation
Auxiliary form of the upper bound, declared before V_eq so that the main reduction can refer to it. Its content is identical to upper_bound.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Real, Imo2026P3.AdmissibleMark, Exists, And, Disjoint, LE.le, Imo2026P3.L, HDiv.hDiv, HPow.hPow, HSub.hSub, HAdd.hAdd
Proof uses: Imo2026P3.codex_upper_bound_aux
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem upper_bound_aux (n : ℕ) (hn : 0 < n) :
    ∀ A : Finset ℝ, AdmissibleMark n A →
      ∃ B : Finset ℝ, AdmissibleMark n B ∧ Disjoint A B ∧
        L A B ≤ (2 : ℝ) ^ n / ((2 : ℝ) ^ (n + 1) - 1) := by
…
```
Mentions: Imo2026P3.AdmissibleMark, Imo2026P3.L
theorem Imo2026P3.lower_bound Lower bound line 3896 source
Source documentation
Lower bound. Liu Bang has an admissible marking A such that for every admissible marking B disjoint from A, his guaranteed share is at least 2^n / (2^(n+1) - 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, Finset, Real, And, Imo2026P3.AdmissibleMark, Disjoint, LE.le, HDiv.hDiv, HPow.hPow, HSub.hSub, HAdd.hAdd, Imo2026P3.L
Proof uses: Imo2026P3.lower_bound_aux
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem lower_bound (n : ℕ) (hn : 0 < n) :
    ∃ A : Finset ℝ, AdmissibleMark n A ∧
      ∀ B : Finset ℝ, AdmissibleMark n B → Disjoint A B →
        (2 : ℝ) ^ n / ((2 : ℝ) ^ (n + 1) - 1) ≤ L A B := by
…
```
Mentions: Imo2026P3.AdmissibleMark, Imo2026P3.L
theorem Imo2026P3.upper_bound Upper bound / optimality line 3905 source
Source documentation
Upper bound / optimality. For every admissible marking A of Liu Bang, Xiang Yu has an admissible marking B disjoint from A with L A B ≤ 2^n / (2^(n+1) - 1), so Liu Bang cannot guarantee more.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Real, Imo2026P3.AdmissibleMark, Exists, And, Disjoint, LE.le, Imo2026P3.L, HDiv.hDiv, HPow.hPow, HSub.hSub, HAdd.hAdd
Proof uses: Imo2026P3.upper_bound_aux
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem upper_bound (n : ℕ) (hn : 0 < n) :
    ∀ A : Finset ℝ, AdmissibleMark n A →
      ∃ B : Finset ℝ, AdmissibleMark n B ∧ Disjoint A B ∧
        L A B ≤ (2 : ℝ) ^ n / ((2 : ℝ) ^ (n + 1) - 1) := by
…
```
Mentions: Imo2026P3.AdmissibleMark, Imo2026P3.L
problem Imo2026P3.imo2026_p3 line 3914 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Real, Imo2026P3.V, Imo2026P3.answer
Proof uses: Finset, And, Imo2026P3.AdmissibleMark, Disjoint, LE.le, HDiv.hDiv, HPow.hPow, HSub.hSub, HAdd.hAdd, Imo2026P3.L, Exists, Imo2026P3.lower_bound_aux, Imo2026P3.upper_bound_aux, EmptyCollection.emptyCollection, And.intro, Set, Set.Ioo, Finset.card, of_eq_true, Eq.trans and 28 more
56 instances, coercions and auxiliary constants left out.

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