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

42 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2012, Problem 3

Determine which integers n > 1 have the property that there exists an infinite sequence a₁, a₂, a₃, ... of nonzero integers such that the equality

aₖ + 2a₂ₖ + ⋯ + naₙₖ = 0

holds for every positive integer k.

Imports (5)

Imported by 1 file

Compfiles.lean

def Usa2012P3.mulSeq A completely multiplicative sequence built from values assigned on a finite set of primes: mulSeq P c j = ∏ r ∈ P, c r ^ (Nat.factorization j r) line 36 source
Source documentation
A completely multiplicative sequence built from values assigned on a finite set of primes: mulSeq P c j = ∏ r ∈ P, c r ^ (Nat.factorization j r).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Int
Proof uses: Finset.prod, HPow.hPow, Finsupp, Nat.factorization
9 instances, coercions and auxiliary constants left out.
```
def mulSeq (P : Finset ℕ) (c : ℕ → ℤ) (j : ℕ) : ℤ :=
…
```
Mentions: P
lemma Usa2012P3.mulSeq_mul line 39 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Int, Ne, OfNat.ofNat, Eq, Usa2012P3.mulSeq, HMul.hMul
Proof uses: of_eq_true, Finset.prod, HPow.hPow, Finsupp, Nat.factorization, Eq.trans, True, congrFun', congrArg, Finset.prod_congr, Eq.refl, Membership.mem, HAdd.hAdd, Nat.factorization_mul, pow_add, Finset.prod_mul_distrib, eq_self
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.mulSeq_ne_zero line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Int, Membership.mem, Ne, OfNat.ofNat, Usa2012P3.mulSeq
Proof uses: Iff.mpr, Finset.prod, HPow.hPow, Finsupp, Nat.factorization, Finset.prod_ne_zero_iff, pow_ne_zero
33 instances, coercions and auxiliary constants left out.
lemma Usa2012P3.condition_of_sum_eq_zero If the sum ∑ j ∈ [1, n], j * a j vanishes for a completely multiplicative sequence a, then a satisfies all the required identities line 50 source
Source documentation
If the sum ∑ j ∈ [1, n], j * a j vanishes for a completely multiplicative sequence a, then a satisfies all the required identities.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Int, Eq, Finset.sum, Finset.Icc, OfNat.ofNat, HMul.hMul, Usa2012P3.mulSeq, LE.le
Proof uses: Ne, Trans.trans, Finset.sum_congr, rfl, Membership.mem, And.left, Iff.mp, And, Finset.mem_Icc, Eq.mpr, id, congrArg, Usa2012P3.mulSeq_mul, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.symm and 13 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma condition_of_sum_eq_zero {n : ℕ} {P : Finset ℕ} {c : ℕ → ℤ}
    (h : ∑ j ∈ Finset.Icc 1 n, (j : ℤ) * mulSeq P c j = 0) (k : ℕ) (hk : 1 ≤ k) :
    ∑ j ∈ Finset.Icc 1 n, (j : ℤ) * mulSeq P c (j * k) = 0 := by
…
```
Mentions: P, h, Usa2012P3.mulSeq
lemma Usa2012P3.bezout_nonzero Bézout's identity, arranged so that both coefficients are nonzero line 67 source
Source documentation
Bézout's identity, arranged so that both coefficients are nonzero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LT.lt, OfNat.ofNat, IsCoprime, Exists, And, Ne, Eq, HAdd.hAdd, HMul.hMul
Proof uses: LE.le, Neg.neg, Int.natAbs, Int.le_natAbs, Eq.mp, congrArg, Nat, Int.natAbs_neg, rfl, mul_le_mul_of_nonneg_right, le_of_lt, one_mul, Exists.intro, HSub.hSub, And.intro, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast and 40 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma bezout_nonzero {A B c : ℤ} (hA : 0 < A) (hB : 0 < B) (h : IsCoprime A B) :
    ∃ x y : ℤ, x ≠ 0 ∧ y ≠ 0 ∧ A * x + B * y = c := by
…
```
Mentions: h
lemma Usa2012P3.not_property_two The case n = 2 is impossible: the relation a k + 2 * a (2 * k) = 0 forces 2 ^ j ∣ a 1 for every j, so a 1 = 0 line 95 source
Source documentation
The case n = 2 is impossible: the relation a k + 2 * a (2 * k) = 0 forces 2 ^ j ∣ a 1 for every j, so a 1 = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LE.le, OfNat.ofNat, Ne, Eq, HAdd.hAdd, HMul.hMul, False
Proof uses: HPow.hPow, Neg.neg, Nat.recAux, of_eq_true, Eq.trans, True, congrArg, congr, pow_zero, one_mul, eq_self, Nat.one_le_two_pow, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf and 79 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma not_property_two {a : ℕ → ℤ} (ha : ∀ i, 1 ≤ i → a i ≠ 0)
    (h : ∀ k, 1 ≤ k → a k + 2 * a (2 * k) = 0) : False := by
