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

39 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1990, Problem 4

How many positive integers can be written in base n so that (1) the integer has no two digits the same, and (2) each digit after the first differs by one from an earlier digit? For example, in base 3, the possible numbers are 1, 2, 10, 12, 21, 102, 120, 210.

Imports (6)

Imported by 1 file

Compfiles.lean

def Usa1990P4.DiffByOne Documented declaration: DiffByOne line 35 source
Source documentation
Condition (2) of the problem, phrased for the list of base-n digits of a number as produced by Nat.digits (least significant digit first, so the "first" digit of the number is the last entry of the list): every digit except the most significant one differs by one from some more significant digit.

standard axioms: Quot.sound, propext what this means
Statement uses: List, Nat
Proof uses: LT.lt, HAdd.hAdd, OfNat.ofNat, List.length, Exists, And, Or, Eq, GetElem.getElem
6 instances, coercions and auxiliary constants left out.
```
def DiffByOne (l : List ℕ) : Prop :=
…
```
inductive Usa1990P4.IV Documented declaration: IV line 45 source
Source documentation
IV a b l holds when l is a list of natural numbers whose set of entries is exactly the interval [a, b], built by starting from a single digit and repeatedly prepending a new minimum or a new maximum. These are essentially the valid digit lists of the problem (up to the leading-digit condition).

no axioms what this means
Statement uses: Nat, List
```
inductive IV : ℕ → ℕ → List ℕ → Prop
  | single (d : ℕ) : IV d d [d]
  | consLo {a b : ℕ} {l : List ℕ} (h : IV (a + 1) b l) : IV a b (a :: l)
  | consHi {a b : ℕ} {l : List ℕ} (h : IV a (b - 1) l) (hhi : 0 < b) :
      IV a b (b :: l)

namespace IV
```
Mentions: h
theorem Usa1990P4.IV.ne_nil line 53 source
no axioms what this means
Statement uses: Nat, List, Usa1990P4.IV, Ne, List.nil
Proof uses: Eq, HEq, List.cons, Usa1990P4.IV.single, List.cons_ne_nil, Eq.symm, HAdd.hAdd, OfNat.ofNat, Usa1990P4.IV.consLo, HSub.hSub, LT.lt, Usa1990P4.IV.consHi, Eq.refl, HEq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.IV.lo_le_hi line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Usa1990P4.IV, LE.le
Proof uses: Usa1990P4.IV.rec, Nat.le_refl, HAdd.hAdd, OfNat.ofNat, HSub.hSub, LT.lt
10 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.IV.mem_iff line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Usa1990P4.IV, Iff, Membership.mem, And, LE.le
Proof uses: Usa1990P4.IV.rec, Eq.mpr, List.cons, List.nil, Eq, id, congrArg, propext, List.mem_singleton, ge_antisymm_iff, HAdd.hAdd, OfNat.ofNat, Usa1990P4.IV.lo_le_hi, Or, List.mem_cons, HSub.hSub, LT.lt
13 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.IV.mem_lo line 75 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Usa1990P4.IV, Membership.mem
Proof uses: Iff.mpr, And, LE.le, Usa1990P4.IV.mem_iff, And.intro, Nat.le_refl, Usa1990P4.IV.lo_le_hi
3 instances, coercions and auxiliary constants left out.
theorem Usa1990P4.IV.mem_hi line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Usa1990P4.IV, Membership.mem
Proof uses: Iff.mpr, And, LE.le, Usa1990P4.IV.mem_iff, And.intro, Usa1990P4.IV.lo_le_hi, Nat.le_refl
3 instances, coercions and auxiliary constants left out.
theorem Usa1990P4.IV.nodup line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Usa1990P4.IV, List.Nodup
Proof uses: Usa1990P4.IV.rec, of_eq_true, List.cons, List.nil, Eq.trans, And, Not, Membership.mem, True, congr, congrArg, False, not_false_eq_true, and_self, HAdd.hAdd, OfNat.ofNat, Iff.mpr, List.nodup_cons, And.intro, LE.le and 4 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.IV.length_eq line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Usa1990P4.IV, Eq, List.length, HSub.hSub, HAdd.hAdd, OfNat.ofNat
Proof uses: Usa1990P4.IV.rec, id, List.cons, List.nil, LE.le, Usa1990P4.IV.lo_le_hi, Eq.mpr, congrArg, List.length_cons, LT.lt
15 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.IV.cons_iff Inversion principle for IV on a cons list line 107 source
Source documentation
Inversion principle for IV on a cons list.

