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

52 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2000, Problem 3

A player starts with A blue cards, B red cards and C white cards. He scores points as he plays each card. If he plays a blue card, his score is the number of white cards remaining in his hand. If he plays a red card it is three times the number of blue cards remaining in his hand. If he plays a white card, it is twice the number of red cards remaining in his hand. What is the lowest possible score as a function of A, B and C and how many different ways can it be achieved?

Imports (7)

Imported by 1 file

Compfiles.lean

inductive Usa2000P3.Card The three colors of cards line 36 source
Source documentation
The three colors of cards.

no axioms what this means

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
inductive Card where
…
```
instance Usa2000P3.(instance at line 42) line 42 source
def Usa2000P3.score The score accumulated when playing the sequence of cards l, listed in the order they are played line 52 source
Source documentation
The score accumulated when playing the sequence of cards l, listed in the order they are played. When a blue card is played, the score gained is the number of white cards remaining; for a red card it is three times the number of blue cards remaining; for a white card it is twice the number of red cards remaining.

no axioms what this means
Statement uses: List, Usa2000P3.Card, Nat
2 instances, coercions and auxiliary constants left out.
```
def score : List Card → ℕ
  | [] => 0
  | .blue :: t => t.count .white + score t
  | .red :: t => 3 * t.count .blue + score t
  | .white :: t => 2 * t.count .red + score t

