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

31 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2019, Problem 5

Let n be a positive integer. Harry has n coins lined up on his desk, which can show either heads or tails. He does the following operation: if there are k > 0 coins which show heads, then he flips the kth coin over; otherwise he stops the process. (For example, the process starting with THT would be THT → HHT → HTT → TTT, which takes three steps.)

Prove the process will always terminate, and determine the average number of steps this takes over all 2ⁿ configurations.

Imports (17)

Imported by 1 file

Compfiles.lean

def Imo2019P5.numHeads The number of coins showing heads in a configuration of n coins line 53 source
Source documentation
The number of coins showing heads in a configuration of n coins. A configuration is a function Fin n → Bool, where c i = true means that the i-th coin from the left (starting the count at 0) shows heads.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool
Proof uses: Finset.card, Finset.filter, Eq, Bool.true, Finset.univ
2 instances, coercions and auxiliary constants left out.
```
def numHeads {n : ℕ} (c : Fin n → Bool) : ℕ :=
…
```
def Imo2019P5.flipIx The index of the coin that Harry flips in configuration c: the k-th coin from the left, where k is the number of heads line 58 source
Source documentation
The index of the coin that Harry flips in configuration c: the k-th coin from the left, where k is the number of heads.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Ne, Imo2019P5.numHeads, OfNat.ofNat
Proof uses: Fin.mk, HSub.hSub
5 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def flipIx {n : ℕ} (c : Fin n → Bool) (h : numHeads c ≠ 0) : Fin n :=
…
```
Mentions: h, Imo2019P5.numHeads
def Imo2019P5.step One step of Harry's process: if there are k > 0 heads, flip the k-th coin from the left; otherwise (all coins show tails) do nothing line 65 source
Source documentation
One step of Harry's process: if there are k > 0 heads, flip the k-th coin from the left; otherwise (all coins show tails) do nothing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool
Proof uses: dite, Eq, Imo2019P5.numHeads, OfNat.ofNat, Not, Function.update, Imo2019P5.flipIx, Bool.not
3 instances, coercions and auxiliary constants left out.
```
def step {n : ℕ} (c : Fin n → Bool) : Fin n → Bool :=
…
```
def Imo2019P5.weightedSum The sum of the 1-based positions of the coins showing heads line 71 source
Source documentation
The sum of the 1-based positions of the coins showing heads.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool
Proof uses: Finset.sum, Finset.univ, HMul.hMul, HAdd.hAdd, OfNat.ofNat, ite, Eq, Bool.true
9 instances, coercions and auxiliary constants left out.
```
def weightedSum {n : ℕ} (c : Fin n → Bool) : ℕ :=
…
```
def Imo2019P5.meas The measure of a configuration: twice the sum of the 1-based positions of the heads minus the square of the number of heads line 78 source
Source documentation
The measure of a configuration: twice the sum of the 1-based positions of the heads minus the square of the number of heads. We will show that this is a nonnegative integer (see meas_nonneg) which drops by exactly one at each step (see step_meas), hence it equals the number of steps the process takes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Int
Proof uses: HSub.hSub, HMul.hMul, OfNat.ofNat, Imo2019P5.weightedSum, HPow.hPow, Imo2019P5.numHeads
12 instances, coercions and auxiliary constants left out.
```
def meas {n : ℕ} (c : Fin n → Bool) : ℤ :=
…
```
determine Imo2019P5.L The number of steps that Harry's process takes starting from configuration c line 85 source
Source documentation
The number of steps that Harry's process takes starting from configuration c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool
Proof uses: Int.toNat, Imo2019P5.meas
```
determine L {n : ℕ} (c : Fin n → Bool) : ℕ := (meas c).toNat
…
```
Mentions: Imo2019P5.meas
theorem Imo2019P5.le_orderEmbOfFin The j-th smallest element of a finset S of Fin n is at least j line 90 source
Source documentation
The j-th smallest element of a finset S of Fin n is at least j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Finset.card, LE.le, OrderEmbedding, Finset.orderEmbOfFin, rfl
Proof uses: Finset.map, RelEmbedding.toEmbedding, Finset.Iio, Membership.mem, And, Eq, Function.Embedding, Exists, Eq.mp, congrArg, propext, Finset.mem_map, Eq.mpr, LT.lt, id, Finset.mem_Iio, Iff.mpr, OrderEmbedding.lt_iff_lt, Trans.trans, Eq.symm and 3 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem le_orderEmbOfFin {n : ℕ} (S : Finset (Fin n)) (j : Fin S.card) :
    (j : ℕ) ≤ (S.orderEmbOfFin rfl j).val := by
…
```
Mentions: S
theorem Imo2019P5.sum_range_card_le For a finset S of Fin n, the sum of the values of its elements is at least card S * (card S - 1) / 2 (twice that sum, to stay in ℕ) line 106 source
Source documentation
For a finset S of Fin n, the sum of the values of its elements is at least card S * (card S - 1) / 2 (twice that sum, to stay in ℕ).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, LE.le, HMul.hMul, Finset.card, HSub.hSub, OfNat.ofNat, Finset.sum
Proof uses: OrderEmbedding, Finset.orderEmbOfFin, rfl, Imo2019P5.le_orderEmbOfFin, Eq, Finset.univ, Eq.mpr, Finset.map, RelEmbedding.toEmbedding, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, Finset.map_orderEmbOfFin_univ, Function.Embedding, Finset.sum_map, of_eq_true, RelEmbedding and 71 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem sum_range_card_le {n : ℕ} (S : Finset (Fin n)) :
    S.card * (S.card - 1) ≤ 2 * ∑ i ∈ S, (i : ℕ) := by