…
```
Mentions: h
def Usa2012P3.cfun The coefficient function assigning x to p, y to q, and 1 to everything else line 129 source
Source documentation
The coefficient function assigning x to p, y to q, and 1 to everything else.

no axioms what this means
Statement uses: Nat, Int
Proof uses: ite, Eq, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
```
def cfun (p q : ℕ) (x y : ℤ) (r : ℕ) : ℤ := if r = p then x else if r = q then y else 1
```
lemma Usa2012P3.mulSeq_cfun_apply line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Ne, Eq, Usa2012P3.mulSeq, Insert.insert, Finset, Singleton.singleton, Usa2012P3.cfun, HMul.hMul, HPow.hPow, Finsupp, Nat.factorization
Proof uses: Not, Membership.mem, Eq.mpr, id, congrArg, Finset.prod, Usa2012P3.mulSeq.eq_1, Finset.prod_insert, Finset.prod_singleton, of_eq_true, Eq.trans, True, congrFun', congr, ite_eq_left_of_eq_true, ite, OfNat.ofNat, eq_self, ite_eq_right_of_eq_false, eq_false and 1 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.mulSeq_cfun_p line 140 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Nat.Prime, LT.lt, Eq, Usa2012P3.mulSeq, Insert.insert, Finset, Singleton.singleton, Usa2012P3.cfun
Proof uses: Ne, ne_of_lt, Eq.mpr, HMul.hMul, HPow.hPow, Finsupp, Nat.factorization, id, congrArg, Usa2012P3.mulSeq_cfun_apply, OfNat.ofNat, Nat.Prime.factorization_self, Nat.factorization_eq_zero_of_not_dvd, Nat.not_dvd_of_pos_of_lt, Nat.Prime.pos, of_eq_true, Eq.trans, True, congrFun', congr and 4 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.mulSeq_cfun_2p line 147 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Nat.Prime, LE.le, OfNat.ofNat, LT.lt, Eq, Usa2012P3.mulSeq, Insert.insert, Finset, Singleton.singleton, Usa2012P3.cfun, HMul.hMul
Proof uses: Ne, ne_of_lt, Finsupp, Nat.factorization, Eq.mpr, HAdd.hAdd, id, congrArg, Nat.factorization_mul, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Nat.Prime.ne_zero, Finsupp.add_apply, Nat.factorization_eq_zero_of_not_dvd, Nat.not_dvd_of_pos_of_lt, Mathlib.Meta.NormNum.isNat_lt_true, Nat.Prime.factorization_self and 17 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.mulSeq_cfun_3p line 165 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Nat.Prime, LE.le, OfNat.ofNat, LT.lt, Eq, Usa2012P3.mulSeq, Insert.insert, Finset, Singleton.singleton, Usa2012P3.cfun, HMul.hMul
Proof uses: Ne, ne_of_lt, Finsupp, Nat.factorization, Eq.mpr, HAdd.hAdd, id, congrArg, Nat.factorization_mul, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Nat.Prime.ne_zero, Finsupp.add_apply, Nat.factorization_eq_zero_of_not_dvd, Nat.not_dvd_of_pos_of_lt, Mathlib.Meta.NormNum.isNat_lt_true, Nat.Prime.factorization_self and 17 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.mulSeq_cfun_q line 183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Nat.Prime, LT.lt, Eq, Usa2012P3.mulSeq, Insert.insert, Finset, Singleton.singleton, Usa2012P3.cfun
Proof uses: Ne, ne_of_lt, Finsupp, Nat.factorization, OfNat.ofNat, Nat.factorization_eq_zero_of_not_dvd, Dvd.dvd, Iff.mp, Nat.prime_dvd_prime_iff_eq, Eq.mpr, HMul.hMul, HPow.hPow, id, congrArg, Usa2012P3.mulSeq_cfun_apply, Nat.Prime.factorization_self, of_eq_true, Eq.trans, True, congrFun' and 5 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.term_eq_zero Terms j * (a j - 1) vanish when j ∈ [1, n] is none of p, 2p, 3p, q: such a j is divisible by neither p nor q, so a j = 1 line 195 source
Source documentation
Terms j * (a j - 1) vanish when j ∈ [1, n] is none of p, 2p, 3p, q: such a j is divisible by neither p nor q, so a j = 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LT.lt, HMul.hMul, OfNat.ofNat, LE.le, Ne, Eq, HSub.hSub, Usa2012P3.mulSeq, Insert.insert, Finset, Singleton.singleton, Usa2012P3.cfun
Proof uses: ne_of_lt, Not, Dvd.dvd, False, GT.gt, Or, Nat.eq_zero_or_pos, False.elim, Eq.mp, Eq.trans, congrArg, MulZeroClass.mul_zero, Eq.symm, Nat.lt_of_mul_lt_mul_left, lt_of_le_of_lt, dite, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat.rawCast and 34 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
lemma term_eq_zero {n p q j : ℕ} {x y : ℤ} (hplt : p < q)
    (h2q : n < 2 * q) (h4p : n < 4 * p) (hj1 : 1 ≤ j) (hjn : j ≤ n)
    (h1 : j ≠ p) (h2 : j ≠ 2 * p) (h3 : j ≠ 3 * p) (h4 : j ≠ q) :
    (j : ℤ) * (mulSeq {p, q} (cfun p q x y) j - 1) = 0 := by
…
```
Mentions: Usa2012P3.mulSeq, Usa2012P3.cfun
lemma Usa2012P3.sum_mulSeq_cfun_sub_one The correction terms in ∑ j ∈ [1,n], j * (a j - 1): the only nonzero contributions come from j ∈ {p, 2p, 3p, q} ∩ [1, n] line 228 source
Source documentation
The correction terms in ∑ j ∈ [1,n], j * (a j - 1): the only nonzero contributions come from j ∈ {p, 2p, 3p, q} ∩ [1, n].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Nat.Prime, LE.le, OfNat.ofNat, LT.lt, HMul.hMul, Eq, Finset.sum, Finset.Icc, HSub.hSub, Usa2012P3.mulSeq, Insert.insert, Finset, Singleton.singleton, Usa2012P3.cfun, HAdd.hAdd, ite
Proof uses: Ne, ne_of_lt, HMod.hMod, Or, Nat.Prime.eq_two_or_odd, Iff.mp, Dvd.dvd, Nat.prime_dvd_prime_iff_eq, Exists.intro, Eq.mpr, id, congrArg, mul_comm, Eq.symm, dite, ite_eq_left, Membership.mem, And, propext, Finset.mem_Icc and 61 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 111 steps
Open to load the checked before-and-after goal states.
```
lemma sum_mulSeq_cfun_sub_one {n p q : ℕ} {x y : ℤ} (hp : p.Prime) (hq : q.Prime)
    (hp5 : 5 ≤ p) (hq7 : 7 ≤ q) (hplt : p < q)
    (h2q : n < 2 * q) (h4p : n < 4 * p) (hpn : p ≤ n) (hqn : q ≤ n) :
    ∑ j ∈ Finset.Icc 1 n, (j : ℤ) * (mulSeq {p, q} (cfun p q x y) j - 1)
      = (p : ℤ) * (x - 1)
        + (if 2 * p ≤ n then ((2 * p : ℕ) : ℤ) * (x - 1) else 0)
        + (if 3 * p ≤ n then ((3 * p : ℕ) : ℤ) * (x - 1) else 0)
        + (q : ℤ) * (y - 1) := by
…
```
Mentions: Usa2012P3.mulSeq, Usa2012P3.cfun
lemma Usa2012P3.exists_good_seq_of_nine_le Documented declaration: exists_good_seq_of_nine_le line 321 source
Source documentation
Construction for 9 ≤ n: pick primes p, q via Bertrand's postulate with ⌈n/2⌉ < q ≤ 2⌈n/2⌉ and (q-1)/2 < p ≤ q-1, take a r = 1 for primes r ∉ {p, q}, and choose nonzero a p, a q by Bézout so that ∑ j ∈ [1,n], j * a j = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Int, And, Ne, Eq, Finset.sum, Finset.Icc, HMul.hMul
Proof uses: Nat.Prime, LT.lt, HDiv.hDiv, HAdd.hAdd, Nat.exists_prime_lt_and_le_two_mul, Or, lt_or_ge, False.elim, Eq.mp, False, eq_false, Mathlib.Meta.NormNum.isNat_not_prime, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.not_prime_mul_of_ble, Bool, Bool.false, Eq.symm, le_antisymm, Nat.ge_of_not_lt and 96 more
143 instances, coercions and auxiliary constants left out.

