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

23 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2019, Problem 4

Let n be a nonnegative integer. Determine the number of ways to choose sets Sᵢⱼ ⊆ {1, 2, ..., 2n}, for all 0 ≤ i ≤ n and 0 ≤ j ≤ n (not necessarily distinct), such that

• |Sᵢⱼ| = i + j, and • Sᵢⱼ ⊆ Sₖₗ if 0 ≤ i ≤ k ≤ n and 0 ≤ j ≤ l ≤ n.

Imports (5)

Imported by 1 file

Compfiles.lean

abbrev Usa2019P4.Cell The grid cells indexing the sets Sᵢⱼ line 37 source
Source documentation
The grid cells indexing the sets Sᵢⱼ.

no axioms what this means
Statement uses: Nat
Proof uses: Prod, Fin, HAdd.hAdd, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
abbrev Cell (n : ℕ) := Fin (n + 1) × Fin (n + 1)
```
def Usa2019P4.target The cardinality required at cell (i, j) line 40 source
Source documentation
The cardinality required at cell (i, j).

no axioms what this means
Statement uses: Nat, Usa2019P4.Cell
Proof uses: HAdd.hAdd, OfNat.ofNat, Prod.fst, Fin, Prod.snd
4 instances, coercions and auxiliary constants left out.
```
def target {n : ℕ} (c : Cell n) : ℕ := c.1.val + c.2.val
```
Mentions: Usa2019P4.Cell
def Usa2019P4.Fillings Documented declaration: Fillings line 45 source
Source documentation
Partial configurations on a set D of cells: the cardinality and monotonicity conditions hold on D, and the value is ∅ off D (the latter condition keeps the ambient function type finite).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set, Usa2019P4.Cell, Finset, Fin, HMul.hMul, OfNat.ofNat
Proof uses: Set.ofPred, And, Membership.mem, Eq, Finset.card, Usa2019P4.target, LE.le, HAdd.hAdd, Not, EmptyCollection.emptyCollection
15 instances, coercions and auxiliary constants left out.
```
def Fillings (n : ℕ) (D : Set (Cell n)) : Set (Cell n → Finset (Fin (2 * n))) :=
…
```
Mentions: Usa2019P4.Cell
def Usa2019P4.colZero The cells of column 0 in rows ≤ j line 51 source
Source documentation
The cells of column 0 in rows ≤ j.

no axioms what this means
Statement uses: Nat, Set, Usa2019P4.Cell
Proof uses: Set.ofPred, And, Eq, HAdd.hAdd, OfNat.ofNat, Prod.fst, Fin, LE.le, Prod.snd
5 instances, coercions and auxiliary constants left out.
```
def colZero (n j : ℕ) : Set (Cell n) := {c | c.1.val = 0 ∧ c.2.val ≤ j}
```
Mentions: Usa2019P4.Cell
def Usa2019P4.topRow The cells of row n in columns 1..i line 54 source
Source documentation
The cells of row n in columns 1..i.

no axioms what this means
Statement uses: Nat, Set, Usa2019P4.Cell
Proof uses: Set.ofPred, And, LE.le, OfNat.ofNat, HAdd.hAdd, Prod.fst, Fin, Eq, Prod.snd
5 instances, coercions and auxiliary constants left out.
```
def topRow (n i : ℕ) : Set (Cell n) := {c | 1 ≤ c.1.val ∧ c.1.val ≤ i ∧ c.2.val = n}
```
Mentions: Usa2019P4.Cell
def Usa2019P4.intCols The interior cells (rows < n) in columns 1..i line 57 source
Source documentation
The interior cells (rows < n) in columns 1..i.

no axioms what this means
Statement uses: Nat, Set, Usa2019P4.Cell
Proof uses: Set.ofPred, And, LE.le, OfNat.ofNat, HAdd.hAdd, Prod.fst, Fin, LT.lt, Prod.snd
6 instances, coercions and auxiliary constants left out.
```
def intCols (n i : ℕ) : Set (Cell n) := {c | 1 ≤ c.1.val ∧ c.1.val ≤ i ∧ c.2.val < n}
```
Mentions: Usa2019P4.Cell
def Usa2019P4.colPart The interior cells of column k in rows `n - r line 60 source
Source documentation
The interior cells of column k in rows n - r .. n - 1.

