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

56 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2000, Problem 4

100 cards are numbered 1 to 100 (each card different) and placed in 3 boxes (at least one card in each box). How many ways can this be done so that if two boxes are selected and a card is taken from each, then the knowledge of their sum alone is always sufficient to identify the third box?

Imports (8)

Imported by 1 file

Compfiles.lean

def Imo2000P4.Good Documented declaration: Good line 63 source
Source documentation
A placement of the cards 1, ..., n into three boxes (labeled by ZMod 3) is good if every box is nonempty and whenever two pairs of cards from two different pairs of boxes have the same sum, the pairs of boxes coincide.

no axioms what this means
Statement uses: Nat, ZMod, OfNat.ofNat
Proof uses: And, Exists, LE.le, Eq, Ne, HAdd.hAdd, Or
5 instances, coercions and auxiliary constants left out.
```
def Good (n : ℕ) (f : ℕ → ZMod 3) : Prop :=
…
```
Mentions: f
def Imo2000P4.Mod3 The mod-3 placements: the box of card a depends only on a % 3 line 70 source
Source documentation
The mod-3 placements: the box of card a depends only on a % 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ZMod, OfNat.ofNat
Proof uses: Exists, Equiv.Perm, LE.le, Eq
14 instances, coercions and auxiliary constants left out.
```
def Mod3 (n : ℕ) (f : ℕ → ZMod 3) : Prop :=
…
```
Mentions: f
def Imo2000P4.Ends The "ends" placements: cards 1 and n are alone in two boxes and all cards 2, ..., n - 1 are in the third box line 75 source
Source documentation
The "ends" placements: cards 1 and n are alone in two boxes and all cards 2, ..., n - 1 are in the third box.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ZMod, OfNat.ofNat
Proof uses: Exists, Equiv.Perm, And, Eq, LE.le, HSub.hSub
25 instances, coercions and auxiliary constants left out.
```
def Ends (n : ℕ) (f : ℕ → ZMod 3) : Prop :=
…
```
Mentions: f
lemma Imo2000P4.exists_third line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Exists, And, Ne
Proof uses: of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.eq_third line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Ne, Eq
Proof uses: And, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, And.intro
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.equiv_of_distinct line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Ne, Exists, Equiv.Perm, And, Eq
Proof uses: Function.Injective, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, of_eq_true and 28 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.tri line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Or, Eq
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
42 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.pair_eq_of_sum_aux line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Ne, Eq, HAdd.hAdd, Or, And
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.pair_eq_of_sum line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Ne, Eq, HAdd.hAdd, Or, And
Proof uses: Imo2000P4.pair_eq_of_sum_aux
18 instances, coercions and auxiliary constants left out.
lemma Imo2000P4.cast_ne_add_one_two line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Or, Eq, OfNat.ofNat, Ne, ZMod, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, Nat.cast_add, Nat.cast_one, add_zero, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, add_left_cancel, Eq.symm, Nat.cast_ofNat
51 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.good_mono If n + 1 shares its box with another card, then a good placement of 1, ..., n + 1 restricts to a good placement of 1, ..., n line 120 source
Source documentation
If n + 1 shares its box with another card, then a good placement of 1, ..., n + 1 restricts to a good placement of 1, ..., n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ZMod, OfNat.ofNat, Imo2000P4.Good, HAdd.hAdd, Exists, And, LE.le, Eq
Proof uses: And.intro, Ne, Or, And.left, dite, Exists.intro, Not, Eq.mpr, id, congrArg, Eq.symm, And.right
14 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma good_mono {n : ℕ} {f : ℕ → ZMod 3} (hf : Good (n + 1) f)
    (h : ∃ m, 1 ≤ m ∧ m ≤ n ∧ f m = f (n + 1)) : Good n f := by
