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

22 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2021, Problem 4

A finite set S of positive integers has the property that, for each s ∈ S, and each positive integer divisor d of s, there exists a unique element t ∈ S satisfying gcd(s, t) = d. (The elements s and t could be equal.)

Given this information, find all possible values for the number of elements of S.

Imports (4)

Imported by 1 file

Compfiles.lean

def Usa2021P4.IsValid Documented declaration: IsValid line 33 source
Source documentation
The property from the problem statement: S is a finite set of positive integers such that for every s ∈ S and every positive divisor d of s there exists a unique t ∈ S with Nat.gcd s t = d.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: And, Membership.mem, LT.lt, OfNat.ofNat, Dvd.dvd, ExistsUnique, Eq, Nat.gcd
5 instances, coercions and auxiliary constants left out.
```
def IsValid (S : Finset ℕ) : Prop :=
…
```
Mentions: S
determine Usa2021P4.solution_set line 36 source
standard axioms: propext what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, Or, Eq, OfNat.ofNat, Exists, HPow.hPow
5 instances, coercions and auxiliary constants left out.
theorem Usa2021P4.card_eq_card_divisors For s ∈ S, the map t ↦ Nat.gcd s t is a bijection from S onto the divisors of s; in particular #S = τ(s) line 42 source
Source documentation
For s ∈ S, the map t ↦ Nat.gcd s t is a bijection from S onto the divisors of s; in particular #S = τ(s).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Usa2021P4.IsValid, Membership.mem, Eq, Finset.card, Nat.divisors
Proof uses: LT.lt, OfNat.ofNat, Dvd.dvd, ExistsUnique, And, Nat.gcd, Ne, LT.lt.ne', Finset.card_bij, Iff.mpr, Nat.mem_divisors, And.intro, Nat.gcd_dvd_left, Nat.gcd_pos_of_pos_left, Eq.trans, rfl, Eq.symm, Exists, Iff.mp, Nat.pos_of_mem_divisors and 1 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem card_eq_card_divisors {S : Finset ℕ} (hS : IsValid S) {s : ℕ} (hs : s ∈ S) :
    S.card = s.divisors.card := by
…
```
Mentions: S, Usa2021P4.IsValid
theorem Usa2021P4.card_filter_dvd The same bijection identifies the elements of S divisible by p with the divisors of s divisible by p (for p ∣ s) line 60 source
Source documentation
The same bijection identifies the elements of S divisible by p with the divisors of s divisible by p (for p ∣ s).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Usa2021P4.IsValid, Membership.mem, Dvd.dvd, Eq, Finset.card, Finset.filter, Nat.divisors
Proof uses: LT.lt, OfNat.ofNat, ExistsUnique, And, Nat.gcd, Ne, LT.lt.ne', Finset.card_bij, Iff.mp, Finset.mem_filter, Iff.mpr, And.intro, Nat.mem_divisors, Nat.gcd_dvd_left, Nat.dvd_gcd, Nat.gcd_pos_of_pos_left, Eq.trans, rfl, Eq.symm, Exists and 6 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
theorem card_filter_dvd {S : Finset ℕ} (hS : IsValid S) {s : ℕ} (hs : s ∈ S) {p : ℕ}
    (hps : p ∣ s) :
    (S.filter (fun t => p ∣ t)).card = (s.divisors.filter (fun d => p ∣ d)).card := by
…
```
Mentions: S, Usa2021P4.IsValid
theorem Usa2021P4.card_divisors_filter_dvd The divisors of s divisible by a prime p ∣ s are in bijection (via d ↦ d / p) with the divisors of s / p line 87 source
Source documentation
The divisors of s divisible by a prime p ∣ s are in bijection (via d ↦ d / p) with the divisors of s / p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Ne, OfNat.ofNat, Dvd.dvd, Eq, Finset.card, Finset.filter, Nat.divisors, HDiv.hDiv
Proof uses: LT.lt.ne', Nat.div_pos, Nat.le_of_dvd, Iff.mpr, LT.lt, Nat.pos_iff_ne_zero, Nat.Prime.pos, Finset.card_bij, Membership.mem, Finset, And, Iff.mp, Finset.mem_filter, Nat.mem_divisors, HMul.hMul, Eq.mpr, id, congrArg, Nat.mul_div_cancel_left, And.intro and 7 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
theorem card_divisors_filter_dvd {s p : ℕ} (hp : p.Prime) (hs0 : s ≠ 0) (hps : p ∣ s) :
    (s.divisors.filter (fun d => p ∣ d)).card = (s / p).divisors.card := by