/-- The canonical play: all blue cards, then all red cards, then all white
cards. Every play with the same card counts is a permutation of this one. -/
```
Mentions: Usa2000P3.Card
def Usa2000P3.canonicalPlay The canonical play: all blue cards, then all red cards, then all white cards line 60 source
Source documentation
The canonical play: all blue cards, then all red cards, then all white cards. Every play with the same card counts is a permutation of this one.

no axioms what this means
Statement uses: Nat, List, Usa2000P3.Card
Proof uses: HAppend.hAppend, List.replicate, Usa2000P3.Card.blue, Usa2000P3.Card.red, Usa2000P3.Card.white
2 instances, coercions and auxiliary constants left out.
```
def canonicalPlay (A B C : ℕ) : List Card :=
…
```
Mentions: Usa2000P3.Card
def Usa2000P3.plays The finite set of all plays with A blue, B red and C white cards line 64 source
Source documentation
The finite set of all plays with A blue, B red and C white cards.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, List, Usa2000P3.Card
Proof uses: List.toFinset, List.permutations, Usa2000P3.canonicalPlay
2 instances, coercions and auxiliary constants left out.
```
def plays (A B C : ℕ) : Finset (List Card) :=
…
```
Mentions: Usa2000P3.Card
determine Usa2000P3.lowestScore line 67 source
no axioms what this means
Statement uses: Nat
Proof uses: Min.min, HMul.hMul, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
determine Usa2000P3.fewestWays The number of different ways the lowest score can be achieved line 70 source
Source documentation
The number of different ways the lowest score can be achieved.

no axioms what this means
Statement uses: Nat
Proof uses: ite, And, Eq, OfNat.ofNat, HMul.hMul, HAdd.hAdd, LT.lt
9 instances, coercions and auxiliary constants left out.
```
determine fewestWays (A B C : ℕ) : ℕ :=
…
```
lemma Usa2000P3.score_nil line 80 source
no axioms what this means
Statement uses: Eq, Nat, Usa2000P3.score, List.nil, Usa2000P3.Card, OfNat.ofNat
Proof uses: rfl
1 instances, coercions and auxiliary constants left out.
lemma Usa2000P3.score_cons_blue line 81 source
no axioms what this means
Statement uses: List, Usa2000P3.Card, Eq, Nat, Usa2000P3.score, List.cons, Usa2000P3.Card.blue, HAdd.hAdd, List.count, Usa2000P3.Card.white
Proof uses: rfl
3 instances, coercions and auxiliary constants left out.
lemma Usa2000P3.score_cons_red line 83 source
no axioms what this means
Statement uses: List, Usa2000P3.Card, Eq, Nat, Usa2000P3.score, List.cons, Usa2000P3.Card.red, HAdd.hAdd, HMul.hMul, OfNat.ofNat, List.count, Usa2000P3.Card.blue
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma Usa2000P3.score_cons_white line 85 source
no axioms what this means
Statement uses: List, Usa2000P3.Card, Eq, Nat, Usa2000P3.score, List.cons, Usa2000P3.Card.white, HAdd.hAdd, HMul.hMul, OfNat.ofNat, List.count, Usa2000P3.Card.red
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma Usa2000P3.mem_plays line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Usa2000P3.Card, Iff, Membership.mem, Finset, Usa2000P3.plays, And, Eq, List.count, Usa2000P3.Card.blue, Usa2000P3.Card.red, Usa2000P3.Card.white
Proof uses: Eq.mpr, List.toFinset, List.permutations, Usa2000P3.canonicalPlay, id, congrArg, Usa2000P3.plays.eq_1, propext, List.mem_toFinset, List.Perm, List.mem_permutations, List.perm_iff_count, Iff.intro, And.intro, Eq.mp, Eq.trans, HAppend.hAppend, List.replicate, HAdd.hAdd, List.count_append and 19 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.lowestScore_cases line 107 source
standard axioms: propext what this means
Statement uses: Nat, Or, Eq, Usa2000P3.lowestScore, HMul.hMul, OfNat.ofNat
Proof uses: id, LE.le, Min.min, le_total, Eq.mpr, congrArg, min_eq_left, Or.inl, Or.inr, min_eq_right
13 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.lowestScore_le_ac line 125 source
standard axioms: propext what this means
Statement uses: Nat, LE.le, Usa2000P3.lowestScore, HMul.hMul
Proof uses: le_trans, Min.min, OfNat.ofNat, min_le_left
9 instances, coercions and auxiliary constants left out.
lemma Usa2000P3.lowestScore_le_ab line 128 source
standard axioms: propext what this means
Statement uses: Nat, LE.le, Usa2000P3.lowestScore, HMul.hMul, OfNat.ofNat
Proof uses: le_trans, Min.min, min_le_left, min_le_right
10 instances, coercions and auxiliary constants left out.
lemma Usa2000P3.lowestScore_le_bc line 131 source
standard axioms: propext what this means
Statement uses: Nat, LE.le, Usa2000P3.lowestScore, HMul.hMul, OfNat.ofNat
Proof uses: min_le_right, Min.min
9 instances, coercions and auxiliary constants left out.
lemma Usa2000P3.lowestScore_eq_ac line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Not, And, LE.le, HMul.hMul, Ne, Usa2000P3.lowestScore
Proof uses: Eq.mpr, id, Eq, Eq.trans, Min.min, congrFun', congrArg, Nat.min_assoc, propext, mul_le_mul_iff_left₀, of_eq_true, True, congr, mul_comm, mul_left_comm, eq_self
40 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.lowestScore_zero_b_c line 140 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Usa2000P3.lowestScore, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Min.min, HMul.hMul, congr, MulZeroClass.zero_mul, MulZeroClass.mul_zero, min_self, inf_of_le_left, LE.le, eq_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.lowestScore_a_zero_c line 142 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Usa2000P3.lowestScore, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Min.min, HMul.hMul, congr, MulZeroClass.mul_zero, inf_of_le_right, LE.le, MulZeroClass.zero_mul, min_self, eq_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.lowestScore_a_b_zero line 144 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Usa2000P3.lowestScore, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Min.min, HMul.hMul, congr, MulZeroClass.mul_zero, inf_of_le_left, LE.le, min_self, eq_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.lowestScore_le_add_blue line 146 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Usa2000P3.lowestScore, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq, HMul.hMul, Or, Usa2000P3.lowestScore_cases, Trans.trans, le_trans, Min.min, min_le_left, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl and 64 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.lowestScore_le_add_red line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Usa2000P3.lowestScore, HAdd.hAdd, OfNat.ofNat, HMul.hMul
Proof uses: Eq, Or, Usa2000P3.lowestScore_cases, Trans.trans, le_trans, Min.min, min_le_left, Eq.mpr, id, congrArg, Eq.refl, min_le_right, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 66 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.lowestScore_le_add_white line 206 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Usa2000P3.lowestScore, HAdd.hAdd, OfNat.ofNat, HMul.hMul
Proof uses: Eq, Or, Usa2000P3.lowestScore_cases, Eq.mpr, id, congrArg, Eq.symm, Usa2000P3.lowestScore_le_bc, dite, Trans.trans, le_trans, Min.min, min_le_left, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.refl and 65 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.tight_blue line 236 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Eq, HAdd.hAdd, Usa2000P3.lowestScore, OfNat.ofNat, HMul.hMul
Proof uses: Iff.intro, dite, Usa2000P3.lowestScore_a_b_zero, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.mul_congr, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.cast_pos, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero and 72 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 70 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.tight_red line 285 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Usa2000P3.lowestScore
Proof uses: Iff.intro, dite, Usa2000P3.lowestScore_zero_b_c, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.mul_congr, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.cast_pos, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_zero, Mathlib.Tactic.Ring.Common.zero_mul, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf and 81 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 83 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.tight_white line 342 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Usa2000P3.lowestScore
Proof uses: Iff.intro, dite, Usa2000P3.lowestScore_a_zero_c, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.mul_congr, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.cast_pos, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_zero, Mathlib.Tactic.Ring.Common.zero_mul, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf and 78 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 81 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.fewestWays_zero_b_c line 401 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2000P3.fewestWays, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.fewestWays_a_zero_c line 403 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2000P3.fewestWays, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.fewestWays_a_b_zero line 405 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2000P3.fewestWays, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.fewestWays_rec line 408 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, HAdd.hAdd, Eq, Usa2000P3.fewestWays, ite, And, Usa2000P3.lowestScore, HMul.hMul, HSub.hSub
Proof uses: dite, Eq.symm, Not, le_antisymm, Usa2000P3.lowestScore_le_ab, LE.le, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 114 more
196 instances, coercions and auxiliary constants left out.

Tactic trace: 385 steps (first 200 of 385)
Open to load the checked before-and-after goal states.
lemma Usa2000P3.score_ge line 663 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Usa2000P3.Card, LE.le, Nat, Usa2000P3.lowestScore, List.count, Usa2000P3.Card.blue, Usa2000P3.Card.red, Usa2000P3.Card.white, Usa2000P3.score
Proof uses: List.rec, Nat.zero_le, List.nil, Eq, List.cons, Eq.mpr, HAdd.hAdd, OfNat.ofNat, id, congrFun', congrArg, congr, List.count_cons_self, List.count_cons_of_ne, of_decide_eq_true, Ne, Bool, Decidable.decide, Bool.true, Eq.refl and 7 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.score_replicate_blue_append line 685 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, List, Usa2000P3.Card, Eq, Usa2000P3.score, HAppend.hAppend, List.replicate, Usa2000P3.Card.blue, HAdd.hAdd, HMul.hMul, List.count, Usa2000P3.Card.white
Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congrArg, congrFun', MulZeroClass.zero_mul, zero_add, eq_self, Eq.mpr, List.cons, id, List.replicate_succ, List.cons_append, Usa2000P3.score_cons_blue, List.count_append, ite, Bool, BEq.beq and 32 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.score_replicate_red_append line 694 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, List, Usa2000P3.Card, Eq, Usa2000P3.score, HAppend.hAppend, List.replicate, Usa2000P3.Card.red, HAdd.hAdd, HMul.hMul, OfNat.ofNat, List.count, Usa2000P3.Card.blue
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, congrFun', MulZeroClass.mul_zero, MulZeroClass.zero_mul, zero_add, eq_self, Eq.mpr, List.cons, id, List.replicate_succ, List.cons_append, Usa2000P3.score_cons_red, List.count_append, ite, Bool, BEq.beq and 32 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.score_replicate_white_append line 703 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, List, Usa2000P3.Card, Eq, Usa2000P3.score, HAppend.hAppend, List.replicate, Usa2000P3.Card.white, HAdd.hAdd, HMul.hMul, OfNat.ofNat, List.count, Usa2000P3.Card.red
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, congrFun', MulZeroClass.mul_zero, MulZeroClass.zero_mul, zero_add, eq_self, Eq.mpr, List.cons, id, List.replicate_succ, List.cons_append, Usa2000P3.score_cons_white, List.count_append, ite, Bool, BEq.beq and 32 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.score_replicate_blue line 712 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2000P3.score, List.replicate, Usa2000P3.Card, Usa2000P3.Card.blue, OfNat.ofNat
Proof uses: HAppend.hAppend, List, List.nil, HAdd.hAdd, HMul.hMul, List.count, Usa2000P3.Card.white, Usa2000P3.score_replicate_blue_append, Eq.mp, congr, congrArg, List.append_nil, Eq.trans, congrFun', MulZeroClass.mul_zero, add_zero
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.score_replicate_red line 717 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2000P3.score, List.replicate, Usa2000P3.Card, Usa2000P3.Card.red, OfNat.ofNat
Proof uses: HAppend.hAppend, List, List.nil, HAdd.hAdd, HMul.hMul, List.count, Usa2000P3.Card.blue, Usa2000P3.score_replicate_red_append, Eq.mp, congr, congrArg, List.append_nil, Eq.trans, congrFun', MulZeroClass.mul_zero, add_zero
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.score_replicate_white line 722 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2000P3.score, List.replicate, Usa2000P3.Card, Usa2000P3.Card.white, OfNat.ofNat
Proof uses: HAppend.hAppend, List, List.nil, HAdd.hAdd, HMul.hMul, List.count, Usa2000P3.Card.red, Usa2000P3.score_replicate_white_append, Eq.mp, congr, congrArg, List.append_nil, Eq.trans, congrFun', MulZeroClass.mul_zero, add_zero
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.score_canonicalPlay line 727 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2000P3.score, Usa2000P3.canonicalPlay, HMul.hMul
Proof uses: Eq.mpr, HAppend.hAppend, List, Usa2000P3.Card, List.replicate, Usa2000P3.Card.blue, Usa2000P3.Card.red, Usa2000P3.Card.white, id, congrArg, Usa2000P3.canonicalPlay.eq_1, HAdd.hAdd, List.count, Usa2000P3.score_replicate_blue_append, List.count_append, OfNat.ofNat, Usa2000P3.score_replicate_red_append, Usa2000P3.score_replicate_white, of_eq_true, Eq.trans and 19 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.score_rwb line 732 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2000P3.score, HAppend.hAppend, List, Usa2000P3.Card, List.replicate, Usa2000P3.Card.red, Usa2000P3.Card.white, Usa2000P3.Card.blue, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, HAdd.hAdd, List.count, id, congrArg, Usa2000P3.score_replicate_red_append, List.count_append, Usa2000P3.score_replicate_white_append, Usa2000P3.score_replicate_blue, congrFun', Eq.trans, congr, ite, Bool, BEq.beq, Bool.true, List.count_replicate, ite_eq_right_of_eq_false, False, eq_false' and 27 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.score_wbr line 740 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2000P3.score, HAppend.hAppend, List, Usa2000P3.Card, List.replicate, Usa2000P3.Card.white, Usa2000P3.Card.blue, Usa2000P3.Card.red, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, HAdd.hAdd, List.count, id, congrArg, Usa2000P3.score_replicate_white_append, List.count_append, Usa2000P3.score_replicate_blue_append, Usa2000P3.score_replicate_red, congrFun', Eq.trans, congr, ite, Bool, BEq.beq, Bool.true, List.count_replicate, ite_eq_right_of_eq_false, False, eq_false' and 27 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Usa2000P3.optPlays The set of plays that achieve the lowest score line 751 source
Source documentation
The set of plays that achieve the lowest score.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, List, Usa2000P3.Card
Proof uses: Finset.filter, Eq, Usa2000P3.score, Usa2000P3.lowestScore, Usa2000P3.plays
1 instances, coercions and auxiliary constants left out.
```
def optPlays (A B C : ℕ) : Finset (List Card) :=
…
```
Mentions: Usa2000P3.Card
lemma Usa2000P3.card_optPlays_head_blue line 754 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, List, Usa2000P3.Card, Finset.filter, Option, List.head?, Option.some, Usa2000P3.Card.blue, Usa2000P3.optPlays, ite, And, LT.lt, OfNat.ofNat, Usa2000P3.lowestScore, HMul.hMul, HSub.hSub
Proof uses: dite, Finset, EmptyCollection.emptyCollection, Eq.mpr, Not, Membership.mem, id, congrArg, propext, Finset.eq_empty_iff_forall_notMem, List.cons, Exists, False, Iff.mp, List.head?_eq_some_iff, And.right, Usa2000P3.plays, Usa2000P3.score, Eq.mp, Finset.mem_filter and 42 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 82 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.card_optPlays_head_red line 823 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, List, Usa2000P3.Card, Finset.filter, Option, List.head?, Option.some, Usa2000P3.Card.red, Usa2000P3.optPlays, ite, And, LT.lt, OfNat.ofNat, Usa2000P3.lowestScore, HMul.hMul, HSub.hSub
Proof uses: dite, Finset, EmptyCollection.emptyCollection, Eq.mpr, Not, Membership.mem, id, congrArg, propext, Finset.eq_empty_iff_forall_notMem, List.cons, Exists, False, Iff.mp, List.head?_eq_some_iff, And.right, Usa2000P3.plays, Usa2000P3.score, Eq.mp, Finset.mem_filter and 42 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 82 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.card_optPlays_head_white line 892 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, List, Usa2000P3.Card, Finset.filter, Option, List.head?, Option.some, Usa2000P3.Card.white, Usa2000P3.optPlays, ite, And, LT.lt, OfNat.ofNat, Usa2000P3.lowestScore, HMul.hMul, HSub.hSub
Proof uses: dite, Finset, EmptyCollection.emptyCollection, Eq.mpr, Not, Membership.mem, id, congrArg, propext, Finset.eq_empty_iff_forall_notMem, List.cons, Exists, False, Iff.mp, List.head?_eq_some_iff, And.right, Usa2000P3.plays, Usa2000P3.score, Eq.mp, Finset.mem_filter and 42 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 82 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.optPlays_card_rec line 961 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, HAdd.hAdd, Eq, Finset.card, List, Usa2000P3.Card, Usa2000P3.optPlays, ite, And, Usa2000P3.lowestScore, HMul.hMul, HSub.hSub
Proof uses: Membership.mem, Finset, Ne, List.nil, List.count, Usa2000P3.Card.blue, Usa2000P3.Card.red, Usa2000P3.Card.white, False, Iff.mp, Usa2000P3.plays, Usa2000P3.mem_plays, And.left, Usa2000P3.score, Eq.mp, Finset.filter, congrArg, propext, Finset.mem_filter, Usa2000P3.optPlays.eq_1 and 33 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.optPlays_zero line 1020 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, List, Usa2000P3.Card, Usa2000P3.optPlays, OfNat.ofNat
Proof uses: Finset, Singleton.singleton, List.nil, Finset.ext, Eq.mpr, Iff, Membership.mem, Finset.filter, Usa2000P3.score, Usa2000P3.lowestScore, Usa2000P3.plays, id, congrArg, Usa2000P3.optPlays.eq_1, And, propext, Finset.mem_filter, Finset.mem_singleton, Iff.intro, List.count and 18 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.optPlays_card line 1043 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, List, Usa2000P3.Card, Usa2000P3.optPlays, Usa2000P3.fewestWays
Proof uses: LT.lt, HAdd.hAdd, Nat.recAux, OfNat.ofNat, dite, And, Eq.mpr, id, congrArg, Usa2000P3.optPlays_zero, of_eq_true, Eq.trans, True, ite_eq_left_of_eq_true, ite, HMul.hMul, congr, eq_self, and_self, Eq.symm and 10 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.canonicalPlay_mem_plays line 1083 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, List, Usa2000P3.Card, Finset, Usa2000P3.plays, Usa2000P3.canonicalPlay
Proof uses: Iff.mpr, And, Eq, List.count, Usa2000P3.Card.blue, Usa2000P3.Card.red, Usa2000P3.Card.white, Usa2000P3.mem_plays, And.intro, of_eq_true, Eq.trans, True, congrFun', congrArg, HAppend.hAppend, List.replicate, HAdd.hAdd, List.count_append, OfNat.ofNat, congr and 15 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.mem_plays_rwb line 1088 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, List, Usa2000P3.Card, Finset, Usa2000P3.plays, HAppend.hAppend, List.replicate, Usa2000P3.Card.red, Usa2000P3.Card.white, Usa2000P3.Card.blue
Proof uses: Iff.mpr, And, Eq, List.count, Usa2000P3.mem_plays, And.intro, of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, List.count_append, OfNat.ofNat, congr, ite, Bool, BEq.beq, Bool.true, List.count_replicate and 10 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.mem_plays_wbr line 1094 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, List, Usa2000P3.Card, Finset, Usa2000P3.plays, HAppend.hAppend, List.replicate, Usa2000P3.Card.white, Usa2000P3.Card.blue, Usa2000P3.Card.red
Proof uses: Iff.mpr, And, Eq, List.count, Usa2000P3.mem_plays, And.intro, of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, List.count_append, OfNat.ofNat, congr, ite, Bool, BEq.beq, Bool.true, List.count_replicate and 10 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P3.isLeast_lowestScore line 1100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, IsLeast, Set.ofPred, Exists, List, Usa2000P3.Card, And, Membership.mem, Finset, Usa2000P3.plays, Eq, Usa2000P3.score, Usa2000P3.lowestScore
Proof uses: And.intro, Set, lowerBounds, HMul.hMul, Or, OfNat.ofNat, Usa2000P3.lowestScore_cases, Exists.intro, Usa2000P3.canonicalPlay, Usa2000P3.canonicalPlay_mem_plays, Eq.mpr, id, congrArg, Usa2000P3.score_canonicalPlay, Eq.symm, HAppend.hAppend, List.replicate, Usa2000P3.Card.red, Usa2000P3.Card.white, Usa2000P3.Card.blue and 9 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
problem Usa2000P3.usa2000_p3 line 1118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, IsLeast, Set.ofPred, Exists, List, Usa2000P3.Card, Membership.mem, Finset, Usa2000P3.plays, Eq, Usa2000P3.score, Usa2000P3.lowestScore, Finset.card, Finset.filter, Usa2000P3.fewestWays
Proof uses: And.intro, Usa2000P3.isLeast_lowestScore, Usa2000P3.optPlays_card
8 instances, coercions and auxiliary constants left out.

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