Tactic trace: 145 steps
Open to load the checked before-and-after goal states.
```
lemma exists_good_seq_of_nine_le {n : ℕ} (hn : 9 ≤ n) :
    ∃ a : ℕ → ℤ, (∀ i, 1 ≤ i → a i ≠ 0) ∧
      ∀ k, 1 ≤ k → ∑ j ∈ Finset.Icc 1 n, (j : ℤ) * a (j * k) = 0 := by
…
```
lemma Usa2012P3.small_case The small cases 3 ≤ n ≤ 8, each given by an explicit completely multiplicative sequence line 437 source
Source documentation
The small cases 3 ≤ n ≤ 8, each given by an explicit completely multiplicative sequence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Int, Membership.mem, Ne, OfNat.ofNat, Eq, Finset.sum, Finset.range, HMul.hMul, HAdd.hAdd, Usa2012P3.mulSeq, Exists, And, LE.le
Proof uses: Exists.intro, And.intro, Usa2012P3.mulSeq_ne_zero, Finset.Icc, Eq.mpr, id, congrFun', congrArg, Eq.trans, HSub.hSub, Finset.Ico, Finset.sum_congr, Eq.refl, Finset.sum_Ico_eq_sum_range, add_tsub_cancel_right, congr, add_comm, Nat.cast_add, Nat.cast_one, Usa2012P3.condition_of_sum_eq_zero and 1 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma small_case (n : ℕ) (P : Finset ℕ) (c : ℕ → ℤ) (hc : ∀ r ∈ P, c r ≠ 0)
    (hsum : ∑ j ∈ Finset.range n, (j + 1 : ℤ) * mulSeq P c (j + 1) = 0) :
    ∃ a : ℕ → ℤ, (∀ i, 1 ≤ i → a i ≠ 0) ∧
      ∀ k, 1 ≤ k → ∑ j ∈ Finset.range n, (j + 1 : ℤ) * a ((j + 1) * k) = 0 := by