…
```
Mentions: S
theorem Imo2019P5.numHeads_mul_succ_le The key combinatorial estimate: if a configuration has k heads, then the sum of the 1-based positions of the heads is at least k * (k + 1) / 2 line 124 source
Source documentation
The key combinatorial estimate: if a configuration has k heads, then the sum of the 1-based positions of the heads is at least k * (k + 1) / 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, LE.le, HMul.hMul, Imo2019P5.numHeads, HAdd.hAdd, OfNat.ofNat, Imo2019P5.weightedSum
Proof uses: Finset.card, Finset.filter, Eq, Bool.true, Finset.univ, HSub.hSub, Finset.sum, Imo2019P5.sum_range_card_le, Eq.mpr, ite, id, congrArg, Imo2019P5.weightedSum.eq_1, Finset.sum_filter, Finset.sum_congr, rfl, Finset, Membership.mem, dite, of_eq_true and 85 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
theorem numHeads_mul_succ_le {n : ℕ} (c : Fin n → Bool) :
    numHeads c * (numHeads c + 1) ≤ 2 * weightedSum c := by
…
```
Mentions: Imo2019P5.numHeads, Imo2019P5.weightedSum
theorem Imo2019P5.meas_def line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Int, Imo2019P5.meas, HSub.hSub, HMul.hMul, OfNat.ofNat, Imo2019P5.weightedSum, HPow.hPow, Imo2019P5.numHeads
Proof uses: rfl
12 instances, coercions and auxiliary constants left out.
theorem Imo2019P5.meas_nonneg line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, LE.le, Int, OfNat.ofNat, Imo2019P5.meas
Proof uses: HMul.hMul, Imo2019P5.numHeads, HAdd.hAdd, Imo2019P5.weightedSum, Imo2019P5.numHeads_mul_succ_le, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_one, congr, Int.natCast_nonneg, id, le_of_not_gt, HSub.hSub, HPow.hPow, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp and 63 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P5.meas_ge_numHeads line 156 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, LE.le, Int, Imo2019P5.numHeads, Imo2019P5.meas
Proof uses: HMul.hMul, HAdd.hAdd, OfNat.ofNat, Imo2019P5.weightedSum, Imo2019P5.numHeads_mul_succ_le, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_one, congr, id, le_of_not_gt, HSub.hSub, HPow.hPow, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg and 61 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P5.meas_eq_zero_iff line 163 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Iff, Eq, Int, Imo2019P5.meas, OfNat.ofNat, Imo2019P5.numHeads
Proof uses: Iff.intro, LE.le, Imo2019P5.meas_ge_numHeads, Int.natCast_nonneg, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HMul.hMul and 79 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P5.numHeads_cast The number of heads as a sum of indicators, in ℤ line 187 source
Source documentation
The number of heads as a sum of indicators, in ℤ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Int, Imo2019P5.numHeads, Finset.sum, Finset.univ, ite, Bool.true, OfNat.ofNat
Proof uses: Finset.card_filter, cast, Eq.symm, Eq.trans, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, ite_congr, Nat.cast_one, Not, Nat.cast_zero
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem numHeads_cast {n : ℕ} (c : Fin n → Bool) :
    (numHeads c : ℤ) = ∑ i : Fin n, (if c i then (1 : ℤ) else 0) := by
