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

112 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2024, Problem 2

Let S₁, S₂, ..., S₁₀₀ be finite sets of integers whose intersection is not empty. For each non-empty T ⊆ {S₁, S₂, ..., S₁₀₀}, the size of the intersection of the sets in T is a multiple of the number of sets in T. What is the least possible number of elements that are in at least 50 sets?

Imports (7)

Imported by 1 file

Compfiles.lean

determine Usa2024P2.solution line 34 source
no axioms what this means
Statement uses: Nat
Proof uses: HMul.hMul, OfNat.ofNat, Nat.choose
3 instances, coercions and auxiliary constants left out.
structure Usa2024P2.Good line 36 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Set, Int
1 instances, coercions and auxiliary constants left out.
abbrev Usa2024P2.InAtLeastKSubsets z is in at least k of the sets S line 43 source
Source comment
z is in at least k of the sets S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Set, Int
Proof uses: LE.le, Set.ncard, Set.ofPred, Membership.mem
4 instances, coercions and auxiliary constants left out.
```
abbrev InAtLeastKSubsets (S : Fin 100 → Set ℤ) (k : ℕ) (z : ℤ) : Prop :=
…
```
Mentions: S
abbrev Usa2024P2.Signature line 48 source
standard axioms: Quot.sound, propext what this means
Proof uses: Finset, Fin, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
def Usa2024P2.topSignature line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature
Proof uses: Finset.univ, Fin, OfNat.ofNat, Nat
2 instances, coercions and auxiliary constants left out.
def Usa2024P2.signatureOf The membership signature of an integer with respect to the family S line 53 source
Source documentation
The membership signature of an integer with respect to the family S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Set, Int, Usa2024P2.Signature
Proof uses: Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def signatureOf (S : Fin 100 → Set ℤ) (z : ℤ) : Signature := by
…
```
Mentions: S, Usa2024P2.Signature
lemma Usa2024P2.ncard_preimage_eq_sum_fibers line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidablePred, Set.Finite, Set.ofPred, Eq, Nat, Set.ncard, Finset.sum, Finset.univ, ite, OfNat.ofNat
Proof uses: Equiv, Sigma, Membership.mem, Set, Equiv.mk, Sigma.mk, Subtype.mk, Subtype.property, rfl, Sigma.fst, Sigma.snd, id, Eq.mpr, congrArg, Subtype.ext, Eq.refl, Sigma.subtype_ext, Subtype, Eq.symm, Set.Finite.subset and 20 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
def Usa2024P2.SignatureIntersectionCount Counts elements whose signature contains u line 124 source
Source documentation
Counts elements whose signature contains u.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat
Proof uses: Finset.sum, Finset.univ, Fin, OfNat.ofNat, ite, LE.le
9 instances, coercions and auxiliary constants left out.
```
noncomputable def SignatureIntersectionCount (f : Signature → ℕ) (u : Signature) : ℕ :=
…
```
Mentions: f, Usa2024P2.Signature
def Usa2024P2.SignatureCountCondition Divisibility condition in signature-count form line 128 source
Source documentation
Divisibility condition in signature-count form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat
Proof uses: Finset.Nonempty, Fin, OfNat.ofNat, Dvd.dvd, Finset.card, Usa2024P2.SignatureIntersectionCount
2 instances, coercions and auxiliary constants left out.
```
def SignatureCountCondition (f : Signature → ℕ) : Prop :=
…
```
Mentions: f, Usa2024P2.Signature
def Usa2024P2.SignatureObjective Number of realized points lying in at least 50 sets line 132 source
Source documentation
Number of realized points lying in at least 50 sets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat
Proof uses: Finset.sum, Finset.univ, Fin, OfNat.ofNat, ite, LE.le, Finset.card
6 instances, coercions and auxiliary constants left out.
```
noncomputable def SignatureObjective (f : Signature → ℕ) : ℕ :=
…
```
Mentions: f, Usa2024P2.Signature
def Usa2024P2.canonicalHighCount Canonical high-rank counts used by the construction line 136 source
Source documentation
Canonical high-rank counts used by the construction.

standard axioms: Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat
Proof uses: ite, LE.le, OfNat.ofNat, Finset.card, Fin, HSub.hSub, HMul.hMul
7 instances, coercions and auxiliary constants left out.
```
def canonicalHighCount (v : Signature) : ℕ :=
…
```
Mentions: Usa2024P2.Signature
lemma Usa2024P2.superset_layer_card Count supersignatures of u with exactly j new indices line 140 source
Source documentation
Count supersignatures of u with exactly j new indices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Eq, Finset.card, Finset.filter, And, LE.le, Fin, OfNat.ofNat, HAdd.hAdd, Finset.univ, Nat.choose, HSub.hSub
Proof uses: Usa2024P2.topSignature, Membership.mem, Finset, of_eq_true, Finset.powersetCard, Finset.ext, Iff.intro, Eq.mpr, id, congrArg, propext, Finset.mem_filter, And.intro, Iff.mpr, Finset.mem_powersetCard, And.right, Eq.mp, And.left, Finset.mem_univ, Iff.mp and 8 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma superset_layer_card (u : Signature) (j : ℕ) :
    ((Finset.univ : Finset Signature).filter
        (fun v : Signature => u ⊆ v ∧ v.card = u.card + j)).card =
      (100 - u.card).choose j := by
…
```
Mentions: Usa2024P2.Signature
def Usa2024P2.supersetLayer line 168 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Finset
Proof uses: Finset.filter, And, LE.le, Fin, OfNat.ofNat, Eq, Finset.card, HAdd.hAdd, Finset.univ
12 instances, coercions and auxiliary constants left out.
lemma Usa2024P2.mem_supersetLayer line 172 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Iff, Membership.mem, Finset, Usa2024P2.supersetLayer, And, LE.le, Fin, OfNat.ofNat, Eq, Finset.card, HAdd.hAdd
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.filter, Finset.univ, true_and, iff_self
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.supersetLayer_card line 176 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Eq, Finset.card, Usa2024P2.supersetLayer, Nat.choose, HSub.hSub, OfNat.ofNat, Fin
Proof uses: id, Usa2024P2.superset_layer_card
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.canonicalHighCount_of_superset_high line 180 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, LE.le, Nat, OfNat.ofNat, Finset.card, Fin, Eq, Usa2024P2.canonicalHighCount, HSub.hSub, HMul.hMul
Proof uses: Finset.card_le_card, of_eq_true, Eq.trans, True, congrFun', congrArg, ite_eq_left_of_eq_true, eq_true, le_trans, eq_self
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.canonicalHighCount_grouped_summand line 186 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, OfNat.ofNat, LE.le, HSub.hSub, HMul.hMul
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.sum_supersets_by_rank line 191 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Eq, Finset.sum, Finset.univ, Fin, OfNat.ofNat, ite, LE.le, Finset.card, Finset.range, HAdd.hAdd, HSub.hSub, HMul.hMul, Nat.choose
Proof uses: Trans.trans, Finset.filter, Eq.mpr, id, congrArg, Eq.symm, Finset.sum_filter, Eq.refl, Finset.sum_congr, rfl, Finset, Membership.mem, And.right, Eq.mp, And, propext, Finset.mem_filter, Finset.card_le_card, card_finset_fin_le, Eq.trans and 27 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.SignatureIntersectionCount_canonicalHighCount_grouped Group the high-count intersection sum by rank difference line 264 source
Source documentation
Group the high-count intersection sum by rank difference.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, LE.le, Nat, OfNat.ofNat, Finset.card, Fin, Eq, Usa2024P2.SignatureIntersectionCount, Usa2024P2.canonicalHighCount, Finset.sum, Finset.range, HAdd.hAdd, HSub.hSub, HMul.hMul, Nat.choose
Proof uses: Eq.mpr, Finset.univ, ite, id, congrArg, Usa2024P2.SignatureIntersectionCount.eq_1, Trans.trans, Finset.sum_congr, rfl, Finset, Membership.mem, dite, ite_eq_left, Usa2024P2.canonicalHighCount_of_superset_high, Eq.refl, Not, of_eq_true, Eq.trans, True, congr and 4 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma SignatureIntersectionCount_canonicalHighCount_grouped
    (u : Signature) (hu : 50 ≤ u.card) :
    SignatureIntersectionCount canonicalHighCount u =
      ∑ j ∈ Finset.range (100 - u.card + 1),
        (2 * (u.card + j) - 100) * (100 - u.card).choose j := by
