`Compfiles/Usa2020P5.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 2020, Problem 5

A finite set S of points in the coordinate plane is called overdetermined if |S| ≥ 2 and there exists a nonzero polynomial P(t), with real coefficients and of degree at most |S| − 2, satisfying P(x) = y for every point (x, y) ∈ S.

For each integer n ≥ 2, find the largest integer k (in terms of n) such that there exists a set of n distinct points that is not overdetermined, but has k overdetermined subsets.

Imports (3)

Imported by 1 file

Compfiles.lean

def Usa2020P5.Overdetermined Documented declaration: Overdetermined line 36 source
Source documentation
A finite set of points in the coordinate plane is overdetermined if it has at least two elements and some nonzero real polynomial of degree at most |S| - 2 passes through every point of S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Real
Proof uses: And, LE.le, Nat, OfNat.ofNat, Finset.card, Exists, Polynomial, Ne, Polynomial.natDegree, HSub.hSub, Membership.mem, Eq, Polynomial.eval, Prod.fst, Prod.snd
9 instances, coercions and auxiliary constants left out.
```
def Overdetermined (S : Finset (ℝ × ℝ)) : Prop :=
…
```
Mentions: S
determine Usa2020P5.solution line 39 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HSub.hSub, HPow.hPow, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
lemma Usa2020P5.two_pow_ge_succ k + 1 ≤ 2 ^ k for every natural number k line 56 source
Source documentation
k + 1 ≤ 2 ^ k for every natural number k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, OfNat.ofNat, HPow.hPow
Proof uses: Nat.recAux, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, HMul.hMul, congrArg, pow_succ
22 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma two_pow_ge_succ (k : ℕ) : k + 1 ≤ 2 ^ k := by
…
```
lemma Usa2020P5.roots_card_bound A nonzero polynomial that vanishes on every element of a finite set of reals has degree at least the cardinality of that set line 65 source
Source documentation
A nonzero polynomial that vanishes on every element of a finite set of reals has degree at least the cardinality of that set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Real, Ne, OfNat.ofNat, Finset, Membership.mem, Eq, Polynomial.eval, LE.le, Nat, Finset.card, Polynomial.natDegree
Proof uses: Multiset.toFinset, Polynomial.roots, Eq.mpr, Multiset, id, congrArg, propext, Multiset.mem_toFinset, Polynomial.IsRoot, Polynomial.mem_roots, Polynomial.IsRoot.def, LE.le.trans, Finset.card_le_card, Multiset.card, Multiset.toFinset_card_le, Polynomial.card_roots'
25 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma roots_card_bound {P : ℝ[X]} (hP : P ≠ 0) {X : Finset ℝ}
    (hX : ∀ x ∈ X, P.eval x = 0) : X.card ≤ P.natDegree := by