no axioms what this means
Statement uses: Nat, List, Iff, Usa1990P4.IV, List.cons, Or, And, Eq, HAdd.hAdd, OfNat.ofNat, LT.lt, HSub.hSub, List.nil
Proof uses: Iff.intro, HEq, Usa1990P4.IV.single, Or.inr, And.intro, rfl, Eq.symm, eq_of_heq, Usa1990P4.IV.consLo, Or.inl, Usa1990P4.IV.consHi, Eq.refl, HEq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem cons_iff {a b d : ℕ} {l : List ℕ} :
    IV a b (d :: l) ↔
      (d = a ∧ IV (a + 1) b l) ∨ (d = b ∧ 0 < b ∧ IV a (b - 1) l) ∨
        (a = d ∧ b = d ∧ l = []) := by
…
```
Mentions: Usa1990P4.IV
theorem Usa1990P4.IV.diffByOne IV lists satisfy condition (2) of the problem line 124 source
Source documentation
IV lists satisfy condition (2) of the problem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Usa1990P4.IV, Usa1990P4.DiffByOne
Proof uses: Usa1990P4.IV.rec, LT.lt, HAdd.hAdd, OfNat.ofNat, List.length, List.cons, List.nil, Eq, rfl, Nat.casesAuxOn, Exists, And, Or, GetElem.getElem, Iff.mp, Membership.mem, List.mem_iff_getElem, Usa1990P4.IV.mem_lo, Exists.intro, And.intro and 14 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
```
theorem diffByOne {a b : ℕ} {l : List ℕ} (h : IV a b l) : DiffByOne l := by
…
```
Mentions: h, Usa1990P4.IV, Usa1990P4.DiffByOne
theorem Usa1990P4.IV.of_diffByOne Lists with distinct entries satisfying condition (2) are exactly the IV lists line 163 source
Source documentation
Lists with distinct entries satisfying condition (2) are exactly the IV lists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Ne, List.nil, List.Nodup, Usa1990P4.DiffByOne, Exists, Usa1990P4.IV
Proof uses: List.rec, absurd, Eq, rfl, List.cons, Exists.intro, Usa1990P4.IV.single, And.right, Not, Membership.mem, Iff.mp, And, List.nodup_cons, LT.lt, HAdd.hAdd, OfNat.ofNat, List.length, Or, GetElem.getElem, Eq.mpr and 23 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
```
theorem of_diffByOne {l : List ℕ} (hne : l ≠ []) (hn : l.Nodup) (hd : DiffByOne l) :
    ∃ a b, IV a b l := by
…
```
Mentions: Usa1990P4.DiffByOne, Usa1990P4.IV
theorem Usa1990P4.IV.unique_indices The interval endpoints of an IV list are uniquely determined line 202 source
Source documentation
The interval endpoints of an IV list are uniquely determined.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Usa1990P4.IV, And, Eq
Proof uses: LE.le, Iff.mp, Membership.mem, Usa1990P4.IV.mem_iff, Usa1990P4.IV.mem_lo, Usa1990P4.IV.mem_hi
3 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem unique_indices {a b a' b' : ℕ} {l : List ℕ} (h : IV a b l)
    (h' : IV a' b' l) : a = a' ∧ b = b' := by
…
```
Mentions: h, Usa1990P4.IV
def Usa1990P4.ValidLists Documented declaration: ValidLists line 216 source
Source documentation
Digit lists satisfying the conditions of the problem in base n: distinct digits, condition (2), all digits less than n, and a nonzero leading digit (the last entry of the list, since digits are stored least-significant first).

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Set, List
Proof uses: Set.ofPred, And, List.Nodup, Usa1990P4.DiffByOne, Membership.mem, LT.lt, Ne, List.nil, List.getLast, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
def ValidLists (n : ℕ) : Set (List ℕ) :=
…
```
def Usa1990P4.W Valid digit lists whose digits form exactly the interval [a, b] line 221 source
Source documentation
Valid digit lists whose digits form exactly the interval [a, b].

no axioms what this means
Statement uses: Nat, Set, List
Proof uses: Set.ofPred, And, Usa1990P4.IV, Ne, List.nil, List.getLast, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
def W (a b : ℕ) : Set (List ℕ) := {l | IV a b l ∧ ∀ h : l ≠ [], l.getLast h ≠ 0}
```
Mentions: Usa1990P4.IV, h
def Usa1990P4.IVSet Lists whose digits form exactly the interval [a, b] line 224 source
Source documentation
Lists whose digits form exactly the interval [a, b].

