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

40 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2015, Problem 3

Let S = {1, 2, ..., n}, where n ≥ 1. Each of the 2ⁿ subsets of S is to be colored red or blue. (The subset itself is assigned a color and not its individual elements.) For any set T ⊆ S, we then write f(T) for the number of subsets of T that are blue. Determine the number of colorings that satisfy the following condition: for any subsets T₁ and T₂ of S,

f(T₁) f(T₂) = f(T₁ ∪ T₂) f(T₁ ∩ T₂).

Imports (5)

Imported by 1 file

Compfiles.lean

abbrev Usa2015P3.Coloring A coloring of the subsets of Fin n; true means blue, false means red line 33 source
Source documentation
A coloring of the subsets of Fin n; true means blue, false means red.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset, Fin, Bool
```
abbrev Coloring (n : ℕ) : Type := Finset (Fin n) → Bool
```
def Usa2015P3.blueCard blueCard c T is the number of subsets of T that are colored blue by c; this is the function f of the problem statement line 37 source
Source documentation
blueCard c T is the number of subsets of T that are colored blue by c; this is the function f of the problem statement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Finset, Fin
Proof uses: Finset.card, Finset.filter, Eq, Bool, Bool.true, Finset.powerset
1 instances, coercions and auxiliary constants left out.
```
def blueCard {n : ℕ} (c : Coloring n) (T : Finset (Fin n)) : ℕ :=
…
```
Mentions: Usa2015P3.Coloring
def Usa2015P3.IsValid A coloring is valid if it satisfies the multiplicative condition of the problem line 41 source
Source documentation
A coloring is valid if it satisfies the multiplicative condition of the problem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring
Proof uses: Finset, Fin, Eq, HMul.hMul, Usa2015P3.blueCard, Union.union, Inter.inter
5 instances, coercions and auxiliary constants left out.
```
def IsValid {n : ℕ} (c : Coloring n) : Prop :=
…
```
Mentions: Usa2015P3.Coloring
def Usa2015P3.ValidColorings The colorings that the problem asks to count line 46 source
Source documentation
The colorings that the problem asks to count.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Subtype, Usa2015P3.Coloring, Usa2015P3.IsValid
```
def ValidColorings (n : ℕ) : Type := {c : Coloring n // IsValid c}
```
Mentions: Usa2015P3.Coloring, Usa2015P3.IsValid
instance Usa2015P3.(instance at line 48) line 48 source
instance Usa2015P3.(instance at line 50) line 50 source
def Usa2015P3.X The intersection of all blue sets of a coloring line 56 source
Source documentation
The intersection of all blue sets of a coloring. We show that for a nontrivial valid coloring the blue sets are exactly the sets T with X c ⊆ T ⊆ X c ∪ B c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Finset, Fin
Proof uses: Finset.filter, Eq, Bool, Bool.true, Membership.mem, Finset.univ
9 instances, coercions and auxiliary constants left out.
```
def X {n : ℕ} (c : Coloring n) : Finset (Fin n) :=
…
```
Mentions: Usa2015P3.Coloring
def Usa2015P3.B The elements i outside X c such that X c ∪ {i} is blue line 60 source
Source documentation
The elements i outside X c such that X c ∪ {i} is blue.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Finset, Fin
Proof uses: Finset.filter, And, Not, Membership.mem, Usa2015P3.X, Eq, Bool, Union.union, Singleton.singleton, Bool.true, Finset.univ
10 instances, coercions and auxiliary constants left out.
```
def B {n : ℕ} (c : Coloring n) : Finset (Fin n) :=
…
```
Mentions: Usa2015P3.Coloring
lemma Usa2015P3.mem_X line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Fin, Iff, Membership.mem, Finset, Usa2015P3.X, Eq, Bool, Bool.true
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.filter, Finset.univ, And, true_and, iff_self
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2015P3.mem_B line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Fin, Iff, Membership.mem, Finset, Usa2015P3.B, And, Not, Usa2015P3.X, Eq, Bool, Union.union, Singleton.singleton, Bool.true
Proof uses: of_eq_true, Eq.trans, Insert.insert, True, congr, congrArg, Finset.univ, Finset.filter, congrFun', Finset.filter_congr, Iff.of_eq, Finset.union_singleton, true_and, iff_self
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2015P3.blueCard_ne_zero_iff line 71 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Finset, Fin, Iff, Ne, Usa2015P3.blueCard, OfNat.ofNat, Exists, And, LE.le, Eq, Bool, Bool.true
Proof uses: Eq.mpr, Finset.card, Finset.filter, Finset.powerset, id, congrArg, Usa2015P3.blueCard.eq_1, LT.lt, Eq.symm, propext, pos_iff_ne_zero, Finset.Nonempty, Finset.card_pos, Membership.mem, Finset.filter_nonempty_iff, of_eq_true, Eq.trans, True, congrFun', funext and 1 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2015P3.blueCard_ne_zero_of_mem line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Finset, Fin, Eq, Bool, Bool.true, Ne, Usa2015P3.blueCard, OfNat.ofNat
Proof uses: Iff.mpr, Exists, And, LE.le, Usa2015P3.blueCard_ne_zero_iff, Exists.intro, And.intro, Finset.Subset.refl
5 instances, coercions and auxiliary constants left out.
lemma Usa2015P3.blueCard_ne_zero_inter If two sets contain a blue subset each, so does their intersection line 87 source
Source documentation
If two sets contain a blue subset each, so does their intersection.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Usa2015P3.IsValid, Finset, Fin, Ne, Usa2015P3.blueCard, OfNat.ofNat, Inter.inter
Proof uses: Eq, HMul.hMul, Union.union, mul_ne_zero, Eq.mp, congrArg, MulZeroClass.mul_zero
22 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma blueCard_ne_zero_inter {T₁ T₂ : Finset (Fin n)}
    (h₁ : blueCard c T₁ ≠ 0) (h₂ : blueCard c T₂ ≠ 0) : blueCard c (T₁ ∩ T₂) ≠ 0 := by