no axioms what this means
Statement uses: Nat, Set, Usa2019P4.Cell
Proof uses: Set.ofPred, And, Eq, HAdd.hAdd, OfNat.ofNat, Prod.fst, Fin, LE.le, HSub.hSub, Prod.snd, LT.lt
8 instances, coercions and auxiliary constants left out.
```
def colPart (n k r : ℕ) : Set (Cell n) := {c | c.1.val = k ∧ n - r ≤ c.2.val ∧ c.2.val < n}
```
Mentions: Usa2019P4.Cell
lemma Usa2019P4.cell_ext Cell equality in terms of coordinate values line 63 source
Source documentation
Cell equality in terms of coordinate values.

no axioms what this means
Statement uses: Nat, Usa2019P4.Cell, LT.lt, HAdd.hAdd, OfNat.ofNat, Iff, Eq, Prod.mk, Fin, Fin.mk, And, Prod.fst, Prod.snd
Proof uses: Iff.intro, Eq.mpr, id, congrArg, And.intro, rfl, Iff.mpr, Prod, Prod.ext_iff, Fin.ext_iff
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma cell_ext {n : ℕ} {c : Cell n} {a b : ℕ} {ha : a < n + 1} {hb : b < n + 1} :
    c = (⟨a, ha⟩, ⟨b, hb⟩) ↔ c.1.val = a ∧ c.2.val = b :=
…
```
Mentions: Usa2019P4.Cell
lemma Usa2019P4.fillings_empty The only filling of the empty set of cells line 69 source
Source documentation
The only filling of the empty set of cells.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Set, Usa2019P4.Cell, Finset, Fin, HMul.hMul, OfNat.ofNat, Usa2019P4.Fillings, EmptyCollection.emptyCollection, Singleton.singleton
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, HAdd.hAdd, Prod.mk, True, congr, congrArg, congrFun', Set.ofPred, And, Finset.card, Usa2019P4.target, LE.le, Not, funext, forall_congr, False and 7 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma fillings_empty (n : ℕ) : Fillings n (∅ : Set (Cell n)) = {fun _ ↦ ∅} := by
…
```
Mentions: Usa2019P4.Fillings, Usa2019P4.Cell
lemma Usa2019P4.restrict_mem Restricting a filling of insert s D to a filling of D by resetting the value at s to ∅ line 75 source
Source documentation
Restricting a filling of insert s D to a filling of D by resetting the value at s to ∅.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set, Usa2019P4.Cell, Not, Membership.mem, Finset, Fin, HMul.hMul, OfNat.ofNat, Usa2019P4.Fillings, Insert.insert, Function.update, HAdd.hAdd, EmptyCollection.emptyCollection
Proof uses: Eq, Finset.card, Usa2019P4.target, And, LE.le, And.intro, Eq.mpr, id, congrArg, Function.update_of_ne, ne_of_mem_of_not_mem, Set.mem_insert_of_mem, dite, Function.update_self, Set.mem_of_mem_insert_of_ne
26 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma restrict_mem {n : ℕ} {D : Set (Cell n)} {s : Cell n} (hs : s ∉ D)
    {S : Cell n → Finset (Fin (2 * n))} (hS : S ∈ Fillings n (insert s D)) :
    Function.update S s ∅ ∈ Fillings n D := by