…
```
Mentions: Usa2024P2.Signature, Usa2024P2.SignatureIntersectionCount, Usa2024P2.canonicalHighCount
lemma Usa2024P2.canonicalHighCount_grouped_sum_eq The binomial identity after grouping by rank line 283 source
Source documentation
The binomial identity after grouping by rank.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, OfNat.ofNat, LE.le, Finset.sum, Finset.range, HMul.hMul, HSub.hSub, Nat.choose, HPow.hPow
Proof uses: Nat.sum_range_choose, Nat.sum_range_mul_choose, Trans.trans, Finset.sum_congr, rfl, Finset, Membership.mem, Nat.le_of_lt_succ, Iff.mp, Nat.succ, LT.lt, Finset.mem_range, Eq.mpr, id, congrArg, Usa2024P2.canonicalHighCount_grouped_summand, Eq.refl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr and 42 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma canonicalHighCount_grouped_sum_eq {a m : ℕ}
    (ham : a + m = 100) (ha : 50 ≤ a) :
    (∑ j ∈ Finset.range (m + 1),
        (2 * (a + j) - 100) * m.choose j) =
      a * 2 ^ m := by
…
```
lemma Usa2024P2.SignatureIntersectionCount_canonicalHighCount_closed_form Closed form for canonical high-rank intersections line 330 source
Source documentation
Closed form for canonical high-rank intersections.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, LE.le, Nat, OfNat.ofNat, Finset.card, Fin, Eq, Usa2024P2.SignatureIntersectionCount, Usa2024P2.canonicalHighCount, HMul.hMul, HPow.hPow, HSub.hSub
Proof uses: Eq.mpr, Finset.sum, Finset.range, HAdd.hAdd, Nat.choose, id, congrArg, Usa2024P2.SignatureIntersectionCount_canonicalHighCount_grouped, card_finset_fin_le, Usa2024P2.canonicalHighCount_grouped_sum_eq
24 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma SignatureIntersectionCount_canonicalHighCount_closed_form
    (u : Signature) (hu : 50 ≤ u.card) :
    SignatureIntersectionCount canonicalHighCount u =
      u.card * 2 ^ (100 - u.card) := by