…
```
Mentions: f, Imo2000P4.Good, h
lemma Imo2000P4.case_alone Case 1 of the induction step: n + 1 is alone in its box line 136 source
Source documentation
Case 1 of the induction step: n + 1 is alone in its box. Then 1 is also alone, and we get an Ends placement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, ZMod, Imo2000P4.Good, HAdd.hAdd, Ne, Imo2000P4.Ends
Proof uses: le_rfl, Decidable.byContradiction, Eq, Not, And, Exists, False, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, Eq.symm, Imo2000P4.exists_third, And.left, Or, HSub.hSub, dite, Exists.intro, And.intro and 8 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 75 steps
Open to load the checked before-and-after goal states.
```
lemma case_alone {n : ℕ} (hn : 3 ≤ n) {f : ℕ → ZMod 3} (hf : Good (n + 1) f)
    (halone : ∀ a, 1 ≤ a → a ≤ n → f a ≠ f (n + 1)) : Ends (n + 1) f := by
…
```
Mentions: f, Imo2000P4.Good, Imo2000P4.Ends
lemma Imo2000P4.case_mod3 Case 2a of the induction step: the restriction to 1, ..., n is a mod-3 placement; then n + 1 must go into the box of its own residue line 195 source
Source documentation
Case 2a of the induction step: the restriction to 1, ..., n is a mod-3 placement; then n + 1 must go into the box of its own residue.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, ZMod, Imo2000P4.Good, HAdd.hAdd, Imo2000P4.Mod3
Proof uses: Eq, Exists, Exists.intro, HSub.hSub, Equiv.Perm, Ne, Imo2000P4.cast_ne_add_one_two, Or.inl, rfl, Or.inr, Eq.mpr, id, congrArg, Iff.mpr, Equiv, Function.Injective.ne_iff, Equiv.injective, Decidable.byContradiction, Not, And and 12 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
```
lemma case_mod3 {n : ℕ} (hn : 3 ≤ n) {f : ℕ → ZMod 3} (hf : Good (n + 1) f)
    (hm : Mod3 n f) : Mod3 (n + 1) f := by
…
```
Mentions: f, Imo2000P4.Good, Imo2000P4.Mod3
lemma Imo2000P4.case_ends Case 2b of the induction step: the restriction to 1, ..., n is an Ends placement with 4 ≤ n; then there is no room for the card n + 1 line 234 source
Source documentation
Case 2b of the induction step: the restriction to 1, ..., n is an Ends placement with 4 ≤ n; then there is no room for the card n + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, ZMod, Imo2000P4.Good, HAdd.hAdd, Imo2000P4.Ends, False
Proof uses: Equiv.Perm, And, Eq, HSub.hSub, le_rfl, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Ne, Iff.mpr, Equiv, Function.Injective.ne_iff, Equiv.injective, of_decide_eq_true, id, Decidable.decide, Exists, Equiv.surjective and 8 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 80 steps
Open to load the checked before-and-after goal states.
```
lemma case_ends {n : ℕ} (hn : 4 ≤ n) {f : ℕ → ZMod 3} (hf : Good (n + 1) f)
    (he : Ends n f) : False := by