…
```
Mentions: Usa2019P4.Cell, S, Usa2019P4.Fillings
lemma Usa2019P4.extend_mem Extending a filling of D by an admissible value X at s line 94 source
Source documentation
Extending a filling of D by an admissible value X at s.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set, Usa2019P4.Cell, Not, Membership.mem, Finset, Fin, HMul.hMul, OfNat.ofNat, Usa2019P4.Fillings, LE.le, HAdd.hAdd, Eq, Finset.card, Usa2019P4.target, Insert.insert, Function.update
Proof uses: And.intro, And, EmptyCollection.emptyCollection, Or, Iff.mp, Set.mem_insert_iff, Eq.mpr, id, congrArg, Function.update_self, Function.update_of_ne, ne_of_mem_of_not_mem, And.left, Finset.Subset.refl, Finset.Subset.trans, And.right, Ne, Eq.mp, Set.mem_insert, Set.mem_insert_of_mem
31 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
lemma extend_mem {n : ℕ} {D : Set (Cell n)} {s : Cell n} (hs : s ∉ D)
    {A C : (Cell n → Finset (Fin (2 * n))) → Finset (Fin (2 * n))}
    (hlo : ∀ f ∈ Fillings n D, ∀ d ∈ D, d ≤ s → f d ⊆ A f)
    (hhi : ∀ f ∈ Fillings n D, ∀ d ∈ D, s ≤ d → C f ⊆ f d)
    {f : Cell n → Finset (Fin (2 * n))} (hf : f ∈ Fillings n D)
    {X : Finset (Fin (2 * n))} (hXA : A f ⊆ X) (hXC : X ⊆ C f)
    (hXt : X.card = target s) :
    Function.update f s X ∈ Fillings n (insert s D) := by
…
```
Mentions: Usa2019P4.Cell, f, Usa2019P4.Fillings, Usa2019P4.target
lemma Usa2019P4.card_between The sets between A and C with cardinality t are counted by a binomial coefficient line 128 source
Source documentation
The sets between A and C with cardinality t are counted by a binomial coefficient.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, LE.le, Nat, Finset.card, Eq, Nat.card, Subtype, And, Nat.choose, HSub.hSub
Proof uses: Equiv, Membership.mem, Finset.powersetCard, SDiff.sdiff, Equiv.mk, Subtype.mk, Iff.mpr, Finset.mem_powersetCard, And.intro, Finset.sdiff_subset_sdiff, And.left, And.right, Subtype.property, Finset.Subset.refl, Eq.mpr, id, congrArg, Finset.card_sdiff_of_subset, Eq.refl, Union.union and 18 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma card_between {α : Type*} [DecidableEq α] {A C : Finset α} (hAC : A ⊆ C)
    {t : ℕ} (hAt : A.card ≤ t) :
    Nat.card {X : Finset α // A ⊆ X ∧ X ⊆ C ∧ X.card = t} =
      (C.card - A.card).choose (t - A.card) := by
…
```
abbrev Usa2019P4.Fiber The possible values of a filling at a fresh cell s, given the values A f and C f forced by the neighbors of s line 153 source
Source documentation
The possible values of a filling at a fresh cell s, given the values A f and C f forced by the neighbors of s.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set, Usa2019P4.Cell, Finset, Fin, HMul.hMul, OfNat.ofNat, Usa2019P4.Fillings
Proof uses: Subtype, And, LE.le, Membership.mem, Eq, Finset.card, Usa2019P4.target
13 instances, coercions and auxiliary constants left out.
```
abbrev Fiber {n : ℕ} {D : Set (Cell n)}
    (A C : (Cell n → Finset (Fin (2 * n))) → Finset (Fin (2 * n))) (s : Cell n)
    (f : ↥(Fillings n D)) : Type :=
…
```
Mentions: Usa2019P4.Cell, f, Usa2019P4.Fillings
lemma Usa2019P4.ncard_fillings_insert Adding one cell to the domain multiplies the number of fillings by a binomial coefficient line 160 source
Source documentation
Adding one cell to the domain multiplies the number of fillings by a binomial coefficient.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set, Usa2019P4.Cell, Not, Membership.mem, Finset, Fin, HMul.hMul, OfNat.ofNat, Usa2019P4.Fillings, LE.le, HAdd.hAdd, Insert.insert, Function.update, EmptyCollection.emptyCollection, Eq, Finset.card, Usa2019P4.target, Set.ncard, Nat.choose and 1 more
Proof uses: Nat.card, Usa2019P4.Fiber, Subtype, And, Usa2019P4.card_between, Subtype.property, Eq.mp, congrArg, Sigma, Sigma.mk, Subtype.mk, Usa2019P4.restrict_mem, And.intro, And.left, Set.mem_insert, Sigma.fst, Sigma.snd, Usa2019P4.extend_mem, And.right, Function.Injective and 28 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 65 steps
Open to load the checked before-and-after goal states.
```
lemma ncard_fillings_insert {n : ℕ} {D : Set (Cell n)} {s : Cell n} (hs : s ∉ D)
    {A C : (Cell n → Finset (Fin (2 * n))) → Finset (Fin (2 * n))}
    (hlo : ∀ f ∈ Fillings n D, ∀ d ∈ D, d ≤ s → f d ⊆ A f)
    (hhi : ∀ f ∈ Fillings n D, ∀ d ∈ D, s ≤ d → C f ⊆ f d)
    (hAs : ∀ g ∈ Fillings n (insert s D), A (Function.update g s ∅) ⊆ g s)
    (hsC : ∀ g ∈ Fillings n (insert s D), g s ⊆ C (Function.update g s ∅))
    (hAC : ∀ f ∈ Fillings n D, A f ⊆ C f)
    {a₀ c₀ : ℕ}
    (hAcard : ∀ f ∈ Fillings n D, (A f).card = a₀)
    (hCcard : ∀ f ∈ Fillings n D, (C f).card = c₀)
    (hAt : ∀ f ∈ Fillings n D, (A f).card ≤ target s) :
    (Fillings n (insert s D)).ncard =
…
```
Mentions: Usa2019P4.Cell, f, Usa2019P4.Fillings, Usa2019P4.target
lemma Usa2019P4.stageA Counting the fillings of the leftmost column: after j steps there are ∏ i ∈ range j, (2 * n - i) fillings line 249 source
Source documentation
Counting the fillings of the leftmost column: after j steps there are ∏ i ∈ range j, (2 * n - i) fillings.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Eq, Set.ncard, Usa2019P4.Cell, Finset, Fin, HMul.hMul, OfNat.ofNat, Usa2019P4.Fillings, Usa2019P4.colZero, Finset.prod, Finset.range, HSub.hSub
Proof uses: Nat.recAux, LT.lt, HAdd.hAdd, Nat.zero_lt_succ, Set, Insert.insert, Prod, Prod.mk, Fin.mk, EmptyCollection.emptyCollection, Set.ext, Eq.mpr, Iff, Membership.mem, And, Prod.fst, Prod.snd, id, congrArg, Eq.trans and 68 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 87 steps
Open to load the checked before-and-after goal states.
```
lemma stageA (n : ℕ) : ∀ j, j ≤ n →
    (Fillings n (colZero n j)).ncard = ∏ i ∈ Finset.range j, (2 * n - i) := by
…
```
Mentions: Usa2019P4.Fillings, Usa2019P4.colZero
lemma Usa2019P4.stageB Counting the fillings of the left column together with the top row line 331 source
Source documentation
Counting the fillings of the left column together with the top row.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Eq, Set.ncard, Usa2019P4.Cell, Finset, Fin, HMul.hMul, OfNat.ofNat, Usa2019P4.Fillings, Union.union, Set, Usa2019P4.colZero, Usa2019P4.topRow, Finset.prod, Finset.range, HSub.hSub
Proof uses: Nat.recAux, EmptyCollection.emptyCollection, Set.ext, Eq.mpr, Iff, Membership.mem, Not, And, HAdd.hAdd, Prod.fst, Prod.snd, id, Eq.trans, False, congrArg, iff_false, Set.union_empty, Finset.prod_range_zero, one_mul, Usa2019P4.stageA and 55 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 70 steps
Open to load the checked before-and-after goal states.
```
lemma stageB (n : ℕ) : ∀ i, i ≤ n →
    (Fillings n (colZero n n ∪ topRow n i)).ncard =
      (∏ j ∈ Finset.range i, (n - j)) * ∏ j ∈ Finset.range n, (2 * n - j) := by
…
```
Mentions: Usa2019P4.Fillings, Usa2019P4.colZero, Usa2019P4.topRow
lemma Usa2019P4.stageC_inner Filling the interior column k + 1 from the top down: each of the n cells doubles the number of fillings line 404 source
Source documentation
Filling the interior column k + 1 from the top down: each of the n cells doubles the number of fillings.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, LT.lt, Eq, Set.ncard, Usa2019P4.Cell, Finset, Fin, HMul.hMul, OfNat.ofNat, Usa2019P4.Fillings, Union.union, Set, Usa2019P4.colZero, Usa2019P4.topRow, Usa2019P4.intCols, Usa2019P4.colPart, HAdd.hAdd, HPow.hPow
Proof uses: Nat.recAux, EmptyCollection.emptyCollection, Set.ext, Eq.mpr, Iff, Membership.mem, Not, And, Prod.fst, HSub.hSub, Prod.snd, id, Eq.trans, False, congrArg, iff_false, Set.union_empty, pow_zero, one_mul, Eq.refl and 54 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 97 steps
Open to load the checked before-and-after goal states.
```
lemma stageC_inner (n : ℕ) : ∀ r, r ≤ n → ∀ k, k < n →
    (Fillings n (colZero n n ∪ topRow n n ∪ intCols n k ∪ colPart n (k + 1) r)).ncard =
      2 ^ r * (Fillings n (colZero n n ∪ topRow n n ∪ intCols n k)).ncard := by
…
```
Mentions: Usa2019P4.Fillings, Usa2019P4.colZero, Usa2019P4.topRow, Usa2019P4.intCols, Usa2019P4.colPart
lemma Usa2019P4.stageC Counting the fillings of everything except the right column of the grid line 501 source
Source documentation
Counting the fillings of everything except the right column of the grid.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Eq, Set.ncard, Usa2019P4.Cell, Finset, Fin, HMul.hMul, OfNat.ofNat, Usa2019P4.Fillings, Union.union, Set, Usa2019P4.colZero, Usa2019P4.topRow, Usa2019P4.intCols, HPow.hPow, Finset.prod, Finset.range, HSub.hSub
Proof uses: Nat.recAux, EmptyCollection.emptyCollection, Set.ext, Eq.mpr, Iff, Membership.mem, Not, And, HAdd.hAdd, Prod.fst, LT.lt, Prod.snd, id, Eq.trans, False, congrArg, iff_false, Set.union_empty, Usa2019P4.stageB, le_refl and 41 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma stageC (n : ℕ) : ∀ k, k ≤ n →
    (Fillings n (colZero n n ∪ topRow n n ∪ intCols n k)).ncard =
      2 ^ (n * k) * ((∏ i ∈ Finset.range n, (n - i)) * ∏ j ∈ Finset.range n, (2 * n - j)) := by
…
```
Mentions: Usa2019P4.Fillings, Usa2019P4.colZero, Usa2019P4.topRow, Usa2019P4.intCols
theorem Usa2019P4.prod_range_self_sub line 526 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.prod, Finset.range, HSub.hSub, Nat.factorial
Proof uses: Eq.mpr, HAdd.hAdd, OfNat.ofNat, id, congrArg, Eq.symm, Finset.prod_range_add_one_eq_factorial, Finset.prod_range_reflect, Finset.prod_congr, rfl, Finset, Membership.mem, Eq.mp, LT.lt, propext, Finset.mem_range
13 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Usa2019P4.prod_range_two_mul_sub_mul line 534 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMul.hMul, Finset.prod, Finset.range, HSub.hSub, OfNat.ofNat, Nat.factorial
Proof uses: HAdd.hAdd, Eq.mpr, id, congrArg, Eq.symm, Finset.prod_range_reflect, Finset.prod_congr, rfl, Finset, Membership.mem, Eq.mp, LT.lt, propext, Finset.mem_range, Finset.prod_range_add, Finset.prod_range_add_one_eq_factorial, Nat.two_mul, Nat.mul_comm, Usa2019P4.prod_range_self_sub, Eq.refl
22 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Usa2019P4.main_count The full count: the number of valid configurations is `(2 * n)! line 551 source
Source documentation
The full count: the number of valid configurations is (2 * n)! * 2 ^ (n ^ 2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Set.ncard, Usa2019P4.Cell, Finset, Fin, HMul.hMul, OfNat.ofNat, Usa2019P4.Fillings, Set.univ, Nat.factorial, HPow.hPow
Proof uses: Set, Union.union, Usa2019P4.colZero, Usa2019P4.topRow, Usa2019P4.intCols, Set.ext, Eq.mpr, Iff, Membership.mem, Or, And, HAdd.hAdd, Prod.fst, LE.le, Prod.snd, LT.lt, id, Eq.trans, True, congr and 15 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma main_count (n : ℕ) : (Fillings n Set.univ).ncard = (2 * n)! * 2 ^ (n ^ 2) := by
…
```
Mentions: Usa2019P4.Fillings
determine Usa2019P4.answer line 565 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HMul.hMul, Nat.factorial, OfNat.ofNat, HPow.hPow
7 instances, coercions and auxiliary constants left out.
problem Usa2019P4.usa2019_p4 line 567 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Nat.card, Subtype, Fin, HAdd.hAdd, OfNat.ofNat, Finset, HMul.hMul, And, Finset.card, LE.le, Usa2019P4.answer
Proof uses: Equiv, Usa2019P4.Cell, Usa2019P4.Fillings, Set.univ, Equiv.mk, Subtype.mk, Membership.mem, Set, Prod.fst, Prod.snd, And.intro, Usa2019P4.target, Not, EmptyCollection.emptyCollection, And.left, Subtype.property, And.right, Iff.mp, Prod, Prod.le_def and 18 more
29 instances, coercions and auxiliary constants left out.

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