…
```
theorem Usa2021P4.card_divisors_div_mul The ratio identity for the divisor counting function: if p ∣ s is prime and e = νₚ(s), then (e + 1) * τ(s / p) = e * τ(s) line 117 source
Source documentation
The ratio identity for the divisor counting function: if p ∣ s is prime and e = νₚ(s), then (e + 1) * τ(s / p) = e * τ(s).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Ne, OfNat.ofNat, Dvd.dvd, Eq, HMul.hMul, HAdd.hAdd, Finsupp, Nat.factorization, Finset.card, Nat.divisors, HDiv.hDiv
Proof uses: Eq.mpr, id, congrArg, rfl, LE.le, Nat.Prime.factorization_pos_of_dvd, HPow.hPow, Iff.mpr, Nat.Prime.pow_dvd_iff_le_factorization, le_rfl, Eq.symm, Nat.mul_div_cancel', Not, Nat.not_dvd_ordCompl, Nat.Coprime, Nat.Coprime.symm, Nat.Prime.coprime_pow_of_not_dvd, Nat.Coprime.card_divisors_mul, Finset.map, Function.Embedding.mk and 43 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
theorem card_divisors_div_mul {s p : ℕ} (hp : p.Prime) (hs0 : s ≠ 0) (hps : p ∣ s) :
    (s.factorization p + 1) * (s / p).divisors.card = s.factorization p * s.divisors.card := by
…
```
theorem Usa2021P4.factorization_le_one The key claim: in a valid set every element is squarefree, i.e. every prime appears with exponent at most one line 146 source
Source documentation
The key claim: in a valid set every element is squarefree, i.e. every prime appears with exponent at most one. Otherwise the density of multiples of p in S would have to equal both e / (e + 1) and 1 / 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Usa2021P4.IsValid, Membership.mem, Nat.Prime, LE.le, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: LT.lt, And.left, Dvd.dvd, ExistsUnique, And, Eq, Nat.gcd, And.right, Ne, LT.lt.ne', Decidable.byContradiction, Not, lt_of_not_ge, rfl, HPow.hPow, Iff.mpr, Nat.Prime.pow_dvd_iff_le_factorization, Eq.mp, congrArg, pow_one and 46 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
```
theorem factorization_le_one {S : Finset ℕ} (hS : IsValid S) {x : ℕ} (hx : x ∈ S) {p : ℕ}
    (hp : p.Prime) :
    x.factorization p ≤ 1 := by
…
```
Mentions: S, Usa2021P4.IsValid
theorem Usa2021P4.card_eq_two_pow Any valid nonempty set has cardinality a power of two: #S = τ(x) = 2^{ω(x)} for any x ∈ S line 207 source
Source documentation
Any valid nonempty set has cardinality a power of two: #S = τ(x) = 2^{ω(x)} for any x ∈ S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Usa2021P4.IsValid, Finset.Nonempty, Exists, Eq, Finset.card, HPow.hPow, OfNat.ofNat
Proof uses: Membership.mem, LT.lt, And.left, Dvd.dvd, ExistsUnique, And, Nat.gcd, Ne, LT.lt.ne', Exists.intro, Nat.primeFactors, Eq.mpr, Nat.divisors, id, congrArg, Usa2021P4.card_eq_card_divisors, Finset.prod, HAdd.hAdd, Finsupp, Nat.factorization and 13 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem card_eq_two_pow {S : Finset ℕ} (hS : IsValid S) (hne : S.Nonempty) :
    ∃ k : ℕ, S.card = 2 ^ k := by