…
```
Mentions: f, Imo2000P4.Good, Imo2000P4.Ends
lemma Imo2000P4.base_case Base case: every good placement of 1, 2, 3 puts the three cards in three different boxes line 268 source
Source documentation
Base case: every good placement of 1, 2, 3 puts the three cards in three different boxes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ZMod, OfNat.ofNat, Imo2000P4.Good, Imo2000P4.Ends
Proof uses: Ne, Eq, And, Exists, False, Imo2000P4.exists_third, LE.le, And.left, HAdd.hAdd, Or, dite, Eq.symm, le_antisymm, Nat.rawCast, Mathlib.Tactic.IntervalCases.of_le_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Not, Eq.mp and 11 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma base_case {f : ℕ → ZMod 3} (hf : Good 3 f) : Ends 3 f := by
…
```
Mentions: f, Imo2000P4.Good, Imo2000P4.Ends
lemma Imo2000P4.ends3_mod3 For n = 3 the two families coincide line 299 source
Source documentation
For n = 3 the two families coincide.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ZMod, OfNat.ofNat, Imo2000P4.Ends, Imo2000P4.Mod3
Proof uses: Equiv.Perm, And, Eq, LE.le, HSub.hSub, le_rfl, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.isNat_natSub, Bool, Bool.true, Ne, Eq.mpr, id, congrArg, Iff.mpr, Equiv, Function.Injective.ne_iff, Equiv.injective and 17 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma ends3_mod3 {f : ℕ → ZMod 3} (he : Ends 3 f) : Mod3 3 f := by
…
```
Mentions: f, Imo2000P4.Ends, Imo2000P4.Mod3
lemma Imo2000P4.classify The classification: every good placement of 1, ..., n (3 ≤ n) is either by residue mod 3 or an Ends placement line 314 source
Source documentation
The classification: every good placement of 1, ..., n (3 ≤ n) is either by residue mod 3 or an Ends placement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, ZMod, Imo2000P4.Good, Or, Imo2000P4.Mod3, Imo2000P4.Ends
Proof uses: Nat.le_induction, Or.inr, Imo2000P4.base_case, HAdd.hAdd, dite, Ne, Classical.propDecidable, Imo2000P4.case_alone, Not, And, Eq, Exists, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, Imo2000P4.good_mono, Exists.intro, And.intro and 8 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma classify (n : ℕ) (hn : 3 ≤ n) (f : ℕ → ZMod 3) :
    Good n f → Mod3 n f ∨ Ends n f := by
…
```
Mentions: f, Imo2000P4.Good, Imo2000P4.Mod3, Imo2000P4.Ends
def Imo2000P4.ValidPlacement Documented declaration: ValidPlacement line 342 source
Source documentation
A placement of the 100 cards into 3 boxes (labeled by ZMod 3) is valid if every box is nonempty and whenever two boxes are selected and a card is taken from each, the sum of the two drawn cards always suffices to identify the third box: any two such selections of two distinct boxes and two cards with the same sum leave the same box unselected. Card i + 1 is represented by the index i : Fin 100.

no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat, ZMod
Proof uses: And, Function.Surjective, Ne, Eq, HAdd.hAdd, Iff
5 instances, coercions and auxiliary constants left out.
```
def ValidPlacement (f : Fin 100 → ZMod 3) : Prop :=
…
```
Mentions: f
def Imo2000P4.GoodPlacement Combinatorial form of validity: whenever two pairs of cards from two different pairs of boxes have the same sum of indices, the pairs of boxes coincide line 354 source
Source documentation
Combinatorial form of validity: whenever two pairs of cards from two different pairs of boxes have the same sum of indices, the pairs of boxes coincide. Equivalent to ValidPlacement (valid_iff_good); this is the form used in the classification argument.

no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat, ZMod
Proof uses: And, Function.Surjective, Ne, Eq, HAdd.hAdd, Or
5 instances, coercions and auxiliary constants left out.
```
def GoodPlacement (f : Fin 100 → ZMod 3) : Prop :=
…
```
Mentions: f
lemma Imo2000P4.third_box_iff_pair Two pairs of distinct boxes leave the same third box unselected if and only if the two pairs of boxes coincide line 361 source
Source documentation
Two pairs of distinct boxes leave the same third box unselected if and only if the two pairs of boxes coincide.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Ne, Iff, And, Or, Eq
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma third_box_iff_pair {x y z w : ZMod 3} (hxy : x ≠ y) (hzw : z ≠ w) :
    (∀ b : ZMod 3, (b ≠ x ∧ b ≠ y) ↔ (b ≠ z ∧ b ≠ w)) ↔
      (x = z ∧ y = w) ∨ (x = w ∧ y = z) := by