…
```
Mentions: Imo2019P5.numHeads
theorem Imo2019P5.weightedSum_cast The weighted sum as a sum over all positions, in ℤ line 194 source
Source documentation
The weighted sum as a sum over all positions, in ℤ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Int, Imo2019P5.weightedSum, Finset.sum, Finset.univ, HMul.hMul, HAdd.hAdd, OfNat.ofNat, ite, Bool.true
Proof uses: Eq.mpr, id, congrArg, Imo2019P5.weightedSum.eq_1, Nat.cast_sum, Finset.sum_congr, rfl, Finset, Membership.mem, dite, of_eq_true, Eq.trans, True, congr, ite_eq_left_of_eq_true, congrFun', eq_self, mul_one, Nat.cast_add, Nat.cast_one and 8 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem weightedSum_cast {n : ℕ} (c : Fin n → Bool) :
    (weightedSum c : ℤ) = ∑ i : Fin n, ((i : ℕ) + 1 : ℤ) * (if c i then (1 : ℤ) else 0) := by
…
```
Mentions: Imo2019P5.weightedSum
theorem Imo2019P5.headsZ_update How the head-count sum changes when coin p is flipped line 202 source
Source documentation
How the head-count sum changes when coin p is flipped.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Int, Finset.sum, Finset.univ, ite, Function.update, Bool.not, Bool.true, OfNat.ofNat, HAdd.hAdd, Neg.neg
Proof uses: funext, dite, of_eq_true, Eq.trans, True, congr, congrArg, ite_eq_right_of_eq_false, Bool.false, False, congrFun', Function.update_congr, Eq.refl, Bool.not_true, Function.update_self, Bool.false_eq_true, ite_eq_left_of_eq_true, eq_self, Not, id and 47 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem headsZ_update {n : ℕ} (c : Fin n → Bool) (p : Fin n) :
    ∑ i : Fin n, (if Function.update c p (!c p) i then (1 : ℤ) else 0)
      = (∑ i : Fin n, (if c i then (1 : ℤ) else 0)) + (if c p then (-1 : ℤ) else 1) := by
…
```
theorem Imo2019P5.weightedZ_update How the weighted sum changes when coin p is flipped line 220 source
Source documentation
How the weighted sum changes when coin p is flipped.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Int, Finset.sum, Finset.univ, HMul.hMul, HAdd.hAdd, OfNat.ofNat, ite, Function.update, Bool.not, Bool.true, Neg.neg
Proof uses: funext, dite, of_eq_true, Eq.trans, True, congr, congrArg, ite_eq_right_of_eq_false, Bool.false, False, congrFun', Function.update_congr, Eq.refl, Bool.not_true, Function.update_self, Bool.false_eq_true, MulZeroClass.mul_zero, mul_ite, ite_congr, mul_one and 60 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem weightedZ_update {n : ℕ} (c : Fin n → Bool) (p : Fin n) :
    ∑ i : Fin n, ((i : ℕ) + 1 : ℤ) * (if Function.update c p (!c p) i then (1 : ℤ) else 0)
      = (∑ i : Fin n, ((i : ℕ) + 1 : ℤ) * (if c i then (1 : ℤ) else 0))
        + ((p : ℕ) + 1 : ℤ) * (if c p then (-1 : ℤ) else 1) := by
…
```
theorem Imo2019P5.step_meas The measure drops by exactly one at each step line 240 source
Source documentation
The measure drops by exactly one at each step.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Ne, Imo2019P5.numHeads, OfNat.ofNat, Eq, Int, Imo2019P5.meas, Imo2019P5.step, HSub.hSub
Proof uses: Function.update, Imo2019P5.flipIx, Bool.not, id, Eq.mpr, dite, Not, congrArg, dite_eq_right, Eq.refl, rfl, HAdd.hAdd, LT.lt, Nat.pos_of_ne_zero, Finset.sum, Finset.univ, ite, Bool.true, Eq.symm, Imo2019P5.numHeads_cast and 89 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
theorem step_meas {n : ℕ} (c : Fin n → Bool) (h : numHeads c ≠ 0) :
    meas (step c) = meas c - 1 := by