…
```
Mentions: P
lemma Usa2020P5.poly_unique Documented declaration: poly_unique line 77 source
Source documentation
Uniqueness of low-degree interpolating polynomials: two real polynomials of degree at most |T| - 1 that both pass through every point of a nonempty finite set T of points in the plane are equal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Real, Finset.Nonempty, Polynomial, LE.le, Nat, Polynomial.natDegree, HSub.hSub, Finset.card, OfNat.ofNat, Membership.mem, Eq, Polynomial.eval, Prod.fst, Prod.snd
Proof uses: Decidable.byContradiction, Not, Ne, Iff.mpr, sub_ne_zero, Finset.image, And, Exists, Iff.mp, Finset.mem_image, Eq.mpr, id, congrArg, Polynomial.eval_sub, sub_self, Eq.refl, Usa2020P5.roots_card_bound, LE.le.trans, Max.max, Polynomial.natDegree_sub_le and 7 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma poly_unique {T : Finset (ℝ × ℝ)} (hT : T.Nonempty) {f g : ℝ[X]}
    (hf : f.natDegree ≤ T.card - 1) (hg : g.natDegree ≤ T.card - 1)
    (hfT : ∀ p ∈ T, f.eval p.1 = p.2) (hgT : ∀ p ∈ T, g.eval p.1 = p.2) :
    f = g := by
…
```
Mentions: f
lemma Usa2020P5.eq_of_overdetermined_of_flooded A flooded (i.e. not overdetermined) set of m + 2 points has at most one overdetermined subset of size m + 1 line 99 source
Source documentation
A flooded (i.e. not overdetermined) set of m + 2 points has at most one overdetermined subset of size m + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Real, Not, Usa2020P5.Overdetermined, Nat, Eq, Finset.card, HAdd.hAdd, OfNat.ofNat, LE.le
Proof uses: Exists, Polynomial, And, Ne, Polynomial.natDegree, HSub.hSub, Membership.mem, Polynomial.eval, Prod.fst, Prod.snd, SDiff.sdiff, Finset.card_sdiff_of_subset, Singleton.singleton, Iff.mp, Finset.card_eq_one, Eq.mpr, id, congrArg, Finset.mem_singleton_self, And.left and 31 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 83 steps
Open to load the checked before-and-after goal states.
```
lemma eq_of_overdetermined_of_flooded {S : Finset (ℝ × ℝ)} (hS : ¬ Overdetermined S)
    {m : ℕ} (hcard : S.card = m + 2) {U₁ U₂ : Finset (ℝ × ℝ)}
    (hU₁ : U₁ ⊆ S) (hU₁c : U₁.card = m + 1) (hU₁o : Overdetermined U₁)
    (hU₂ : U₂ ⊆ S) (hU₂c : U₂.card = m + 1) (hU₂o : Overdetermined U₂) :
    U₁ = U₂ := by
…
```
Mentions: S, Usa2020P5.Overdetermined
lemma Usa2020P5.card_flooded_subsets A flooded set of t ≥ 3 points has at least t - 1 flooded subsets of size t - 1 line 177 source
Source documentation
A flooded set of t ≥ 3 points has at least t - 1 flooded subsets of size t - 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Real, Nat, LE.le, OfNat.ofNat, Eq, Finset.card, Not, Usa2020P5.Overdetermined, HSub.hSub, Finset.filter, Finset.powersetCard
Proof uses: Eq.mpr, Membership.mem, id, congrArg, propext, Finset.card_le_one, And, Eq.mp, Eq.trans, congrFun', Usa2020P5.eq_of_overdetermined_of_flooded, Nat.choose, Finset.card_powersetCard, Eq.symm, Nat.choose_symm, Nat.choose_one_right, Eq.refl, HAdd.hAdd, Finset.card_filter_add_card_filter_not
27 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma card_flooded_subsets {S : Finset (ℝ × ℝ)} {t : ℕ} (ht : 3 ≤ t)
    (hScard : S.card = t) (hS : ¬ Overdetermined S) :
    t - 1 ≤ ((S.powersetCard (t - 1)).filter (fun a => ¬ Overdetermined a)).card := by