…
```
Mentions: Usa2015P3.blueCard
lemma Usa2015P3.blueCard_ne_zero_inter_all The intersection of a nonempty family of sets each containing a blue subset itself contains a blue subset line 96 source
Source documentation
The intersection of a nonempty family of sets each containing a blue subset itself contains a blue subset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Usa2015P3.IsValid, Finset, Fin, Finset.Nonempty, Membership.mem, Ne, Usa2015P3.blueCard, OfNat.ofNat, Finset.filter, Finset.univ
Proof uses: Finset.Nonempty.cons_induction, Singleton.singleton, Eq, Finset.ext, of_eq_true, Iff, Eq.trans, True, congrFun', congrArg, Finset.filter_congr, Iff.of_eq, forall_congr, implies_congr, Eq.refl, Finset.filter_mem_eq_of_subset, LE.le, iff_self, Eq.mpr, id and 15 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma blueCard_ne_zero_inter_all (F : Finset (Finset (Fin n))) :
    F.Nonempty → (∀ T ∈ F, blueCard c T ≠ 0) →
    blueCard c (Finset.univ.filter fun i => ∀ T ∈ F, i ∈ T) ≠ 0 := by
…
```
Mentions: Usa2015P3.blueCard
lemma Usa2015P3.blueCard_ne_zero_X The intersection X c of all blue sets contains a blue subset line 123 source
Source documentation
The intersection X c of all blue sets contains a blue subset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Usa2015P3.IsValid, Exists, Finset, Fin, Eq, Bool, Bool.true, Ne, Usa2015P3.blueCard, Usa2015P3.X, OfNat.ofNat
Proof uses: Finset.filter, Membership.mem, Finset.univ, Finset.ext, of_eq_true, Iff, Eq.trans, True, congr, congrArg, And, congrFun', true_and, Finset.filter_congr, Iff.of_eq, forall_congr, implies_congr, Eq.refl, iff_self, Eq.mpr and 10 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma blueCard_ne_zero_X (hne : ∃ T, c T = true) : blueCard c (X c) ≠ 0 := by
…
```
Mentions: Usa2015P3.blueCard, Usa2015P3.X
lemma Usa2015P3.X_blue The intersection X c of all blue sets is itself blue line 136 source
Source documentation
The intersection X c of all blue sets is itself blue.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Usa2015P3.IsValid, Exists, Finset, Fin, Eq, Bool, Bool.true, Usa2015P3.X
Proof uses: And, LE.le, Iff.mp, Ne, Usa2015P3.blueCard, OfNat.ofNat, Usa2015P3.blueCard_ne_zero_iff, Usa2015P3.blueCard_ne_zero_X, Membership.mem, Usa2015P3.mem_X, Finset.Subset.antisymm, Eq.mp, congrArg
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma X_blue (hne : ∃ T, c T = true) : c (X c) = true := by
…
```
Mentions: Usa2015P3.X
lemma Usa2015P3.blueCard_X X c is the only blue subset of itself line 143 source
Source documentation
X c is the only blue subset of itself.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Usa2015P3.IsValid, Exists, Finset, Fin, Eq, Bool, Bool.true, Usa2015P3.blueCard, Usa2015P3.X, OfNat.ofNat
Proof uses: Finset.filter, Finset.powerset, Singleton.singleton, Finset.ext, Eq.mpr, Iff, Membership.mem, And, LE.le, id, congr, congrArg, Eq.trans, congrFun', Iff.intro, Finset.Subset.antisymm, Iff.mp, Usa2015P3.mem_X, And.intro, Finset.Subset.refl and 5 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma blueCard_X (hne : ∃ T, c T = true) : blueCard c (X c) = 1 := by
…
```
Mentions: Usa2015P3.blueCard, Usa2015P3.X
lemma Usa2015P3.blueCard_union Multiplicativity of blueCard over pairs of sets whose intersection is X c line 156 source
Source documentation
Multiplicativity of blueCard over pairs of sets whose intersection is X c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Usa2015P3.IsValid, Finset, Fin, LE.le, Usa2015P3.X, Inter.inter, Exists, Eq, Bool, Bool.true, Usa2015P3.blueCard, Union.union, HMul.hMul
Proof uses: Finset.Subset.antisymm, Finset.subset_inter, Eq.symm, Eq.mp, OfNat.ofNat, congrArg, mul_one, Usa2015P3.blueCard_X
22 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma blueCard_union {T₁ T₂ : Finset (Fin n)} (h1 : X c ⊆ T₁) (h2 : X c ⊆ T₂)
    (h3 : T₁ ∩ T₂ ⊆ X c) (hne : ∃ T, c T = true) :
    blueCard c (T₁ ∪ T₂) = blueCard c T₁ * blueCard c T₂ := by
…
```
Mentions: Usa2015P3.X, Usa2015P3.blueCard
lemma Usa2015P3.blueCard_singleton X c ∪ {i} has one blue subset if it is red (X c itself) and two if it is blue line 165 source
Source documentation
X c ∪ {i} has one blue subset if it is red (X c itself) and two if it is blue.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Usa2015P3.IsValid, Fin, Not, Membership.mem, Finset, Usa2015P3.X, Exists, Eq, Bool, Bool.true, Usa2015P3.blueCard, Union.union, Singleton.singleton, ite, OfNat.ofNat
Proof uses: LE.le, Or, Iff.mp, Usa2015P3.mem_X, SDiff.sdiff, And, Finset.mem_sdiff, Eq.mp, Eq.trans, congrArg, absurd, Iff.mpr, Finset.mem_singleton, EmptyCollection.emptyCollection, Finset.subset_singleton_iff, Or.inl, Finset.Subset.antisymm, propext, Finset.sdiff_eq_empty_iff_subset, Or.inr and 27 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
```
lemma blueCard_singleton (i : Fin n) (hi : i ∉ X c) (hne : ∃ T, c T = true) :
    blueCard c (X c ∪ {i}) = if c (X c ∪ {i}) then 2 else 1 := by
…
```
Mentions: Usa2015P3.X, Usa2015P3.blueCard
lemma Usa2015P3.blueCard_prod blueCard is multiplicative over the elements of a set disjoint from X c line 220 source
Source documentation
blueCard is multiplicative over the elements of a set disjoint from X c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Usa2015P3.IsValid, Finset, Fin, Exists, Eq, Bool, Bool.true, Disjoint, Usa2015P3.X, Usa2015P3.blueCard, Union.union, Finset.prod, Singleton.singleton
Proof uses: Finset.induction, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, OfNat.ofNat, True, congr, congrArg, Finset.union_empty, Usa2015P3.blueCard_X, Finset.prod_congr, Insert.insert, Eq.refl, Membership.mem, Finset.union_singleton, eq_self, Not, Disjoint.mono_right, Finset.subset_insert, Iff.mp and 23 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma blueCard_prod (U : Finset (Fin n)) (hne : ∃ T, c T = true) :
    Disjoint (X c) U → blueCard c (X c ∪ U) = ∏ i ∈ U, blueCard c (X c ∪ {i}) := by