…
```
Mentions: h, Imo2019P5.numHeads, Imo2019P5.meas, Imo2019P5.step
theorem Imo2019P5.iter_meas After m steps with m ≤ meas c, the measure has dropped by exactly m line 262 source
Source documentation
After m steps with m ≤ meas c, the measure has dropped by exactly m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, LE.le, Int, Imo2019P5.meas, Eq, Nat.iterate, Imo2019P5.step, HSub.hSub
Proof uses: Nat.recAux, OfNat.ofNat, of_eq_true, Eq.trans, True, congrArg, CharP.cast_eq_zero, sub_zero, eq_self, HAdd.hAdd, cast, Eq.symm, congrFun', Nat.cast_one, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, Neg.neg and 63 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem iter_meas {n : ℕ} (c : Fin n → Bool) (m : ℕ) (hm : (m : ℤ) ≤ meas c) :
    meas (step^[m] c) = meas c - (m : ℤ) := by
…
```
Mentions: Imo2019P5.meas, Imo2019P5.step
theorem Imo2019P5.iterate_L The process from c stops after exactly L c steps in the all-tails configuration line 281 source
Source documentation
The process from c stops after exactly L c steps in the all-tails configuration.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Nat.iterate, Imo2019P5.step, Imo2019P5.L, Bool.false
Proof uses: Int, Imo2019P5.meas, Int.toNat_of_nonneg, Imo2019P5.meas_nonneg, HSub.hSub, Imo2019P5.iter_meas, le_of_eq, OfNat.ofNat, Eq.mpr, id, congrArg, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 46 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem iterate_L {n : ℕ} (c : Fin n → Bool) : step^[L c] c = fun _ ↦ false := by
…
```
Mentions: Imo2019P5.step, Imo2019P5.L
theorem Imo2019P5.not_iterate_lt_L Before step L c, the process has not stopped yet line 298 source
Source documentation
Before step L c, the process has not stopped yet.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, LT.lt, Imo2019P5.L, Ne, Nat.iterate, Imo2019P5.step, Bool.false
Proof uses: Eq, Int, Imo2019P5.meas, Int.toNat_of_nonneg, Imo2019P5.meas_nonneg, LE.le, cast, Eq.symm, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast and 75 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
theorem not_iterate_lt_L {n : ℕ} (c : Fin n → Bool) {m : ℕ} (hm : m < L c) :
    step^[m] c ≠ fun _ ↦ false := by
…
```
Mentions: Imo2019P5.L, Imo2019P5.step
theorem Imo2019P5.card_filter_true_eq_card_filter_false Configurations with a head at position i are in bijection with those with a tail at position i, by flipping coin i line 324 source
Source documentation
Configurations with a head at position i are in bijection with those with a tail at position i, by flipping coin i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset.card, Bool, Finset.filter, Bool.true, Finset.univ, Bool.false
Proof uses: Finset.card_bij', Membership.mem, Finset, Function.update, Bool.not, Iff.mpr, And, Finset.mem_filter, And.intro, Finset.mem_univ, And.right, Iff.mp, of_eq_true, Eq.trans, True, congrFun', congrArg, Function.update_congr, Eq.refl, Bool.not_true and 9 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem card_filter_true_eq_card_filter_false {n : ℕ} (i : Fin n) :
    (univ.filter fun c : Fin n → Bool ↦ c i = true).card
      = (univ.filter fun c : Fin n → Bool ↦ c i = false).card := by
