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

44 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2011, Problem 4

Let n > 0 be an integer. We are given a balance and n weights of weight 2^0, 2^1, . . . , 2^(n−1). We are to place each of the n weights on the balance, one after another, in such a way that the right pan is never heavier than the left pan. At each step we choose one of the weights that has not yet been placed on the balance, and place it on either the left pan or the right pan, until all of the weights have been placed. Determine the number of ways in which this can be done.

Imports (12)

Imported by 1 file

Compfiles.lean

def Imo2011P4.Balance The imbalance (left pan minus right pan) after a sequence of placements line 47 source
Source documentation
The imbalance (left pan minus right pan) after a sequence of placements. A pair (i, b) denotes one placement of the weight 2^i; the boolean is true if the weight is placed on the left pan and false if it is placed on the right pan.

standard axioms: propext what this means
Statement uses: List, Prod, Nat, Bool, Int
Proof uses: List.sum, List.map, ite, Eq, Prod.snd, Bool.true, HPow.hPow, OfNat.ofNat, Prod.fst, Neg.neg
11 instances, coercions and auxiliary constants left out.
```
def Balance (l : List (ℕ × Bool)) : ℤ :=
…
```
def Imo2011P4.ValidSeq A sequence of placements is valid if after every step the right pan is not heavier than the left pan line 52 source
Source documentation
A sequence of placements is valid if after every step the right pan is not heavier than the left pan.

standard axioms: propext what this means
Statement uses: List, Prod, Nat, Bool
Proof uses: List.IsPrefix, LE.le, Int, OfNat.ofNat, Imo2011P4.Balance
2 instances, coercions and auxiliary constants left out.
```
def ValidSeq (l : List (ℕ × Bool)) : Prop :=
…
```
def Imo2011P4.Ways Documented declaration: Ways line 58 source
Source documentation
The set of ways to carry out the process with the weights 2^0, 2^1, ..., 2^(n-1): sequences of placements in which every weight is used exactly once and the right pan is never heavier than the left pan.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: Subtype, List, Prod, Bool, And, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.ValidSeq
```
def Ways (n : ℕ) : Type :=
…
```
lemma Imo2011P4.balance_nil line 74 source
standard axioms: propext what this means
Statement uses: Eq, Int, Imo2011P4.Balance, List.nil, Prod, Nat, Bool, OfNat.ofNat
Proof uses: rfl
1 instances, coercions and auxiliary constants left out.
lemma Imo2011P4.balance_cons line 76 source
standard axioms: propext what this means
Statement uses: Prod, Nat, Bool, List, Eq, Int, Imo2011P4.Balance, List.cons, HAdd.hAdd, ite, Prod.snd, Bool.true, HPow.hPow, OfNat.ofNat, Prod.fst, Neg.neg
Proof uses: of_eq_true, List.sum, List.map, Eq.trans, True, congrFun', congrArg, List.map_cons, 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 Imo2011P4.balance_append line 80 source
standard axioms: propext what this means
Statement uses: List, Prod, Nat, Bool, Eq, Int, Imo2011P4.Balance, HAppend.hAppend, HAdd.hAdd
Proof uses: of_eq_true, List.sum, List.map, ite, Prod.snd, Bool.true, HPow.hPow, OfNat.ofNat, Prod.fst, Neg.neg, Eq.trans, True, congrFun', congrArg, List.map_append, List.sum_append, 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 Imo2011P4.balance_map_succ Doubling all weights doubles the imbalance line 85 source
Source documentation
Doubling all weights doubles the imbalance.

standard axioms: Quot.sound, propext what this means
Statement uses: List, Prod, Nat, Bool, Eq, Int, Imo2011P4.Balance, List.map, Prod.mk, HAdd.hAdd, Prod.fst, OfNat.ofNat, Prod.snd, HMul.hMul
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, List.map_nil, MulZeroClass.mul_zero, eq_self, Eq.mpr, List.cons, ite, Bool.true, HPow.hPow, Neg.neg, id, List.map_cons, Imo2011P4.balance_cons, ite_congr and 52 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma balance_map_succ (l : List (ℕ × Bool)) :
    Balance (l.map fun p : ℕ × Bool ↦ (p.1 + 1, p.2)) = 2 * Balance l := by