…
```
Mentions: Usa2024P2.Signature, Usa2024P2.SignatureIntersectionCount, Usa2024P2.canonicalHighCount
def Usa2024P2.pushDown Move one full block from v to its immediate sub-signatures line 339 source
Source documentation
Move one full block from v to its immediate sub-signatures.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat
Proof uses: ite, Eq, Fin, OfNat.ofNat, HSub.hSub, Finset.card, And, LE.le, HAdd.hAdd
13 instances, coercions and auxiliary constants left out.
```
def pushDown (f : Signature → ℕ) (v : Signature) : Signature → ℕ :=
…
```
Mentions: f, Usa2024P2.Signature
lemma Usa2024P2.immediate_supersets_count line 345 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, LE.le, Fin, OfNat.ofNat, Nat, Eq, Finset.sum, Finset.erase, Finset.univ, ite, And, HAdd.hAdd, Finset.card, HSub.hSub
Proof uses: Eq.mpr, Finset.filter, id, congrArg, Eq.symm, Finset.card_filter, dite, tsub_self, Finset, EmptyCollection.emptyCollection, Finset.ext, Iff.intro, Membership.mem, False.elim, Finset.Subset.antisymm, And.left, And.right, Eq.mp, propext, Finset.mem_filter and 25 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.canonicalHighCount_valid_on_high line 395 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, LE.le, Nat, OfNat.ofNat, Finset.card, Fin, Dvd.dvd, Usa2024P2.SignatureIntersectionCount, Usa2024P2.canonicalHighCount
Proof uses: Eq.mpr, HMul.hMul, HPow.hPow, HSub.hSub, id, Eq, congrArg, Usa2024P2.SignatureIntersectionCount_canonicalHighCount_closed_form, dvd_mul_right
15 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.sum_signatures_by_card line 402 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Usa2024P2.Signature, Finset.univ, Fin, OfNat.ofNat, Finset.card, Finset.range, HMul.hMul, Nat.choose
Proof uses: Eq.mp, ite, LE.le, EmptyCollection.emptyCollection, HAdd.hAdd, HSub.hSub, congr, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, ite_eq_left_of_eq_true, congrFun', tsub_zero, zero_add, Usa2024P2.sum_supersets_by_rank
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.high_rank_objective_sum_eq_tail line 407 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.sum, Finset.range, OfNat.ofNat, HMul.hMul, ite, LE.le, HSub.hSub, Nat.choose, HAdd.hAdd
Proof uses: Finset.sum_range_add, Eq.mpr, id, congrArg, Eq.mp, congrFun', Finset.sum_congr, Finset, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Membership.mem, Finset.sum_eq_zero, LT.lt, Iff.mp, Finset.mem_range, of_eq_true, Eq.trans, True and 12 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.high_rank_objective_summand_int line 427 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Int, HMul.hMul, HSub.hSub, Nat.choose
Proof uses: LT.lt, HAdd.hAdd, Nat.add_one_mul_choose_eq, Nat.sub_add_cancel, Eq.mpr, id, congrFun', congrArg, Nat.mul_comm, Eq.mp, congr, Eq.trans, Nat.choose_mul_succ_eq, cast, Eq.symm, Trans.trans, of_eq_true, True, Nat.cast_mul, eq_self and 37 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.high_rank_choose_telescope_int line 457 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, HMul.hMul, HSub.hSub, Nat.choose
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, Singleton.singleton, Finset, congrFun', zero_add, Finset.sum_singleton, add_zero, eq_self, Eq.mpr, id, Finset.sum_range_succ, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance and 48 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.high_rank_weighted_choose_sum line 469 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.sum, Finset.range, OfNat.ofNat, HMul.hMul, HSub.hSub, HAdd.hAdd, Nat.choose
Proof uses: Int, Trans.trans, Eq.mpr, id, congrArg, Nat.cast_sum, Eq.refl, Finset.sum_congr, rfl, Finset, Membership.mem, LT.lt, Iff.mp, Finset.mem_range, Usa2024P2.high_rank_objective_summand_int, Usa2024P2.high_rank_choose_telescope_int, Nat.add_one_mul_choose_eq, Nat.choose_succ_self, congr, Eq.trans and 10 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.canonicalHighCount_objective_rank_sum line 502 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.sum, Finset.range, OfNat.ofNat, HMul.hMul, ite, LE.le, HSub.hSub, Nat.choose, Usa2024P2.solution
Proof uses: Eq.mpr, HAdd.hAdd, id, congrArg, Usa2024P2.high_rank_objective_sum_eq_tail, Usa2024P2.solution.eq_1, Usa2024P2.high_rank_weighted_choose_sum
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.canonicalHighCount_objective line 509 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Usa2024P2.SignatureObjective, Usa2024P2.canonicalHighCount, Usa2024P2.solution
Proof uses: Eq.mpr, Finset.sum, Usa2024P2.Signature, Finset.univ, Fin, OfNat.ofNat, ite, LE.le, Finset.card, id, congrArg, Usa2024P2.SignatureObjective.eq_1, Trans.trans, Finset.range, HMul.hMul, HSub.hSub, Nat.choose, Finset.sum_congr, rfl, Finset and 14 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.pushDown_preserves_condition line 525 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LE.le, Finset.card, Fin, OfNat.ofNat, Usa2024P2.SignatureCountCondition, Usa2024P2.pushDown
Proof uses: Finset.Nonempty, dite, Dvd.dvd, Usa2024P2.SignatureIntersectionCount, Finset.card_le_card, Eq, HAdd.hAdd, Eq.mpr, Finset.sum, Finset.univ, ite, id, congrArg, Usa2024P2.SignatureIntersectionCount.eq_1, Finset.erase, Eq.symm, Finset.sum_erase_add, Finset.mem_univ, HSub.hSub, Trans.trans and 31 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.pushDown_preserves_objective_of_large line 597 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LT.lt, OfNat.ofNat, Finset.card, Fin, LE.le, Eq, Usa2024P2.SignatureObjective, Usa2024P2.pushDown
Proof uses: HSub.hSub, of_eq_true, Eq.trans, True, congrFun', congrArg, ite_eq_left_of_eq_true, ite, And, HAdd.hAdd, eq_self, eq_true, Nat.choose, Nat.casesAuxOn, Eq.symm, Eq.refl, add_tsub_cancel_right, Nat.choose_succ_self_right, Finset.sum, Finset.erase and 34 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.pushDown_decreases_objective_at_middle line 696 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Eq, Finset.card, Fin, OfNat.ofNat, LE.le, HAdd.hAdd, Usa2024P2.SignatureObjective, Usa2024P2.pushDown
Proof uses: HSub.hSub, of_eq_true, Eq.trans, True, congrFun', congrArg, ite, And, ite_eq_left_of_eq_true, eq_self, eq_true, Finset.sum, Finset.erase, Finset.univ, Finset.sum_congr, rfl, Finset, Membership.mem, Ne, And.left and 15 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
def Usa2024P2.strictSupersetContribution Strict-superset part of an intersection count line 750 source
Source documentation
Strict-superset part of an intersection count.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat
Proof uses: Finset.sum, Finset.univ, Fin, OfNat.ofNat, ite, LT.lt
9 instances, coercions and auxiliary constants left out.
```
noncomputable def strictSupersetContribution (f : Signature → ℕ) (u : Signature) : ℕ :=
…
```
Mentions: f, Usa2024P2.Signature
def Usa2024P2.fillRank Fill one rank with the least residue making divisibility hold line 754 source
Source documentation
Fill one rank with the least residue making divisibility hold.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature
Proof uses: ite, Eq, Finset.card, Fin, OfNat.ofNat, Usa2024P2.strictSupersetContribution, HMod.hMod, HSub.hSub
6 instances, coercions and auxiliary constants left out.
```
noncomputable def fillRank (k : ℕ) (f : Signature → ℕ) : Signature → ℕ :=
…
```
Mentions: f, Usa2024P2.Signature
lemma Usa2024P2.dvd_complement_mod_add The chosen residue makes residue + s divisible by d line 762 source
Source documentation
The chosen residue makes residue + s divisible by d.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Dvd.dvd, HAdd.hAdd, HMod.hMod, HSub.hSub
Proof uses: id, Nat.mod_lt, dite, Eq, Eq.mpr, congrArg, propext, Nat.dvd_iff_mod_eq_zero, of_eq_true, Eq.trans, True, congrFun', tsub_zero, Nat.mod_self, zero_add, eq_self, Not, Nat.mod_eq_of_lt, Exists.intro, HMul.hMul and 29 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma dvd_complement_mod_add {d s : ℕ} (hd : 0 < d) :
    d ∣ ((d - s % d) % d) + s := by
…
```
lemma Usa2024P2.fillRank_eq_of_card line 781 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, Eq, Finset.card, Fin, OfNat.ofNat, Usa2024P2.fillRank, Usa2024P2.strictSupersetContribution, HMod.hMod, HSub.hSub
Proof uses: of_eq_true, Eq.trans, True, congr, congrArg, ite, ite_eq_left_of_eq_true, congrFun', eq_self
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.fillRank_eq_self_of_card_ne line 788 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, Ne, Finset.card, Fin, OfNat.ofNat, Eq, Usa2024P2.fillRank
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite_eq_right_of_eq_false, Usa2024P2.strictSupersetContribution, HMod.hMod, HSub.hSub, eq_false, eq_self
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.fillRank_eq_self_of_card_gt line 792 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, LT.lt, Finset.card, Fin, OfNat.ofNat, Eq, Usa2024P2.fillRank
Proof uses: Usa2024P2.fillRank_eq_self_of_card_ne
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.fillRank_eq_self_of_card_lt line 796 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, LT.lt, Finset.card, Fin, OfNat.ofNat, Eq, Usa2024P2.fillRank
Proof uses: Usa2024P2.fillRank_eq_self_of_card_ne
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.fillRank_eq_self_of_high line 800 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, LT.lt, OfNat.ofNat, LE.le, Finset.card, Fin, Eq, Usa2024P2.fillRank
Proof uses: Usa2024P2.fillRank_eq_self_of_card_gt
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.fillRank_eq_self_on_supersets_of_card_lt line 804 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, LT.lt, Finset.card, Fin, OfNat.ofNat, LE.le, Eq, Usa2024P2.fillRank
Proof uses: Usa2024P2.fillRank_eq_self_of_card_gt, lt_of_lt_of_le, Finset.card_le_card
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.strictSupersetContribution_congr line 810 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LT.lt, Fin, OfNat.ofNat, Eq, Usa2024P2.strictSupersetContribution
Proof uses: id, Finset.sum_congr, Finset.univ, ite, rfl, Finset, Membership.mem, ite_congr, Not
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.strictSupersetContribution_eq_canonical_of_strict Canonical strict supersets give the canonical strict contribution line 817 source
Source documentation
Canonical strict supersets give the canonical strict contribution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LT.lt, Fin, OfNat.ofNat, Eq, Usa2024P2.canonicalHighCount, Usa2024P2.strictSupersetContribution
Proof uses: Usa2024P2.strictSupersetContribution_congr
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma strictSupersetContribution_eq_canonical_of_strict
    {f : Signature → ℕ} {u : Signature}
    (hstrict : ∀ w : Signature, u ⊂ w → f w = canonicalHighCount w) :
    strictSupersetContribution f u =
      strictSupersetContribution canonicalHighCount u := by
…
```
Mentions: f, Usa2024P2.Signature, Usa2024P2.canonicalHighCount, Usa2024P2.strictSupersetContribution
lemma Usa2024P2.SignatureIntersectionCount_eq_self_add_strict Split an intersection count into exact and strict-superset terms line 825 source
Source documentation
Split an intersection count into exact and strict-superset terms.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Eq, Usa2024P2.SignatureIntersectionCount, HAdd.hAdd, Usa2024P2.strictSupersetContribution
Proof uses: ite, LE.le, Fin, OfNat.ofNat, LT.lt, Finset.sum, Finset.erase, Finset.univ, Finset.sum_congr, rfl, Finset, Membership.mem, Ne, And.left, Iff.mp, And, Finset.mem_erase, dite, Iff.mpr, Finset.ssubset_iff_subset_ne and 27 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma SignatureIntersectionCount_eq_self_add_strict
    (f : Signature → ℕ) (u : Signature) :
    SignatureIntersectionCount f u = f u + strictSupersetContribution f u := by
…
```
Mentions: f, Usa2024P2.Signature, Usa2024P2.SignatureIntersectionCount, Usa2024P2.strictSupersetContribution
lemma Usa2024P2.modEq_self_of_split_divisibilities Divisibility after adding the same tail gives a congruence line 862 source
Source documentation
Divisibility after adding the same tail gives a congruence.

standard axioms: propext what this means
Statement uses: Nat, Dvd.dvd, HAdd.hAdd, Nat.ModEq
Proof uses: OfNat.ofNat, Iff.mpr, Nat.modEq_zero_iff_dvd, Nat.ModEq.add_right_cancel', Nat.ModEq.trans, Nat.ModEq.symm
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma modEq_self_of_split_divisibilities {d a b T : ℕ}
    (ha : d ∣ a + T) (hb : d ∣ b + T) :
    a ≡ b [MOD d] := by