…
```
lemma Imo2000P4.valid_iff_good Documented declaration: valid_iff_good line 370 source
Source documentation
The olympiad formulation of validity is equivalent to its combinatorial form: the sum of two cards drawn from two different boxes determines the third box iff equal sums force the two pairs of boxes to coincide.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, ZMod, Iff, Imo2000P4.ValidPlacement, Imo2000P4.GoodPlacement
Proof uses: Iff.intro, Function.Surjective, Ne, Eq, HAdd.hAdd, And, And.intro, Or, Iff.mp, Imo2000P4.third_box_iff_pair, Iff.mpr
8 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma valid_iff_good (f : Fin 100 → ZMod 3) :
    ValidPlacement f ↔ GoodPlacement f := by
…
```
Mentions: f, Imo2000P4.ValidPlacement, Imo2000P4.GoodPlacement
def Imo2000P4.lift Extend a placement g : Fin 100 → ZMod 3 to all of ℕ (by 0 outside [1, 100]); card a corresponds to index a - 1 line 381 source
Source documentation
Extend a placement g : Fin 100 → ZMod 3 to all of ℕ (by 0 outside [1, 100]); card a corresponds to index a - 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, ZMod
Proof uses: dite, And, LE.le, Fin.mk, HSub.hSub, Not
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def lift (g : Fin 100 → ZMod 3) (a : ℕ) : ZMod 3 :=
…
```
lemma Imo2000P4.lift_apply line 384 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, ZMod, LE.le, Eq, Imo2000P4.lift, Fin.mk, HSub.hSub
Proof uses: dite_eq_left, And, And.intro, Not
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.lift_apply_fin line 387 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, ZMod, Eq, Imo2000P4.lift, HAdd.hAdd
Proof uses: Eq.mpr, Fin.mk, HSub.hSub, id, congrArg, Imo2000P4.lift_apply, Fin.ext
14 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.lift_good line 391 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, ZMod, Imo2000P4.GoodPlacement, Imo2000P4.Good, Imo2000P4.lift
Proof uses: And.intro, Exists, And, LE.le, Eq, Ne, HAdd.hAdd, Or, And.left, Function.Surjective, Exists.intro, Eq.mpr, id, congrArg, Imo2000P4.lift_apply_fin, Fin.mk, HSub.hSub, Imo2000P4.lift_apply, And.right, Eq.mp
15 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
def Imo2000P4.T The box of card i in an "ends" placement line 405 source
Source documentation
The box of card i in an "ends" placement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, ZMod
Proof uses: ite, Eq
21 instances, coercions and auxiliary constants left out.
```
def T (i : Fin 100) : ZMod 3 := if (i : ℕ) = 0 then 0 else if (i : ℕ) = 99 then 1 else 2
```
lemma Imo2000P4.T_of_zero line 407 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, ZMod, Imo2000P4.T
Proof uses: id, Eq.mpr, ite, congrArg, ite_eq_left, Eq.refl
30 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.T_of_99 line 410 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, ZMod, Imo2000P4.T
Proof uses: id, Eq.mpr, ite, congrArg, ite_eq_right, ite_eq_left, Eq.refl
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.T_of_other line 413 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Eq, ZMod, Imo2000P4.T
Proof uses: id, Eq.mpr, ite, congrArg, ite_eq_right, Eq.refl
34 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.eq_zero_of_T line 416 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, ZMod, Imo2000P4.T
Proof uses: Decidable.byContradiction, Not, dite, False, absurd, Eq.mp, congrArg, Imo2000P4.T_of_99, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Imo2000P4.T_of_other
33 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.eq_99_of_T line 422 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, ZMod, Imo2000P4.T
Proof uses: Decidable.byContradiction, Not, dite, False, absurd, Eq.mp, congrArg, Imo2000P4.T_of_zero, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Imo2000P4.T_of_other
33 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.ne_of_T2 line 428 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, ZMod, Imo2000P4.T, And, Ne
Proof uses: And.intro, absurd, False, Eq.mp, congrArg, Imo2000P4.T_of_zero, of_decide_eq_true, Not, id, Bool, Decidable.decide, Bool.true, Eq.refl, Imo2000P4.T_of_99
34 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def Imo2000P4.mod3fun The mod-3 placements of the 100 cards line 434 source
Source documentation
The mod-3 placements of the 100 cards.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv.Perm, ZMod, OfNat.ofNat, Nat, Fin
Proof uses: HAdd.hAdd
16 instances, coercions and auxiliary constants left out.
```
def mod3fun (σ : Equiv.Perm (ZMod 3)) : Fin 100 → ZMod 3 :=
…
```
lemma Imo2000P4.mod3fun_apply0 line 437 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv.Perm, ZMod, OfNat.ofNat, Nat, Eq, Imo2000P4.mod3fun, Fin
Proof uses: id, Eq.mpr, HAdd.hAdd, congrArg, rfl, Nat.cast_one, Eq.refl
33 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.mod3fun_apply1 line 441 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv.Perm, ZMod, OfNat.ofNat, Nat, Eq, Imo2000P4.mod3fun, Fin
Proof uses: id, Eq.mpr, HAdd.hAdd, congrArg, rfl, Nat.cast_ofNat, Eq.refl
34 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.mod3fun_apply2 line 445 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv.Perm, ZMod, OfNat.ofNat, Nat, Eq, Imo2000P4.mod3fun, Fin
Proof uses: id, Eq.mpr, HAdd.hAdd, congrArg, rfl, ZMod.natCast_self, Eq.refl
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2000P4.endsfun The "ends" placements of the 100 cards line 450 source
Source documentation
The "ends" placements of the 100 cards.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv.Perm, ZMod, OfNat.ofNat, Nat, Fin
Proof uses: Imo2000P4.T
5 instances, coercions and auxiliary constants left out.
```
def endsfun (σ : Equiv.Perm (ZMod 3)) : Fin 100 → ZMod 3 := fun i ↦ σ (T i)
```
Mentions: Imo2000P4.T
lemma Imo2000P4.endsfun_apply0 line 452 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv.Perm, ZMod, OfNat.ofNat, Nat, Eq, Imo2000P4.endsfun, Fin
Proof uses: id, Eq.mpr, Imo2000P4.T, congrArg, Imo2000P4.T_of_zero, rfl, Eq.refl
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.endsfun_apply1 line 455 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv.Perm, ZMod, OfNat.ofNat, Nat, Eq, Imo2000P4.endsfun, Fin
Proof uses: id, Eq.mpr, Imo2000P4.T, congrArg, Imo2000P4.T_of_other, of_decide_eq_true, Ne, Bool, Decidable.decide, Bool.true, Eq.refl
33 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.endsfun_apply2 line 458 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv.Perm, ZMod, OfNat.ofNat, Nat, Eq, Imo2000P4.endsfun, Fin
Proof uses: id, Eq.mpr, Imo2000P4.T, congrArg, Imo2000P4.T_of_other, of_decide_eq_true, Ne, Bool, Decidable.decide, Bool.true, Eq.refl
33 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.endsfun_apply99 line 461 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv.Perm, ZMod, OfNat.ofNat, Nat, Eq, Imo2000P4.endsfun, Fin
Proof uses: id, Eq.mpr, Imo2000P4.T, congrArg, Imo2000P4.T_of_99, rfl, Eq.refl
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.mod3fun_valid line 464 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv.Perm, ZMod, OfNat.ofNat, Nat, Imo2000P4.GoodPlacement, Imo2000P4.mod3fun
Proof uses: And.intro, Function.Surjective, Fin, Ne, Eq, HAdd.hAdd, Or, And, Equiv, Exists, Equiv.surjective, Imo2000P4.tri, Exists.intro, Eq.mpr, id, congrArg, Imo2000P4.mod3fun_apply2, Eq.symm, Imo2000P4.mod3fun_apply0, Imo2000P4.mod3fun_apply1 and 8 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.bucket_of_ne For a pair of indices from two different T-boxes, the sum determines the (unordered) pair of T-values line 488 source
Source documentation
For a pair of indices from two different T-boxes, the sum determines the (unordered) pair of T-values.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, ZMod, Imo2000P4.T, Or, And, Eq, HAdd.hAdd, LT.lt
Proof uses: Imo2000P4.tri, absurd, Eq.trans, Eq.symm, Or.inl, And.intro, Imo2000P4.eq_zero_of_T, Imo2000P4.eq_99_of_T, Or.inr, Imo2000P4.ne_of_T2
54 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
lemma bucket_of_ne {i j : Fin 100} (hij : T i ≠ T j) :
    (((T i = 0 ∧ T j = 1) ∨ (T i = 1 ∧ T j = 0)) ∧ (i : ℕ) + j = 99) ∨
    (((T i = 0 ∧ T j = 2) ∨ (T i = 2 ∧ T j = 0)) ∧ (i : ℕ) + j < 99) ∨
    (((T i = 1 ∧ T j = 2) ∨ (T i = 2 ∧ T j = 1)) ∧ 99 < (i : ℕ) + j) := by
…
```
Mentions: Imo2000P4.T
lemma Imo2000P4.ends_pair line 509 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, ZMod, Imo2000P4.T, Eq, HAdd.hAdd, Or, And
Proof uses: LT.lt, Imo2000P4.bucket_of_ne, of_eq_true, Eq.trans, True, False, congr, congrArg, eq_self, and_self, or_false, or_true, False.elim, eq_false, id, Not, Eq.mp, false_and
41 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.endsfun_valid line 519 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv.Perm, ZMod, OfNat.ofNat, Nat, Imo2000P4.GoodPlacement, Imo2000P4.endsfun
Proof uses: And.intro, Function.Surjective, Fin, Ne, Eq, HAdd.hAdd, Or, And, Equiv, Exists, Equiv.surjective, Imo2000P4.tri, Exists.intro, Eq.mpr, id, congrArg, Imo2000P4.endsfun_apply0, Eq.symm, Imo2000P4.endsfun_apply99, Imo2000P4.endsfun_apply1 and 7 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.mem_solutions Every valid placement is one of the twelve explicit placements line 535 source
Source documentation
Every valid placement is one of the twelve explicit placements.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, ZMod, Imo2000P4.GoodPlacement, Membership.mem, Set, Union.union, Set.range, Equiv.Perm, Imo2000P4.mod3fun, Imo2000P4.endsfun
Proof uses: Imo2000P4.Mod3, Imo2000P4.lift, Imo2000P4.Ends, Or, Imo2000P4.classify, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Imo2000P4.lift_good, LE.le, Eq, Or.inl, Exists.intro, funext, HAdd.hAdd, Eq.symm, Eq.mp, congrArg and 12 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
```
lemma mem_solutions {g : Fin 100 → ZMod 3} (hg : GoodPlacement g) :
    g ∈ Set.range mod3fun ∪ Set.range endsfun := by
…
```
Mentions: Imo2000P4.GoodPlacement, Imo2000P4.mod3fun, Imo2000P4.endsfun
lemma Imo2000P4.mod3fun_injective line 567 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Equiv.Perm, ZMod, OfNat.ofNat, Nat, Fin, Imo2000P4.mod3fun
Proof uses: Eq, Equiv.Perm.ext, Or, Imo2000P4.tri, congrFun, Eq.mp, congrArg, Imo2000P4.mod3fun_apply2, Eq.symm, Imo2000P4.mod3fun_apply0, Imo2000P4.mod3fun_apply1
26 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.endsfun_injective line 581 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Equiv.Perm, ZMod, OfNat.ofNat, Nat, Fin, Imo2000P4.endsfun
Proof uses: Eq, Equiv.Perm.ext, Or, Imo2000P4.tri, congrFun, Eq.mp, congrArg, Imo2000P4.endsfun_apply0, Eq.symm, Imo2000P4.endsfun_apply99, Imo2000P4.endsfun_apply1
26 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.disjoint_ranges line 595 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Disjoint, Set, Fin, OfNat.ofNat, Nat, ZMod, Set.range, Equiv.Perm, Imo2000P4.mod3fun, Imo2000P4.endsfun
Proof uses: Eq.mpr, LE.le, Inter.inter, EmptyCollection.emptyCollection, id, Eq, congrArg, propext, Set.disjoint_iff, Membership.mem, congrFun, Eq.trans, Eq.mp, Imo2000P4.endsfun_apply1, Imo2000P4.mod3fun_apply1, Eq.symm, Imo2000P4.endsfun_apply2, Imo2000P4.mod3fun_apply2, Equiv.injective, absurd and 6 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.card_perm_zmod3 line 606 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Fintype.card, Equiv.Perm, ZMod, OfNat.ofNat
Proof uses: Nat.factorial, rfl, Eq.mpr, id, congrArg, Fintype.card_perm, ZMod.card, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.card_mod3fun_range line 610 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Set.ncard, Fin, OfNat.ofNat, ZMod, Set.range, Equiv.Perm, Imo2000P4.mod3fun
Proof uses: Eq.mpr, Set.image, Set.univ, id, congrArg, Set, Eq.symm, Set.image_univ, Set.ncard_image_of_injective, Imo2000P4.mod3fun_injective, Nat.card, Set.ncard_univ, Fintype.card, Nat.card_eq_fintype_card, Imo2000P4.card_perm_zmod3, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.card_endsfun_range line 614 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Set.ncard, Fin, OfNat.ofNat, ZMod, Set.range, Equiv.Perm, Imo2000P4.endsfun
Proof uses: Eq.mpr, Set.image, Set.univ, id, congrArg, Set, Eq.symm, Set.image_univ, Set.ncard_image_of_injective, Imo2000P4.endsfun_injective, Nat.card, Set.ncard_univ, Fintype.card, Nat.card_eq_fintype_card, Imo2000P4.card_perm_zmod3, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.card_solutions line 618 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Set.ncard, Fin, OfNat.ofNat, ZMod, Set.ofPred, Imo2000P4.GoodPlacement
Proof uses: HAdd.hAdd, rfl, Set, Union.union, Set.range, Equiv.Perm, Imo2000P4.mod3fun, Imo2000P4.endsfun, Set.ext, Iff.intro, Membership.mem, Imo2000P4.mem_solutions, Imo2000P4.mod3fun_valid, Imo2000P4.endsfun_valid, Eq.mpr, id, congrArg, Set.ncard_union_eq, Imo2000P4.disjoint_ranges, Set.toFinite and 3 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P4.card_valid The valid placements are exactly the good placements, so there are twelve of them line 634 source
Source documentation
The valid placements are exactly the good placements, so there are twelve of them.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Set.ncard, Fin, OfNat.ofNat, ZMod, Set.ofPred, Imo2000P4.ValidPlacement
Proof uses: Set, Imo2000P4.GoodPlacement, Set.ext, Imo2000P4.valid_iff_good, Eq.mpr, id, congrArg, Imo2000P4.card_solutions
2 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma card_valid : {g : Fin 100 → ZMod 3 | ValidPlacement g}.ncard = 12 := by
…
```
Mentions: Imo2000P4.ValidPlacement
determine Imo2000P4.solution_value line 643 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Imo2000P4.imo2000_p4 line 645 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Set.ncard, Fin, OfNat.ofNat, ZMod, Set.ofPred, Imo2000P4.ValidPlacement, Imo2000P4.solution_value
Proof uses: Imo2000P4.card_valid
1 instances, coercions and auxiliary constants left out.

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