…
```
Mentions: Imo2011P4.Balance
lemma Imo2011P4.balance_map_pred Halving all weights halves the imbalance (all weights here are even) line 94 source
Source documentation
Halving all weights halves the imbalance (all weights here are even).

standard axioms: propext what this means
Statement uses: List, Prod, Nat, Bool, Membership.mem, LE.le, OfNat.ofNat, Prod.fst, Eq, Int, HMul.hMul, Imo2011P4.Balance, List.map, Prod.mk, HSub.hSub, Prod.snd
Proof uses: List.rec, List.nil, of_eq_true, Eq.trans, True, congrFun', congrArg, List.map_nil, MulZeroClass.mul_zero, eq_self, List.cons, List.mem_cons_self, List.mem_cons_of_mem, HPow.hPow, Eq.mpr, HAdd.hAdd, id, Eq.rec, Eq.refl, Eq.symm and 41 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma balance_map_pred (l : List (ℕ × Bool)) (h : ∀ p ∈ l, 1 ≤ p.1) :
    2 * Balance (l.map fun p : ℕ × Bool ↦ (p.1 - 1, p.2)) = Balance l := by
…
```
Mentions: h, Imo2011P4.Balance
lemma Imo2011P4.balance_ne_zero Key nonzero fact: a nonempty signed sum of distinct powers of two is nonzero line 110 source
Source documentation
Key nonzero fact: a nonempty signed sum of distinct powers of two is nonzero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Nat, Bool, Ne, List.nil, List.Nodup, List.map, Prod.fst, Int, Imo2011P4.Balance, OfNat.ofNat
Proof uses: LE.le, abs, List.sum, HPow.hPow, List.rec, of_eq_true, Eq.trans, True, congr, congrArg, abs_zero, List.map_nil, Eq.mpr, List.cons, HAdd.hAdd, ite, Eq, Prod.snd, Bool.true, Neg.neg and 127 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 88 steps
Open to load the checked before-and-after goal states.
```
lemma balance_ne_zero {l : List (ℕ × Bool)} (hne : l ≠ []) (hnd : (l.map Prod.fst).Nodup) :
    Balance l ≠ 0 := by
…
```
Mentions: Imo2011P4.Balance
lemma Imo2011P4.prefix_append_cases A prefix of an append either lies in the first part or extends it line 205 source
Source documentation
A prefix of an append either lies in the first part or extends it.

standard axioms: Quot.sound, propext what this means
Statement uses: List, List.IsPrefix, HAppend.hAppend, Or, Exists, And, Eq
Proof uses: Iff.mp, List.append_eq_append_iff, Or.inl, Exists.intro, Eq.symm, Or.inr, And.intro
7 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma prefix_append_cases {α : Type*} {pre X Y : List α} (h : pre <+: X ++ Y) :
    pre <+: X ∨ ∃ pre', pre = X ++ pre' ∧ pre' <+: Y := by