no axioms what this means
Statement uses: Nat, Set, List
Proof uses: Set.ofPred, Usa1990P4.IV
```
def IVSet (a b : ℕ) : Set (List ℕ) := {l | IV a b l}
```
Mentions: Usa1990P4.IV
def Usa1990P4.descend The decreasing list b, b-1, ..., 1, 0 line 227 source
Source documentation
The decreasing list b, b-1, ..., 1, 0.

no axioms what this means
Statement uses: Nat, List
2 instances, coercions and auxiliary constants left out.
```
def descend : ℕ → List ℕ
  | 0 => [0]
  | b + 1 => (b + 1) :: descend b
```
theorem Usa1990P4.descend_ne_nil line 231 source
no axioms what this means
Statement uses: Nat, Ne, List, Usa1990P4.descend, List.nil
Proof uses: Nat.casesAuxOn, List.cons_ne_nil, OfNat.ofNat, HAdd.hAdd
3 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.descend_eq line 237 source
standard axioms: propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, List, Usa1990P4.descend, List.cons, HSub.hSub
Proof uses: Nat.casesAuxOn, HAdd.hAdd, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.IV_descend line 242 source
no axioms what this means
Statement uses: Nat, Usa1990P4.IV, OfNat.ofNat, Usa1990P4.descend
Proof uses: Nat.recAux, Usa1990P4.IV.single, Usa1990P4.IV.consHi, HAdd.hAdd, Nat.zero_lt_succ
4 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.getLast?_descend line 248 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Option, List.getLast?, Usa1990P4.descend, Option.some, OfNat.ofNat
Proof uses: Nat.recAux, Eq.refl, id, HAdd.hAdd, Eq.mpr, List.cons, congrArg, List.getLast?_cons_of_ne_nil, Usa1990P4.descend_ne_nil
4 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.getLast_descend line 257 source
standard axioms: propext what this means
Statement uses: Nat, Ne, List, Usa1990P4.descend, List.nil, Eq, List.getLast, OfNat.ofNat
Proof uses: Iff.mpr, Option, List.getLast?, Option.some, List.getLast_eq_iff_getLast?_eq_some, Usa1990P4.getLast?_descend
2 instances, coercions and auxiliary constants left out.
theorem Usa1990P4.eq_descend Among IV 0 b lists, only the decreasing list ends in 0 line 261 source
Source documentation
Among IV 0 b lists, only the decreasing list ends in 0.

standard axioms: propext what this means
Statement uses: Nat, List, Usa1990P4.IV, Ne, List.nil, Eq, List.getLast, OfNat.ofNat, And, Usa1990P4.descend
Proof uses: Usa1990P4.IV.rec, List.cons, List.cons_ne_nil, Eq.mp, congrArg, List.getLast_singleton, And.intro, rfl, Eq.symm, HAdd.hAdd, List.getLast_cons, absurd, Nat.succ_ne_zero, HSub.hSub, LT.lt, Eq.mpr, id, Usa1990P4.descend_eq, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem eq_descend {a b : ℕ} {l : List ℕ} (h : IV a b l)
    (hgl : ∀ hh : l ≠ [], l.getLast hh = 0) : a = 0 ∧ l = descend b := by
…
```
Mentions: h, Usa1990P4.IV, Usa1990P4.descend
theorem Usa1990P4.finite_and_ncard_IVSet The number of IV lists over the interval [a, a + k] is 2 ^ k line 287 source
Source documentation
The number of IV lists over the interval [a, a + k] is 2 ^ k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, Set.Finite, List, Usa1990P4.IVSet, HAdd.hAdd, Eq, Set.ncard, HPow.hPow, OfNat.ofNat
Proof uses: Nat.recAux, Set, Singleton.singleton, List.cons, List.nil, Set.ext, Eq.mpr, Iff, Membership.mem, Usa1990P4.IV, id, congrArg, Iff.intro, LE.le, Usa1990P4.IV.lo_le_hi, List.length, HSub.hSub, Usa1990P4.IV.length_eq, Exists, Iff.mp and 66 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 72 steps
Open to load the checked before-and-after goal states.
```
theorem finite_and_ncard_IVSet : ∀ (k a : ℕ),
    (IVSet a (a + k)).Finite ∧ (IVSet a (a + k)).ncard = 2 ^ k := by