…
```
Mentions: Usa2015P3.X, Usa2015P3.blueCard
lemma Usa2015P3.blueCard_pow For U disjoint from X c, the number of blue subsets of X c ∪ U is a power of two determined by which of the X c ∪ {i} are blue line 250 source
Source documentation
For U disjoint from X c, the number of blue subsets of X c ∪ U is a power of two determined by which of the X c ∪ {i} are blue.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Usa2015P3.IsValid, Finset, Fin, Disjoint, Usa2015P3.X, Exists, Eq, Bool, Bool.true, Usa2015P3.blueCard, Union.union, HPow.hPow, OfNat.ofNat, Finset.card, Finset.filter, Singleton.singleton
Proof uses: Membership.mem, ite, Usa2015P3.blueCard_singleton, Iff.mp, Not, Finset.disjoint_right, Eq.mpr, Finset.prod, id, congrArg, Usa2015P3.blueCard_prod, Finset.prod_congr, rfl, HMul.hMul, Finset.prod_ite, of_eq_true, Eq.trans, Insert.insert, True, congr and 11 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma blueCard_pow (U : Finset (Fin n)) (hU : Disjoint (X c) U) (hne : ∃ T, c T = true) :
    blueCard c (X c ∪ U) = 2 ^ (U.filter fun i => c (X c ∪ {i})).card := by
…
```
Mentions: Usa2015P3.X, Usa2015P3.blueCard
lemma Usa2015P3.blue_of_mem_interval Every set in the interval [X c, X c ∪ B c] is blue line 259 source
Source documentation
Every set in the interval [X c, X c ∪ B c] is blue.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Usa2015P3.IsValid, Exists, Finset, Fin, Eq, Bool, Bool.true, LE.le, Usa2015P3.X, Union.union, Usa2015P3.B
Proof uses: SDiff.sdiff, Eq.symm, Finset.union_sdiff_of_subset, Membership.mem, Not, And, Iff.mp, Finset.mem_sdiff, Eq.mpr, Singleton.singleton, id, congrArg, propext, Usa2015P3.mem_B, And.intro, Or, Eq.mp, absurd, And.right, Finset.filter and 28 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
```
lemma blue_of_mem_interval (hne : ∃ T, c T = true) {T : Finset (Fin n)}
    (hXT : X c ⊆ T) (hTB : T ⊆ X c ∪ B c) : c T = true := by
…
```
Mentions: Usa2015P3.X, Usa2015P3.B
lemma Usa2015P3.interval_of_blue Every blue set lies in the interval [X c, X c ∪ B c] line 313 source
Source documentation
Every blue set lies in the interval [X c, X c ∪ B c].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Usa2015P3.IsValid, Exists, Finset, Fin, Eq, Bool, Bool.true, And, LE.le, Usa2015P3.X, Union.union, Usa2015P3.B
Proof uses: Membership.mem, Iff.mp, Usa2015P3.mem_X, And.intro, Decidable.byContradiction, Not, Iff.mpr, Or, Finset.mem_union, Or.inl, Or.inr, Singleton.singleton, Bool.false, Usa2015P3.mem_B, Bool.eq_true_of_not_eq_false, SDiff.sdiff, Eq.symm, Finset.union_sdiff_of_subset, Usa2015P3.blueCard, HPow.hPow and 42 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
lemma interval_of_blue (hne : ∃ T, c T = true) {T : Finset (Fin n)} (hcT : c T = true) :
    X c ⊆ T ∧ T ⊆ X c ∪ B c := by