…
```
Mentions: h
lemma Imo2011P4.map_down_map_up line 212 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Nat, Bool, Eq, List.map, Prod.mk, HSub.hSub, Prod.fst, OfNat.ofNat, Prod.snd, HAdd.hAdd
Proof uses: List.rec, Eq.refl, List.nil, of_eq_true, List.cons, Eq.trans, True, congrFun', congrArg, List.map_cons, congr, add_tsub_cancel_right, Prod.mk.eta, Function.comp, List.map_map, id, Eq.mp, eq_self
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P4.map_up_map_down line 218 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Nat, Bool, Membership.mem, LE.le, OfNat.ofNat, Prod.fst, Eq, List.map, Prod.mk, HAdd.hAdd, Prod.snd, HSub.hSub
Proof uses: List.rec, List.nil, Eq.refl, List.cons, List.mem_cons_self, List.mem_cons_of_mem, Eq.mpr, And, id, Eq.trans, congrFun', congrArg, List.map_cons, List.cons.injEq, And.intro
15 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P4.ways_length line 231 source
standard axioms: propext what this means
Statement uses: Nat, Imo2011P4.Ways, Eq, List.length, Prod, Bool, List, And, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.ValidSeq
Proof uses: List.Perm.length_eq, And.left, Subtype.property, Eq.mp, congrArg, List.length_range, List.length_map
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P4.ways_nodup line 235 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, List.Nodup, List.map, Prod, Bool, Prod.fst, List, And, List.Perm, List.range, Imo2011P4.ValidSeq
Proof uses: Iff.mpr, List.Perm.nodup_iff, And.left, Subtype.property, List.nodup_range
2 instances, coercions and auxiliary constants left out.
abbrev Imo2011P4.removeIdx The position of the weight 2^0 in a valid sequence line 239 source
Source documentation
The position of the weight 2^0 in a valid sequence.

standard axioms: propext what this means
Statement uses: Nat, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat
Proof uses: List.findIdx, Prod, Bool, BEq.beq, Prod.fst, List, And, List.Perm, List.map, List.range, Imo2011P4.ValidSeq
9 instances, coercions and auxiliary constants left out.
```
abbrev removeIdx {n : ℕ} (w : Ways (n + 1)) : ℕ := w.1.findIdx fun p ↦ p.1 == 0
```
Mentions: Imo2011P4.Ways
lemma Imo2011P4.ways_findIdx_lt line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, LT.lt, List.findIdx, Prod, Bool, BEq.beq, Prod.fst, List, And, List.Perm, List.map, List.range, Imo2011P4.ValidSeq, List.length
Proof uses: Eq.mpr, Exists, Membership.mem, Eq, Bool.true, id, congrArg, propext, List.findIdx_lt_length, Iff.mpr, List.mem_range, Nat.succ_pos, List.Perm.mem_iff, And.left, Subtype.property, Iff.mp, List.mem_map, Exists.intro, And.intro, beq_iff_eq
18 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
abbrev Imo2011P4.removePan The pan on which the weight 2^0 was placed line 250 source
Source documentation
The pan on which the weight 2^0 was placed.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, Bool
Proof uses: Prod.snd, GetElem.getElem, List, Prod, LT.lt, List.length, And, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.ValidSeq, Imo2011P4.removeIdx, Imo2011P4.ways_findIdx_lt
9 instances, coercions and auxiliary constants left out.
```
abbrev removePan {n : ℕ} (w : Ways (n + 1)) : Bool :=
…
```
Mentions: Imo2011P4.Ways
lemma Imo2011P4.ways_getElem_fst line 253 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, Eq, Prod.fst, Bool, GetElem.getElem, List, Prod, LT.lt, List.length, And, List.Perm, List.map, List.range, Imo2011P4.ValidSeq, List.findIdx, BEq.beq, Imo2011P4.ways_findIdx_lt
Proof uses: Bool.true, List.findIdx_getElem, Iff.mp, beq_iff_eq
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P4.ways_split A valid sequence splits around its 2^0 weight line 260 source
Source documentation
A valid sequence splits around its 2^0 weight.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, Eq, List, Prod, Bool, And, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.ValidSeq, HAppend.hAppend, List.take, Imo2011P4.removeIdx, List.cons, Prod.mk, Imo2011P4.removePan and 1 more
Proof uses: GetElem.getElem, LT.lt, List.length, Imo2011P4.ways_findIdx_lt, Prod.ext, Imo2011P4.ways_getElem_fst, rfl, Prod.snd, Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, List.take_append_drop, List.findIdx, BEq.beq, List.getElem_cons_drop
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma ways_split {n : ℕ} (w : Ways (n + 1)) :
    w.1 = w.1.take (removeIdx w) ++ (0, removePan w) :: w.1.drop (removeIdx w + 1) := by
…
```
Mentions: Imo2011P4.Ways, Imo2011P4.removeIdx, Imo2011P4.removePan
lemma Imo2011P4.ways_fst_pos The weights before and after the 2^0 weight are all even line 269 source
Source documentation
The weights before and after the 2^0 weight are all even.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, And, Prod, Bool, Membership.mem, List, List.take, Imo2011P4.removeIdx, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.ValidSeq, LE.le, List.drop
Proof uses: List.Nodup, Iff.mpr, List.Perm.nodup_iff, And.left, Subtype.property, List.nodup_range, Not, List.cons, Ne, Eq.mp, Prod.mk, Imo2011P4.removePan, congrArg, propext, List.nodup_cons, HAppend.hAppend, List.nodup_append, List.map_cons, List.map_append, Imo2011P4.ways_split and 8 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma ways_fst_pos {n : ℕ} (w : Ways (n + 1)) :
    (∀ p ∈ w.1.take (removeIdx w), 1 ≤ p.1) ∧
    (∀ p ∈ w.1.drop (removeIdx w + 1), 1 ≤ p.1) := by
