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

100 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2022, Problem 1

The bank of Oslo issues two types of coin: aluminum (denoted A) and bronze (denoted B). Marianne has n aluminum coins and n bronze coins arranged in a row in some arbitrary initial order. A chain is any subsequence of consecutive coins of the same type. Given a fixed positive integer k ≤ 2n, Gilberty repeatedly performs the following operation: he identifies the longest chain containing the kth coin from the left and moves all the coins in that chain to the left end of the row. For example, if n = 4 and k = 4, the process starting from the ordering AABBBABA would be

AABBBABA → BBBAAABA → AAABBBBA → BBBBAAAA → ⋯.

Find all pairs (n,k) with 1 ≤ k ≤ 2n such that for every initial ordering, at some moment in the process, the leftmost n coins will all be of the same type.

Imports (2)

Imported by 1 file

Compfiles.lean

inductive Imo2022P1.Coin The two types of coins line 41 source
Source documentation
The two types of coins.

no axioms what this means
```
inductive Coin : Type where
…
```
abbrev Imo2022P1.Row A row of coins line 47 source
Source documentation
A row of coins.

no axioms what this means
Statement uses: Nat
Proof uses: Fin, HMul.hMul, OfNat.ofNat, Imo2022P1.Coin
3 instances, coercions and auxiliary constants left out.
```
abbrev Row (n : ℕ) : Type := Fin (2 * n) → Coin
```
Mentions: Imo2022P1.Coin
def Imo2022P1.Row.valid The property of a row having n of each kind of coin line 50 source
Source documentation
The property of a row having n of each kind of coin.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P1.Row
Proof uses: Eq, Finset.card, Fin, HMul.hMul, OfNat.ofNat, Finset.filter, Imo2022P1.Coin, Imo2022P1.Coin.A, Finset.univ
5 instances, coercions and auxiliary constants left out.
```
def Row.valid {n : ℕ} (c : Row n) : Prop := #{i | c i = Coin.A} = n
```
Mentions: Imo2022P1.Row
def Imo2022P1.Row.chainLeft The first coin in the chain containing coin k (zero-based) line 53 source
Source documentation
The first coin in the chain containing coin k (zero-based).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P1.Row, Fin, HMul.hMul, OfNat.ofNat
Proof uses: Finset.min', Finset.filter, LE.le, Eq, Imo2022P1.Coin, Finset.Iic
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def Row.chainLeft {n : ℕ} (c : Row n) (k : Fin (2 * n)) : Fin (2 * n) :=
…
```
Mentions: Imo2022P1.Row
def Imo2022P1.Row.chainRight The last coin in the chain containing coin k (zero-based) line 60 source
Source documentation
The last coin in the chain containing coin k (zero-based).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P1.Row, Fin, HMul.hMul, OfNat.ofNat
Proof uses: Finset.max', Finset.filter, LE.le, Eq, Imo2022P1.Coin, Finset.Ici
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def Row.chainRight {n : ℕ} (c : Row n) (k : Fin (2 * n)) : Fin (2 * n) :=
…
```
Mentions: Imo2022P1.Row
def Imo2022P1.Row.move Move coins a through b to the left of the row line 67 source
Source documentation
Move coins a through b to the left of the row.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P1.Row, Fin, HMul.hMul, OfNat.ofNat
Proof uses: ite, Imo2022P1.Coin, LT.lt, Fin.mk, HMod.hMod, HAdd.hAdd
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def Row.move {n : ℕ} (c : Row n) (a b : Fin (2 * n)) : Row n :=
…
```
Mentions: Imo2022P1.Row
def Imo2022P1.Row.operation The operation moving the chain containing coin k (zero-based) line 72 source
Source documentation
The operation moving the chain containing coin k (zero-based).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Imo2022P1.Row
Proof uses: Imo2022P1.Row.move, Imo2022P1.Row.chainLeft, Imo2022P1.Row.chainRight
6 instances, coercions and auxiliary constants left out.
```
def Row.operation {n : ℕ} (k : Fin (2 * n)) (c : Row n) : Row n :=
…
```
Mentions: Imo2022P1.Row
def Imo2022P1.Row.operationOneBased The operation moving the chain containing coin k (one-based) line 76 source
Source documentation
The operation moving the chain containing coin k (one-based).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, Imo2022P1.Row
Proof uses: Imo2022P1.Row.operation, Fin.mk, HSub.hSub
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def Row.operationOneBased {n k : ℕ} (hk1 : 1 ≤ k) (hkn : k ≤ 2 * n) (c : Row n) :
    Row n :=
…
```
Mentions: Imo2022P1.Row
def Imo2022P1.Row.leftmostNSame The property of a row having leftmost n coin with the same type line 81 source
Source documentation
The property of a row having leftmost n coin with the same type.