…
```
Mentions: Usa2015P3.X, Usa2015P3.B
lemma Usa2015P3.blue_iff A nontrivial valid coloring is exactly the interval [X c, X c ∪ B c] line 386 source
Source documentation
A nontrivial valid coloring is exactly the interval [X c, X c ∪ B c].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Usa2015P3.IsValid, Exists, Finset, Fin, Eq, Bool, Bool.true, Iff, And, LE.le, Usa2015P3.X, Union.union, Usa2015P3.B
Proof uses: Iff.intro, Usa2015P3.interval_of_blue, Usa2015P3.blue_of_mem_interval
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma blue_iff (hne : ∃ T, c T = true) (T : Finset (Fin n)) :
    c T = true ↔ X c ⊆ T ∧ T ⊆ X c ∪ B c := by
…
```
Mentions: Usa2015P3.X, Usa2015P3.B
def Usa2015P3.colorOf The coloring whose blue sets are exactly the sets T with X₀ ⊆ T ⊆ X₀ ∪ B₀ line 397 source
Source documentation
The coloring whose blue sets are exactly the sets T with X₀ ⊆ T ⊆ X₀ ∪ B₀.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Usa2015P3.Coloring
Proof uses: Decidable.decide, And, LE.le, Union.union
7 instances, coercions and auxiliary constants left out.
```
def colorOf (X₀ B₀ : Finset (Fin n)) : Coloring n := fun T => decide (X₀ ⊆ T ∧ T ⊆ X₀ ∪ B₀)
```
Mentions: Usa2015P3.Coloring
lemma Usa2015P3.blueCard_colorOf line 399 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Disjoint, Eq, Usa2015P3.blueCard, Usa2015P3.colorOf, ite, LE.le, HPow.hPow, OfNat.ofNat, Finset.card, Inter.inter
Proof uses: dite, Eq.mpr, id, congrArg, ite_eq_left, Finset.filter, Bool, Bool.true, Finset.powerset, Finset.image, Union.union, Finset.ext, Iff, Membership.mem, And, Exists, congr, Eq.trans, congrFun', Finset.filter.congr_simp and 36 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 66 steps
Open to load the checked before-and-after goal states.
lemma Usa2015P3.isValid_colorOf line 457 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Disjoint, Usa2015P3.IsValid, Usa2015P3.colorOf
Proof uses: Eq.mpr, Eq, HMul.hMul, Usa2015P3.blueCard, Union.union, Inter.inter, ite, LE.le, HPow.hPow, OfNat.ofNat, Finset.card, id, congrArg, Usa2015P3.blueCard_colorOf, dite, ite_eq_left, Finset.Subset.trans, Finset.subset_union_left, Finset.subset_inter, HAdd.hAdd and 14 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Usa2015P3.isValid_all_red line 478 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.IsValid, Finset, Fin, Bool.false
Proof uses: Eq, Usa2015P3.blueCard, OfNat.ofNat, Eq.mpr, Finset.card, Finset.filter, Bool, Bool.true, Finset.powerset, id, congrArg, Usa2015P3.blueCard.eq_1, of_eq_true, Eq.trans, True, congrFun', EmptyCollection.emptyCollection, False, Finset.filter_congr, Membership.mem and 9 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def Usa2015P3.DisjointPairs The type of disjoint pairs (X₀, B₀) of finsets of Fin n; these parametrize the nontrivial valid colorings line 490 source
Source documentation
The type of disjoint pairs (X₀, B₀) of finsets of Fin n; these parametrize the nontrivial valid colorings.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Subtype, Prod, Finset, Fin, Disjoint, Prod.fst, Prod.snd
2 instances, coercions and auxiliary constants left out.
```
def DisjointPairs (n : ℕ) : Type :=
…
```
instance Usa2015P3.(instance at line 493) line 493 source
lemma Usa2015P3.X_colorOf The blue interval [X₀, X₀ ∪ B₀] of a disjoint pair determines a valid coloring, and conversely every nontrivial valid coloring arises this way line 497 source
Source documentation
The blue interval [X₀, X₀ ∪ B₀] of a disjoint pair determines a valid coloring, and conversely every nontrivial valid coloring arises this way.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Eq, Usa2015P3.X, Usa2015P3.colorOf
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, LE.le, Union.union, id, congrFun', congrArg, Eq.trans, Bool, Bool.true, forall_congr, Decidable.decide, implies_congr, decide_eq_true_eq, Eq.refl, Iff.intro, And.intro and 3 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma X_colorOf {n : ℕ} {X₀ B₀ : Finset (Fin n)} :
    X (colorOf X₀ B₀) = X₀ := by