…
```
Mentions: Imo2011P4.Ways, Imo2011P4.removeIdx
abbrev Imo2011P4.removeList The list of placements with the 2^0 weight removed and the remaining weights halved line 284 source
Source documentation
The list of placements with the 2^0 weight removed and the remaining weights halved.

standard axioms: propext what this means
Statement uses: Nat, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, List, Prod, Bool
Proof uses: List.map, Prod.mk, HSub.hSub, Prod.fst, Prod.snd, HAppend.hAppend, List.take, Imo2011P4.removeIdx, And, List.Perm, List.range, Imo2011P4.ValidSeq, List.drop
11 instances, coercions and auxiliary constants left out.
```
abbrev removeList {n : ℕ} (w : Ways (n + 1)) : List (ℕ × Bool) :=
…
```
Mentions: Imo2011P4.Ways
abbrev Imo2011P4.insertList Inserting a fresh 2^0 weight at position k on pan b into a list of placements whose weights are all doubled line 289 source
Source documentation
Inserting a fresh 2^0 weight at position k on pan b into a list of placements whose weights are all doubled.

no axioms what this means
Statement uses: List, Prod, Nat, Bool
Proof uses: HAppend.hAppend, List.take, List.map, Prod.mk, HAdd.hAdd, Prod.fst, OfNat.ofNat, Prod.snd, List.cons, List.drop
5 instances, coercions and auxiliary constants left out.
```
abbrev insertList (lr : List (ℕ × Bool)) (k : ℕ) (b : Bool) : List (ℕ × Bool) :=
…
```
lemma Imo2011P4.validSeq_remove Documented declaration: validSeq_remove line 296 source
Source documentation
Removing the weight 2^0 and halving preserves validity: before the removed weight the imbalances are unchanged, and afterwards the (even) imbalance without the ±1 contribution can only drop by 1, so it stays nonnegative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, List, Prod, Nat, Membership.mem, LE.le, OfNat.ofNat, Prod.fst, Imo2011P4.ValidSeq, HAppend.hAppend, List.cons, Prod.mk, List.map, HSub.hSub, Prod.snd
Proof uses: List.IsPrefix, Or.elim, Iff.mp, Or, List.mem_append, Eq, List.take, List.length, List.prefix_iff_eq_take, Eq.mpr, id, congrArg, Eq.symm, List.map_take, Eq.refl, rfl, List.IsPrefix.subset, List.take_prefix, Int, HMul.hMul and 39 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
lemma validSeq_remove {b : Bool} {l₁ l₂ : List (ℕ × Bool)}
    (hfst₁ : ∀ p ∈ l₁, 1 ≤ p.1) (hfst₂ : ∀ p ∈ l₂, 1 ≤ p.1)
    (hval : ValidSeq (l₁ ++ (0, b) :: l₂)) :
    ValidSeq ((l₁ ++ l₂).map fun p : ℕ × Bool ↦ (p.1 - 1, p.2)) := by
…
```
Mentions: Imo2011P4.ValidSeq
lemma Imo2011P4.removeList_perm line 337 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, List.Perm, List.map, Prod, Bool, Prod.fst, Imo2011P4.removeList, List.range
Proof uses: And, Membership.mem, List, List.take, Imo2011P4.removeIdx, Imo2011P4.ValidSeq, LE.le, List.drop, Imo2011P4.ways_fst_pos, HAppend.hAppend, List.erase, List.Perm.erase, And.left, Subtype.property, Not, Eq, Exists, False, Iff.mp, List.mem_map and 26 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P4.removeList_valid line 369 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, Imo2011P4.ValidSeq, Imo2011P4.removeList
Proof uses: HAppend.hAppend, List, Prod, Bool, List.take, Imo2011P4.removeIdx, And, List.Perm, List.map, Prod.fst, List.range, List.cons, Prod.mk, Imo2011P4.removePan, List.drop, Eq.mpr, id, Eq, congrArg, Eq.symm and 8 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P4.validSeq_insert Documented declaration: validSeq_insert line 380 source
Source documentation
Inserting the weight 2^0 into a valid sequence of doubled weights preserves validity: prefixes before the insertion point keep their (nonnegative, doubled) imbalance; later prefixes have imbalance 2d ± 1 with d ≥ 0, and when the new weight goes on the right pan the insertion is not at the beginning, so d ≠ 0 (a nonempty signed sum of distinct powers of two), hence d ≥ 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Nat, Bool, List.Nodup, List.map, Prod.fst, Imo2011P4.ValidSeq, LE.le, List.length, Eq, Bool.false, OfNat.ofNat, Imo2011P4.insertList
Proof uses: id, List.IsPrefix, HAppend.hAppend, List.take, Prod.mk, HAdd.hAdd, Prod.snd, List.cons, List.drop, Exists, And, Or, Int, Imo2011P4.Balance, Imo2011P4.prefix_append_cases, List.IsPrefix.trans, List.take_prefix, Iff.mp, List.prefix_iff_eq_take, Eq.mpr and 34 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
```
lemma validSeq_insert {lr : List (ℕ × Bool)} (hnd : (lr.map Prod.fst).Nodup)
    (hval : ValidSeq lr) {k : ℕ} (hk : k ≤ lr.length) {b : Bool} (hb : b = false → 1 ≤ k) :
    ValidSeq (insertList lr k b) := by
…
```
Mentions: Imo2011P4.ValidSeq, Imo2011P4.insertList
lemma Imo2011P4.insertZero_perm line 439 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, List, Prod, Bool, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.insertList, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq, Prod.mk, Prod.snd, Nat.succ, Eq.mpr, Function.comp, id, congrArg, List.map_map, Eq.rec, Eq.refl, Trans.trans, List.cons, HAppend.hAppend, List.take, List.drop, List.map_append, List.map_cons, List.perm_middle, List.take_append_drop and 4 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
abbrev Imo2011P4.IData The insertion data: where and on which pan the weight 2^0 is inserted line 464 source
Source documentation
The insertion data: where and on which pan the weight 2^0 is inserted. Sum.inl k (with k : Fin (n + 1)) inserts it on the left pan at position k; Sum.inr k (with k : Fin n) inserts it on the right pan at position k + 1 (the right pan is forbidden at the very beginning).