no axioms what this means
Statement uses: Nat, Imo2022P1.Row
Proof uses: Fin, HMul.hMul, OfNat.ofNat, LT.lt, Eq, Imo2022P1.Coin
5 instances, coercions and auxiliary constants left out.
```
def Row.leftmostNSame {n : ℕ} (c : Row n) := ∀ j₁ j₂ : Fin (2 * n),
…
```
Mentions: Imo2022P1.Row
lemma Imo2022P1.Nat.ceilDiv_two_add_floorDiv_two line 86 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, CeilDiv.ceilDiv, OfNat.ofNat, FloorDiv.floorDiv
Proof uses: Eq.mpr, HDiv.hDiv, HSub.hSub, id, congrArg, Nat.ceilDiv_eq_add_pred_div, Nat.floorDiv_eq_div
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.Coin.flip line 90 source
no axioms what this means
Statement uses: Imo2022P1.Coin
Proof uses: Imo2022P1.Coin.flip.match_1, Unit, Imo2022P1.Coin.B, Imo2022P1.Coin.A
lemma Imo2022P1.Coin.flip_eq_iff line 94 source
no axioms what this means
Statement uses: Imo2022P1.Coin, Iff, Eq, Imo2022P1.Coin.flip, Ne
Proof uses: Imo2022P1.Coin.A, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm, Imo2022P1.Coin.B
5 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Coin.flip_eq_iff' line 97 source
standard axioms: propext what this means
Statement uses: Imo2022P1.Coin, Iff, Eq, Imo2022P1.Coin.flip, Ne
Proof uses: Eq.mpr, id, congrArg, propext, ne_comm, Eq.symm, Imo2022P1.Coin.flip_eq_iff, eq_comm, Iff.rfl

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.isValidRow line 100 source
no axioms what this means
Statement uses: List, Imo2022P1.Coin
Proof uses: Eq, Nat, HMul.hMul, OfNat.ofNat, List.count, Imo2022P1.Coin.A, List.length
5 instances, coercions and auxiliary constants left out.
lemma Imo2022P1.List.count_ofFn line 104 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Nat, Fin, Eq, Finset.card, Finset.filter, Finset.univ, List.count, List.ofFn
Proof uses: Nat.recAux, OfNat.ofNat, Eq.mpr, List.nil, id, congrArg, List, List.ofFn_zero, List.count_nil, Finset, EmptyCollection.emptyCollection, propext, Finset.card_eq_zero, Finset.eq_empty_of_isEmpty, HAdd.hAdd, List.cons, Fin.succ, List.ofFn_succ, ite, Bool and 52 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.sum_rotate line 144 source
standard axioms: Quot.sound, propext what this means
Statement uses: AddCommMonoid, List, Nat, Eq, List.sum, List.rotate
Proof uses: List.Perm.sum_eq, List.rotate_perm
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.splitBy_append' line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, List, Exists, And, Membership.mem, Option, List.getLast?, List.head?, Eq, Bool.true, List.splitBy, HAppend.hAppend, List.dropLast, List.cons, Option.getD, List.nil, List.tail
Proof uses: Ne, Mathlib.Tactic.Contrapose.contrapose₃, Eq.mpr, Not, id, congrArg, Option.none, List.getLast?_nil, Option.not_mem_none, List.head?_nil, Iff.mpr, List.splitBy_ne_nil, Option.some, List.getLast, List.getLast?_eq_some_getLast, Option.getD_some, List.head, List.head?_eq_some_head, List.flatten, List.IsChain and 55 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 127 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.valid_iff_isValidRow_ofFn line 260 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P1.Row, Iff, Imo2022P1.Row.valid, Imo2022P1.isValidRow, List.ofFn, Imo2022P1.Coin, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, Eq, Finset.card, Fin, Finset.filter, Imo2022P1.Coin.A, Finset.univ, id, congrArg, Imo2022P1.Row.valid.eq_1, List.count, List.length, Imo2022P1.isValidRow.eq_1, List.length_ofFn, Or, propext, mul_eq_mul_left_iff, or_iff_left, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat and 5 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.List.chainLeft line 265 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length
Proof uses: Finset.min', Finset.filter, LE.le, Eq, List.get, Finset.Iic
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.chainLeft_eq_chainLeft_ofFn line 271 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P1.Row, Fin, HMul.hMul, OfNat.ofNat, Eq, Imo2022P1.Row.chainLeft, Fin.cast, List.length, Imo2022P1.Coin, List.ofFn, Imo2022P1.List.chainLeft
Proof uses: Eq.mpr, id, congrArg, List.length_ofFn, Eq.refl, Finset.min', Finset.filter, LE.le, Finset.Iic, Imo2022P1.Row.chainLeft.eq_1, List.get, Imo2022P1.List.chainLeft.eq_1, rfl, Monotone, StrictMono.monotone, Fin.cast_strictMono, Finset.image, Finset.Nonempty, propext, Finset.image_nonempty and 36 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.chainLeft_le line 313 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, LE.le, Imo2022P1.List.chainLeft
Proof uses: Eq.mpr, Finset.min', Finset.filter, Eq, List.get, Finset.Iic, id, congrArg, Imo2022P1.List.chainLeft.eq_1, Finset.min'_le, Membership.mem, Finset, Eq.trans, And, True, congrFun', true_and, le_antisymm, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.List.chainRight line 321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length
Proof uses: Finset.max', Finset.filter, LE.le, Eq, List.get, Finset.Ici
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.chainRight_eq_chainRight_ofFn line 327 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P1.Row, Fin, HMul.hMul, OfNat.ofNat, Eq, Imo2022P1.Row.chainRight, Fin.cast, List.length, Imo2022P1.Coin, List.ofFn, Imo2022P1.List.chainRight
Proof uses: Eq.mpr, id, congrArg, List.length_ofFn, Eq.refl, Finset.max', Finset.filter, LE.le, Finset.Ici, Imo2022P1.Row.chainRight.eq_1, List.get, Imo2022P1.List.chainRight.eq_1, rfl, Monotone, StrictMono.monotone, Fin.cast_strictMono, Finset.image, Finset.Nonempty, propext, Finset.image_nonempty and 36 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.le_chainRight line 369 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, LE.le, Imo2022P1.List.chainRight
Proof uses: Eq.mpr, Finset.max', Finset.filter, Eq, List.get, Finset.Ici, id, congrArg, Imo2022P1.List.chainRight.eq_1, Finset.le_max', Membership.mem, Finset, Eq.trans, And, True, congrFun', true_and, le_antisymm, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.chainLeft_le_chainRight line 377 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, LE.le, Imo2022P1.List.chainLeft, Imo2022P1.List.chainRight
Proof uses: le_trans, Imo2022P1.List.chainLeft_le, Imo2022P1.List.le_chainRight
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.List.move line 381 source
no axioms what this means
Statement uses: Nat, List
Proof uses: HAppend.hAppend, List.take, HSub.hSub, HAdd.hAdd, OfNat.ofNat, List.drop
7 instances, coercions and auxiliary constants left out.
lemma Imo2022P1.List.length_move line 384 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, List, Eq, List.length, Imo2022P1.List.move
Proof uses: Eq.mpr, HAppend.hAppend, List.take, HSub.hSub, HAdd.hAdd, OfNat.ofNat, List.drop, id, congrArg, Imo2022P1.List.move.eq_1, List.length_append, Eq.symm, List.take_append_drop, List.drop_drop, Nat.add_sub_cancel'
11 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.count_move line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Nat, LE.le, List, Eq, List.count, Imo2022P1.List.move
Proof uses: Eq.mpr, HAppend.hAppend, List.take, HSub.hSub, HAdd.hAdd, OfNat.ofNat, List.drop, id, congrArg, Imo2022P1.List.move.eq_1, List.count_append, Eq.symm, List.take_append_drop, List.drop_drop, Nat.add_sub_cancel'
13 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.ofFn_move_eq_move_ofFn line 410 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P1.Row, Fin, HMul.hMul, OfNat.ofNat, LE.le, Eq, List, Imo2022P1.Coin, List.ofFn, Imo2022P1.Row.move, Imo2022P1.List.move
Proof uses: Eq.mpr, List.length, List.get, id, congrArg, Eq.symm, List.ofFn_get, Imo2022P1.List.length_move, List.length_ofFn, Eq.refl, Fin.cast, List.ofFn_congr, propext, List.ofFn_inj, funext, LT.lt, Fin.is_lt, ite, Fin.mk, HMod.hMod and 33 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.List.operation line 461 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length
Proof uses: Imo2022P1.List.move, Imo2022P1.List.chainLeft, Imo2022P1.List.chainRight
1 instances, coercions and auxiliary constants left out.
lemma Imo2022P1.Row.ofFn_operation_eq_operation_ofFn line 464 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Imo2022P1.Row, Eq, List, Imo2022P1.Coin, List.ofFn, Imo2022P1.Row.operation, Imo2022P1.List.operation, Fin.cast, List.length
Proof uses: LE.le, Imo2022P1.Row.chainLeft, Imo2022P1.Row.chainRight, Eq.mpr, Imo2022P1.List.chainLeft, id, congrArg, Imo2022P1.Row.chainLeft_eq_chainLeft_ofFn, Imo2022P1.List.chainRight, Imo2022P1.Row.chainRight_eq_chainRight_ofFn, propext, Fin.cast_le_cast, Imo2022P1.List.chainLeft_le_chainRight, Imo2022P1.List.move, Imo2022P1.List.operation.eq_1, Imo2022P1.Row.move, Imo2022P1.Row.operation.eq_1, Imo2022P1.Row.ofFn_move_eq_move_ofFn, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.List.operationOneBased line 474 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Nat, LE.le, OfNat.ofNat, List.length
Proof uses: Imo2022P1.List.operation, Fin.mk, HSub.hSub
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.ofFn_operationOneBased_eq_operationOneBased_ofFn line 478 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, Imo2022P1.Row, Eq, List, Imo2022P1.Coin, List.ofFn, Imo2022P1.Row.operationOneBased, Imo2022P1.List.operationOneBased
Proof uses: Eq.mpr, Imo2022P1.List.operation, Fin.mk, List.length, HSub.hSub, id, congrArg, Imo2022P1.List.operationOneBased.eq_1, Imo2022P1.Row.operation, Imo2022P1.Row.operationOneBased.eq_1, Fin.cast, Imo2022P1.Row.ofFn_operation_eq_operation_ofFn, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.operationOneBased_valid line 486 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P1.Row, Imo2022P1.Row.valid, LE.le, OfNat.ofNat, HMul.hMul, Imo2022P1.Row.operationOneBased
Proof uses: Eq.mpr, Imo2022P1.isValidRow, List.ofFn, Imo2022P1.Coin, id, Eq, congrArg, propext, Imo2022P1.Row.valid_iff_isValidRow_ofFn, Imo2022P1.List.operationOneBased, List, Imo2022P1.Row.ofFn_operationOneBased_eq_operationOneBased_ofFn, Imo2022P1.List.operation, Fin.mk, List.length, HSub.hSub, Imo2022P1.List.operationOneBased.eq_1, Imo2022P1.List.move, Imo2022P1.List.chainLeft, Imo2022P1.List.chainRight and 8 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.operationOneBased_iterate_valid line 494 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P1.Row, Imo2022P1.Row.valid, LE.le, OfNat.ofNat, HMul.hMul, Nat.iterate, Imo2022P1.Row.operationOneBased
Proof uses: Function.Iterate.rec, Imo2022P1.Row.operationOneBased_valid
8 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.leftmostNSame_iff_of_valid line 500 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P1.Row, Imo2022P1.Row.valid, Iff, Imo2022P1.Row.leftmostNSame, Exists, Imo2022P1.Coin, Fin, HMul.hMul, OfNat.ofNat, Eq, LT.lt
Proof uses: Eq.mpr, id, congrArg, Imo2022P1.Row.leftmostNSame.eq_1, Iff.intro, dite, Ne, NeZero, NeZero.mk, ne_of_gt, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, lt_of_le_of_ne', zero_le, Exists.intro, HAdd.hAdd and 46 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.List.segments line 544 source
no axioms what this means
Statement uses: DecidableEq, List
Proof uses: List.splitBy, BEq.beq
1 instances, coercions and auxiliary constants left out.
lemma Imo2022P1.List.exists_replicate_of_isChain_beq line 547 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, List.IsChain, Eq, Bool, BEq.beq, Bool.true, Ne, List.nil, Exists, Nat, List.replicate
Proof uses: List.rec, Mathlib.Tactic.Contrapose.contrapose₂, Eq.mpr, Not, id, implies_congr, binderNameHint, Eq.trans, forall_congr, Eq.refl, List.cons, dite, congrArg, Exists.intro, OfNat.ofNat, List.replicate_one, And.right, Membership.mem, Option, List.head? and 17 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.segments_getElem?_map_eq line 574 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Imo2022P1.Coin, Nat, LT.lt, List.length, Imo2022P1.List.segments, Eq, Option, Option.bind, GetElem?.getElem?, List.head?, Option.map, ite, Even, Imo2022P1.Coin.flip
Proof uses: dite, List.nil, Eq.mpr, id, congrArg, List.splitBy, BEq.beq, Imo2022P1.List.segments.eq_1, List.splitBy_nil, Option.none, List.getElem?_nil, List.head?_nil, Option.map_none, Option.bind_none, Eq.refl, Not, Option.some, List.head, List.head?_eq_some_head, Option.map_some and 49 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.List.blocks line 631 source
no axioms what this means
Statement uses: DecidableEq, List, Nat
Proof uses: List.map, List.length, Imo2022P1.List.segments
lemma Imo2022P1.List.isChain_beq_replicate line 634 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Nat, List.IsChain, Eq, Bool, BEq.beq, Bool.true, List.replicate
Proof uses: List.isChain_replicate_of_rel, beq_self_eq_true
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.sum_blocks line 639 source
standard axioms: propext what this means
Statement uses: DecidableEq, List, Eq, Nat, List.sum, Imo2022P1.List.blocks, List.length
Proof uses: Eq.mpr, List.map, Imo2022P1.List.segments, id, congrArg, Imo2022P1.List.blocks.eq_1, List.splitBy, BEq.beq, Imo2022P1.List.segments.eq_1, List.flatten, Eq.symm, List.length_flatten, List.flatten_splitBy, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.zero_lt_of_mem_blocks line 643 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Nat, Membership.mem, Imo2022P1.List.blocks, LT.lt, OfNat.ofNat
Proof uses: And, Imo2022P1.List.segments, Eq, List.length, Exists, Eq.mp, List.map, congrArg, propext, List.mem_map, Imo2022P1.List.blocks.eq_1, Mathlib.Tactic.Contrapose.contrapose₂, List.nil, Eq.mpr, Not, LE.le, id, implies_congr, Eq.refl, List.length_eq_zero_iff and 3 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.blocks_semi_inj_helper line 653 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Imo2022P1.Coin, Eq, Nat, List.map, List.length, Option, Option.bind, List.head?, Not, Membership.mem, List.nil, List.IsChain, Bool, BEq.beq, Bool.true, Exists, Ne, List.getLast, List.head and 1 more
Proof uses: List.rec, Eq.mpr, id, congrArg, Eq.mp, propext, List.map_eq_nil_iff, Eq.symm, List.map_nil, Eq.refl, List.cons, Mathlib.Tactic.Contrapose.contrapose₁, False, True, implies_congr, not_false_eq_true, List.cons_ne_nil, List.exists_cons_of_ne_nil, List.replicate, Imo2022P1.List.exists_replicate_of_isChain_beq and 42 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 73 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.head?_flatten_of_nil_not_mem line 730 source
standard axioms: propext what this means
Statement uses: List, Not, Membership.mem, List.nil, Eq, Option, List.head?, List.flatten, Option.bind
Proof uses: dite, Eq.mpr, id, congrArg, List.flatten_nil, Option.none, List.head?_nil, Option.bind_none, Eq.refl, Exists, List.cons, List.exists_cons_of_ne_nil, HAppend.hAppend, List.flatten_cons, Option.some, List.head?_cons, Option.bind_some, Option.or, List.head?_append, Option.or_eq_left_of_isSome and 9 more
6 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.blocks_semi_inj line 742 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Imo2022P1.Coin, Eq, Nat, Imo2022P1.List.blocks, Option, List.head?
Proof uses: List.splitBy, BEq.beq, rfl, List.flatten, And, Not, Membership.mem, List.nil, List.IsChain, Bool, Bool.true, Exists, Ne, List.getLast, List.head, Bool.false, Eq.mp, congrArg, propext, List.splitBy_eq_iff and 12 more
5 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.Row.blocks line 754 source
no axioms what this means
Statement uses: Nat, Imo2022P1.Row, List
Proof uses: Imo2022P1.List.blocks, Imo2022P1.Coin, List.ofFn, HMul.hMul, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
lemma Imo2022P1.Row.sum_blocks line 756 source
standard axioms: propext what this means
Statement uses: Nat, Imo2022P1.Row, Eq, List.sum, Imo2022P1.Row.blocks, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, Imo2022P1.List.blocks, Imo2022P1.Coin, List.ofFn, id, congrArg, List, Imo2022P1.Row.blocks.eq_1, List.length, Imo2022P1.List.sum_blocks, List.length_ofFn, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.listOfBlocks line 760 source
no axioms what this means
Statement uses: List, Nat, Imo2022P1.Coin
2 instances, coercions and auxiliary constants left out.
lemma Imo2022P1.List.head?_listOfBlocks line 765 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Imo2022P1.Coin, Ne, List.nil, LT.lt, OfNat.ofNat, List.head, Eq, Option, List.head?, Imo2022P1.listOfBlocks, Option.some
Proof uses: Exists, List.cons, Eq.mp, congrArg, propext, List.ne_nil_iff_exists_cons, List.replicate, Eq.mpr, id, Iff.ne, List.replicate_eq_nil_iff, List.head.congr_simp, HAppend.hAppend, Imo2022P1.Coin.flip, Imo2022P1.listOfBlocks.eq_2, List.head?_append_of_ne_nil, ite, Option.none, List.head?_replicate, ite_eq_right and 1 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.blocks_listOfBlock line 776 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Imo2022P1.Coin, Membership.mem, LT.lt, OfNat.ofNat, Eq, Imo2022P1.List.blocks, Imo2022P1.listOfBlocks
Proof uses: List.rec, List.nil, Eq.mpr, id, congrArg, Imo2022P1.listOfBlocks.eq_1, List.map, List.length, Imo2022P1.List.segments, Imo2022P1.List.blocks.eq_1, List.splitBy, BEq.beq, Imo2022P1.List.segments.eq_1, List.splitBy_nil, List.map_nil, Eq.refl, List.cons, List.mem_cons_self, List.mem_cons_of_mem, Imo2022P1.Coin.flip and 39 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.listOfBlocks_blocks line 816 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Imo2022P1.Coin, Exists, Eq, Imo2022P1.listOfBlocks, Imo2022P1.List.blocks
Proof uses: dite, List.nil, Exists.intro, Imo2022P1.Coin.A, Eq.mpr, id, congrArg, List.map, Nat, List.length, Imo2022P1.List.segments, Imo2022P1.List.blocks.eq_1, List.splitBy, BEq.beq, Imo2022P1.List.segments.eq_1, List.splitBy_nil, List.map_nil, Imo2022P1.listOfBlocks.eq_1, Eq.refl, Not and 24 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.listOfBlocks_length line 837 source
standard axioms: propext what this means
Statement uses: List, Nat, Imo2022P1.Coin, Eq, List.length, Imo2022P1.listOfBlocks, List.sum
Proof uses: List.rec, Eq.mpr, List.nil, id, congrArg, Imo2022P1.listOfBlocks.eq_1, OfNat.ofNat, List.length_nil, List.sum_nil, Eq.refl, List.cons, HAppend.hAppend, List.replicate, Imo2022P1.Coin.flip, Imo2022P1.listOfBlocks.eq_2, HAdd.hAdd, List.length_append, List.sum_cons, List.length_replicate
11 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.Row.ofBlocks line 844 source
standard axioms: propext what this means
Statement uses: Nat, List, Imo2022P1.Coin, Eq, List.sum, HMul.hMul, OfNat.ofNat, Imo2022P1.Row
Proof uses: List.length, Imo2022P1.listOfBlocks, Fin, List.get, Fin.cast
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.blocks_ofBlocks line 850 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Imo2022P1.Coin, Eq, List.sum, HMul.hMul, OfNat.ofNat, Membership.mem, LT.lt, Imo2022P1.Row.blocks, Imo2022P1.Row.ofBlocks
Proof uses: Eq.mpr, Imo2022P1.List.blocks, Imo2022P1.listOfBlocks, id, congrArg, Eq.symm, Imo2022P1.List.blocks_listOfBlock, List.ofFn, List.length, List.get, List.ofFn_get, Fin, Fin.cast, Imo2022P1.Row, Imo2022P1.Row.ofBlocks.eq_1, Imo2022P1.Row.blocks.eq_1, DecidableEq, Eq.rec, Eq.refl, Subsingleton.elim and 3 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.ofBlocks_blocks line 858 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2022P1.Row, Exists, Imo2022P1.Coin, Eq, Imo2022P1.Row.ofBlocks, Imo2022P1.Row.blocks, Imo2022P1.Row.sum_blocks
Proof uses: List, Imo2022P1.listOfBlocks, Imo2022P1.List.blocks, List.ofFn, HMul.hMul, OfNat.ofNat, Imo2022P1.List.listOfBlocks_blocks, Exists.intro, Eq.mpr, Fin, Fin.mk, List.length, Fin.cast, LT.lt, Fin.isLt, Eq.refl, id, congrFun', congrArg, funext and 5 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.ofFn_ofBlocks line 866 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, List, Imo2022P1.Coin, Eq, List.sum, HMul.hMul, OfNat.ofNat, List.ofFn, Imo2022P1.Row.ofBlocks, Imo2022P1.listOfBlocks
Proof uses: List.length, Eq.mpr, id, congrArg, Imo2022P1.listOfBlocks_length, Eq.symm, List.get, Fin, Fin.cast, List.ofFn_congr, Eq.rec, Eq.refl, List.ofFn_get
12 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.List.alternateSum line 876 source
no axioms what this means
Statement uses: Add, Zero, List, Bool
2 instances, coercions and auxiliary constants left out.
lemma Imo2022P1.List.alternateSum_pos_of_nat line 881 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Bool, Membership.mem, LT.lt, OfNat.ofNat, LE.le, List.length, Imo2022P1.List.alternateSum
Proof uses: Exists, Eq, List.cons, List.exists_cons_of_length_pos, Eq.mpr, id, congrArg, Eq.mp, HAdd.hAdd, List.length_cons, ite, Bool.true, Bool.not, Imo2022P1.List.alternateSum.eq_2, Bool.false, Or, Eq.trans, congr, ite_eq_right_of_eq_false, Bool.false_eq_true and 12 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.lt_alternateSum_of_nat_mem line 894 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Membership.mem, LT.lt, OfNat.ofNat, LE.le, List.length, Max.max, Imo2022P1.List.alternateSum, Bool.true, Bool.false
Proof uses: List.rec, List.nil, Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, id, Eq, implies_congr, Eq.refl, List.not_mem_nil, List.cons, dite, Exists, Eq.mp, congrArg, propext, List.length_eq_four, And.right, And, List.cons_eq_cons and 31 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.sum_eq_alternateSum_add_alternateSum line 931 source
standard axioms: propext what this means
Statement uses: AddCommMonoid, List, Bool, Eq, List.sum, HAdd.hAdd, Imo2022P1.List.alternateSum, Bool.not
Proof uses: List.rec, Eq.mpr, List.nil, OfNat.ofNat, id, congrArg, Imo2022P1.List.alternateSum.eq_1, List.sum_nil, List.cons, ite, Bool.true, Imo2022P1.List.alternateSum.eq_2, List.sum_cons, dite, ite_eq_left, of_decide_eq_true, Decidable.decide, Eq.refl, ite_eq_right, Not and 6 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.count_ListOfBlocks_eq_alternateSum line 945 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Imo2022P1.Coin, Eq, List.count, Imo2022P1.Coin.A, Imo2022P1.listOfBlocks, Imo2022P1.List.alternateSum, Decidable.decide
Proof uses: List.rec, Eq.mpr, List.nil, OfNat.ofNat, id, congrArg, Imo2022P1.List.alternateSum.eq_1, Imo2022P1.listOfBlocks.eq_1, List.count_nil, Eq.refl, List.cons, HAdd.hAdd, ite, Bool, Bool.true, Bool.not, Imo2022P1.List.alternateSum.eq_2, HAppend.hAppend, List.replicate, Imo2022P1.Coin.flip and 13 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.ofBlocks_valid_iff_alternateSum_eq line 954 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Imo2022P1.Coin, Eq, List.sum, HMul.hMul, OfNat.ofNat, Bool, Iff, Imo2022P1.Row.valid, Imo2022P1.Row.ofBlocks, Imo2022P1.List.alternateSum
Proof uses: Eq.mpr, Imo2022P1.isValidRow, List.ofFn, id, congrArg, propext, Imo2022P1.Row.valid_iff_isValidRow_ofFn, Imo2022P1.listOfBlocks, Imo2022P1.ofFn_ofBlocks, List.count, Imo2022P1.Coin.A, List.length, Imo2022P1.isValidRow.eq_1, Imo2022P1.listOfBlocks_length, Or, mul_eq_mul_left_iff, or_iff_left, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 17 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.blocks_eq_iff line 967 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2022P1.Row, Iff, Eq, List, Imo2022P1.Row.blocks, List.cons, List.nil, Exists, Imo2022P1.Coin, Fin, HMul.hMul, OfNat.ofNat, LT.lt
Proof uses: Iff.intro, Imo2022P1.Row.ofBlocks, Imo2022P1.Row.sum_blocks, Imo2022P1.Row.ofBlocks_blocks, Exists.intro, Eq.mpr, List.get, Imo2022P1.listOfBlocks, Fin.cast, List.length, id, congrArg, Eq.symm, Eq.mp, Imo2022P1.Row.ofBlocks.eq_1, LE.le, Imo2022P1.Coin.flip, congrFun', Eq.trans, Not and 72 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.leftmostNSame_iff_length_blocks_ofFn_of_valid line 1012 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2022P1.Row, Imo2022P1.Row.valid, Iff, Imo2022P1.Row.leftmostNSame, Eq, List.length, Imo2022P1.Row.blocks, OfNat.ofNat
Proof uses: Eq.mpr, Exists, Imo2022P1.Coin, Fin, HMul.hMul, LT.lt, id, congrArg, propext, Imo2022P1.Row.leftmostNSame_iff_of_valid, List, List.cons, List.nil, Eq.symm, Imo2022P1.Row.blocks_eq_iff, Iff.intro, HAdd.hAdd, List.length_cons, List.length_singleton, Eq.refl and 28 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.blocks_take line 1030 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Nat, Eq, Imo2022P1.List.blocks, List.take, List.sum
Proof uses: Eq.mpr, List.map, List.length, Imo2022P1.List.segments, id, congrArg, Imo2022P1.List.blocks.eq_1, List.splitBy, BEq.beq, Imo2022P1.List.segments.eq_1, Eq.symm, List.map_take, Eq.rec, Eq.refl, And, List.flatten, Not, Membership.mem, List.nil, List.IsChain and 22 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.blocks_drop line 1047 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Nat, Eq, Imo2022P1.List.blocks, List.drop, List.sum, List.take
Proof uses: Eq.mpr, List.map, List.length, Imo2022P1.List.segments, id, congrArg, Imo2022P1.List.blocks.eq_1, List.splitBy, BEq.beq, Imo2022P1.List.segments.eq_1, Eq.symm, List.map_drop, Eq.rec, Eq.refl, And, List.flatten, Not, Membership.mem, List.nil, List.IsChain and 22 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.blocks_drop_take line 1064 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Nat, Eq, Imo2022P1.List.blocks, List.take, List.sum, List.drop
Proof uses: Eq.mpr, id, congrArg, Eq.symm, Imo2022P1.List.blocks_drop, Imo2022P1.List.blocks_take, Eq.rec, Eq.refl, Subsingleton.elim, Decidable, Add, Zero
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.blocks_append line 1070 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Membership.mem, Option, List.getLast?, List.head?, Eq, Bool, BEq.beq, Bool.false, Nat, Imo2022P1.List.blocks, HAppend.hAppend
Proof uses: of_eq_true, List.map, List.length, List.splitBy, Eq.trans, True, congrFun', congrArg, Imo2022P1.List.segments, List.splitBy_append, List.map_append, eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.length_blocks_append_lt_of line 1074 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Exists, And, Membership.mem, Option, List.getLast?, List.head?, Eq, Bool, BEq.beq, Bool.true, LT.lt, Nat, List.length, Imo2022P1.List.blocks, HAppend.hAppend, HAdd.hAdd
Proof uses: Eq.mpr, HSub.hSub, List.splitBy, OfNat.ofNat, id, congr, congrArg, Eq.trans, List.dropLast, List.cons, Option.getD, List.nil, List.tail, List.map, Imo2022P1.List.segments, Imo2022P1.List.splitBy_append', List.length_map, List.length_append, congrFun', List.length_dropLast and 14 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.length_blocks_append_le line 1093 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, LE.le, Nat, List.length, Imo2022P1.List.blocks, HAppend.hAppend, HAdd.hAdd
Proof uses: dite, Exists, And, Membership.mem, Option, List.getLast?, List.head?, Eq, Bool, BEq.beq, Bool.true, le_of_lt, Imo2022P1.List.length_blocks_append_lt_of, Not, Bool.false, Bool.eq_false_of_ne_true, Eq.mp, Ne, Eq.trans, binderNameHint and 10 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.indexInBlock line 1101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat
Proof uses: Finset.max', Finset.filter, LE.le, List.sum, List.take, Finset.Iic, List.length
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.indexInBlock_eq_length_sub_one_of line 1104 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Ne, List.nil, LE.le, List.sum, HAdd.hAdd, List.getLast, LT.lt, Eq, Imo2022P1.indexInBlock, HSub.hSub, List.length, OfNat.ofNat
Proof uses: Eq.mpr, Finset.max', Finset.filter, List.take, Finset.Iic, id, congrArg, Imo2022P1.indexInBlock.eq_1, And, Membership.mem, Finset, propext, Finset.max'_eq_iff, congr, Eq.trans, True, congrFun', true_and, forall_congr, implies_congr and 15 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
def Imo2022P1.List.blockIndex line 1121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, Nat
Proof uses: Imo2022P1.indexInBlock, Imo2022P1.List.blocks
1 instances, coercions and auxiliary constants left out.
lemma Imo2022P1.List.blockIndex_lt line 1124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, LT.lt, Nat, Imo2022P1.List.blockIndex, Imo2022P1.List.blocks
Proof uses: Eq.mpr, Imo2022P1.indexInBlock, id, Eq, congrArg, Imo2022P1.List.blockIndex.eq_1, Finset.max', Finset.filter, LE.le, List.sum, List.take, Finset.Iic, Imo2022P1.indexInBlock.eq_1, Membership.mem, Finset, propext, Finset.max'_lt_iff, lt_of_le_of_ne, And.left, Eq.mp and 13 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.sum_take_blockIndex_blocks_le line 1135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, LE.le, Nat, List.sum, List.take, Imo2022P1.List.blockIndex, Imo2022P1.List.blocks
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, And.right, And.left, And, Eq.mp, Membership.mem, Finset, Finset.filter, Finset.Iic, congr, Eq.trans, congrFun', forall_congr, implies_congr, Eq.refl, Finset.max' and 6 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.lt_sum_take_succ_blockIndex_blocks line 1144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, LT.lt, Nat, List.sum, List.take, HAdd.hAdd, Imo2022P1.List.blockIndex, OfNat.ofNat, Imo2022P1.List.blocks
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, Mathlib.Tactic.Contrapose.contrapose₁, And, LE.le, Not, Exists, implies_congr, Eq.trans, Mathlib.Tactic.Push.not_and_eq, Eq.refl, Mathlib.Tactic.Push.not_forall_eq, funext, Exists.intro, And.intro, Nat.succ, propext and 16 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.some_get_eq_head?_get?_segments_blockIndex line 1161 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, Eq, Option, Option.some, List.get, Option.bind, GetElem?.getElem?, Nat, LT.lt, Imo2022P1.List.segments, Imo2022P1.List.blockIndex, List.head?
Proof uses: Imo2022P1.List.blocks, Imo2022P1.List.blockIndex_lt, Fin.mk, Eq.mp, List.map, congrArg, List.length_map, Imo2022P1.List.blocks.eq_1, Eq.mpr, Option.get, id, List.get_eq_getElem?, Option.some_get, Fin.getElem?_fin, Fin.val_mk, Eq.refl, Eq.symm, Option.bind_some, HAppend.hAppend, List.flatten and 68 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.some_get_eq_head?_bind_get?_segments_blockIndex line 1223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Imo2022P1.Coin, Fin, List.length, Eq, Option, Option.some, List.get, Option.map, ite, Even, Nat, Imo2022P1.List.blockIndex, Imo2022P1.Coin.flip, List.head?
Proof uses: Eq.mpr, Option.bind, GetElem?.getElem?, LT.lt, Imo2022P1.List.segments, id, congrArg, Imo2022P1.List.some_get_eq_head?_get?_segments_blockIndex, Imo2022P1.List.blocks, Imo2022P1.List.blockIndex_lt, Imo2022P1.segments_getElem?_map_eq, Eq.mp, List.map, List.length_map, Imo2022P1.List.blocks.eq_1, 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 Imo2022P1.List.head?_get?_segments_blockIndex_ne_of line 1230 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Nat, Eq, HAdd.hAdd, OfNat.ofNat, LT.lt, List.length, Imo2022P1.List.segments, Ne, Option, Option.bind, GetElem?.getElem?, List.head?
Proof uses: Option.some, List.get, Fin.mk, Eq.mpr, Option.get, Fin, id, congrArg, List.get_eq_getElem?, Option.some_get, Fin.getElem?_fin, Fin.val_mk, Eq.refl, Eq.symm, Option.bind_some, Exists, List.replicate, Imo2022P1.List.exists_replicate_of_isChain_beq, List.splitBy, BEq.beq and 35 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.chainLeft_eq line 1280 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, Eq, Nat, Imo2022P1.List.chainLeft, List.sum, List.take, Imo2022P1.List.blockIndex, Imo2022P1.List.blocks
Proof uses: Eq.mpr, Finset.min', Finset.filter, LE.le, List.get, Finset.Iic, id, congrArg, Imo2022P1.List.chainLeft.eq_1, Imo2022P1.List.sum_take_blockIndex_blocks_le, LT.lt, Fin.mk, Eq.symm, Fin.val_mk, propext, Fin.val_inj, And, Membership.mem, Finset, Finset.min'_eq_iff and 72 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 97 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.chainRight_succ_eq line 1356 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, Eq, Nat, HAdd.hAdd, Imo2022P1.List.chainRight, OfNat.ofNat, List.sum, List.take, Imo2022P1.List.blockIndex, Imo2022P1.List.blocks
Proof uses: Eq.symm, LT.lt, Imo2022P1.List.lt_sum_take_succ_blockIndex_blocks, Nat.eq_add_of_sub_eq, Nat.succ, HSub.hSub, Eq.mpr, Finset.max', Finset.filter, LE.le, List.get, Finset.Ici, id, congrArg, Imo2022P1.List.chainRight.eq_1, Imo2022P1.List.sum_blocks, List.drop, List.sum_take_add_sum_drop, Nat.le_add_right, Fin.mk and 68 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 95 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.blocks_operation_left_segment line 1434 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, Eq, Nat, Imo2022P1.List.blocks, List.take, Imo2022P1.List.chainLeft, Imo2022P1.List.blockIndex
Proof uses: Eq.mpr, List.sum, id, congrArg, Eq.symm, Imo2022P1.List.blocks_take, Eq.rec, Eq.refl, Subsingleton.elim, Decidable, Imo2022P1.List.chainLeft_eq
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.blocks_operation_right_segment line 1440 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, Eq, Nat, Imo2022P1.List.blocks, List.drop, HAdd.hAdd, Imo2022P1.List.chainRight, OfNat.ofNat, Imo2022P1.List.blockIndex
Proof uses: Eq.mpr, List.sum, List.take, id, congrArg, Eq.symm, Imo2022P1.List.blocks_drop, Eq.rec, Eq.refl, Subsingleton.elim, Decidable, Imo2022P1.List.chainRight_succ_eq
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.blocks_operation_middle_segment line 1446 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, Eq, Nat, Imo2022P1.List.blocks, List.take, HSub.hSub, HAdd.hAdd, Imo2022P1.List.chainRight, OfNat.ofNat, Imo2022P1.List.chainLeft, List.drop, Imo2022P1.List.blockIndex
Proof uses: Eq.mpr, List.sum, id, congrArg, Eq.symm, Imo2022P1.List.blocks_drop_take, Eq.rec, Eq.refl, Subsingleton.elim, Decidable, Imo2022P1.List.chainLeft_eq, Imo2022P1.List.chainRight_succ_eq, Nat.sub_eq_of_eq_add', List.sum_take_add_sum_drop, HAdd, Min.min, List.take_take, Add, Zero, Nat.min_add_right_self and 2 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.blocks_operation_left_head? line 1460 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Fin, List.length, Ne, Nat, Imo2022P1.List.chainLeft, OfNat.ofNat, Eq, Option, List.head?, List.take
Proof uses: Eq.mpr, ite, Option.none, id, congrArg, List.head?_take, ite_eq_right, Eq.refl
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.blocks_operation_left_getLast? line 1464 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Imo2022P1.Coin, Fin, List.length, Ne, Nat, Imo2022P1.List.chainLeft, OfNat.ofNat, Eq, Option, List.getLast?, List.take, Option.map, ite, Even, Imo2022P1.List.blockIndex, Imo2022P1.Coin.flip, List.head?
Proof uses: Eq.mpr, Option.none, Option.or, GetElem?.getElem?, LT.lt, HSub.hSub, id, congrArg, List.getLast?_take, ite_eq_right, Option.some, List.get, Fin.mk, Option.get, List.get_eq_getElem?, Option.some_get, Fin.getElem?_fin, Fin.val_mk, Eq.refl, Eq.symm and 80 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.blocks_operation_right_head? line 1517 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Imo2022P1.Coin, Fin, List.length, Ne, Nat, Imo2022P1.List.chainRight, HSub.hSub, OfNat.ofNat, Eq, Option, List.head?, List.drop, HAdd.hAdd, Option.map, ite, Even, Imo2022P1.List.blockIndex, Imo2022P1.Coin.flip
Proof uses: Eq.mpr, GetElem?.getElem?, LT.lt, id, congrArg, List.head?_drop, Option.some, List.get, Fin.mk, Option.get, List.get_eq_getElem?, Option.some_get, Fin.getElem?_fin, Fin.val_mk, Eq.refl, Eq.symm, Imo2022P1.some_get_eq_head?_bind_get?_segments_blockIndex, Eq.rec, funext, Not and 48 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.List.blocks_operation_middle_getLast? line 1550 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Imo2022P1.Coin, Fin, List.length, Eq, Option, List.getLast?, List.take, HSub.hSub, Nat, HAdd.hAdd, Imo2022P1.List.chainRight, OfNat.ofNat, Imo2022P1.List.chainLeft, List.drop, Option.map, ite, Even, Imo2022P1.List.blockIndex, Imo2022P1.Coin.flip and 1 more
Proof uses: LE.le, Imo2022P1.List.chainLeft_le_chainRight, Not, Eq.mpr, Option.none, Option.or, GetElem?.getElem?, LT.lt, id, congrArg, List.getLast?_take, ite_eq_right, List.getElem?_drop, Nat.sub_right_comm, Nat.add_sub_cancel, Eq.symm, Nat.add_sub_assoc, Nat.add_sub_cancel_left, Fin.getElem?_fin, Option.some and 65 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.blocks_operationOneBased_eq_blocks_of line 1591 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, Imo2022P1.Row, List, Eq, Imo2022P1.Row.blocks, Imo2022P1.indexInBlock, HSub.hSub, Imo2022P1.Row.operationOneBased
Proof uses: Eq.mpr, Imo2022P1.List.blocks, Imo2022P1.Coin, List.ofFn, id, congrArg, Imo2022P1.Row.blocks.eq_1, Imo2022P1.List.operationOneBased, Imo2022P1.Row.ofFn_operationOneBased_eq_operationOneBased_ofFn, Imo2022P1.List.operation, Fin.mk, List.length, Imo2022P1.List.operationOneBased.eq_1, Imo2022P1.List.move, Imo2022P1.List.chainLeft, Imo2022P1.List.chainRight, Imo2022P1.List.operation.eq_1, HAppend.hAppend, List.take, HAdd.hAdd and 33 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.blocks_operationOneBased_iterate_eq_blocks_of line 1613 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, Imo2022P1.Row, List, Eq, Imo2022P1.Row.blocks, Imo2022P1.indexInBlock, HSub.hSub, Nat.iterate, Imo2022P1.Row.operationOneBased
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, Function.iterate_zero, id.eq_1, HAdd.hAdd, Nat.succ, Function.iterate_succ_apply', Imo2022P1.Row.blocks_operationOneBased_eq_blocks_of
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.blocks_operationOneBased_eq_rotate_one_blocks_of line 1623 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, Imo2022P1.Row, List, Even, List.length, Eq, Imo2022P1.Row.blocks, Imo2022P1.indexInBlock, HSub.hSub, Imo2022P1.Row.operationOneBased, List.reverse, List.rotate
Proof uses: Eq.mpr, Imo2022P1.List.blocks, Imo2022P1.Coin, List.ofFn, id, congrArg, Imo2022P1.Row.blocks.eq_1, Imo2022P1.List.operationOneBased, Imo2022P1.Row.ofFn_operationOneBased_eq_operationOneBased_ofFn, Imo2022P1.List.operation, Fin.mk, Imo2022P1.List.operationOneBased.eq_1, Imo2022P1.List.move, Imo2022P1.List.chainLeft, Imo2022P1.List.chainRight, Imo2022P1.List.operation.eq_1, HAppend.hAppend, List.take, HAdd.hAdd, List.drop and 89 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.blocks_operationOneBased_iterate_eq_rotate_blocks_of line 1683 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, Imo2022P1.Row, List, Even, List.length, Eq, Imo2022P1.Row.blocks, Membership.mem, LT.lt, HAdd.hAdd, Nat.iterate, Imo2022P1.Row.operationOneBased, List.reverse, List.rotate
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, Function.iterate_zero, id.eq_1, List.rotate_zero, List.reverse_reverse, Nat.succ, Function.iterate_succ_apply', List.length_reverse, List.length_rotate, Eq.refl, Ne, List.nil, Eq.symm, propext, List.length_pos_iff_ne_nil, Imo2022P1.List.blocks, Imo2022P1.Coin and 26 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.length_blocks_operationOneBased_lt_of_odd_last line 1717 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, Imo2022P1.Row, List, Odd, List.length, Eq, Imo2022P1.Row.blocks, Imo2022P1.indexInBlock, HSub.hSub, LT.lt, Imo2022P1.Row.operationOneBased
Proof uses: Eq.mpr, Imo2022P1.List.blocks, Imo2022P1.Coin, List.ofFn, id, congrArg, Imo2022P1.Row.blocks.eq_1, Imo2022P1.List.operationOneBased, Imo2022P1.Row.ofFn_operationOneBased_eq_operationOneBased_ofFn, Imo2022P1.List.operation, Fin.mk, Imo2022P1.List.operationOneBased.eq_1, Imo2022P1.List.move, Imo2022P1.List.chainLeft, Imo2022P1.List.chainRight, Imo2022P1.List.operation.eq_1, HAppend.hAppend, List.take, HAdd.hAdd, List.drop and 83 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.length_blocks_operationOneBased_lt_of_middle line 1766 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, Imo2022P1.Row, List, Eq, Imo2022P1.Row.blocks, Ne, Imo2022P1.indexInBlock, HSub.hSub, List.length, LT.lt, Imo2022P1.Row.operationOneBased
Proof uses: Imo2022P1.Coin, List.ofFn, Eq.mpr, id, congrArg, List.length_ofFn, Imo2022P1.List.blocks, Imo2022P1.Row.blocks.eq_1, Imo2022P1.List.operationOneBased, Imo2022P1.Row.ofFn_operationOneBased_eq_operationOneBased_ofFn, Imo2022P1.List.operation, Fin.mk, Imo2022P1.List.operationOneBased.eq_1, Imo2022P1.List.move, Imo2022P1.List.chainLeft, Imo2022P1.List.chainRight, Imo2022P1.List.operation.eq_1, HAppend.hAppend, List.take, HAdd.hAdd and 67 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.exists_length_blocks_operationOneBased_iterate_lt_of line 1826 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, Imo2022P1.Row, List, Even, List.length, Eq, Imo2022P1.Row.blocks, Membership.mem, HSub.hSub, Option, List.findIdx?, Decidable.decide, HAdd.hAdd, List.reverse, Option.some, Exists, LT.lt and 2 more
Proof uses: Nat.recAux, Exists.intro, Eq.mpr, id, congrArg, Function.iterate_one, And, Bool, GetElem.getElem, Bool.true, Not, Nat.lt_trans, Eq.mp, propext, List.findIdx?_eq_some_iff_getElem, Ne, List.nil, Imo2022P1.List.blocks, Imo2022P1.Coin, List.ofFn and 81 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 87 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.exists_length_blocks_operationOneBased_iterate_lt line 1909 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, CeilDiv.ceilDiv, HMul.hMul, Imo2022P1.Row, Imo2022P1.Row.valid, List.length, Imo2022P1.Row.blocks, Exists, Nat.iterate, Imo2022P1.Row.operationOneBased
Proof uses: Imo2022P1.Coin, Eq, Imo2022P1.Row.ofBlocks, Imo2022P1.Row.sum_blocks, Imo2022P1.Row.ofBlocks_blocks, Ne, Imo2022P1.indexInBlock, HSub.hSub, Eq.mpr, Finset.max', Finset.filter, List.sum, List.take, Finset.Iic, id, congrArg, Imo2022P1.indexInBlock.eq_1, Not, ne_eq, And and 101 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 91 steps
Open to load the checked before-and-after goal states.
lemma Imo2022P1.Row.exists_length_blocks_operationOneBased_iterate_eq_two line 1986 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, CeilDiv.ceilDiv, HMul.hMul, Imo2022P1.Row, Imo2022P1.Row.valid, Eq, List.length, Imo2022P1.Row.blocks, Exists, Nat.iterate, Imo2022P1.Row.operationOneBased
Proof uses: Nat.strong_induction_on, dite, Exists.intro, Eq.mpr, id, congrArg, Function.iterate_zero, id.eq_1, le_antisymm, Eq.mp, Imo2022P1.Coin, Imo2022P1.Row.ofBlocks, Imo2022P1.Row.sum_blocks, Imo2022P1.Row.ofBlocks_blocks, Mathlib.Tactic.Contrapose.contrapose₁, Imo2022P1.List.alternateSum, Bool.false, Not, Ne, implies_congr and 23 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
determine Imo2022P1.answer The answer to be determined line 2026 source
Source documentation
The answer to be determined.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Prod, Nat
Proof uses: Set.ofPred, Imo2022P1.answer.match_1, And, LT.lt, OfNat.ofNat, LE.le, CeilDiv.ceilDiv, HMul.hMul
13 instances, coercions and auxiliary constants left out.
```
determine answer : Set (ℕ × ℕ) := {(n, k) : ℕ × ℕ | 0 < n ∧ n ≤ k ∧ k ≤ 3 * n ⌈/⌉ 2}
```
problem Imo2022P1.imo2022_p1 line 2028 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Set, Prod, Nat, Set.ofPred, Imo2022P1.answer.match_1, Exists, LE.le, OfNat.ofNat, HMul.hMul, Imo2022P1.Row, Imo2022P1.Row.valid, Imo2022P1.Row.leftmostNSame, Nat.iterate, Imo2022P1.Row.operationOneBased, Imo2022P1.answer
Proof uses: Eq.mpr, And, LT.lt, CeilDiv.ceilDiv, id, congrArg, Imo2022P1.answer.eq_1, Set.ext, Iff, Membership.mem, Prod.mk, Iff.intro, Mathlib.Tactic.Contrapose.contrapose₁, Not, Or, implies_congr, Eq.trans, Mathlib.Tactic.Push.not_and_or_eq, congr, binderNameHint and 126 more
117 instances, coercions and auxiliary constants left out.

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