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

66 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2016, Problem 2

Find all positive integers $n$ for which each cell of an $n \times n$ table can be filled with one of the letters $I$, $M$ and $O$ in such a way that:

in each row and each column, one third of the entries are $I$, one third are $M$ and one third are $O$; and
in any diagonal, if the number of entries on the diagonal is a multiple of three, then one third of the entries are $I$, one third are $M$ and one third are $O$.

Note. The rows and columns of an $n \times n$ table are each labelled $1$ to $n$ in a natural order. Thus each cell corresponds to a pair of positive integers $(i, j)$ with $1 \le i, j \le n$. For $n > 1$, the table has $4n - 2$ diagonals of two types. A diagonal of the first type consists of all cells $(i, j)$ for which $i + j$ is a constant, and a diagonal of the second type consists of all cells $(i, j)$ for which $i - j$ is constant.

Imports (2)

Imported by 1 file

Compfiles.lean

abbrev Imo2016P2.Letter The three letters I, M, O line 40 source
Source documentation
The three letters I, M, O.

no axioms what this means
Proof uses: Fin, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
```
abbrev Letter := Fin 3
…
```
def Imo2016P2.Balanced A finite set of cells is balanced under the coloring f if each of the three letters occurs on exactly one third of its cells line 46 source
Source documentation
A finite set of cells is balanced under the coloring f if each of the three letters occurs on exactly one third of its cells.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo2016P2.Letter, Finset, Prod
Proof uses: Eq, Finset.card, Finset.filter, Prod.fst, Prod.snd, OfNat.ofNat, HDiv.hDiv
4 instances, coercions and auxiliary constants left out.
```
def Balanced (f : Fin n → Fin n → Letter) (cells : Finset (Fin n × Fin n)) : Prop :=
…
```
Mentions: f, Imo2016P2.Letter
def Imo2016P2.row The cells of row r line 50 source
Source documentation
The cells of row r.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, Prod
Proof uses: Finset.filter, Eq, Prod.fst, Finset.univ
3 instances, coercions and auxiliary constants left out.
```
def row (r : Fin n) : Finset (Fin n × Fin n) := Finset.univ.filter (fun p ↦ p.1 = r)
```
def Imo2016P2.col The cells of column k line 53 source
Source documentation
The cells of column k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, Prod
Proof uses: Finset.filter, Eq, Prod.snd, Finset.univ
3 instances, coercions and auxiliary constants left out.
```
def col (k : Fin n) : Finset (Fin n × Fin n) := Finset.univ.filter (fun p ↦ p.2 = k)
```
def Imo2016P2.diagSum A diagonal of the first type: the cells (i, j) with i + j = s line 56 source
Source documentation
A diagonal of the first type: the cells (i, j) with i + j = s.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin
Proof uses: Finset.filter, Eq, HAdd.hAdd, Prod.fst, Prod.snd, Finset.univ
6 instances, coercions and auxiliary constants left out.
```
def diagSum (s : ℕ) : Finset (Fin n × Fin n) :=
…
```
def Imo2016P2.diagDiff A diagonal of the second type: the cells (i, j) with i - j = d line 60 source
Source documentation
A diagonal of the second type: the cells (i, j) with i - j = d.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Finset, Prod, Fin
Proof uses: Finset.filter, Eq, HSub.hSub, Prod.fst, Prod.snd, Finset.univ
8 instances, coercions and auxiliary constants left out.
```
def diagDiff (d : ℤ) : Finset (Fin n × Fin n) :=
…
```
def Imo2016P2.MODTable The coloring f of the n × n table satisfies all the required conditions: every row and column is balanced, and every diagonal whose length is a multiple of three is balanced line 66 source
Source documentation
The coloring f of the n × n table satisfies all the required conditions: every row and column is balanced, and every diagonal whose length is a multiple of three is balanced.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo2016P2.Letter
Proof uses: And, Imo2016P2.Balanced, Imo2016P2.row, Imo2016P2.col, Dvd.dvd, OfNat.ofNat, Finset.card, Prod, Imo2016P2.diagSum, Int, Imo2016P2.diagDiff
2 instances, coercions and auxiliary constants left out.
```
def MODTable (f : Fin n → Fin n → Letter) : Prop :=
…
```
Mentions: f, Imo2016P2.Letter
determine Imo2016P2.solution line 72 source
no axioms what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, Dvd.dvd, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
def Imo2016P2.periodicColor line 76 source
standard axioms: propext what this means
Statement uses: Nat, Fin, Imo2016P2.Letter
Proof uses: Fin.ofNat, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv
7 instances, coercions and auxiliary constants left out.
lemma Imo2016P2.row_eq_product line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset, Prod, Imo2016P2.row, SProd.sprod, Singleton.singleton, Finset.univ
Proof uses: Finset.ext, Iff, Membership.mem, of_eq_true, Prod.mk, Eq.trans, True, congr, congrArg, And, Prod.fst, Finset.filter, congrFun', Finset.filter_congr, Iff.of_eq, true_and, Exists, Function.Embedding, Function.Embedding.sectR, Finset.map and 12 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.map_filter_periodicColor line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo2016P2.Letter, Eq, Finset, Finset.map, Fin.valEmbedding, Finset.filter, Imo2016P2.periodicColor, OfNat.ofNat, Finset.univ, Fin.ofNat, HAdd.hAdd, HDiv.hDiv, Finset.range
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, And, LT.lt, id, congr, congrArg, Eq.trans, Function.Embedding, funext, True, congrFun', true_and, congrFun, Fin.valEmbedding_apply, Iff.intro, And.intro and 4 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.row_block_count line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2016P2.Letter, Eq, Finset.card, Finset.filter, Fin, OfNat.ofNat, Fin.ofNat, HAdd.hAdd, HDiv.hDiv, Finset.range
Proof uses: LT.lt, HMod.hMod, Nat.mod_lt, dite, LE.le, 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, Eq.mpr and 34 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.row_periodic_count line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2016P2.Letter, Eq, Finset.card, Finset.filter, Fin, OfNat.ofNat, Fin.ofNat, HAdd.hAdd, HDiv.hDiv, Finset.range, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, Finset, EmptyCollection.emptyCollection, Fin.NatCast.instNatCast, Finset.filter_congr, Membership.mem, Iff.of_eq, Eq.refl, Finset.filter.congr_simp, MulZeroClass.mul_zero, Finset.filter_empty, eq_self, Eq.mpr, id, Union.union and 32 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.add_block_count line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2016P2.Letter, Eq, Finset.card, Finset.filter, Fin, OfNat.ofNat, Fin.ofNat, HAdd.hAdd, Finset.range
Proof uses: LT.lt, HMod.hMod, Nat.mod_lt, dite, LE.le, 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, Eq.mpr and 34 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.add_periodic_count line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2016P2.Letter, Eq, Finset.card, Finset.filter, Fin, OfNat.ofNat, Fin.ofNat, HAdd.hAdd, Finset.range, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset, EmptyCollection.emptyCollection, Fin.NatCast.instNatCast, Finset.filter_congr, Membership.mem, Iff.of_eq, Eq.refl, Finset.filter.congr_simp, MulZeroClass.mul_zero, Finset.filter_empty, eq_self, Eq.mpr, id, Union.union and 32 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.col_eq_product line 177 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset, Prod, Imo2016P2.col, SProd.sprod, Finset.univ, Singleton.singleton
Proof uses: Finset.ext, Iff, Membership.mem, of_eq_true, Prod.mk, Eq.trans, True, congr, congrArg, And, Prod.snd, Finset.filter, congrFun', Finset.filter_congr, Iff.of_eq, true_and, Exists, Function.Embedding, Function.Embedding.sectL, Finset.map and 11 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.map_filter_periodicColor_col line 182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo2016P2.Letter, Eq, Finset, Finset.map, Fin.valEmbedding, Finset.filter, Imo2016P2.periodicColor, OfNat.ofNat, Finset.univ, Fin.ofNat, HAdd.hAdd, HDiv.hDiv, Finset.range
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, And, LT.lt, id, congr, congrArg, Eq.trans, Function.Embedding, funext, True, congrFun', true_and, congrFun, Fin.valEmbedding_apply, Iff.intro, And.intro and 4 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.diagSum_card_eq line 194 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Fin, Imo2016P2.diagSum, HSub.hSub, Min.min, HAdd.hAdd, OfNat.ofNat
Proof uses: Trans.trans, Finset.Ico, Finset.card_bij, Membership.mem, Finset, Prod.snd, Eq.mpr, And, LE.le, LT.lt, id, And.intro, Eq.mp, Prod.fst, Eq.trans, Finset.filter, Finset.univ, True, congrFun', congrArg and 9 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.diagSum_color_card_eq line 219 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2016P2.Letter, Eq, Finset.card, Prod, Fin, Finset.filter, Imo2016P2.periodicColor, Prod.fst, Prod.snd, OfNat.ofNat, Imo2016P2.diagSum, Fin.ofNat, HAdd.hAdd, HSub.hSub, HDiv.hDiv, Finset.Ico, Min.min
Proof uses: Finset.card_bij, Membership.mem, Finset, Eq.mpr, And, id, And.intro, LE.le, LT.lt, Eq.mp, congrFun', congrArg, Eq.trans, Finset.univ, True, true_and, Fin.NatCast.instNatCast, Fin.ofNat.congr_simp, And.right, Prod.ext and 6 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.desc_block_count line 252 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2016P2.Letter, Eq, Finset.card, Finset.filter, Fin, OfNat.ofNat, Fin.ofNat, HSub.hSub, HAdd.hAdd, Finset.range
Proof uses: Trans.trans, HMod.hMod, Finset, Eq.rec, Eq.refl, Finset.ext, Eq.mpr, Iff, Membership.mem, And, LT.lt, id, congr, congrArg, Eq.trans, congrFun', Iff.intro, And.intro, Eq.symm, Fin.ext and 49 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.desc_block_count' line 283 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2016P2.Letter, Eq, Finset.card, Finset.filter, Fin, Fin.ofNat, HSub.hSub, Finset.range
Proof uses: Trans.trans, HAdd.hAdd, Finset, Eq.rec, Eq.refl, Finset.ext, Eq.mpr, Iff, Membership.mem, And, LT.lt, id, congr, congrArg, Eq.trans, congrFun', Fin.ext, of_eq_true, HMod.hMod, True and 8 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.desc_periodic_count line 306 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2016P2.Letter, LE.le, HMul.hMul, OfNat.ofNat, HAdd.hAdd, Eq, Finset.card, Finset.filter, Fin, Fin.ofNat, HSub.hSub, HDiv.hDiv, Finset.range
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset, EmptyCollection.emptyCollection, Fin.NatCast.instNatCast, Finset.filter_congr, Membership.mem, Iff.of_eq, Eq.refl, Finset.filter.congr_simp, MulZeroClass.mul_zero, Finset.filter_empty, eq_self, Eq.mpr, id, Union.union and 25 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.Ico_eq_map_range line 349 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Finset.Ico, Finset.map, addLeftEmbedding, Finset.range, HSub.hSub
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, LE.le, LT.lt, Exists, HAdd.hAdd, id, congr, congrArg, Eq.trans, Function.Embedding, funext, congrFun', addLeftEmbedding_apply, Iff.intro, Exists.intro, And.intro
37 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.periodicColor_diagSum line 360 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, OfNat.ofNat, Finset.card, Prod, Fin, Imo2016P2.diagSum, Imo2016P2.Balanced, Imo2016P2.periodicColor
Proof uses: id, Imo2016P2.Letter, Eq.mpr, Eq, Finset.filter, Prod.fst, Prod.snd, HDiv.hDiv, Fin.ofNat, HAdd.hAdd, HSub.hSub, Finset.Ico, Min.min, congrArg, Imo2016P2.diagSum_color_card_eq, Imo2016P2.diagSum_card_eq, Eq.mp, dite, Finset.map, addLeftEmbedding and 44 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.diagDiff_card_eq_nonneg line 415 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Fin, Imo2016P2.diagDiff, Int, HSub.hSub
Proof uses: Trans.trans, Finset.range, Finset.card_bij, Membership.mem, Finset, Prod.snd, Eq.mpr, LT.lt, id, Decidable.byContradiction, Not, Eq.mp, Prod.fst, Eq.trans, Finset.filter, Finset.univ, And, True, congrFun', congrArg and 16 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.diagDiff_card_eq_neg line 438 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Fin, Imo2016P2.diagDiff, Neg.neg, Int, HSub.hSub
Proof uses: Trans.trans, Finset.range, Finset.card_bij, Membership.mem, Finset, Prod.fst, Eq.mpr, LT.lt, id, Decidable.byContradiction, Not, Eq.mp, Prod.snd, Eq.trans, Finset.filter, Finset.univ, And, True, congrFun', congrArg and 16 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.diagDiff_color_card_eq_nonneg line 461 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2016P2.Letter, Eq, Finset.card, Prod, Fin, Finset.filter, Imo2016P2.periodicColor, Prod.fst, Prod.snd, OfNat.ofNat, Imo2016P2.diagDiff, Int, Fin.ofNat, HAdd.hAdd, HDiv.hDiv, Finset.range, HSub.hSub
Proof uses: Finset.card_bij, Membership.mem, Finset, Eq.mpr, And, id, And.intro, LT.lt, Decidable.byContradiction, Not, Eq.mp, congrFun', congrArg, Eq.trans, Finset.univ, True, true_and, Fin.NatCast.instNatCast, Fin.ofNat.congr_simp, Nat.add_assoc and 14 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.diagDiff_color_card_eq_neg line 493 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2016P2.Letter, Eq, Finset.card, Prod, Fin, Finset.filter, Imo2016P2.periodicColor, Prod.fst, Prod.snd, OfNat.ofNat, Imo2016P2.diagDiff, Neg.neg, Int, Fin.ofNat, HAdd.hAdd, HDiv.hDiv, Finset.range, HSub.hSub
Proof uses: Finset.card_bij, Membership.mem, Finset, Eq.mpr, And, id, And.intro, LT.lt, Decidable.byContradiction, Not, Eq.mp, congrFun', congrArg, Eq.trans, Finset.univ, True, true_and, Fin.NatCast.instNatCast, Fin.ofNat.congr_simp, And.right and 13 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.asc_periodic_count line 525 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2016P2.Letter, Eq, Finset.card, Finset.filter, Fin, OfNat.ofNat, Fin.ofNat, HAdd.hAdd, HDiv.hDiv, Finset.range, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset, EmptyCollection.emptyCollection, Fin.NatCast.instNatCast, Finset.filter_congr, Membership.mem, Iff.of_eq, Eq.refl, Finset.filter.congr_simp, MulZeroClass.mul_zero, Finset.filter_empty, eq_self, Eq.mpr, id, Union.union and 26 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.periodicColor_diagDiff line 565 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, OfNat.ofNat, Int, Finset.card, Prod, Fin, Imo2016P2.diagDiff, Imo2016P2.Balanced, Imo2016P2.periodicColor
Proof uses: id, Imo2016P2.Letter, dite, Eq, Finset.filter, Prod.fst, Prod.snd, HDiv.hDiv, LE.le, Int.toNat, Int.toNat_of_nonneg, HSub.hSub, Eq.mpr, congrArg, Eq.symm, Imo2016P2.diagDiff_card_eq_nonneg, Finset, HMul.hMul, Fin.ofNat, HAdd.hAdd and 33 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.periodicColor_row line 619 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Dvd.dvd, OfNat.ofNat, Imo2016P2.Balanced, Imo2016P2.periodicColor, Imo2016P2.row
Proof uses: id, Imo2016P2.Letter, Eq.mpr, Eq, Finset.card, Prod, Finset.filter, Prod.fst, Prod.snd, HDiv.hDiv, SProd.sprod, Finset, Singleton.singleton, Finset.univ, congrArg, Imo2016P2.row_eq_product, Finset.ext, Iff, Membership.mem, Prod.mk and 25 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.periodicColor_col line 649 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Dvd.dvd, OfNat.ofNat, Imo2016P2.Balanced, Imo2016P2.periodicColor, Imo2016P2.col
Proof uses: id, Imo2016P2.Letter, Eq.mpr, Eq, Finset.card, Prod, Finset.filter, Prod.fst, Prod.snd, HDiv.hDiv, SProd.sprod, Finset, Finset.univ, Singleton.singleton, congrArg, Imo2016P2.col_eq_product, Finset.ext, Iff, Membership.mem, Prod.mk and 31 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.exists_modTable_of_nine_dvd line 684 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, OfNat.ofNat, Exists, Fin, Imo2016P2.Letter, Imo2016P2.MODTable
Proof uses: Exists.intro, Imo2016P2.periodicColor, And.intro, Imo2016P2.Balanced, Imo2016P2.row, And, Imo2016P2.col, Finset.card, Prod, Imo2016P2.diagSum, Int, Imo2016P2.diagDiff, Imo2016P2.periodicColor_row, Imo2016P2.periodicColor_col, Imo2016P2.periodicColor_diagSum, Imo2016P2.periodicColor_diagDiff
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.Balanced.three_dvd_card line 692 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo2016P2.Letter, Finset, Prod, Imo2016P2.Balanced, Dvd.dvd, OfNat.ofNat, Finset.card
Proof uses: Eq, Finset.sum, Finset.univ, Finset.filter, Prod.fst, Prod.snd, Finset.card_eq_sum_card_fiberwise, of_eq_true, Set.MapsTo, Eq.trans, Set.univ, True, congrArg, Set, Finset.coe_univ, HMul.hMul, HDiv.hDiv, Trans.trans, Finset.sum_congr, rfl and 7 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.balanced_of_fibers line 708 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidableEq, Fin, Imo2016P2.Letter, Finset, Prod, Membership.mem, Imo2016P2.Balanced, Finset.filter, Eq
Proof uses: Finset.card, Finset.sum, Finset.card_eq_sum_card_fiberwise, HMul.hMul, OfNat.ofNat, HDiv.hDiv, Dvd.dvd, Imo2016P2.Balanced.three_dvd_card, Trans.trans, Finset.sum_congr, rfl, Eq.mpr, id, congrArg, Finset.mul_sum, Eq.refl, Prod.fst, Prod.snd, And.left, Iff.mp and 10 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
def Imo2016P2.vitalIndices line 755 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, HMul.hMul, OfNat.ofNat
Proof uses: Finset.filter, Eq, Fin.ofNat, Finset.univ
11 instances, coercions and auxiliary constants left out.
def Imo2016P2.vitalRowCells line 758 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin, HMul.hMul, OfNat.ofNat
Proof uses: SProd.sprod, Imo2016P2.vitalIndices, Finset.univ
8 instances, coercions and auxiliary constants left out.
def Imo2016P2.vitalColCells line 761 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin, HMul.hMul, OfNat.ofNat
Proof uses: SProd.sprod, Finset.univ, Imo2016P2.vitalIndices
8 instances, coercions and auxiliary constants left out.
def Imo2016P2.vitalSumCells line 764 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin, HMul.hMul, OfNat.ofNat
Proof uses: Finset.filter, Eq, Fin.ofNat, HAdd.hAdd, Prod.fst, Prod.snd, Finset.univ
14 instances, coercions and auxiliary constants left out.
def Imo2016P2.vitalDiffCells line 767 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin, HMul.hMul, OfNat.ofNat
Proof uses: Finset.filter, Eq, Fin.ofNat, Prod.fst, Prod.snd, Finset.univ
11 instances, coercions and auxiliary constants left out.
def Imo2016P2.centerCells line 770 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Fin, HMul.hMul, OfNat.ofNat
Proof uses: SProd.sprod, Imo2016P2.vitalIndices
7 instances, coercions and auxiliary constants left out.
def Imo2016P2.colorCount line 773 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo2016P2.Letter, Finset, Prod
Proof uses: Finset.card, Finset.filter, Eq, Prod.fst, Prod.snd, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
def Imo2016P2.vitalSumKeys line 777 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: Finset.filter, Eq, Fin, OfNat.ofNat, Fin.ofNat, Finset.range, HMul.hMul
6 instances, coercions and auxiliary constants left out.
def Imo2016P2.vitalDiffKeys line 780 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Int
Proof uses: Finset.filter, Dvd.dvd, OfNat.ofNat, Finset.map, Function.Embedding.mk, HSub.hSub, HMul.hMul, Eq, Finset.range, HAdd.hAdd
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.card_filter_grid line 786 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, DecidableRel, Eq, Finset.card, Prod, Finset.filter, Prod.fst, Prod.snd, Finset.univ, Finset.sum
Proof uses: Finset, Membership.mem, of_eq_true, Eq.trans, True, forall_congr, implies_congr, Eq.refl, implies_true, Trans.trans, Finset.card_eq_sum_card_fiberwise, Finset.sum_congr, rfl, Finset.card_bij, Eq.mpr, id, And, congrFun', congrArg, true_and and 12 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.fin_add_count line 810 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2016P2.Letter, Eq, Finset.card, Fin, HMul.hMul, OfNat.ofNat, Finset.filter, Fin.ofNat, HAdd.hAdd, Finset.univ
Proof uses: Finset, Finset.map, Fin.valEmbedding, Finset.range, Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, And, LT.lt, id, congr, congrArg, Eq.trans, Function.Embedding, funext, True, congrFun', true_and and 11 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.vitalIndices_card line 828 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Fin, HMul.hMul, OfNat.ofNat, Imo2016P2.vitalIndices
Proof uses: Eq.mpr, Finset.filter, Fin.NatCast.instNatCast, Finset.univ, id, congrFun', congrArg, Finset, Finset.filter_congr, Fin.ofNat, Membership.mem, Iff.of_eq, Eq.refl, Eq.mp, HAdd.hAdd, Imo2016P2.Letter, Fin.ofNat.congr_simp, zero_add, Imo2016P2.fin_add_count
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.vitalRowCells_card line 831 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Fin, HMul.hMul, OfNat.ofNat, Imo2016P2.vitalRowCells, HPow.hPow
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, SProd.sprod, Finset, Imo2016P2.vitalIndices, Finset.univ, Finset.card_product, congr, Imo2016P2.vitalIndices_card, Fintype.card_fin, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm and 22 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.vitalColCells_card line 835 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Fin, HMul.hMul, OfNat.ofNat, Imo2016P2.vitalColCells, HPow.hPow
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, SProd.sprod, Finset, Finset.univ, Imo2016P2.vitalIndices, Finset.card_product, congr, Fintype.card_fin, Imo2016P2.vitalIndices_card, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 22 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.vitalSumCells_card line 839 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Fin, HMul.hMul, OfNat.ofNat, Imo2016P2.vitalSumCells, HPow.hPow
Proof uses: Trans.trans, Finset.sum, Finset.univ, Finset.filter, Fin.ofNat, HAdd.hAdd, Imo2016P2.card_filter_grid, Finset.sum_congr, rfl, Finset, Membership.mem, Imo2016P2.fin_add_count, Imo2016P2.Letter, Eq.mpr, id, congrFun', congrArg, Eq.trans, HSMul.hSMul, Finset.sum_const and 28 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.vitalDiffCells_card line 853 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Fin, HMul.hMul, OfNat.ofNat, Imo2016P2.vitalDiffCells, HPow.hPow
Proof uses: Trans.trans, Finset.sum, Finset.univ, Finset.filter, Fin.ofNat, Imo2016P2.card_filter_grid, Finset.sum_congr, rfl, Finset, Membership.mem, Eq.mpr, Fin.NatCast.instNatCast, id, Eq.trans, congrFun', congrArg, Finset.filter_congr, Iff.of_eq, Eq.refl, Eq.mp and 33 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.three_dvd_diagSum_card line 867 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Fin, OfNat.ofNat, Fin.ofNat, Dvd.dvd, Finset.card, Prod, HMul.hMul, Imo2016P2.diagSum
Proof uses: HMod.hMod, Eq.mp, congrArg, Nat.mod_succ, HAdd.hAdd, HDiv.hDiv, Nat.div_add_mod, Eq.mpr, HSub.hSub, Min.min, id, Imo2016P2.diagSum_card_eq, dite, LE.le, Exists.intro, Nat.min_eq_right, Nat.sub_eq_zero_of_le, Not, Nat.min_eq_left
30 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.three_dvd_diagDiff_card line 887 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Dvd.dvd, OfNat.ofNat, Finset.card, Prod, Fin, HMul.hMul, Imo2016P2.diagDiff
Proof uses: Eq, dite, LE.le, Int.toNat, Int.toNat_of_nonneg, Eq.mpr, id, congrArg, Eq.symm, HSub.hSub, Imo2016P2.diagDiff_card_eq_nonneg, Exists.intro, Not, Neg.neg, Imo2016P2.diagDiff_card_eq_neg
29 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.finMod_eq_iff_three_dvd_sub line 910 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Eq, Fin, OfNat.ofNat, Fin.ofNat, Dvd.dvd, Int, HSub.hSub
Proof uses: Iff.intro, HMod.hMod, congrArg, HAdd.hAdd, HMul.hMul, HDiv.hDiv, Nat.div_add_mod, Exists.intro, Fin.ext, id, LT.lt, Nat.mod_lt
32 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.univ_balanced_of_rows line 929 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo2016P2.Letter, Imo2016P2.Balanced, Imo2016P2.row, Finset.univ, Prod
Proof uses: Imo2016P2.balanced_of_fibers, Prod.fst, of_eq_true, Membership.mem, Finset, Eq.trans, True, forall_congr, implies_congr, implies_true
9 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.vitalRowCells_balanced line 937 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Imo2016P2.Letter, Imo2016P2.Balanced, Imo2016P2.row, Imo2016P2.vitalRowCells
Proof uses: Imo2016P2.balanced_of_fibers, Imo2016P2.vitalIndices, Prod, Prod.fst, Membership.mem, Finset, And.left, Finset.univ, Prod.snd, Iff.mp, SProd.sprod, And, Finset.mem_product, Eq.mpr, Finset.filter, Eq, eq_of_heq, HEq, Eq.refl, HEq.refl and 16 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.vitalColCells_balanced line 955 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Imo2016P2.Letter, Imo2016P2.Balanced, Imo2016P2.col, Imo2016P2.vitalColCells
Proof uses: Imo2016P2.balanced_of_fibers, Imo2016P2.vitalIndices, Prod, Prod.snd, Membership.mem, Finset, And.right, Finset.univ, Prod.fst, Iff.mp, SProd.sprod, And, Finset.mem_product, Eq.mpr, Finset.filter, Eq, eq_of_heq, HEq, Eq.refl, HEq.refl and 14 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.vitalSumCells_balanced line 973 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Imo2016P2.Letter, Dvd.dvd, Finset.card, Prod, Imo2016P2.diagSum, Imo2016P2.Balanced, Imo2016P2.vitalSumCells
Proof uses: Imo2016P2.balanced_of_fibers, Imo2016P2.vitalSumKeys, HAdd.hAdd, Prod.fst, Prod.snd, Membership.mem, Finset, Eq.mpr, And, LT.lt, Eq, Fin.ofNat, id, Eq.trans, Finset.filter, Finset.range, congrFun', congrArg, And.intro, Eq.mp and 17 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.vitalDiffCells_balanced line 996 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Imo2016P2.Letter, Int, Dvd.dvd, Finset.card, Prod, Imo2016P2.diagDiff, Imo2016P2.Balanced, Imo2016P2.vitalDiffCells
Proof uses: Imo2016P2.balanced_of_fibers, Imo2016P2.vitalDiffKeys, HSub.hSub, Prod.fst, Prod.snd, Membership.mem, Finset, Eq.mpr, And, Exists, Finset.range, HAdd.hAdd, Eq, id, Eq.trans, Finset.filter, Finset.map, Function.Embedding.mk, congrFun', congrArg and 23 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.three_dvd_of_modTable line 1026 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Imo2016P2.Letter, Imo2016P2.MODTable, Dvd.dvd
Proof uses: Fin.mk, Finset.card, Prod, Imo2016P2.row, Imo2016P2.Balanced.three_dvd_card, And.left, Imo2016P2.Balanced, And, Imo2016P2.col, Imo2016P2.diagSum, Int, Imo2016P2.diagDiff, Eq.mp, SProd.sprod, Finset, Singleton.singleton, Finset.univ, congrArg, Eq.trans, Finset.map and 5 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.vital_incidence_indicator line 1033 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Fin, HMul.hMul, OfNat.ofNat, Eq, HAdd.hAdd, ite, Membership.mem, Finset, Imo2016P2.vitalRowCells, Imo2016P2.vitalColCells, Imo2016P2.vitalSumCells, Imo2016P2.vitalDiffCells, Imo2016P2.centerCells
Proof uses: Fin.ofNat, Prod.fst, Prod.snd, Fin.ext, of_eq_true, Eq.trans, HMod.hMod, True, congr, congrArg, Fin.mk, LT.lt, Nat.add_mod, congrFun', Nat.mod_mod_of_dvd, Dvd.dvd, Fin.mk.congr_simp, eq_self, Eq.mpr, And and 29 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.colorCount_eq_sum_indicator line 1051 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo2016P2.Letter, Finset, Prod, Eq, Imo2016P2.colorCount, Finset.sum, Finset.univ, ite, And, Membership.mem, Prod.fst, Prod.snd, OfNat.ofNat
Proof uses: id, Eq.mpr, Finset.card, Finset.filter, congrArg, Finset.card_eq_sum_ite, of_eq_true, LE.le, Eq.trans, True, congrFun', Finset.sum_congr, Eq.refl, ite_congr, Not, eq_self
25 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.vital_color_count_identity line 1059 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Imo2016P2.Letter, Eq, HAdd.hAdd, Imo2016P2.colorCount, Imo2016P2.vitalRowCells, Imo2016P2.vitalColCells, Imo2016P2.vitalSumCells, Imo2016P2.vitalDiffCells, Finset.univ, Prod, Imo2016P2.centerCells
Proof uses: Eq.mpr, Finset.sum, ite, And, Membership.mem, Finset, Prod.fst, Prod.snd, id, congr, congrArg, Imo2016P2.colorCount_eq_sum_indicator, Eq.symm, Finset.sum_add_distrib, Finset.mul_sum, Finset.sum_congr, rfl, dite, ite_congr, Eq.trans and 18 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.colorCount_eq_of_balanced_card line 1074 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo2016P2.Letter, Finset, Prod, Imo2016P2.Balanced, Eq, Finset.card, HMul.hMul, OfNat.ofNat, Imo2016P2.colorCount
Proof uses: id, Eq.mpr, Finset.filter, Prod.fst, Prod.snd, HDiv.hDiv, congrArg
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P2.nine_dvd_of_modTable line 1081 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Imo2016P2.Letter, Imo2016P2.MODTable, Dvd.dvd
Proof uses: Imo2016P2.three_dvd_of_modTable, Eq, HMul.hMul, Imo2016P2.Balanced, Imo2016P2.row, And, Imo2016P2.col, Finset.card, Prod, Imo2016P2.diagSum, Int, Imo2016P2.diagDiff, Imo2016P2.vitalRowCells, Imo2016P2.vitalRowCells_balanced, Imo2016P2.vitalColCells, Imo2016P2.vitalColCells_balanced, Imo2016P2.vitalSumCells, Imo2016P2.vitalSumCells_balanced, Imo2016P2.vitalDiffCells, Imo2016P2.vitalDiffCells_balanced and 53 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
problem Imo2016P2.imo2016_p2 line 1117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Iff, Membership.mem, Set, Imo2016P2.solution, Exists, Fin, Imo2016P2.Letter, Imo2016P2.MODTable
Proof uses: Iff.intro, Imo2016P2.exists_modTable_of_nine_dvd, Imo2016P2.nine_dvd_of_modTable
7 instances, coercions and auxiliary constants left out.

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