no axioms what this means
Statement uses: Nat
Proof uses: Sum, Fin, HAdd.hAdd, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
abbrev IData (n : ℕ) : Type := Fin (n + 1) ⊕ Fin n
```
lemma Imo2011P4.removePan_false_idx The weight 2^0 cannot be the first placement if it goes on the right pan line 468 source
Source documentation
The weight 2^0 cannot be the first placement if it goes on the right pan.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, Eq, Bool, Imo2011P4.removePan, Bool.false, LE.le, Imo2011P4.removeIdx
Proof uses: Decidable.byContradiction, Not, Eq.mp, LT.lt, List, Prod, And, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.ValidSeq, HAppend.hAppend, List.take, List.cons, Prod.mk, List.drop, Imo2011P4.ways_split, List.IsPrefix, List.nil and 27 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma removePan_false_idx {n : ℕ} (w : Ways (n + 1)) (hp : removePan w = false) :
    1 ≤ removeIdx w := by
…
```
Mentions: Imo2011P4.Ways, Imo2011P4.removePan, Imo2011P4.removeIdx
def Imo2011P4.removeZeroWays The valid sequence obtained by removing the weight 2^0 and halving line 480 source
Source documentation
The valid sequence obtained by removing the weight 2^0 and halving.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat
Proof uses: Subtype.mk, List, Prod, Bool, And, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.ValidSeq, Imo2011P4.removeList
7 instances, coercions and auxiliary constants left out.
```
def removeZeroWays {n : ℕ} (w : Ways (n + 1)) : Ways n :=
…
```
Mentions: Imo2011P4.Ways
def Imo2011P4.removeZeroData The insertion data describing where the weight 2^0 sits in a valid sequence line 485 source
Source documentation
The insertion data describing where the weight 2^0 sits in a valid sequence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, Imo2011P4.IData
Proof uses: dite, Eq, Bool, Imo2011P4.removePan, Bool.true, Sum.inl, Fin, Fin.mk, Imo2011P4.removeIdx, Not, Sum.inr, HSub.hSub
11 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
def removeZeroData {n : ℕ} (w : Ways (n + 1)) : IData n :=
…
```
Mentions: Imo2011P4.Ways, Imo2011P4.IData
def Imo2011P4.insertZeroWays The valid sequence obtained by inserting the weight 2^0 according to the given insertion data line 502 source
Source documentation
The valid sequence obtained by inserting the weight 2^0 according to the given insertion data.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, Imo2011P4.IData, HAdd.hAdd, OfNat.ofNat
Proof uses: Sum.rec, Fin, Sum, Subtype.mk, List, Prod, Bool, And, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.ValidSeq, Imo2011P4.insertList, Bool.true, Bool.false
10 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def insertZeroWays {n : ℕ} (w : Ways n) (d : IData n) : Ways (n + 1) :=
…
```
Mentions: Imo2011P4.Ways, Imo2011P4.IData
lemma Imo2011P4.insertZeroWays_inl_val line 511 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, Fin, HAdd.hAdd, OfNat.ofNat, Eq, List, Prod, Bool, And, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.ValidSeq, Imo2011P4.insertZeroWays, Sum.inl, Imo2011P4.insertList, Bool.true
Proof uses: rfl
9 instances, coercions and auxiliary constants left out.
lemma Imo2011P4.insertZeroWays_inr_val line 514 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, Fin, Eq, List, Prod, Bool, And, List.Perm, List.map, Prod.fst, List.range, HAdd.hAdd, OfNat.ofNat, Imo2011P4.ValidSeq, Imo2011P4.insertZeroWays, Sum.inr, Imo2011P4.insertList, Bool.false
Proof uses: rfl
9 instances, coercions and auxiliary constants left out.
lemma Imo2011P4.insertList_removeList Removal followed by insertion reconstructs the original sequence line 518 source
Source documentation
Removal followed by insertion reconstructs the original sequence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, Eq, List, Prod, Bool, Imo2011P4.insertList, Imo2011P4.removeList, Imo2011P4.removeIdx, Imo2011P4.removePan, And, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.ValidSeq
Proof uses: Membership.mem, List.take, LE.le, List.drop, Imo2011P4.ways_fst_pos, List.length, Eq.mpr, Min.min, id, congrArg, List.length_take, min_eq_left, le_of_lt, Imo2011P4.ways_findIdx_lt, HAppend.hAppend, Prod.mk, Prod.snd, List.cons, HSub.hSub, Imo2011P4.map_up_map_down and 11 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma insertList_removeList {n : ℕ} (w : Ways (n + 1)) :
    insertList (removeList w) (removeIdx w) (removePan w) = w.1 := by