…
```
Mentions: S, Usa2021P4.IsValid
def Usa2021P4.constr_r The 2k primes used in the construction: in slot i, the "true" choice is the (2 * i)-th prime and the "false" choice is the (2 * i + 1)-th prime line 225 source
Source documentation
The 2k primes used in the construction: in slot i, the "true" choice is the (2 * i)-th prime and the "false" choice is the (2 * i + 1)-th prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool
Proof uses: ite, Eq, Bool.true, Nat.nth, Nat.Prime, HMul.hMul, OfNat.ofNat, HAdd.hAdd
7 instances, coercions and auxiliary constants left out.
```
noncomputable def constr_r (k : ℕ) (b : Fin k → Bool) (i : Fin k) : ℕ :=
…
```
def Usa2021P4.constr_b' The flipped choice function: keep b i exactly when the i-th prime divides d line 229 source
Source documentation
The flipped choice function: keep b i exactly when the i-th prime divides d.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool
Proof uses: ite, Dvd.dvd, Usa2021P4.constr_r, Bool.not
2 instances, coercions and auxiliary constants left out.
```
noncomputable def constr_b' (k : ℕ) (b : Fin k → Bool) (d : ℕ) : Fin k → Bool :=
…
```
theorem Usa2021P4.constr_r_prime Every value of constr_r is prime line 233 source
Source documentation
Every value of constr_r is prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Nat.Prime, Usa2021P4.constr_r
Proof uses: id, Eq, Bool.true, Decidable, ite, Nat.nth, HMul.hMul, OfNat.ofNat, HAdd.hAdd, Not, Eq.mpr, congrArg, ite_eq_right, Nat.nth_mem_of_infinite, Nat.infinite_setOfPred_prime, ite_eq_left
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem constr_r_prime {k : ℕ} (b : Fin k → Bool) (i : Fin k) : Nat.Prime (constr_r k b i) := by
…
```
Mentions: Usa2021P4.constr_r
theorem Usa2021P4.constr_r_inj The primes in different slots are distinct: constr_r k b₁ i = constr_r k b₂ j forces i = j line 239 source
Source documentation
The primes in different slots are distinct: constr_r k b₁ i = constr_r k b₂ j forces i = j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa2021P4.constr_r
Proof uses: Function.Injective, Nat.nth, Nat.Prime, Nat.nth_injective, Nat.infinite_setOfPred_prime, Bool.true, Decidable, Not, Fin.ext, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Eq.mp, ite, congrArg, ite_eq_right, congrFun', absurd, ite_eq_left
12 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem constr_r_inj {k : ℕ} {b₁ b₂ : Fin k → Bool} {i j : Fin k}
    (h : constr_r k b₁ i = constr_r k b₂ j) : i = j := by
…
```
Mentions: h, Usa2021P4.constr_r
theorem Usa2021P4.constr_r_inj_bool Equal primes in the same slot force equal Booleans line 250 source
Source documentation
Equal primes in the same slot force equal Booleans.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa2021P4.constr_r
Proof uses: Function.Injective, Nat.nth, Nat.Prime, Nat.nth_injective, Nat.infinite_setOfPred_prime, Bool.true, Decidable, Not, Eq.mpr, Bool.false, id, congrArg, Eq.mp, Bool.not_eq_true, Eq.refl, absurd, HAdd.hAdd, HMul.hMul, OfNat.ofNat, ite and 3 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem constr_r_inj_bool {k : ℕ} {b₁ b₂ : Fin k → Bool} {i : Fin k}
    (h : constr_r k b₁ i = constr_r k b₂ i) : b₁ i = b₂ i := by
…
```
Mentions: h, Usa2021P4.constr_r
theorem Usa2021P4.constr_bool_not_ne No Boolean equals its own negation line 264 source
Source documentation
No Boolean equals its own negation.