…
```
lemma Usa2024P2.le_of_modEq_of_lt_modulus A small representative is a lower bound for congruent naturals line 870 source
Source documentation
A small representative is a lower bound for congruent naturals.

standard axioms: propext what this means
Statement uses: Nat, LT.lt, Nat.ModEq, LE.le
Proof uses: Eq, HMod.hMod, Nat.mod_eq_of_lt, Eq.mp, congrArg, Trans.trans, Eq.symm, Nat.mod_le
7 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma le_of_modEq_of_lt_modulus {d a b : ℕ}
    (hb : b < d) (hmod : a ≡ b [MOD d]) :
    b ≤ a := by
…
```
lemma Usa2024P2.SignatureIntersectionCount_fillRank_of_card_gt line 880 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, LT.lt, Finset.card, Fin, OfNat.ofNat, Eq, Usa2024P2.SignatureIntersectionCount, Usa2024P2.fillRank
Proof uses: Eq.mpr, Finset.sum, Finset.univ, ite, LE.le, id, congrArg, Usa2024P2.SignatureIntersectionCount.eq_1, Finset.sum_congr, rfl, Finset, Membership.mem, dite, ite_eq_left, Usa2024P2.fillRank_eq_self_on_supersets_of_card_lt, Eq.refl, Not, of_eq_true, Eq.trans, True and 4 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.fillRank_self_add_strictSupersetContribution_dvd line 890 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, Eq, Finset.card, Fin, OfNat.ofNat, LT.lt, Dvd.dvd, HAdd.hAdd, Usa2024P2.fillRank, Usa2024P2.strictSupersetContribution
Proof uses: Eq.mpr, HMod.hMod, HSub.hSub, id, congrArg, Usa2024P2.fillRank_eq_of_card, Usa2024P2.dvd_complement_mod_add
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.fillRank_satisfies_rank Filling rank k makes rank k valid line 897 source
Source documentation
Filling rank k makes rank k valid.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, Eq, Finset.card, Fin, OfNat.ofNat, LT.lt, Dvd.dvd, Usa2024P2.SignatureIntersectionCount, Usa2024P2.fillRank
Proof uses: Eq.mpr, HAdd.hAdd, Usa2024P2.strictSupersetContribution, id, congrArg, Usa2024P2.SignatureIntersectionCount_eq_self_add_strict, Usa2024P2.strictSupersetContribution_congr, Usa2024P2.fillRank_eq_self_of_card_gt, Finset.card_lt_card, Usa2024P2.fillRank_self_add_strictSupersetContribution_dvd
12 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma fillRank_satisfies_rank {k : ℕ} {f : Signature → ℕ} {u : Signature}
    (hu : u.card = k) (hupos : 0 < u.card) :
    u.card ∣ SignatureIntersectionCount (fillRank k f) u := by
…
```
Mentions: f, Usa2024P2.Signature, Usa2024P2.SignatureIntersectionCount, Usa2024P2.fillRank
lemma Usa2024P2.fillRank_preserves_completed_ranks Filling rank k preserves completed higher ranks line 913 source
Source documentation
Filling rank k preserves completed higher ranks.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, Finset.Nonempty, Fin, OfNat.ofNat, LT.lt, Finset.card, Dvd.dvd, Usa2024P2.SignatureIntersectionCount, Usa2024P2.fillRank
Proof uses: Eq.mpr, id, Eq, congrArg, Usa2024P2.SignatureIntersectionCount_fillRank_of_card_gt
6 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma fillRank_preserves_completed_ranks {k : ℕ} {f : Signature → ℕ}
    (hf : ∀ u : Signature, u.Nonempty → k < u.card →
      u.card ∣ SignatureIntersectionCount f u) :
    ∀ u : Signature, u.Nonempty → k < u.card →
      u.card ∣ SignatureIntersectionCount (fillRank k f) u := by
…
```
Mentions: f, Usa2024P2.Signature, Usa2024P2.SignatureIntersectionCount, Usa2024P2.fillRank
lemma Usa2024P2.fillRank_extends_completed_ranks After filling rank k, all ranks at least k are valid line 923 source
Source documentation
After filling rank k, all ranks at least k are valid.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, Finset.Nonempty, Fin, OfNat.ofNat, LT.lt, Finset.card, Dvd.dvd, Usa2024P2.SignatureIntersectionCount, LE.le, Usa2024P2.fillRank
Proof uses: dite, Eq, Usa2024P2.fillRank_satisfies_rank, Iff.mpr, Finset.card_pos, Not, Usa2024P2.fillRank_preserves_completed_ranks
10 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma fillRank_extends_completed_ranks {k : ℕ} {f : Signature → ℕ}
    (hf : ∀ u : Signature, u.Nonempty → k < u.card →
      u.card ∣ SignatureIntersectionCount f u) :
    ∀ u : Signature, u.Nonempty → k ≤ u.card →
      u.card ∣ SignatureIntersectionCount (fillRank k f) u := by
…
```
Mentions: f, Usa2024P2.Signature, Usa2024P2.SignatureIntersectionCount, Usa2024P2.fillRank
lemma Usa2024P2.SignatureObjective_fillRank_of_low Low-rank filling does not change the high-rank objective line 936 source
Source documentation
Low-rank filling does not change the high-rank objective.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, LT.lt, OfNat.ofNat, Eq, Usa2024P2.SignatureObjective, Usa2024P2.fillRank
Proof uses: Eq.mpr, Finset.sum, Finset.univ, Fin, ite, LE.le, Finset.card, id, congrArg, Usa2024P2.SignatureObjective.eq_1, Finset.sum_congr, rfl, Finset, Membership.mem, dite, Usa2024P2.fillRank_eq_self_of_high, Eq.refl, Not, of_eq_true, Eq.trans and 5 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma SignatureObjective_fillRank_of_low {k : ℕ} {f : Signature → ℕ}
    (hk : k < 50) :
    SignatureObjective (fillRank k f) = SignatureObjective f := by
…
```
Mentions: f, Usa2024P2.Signature, Usa2024P2.SignatureObjective, Usa2024P2.fillRank
def Usa2024P2.lowerFill line 946 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature
2 instances, coercions and auxiliary constants left out.
lemma Usa2024P2.lowerFill_valid line 950 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Usa2024P2.Signature, Finset.Nonempty, Fin, HSub.hSub, Finset.card, Dvd.dvd, Usa2024P2.SignatureIntersectionCount, Usa2024P2.lowerFill
Proof uses: Nat.recAux, Usa2024P2.canonicalHighCount_valid_on_high, Eq.mp, congrFun', congrArg, tsub_zero, HAdd.hAdd, id, Usa2024P2.fillRank_extends_completed_ranks, LT.lt
19 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.lowerFill_preserves_high line 971 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, LE.le, OfNat.ofNat, Finset.card, Fin, Eq, Usa2024P2.lowerFill, Usa2024P2.canonicalHighCount
Proof uses: Nat.recAux, Eq.refl, id, HAdd.hAdd, Eq.mpr, Usa2024P2.fillRank, HSub.hSub, congrArg, Usa2024P2.fillRank_eq_self_of_high
9 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.lowerFill_objective line 984 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2024P2.SignatureObjective, Usa2024P2.lowerFill, Usa2024P2.canonicalHighCount
Proof uses: Nat.recAux, Eq.refl, OfNat.ofNat, id, HAdd.hAdd, Eq.mpr, Usa2024P2.fillRank, HSub.hSub, congrArg, Usa2024P2.SignatureObjective_fillRank_of_low
6 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.lower_rank_filling_exists Fill ranks 49, ..., 1 line 997 source
Source documentation
Fill ranks 49, ..., 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Usa2024P2.Signature, Nat, And, Finset.Nonempty, Fin, OfNat.ofNat, Dvd.dvd, Finset.card, Usa2024P2.SignatureIntersectionCount, LE.le, Eq, Usa2024P2.canonicalHighCount, Usa2024P2.SignatureObjective
Proof uses: Exists.intro, Usa2024P2.lowerFill, And.intro, Usa2024P2.lowerFill_valid, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, LT.lt, Iff.mpr, Finset.card_pos, Usa2024P2.lowerFill_preserves_high, Usa2024P2.lowerFill_objective
13 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma lower_rank_filling_exists :
    ∃ f : Signature → ℕ,
      (∀ u : Signature, u.Nonempty →
        u.card ∣ SignatureIntersectionCount f u) ∧
      (∀ v : Signature, 50 ≤ v.card → f v = canonicalHighCount v) ∧
      SignatureObjective f = SignatureObjective canonicalHighCount := by
