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

48 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1998, Problem 4

A computer screen shows a 98 × 98 chessboard, colored in the usual way. One can select with a mouse any rectangle with sides on the lines of the chessboard and click the mouse button: as a result, the colors in the selected rectangle switch (black becomes white, white becomes black). Find, with proof, the minimum number of mouse clicks needed to make the chessboard all one color.

Imports (4)

Imported by 1 file

Compfiles.lean

def Usa1998P4.chessboard line 32 source
no axioms what this means
Proof uses: Prod, Fin, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
def Usa1998P4.coloring line 34 source
no axioms what this means
Proof uses: Usa1998P4.chessboard, ZMod, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
def Usa1998P4.all_same_color line 36 source
no axioms what this means
Statement uses: Usa1998P4.coloring
Proof uses: Exists, ZMod, OfNat.ofNat, Nat, Usa1998P4.chessboard, Eq
1 instances, coercions and auxiliary constants left out.
structure Usa1998P4.Rectangle line 39 source
no axioms what this means
def Usa1998P4.recolor_rect line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.coloring, Usa1998P4.Rectangle
Proof uses: Usa1998P4.chessboard, Usa1998P4.recolor_rect.match_1, ZMod, OfNat.ofNat, Nat, Fin, ite, And, LE.le, Usa1998P4.Rectangle.x, Usa1998P4.Rectangle.y, LT.lt, HAdd.hAdd, Usa1998P4.Rectangle.width, Usa1998P4.Rectangle.height, Prod.mk
22 instances, coercions and auxiliary constants left out.
def Usa1998P4.start_coloring line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.coloring
Proof uses: Usa1998P4.chessboard, Usa1998P4.recolor_rect.match_1, ZMod, OfNat.ofNat, Nat, Fin, HAdd.hAdd
16 instances, coercions and auxiliary constants left out.
def Usa1998P4.possible_num_clicks line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, Exists, List, Usa1998P4.Rectangle, And, Usa1998P4.all_same_color, List.foldl, Usa1998P4.coloring, Usa1998P4.recolor_rect, Usa1998P4.start_coloring, Eq, List.length
determine Usa1998P4.min_clicks line 62 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
def Usa1998P4.rectColor The indicator coloring of a rectangle line 86 source
Source documentation
The indicator coloring of a rectangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.Rectangle, Usa1998P4.coloring
Proof uses: Usa1998P4.chessboard, ite, ZMod, OfNat.ofNat, Nat, And, LE.le, Usa1998P4.Rectangle.x, Prod.fst, Fin, Usa1998P4.Rectangle.y, Prod.snd, LT.lt, HAdd.hAdd, Usa1998P4.Rectangle.width, Usa1998P4.Rectangle.height
23 instances, coercions and auxiliary constants left out.
```
def rectColor (r : Rectangle) : coloring :=
…
```
Mentions: Usa1998P4.Rectangle, Usa1998P4.coloring
lemma Usa1998P4.recolor_rect_apply line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.coloring, Usa1998P4.Rectangle, Usa1998P4.chessboard, Eq, ZMod, OfNat.ofNat, Nat, Usa1998P4.recolor_rect, HAdd.hAdd, Usa1998P4.rectColor
Proof uses: Fin, id, Prod.mk, Usa1998P4.recolor_rect.match_1, ite, And, LE.le, Usa1998P4.Rectangle.x, Usa1998P4.Rectangle.y, LT.lt, Usa1998P4.Rectangle.width, Usa1998P4.Rectangle.height, Prod.fst, Prod.snd, dite, Eq.mpr, congr, congrArg, ite_eq_left, of_eq_true and 6 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.foldl_recolor_apply line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Usa1998P4.Rectangle, Usa1998P4.coloring, Usa1998P4.chessboard, Eq, ZMod, OfNat.ofNat, Nat, List.foldl, Usa1998P4.recolor_rect, HAdd.hAdd, List.sum, List.map, Usa1998P4.rectColor
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congrArg, List.map_nil, add_zero, eq_self, Eq.mpr, List.cons, id, List.foldl_cons, List.map_cons, List.sum_cons, Usa1998P4.recolor_rect_apply, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast and 7 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
abbrev Usa1998P4.Corner line 108 source
no axioms what this means
Proof uses: Prod, Fin, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
def Usa1998P4.cellValue Extend a coloring by zero outside the board line 111 source
Source documentation
Extend a coloring by zero outside the board.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.coloring, Nat, ZMod, OfNat.ofNat
Proof uses: dite, LT.lt, Prod.mk, Fin, Fin.mk, Not
12 instances, coercions and auxiliary constants left out.
```
def cellValue (f : coloring) (x y : ℕ) : ZMod 2 :=
…
```
Mentions: f, Usa1998P4.coloring
def Usa1998P4.addColoring line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.coloring
Proof uses: Usa1998P4.chessboard, HAdd.hAdd, ZMod, OfNat.ofNat, Nat
9 instances, coercions and auxiliary constants left out.
lemma Usa1998P4.cellValue_add line 121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.coloring, Nat, Eq, ZMod, OfNat.ofNat, Usa1998P4.cellValue, Usa1998P4.addColoring, HAdd.hAdd
Proof uses: id, dite, LT.lt, Prod.mk, Fin, Fin.mk, Not, Eq.mpr, congr, congrArg, dite_eq_left, of_eq_true, eq_self, dite_eq_right, Eq.trans, True, add_zero
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Usa1998P4.maskedCell line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Decidable, Usa1998P4.coloring, Nat, ZMod, OfNat.ofNat
Proof uses: ite, Usa1998P4.cellValue
10 instances, coercions and auxiliary constants left out.
lemma Usa1998P4.maskedCell_add line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Decidable, Usa1998P4.coloring, Nat, Eq, ZMod, OfNat.ofNat, Usa1998P4.maskedCell, Usa1998P4.addColoring, HAdd.hAdd
Proof uses: id, ite, Usa1998P4.cellValue, Not, Eq.mpr, congr, congrArg, ite_eq_right, of_eq_true, Eq.trans, True, add_zero, eq_self, ite_eq_left, congrFun', Usa1998P4.cellValue_add
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Usa1998P4.cornerDelta The sum of the values of the four cells touching a grid-line corner line 135 source
Source documentation
The sum of the values of the four cells touching a grid-line corner.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.coloring, Usa1998P4.Corner, ZMod, OfNat.ofNat, Nat
Proof uses: HAdd.hAdd, Usa1998P4.maskedCell, And, LT.lt, Prod.fst, Fin, Prod.snd, HSub.hSub
16 instances, coercions and auxiliary constants left out.
```
def cornerDelta (f : coloring) (c : Corner) : ZMod 2 :=
…
```
Mentions: f, Usa1998P4.coloring, Usa1998P4.Corner
lemma Usa1998P4.cornerDelta_add line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.coloring, Usa1998P4.Corner, Eq, ZMod, OfNat.ofNat, Nat, Usa1998P4.cornerDelta, Usa1998P4.addColoring, HAdd.hAdd
Proof uses: id, Eq.mpr, Usa1998P4.maskedCell, And, LT.lt, Prod.fst, Fin, Prod.snd, HSub.hSub, congrArg, Usa1998P4.maskedCell_add, congr, Eq.trans, congrFun', Usa1998P4.maskedCell.congr_simp, Lean.Data.AC.Context.eq_of_norm, Lean.Data.AC.Context.mk, Option.some, PLift, Std.Commutative and 13 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Usa1998P4.cornerSupport line 147 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.coloring, Finset, Usa1998P4.Corner
Proof uses: Finset.filter, Ne, ZMod, OfNat.ofNat, Nat, Usa1998P4.cornerDelta, Eq, Finset.univ, Fin
13 instances, coercions and auxiliary constants left out.
lemma Usa1998P4.mem_cornerSupport line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.coloring, Usa1998P4.Corner, Iff, Membership.mem, Finset, Usa1998P4.cornerSupport, Ne, ZMod, OfNat.ofNat, Nat, Usa1998P4.cornerDelta
Proof uses: of_eq_true, Not, Eq, Eq.trans, True, congrFun', congrArg, And, Finset.univ, Fin, Finset.filter, Finset.filter_congr, Iff.of_eq, Eq.refl, true_and, iff_self
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.ne_zero_or_ne_zero_of_add_ne_zero line 154 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Ne, HAdd.hAdd, Or
Proof uses: Mathlib.Tactic.Contrapose.contrapose₂, Eq, Eq.mpr, Not, And, id, implies_congr, Eq.trans, congr, congrArg, Eq.refl, of_eq_true, True, congrFun', And.left, And.right, add_zero, eq_self
32 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.cornerSupport_add_subset line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.coloring, LE.le, Finset, Usa1998P4.Corner, Usa1998P4.cornerSupport, Usa1998P4.addColoring, Union.union, Fin, OfNat.ofNat, Nat
Proof uses: Eq.mpr, Membership.mem, Ne, ZMod, Usa1998P4.cornerDelta, id, Eq, congrArg, propext, Usa1998P4.mem_cornerSupport, HAdd.hAdd, Usa1998P4.cornerDelta_add, Or, Finset.mem_union, Usa1998P4.ne_zero_or_ne_zero_of_add_ne_zero
24 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Usa1998P4.clip line 168 source
standard axioms: propext what this means
Statement uses: Nat, Fin, OfNat.ofNat
Proof uses: Fin.mk, Min.min
4 instances, coercions and auxiliary constants left out.
lemma Usa1998P4.maskedCell_rectColor line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Decidable, Usa1998P4.Rectangle, Nat, Eq, ZMod, OfNat.ofNat, Usa1998P4.maskedCell, Usa1998P4.rectColor, ite, And, LT.lt, LE.le, Usa1998P4.Rectangle.x, Usa1998P4.Rectangle.y, HAdd.hAdd, Usa1998P4.Rectangle.width, Usa1998P4.Rectangle.height
Proof uses: id, Usa1998P4.cellValue, dite, Prod.mk, Fin, Fin.mk, Not, Prod.fst, Prod.snd, Eq.mpr, congrFun', congrArg, ite_eq_left, dite_eq_left, Eq.refl, ite_eq_right, Or, Iff.mp, Decidable.not_and_iff_not_or_not', False.elim and 1 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.cornerDelta_rectColor_eq_zero_x line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.Rectangle, Usa1998P4.Corner, Ne, Nat, OfNat.ofNat, Prod.fst, Fin, Min.min, Usa1998P4.Rectangle.x, HAdd.hAdd, Usa1998P4.Rectangle.width, Eq, ZMod, Usa1998P4.cornerDelta, Usa1998P4.rectColor
Proof uses: Prod.mk, LT.lt, Fin.isLt, id, Usa1998P4.maskedCell, And, Prod.snd, HSub.hSub, Eq.mpr, ite, LE.le, Usa1998P4.Rectangle.y, Usa1998P4.Rectangle.height, congrArg, Usa1998P4.maskedCell_rectColor, Iff, Decidable.byContradiction, Not, if_congr, rfl and 5 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.cornerDelta_rectColor_eq_zero_y line 206 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.Rectangle, Usa1998P4.Corner, Ne, Nat, OfNat.ofNat, Prod.snd, Fin, Min.min, Usa1998P4.Rectangle.y, HAdd.hAdd, Usa1998P4.Rectangle.height, Eq, ZMod, Usa1998P4.cornerDelta, Usa1998P4.rectColor
Proof uses: Prod.mk, LT.lt, Fin.isLt, id, Usa1998P4.maskedCell, And, Prod.fst, HSub.hSub, Eq.mpr, ite, LE.le, Usa1998P4.Rectangle.x, Usa1998P4.Rectangle.width, congrArg, Usa1998P4.maskedCell_rectColor, Iff, Decidable.byContradiction, Not, if_congr, rfl and 5 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.cornerSupport_rectColor_card_le line 233 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.Rectangle, LE.le, Nat, Finset.card, Usa1998P4.Corner, Usa1998P4.cornerSupport, Usa1998P4.rectColor, OfNat.ofNat
Proof uses: Finset, SProd.sprod, Fin, Prod, Insert.insert, Usa1998P4.clip, Usa1998P4.Rectangle.x, Singleton.singleton, HAdd.hAdd, Usa1998P4.Rectangle.width, Usa1998P4.Rectangle.y, Usa1998P4.Rectangle.height, Eq.mpr, Membership.mem, Ne, ZMod, Usa1998P4.cornerDelta, id, Eq, congrArg and 29 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.cornerSupport_zero line 261 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Finset, Usa1998P4.Corner, Usa1998P4.cornerSupport, Usa1998P4.chessboard, OfNat.ofNat, ZMod, Nat, EmptyCollection.emptyCollection
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Ne, Usa1998P4.cornerDelta, id, congrArg, propext, Usa1998P4.mem_cornerSupport, of_eq_true, Eq.trans, False, True, congr, congrFun', HAdd.hAdd, Usa1998P4.maskedCell, And, LT.lt and 19 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.cornerSupport_listSum_card_le line 266 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Usa1998P4.Rectangle, LE.le, Nat, Finset.card, Usa1998P4.Corner, Usa1998P4.cornerSupport, Usa1998P4.chessboard, List.sum, ZMod, OfNat.ofNat, List.map, Usa1998P4.rectColor, HMul.hMul, List.length
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, Finset, EmptyCollection.emptyCollection, funext, List.map_nil, Usa1998P4.cornerSupport_zero, MulZeroClass.mul_zero, Eq, List.cons, Usa1998P4.addColoring, HAdd.hAdd, congrFun', List.map_cons, eq_self and 34 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def Usa1998P4.constAddStart line 289 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa1998P4.coloring
Proof uses: Usa1998P4.chessboard, HAdd.hAdd, Usa1998P4.start_coloring
10 instances, coercions and auxiliary constants left out.
lemma Usa1998P4.maskedCell_constAddStart line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Decidable, Eq, Usa1998P4.maskedCell, Usa1998P4.constAddStart, ite, And, LT.lt, HAdd.hAdd
Proof uses: id, Usa1998P4.cellValue, dite, Prod.mk, Fin, Fin.mk, Not, Eq.mpr, congrFun', congrArg, ite_eq_left, dite_eq_left, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm and 9 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Usa1998P4.inner line 300 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Fin, OfNat.ofNat, Nat
Proof uses: Finset.Icc, Fin.mk
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.inner_card line 302 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Fin, OfNat.ofNat, Usa1998P4.inner
Proof uses: Eq.mpr, Finset.Icc, Fin.mk, id, congrArg, Finset, Usa1998P4.inner.eq_1, HSub.hSub, HAdd.hAdd, Fin.card_Icc, 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 Usa1998P4.mem_inner line 306 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Iff, Membership.mem, Finset, Usa1998P4.inner, And, LT.lt
Proof uses: Eq.mpr, Finset.Icc, Fin.mk, id, Eq, congrArg, Usa1998P4.inner.eq_1, LE.le, propext, Finset.mem_Icc, Fin.le_def, Iff.intro
20 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Usa1998P4.quietCorners The two board corners where the corner delta of constAddStart c vanishes line 312 source
Source documentation
The two board corners where the corner delta of constAddStart c vanishes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Finset, Usa1998P4.Corner
Proof uses: ite, Eq, Insert.insert, Prod, Fin, Prod.mk, Fin.mk, Singleton.singleton
17 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def quietCorners (c : ZMod 2) : Finset Corner :=
…
```
Mentions: Usa1998P4.Corner
lemma Usa1998P4.quietCorners_card line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, LE.le, Finset.card, Usa1998P4.Corner, Usa1998P4.quietCorners
Proof uses: id, dite, ite, Finset, Eq, Insert.insert, Prod, Fin, Prod.mk, Fin.mk, Singleton.singleton, Eq.mpr, congrFun', congrArg, ite_eq_left, LE.le.trans, HAdd.hAdd, Finset.card_insert_le, le_of_eq, Finset.card_singleton and 3 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.quiet_subset line 321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, LE.le, Finset, Usa1998P4.Corner, Finset.filter, Not, Ne, Usa1998P4.cornerDelta, Usa1998P4.constAddStart, Eq, Finset.univ, Fin, Union.union, SProd.sprod, Prod, Usa1998P4.inner, Usa1998P4.quietCorners
Proof uses: Or, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, Membership.mem, And, congrArg, propext, Finset.mem_filter, Classical.not_not, Finset.mem_union, Prod.fst, Prod.snd, Finset.mem_product, LT.lt, Usa1998P4.mem_inner and 78 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 122 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.target_support_card line 420 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, LE.le, Finset.card, Usa1998P4.Corner, Usa1998P4.cornerSupport, Usa1998P4.constAddStart
Proof uses: Eq, HAdd.hAdd, Finset.filter, Ne, Usa1998P4.cornerDelta, Finset.univ, Fin, Not, Finset.card_filter_add_card_filter_not, Trans.trans, Prod, SProd.sprod, Finset, Usa1998P4.inner, Usa1998P4.quietCorners, Union.union, Finset.card_le_card, Usa1998P4.quiet_subset, Finset.card_union_le, Eq.mpr and 13 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
def Usa1998P4.colRect line 445 source
no axioms what this means
Statement uses: Nat, Usa1998P4.Rectangle
Proof uses: Usa1998P4.Rectangle.mk, HMul.hMul, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
def Usa1998P4.rowRect line 447 source
no axioms what this means
Statement uses: Nat, Usa1998P4.Rectangle
Proof uses: Usa1998P4.Rectangle.mk, OfNat.ofNat, HMul.hMul
3 instances, coercions and auxiliary constants left out.
lemma Usa1998P4.rectColor_colRect line 449 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Eq, ZMod, Usa1998P4.rectColor, Usa1998P4.colRect, Prod.mk, ite, HMul.hMul
Proof uses: LT.lt, Fin.isLt, id, And, LE.le, Usa1998P4.Rectangle.x, Prod.fst, Usa1998P4.Rectangle.y, Prod.snd, HAdd.hAdd, Usa1998P4.Rectangle.width, Usa1998P4.Rectangle.height, Usa1998P4.Rectangle.mk, if_congr, rfl
46 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.rectColor_rowRect line 456 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Eq, ZMod, Usa1998P4.rectColor, Usa1998P4.rowRect, Prod.mk, ite, HMul.hMul
Proof uses: LT.lt, Fin.isLt, id, And, LE.le, Usa1998P4.Rectangle.x, Prod.fst, Usa1998P4.Rectangle.y, Prod.snd, HAdd.hAdd, Usa1998P4.Rectangle.width, Usa1998P4.Rectangle.height, Usa1998P4.Rectangle.mk, if_congr, rfl
46 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.list_range_map_sum line 463 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, ZMod, OfNat.ofNat, Eq, List.sum, List.map, List.range, Finset.sum, Finset.range
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, List, List.nil, List.map_nil, eq_self, Eq.mpr, HAdd.hAdd, HAppend.hAppend, List.cons, id, Nat.succ, List.range_succ, List.map_append, List.sum_append, Finset.sum_range_succ and 2 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.sum_ite_eq_double line 471 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HMul.hMul, OfNat.ofNat, Eq, ZMod, Finset.sum, Finset.range, ite, Even
Proof uses: dite, HAdd.hAdd, Eq.mpr, id, congrArg, ite_eq_left, Exists.intro, Finset.sum_eq_single, Membership.mem, Finset, Ne, ite_eq_right, Eq.refl, Not, absurd, Iff.mpr, Finset.mem_range, Finset.sum_eq_zero
56 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.natCast_add_ite_even line 486 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, ZMod, OfNat.ofNat, HAdd.hAdd, ite, Even
Proof uses: dite, Eq.mpr, id, congrArg, ite_eq_left, Iff.mpr, ZMod.natCast_eq_zero_iff_even, zero_add, Eq.refl, Not, ite_eq_right, Odd, ZMod.natCast_eq_one_iff_odd, Iff.mp, Nat.not_even_iff_odd, add_zero
53 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa1998P4.construction_makes_zero line 492 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1998P4.chessboard, Eq, ZMod, OfNat.ofNat, Nat, List.foldl, Usa1998P4.coloring, Usa1998P4.Rectangle, Usa1998P4.recolor_rect, Usa1998P4.start_coloring, HAppend.hAppend, List, List.map, Usa1998P4.colRect, List.range, Usa1998P4.rowRect
Proof uses: Fin, LT.lt, Fin.isLt, Eq.mpr, Prod.mk, HAdd.hAdd, List.sum, Usa1998P4.rectColor, id, congrArg, Usa1998P4.foldl_recolor_apply, List.map_append, List.sum_append, Function.comp, List.map_map, ite, Even, HMul.hMul, congrFun', funext and 53 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
problem Usa1998P4.usa1998_p4 line 519 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Usa1998P4.possible_num_clicks, Usa1998P4.min_clicks
Proof uses: And.intro, Membership.mem, Set, lowerBounds, Exists.intro, List, Usa1998P4.Rectangle, And, Usa1998P4.all_same_color, List.foldl, Usa1998P4.coloring, Usa1998P4.recolor_rect, Usa1998P4.start_coloring, Eq, List.length, HAppend.hAppend, List.map, Usa1998P4.colRect, List.range, OfNat.ofNat and 77 more
57 instances, coercions and auxiliary constants left out.

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