…
```
Mentions: Imo2011P4.Ways, Imo2011P4.insertList, Imo2011P4.removeList, Imo2011P4.removeIdx, Imo2011P4.removePan
lemma Imo2011P4.insertList_getElem The element of an inserted list at the insertion position is the new 2^0 weight line 536 source
Source documentation
The element of an inserted list at the insertion position is the new 2^0 weight.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, LE.le, List.length, Prod, Bool, List, And, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.ValidSeq, LT.lt, Imo2011P4.insertList, Eq, GetElem.getElem, Prod.mk, OfNat.ofNat
Proof uses: id, Eq.mpr, HAppend.hAppend, List.take, HAdd.hAdd, Prod.snd, List.cons, List.drop, HSub.hSub, Min.min, congrFun', congrArg, Eq.trans, List.length_take, List.length_map, List.getElem_append_right, of_eq_true, True, GetElem.getElem.congr_simp, Eq.refl and 1 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma insertList_getElem {n : ℕ} (w : Ways n) {k : ℕ} (hk : k ≤ w.1.length) (b : Bool)
    (h : k < (insertList w.1 k b).length) : (insertList w.1 k b)[k]'h = (0, b) := by
…
```
Mentions: Imo2011P4.Ways, h, Imo2011P4.insertList
lemma Imo2011P4.insertList_findIdx The position of the 2^0 weight in an inserted list is exactly the insertion position line 546 source
Source documentation
The position of the 2^0 weight in an inserted list is exactly the insertion position.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2011P4.Ways, LE.le, List.length, Prod, Bool, List, And, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.ValidSeq, Eq, List.findIdx, BEq.beq, OfNat.ofNat, Imo2011P4.insertList
Proof uses: HAdd.hAdd, id, Eq.mpr, HAppend.hAppend, List.take, Prod.mk, Prod.snd, List.cons, List.drop, congrArg, List.length_append, List.length_cons, Min.min, List.length_take, HSub.hSub, List.length_drop, List.length_map, LT.lt, Iff.mpr, GetElem.getElem and 17 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma insertList_findIdx {n : ℕ} (w : Ways n) {k : ℕ} (hk : k ≤ w.1.length) (b : Bool) :
    (insertList w.1 k b).findIdx (fun p ↦ p.1 == 0) = k := by