…
```
Mentions: f, Usa2024P2.Signature, Usa2024P2.SignatureIntersectionCount, Usa2024P2.canonicalHighCount, Usa2024P2.SignatureObjective
lemma Usa2024P2.extend_canonical_high_counts Construct a valid signature count model extending the canonical high ranks line 1012 source
Source documentation
Construct a valid signature count model extending the canonical high ranks.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Usa2024P2.Signature, Nat, And, Usa2024P2.SignatureCountCondition, LT.lt, OfNat.ofNat, Usa2024P2.topSignature, LE.le, Finset.card, Fin, Eq, Usa2024P2.canonicalHighCount, Usa2024P2.SignatureObjective, Usa2024P2.solution
Proof uses: Finset.Nonempty, Dvd.dvd, Usa2024P2.SignatureIntersectionCount, Usa2024P2.lower_rank_filling_exists, Exists.intro, And.intro, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, Fintype.card_fin, eq_true_of_decide, Eq.refl, Bool, Bool.true, ite, HSub.hSub, HMul.hMul and 3 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma extend_canonical_high_counts :
    ∃ f : Signature → ℕ,
      SignatureCountCondition f ∧
      0 < f topSignature ∧
      (∀ v : Signature, 50 ≤ v.card → f v = canonicalHighCount v) ∧
      SignatureObjective f = solution := by
…
```
Mentions: f, Usa2024P2.Signature, Usa2024P2.SignatureCountCondition, Usa2024P2.topSignature, Usa2024P2.canonicalHighCount, Usa2024P2.SignatureObjective, Usa2024P2.solution
abbrev Usa2024P2.RealizedPoint line 1024 source
standard axioms: Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat
Proof uses: Sigma, Fin
def Usa2024P2.encodePoint line 1027 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Function.Embedding, Usa2024P2.RealizedPoint, Int
Proof uses: Equiv, Fin, Fintype.card, OfNat.ofNat, Fintype.equivFin, Function.Embedding.mk
11 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def Usa2024P2.realizedFamily line 1038 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Fin, OfNat.ofNat, Set, Int
Proof uses: Set.range, Subtype, Usa2024P2.RealizedPoint, Membership.mem, Sigma.fst, Function.Embedding, Usa2024P2.encodePoint
7 instances, coercions and auxiliary constants left out.
lemma Usa2024P2.realizedFamily_finite line 1043 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Fin, OfNat.ofNat, Set.Finite, Int, Usa2024P2.realizedFamily
Proof uses: Set.finite_range, Subtype, Usa2024P2.RealizedPoint, Membership.mem, Sigma.fst, Function.Embedding, Usa2024P2.encodePoint
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.mem_realizedFamily_iff line 1048 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Fin, OfNat.ofNat, Usa2024P2.RealizedPoint, Iff, Membership.mem, Int, Set, Usa2024P2.realizedFamily, Function.Embedding, Usa2024P2.encodePoint, Sigma.fst
Proof uses: Iff.intro, Subtype, Eq, Function.Embedding.injective, Eq.mp, congrFun', congrArg, Subtype.property, Exists.intro, Subtype.mk, rfl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.realizedPoint_subtype_card line 1059 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, DecidablePred, Eq, Nat.card, Subtype, Usa2024P2.RealizedPoint, Sigma.fst, Fin, Finset.sum, Finset.univ, OfNat.ofNat, ite
Proof uses: Equiv, Sigma, Equiv.subtypeSigmaEquiv, Trans.trans, Fintype.card, Nat.card_eq_fintype_card, Fintype.card_congr, Eq.mpr, id, congrArg, Fintype.card_sigma, of_eq_true, Eq.trans, True, congrFun', Finset.sum_congr, Eq.refl, Finset, Membership.mem, Fintype.card_fin and 9 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.realized_intersection_eq line 1082 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Finset.Nonempty, Fin, OfNat.ofNat, Eq, Set, Int, Set.iInter, Membership.mem, Usa2024P2.realizedFamily, Set.range, Subtype, Usa2024P2.RealizedPoint, LE.le, Sigma.fst, Function.Embedding, Usa2024P2.encodePoint
Proof uses: Set.ext, Iff.intro, Finset, Iff.mp, Set.mem_iInter₂, Eq.mpr, id, congrArg, Usa2024P2.mem_realizedFamily_iff, Exists.intro, Subtype.mk, Eq.symm, Iff.mpr, Subtype.property
20 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.realized_intersection_ncard line 1106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Finset.Nonempty, Fin, OfNat.ofNat, Eq, Set.ncard, Int, Set.iInter, Membership.mem, Usa2024P2.realizedFamily, Usa2024P2.SignatureIntersectionCount
Proof uses: Eq.mpr, Set.range, Subtype, Usa2024P2.RealizedPoint, LE.le, Sigma.fst, Function.Embedding, Usa2024P2.encodePoint, id, congrArg, Set, Usa2024P2.realized_intersection_eq, Nat.card, Set.ncard_range_of_injective, Subtype.ext, Function.Embedding.injective, Finset.sum, Finset.univ, ite, Usa2024P2.realizedPoint_subtype_card and 2 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.realized_membership_ncard line 1116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Usa2024P2.RealizedPoint, Eq, Set.ncard, Fin, OfNat.ofNat, Set.ofPred, Membership.mem, Int, Set, Usa2024P2.realizedFamily, Function.Embedding, Usa2024P2.encodePoint, Finset.card, Sigma.fst
Proof uses: Set.Finite, Set.Finite.subset, Set.univ, Set.finite_univ, of_eq_true, Eq.mpr, Set.Finite.toFinset, id, congrArg, Set.ncard_eq_toFinset_card, Finset, Finset.ext, Iff, propext, Set.Finite.mem_toFinset, Usa2024P2.mem_realizedFamily_iff, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.realized_objective_ncard line 1129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Eq, Set.ncard, Int, Set.ofPred, Usa2024P2.InAtLeastKSubsets, Usa2024P2.realizedFamily, OfNat.ofNat, Usa2024P2.SignatureObjective
Proof uses: Set, Set.range, Subtype, Usa2024P2.RealizedPoint, LE.le, Finset.card, Fin, Sigma.fst, Function.Embedding, Usa2024P2.encodePoint, Set.ext, Iff.intro, Membership.mem, Set.Finite, Set.Finite.subset, Set.univ, Set.finite_univ, of_eq_true, LT.lt, lt_of_lt_of_le and 29 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.realize_signature_counts Realize finite signature counts by finite integer sets line 1166 source
Source documentation
Realize finite signature counts by finite integer sets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Usa2024P2.SignatureCountCondition, LT.lt, OfNat.ofNat, Usa2024P2.topSignature, Exists, Fin, Set, Int, And, Usa2024P2.Good, Eq, Set.ncard, Set.ofPred, Usa2024P2.InAtLeastKSubsets, Usa2024P2.SignatureObjective
Proof uses: Exists.intro, Usa2024P2.realizedFamily, And.intro, Usa2024P2.Good.mk, Usa2024P2.realizedFamily_finite, Usa2024P2.RealizedPoint, Sigma.mk, Fin.mk, Iff.mp, Set.Nonempty, Set.iInter, Ne, EmptyCollection.emptyCollection, Set.nonempty_iff_ne_empty, Membership.mem, Function.Embedding, Usa2024P2.encodePoint, Iff.mpr, Set.mem_iInter, Sigma.fst and 16 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma realize_signature_counts
    {f : Signature → ℕ}
    (hf : SignatureCountCondition f) (htop : 0 < f topSignature) :
    ∃ S : Fin 100 → Set ℤ,
      Good S ∧
      {z : ℤ | InAtLeastKSubsets S 50 z }.ncard = SignatureObjective f := by