standard axioms: propext what this means
Statement uses: Bool, Ne, Bool.not
Proof uses: Eq, Bool.false, of_eq_true, Eq.trans, Bool.true, True, congrFun', congrArg, Bool.not_false, Not, False, Bool.true_eq_false, not_false_eq_true, Eq.symm, Bool.not_true, Bool.false_eq_true, Eq.refl
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem constr_bool_not_ne (c : Bool) : (!c) ≠ c := by
…
```
theorem Usa2021P4.constr_prod_inj The product map b ↦ ∏ i, constr_r k b i is injective line 268 source
Source documentation
The product map b ↦ ∏ i, constr_r k b i is injective.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Finset.prod, Finset.univ, Usa2021P4.constr_r
Proof uses: funext, Usa2021P4.constr_r_inj_bool, Dvd.dvd, Eq.mpr, id, congrArg, Eq.symm, Finset.dvd_prod_of_mem, Finset.mem_univ, And, Membership.mem, Finset, Exists, Iff.mp, Prime.dvd_finsetProd_iff, Nat.Prime.prime, Usa2021P4.constr_r_prime, Nat.prime_dvd_prime_iff_eq, Usa2021P4.constr_r_inj
16 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem constr_prod_inj {k : ℕ} {b₁ b₂ : Fin k → Bool}
    (h : (∏ i : Fin k, constr_r k b₁ i) = ∏ i : Fin k, constr_r k b₂ i) : b₁ = b₂ := by
…
```
Mentions: h, Usa2021P4.constr_r
theorem Usa2021P4.constr_r_flip The flipped prime equals the original one exactly when the original divides d line 282 source
Source documentation
The flipped prime equals the original one exactly when the original divides d.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Iff, Eq, Usa2021P4.constr_r, Usa2021P4.constr_b', Dvd.dvd
Proof uses: Iff.intro, Decidable.byContradiction, Not, Bool.not, ite_eq_right, Usa2021P4.constr_r_inj_bool, Usa2021P4.constr_bool_not_ne, Eq.mp, congrArg, ite_eq_left, id, Eq.mpr, ite, Bool.true, Nat.nth, Nat.Prime, HMul.hMul, OfNat.ofNat, HAdd.hAdd, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem constr_r_flip {k : ℕ} {b : Fin k → Bool} {d : ℕ} {i : Fin k} :
    constr_r k (constr_b' k b d) i = constr_r k b i ↔ constr_r k b i ∣ d := by
…
```
Mentions: Usa2021P4.constr_r, Usa2021P4.constr_b'
theorem Usa2021P4.constr_prod_dvd_of_forall If every slot prime in J divides d, then so does their product line 297 source
Source documentation
If every slot prime in J divides d, then so does their product.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset, Membership.mem, Dvd.dvd, Usa2021P4.constr_r, Finset.prod
Proof uses: Finset.induction_on, of_eq_true, EmptyCollection.emptyCollection, OfNat.ofNat, Eq.trans, True, implies_congr, forall_congr, False, Eq.refl, implies_true, IsUnit, Eq, Units, eq_self, Not, Insert.insert, Eq.mpr, HMul.hMul, id and 12 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem constr_prod_dvd_of_forall {k : ℕ} {b : Fin k → Bool} {d : ℕ}
    {J : Finset (Fin k)} (hJ : ∀ i ∈ J, constr_r k b i ∣ d) :
    (∏ i ∈ J, constr_r k b i) ∣ d := by
…
```
Mentions: Usa2021P4.constr_r
theorem Usa2021P4.constr_dvd_eq_prod_filter Support representation: a divisor of the full product is the product over the slots whose primes divide it line 315 source
Source documentation
Support representation: a divisor of the full product is the product over the slots whose primes divide it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Dvd.dvd, Finset.prod, Finset.univ, Usa2021P4.constr_r, Eq, Finset.filter
Proof uses: Nat.dvd_antisymm, Nat.Coprime, Not, Nat.Coprime.prod_right, Membership.mem, Finset, Nat.Coprime.symm, Iff.mpr, Nat.Prime.coprime_iff_not_dvd, Usa2021P4.constr_r_prime, And.right, Iff.mp, And, Finset.mem_filter, HMul.hMul, Eq.mpr, id, congrArg, Finset.prod_filter_not_mul_prod_filter, Nat.Coprime.dvd_of_dvd_mul_left and 1 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem constr_dvd_eq_prod_filter {k : ℕ} {b : Fin k → Bool} {d : ℕ}
    (hd : d ∣ ∏ i : Fin k, constr_r k b i) :
    d = ∏ i ∈ Finset.univ.filter (fun i => constr_r k b i ∣ d), constr_r k b i := by
…
```
Mentions: Usa2021P4.constr_r
theorem Usa2021P4.constr_gcd The gcd of the full product with the flipped product is exactly d line 332 source
Source documentation
The gcd of the full product with the flipped product is exactly d.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Dvd.dvd, Finset.prod, Finset.univ, Usa2021P4.constr_r, Eq, Nat.gcd, Usa2021P4.constr_b'
Proof uses: Finset.filter, Usa2021P4.constr_dvd_eq_prod_filter, Nat.gcd_dvd_left, Nat.dvd_antisymm, Eq.mpr, id, congrArg, dvd_trans, Finset.prod_dvd_prod_of_subset, Membership.mem, Finset, And, Iff.mp, Finset.mem_filter, Iff.mpr, And.intro, Finset.mem_univ, Nat.gcd_dvd_right, Exists, Prime.dvd_finsetProd_iff and 13 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem constr_gcd {k : ℕ} {b : Fin k → Bool} {d : ℕ}
    (hds : d ∣ ∏ i : Fin k, constr_r k b i) :
    Nat.gcd (∏ i : Fin k, constr_r k b i) (∏ i : Fin k, constr_r k (constr_b' k b d) i) = d := by
…
```
Mentions: Usa2021P4.constr_r, Usa2021P4.constr_b'
theorem Usa2021P4.constr_gcd_unique Uniqueness: any product of slot primes having gcd d with the full product must be the flipped product line 362 source
Source documentation
Uniqueness: any product of slot primes having gcd d with the full product must be the flipped product.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Nat.gcd, Finset.prod, Finset.univ, Usa2021P4.constr_r, Usa2021P4.constr_b'
Proof uses: Iff, Dvd.dvd, Iff.intro, And, Membership.mem, Finset, Exists, Iff.mp, Prime.dvd_finsetProd_iff, Nat.Prime.prime, Usa2021P4.constr_r_prime, Nat.prime_dvd_prime_iff_eq, Eq.symm, Usa2021P4.constr_r_inj_bool, Usa2021P4.constr_r_inj, id, Eq.mpr, ite, Bool.true, Nat.nth and 37 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
theorem constr_gcd_unique {k : ℕ} {b b'' : Fin k → Bool} {d : ℕ}
    (h : Nat.gcd (∏ i : Fin k, constr_r k b i) (∏ i : Fin k, constr_r k b'' i) = d) :
    (∏ i : Fin k, constr_r k b'' i) = ∏ i : Fin k, constr_r k (constr_b' k b d) i := by
…
```
Mentions: h, Usa2021P4.constr_r, Usa2021P4.constr_b'
theorem Usa2021P4.exists_isValid Construction: for 2k distinct primes p₁, q₁, …, pₖ, qₖ, the set of all products r₁ * … * rₖ with rᵢ ∈ {pᵢ, qᵢ} is valid and has cardinality 2ᵏ line 399 source
Source documentation
Construction: for 2k distinct primes p₁, q₁, …, pₖ, qₖ, the set of all products r₁ * … * rₖ with rᵢ ∈ {pᵢ, qᵢ} is valid and has cardinality 2ᵏ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, Finset, And, Usa2021P4.IsValid, Finset.Nonempty, Eq, Finset.card, HPow.hPow, OfNat.ofNat
Proof uses: Exists.intro, Finset.image, Fin, Bool, Finset.prod, Finset.univ, Usa2021P4.constr_r, And.intro, Membership.mem, LT.lt, Dvd.dvd, ExistsUnique, Nat.gcd, Iff.mp, Finset.mem_image, Finset.prod_pos, Nat.Prime.pos, Usa2021P4.constr_r_prime, Usa2021P4.constr_b', Iff.mpr and 18 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
theorem exists_isValid (k : ℕ) : ∃ S : Finset ℕ, IsValid S ∧ S.Nonempty ∧ S.card = 2 ^ k := by
…
```
Mentions: S, Usa2021P4.IsValid
problem Usa2021P4.usa2021_p4 line 423 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Membership.mem, Set, Usa2021P4.solution_set, Exists, Finset, And, Usa2021P4.IsValid, Eq, Finset.card
Proof uses: id, Iff.intro, Or, OfNat.ofNat, HPow.hPow, Exists.intro, EmptyCollection.emptyCollection, And.intro, LT.lt, Dvd.dvd, ExistsUnique, Nat.gcd, of_eq_true, Eq.trans, True, forall_congr, False, implies_congr, Eq.refl, implies_true and 13 more
21 instances, coercions and auxiliary constants left out.

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