…
```
Mentions: Usa2015P3.X, Usa2015P3.colorOf
lemma Usa2015P3.B_colorOf line 507 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Disjoint, Eq, Usa2015P3.B, Usa2015P3.colorOf
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, Not, Usa2015P3.X, Bool, Union.union, Singleton.singleton, Bool.true, id, congrArg, propext, Usa2015P3.mem_B, Usa2015P3.X_colorOf, LE.le, congrFun', decide_eq_true_eq, Iff.intro and 13 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
def Usa2015P3.fromColoring The map from a valid coloring to its parametrizing data: none for the all-red coloring, and the disjoint pair (X c, B c) otherwise line 527 source
Source documentation
The map from a valid coloring to its parametrizing data: none for the all-red coloring, and the disjoint pair (X c, B c) otherwise.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P3.Coloring, Usa2015P3.IsValid, Option, Usa2015P3.DisjointPairs
Proof uses: dite, Exists, Finset, Fin, Eq, Bool, Bool.true, Option.some, Subtype.mk, Prod, Disjoint, Prod.fst, Prod.snd, Prod.mk, Usa2015P3.X, Usa2015P3.B, Not, Option.none
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def fromColoring {n : ℕ} (c : Coloring n) (_hv : IsValid c) : Option (DisjointPairs n) :=
…
```
Mentions: Usa2015P3.Coloring, Usa2015P3.IsValid, Usa2015P3.DisjointPairs
def Usa2015P3.toColoring The valid coloring associated to a parameter: the all-red coloring for none, and the interval coloring colorOf X₀ B₀ for a disjoint pair (X₀, B₀) line 537 source
Source documentation
The valid coloring associated to a parameter: the all-red coloring for none, and the interval coloring colorOf X₀ B₀ for a disjoint pair (X₀, B₀).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Option, Usa2015P3.DisjointPairs, Usa2015P3.ValidColorings
Proof uses: Usa2015P3.toColoring.match_1, Unit, Subtype.mk, Usa2015P3.Coloring, Usa2015P3.IsValid, Finset, Fin, Bool.false, Usa2015P3.isValid_all_red, Disjoint, Prod.fst, Prod.mk, Prod.snd, Usa2015P3.colorOf, Usa2015P3.isValid_colorOf
2 instances, coercions and auxiliary constants left out.
```
def toColoring {n : ℕ} : Option (DisjointPairs n) → ValidColorings n
  | none => ⟨fun _ => false, isValid_all_red⟩
  | some ⟨(X₀, B₀), h⟩ => ⟨colorOf X₀ B₀, isValid_colorOf h⟩

/-- The valid colorings are in bijection with the parameters. -/
```
Mentions: Usa2015P3.DisjointPairs, Usa2015P3.ValidColorings, Usa2015P3.isValid_all_red, h, Usa2015P3.colorOf, Usa2015P3.isValid_colorOf
def Usa2015P3.mainEquiv The valid colorings are in bijection with the parameters line 542 source
Source documentation
The valid colorings are in bijection with the parameters.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Usa2015P3.ValidColorings, Option, Usa2015P3.DisjointPairs
Proof uses: Equiv.mk, Usa2015P3.fromColoring, Usa2015P3.Coloring, Usa2015P3.IsValid, Usa2015P3.toColoring
4 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
def mainEquiv (n : ℕ) : ValidColorings n ≃ Option (DisjointPairs n) where
…
```
Mentions: Usa2015P3.ValidColorings, Usa2015P3.DisjointPairs
def Usa2015P3.disjointPairEquiv Disjoint pairs of finsets of Fin n correspond to ternary functions: each element is in X₀, in B₀, or in neither line 587 source
Source documentation
Disjoint pairs of finsets of Fin n correspond to ternary functions: each element is in X₀, in B₀, or in neither.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Usa2015P3.DisjointPairs, Fin, OfNat.ofNat
Proof uses: Equiv.mk, ite, Membership.mem, Finset, Prod.fst, Prod, Disjoint, Prod.snd, Subtype.mk, Prod.mk, Finset.filter, Eq, Finset.univ
15 instances, coercions and auxiliary constants left out.

Tactic trace: 78 steps
Open to load the checked before-and-after goal states.
```
def disjointPairEquiv (n : ℕ) : DisjointPairs n ≃ (Fin n → Fin 3) where
…
```
Mentions: Usa2015P3.DisjointPairs
lemma Usa2015P3.card_disjointPairs line 646 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Fintype.card, Usa2015P3.DisjointPairs, HPow.hPow, OfNat.ofNat
Proof uses: Eq.mpr, Fin, id, congrArg, Fintype.card_congr, Usa2015P3.disjointPairEquiv, Fintype.card_fun, of_eq_true, Eq.trans, True, congrFun', congr, Fintype.card_fin, eq_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2015P3.card_validColorings line 650 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Fintype.card, Usa2015P3.ValidColorings, HAdd.hAdd, HPow.hPow, OfNat.ofNat
Proof uses: Eq.mpr, Option, Usa2015P3.DisjointPairs, id, congrArg, Fintype.card_congr, Usa2015P3.mainEquiv, Fintype.card_option, Usa2015P3.card_disjointPairs, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
determine Usa2015P3.NumberOfColorings line 655 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, HPow.hPow, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
problem Usa2015P3.usa2015_p3 line 657 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Fintype.card, Usa2015P3.ValidColorings, Usa2015P3.NumberOfColorings
Proof uses: Usa2015P3.card_validColorings
1 instances, coercions and auxiliary constants left out.

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