…
```
Mentions: Imo2011P4.Ways, Imo2011P4.insertList
def Imo2011P4.stepEquiv The key bijection: valid sequences for n + 1 weights correspond to valid sequences for n weights together with insertion data for the weight 2^0 line 571 source
Source documentation
The key bijection: valid sequences for n + 1 weights correspond to valid sequences for n weights together with insertion data for the weight 2^0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, Prod, Imo2011P4.IData
Proof uses: Equiv.mk, Prod.mk, Imo2011P4.removeZeroWays, Imo2011P4.removeZeroData, Imo2011P4.insertZeroWays, Prod.fst, Prod.snd
8 instances, coercions and auxiliary constants left out.

Tactic trace: 111 steps
Open to load the checked before-and-after goal states.
```
def stepEquiv (n : ℕ) : Ways (n + 1) ≃ Ways n × IData n where
…
```
Mentions: Imo2011P4.Ways, Imo2011P4.IData
lemma Imo2011P4.card_idata line 679 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Nat.card, Imo2011P4.IData, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: id, Eq.mpr, Sum, Fin, congrArg, Nat.card_sum, Nat.card_fin, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_add_lt and 13 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P4.card_ways_zero line 684 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Nat.card, Imo2011P4.Ways, OfNat.ofNat
Proof uses: Eq.mpr, And, Subsingleton, Nonempty, id, congrArg, propext, Nat.card_eq_one_iff_unique, And.intro, Subsingleton.intro, Subtype.ext, List, Prod, Bool, List.Perm, List.map, Prod.fst, List.range, Imo2011P4.ValidSeq, List.nil and 16 more
6 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P4.card_ways_succ line 702 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Nat.card, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, HMul.hMul
Proof uses: Eq.mpr, Prod, Imo2011P4.IData, id, congrArg, Nat.card_congr, Imo2011P4.stepEquiv, Nat.card_prod, Imo2011P4.card_idata, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 13 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P4.card_ways line 707 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Nat.card, Imo2011P4.Ways, HAdd.hAdd, OfNat.ofNat, Nat.doubleFactorial, HMul.hMul
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, Imo2011P4.card_ways_succ, Imo2011P4.card_ways_zero, Eq.refl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_mul and 12 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
determine Imo2011P4.solution_value line 717 source
no axioms what this means
Statement uses: Nat
Proof uses: Nat.doubleFactorial, HSub.hSub, HMul.hMul, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
problem Imo2011P4.imo2011_p4 line 719 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Nat.card, Imo2011P4.Ways, Imo2011P4.solution_value
Proof uses: Nat.succ, Exists, Nat.exists_eq_succ_of_ne_zero, LT.lt.ne', id, HSub.hSub, HMul.hMul, HAdd.hAdd, Eq.mpr, Nat.doubleFactorial, congrArg, Imo2011P4.card_ways, Eq.symm
14 instances, coercions and auxiliary constants left out.

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