…
```
Mentions: f, Usa2024P2.Signature, Usa2024P2.SignatureCountCondition, Usa2024P2.topSignature, S, Usa2024P2.Good, Usa2024P2.InAtLeastKSubsets, Usa2024P2.SignatureObjective
def Usa2024P2.signatureCount Exact signature counts extracted from an actual family line 1187 source
Source documentation
Exact signature counts extracted from an actual family.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Set, Int, Usa2024P2.Signature
Proof uses: ite, Finset.Nonempty, Set.ncard, Set.ofPred, Eq, Usa2024P2.signatureOf
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def signatureCount (S : Fin 100 → Set ℤ) (v : Signature) : ℕ := by
…
```
Mentions: S, Usa2024P2.Signature
lemma Usa2024P2.signatureCount_condition_of_good line 1190 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Set, Int, Usa2024P2.Good, Usa2024P2.SignatureCountCondition, Usa2024P2.signatureCount
Proof uses: Usa2024P2.Signature, Finset.Nonempty, Eq, Set.ncard, Set.iInter, Membership.mem, Finset, HMul.hMul, Finset.card, Exists, Dvd.dvd, Usa2024P2.SignatureIntersectionCount, Usa2024P2.Good.card, Exists.intro, Eq.mpr, id, congrArg, Eq.symm, Eq.mp, mul_comm and 39 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.signatureCount_top_pos_of_good line 1228 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Set, Int, Usa2024P2.Good, LT.lt, Usa2024P2.signatureCount, Usa2024P2.topSignature
Proof uses: Finset.Nonempty, Exists.intro, Membership.mem, Finset, of_eq_true, Finset.univ, Set.Nonempty, Set.iInter, Iff.mpr, Ne, EmptyCollection.emptyCollection, Set.nonempty_iff_ne_empty, Usa2024P2.Good.nonempty_inter, Eq, Usa2024P2.Signature, Usa2024P2.signatureOf, Finset.ext, Iff.mp, Set.mem_iInter, Iff and 23 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.signatureObjective_eq_original_objective line 1254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Set, Int, Usa2024P2.Good, Eq, Usa2024P2.SignatureObjective, Usa2024P2.signatureCount, Set.ncard, Set.ofPred, Usa2024P2.InAtLeastKSubsets
Proof uses: Membership.mem, Finset.card, Usa2024P2.signatureOf, Set.Finite, Set.Finite.subset, Set.univ, Set.finite_univ, of_eq_true, Eq.mpr, Set.Finite.toFinset, id, congrArg, Set.ncard_eq_toFinset_card, Finset.filter, Classical.propDecidable, Finset.univ, Eq.trans, True, congrFun', Finset and 48 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.topSignature_card line 1304 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Fin, OfNat.ofNat, Usa2024P2.topSignature
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Fintype.card_fin, eq_self
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.topSignature_nonempty line 1307 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset.Nonempty, Fin, OfNat.ofNat, Nat, Usa2024P2.topSignature
Proof uses: Exists.intro, Membership.mem, Finset, of_eq_true, Finset.univ
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.eq_topSignature_of_card_eq_100 line 1310 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Eq, Nat, Finset.card, Fin, OfNat.ofNat, Usa2024P2.topSignature
Proof uses: Finset.eq_univ_of_card, of_eq_true, Fintype.card, Eq.trans, True, congr, congrArg, Fintype.card_fin, eq_self
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.card_lt_100_of_ne_topSignature line 1315 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Ne, Usa2024P2.topSignature, LT.lt, Nat, Finset.card, Fin, OfNat.ofNat
Proof uses: LE.le, card_finset_fin_le, Decidable.byContradiction, Not, Eq, Usa2024P2.eq_topSignature_of_card_eq_100
7 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.canonicalHighCount_top line 1322 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Usa2024P2.canonicalHighCount, Usa2024P2.topSignature, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite, LE.le, Finset.card, Fin, HSub.hSub, HMul.hMul, ite_eq_left_of_eq_true, Fintype.card_fin, eq_true_of_decide, Eq.refl, Bool, Bool.true, eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.canonicalHighCount_lt_card_of_high_ne_top line 1325 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, LE.le, Nat, OfNat.ofNat, Finset.card, Fin, Ne, Usa2024P2.topSignature, LT.lt, Usa2024P2.canonicalHighCount
Proof uses: Usa2024P2.card_lt_100_of_ne_topSignature, Eq.mpr, HSub.hSub, HMul.hMul, id, Eq, Eq.trans, congrFun', congrArg, ite_eq_left_of_eq_true, eq_true
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.canonicalHighCount_le_card_of_high line 1332 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, LE.le, Nat, OfNat.ofNat, Finset.card, Fin, Usa2024P2.canonicalHighCount
Proof uses: dite, Eq, Usa2024P2.topSignature, of_eq_true, Eq.trans, True, congr, congrArg, ite, HSub.hSub, HMul.hMul, ite_eq_left_of_eq_true, Fintype.card_fin, eq_true_of_decide, Eq.refl, Bool, Bool.true, congrFun', Eq.symm, Not and 2 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.iterate_pushDown_self line 1339 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Eq, Nat.iterate, Usa2024P2.pushDown, HSub.hSub, HMul.hMul, Finset.card, Fin, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, MulZeroClass.zero_mul, tsub_zero, eq_self, Eq.mpr, HAdd.hAdd, Function.comp, id, Nat.succ, Function.iterate_succ', congrFun', ite_eq_left_of_eq_true, ite, And, LE.le, Nat.sub_sub and 26 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.iterate_pushDown_condition line 1353 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LE.le, HMul.hMul, Finset.card, Fin, OfNat.ofNat, Usa2024P2.SignatureCountCondition, Nat.iterate, Usa2024P2.pushDown
Proof uses: Nat.recAux, id, HAdd.hAdd, Eq.mpr, Function.comp, Eq, congrArg, Nat.succ, Function.iterate_succ', Usa2024P2.pushDown_preserves_condition, HSub.hSub, Usa2024P2.iterate_pushDown_self, 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.symm and 18 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.iterate_pushDown_objective_le line 1372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LE.le, OfNat.ofNat, Finset.card, Fin, HMul.hMul, Usa2024P2.SignatureObjective, Nat.iterate, Usa2024P2.pushDown
Proof uses: Nat.recAux, of_eq_true, HAdd.hAdd, Eq.mpr, Function.comp, id, Eq, congrArg, Nat.succ, Function.iterate_succ', Nat.mul_le_mul_right, Nat.le_succ, HSub.hSub, Usa2024P2.iterate_pushDown_self, 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 and 24 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.pushDown_to_canonical_count line 1405 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Usa2024P2.SignatureCountCondition, LE.le, OfNat.ofNat, Finset.card, Fin, Usa2024P2.canonicalHighCount, Dvd.dvd, HSub.hSub, HDiv.hDiv, Nat.iterate, Usa2024P2.pushDown, And, Usa2024P2.SignatureObjective, Eq
Proof uses: id, HMul.hMul, Nat.div_mul_cancel, And.intro, Usa2024P2.iterate_pushDown_condition, Usa2024P2.iterate_pushDown_objective_le, Eq.mpr, congrArg, Usa2024P2.iterate_pushDown_self
18 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Usa2024P2.rankSignatures Signatures of rank k line 1422 source
Source documentation
Signatures of rank k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2024P2.Signature
Proof uses: Finset.filter, Eq, Finset.card, Fin, OfNat.ofNat, Finset.univ
4 instances, coercions and auxiliary constants left out.
```
def rankSignatures (k : ℕ) : Finset Signature :=
…
```
Mentions: Usa2024P2.Signature
lemma Usa2024P2.mem_rankSignatures line 1425 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, Iff, Membership.mem, Finset, Usa2024P2.rankSignatures, Eq, Finset.card, Fin, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, And, LE.le, Finset.univ, Finset.powersetCard, Finset.univ_filter_card_eq, true_and, iff_self
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.pushDown_eq_self_of_not_affected line 1429 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Ne, Not, And, LE.le, Fin, OfNat.ofNat, Eq, HAdd.hAdd, Finset.card, Usa2024P2.pushDown
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite, HSub.hSub, ite_eq_right_of_eq_false, eq_false, eq_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.pushDown_eq_self_of_card_ge_ne line 1435 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LE.le, Finset.card, Fin, OfNat.ofNat, Ne, Eq, Usa2024P2.pushDown
Proof uses: Usa2024P2.pushDown_eq_self_of_not_affected, And, HAdd.hAdd
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.pushDown_eq_self_of_card_gt line 1442 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LT.lt, Finset.card, Fin, OfNat.ofNat, Eq, Usa2024P2.pushDown
Proof uses: Usa2024P2.pushDown_eq_self_of_card_ge_ne, le_of_lt, False
7 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.iterate_pushDown_eq_self_of_not_affected line 1450 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Ne, Not, And, LE.le, Fin, OfNat.ofNat, Eq, HAdd.hAdd, Finset.card, Nat.iterate, Usa2024P2.pushDown
Proof uses: Nat.recAux, of_eq_true, eq_self, Eq.mpr, Function.comp, id, congrArg, Nat.succ, Function.iterate_succ', Usa2024P2.pushDown_eq_self_of_not_affected, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.iterate_pushDown_eq_self_of_card_ge_ne line 1463 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LE.le, Finset.card, Fin, OfNat.ofNat, Ne, Eq, Nat.iterate, Usa2024P2.pushDown
Proof uses: Usa2024P2.iterate_pushDown_eq_self_of_not_affected, And, HAdd.hAdd
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.iterate_pushDown_eq_self_of_card_gt line 1471 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LT.lt, Finset.card, Fin, OfNat.ofNat, Eq, Nat.iterate, Usa2024P2.pushDown
Proof uses: Usa2024P2.iterate_pushDown_eq_self_of_card_ge_ne, le_of_lt, False
7 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.iterate_pushDown_preserves_canonical_of_card_gt line 1480 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LT.lt, Finset.card, Fin, OfNat.ofNat, Eq, Usa2024P2.canonicalHighCount, Nat.iterate, Usa2024P2.pushDown
Proof uses: Eq.mpr, id, congrArg, Usa2024P2.iterate_pushDown_eq_self_of_card_gt, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.iterate_pushDown_preserves_canonical_of_same_rank_ne line 1488 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Eq, Finset.card, Fin, OfNat.ofNat, Ne, Usa2024P2.canonicalHighCount, Nat.iterate, Usa2024P2.pushDown
Proof uses: Eq.mpr, id, congrArg, Usa2024P2.iterate_pushDown_eq_self_of_card_ge_ne, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Usa2024P2.normalizeSignature Push v down to its canonical high-rank residue line 1497 source
Source documentation
Push v down to its canonical high-rank residue.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat
Proof uses: HDiv.hDiv, HSub.hSub, Usa2024P2.canonicalHighCount, Finset.card, Fin, OfNat.ofNat, Nat.iterate, Usa2024P2.pushDown
5 instances, coercions and auxiliary constants left out.
```
def normalizeSignature (f : Signature → ℕ) (v : Signature) : Signature → ℕ :=
…
```
Mentions: f, Usa2024P2.Signature
lemma Usa2024P2.normalizeSignature_eq_self_of_card_gt line 1501 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LT.lt, Finset.card, Fin, OfNat.ofNat, Eq, Usa2024P2.normalizeSignature
Proof uses: id, Usa2024P2.iterate_pushDown_eq_self_of_card_gt, HDiv.hDiv, HSub.hSub, Usa2024P2.canonicalHighCount
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.normalizeSignature_preserves_canonical_of_card_gt line 1508 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LT.lt, Finset.card, Fin, OfNat.ofNat, Eq, Usa2024P2.canonicalHighCount, Usa2024P2.normalizeSignature
Proof uses: Eq.mpr, id, congrArg, Usa2024P2.normalizeSignature_eq_self_of_card_gt, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.normalizeSignature_preserves_canonical_of_same_rank_ne line 1515 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Eq, Finset.card, Fin, OfNat.ofNat, Ne, Usa2024P2.canonicalHighCount, Usa2024P2.normalizeSignature
Proof uses: id, Usa2024P2.iterate_pushDown_preserves_canonical_of_same_rank_ne, HDiv.hDiv, HSub.hSub
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.high_signature_count_forced_after_supersets_normalized line 1523 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Usa2024P2.SignatureCountCondition, LT.lt, OfNat.ofNat, Usa2024P2.topSignature, LE.le, Finset.card, Fin, Eq, Usa2024P2.canonicalHighCount, And, Dvd.dvd, HSub.hSub
Proof uses: Finset.Nonempty, Iff.mp, Finset.card_pos, Usa2024P2.strictSupersetContribution, Usa2024P2.strictSupersetContribution_eq_canonical_of_strict, HAdd.hAdd, Usa2024P2.SignatureIntersectionCount, Eq.mp, congrArg, Usa2024P2.SignatureIntersectionCount_eq_self_add_strict, Usa2024P2.canonicalHighCount_valid_on_high, Nat.ModEq, Usa2024P2.modEq_self_of_split_divisibilities, dite, Eq.mpr, HMod.hMod, id, congr, Usa2024P2.topSignature_card, Eq.trans and 21 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.normalizeSignature_spec line 1576 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Usa2024P2.SignatureCountCondition, LT.lt, OfNat.ofNat, Usa2024P2.topSignature, LE.le, Finset.card, Fin, Eq, Usa2024P2.canonicalHighCount, And, Usa2024P2.normalizeSignature, Usa2024P2.SignatureObjective
Proof uses: Dvd.dvd, HSub.hSub, Usa2024P2.high_signature_count_forced_after_supersets_normalized, id, Usa2024P2.pushDown_to_canonical_count
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.normalizeSignature_top_pos line 1588 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, LT.lt, OfNat.ofNat, Usa2024P2.topSignature, Eq, Usa2024P2.normalizeSignature, Usa2024P2.canonicalHighCount
Proof uses: dite, Fin, Eq.mpr, id, congrArg, Usa2024P2.canonicalHighCount_top, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Eq.symm, Not, Finset.card, Usa2024P2.card_lt_100_of_ne_topSignature, Usa2024P2.normalizeSignature_eq_self_of_card_gt
13 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.normalize_rank_subset Normalize a finite subset of one rank line 1602 source
Source documentation
Normalize a finite subset of one rank.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2024P2.Signature, LE.le, OfNat.ofNat, Membership.mem, Eq, Finset.card, Fin, Usa2024P2.SignatureCountCondition, LT.lt, Usa2024P2.topSignature, Usa2024P2.canonicalHighCount, Exists, And, Usa2024P2.SignatureObjective
Proof uses: Finset.induction_on, EmptyCollection.emptyCollection, Exists.intro, And.intro, le_rfl, False.elim, Eq.mp, False, Not, Insert.insert, of_eq_true, Eq.trans, Or, True, congrArg, eq_true, or_true, congr, eq_self, eq_false and 14 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
lemma normalize_rank_subset
    (k : ℕ) (A : Finset Signature) (f : Signature → ℕ)
    (hk : 50 ≤ k)
    (hA : ∀ v : Signature, v ∈ A → v.card = k)
    (hf : SignatureCountCondition f)
    (htop : 0 < f topSignature)
    (hgt : ∀ w : Signature, k < w.card → f w = canonicalHighCount w) :
    ∃ g : Signature → ℕ,
      SignatureCountCondition g ∧
      SignatureObjective g ≤ SignatureObjective f ∧
      0 < g topSignature ∧
      (∀ w : Signature, k < w.card → g w = canonicalHighCount w) ∧