…
```
Mentions: Usa1990P4.IVSet
theorem Usa1990P4.geom2 Geometric series with ratio 2 line 347 source
Source documentation
Geometric series with ratio 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Finset.range, HPow.hPow, OfNat.ofNat, HSub.hSub
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, congrFun', pow_zero, tsub_self, eq_self, Eq.mpr, HAdd.hAdd, id, Finset.sum_range_succ, HMul.hMul, pow_succ, LT.lt, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 2 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem geom2 : ∀ m, ∑ k ∈ Finset.range m, 2 ^ k = 2 ^ m - 1 := by
…
```
theorem Usa1990P4.two_pow_ge line 356 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HPow.hPow
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', MulZeroClass.mul_zero, zero_add, pow_one, Eq.mpr, id, Eq, pow_succ
32 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.outer_sum line 364 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Finset.range, HSub.hSub, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, congrFun', congr, zero_add, pow_one, MulZeroClass.mul_zero, tsub_zero, tsub_self, eq_self, Eq.mpr, id, Finset.sum_range_succ, LE.le, Usa1990P4.two_pow_ge, pow_succ, Mathlib.Tactic.Ring.of_eq and 27 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.ncard_biUnion Finite disjoint unions of sets of lists have the sum of the cardinalities line 376 source
Source documentation
Finite disjoint unions of sets of lists have the sum of the cardinalities.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Set, Membership.mem, Ne, Disjoint, Set.Finite, Eq, Set.ncard, Set.iUnion, Finset.sum
Proof uses: Finset.induction, EmptyCollection.emptyCollection, Set.ext, of_eq_true, Iff, Eq.trans, False, True, congr, congrArg, congrFun', funext, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, Set.iUnion_of_empty, Set.iUnion_empty, iff_self, Eq.mpr, id and 22 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem ncard_biUnion {α : Type*} (s : Finset ℕ) (f : ℕ → Set α)
    (hd : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j))
    (hf : ∀ i ∈ s, (f i).Finite) :
    (⋃ i ∈ s, f i).ncard = ∑ i ∈ s, (f i).ncard := by
…
```
Mentions: f
theorem Usa1990P4.W_finite line 406 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.Finite, List, Usa1990P4.W
Proof uses: dite, LE.le, Usa1990P4.IVSet, HAdd.hAdd, HSub.hSub, Eq, Set.ncard, HPow.hPow, OfNat.ofNat, And, Usa1990P4.finite_and_ncard_IVSet, Set.Finite.subset, Eq.mp, congrArg, Membership.mem, Set, And.left, Usa1990P4.IV, Ne, List.nil and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.disjoint_W line 420 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, Prod, Prod.mk, Disjoint, Set, List, Usa1990P4.W
Proof uses: Eq.mpr, Membership.mem, Not, id, Eq, congrArg, propext, Set.disjoint_left, Usa1990P4.IV, List.nil, List.getLast, OfNat.ofNat, False, And, Usa1990P4.IV.unique_indices, rfl
24 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.ncard_W The number of valid digit lists with digit interval [a, b] line 428 source
Source documentation
The number of valid digit lists with digit interval [a, b].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Eq, Set.ncard, List, Usa1990P4.W, HSub.hSub, HPow.hPow, OfNat.ofNat, ite
Proof uses: Set.Finite, Usa1990P4.IVSet, HAdd.hAdd, And, Usa1990P4.finite_and_ncard_IVSet, dite, Set, SDiff.sdiff, Singleton.singleton, Usa1990P4.descend, Set.ext, Eq.mpr, Iff, Membership.mem, Usa1990P4.IV, Ne, List.nil, List.getLast, Not, id and 27 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
theorem ncard_W {a b : ℕ} (hle : a ≤ b) :
    (W a b).ncard = 2 ^ (b - a) - (if a = 0 then 1 else 0) := by
…
```
Mentions: Usa1990P4.W
theorem Usa1990P4.validLists_eq_biUnion The valid digit lists are the disjoint union of the W a b over 0 ≤ a ≤ b < n line 461 source
Source documentation
The valid digit lists are the disjoint union of the W a b over 0 ≤ a ≤ b < n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Set, List, Usa1990P4.ValidLists, Set.iUnion, Membership.mem, Finset, Finset.range, HAdd.hAdd, OfNat.ofNat, Usa1990P4.W
Proof uses: Set.ext, Iff.intro, List.Nodup, And, Usa1990P4.DiffByOne, LT.lt, Ne, List.nil, List.getLast, Exists, Usa1990P4.IV, Usa1990P4.IV.of_diffByOne, Usa1990P4.IV.mem_hi, Nat.lt_succ_of_le, Usa1990P4.IV.lo_le_hi, Iff.mpr, Set.mem_iUnion₂, Exists.intro, Finset.mem_range, And.intro and 9 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem validLists_eq_biUnion (n : ℕ) :
    ValidLists n = ⋃ b ∈ Finset.range n, ⋃ a ∈ Finset.range (b + 1), W a b := by