…
```
Mentions: S, Usa2020P5.Overdetermined
lemma Usa2020P5.card_supersets A set U of m points of A is contained in at most A.card - m subsets of A of size m + 1 line 197 source
Source documentation
A set U of m points of A is contained in at most A.card - m subsets of A of size m + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Real, LE.le, Nat, Eq, Finset.card, Finset.filter, Finset.powersetCard, HAdd.hAdd, OfNat.ofNat, HSub.hSub
Proof uses: Set.InjOn, SDiff.sdiff, Membership.mem, Set, Trans.trans, Union.union, Eq.symm, Finset.union_sdiff_of_subset, And.right, And, Eq.mp, congrFun', Set.ofPred, congrArg, Eq.trans, Finset.coe_filter, funext, Eq.mpr, id, Eq.refl and 14 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma card_supersets {A U : Finset (ℝ × ℝ)} (hU : U ⊆ A) {m : ℕ} (hUm : U.card = m) :
    ((A.powersetCard (m + 1)).filter (fun T => U ⊆ T)).card ≤ A.card - m := by
…
```
lemma Usa2020P5.double_count Double counting of the incidence relation between flooded m-subsets and flooded (m+1)-subsets of A line 224 source
Source documentation
Double counting of the incidence relation between flooded m-subsets and flooded (m+1)-subsets of A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Real, Nat, LE.le, OfNat.ofNat, LT.lt, Finset.card, HMul.hMul, Finset.filter, Not, Usa2020P5.Overdetermined, Finset.powersetCard, HAdd.hAdd, HSub.hSub
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, Membership.mem, And, Eq.mp, Eq.trans, congrFun', propext, Finset.mem_filter, Finset.mem_powersetCard, And.intro, LE.le.trans, And.left, And.right, Usa2020P5.card_flooded_subsets, Finset.card_le_card, Finset.filter.congr_simp and 17 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
lemma double_count {A : Finset (ℝ × ℝ)} {m : ℕ} (hm : 2 ≤ m) (_hmn : m < A.card) :
    m * ((A.powersetCard (m + 1)).filter (fun a => ¬ Overdetermined a)).card ≤
    (A.card - m) * ((A.powersetCard m).filter (fun a => ¬ Overdetermined a)).card := by
…
```
Mentions: Usa2020P5.Overdetermined
lemma Usa2020P5.flooded_count A flooded set A has at least (A.card - 1).choose (m - 1) flooded subsets of size m, for every 2 ≤ m ≤ A.card line 270 source
Source documentation
A flooded set A has at least (A.card - 1).choose (m - 1) flooded subsets of size m, for every 2 ≤ m ≤ A.card.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Real, Not, Usa2020P5.Overdetermined, Nat, LE.le, OfNat.ofNat, Finset.card, Nat.choose, HSub.hSub, Finset.filter, Finset.powersetCard
Proof uses: Nat.decreasingInduction, LT.lt, HAdd.hAdd, HMul.hMul, Usa2020P5.double_count, Eq, Nat.choose_succ_right_eq, Eq.mpr, id, congrArg, mul_comm, Eq.mp, Trans.trans, Eq.symm, Nat.mul_le_mul, le_refl, congrFun', Nat.add_sub_cancel, Nat.le_of_mul_le_mul_left, Singleton.singleton and 14 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
lemma flooded_count {A : Finset (ℝ × ℝ)} (hA : ¬ Overdetermined A) :
    ∀ m, 2 ≤ m → m ≤ A.card → Nat.choose (A.card - 1) (m - 1) ≤
      ((A.powersetCard m).filter (fun a => ¬ Overdetermined a)).card := by
…
```
Mentions: Usa2020P5.Overdetermined
lemma Usa2020P5.sum_choose_Icc The sum of (n - 1).choose m over m ∈ Icc 2 n equals 2 ^ (n - 1) - n line 313 source
Source documentation
The sum of (n - 1).choose m over m ∈ Icc 2 n equals 2 ^ (n - 1) - n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Finset.sum, Finset.Icc, Nat.choose, HSub.hSub, HPow.hPow
Proof uses: HAdd.hAdd, Usa2020P5.two_pow_ge_succ, Finset.range, Nat.sum_range_choose, Eq.mp, congrArg, Nat.sub_add_cancel, Finset, Finset.image, Finset.ext, Eq.mpr, Iff, Membership.mem, And, Exists, LT.lt, id, congr, Eq.trans, funext and 21 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
```
lemma sum_choose_Icc {n : ℕ} (hn : 2 ≤ n) :
    ∑ m ∈ Finset.Icc 2 n, Nat.choose (n - 1) m = 2 ^ (n - 1) - n := by
…
```
lemma Usa2020P5.overdetermined_bound An n-element flooded set of points has at most 2 ^ (n - 1) - n overdetermined subsets line 361 source
Source documentation
An n-element flooded set of points has at most 2 ^ (n - 1) - n overdetermined subsets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Real, LE.le, Nat, OfNat.ofNat, Finset.card, Not, Usa2020P5.Overdetermined, Finset.filter, Finset.powerset, HSub.hSub, HPow.hPow
Proof uses: Eq, Finset.biUnion, Finset.Icc, Finset.powersetCard, Finset.ext, Eq.mpr, Iff, Membership.mem, And, Exists, id, congr, congrArg, Eq.trans, congrFun', funext, Iff.intro, Exists.intro, And.intro, And.left and 29 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma overdetermined_bound {A : Finset (ℝ × ℝ)} (h2 : 2 ≤ A.card) (hA : ¬ Overdetermined A) :
    (A.powerset.filter Overdetermined).card ≤ 2 ^ (A.card - 1) - A.card := by