…
```
theorem Imo2019P5.card_filter_true Exactly half of all 2 ^ n configurations have a head at position i line 348 source
Source documentation
Exactly half of all 2 ^ n configurations have a head at position i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Eq, Finset.card, Bool, Finset.filter, Bool.true, Finset.univ, HPow.hPow, HSub.hSub
Proof uses: Bool.false, Imo2019P5.card_filter_true_eq_card_filter_false, HAdd.hAdd, Not, Finset.card_filter_add_card_filter_not, Finset, Finset.ext, Eq.mpr, Iff, Membership.mem, id, congr, congrArg, Eq.trans, And, True, congrFun', true_and, of_eq_true, False and 23 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
theorem card_filter_true {n : ℕ} (hn : 0 < n) (i : Fin n) :
    (univ.filter fun c : Fin n → Bool ↦ c i = true).card = 2 ^ (n - 1) := by
…
```
theorem Imo2019P5.two_mul_card_filter_pair Twice the number of configurations with heads at both i and j equals 2 ^ (n - 1) line 376 source
Source documentation
Twice the number of configurations with heads at both i and j equals 2 ^ (n - 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Ne, Eq, HMul.hMul, Finset.card, Bool, Finset.filter, And, Bool.true, Finset.univ, HPow.hPow, HSub.hSub
Proof uses: Bool.false, Finset.card_bij', Membership.mem, Finset, Function.update, Bool.not, Iff.mpr, Finset.mem_filter, And.intro, Finset.mem_univ, And.right, Iff.mp, Eq.mpr, id, congrArg, Function.update_of_ne, And.left, of_eq_true, Eq.trans, True and 31 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
theorem two_mul_card_filter_pair {n : ℕ} (hn : 0 < n) {i j : Fin n} (hij : i ≠ j) :
    2 * (univ.filter fun c : Fin n → Bool ↦ c i = true ∧ c j = true).card = 2 ^ (n - 1) := by
…
```
theorem Imo2019P5.card_filter_pair The number of configurations with heads at both i and j is 2 ^ (n - 2) line 423 source
Source documentation
The number of configurations with heads at both i and j is 2 ^ (n - 2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Ne, Eq, Finset.card, Bool, Finset.filter, And, Bool.true, Finset.univ, HPow.hPow, HSub.hSub
Proof uses: HMul.hMul, Imo2019P5.two_mul_card_filter_pair, LE.le, Iff.mp, Nontrivial, Fin.nontrivial_iff_two_le, nontrivial_of_ne, HAdd.hAdd, Eq.mpr, id, congrArg, pow_succ, mul_comm, Nat.mul_left_cancel, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool.false, Eq.mp
48 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem card_filter_pair {n : ℕ} (hn : 0 < n) {i j : Fin n} (hij : i ≠ j) :
    (univ.filter fun c : Fin n → Bool ↦ c i = true ∧ c j = true).card = 2 ^ (n - 2) := by
…
```
theorem Imo2019P5.sum_indicator The sum of the indicator of heads at position i over all configurations line 435 source
Source documentation
The sum of the indicator of heads at position i over all configurations.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Eq, Int, Finset.sum, Bool, Finset.univ, ite, Bool.true, HPow.hPow, HSub.hSub
Proof uses: Finset.card, Finset.filter, Imo2019P5.card_filter_true, Finset.card_filter, cast, Eq.symm, Eq.trans, congrFun', congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, ite_congr, Nat.cast_one, Not, Nat.cast_zero, congr, Eq.mp
56 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem sum_indicator {n : ℕ} (hn : 0 < n) (i : Fin n) :
    ∑ c : Fin n → Bool, (if c i then (1 : ℤ) else 0) = 2 ^ (n - 1) := by
…
```
theorem Imo2019P5.sum_four_L The total of L over all configurations is 2 ^ n * n * (n + 1) / 4; we prove four times that value to stay in ℤ line 444 source
Source documentation
The total of L over all configurations is 2 ^ n * n * (n + 1) / 4; we prove four times that value to stay in ℤ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Int, HMul.hMul, Finset.sum, Fin, Bool, Finset.univ, Imo2019P5.L, HPow.hPow, HAdd.hAdd
Proof uses: ite, Bool.true, HSub.hSub, Imo2019P5.sum_indicator, rfl, Eq.mpr, id, congrArg, Finset.sum_add_distrib, of_eq_true, Eq.trans, True, congrFun', HSMul.hSMul, Finset.card, Finset.sum_const, Fintype.card_fin, mul_one, eq_self, Finset.range and 154 more
170 instances, coercions and auxiliary constants left out.

Tactic trace: 103 steps
Open to load the checked before-and-after goal states.
```
theorem sum_four_L {n : ℕ} (hn : 0 < n) :
    4 * ∑ c : Fin n → Bool, (L c : ℤ) = 2 ^ n * n * (n + 1) := by
…
```
Mentions: Imo2019P5.L
determine Imo2019P5.averageSteps The average number of steps over all 2 ^ n initial configurations line 584 source
Source documentation
The average number of steps over all 2 ^ n initial configurations.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: HDiv.hDiv, HMul.hMul, HAdd.hAdd, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
```
determine averageSteps (n : ℕ) : ℚ := n * (n + 1) / 4
```
problem Imo2019P5.imo2019_p5_parta Part (a): the process always terminates line 587 source
Source documentation
Part (a): the process always terminates.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Exists, Eq, Nat.iterate, Imo2019P5.step, Bool.false
Proof uses: Exists.intro, Imo2019P5.L, Imo2019P5.iterate_L
```
problem imo2019_p5_parta (n : ℕ) (c : Fin n → Bool) :
    ∃ m : ℕ, step^[m] c = fun _ ↦ false :=
…
```
Mentions: Imo2019P5.step
problem Imo2019P5.imo2019_p5_partb_definition Part (b): The number of steps that Harry's process takes starting from configuration c is L line 593 source
Source documentation
Part (b): The number of steps that Harry's process takes starting from configuration c is L

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, IsLeast, Set.ofPred, Eq, Nat.iterate, Imo2019P5.step, Bool.false, Imo2019P5.L
Proof uses: id, And.intro, Membership.mem, Set, lowerBounds, Imo2019P5.iterate_L, Eq.mpr, LE.le, congrArg, propext, mem_lowerBounds, Mathlib.Tactic.Contrapose.contrapose₁, Not, LT.lt, implies_congr, Eq.refl, Imo2019P5.not_iterate_lt_L
10 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
problem imo2019_p5_partb_definition (n : ℕ) (c : Fin n → Bool) :
    IsLeast {m : ℕ| step^[m] c = fun _ ↦ false} (L c) := by
…
```
Mentions: Imo2019P5.step, Imo2019P5.L
problem Imo2019P5.imo2019_p5_partb Part (b): the average number of steps over all 2 ^ n configurations is n * (n + 1) / 4 line 605 source
Source documentation
Part (b): the average number of steps over all 2 ^ n configurations is n * (n + 1) / 4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Rat, HDiv.hDiv, Finset.sum, Fin, Bool, Finset.univ, Imo2019P5.L, HPow.hPow, Imo2019P5.averageSteps
Proof uses: Int, HMul.hMul, HAdd.hAdd, Imo2019P5.sum_four_L, cast, Eq.trans, congrArg, Eq.symm, Nat.cast_one, congr, congrFun', id, Ne, ne_of_gt, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.ble, Eq.mpr and 84 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
problem imo2019_p5_partb (n : ℕ) (hn : 0 < n) :
    (∑ c : Fin n → Bool, (L c : ℚ)) / 2 ^ n = averageSteps n := by
…
```
Mentions: Imo2019P5.L, Imo2019P5.averageSteps