…
```
Mentions: Usa2024P2.Signature, f, Usa2024P2.SignatureCountCondition, Usa2024P2.topSignature, Usa2024P2.canonicalHighCount, Usa2024P2.SignatureObjective
lemma Usa2024P2.normalize_rank Normalize all signatures of one rank line 1653 source
Source documentation
Normalize all signatures of one rank.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P2.Signature, LE.le, OfNat.ofNat, Usa2024P2.SignatureCountCondition, LT.lt, Usa2024P2.topSignature, Finset.card, Fin, Eq, Usa2024P2.canonicalHighCount, Exists, And, Usa2024P2.SignatureObjective
Proof uses: Membership.mem, Finset, Usa2024P2.rankSignatures, Usa2024P2.normalize_rank_subset, Iff.mp, Usa2024P2.mem_rankSignatures, Exists.intro, And.intro, dite, Not, Iff.mpr
12 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma normalize_rank
    (k : ℕ) (f : Signature → ℕ)
    (hk : 50 ≤ k)
    (hf : SignatureCountCondition f)
    (htop : 0 < f topSignature)
    (hgt : ∀ w : Signature, k < w.card → f w = canonicalHighCount w) :
    ∃ g : Signature → ℕ,
      SignatureCountCondition g ∧
      SignatureObjective g ≤ SignatureObjective f ∧
      0 < g topSignature ∧
      (∀ w : Signature, k ≤ w.card → g w = canonicalHighCount w) := by
…
```
Mentions: f, Usa2024P2.Signature, Usa2024P2.SignatureCountCondition, Usa2024P2.topSignature, Usa2024P2.canonicalHighCount, Usa2024P2.SignatureObjective
lemma Usa2024P2.smooth_high_signatures_from_rank line 1674 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Usa2024P2.Signature, Usa2024P2.SignatureCountCondition, LT.lt, Usa2024P2.topSignature, Finset.card, Fin, Eq, Usa2024P2.canonicalHighCount, Exists, And, Usa2024P2.SignatureObjective
Proof uses: Nat.le_induction, Exists.intro, And.intro, le_rfl, HAdd.hAdd, Usa2024P2.normalize_rank, le_trans
15 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.smooth_high_signatures_by_ranks Normalize high ranks from 100 down to 50 line 1701 source
Source documentation
Normalize high ranks from 100 down to 50.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Usa2024P2.SignatureCountCondition, LT.lt, OfNat.ofNat, Usa2024P2.topSignature, Exists, And, LE.le, Usa2024P2.SignatureObjective, Finset.card, Fin, Eq, Usa2024P2.canonicalHighCount
Proof uses: card_finset_fin_le, Usa2024P2.smooth_high_signatures_from_rank, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true
12 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma smooth_high_signatures_by_ranks
    (f : Signature → ℕ)
    (hf : SignatureCountCondition f) (htop : 0 < f topSignature) :
    ∃ g : Signature → ℕ,
      SignatureCountCondition g ∧
      SignatureObjective g ≤ SignatureObjective f ∧
      0 < g topSignature ∧
      (∀ v : Signature, 50 ≤ v.card → g v = canonicalHighCount v) := by
