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

29 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1987, Problem 5

a₁, a₂, ... , aₙ is a sequence of 0s and 1s. T is the number of triples (aᵢ, aⱼ, aₖ) with i < j < k which are not equal to (0, 1, 0) or (1, 0, 1). For 1 ≤ i ≤ n, f(i) is the number of j < i with aⱼ = aᵢ plus the number of j > i with aⱼ ≠ aᵢ. Show that T = f(1)(f(1) - 1)/2 + f(2)(f(2) - 1)/2 + ... + f(n)(f(n) - 1)/2. If n is odd, what is the smallest value of T?

Imports (10)

Imported by 1 file

Compfiles.lean

def Usa1987P5.eqBefore The set of positions j < i with a j = a i line 40 source
Source documentation
The set of positions j < i with a j = a i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset
Proof uses: Finset.filter, And, LT.lt, Eq, Finset.univ
5 instances, coercions and auxiliary constants left out.
```
def eqBefore (a : Fin n → Bool) (i : Fin n) : Finset (Fin n) :=
…
```
def Usa1987P5.neqAfter The set of positions j > i with a j ≠ a i line 44 source
Source documentation
The set of positions j > i with a j ≠ a i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset
Proof uses: Finset.filter, And, LT.lt, Ne, Eq, Finset.univ
6 instances, coercions and auxiliary constants left out.
```
def neqAfter (a : Fin n → Bool) (i : Fin n) : Finset (Fin n) :=
…
```
def Usa1987P5.f The quantity f(i) from the problem statement line 48 source
Source documentation
The quantity f(i) from the problem statement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool
Proof uses: HAdd.hAdd, Finset.card, Usa1987P5.eqBefore, Usa1987P5.neqAfter
2 instances, coercions and auxiliary constants left out.
```
def f (a : Fin n → Bool) (i : Fin n) : ℕ := (eqBefore a i).card + (neqAfter a i).card
```
Mentions: Usa1987P5.eqBefore, Usa1987P5.neqAfter
def Usa1987P5.numGoodTriples The quantity T from the problem statement: the number of triples of indices i < j < k whose values are not (0, 1, 0) or (1, 0, 1) line 52 source
Source documentation
The quantity T from the problem statement: the number of triples of indices i < j < k whose values are not (0, 1, 0) or (1, 0, 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool
Proof uses: Finset.card, Prod, Finset.filter, And, LT.lt, Prod.fst, Prod.snd, Not, Or, Eq, Bool.false, Bool.true, Finset.univ
8 instances, coercions and auxiliary constants left out.
```
def numGoodTriples (a : Fin n → Bool) : ℕ :=
…
```
def Usa1987P5.altSeq The alternating sequence 0, 1, 0, 1, ... line 59 source
Source documentation
The alternating sequence 0, 1, 0, 1, ....

no axioms what this means
Statement uses: Nat, Fin, Bool
Proof uses: BEq.beq, HMod.hMod, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.
```
def altSeq (n : ℕ) : Fin n → Bool := fun i ↦ (i : ℕ) % 2 == 1
```
determine Usa1987P5.minT line 61 source
no axioms what this means
Statement uses: Nat
Proof uses: HDiv.hDiv, HMul.hMul, HSub.hSub, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
lemma Usa1987P5.f_apply line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa1987P5.f, HAdd.hAdd, Finset.card, Usa1987P5.eqBefore, Usa1987P5.neqAfter
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma Usa1987P5.good_iff A triple of bits is good (not alternating) iff two adjacent values agree line 69 source
Source documentation
A triple of bits is good (not alternating) iff two adjacent values agree.

no axioms what this means
Statement uses: Bool, Iff, Not, Or, And, Eq, Bool.false, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl, Eq.symm
7 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma good_iff (x y z : Bool) :
    ¬ ((x = false ∧ y = true ∧ z = false) ∨ (x = true ∧ y = false ∧ z = true)) ↔
      x = y ∨ y = z := by
…
```
lemma Usa1987P5.choose_add_two Vandermonde's identity at k = 2 line 75 source
Source documentation
Vandermonde's identity at k = 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Nat.choose, HAdd.hAdd, OfNat.ofNat, HMul.hMul
Proof uses: Rat, Eq.mpr, HDiv.hDiv, HSub.hSub, id, congr, congrArg, Eq.trans, Nat.cast_choose_two, congrFun', Nat.cast_add, Nat.cast_mul, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Rat.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne', NNRat.rawCast, Mathlib.Tactic.Ring.Common.div_congr and 57 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma choose_add_two (x y : ℕ) : (x + y).choose 2 = x.choose 2 + y.choose 2 + x * y := by
…
```
def Usa1987P5.tripsA Triples i < j < k with a i = a j = a k line 82 source
Source documentation
Triples i < j < k with a i = a j = a k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset, Prod
Proof uses: Finset.filter, And, LT.lt, Prod.fst, Prod.snd, Eq, Finset.univ
6 instances, coercions and auxiliary constants left out.
```
def tripsA (a : Fin n → Bool) : Finset (Fin n × Fin n × Fin n) :=
…
```
def Usa1987P5.tripsB Triples i < j < k with a i = a j ≠ a k line 86 source
Source documentation
Triples i < j < k with a i = a j ≠ a k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset, Prod
Proof uses: Finset.filter, And, LT.lt, Prod.fst, Prod.snd, Eq, Ne, Finset.univ
7 instances, coercions and auxiliary constants left out.
```
def tripsB (a : Fin n → Bool) : Finset (Fin n × Fin n × Fin n) :=
…
```
def Usa1987P5.tripsC Triples i < j < k with a i ≠ a j = a k line 90 source
Source documentation
Triples i < j < k with a i ≠ a j = a k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset, Prod
Proof uses: Finset.filter, And, LT.lt, Prod.fst, Prod.snd, Ne, Eq, Finset.univ
7 instances, coercions and auxiliary constants left out.
```
def tripsC (a : Fin n → Bool) : Finset (Fin n × Fin n × Fin n) :=
…
```
lemma Usa1987P5.numGoodTriples_eq line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa1987P5.numGoodTriples, HAdd.hAdd, Finset.card, Prod, Usa1987P5.tripsA, Usa1987P5.tripsB, Usa1987P5.tripsC
Proof uses: Finset, Finset.filter, And, LT.lt, Prod.fst, Prod.snd, Not, Or, Bool.false, Bool.true, Finset.univ, Union.union, Finset.ext, Eq.mpr, Iff, Membership.mem, Ne, id, congr, congrArg and 21 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
lemma Usa1987P5.card_tripsA line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Finset.card, Prod, Usa1987P5.tripsA, Finset.sum, Finset.univ, Nat.choose, Usa1987P5.eqBefore, OfNat.ofNat
Proof uses: Eq.mpr, Finset.filter, Prod.snd, id, congrArg, Finset.card_eq_sum_card_fiberwise, of_eq_true, Set.MapsTo, Finset, Eq.trans, Set.univ, True, Set, Finset.coe_univ, Finset.sum_congr, rfl, Membership.mem, LT.lt, Prod.fst, SProd.sprod and 22 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma Usa1987P5.card_tripsB line 161 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Finset.card, Prod, Usa1987P5.tripsB, Finset.sum, Finset.univ, HMul.hMul, Usa1987P5.eqBefore, Usa1987P5.neqAfter
Proof uses: Eq.mpr, Finset.filter, Prod.fst, Prod.snd, id, congrArg, Finset.card_eq_sum_card_fiberwise, of_eq_true, Set.MapsTo, Finset, Eq.trans, Set.univ, True, Set, Finset.coe_univ, Finset.sum_congr, rfl, Membership.mem, SProd.sprod, Eq.symm and 22 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma Usa1987P5.card_tripsC line 188 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Finset.card, Prod, Usa1987P5.tripsC, Finset.sum, Finset.univ, Nat.choose, Usa1987P5.neqAfter, OfNat.ofNat
Proof uses: Ne, of_decide_eq_true, id, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, Finset.filter, Prod.fst, congrArg, Finset.card_eq_sum_card_fiberwise, of_eq_true, Set.MapsTo, Finset, Eq.trans, Set.univ, True, Set, Finset.coe_univ, Finset.sum_congr and 28 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma Usa1987P5.sum_eqBefore line 215 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Finset.sum, Finset.univ, Finset.card, Usa1987P5.eqBefore, Prod, Finset.filter, And, LT.lt, Prod.fst, Prod.snd, SProd.sprod, Finset
Proof uses: Eq.mpr, id, congrArg, Finset.card_eq_sum_card_fiberwise, of_eq_true, Set.MapsTo, Eq.trans, Set.ofPred, Set.univ, True, congr, Set, Membership.mem, Finset.coe_filter, funext, congrFun', true_and, Finset.coe_univ, Finset.sum_congr, rfl and 15 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Usa1987P5.sum_neqAfter line 235 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Finset.sum, Finset.univ, Finset.card, Usa1987P5.neqAfter, Prod, Finset.filter, And, LT.lt, Prod.fst, Prod.snd, Ne, SProd.sprod, Finset
Proof uses: Eq.mpr, id, congrArg, Finset.card_eq_sum_card_fiberwise, of_eq_true, Set.MapsTo, Eq.trans, Set.ofPred, Not, Set.univ, True, congr, Set, Membership.mem, Finset.filter_congr, Iff.of_eq, Eq.refl, Finset.coe_filter, funext, congrFun' and 20 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Usa1987P5.sum_f The sum of the f values depends only on n line 256 source
Source documentation
The sum of the f values depends only on n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Finset.sum, Finset.univ, Usa1987P5.f, Nat.choose, Finset.card, OfNat.ofNat
Proof uses: HAdd.hAdd, Usa1987P5.eqBefore, Usa1987P5.neqAfter, Eq.mpr, id, congrArg, Eq.symm, Finset.sum_add_distrib, Finset.sum_congr, rfl, Finset, Membership.mem, Usa1987P5.f_apply, Eq.refl, Prod, Finset.filter, And, LT.lt, Prod.fst, Prod.snd and 27 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma sum_f (a : Fin n → Bool) :
    ∑ i : Fin n, f a i = (Finset.univ : Finset (Fin n)).card.choose 2 := by
…
```
Mentions: Usa1987P5.f
problem Usa1987P5.usa1987_p5_part1 line 285 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa1987P5.numGoodTriples, Finset.sum, Finset.univ, Nat.choose, Usa1987P5.f, OfNat.ofNat
Proof uses: Eq.mpr, HAdd.hAdd, Finset.card, Prod, Usa1987P5.tripsA, Usa1987P5.tripsB, Usa1987P5.tripsC, id, congrArg, Usa1987P5.numGoodTriples_eq, Usa1987P5.eqBefore, Usa1987P5.card_tripsA, HMul.hMul, Usa1987P5.neqAfter, Usa1987P5.card_tripsB, Usa1987P5.card_tripsC, Eq.symm, Finset.sum_add_distrib, Finset.sum_congr, rfl and 24 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa1987P5.key_div Divisibility: n * (n - 1) * (n - 3) = 8 * (n * C((n-1)/2, 2)) for n = 2k + 1 line 296 source
Source documentation
Divisibility: n * (n - 1) * (n - 3) = 8 * (n * C((n-1)/2, 2)) for n = 2k + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMul.hMul, HAdd.hAdd, OfNat.ofNat, HSub.hSub, Nat.choose
Proof uses: Eq.mpr, HDiv.hDiv, id, congrArg, Nat.choose_two_right, Nat.div_two_mul_two_of_even, Nat.even_mul_pred_self, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_right and 13 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma key_div (k : ℕ) :
    (2 * k + 1) * ((2 * k + 1) - 1) * ((2 * k + 1) - 3) = 8 * ((2 * k + 1) * k.choose 2) := by
…
```
lemma Usa1987P5.cast_key Cast of the product n * (n - 1) * (n - 3) to the integers, for odd n line 317 source
Source documentation
Cast of the product n * (n - 1) * (n - 3) to the integers, for odd n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, HMul.hMul, HAdd.hAdd, OfNat.ofNat, HSub.hSub
Proof uses: Nat.casesAuxOn, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNat_natSub, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.isInt_mul, Int.ofNat, Int.negOfNat, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.isInt_sub, Eq.mpr, id, congrArg, congr, Eq.trans, Nat.cast_mul and 41 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma cast_key (k : ℕ) :
    (((2 * k + 1) * ((2 * k + 1) - 1) * ((2 * k + 1) - 3) : ℕ) : ℤ) =
      ((2 * k + 1 : ℕ) : ℤ) * (((2 * k + 1 : ℕ) : ℤ) - 1) * (((2 * k + 1 : ℕ) : ℤ) - 3) := by
…
```
lemma Usa1987P5.lower_bound The lower bound: every sequence on 2k + 1 positions has at least (2k + 1) * C(k, 2) good triples line 330 source
Source documentation
The lower bound: every sequence on 2k + 1 positions has at least (2k + 1) * C(k, 2) good triples.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Bool, LE.le, Nat.choose, Usa1987P5.numGoodTriples
Proof uses: Eq, Int, HSub.hSub, Finset.sum, Finset.univ, HPow.hPow, Usa1987P5.f, Usa1987P5.usa1987_p5_part1, Eq.mpr, id, congrArg, Finset.mul_sum, Finset.sum_congr, rfl, Finset, Membership.mem, HDiv.hDiv, Nat.choose_two_right, Nat.div_two_mul_two_of_even, Nat.even_mul_pred_self and 129 more
142 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
```
lemma lower_bound (k : ℕ) (a : Fin (2 * k + 1) → Bool) :
    (2 * k + 1) * k.choose 2 ≤ numGoodTriples a := by
…
```
Mentions: Usa1987P5.numGoodTriples
lemma Usa1987P5.altSeq_eq_iff line 392 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Iff, Eq, Bool, Usa1987P5.altSeq, HMod.hMod, OfNat.ofNat
Proof uses: LT.lt, Nat.mod_lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool.false, id, Eq.mpr, BEq.beq, Bool.true, congrArg, propext, Bool.eq_iff_iff, beq_iff_eq, Iff.intro
22 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa1987P5.card_eqBefore_alt line 399 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Eq, Finset.card, Usa1987P5.eqBefore, Usa1987P5.altSeq, HDiv.hDiv
Proof uses: LT.lt, HMod.hMod, Nat.mod_lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Eq.mpr, Finset.range, id, congrArg, Eq.symm, Finset.card_range, Finset.card_bij, Membership.mem, Finset, Iff.mp, Usa1987P5.altSeq_eq_iff, And.right and 15 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Usa1987P5.card_neqAfter_alt line 428 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Eq, Finset.card, Usa1987P5.neqAfter, Usa1987P5.altSeq, HSub.hSub, HDiv.hDiv
Proof uses: LT.lt, HMod.hMod, Nat.mod_lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Eq.mpr, Finset.range, id, congrArg, Eq.symm, Finset.card_range, Finset.card_bij, Membership.mem, Finset, Not, Iff.mp, Iff.not and 18 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
lemma Usa1987P5.f_alt line 461 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Eq, Usa1987P5.f, Usa1987P5.altSeq
Proof uses: Eq.mpr, Finset.card, Usa1987P5.eqBefore, Usa1987P5.neqAfter, id, congrArg, Usa1987P5.f_apply, HDiv.hDiv, Usa1987P5.card_eqBefore_alt, HSub.hSub, Usa1987P5.card_neqAfter_alt, LT.lt, Fin.isLt
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1987P5.T_alt The alternating sequence attains the bound line 467 source
Source documentation
The alternating sequence attains the bound.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa1987P5.numGoodTriples, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Usa1987P5.altSeq, Nat.choose
Proof uses: Eq.mpr, Finset.sum, Fin, Finset.univ, Usa1987P5.f, id, congrArg, Usa1987P5.usa1987_p5_part1, Finset.sum_congr, rfl, Finset, Membership.mem, Usa1987P5.f_alt, Eq.refl, HSMul.hSMul, Finset.card, Finset.sum_const, Fintype.card, Finset.card_univ, Fintype.card_fin and 1 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma T_alt (k : ℕ) : numGoodTriples (altSeq (2 * k + 1)) = (2 * k + 1) * k.choose 2 := by
…
```
Mentions: Usa1987P5.numGoodTriples, Usa1987P5.altSeq
problem Usa1987P5.usa1987_p5_part2 line 476 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, IsLeast, Set.range, Fin, Bool, Usa1987P5.numGoodTriples, Usa1987P5.minT
Proof uses: Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Nat.choose, HSub.hSub, Usa1987P5.key_div, id, And.intro, Membership.mem, Set, lowerBounds, Exists.intro, Usa1987P5.altSeq, Eq.mpr, congrArg, Usa1987P5.T_alt, Eq.refl, LE.le, Usa1987P5.lower_bound and 1 more
26 instances, coercions and auxiliary constants left out.

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