…
```
Mentions: Usa2020P5.Overdetermined
lemma Usa2020P5.card_powerset_filter_two_le A finite set s has exactly 2 ^ s.card - s.card - 1 subsets of cardinality at least two line 401 source
Source documentation
A finite set s has exactly 2 ^ s.card - s.card - 1 subsets of cardinality at least two.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Eq, Nat, Finset.card, Finset.filter, LE.le, OfNat.ofNat, Finset.powerset, HSub.hSub, HPow.hPow
Proof uses: HAdd.hAdd, Usa2020P5.two_pow_ge_succ, Not, Finset.card_filter_add_card_filter_not, Eq.mpr, id, congrFun', congrArg, Finset.filter_congr, Membership.mem, Iff.of_eq, Eq.trans, LT.lt, Eq.mp, Finset.card_powerset, Union.union, Finset.powersetCard, Finset.ext, Iff, And and 17 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma card_powerset_filter_two_le {α : Type*} [DecidableEq α] (s : Finset α) :
    (s.powerset.filter (fun T => 2 ≤ T.card)).card = 2 ^ s.card - s.card - 1 := by
…
```
def Usa2020P5.tail The "tail" of the extremal construction: the points (i, 2) for 2 ≤ i ≤ n line 432 source
Source documentation
The "tail" of the extremal construction: the points (i, 2) for 2 ≤ i ≤ n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Real
Proof uses: Finset.image, Prod.mk, OfNat.ofNat, Finset.Icc
9 instances, coercions and auxiliary constants left out.
```
noncomputable def tail (n : ℕ) : Finset (ℝ × ℝ) :=
…
```
def Usa2020P5.constrSet The extremal construction: the points (1, 1) and (i, 2) for 2 ≤ i ≤ n line 436 source
Source documentation
The extremal construction: the points (1, 1) and (i, 2) for 2 ≤ i ≤ n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Real
Proof uses: Insert.insert, Prod.mk, OfNat.ofNat, Usa2020P5.tail
5 instances, coercions and auxiliary constants left out.
```
noncomputable def constrSet (n : ℕ) : Finset (ℝ × ℝ) :=
…
```
lemma Usa2020P5.card_tail line 439 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Real, Usa2020P5.tail, HSub.hSub, OfNat.ofNat
Proof uses: Set.InjOn, Prod.mk, Finset, Finset.Icc, Membership.mem, Set, congrArg, Prod.fst, Nat.cast_injective, Eq.mpr, Finset.image, id, Usa2020P5.tail.eq_1, Finset.card_image_of_injOn, HAdd.hAdd, Nat.card_Icc
31 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2020P5.one_one_not_mem_tail line 447 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Membership.mem, Prod, Real, Finset, Usa2020P5.tail, Prod.mk, OfNat.ofNat
Proof uses: Eq.mpr, Exists, And, LE.le, Eq, id, congrArg, Eq.trans, Finset.image, Finset.Icc, funext, congrFun', False, Prod.snd, False.elim, Eq.mp, eq_false, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 4 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2020P5.card_constrSet line 453 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Finset.card, Prod, Real, Usa2020P5.constrSet
Proof uses: Eq.mpr, Insert.insert, Finset, Prod.mk, Usa2020P5.tail, id, congrArg, Usa2020P5.constrSet.eq_1, HAdd.hAdd, Finset.card_insert_of_notMem, Usa2020P5.one_one_not_mem_tail, HSub.hSub, Usa2020P5.card_tail
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2020P5.not_overdetermined_constrSet line 457 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Not, Usa2020P5.Overdetermined, Usa2020P5.constrSet
Proof uses: Finset.card, Prod, Real, Exists, Polynomial, And, Ne, Polynomial.natDegree, HSub.hSub, Membership.mem, Finset, Eq, Polynomial.eval, Prod.fst, Prod.snd, False, Finset.image, Finset.Icc, RingHom, Polynomial.C and 41 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma Usa2020P5.overdetermined_subset_constrSet_iff The overdetermined subsets of the extremal construction are exactly the subsets of its tail with at least two elements line 488 source
Source documentation
The overdetermined subsets of the extremal construction are exactly the subsets of its tail with at least two elements.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Real, LE.le, Usa2020P5.constrSet, Iff, Usa2020P5.Overdetermined, And, Usa2020P5.tail, OfNat.ofNat, Finset.card
Proof uses: Iff.intro, Exists, Polynomial, Ne, Polynomial.natDegree, HSub.hSub, Membership.mem, Eq, Polynomial.eval, Prod.fst, Prod.snd, Not, Prod.mk, SDiff.sdiff, Singleton.singleton, And.left, Eq.mp, congrArg, propext, Finset.mem_singleton and 53 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 71 steps
Open to load the checked before-and-after goal states.
```
lemma overdetermined_subset_constrSet_iff {n : ℕ} {T : Finset (ℝ × ℝ)}
    (hT : T ⊆ constrSet n) : Overdetermined T ↔ T ⊆ tail n ∧ 2 ≤ T.card := by
…
```
Mentions: Usa2020P5.constrSet, Usa2020P5.Overdetermined, Usa2020P5.tail
lemma Usa2020P5.count_constrSet The extremal construction has exactly 2 ^ (n - 1) - n overdetermined subsets line 557 source
Source documentation
The extremal construction has exactly 2 ^ (n - 1) - n overdetermined subsets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Finset.card, Finset, Prod, Real, Finset.filter, Usa2020P5.Overdetermined, Finset.powerset, Usa2020P5.constrSet, HSub.hSub, HPow.hPow
Proof uses: Usa2020P5.tail, Finset.ext, Eq.mpr, Iff, Membership.mem, And, id, congr, congrArg, Eq.trans, congrFun', Iff.intro, Iff.mp, Usa2020P5.overdetermined_subset_constrSet_iff, Finset.mem_insert_of_mem, Prod.mk, And.intro, Iff.mpr, HAdd.hAdd, Usa2020P5.two_pow_ge_succ and 2 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma count_constrSet {n : ℕ} (hn : 2 ≤ n) :
    ((constrSet n).powerset.filter Overdetermined).card = 2 ^ (n - 1) - n := by
…
```
Mentions: Usa2020P5.constrSet, Usa2020P5.Overdetermined
problem Usa2020P5.usa2020_p5 line 577 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, IsGreatest, Set.ofPred, Exists, Finset, Prod, Real, And, Eq, Finset.card, Not, Usa2020P5.Overdetermined, Finset.filter, Finset.powerset, Usa2020P5.solution
Proof uses: And.intro, Membership.mem, Set, upperBounds, Exists.intro, Usa2020P5.constrSet, Usa2020P5.card_constrSet, Usa2020P5.not_overdetermined_constrSet, Usa2020P5.count_constrSet, Eq.mpr, id, congrArg, Eq.symm, HSub.hSub, HPow.hPow, Usa2020P5.overdetermined_bound, Eq.mp
16 instances, coercions and auxiliary constants left out.

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