…
```
Mentions: P, Usa2012P3.mulSeq
lemma Usa2012P3.factorization.f22 line 452 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finsupp.single, Nat.Prime.factorization, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_2, Mathlib.Meta.NormNum.IsNat.raw_refl, Finsupp.single_eq_same, eq_self, eq_true, True.intro
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f23 line 454 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finsupp.single, Nat.Prime.factorization, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_2, Mathlib.Meta.NormNum.IsNat.raw_refl, Finsupp.single_eq_of_ne, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.instAtLeastTwo, Bool.false, eq_self, eq_true and 1 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f25 line 456 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finsupp.single, Nat.Prime.factorization, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_2, Mathlib.Meta.NormNum.IsNat.raw_refl, Finsupp.single_eq_of_ne, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.instAtLeastTwo, Bool.false, eq_self, eq_true and 1 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f27 line 458 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finsupp.single, Nat.Prime.factorization, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_2, Mathlib.Meta.NormNum.IsNat.raw_refl, Finsupp.single_eq_of_ne, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.instAtLeastTwo, Bool.false, eq_self, eq_true and 1 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f32 line 460 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finsupp.single, Nat.Prime.factorization, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Finsupp.single_eq_of_ne, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.instAtLeastTwo, eq_self and 2 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f33 line 462 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finsupp.single, Nat.Prime.factorization, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Finsupp.single_eq_same, eq_self, eq_true, True.intro
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f35 line 464 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finsupp.single, Nat.Prime.factorization, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Finsupp.single_eq_of_ne, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.instAtLeastTwo, eq_self and 2 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f37 line 466 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finsupp.single, Nat.Prime.factorization, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Finsupp.single_eq_of_ne, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.instAtLeastTwo, eq_self and 2 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f42 line 468 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: Eq.mpr, HMul.hMul, id, congrArg, rfl, HAdd.hAdd, Nat.factorization_mul, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Finsupp.add_apply, Usa2012P3.factorization.f22
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f43 line 472 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Nat.factorization_eq_zero_of_not_dvd, Mathlib.Meta.NormNum.isNat_dvd_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.succ
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f45 line 476 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Nat.factorization_eq_zero_of_not_dvd, Mathlib.Meta.NormNum.isNat_dvd_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.succ
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f47 line 480 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Nat.factorization_eq_zero_of_not_dvd, Mathlib.Meta.NormNum.isNat_dvd_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.succ
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f52 line 484 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finsupp.single, Nat.Prime.factorization, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Finsupp.single_eq_of_ne, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.instAtLeastTwo, eq_self and 2 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f53 line 486 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finsupp.single, Nat.Prime.factorization, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Finsupp.single_eq_of_ne, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.instAtLeastTwo, eq_self and 2 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f55 line 488 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finsupp.single, Nat.Prime.factorization, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Finsupp.single_eq_same, eq_self, eq_true, True.intro
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f57 line 490 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finsupp.single, Nat.Prime.factorization, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Finsupp.single_eq_of_ne, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.instAtLeastTwo, eq_self and 2 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f62 line 492 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: Eq.mpr, HMul.hMul, id, congrArg, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.isNat_mul, HAdd.hAdd, Nat.factorization_mul, Mathlib.Meta.NormNum.isNat_eq_false, Bool, Bool.false, of_eq_true, Eq.trans, True, congrFun', Finsupp.single, congr, Nat.Prime.factorization and 13 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f63 line 496 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: Eq.mpr, HMul.hMul, id, congrArg, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.isNat_mul, HAdd.hAdd, Nat.factorization_mul, Mathlib.Meta.NormNum.isNat_eq_false, Bool, Bool.false, of_eq_true, Eq.trans, True, congrFun', Finsupp.single, congr, Nat.Prime.factorization and 13 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f65 line 500 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Nat.factorization_eq_zero_of_not_dvd, Mathlib.Meta.NormNum.isNat_dvd_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.succ
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f67 line 504 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Nat.factorization_eq_zero_of_not_dvd, Mathlib.Meta.NormNum.isNat_dvd_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.succ
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f75 line 508 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Nat.factorization_eq_zero_of_not_dvd, Mathlib.Meta.NormNum.isNat_dvd_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.succ
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f77 line 512 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finsupp.single, Nat.Prime.factorization, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Finsupp.single_eq_same, eq_self, eq_true, True.intro
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f85 line 514 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Nat.factorization_eq_zero_of_not_dvd, Mathlib.Meta.NormNum.isNat_dvd_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.succ
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P3.factorization.f87 line 518 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finsupp, Nat.factorization, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Nat.factorization_eq_zero_of_not_dvd, Mathlib.Meta.NormNum.isNat_dvd_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.succ
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
determine Usa2012P3.SolutionSet line 526 source
no axioms what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, LT.lt, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
problem Usa2012P3.usa2012_p3 line 528 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Iff, Membership.mem, Set, Usa2012P3.SolutionSet, Exists, Int, And, LE.le, Ne, Eq, Finset.sum, Finset.Icc, HMul.hMul
Proof uses: id, Iff.intro, Or, lt_or_ge, dite, Usa2012P3.small_case, Insert.insert, Finset, Singleton.singleton, Neg.neg, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, of_eq_true, Finset.range, HAdd.hAdd, Usa2012P3.mulSeq, Eq.trans and 78 more
117 instances, coercions and auxiliary constants left out.

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