…
```
Mentions: f, Usa2024P2.Signature, Usa2024P2.SignatureCountCondition, Usa2024P2.topSignature, Usa2024P2.SignatureObjective, Usa2024P2.canonicalHighCount
lemma Usa2024P2.smooth_high_signatures_to_canonical line 1715 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Usa2024P2.SignatureCountCondition, LT.lt, OfNat.ofNat, Usa2024P2.topSignature, Exists, And, LE.le, Usa2024P2.SignatureObjective, Finset.card, Fin, Eq, Usa2024P2.canonicalHighCount
Proof uses: Usa2024P2.smooth_high_signatures_by_ranks, Exists.intro, And.intro
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2024P2.signature_model_lower_bound Smoothing gives the signature-model lower bound line 1727 source
Source documentation
Smoothing gives the signature-model lower bound.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P2.Signature, Nat, Usa2024P2.SignatureCountCondition, LT.lt, OfNat.ofNat, Usa2024P2.topSignature, LE.le, Usa2024P2.solution, Usa2024P2.SignatureObjective
Proof uses: And, Finset.card, Fin, Eq, Usa2024P2.canonicalHighCount, Exists, Usa2024P2.smooth_high_signatures_to_canonical, Eq.mpr, Finset.sum, Finset.univ, ite, id, congrArg, Usa2024P2.SignatureObjective.eq_1, Finset.sum_congr, rfl, Finset, Membership.mem, ite_congr, Not and 3 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma signature_model_lower_bound
    (f : Signature → ℕ)
    (hf : SignatureCountCondition f) (htop : 0 < f topSignature) :
    solution ≤ SignatureObjective f := by
…
```
Mentions: f, Usa2024P2.Signature, Usa2024P2.SignatureCountCondition, Usa2024P2.topSignature, Usa2024P2.solution, Usa2024P2.SignatureObjective
lemma Usa2024P2.construction_attains_solution The signature construction realizes the claimed value line 1742 source
Source documentation
The signature construction realizes the claimed value.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Fin, OfNat.ofNat, Nat, Set, Int, And, Usa2024P2.Good, Eq, Usa2024P2.solution, Set.ncard, Set.ofPred, Usa2024P2.InAtLeastKSubsets
Proof uses: Usa2024P2.Signature, Usa2024P2.SignatureCountCondition, LT.lt, Usa2024P2.topSignature, LE.le, Finset.card, Usa2024P2.canonicalHighCount, Usa2024P2.SignatureObjective, Usa2024P2.extend_canonical_high_counts, Usa2024P2.realize_signature_counts, Exists.intro, And.intro, Eq.mpr, id, congrArg, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma construction_attains_solution :
    ∃ S, Good S ∧
      solution = {z : ℤ | InAtLeastKSubsets S 50 z }.ncard := by
…
```
Mentions: S, Usa2024P2.Good, Usa2024P2.solution, Usa2024P2.InAtLeastKSubsets
lemma Usa2024P2.at_least_solution_elements Lower bound for any good family line 1751 source
Source documentation
Lower bound for any good family.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Set, Int, Usa2024P2.Good, LE.le, Usa2024P2.solution, Set.ncard, Set.ofPred, Usa2024P2.InAtLeastKSubsets
Proof uses: Eq.mpr, Usa2024P2.SignatureObjective, Usa2024P2.signatureCount, id, Eq, congrArg, Eq.symm, Usa2024P2.signatureObjective_eq_original_objective, Usa2024P2.signature_model_lower_bound, Usa2024P2.signatureCount_condition_of_good, Usa2024P2.signatureCount_top_pos_of_good
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma at_least_solution_elements (S : Fin 100 → Set ℤ) (hS : Good S) :
    solution ≤ {z : ℤ | InAtLeastKSubsets S 50 z }.ncard := by
…
```
Mentions: S, Usa2024P2.Good, Usa2024P2.solution, Usa2024P2.InAtLeastKSubsets
problem Usa2024P2.usa2024_p2 line 1761 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Exists, Fin, OfNat.ofNat, Set, Int, And, Usa2024P2.Good, Eq, Set.ncard, Usa2024P2.InAtLeastKSubsets, Usa2024P2.solution
Proof uses: And.intro, Membership.mem, lowerBounds, Usa2024P2.construction_attains_solution, LE.le, Eq.mpr, id, congrArg, Usa2024P2.at_least_solution_elements
7 instances, coercions and auxiliary constants left out.

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