…
```
Mentions: Usa1990P4.ValidLists, Usa1990P4.W
theorem Usa1990P4.disjoint_inner line 481 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, Disjoint, Set, List, Set.iUnion, Membership.mem, Finset, Finset.range, HAdd.hAdd, OfNat.ofNat, Usa1990P4.W
Proof uses: Eq.mpr, Not, id, Eq, congrArg, propext, Set.disjoint_left, Exists, False, Eq.mp, Set.mem_iUnion₂, And, Usa1990P4.IV.unique_indices, And.left, Usa1990P4.IV, List.nil, List.getLast
33 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Usa1990P4.inner_finite line 492 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.Finite, List, Set.iUnion, Membership.mem, Finset, Finset.range, HAdd.hAdd, OfNat.ofNat, Usa1990P4.W
Proof uses: Set.Finite.biUnion, Finset.finite_toSet, Set, Usa1990P4.W_finite
11 instances, coercions and auxiliary constants left out.
theorem Usa1990P4.ncard_inner The number of valid digit lists whose largest digit is exactly b line 497 source
Source documentation
The number of valid digit lists whose largest digit is exactly b.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Set.ncard, List, Set.iUnion, Membership.mem, Finset, Finset.range, HAdd.hAdd, OfNat.ofNat, Usa1990P4.W, HSub.hSub, HPow.hPow
Proof uses: Eq.mpr, Finset.sum, id, congrArg, Usa1990P4.ncard_biUnion, Ne, Usa1990P4.disjoint_W, Prod, Prod.mk, Not, Eq.trans, And, Prod.mk.injEq, True, eq_self, and_true, Usa1990P4.W_finite, Finset.sum_range_succ', ite, Usa1990P4.ncard_W and 29 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
theorem ncard_inner (b : ℕ) :
    (⋃ a ∈ Finset.range (b + 1), W a b).ncard = 2 ^ (b + 1) - 2 := by
…
```
Mentions: Usa1990P4.W
theorem Usa1990P4.ncard_validLists The total number of valid digit lists in base n line 521 source
Source documentation
The total number of valid digit lists in base n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Set.ncard, List, Usa1990P4.ValidLists, HSub.hSub, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul
Proof uses: Eq.mpr, Set.iUnion, Membership.mem, Finset, Finset.range, Usa1990P4.W, id, congrArg, Set, Usa1990P4.validLists_eq_biUnion, Finset.sum, Usa1990P4.ncard_biUnion, Ne, Usa1990P4.disjoint_inner, Usa1990P4.inner_finite, Eq.trans, Finset.sum_congr, rfl, Usa1990P4.ncard_inner, Usa1990P4.outer_sum
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem ncard_validLists (n : ℕ) :
    (ValidLists n).ncard = 2 ^ (n + 1) - 2 * n - 2 := by
…
```
Mentions: Usa1990P4.ValidLists
theorem Usa1990P4.ncard_numbers_eq Positive integers satisfying the conditions of the problem correspond to valid digit lists via Nat.digits line 530 source
Source documentation
Positive integers satisfying the conditions of the problem correspond to valid digit lists via Nat.digits.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Set.ncard, Set.ofPred, And, List.Nodup, Nat.digits, Usa1990P4.DiffByOne, List, Usa1990P4.ValidLists
Proof uses: Set.ncard_congr, Membership.mem, Set, Ne, List.nil, Iff.mpr, Nat.digits_ne_nil_iff_ne_zero, And.intro, List.getLast, Nat.digits_lt_base, Nat.getLast_digit_ne_zero, Nat.digits.injective, Exists, Nat.ofDigits, Nat.digits_ofDigits, GT.gt, Or, Nat.eq_zero_or_pos, absurd, Eq.symm and 6 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
theorem ncard_numbers_eq (n : ℕ) (hn : 1 < n) :
    Set.ncard {m : ℕ | 0 < m ∧ (Nat.digits n m).Nodup ∧ DiffByOne (Nat.digits n m)} =
      (ValidLists n).ncard := by
…
```
Mentions: Usa1990P4.DiffByOne, Usa1990P4.ValidLists
determine Usa1990P4.answer line 554 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HSub.hSub, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul
11 instances, coercions and auxiliary constants left out.
problem Usa1990P4.usa1990_p4 line 556 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Set.ncard, Set.ofPred, And, LT.lt, List.Nodup, Nat.digits, Usa1990P4.DiffByOne, Usa1990P4.answer
Proof uses: Eq.mpr, List, Usa1990P4.ValidLists, id, congrArg, Usa1990P4.ncard_numbers_eq, HSub.hSub, HPow.hPow, HAdd.hAdd, HMul.hMul, Usa1990P4.ncard_validLists, Eq.refl
17 instances, coercions and auxiliary constants left out.

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