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

33 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2005, Problem 1

Determine all composite positive integers n for which it is possible to arrange all divisors of n that are greater than 1 in a circle so that no two adjacent divisors are relatively prime.

Imports (11)

Imported by 1 file

Compfiles.lean

def Usa2005P1.R The adjacency condition required of neighboring divisors in the circle: they must not be relatively prime line 37 source
Source documentation
The adjacency condition required of neighboring divisors in the circle: they must not be relatively prime.

no axioms what this means
Statement uses: Nat
Proof uses: Not, Nat.Coprime
```
def R (a b : ℕ) : Prop := ¬ Nat.Coprime a b
```
def Usa2005P1.GoodCircle GoodCircle n says that all divisors of n that are greater than 1 can be arranged in a circle so that no two adjacent divisors are relatively prime line 44 source
Source documentation
GoodCircle n says that all divisors of n that are greater than 1 can be arranged in a circle so that no two adjacent divisors are relatively prime. The circle is represented by a list l containing each such divisor exactly once; adjacency means "consecutive in l" (via l.IsChain R) plus the wrap-around pair (l.getLast? with l.head?).

no axioms what this means
Statement uses: Nat
Proof uses: Exists, List, And, List.Nodup, Ne, List.nil, Iff, Membership.mem, Dvd.dvd, LT.lt, OfNat.ofNat, List.IsChain, Usa2005P1.R, Option, List.getLast?, List.head?
5 instances, coercions and auxiliary constants left out.
```
def GoodCircle (n : ℕ) : Prop :=
…
```
determine Usa2005P1.SolutionSet The answer: all composite positive integers other than products of two distinct primes line 52 source
Source documentation
The answer: all composite positive integers other than products of two distinct primes.

standard axioms: propext what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, And, LT.lt, OfNat.ofNat, Not, Nat.Prime, Exists, Ne, Eq, HMul.hMul
4 instances, coercions and auxiliary constants left out.
```
determine SolutionSet : Set ℕ :=
…
```
lemma Usa2005P1.R_of_dvd_of_dvd Numbers sharing a common factor ≥ 2 are not coprime line 58 source
Source documentation
Numbers sharing a common factor ≥ 2 are not coprime.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Dvd.dvd, Usa2005P1.R
Proof uses: Nat.Coprime, Eq.rec, Nat.gcd, Eq, Nat.dvd_gcd, Nat.le_of_dvd, one_pos
14 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma R_of_dvd_of_dvd {d a b : ℕ} (hd : 2 ≤ d) (ha : d ∣ a) (hb : d ∣ b) : R a b := by
…
```
Mentions: Usa2005P1.R
lemma Usa2005P1.R_of_dvd If 2 ≤ a and a ∣ b, then a and b are not coprime line 65 source
Source documentation
If 2 ≤ a and a ∣ b, then a and b are not coprime.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Dvd.dvd, Usa2005P1.R
Proof uses: Usa2005P1.R_of_dvd_of_dvd, dvd_rfl
7 instances, coercions and auxiliary constants left out.
```
lemma R_of_dvd {a b : ℕ} (ha : 2 ≤ a) (hb : a ∣ b) : R a b :=
…
```
Mentions: Usa2005P1.R
lemma Usa2005P1.R_of_dvd_left R transfers along divisibility on the left line 69 source
Source documentation
R transfers along divisibility on the left.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Usa2005P1.R, Dvd.dvd
Proof uses: Nat.Coprime, Nat.Coprime.coprime_dvd_left
2 instances, coercions and auxiliary constants left out.
```
lemma R_of_dvd_left {a b c : ℕ} (h : R a b) (hac : a ∣ c) : R c b :=
…
```
Mentions: h, Usa2005P1.R
lemma Usa2005P1.R_of_dvd_right R transfers along divisibility on the right line 73 source
Source documentation
R transfers along divisibility on the right.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Usa2005P1.R, Dvd.dvd
Proof uses: Nat.Coprime, Nat.Coprime.coprime_dvd_right
2 instances, coercions and auxiliary constants left out.
```
lemma R_of_dvd_right {a b c : ℕ} (h : R a b) (hbc : b ∣ c) : R a c :=
…
```
Mentions: h, Usa2005P1.R
lemma Usa2005P1.R_symm R is symmetric line 77 source
Source documentation
R is symmetric.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Usa2005P1.R
Proof uses: Nat.Coprime, Nat.Coprime.symm
```
lemma R_symm {a b : ℕ} (h : R a b) : R b a := fun hc => h hc.symm
```
Mentions: h, Usa2005P1.R

lemma Usa2005P1.isChain_append Appending two chains gives a chain when the boundary elements are related line 80 source

Source documentation

Appending two chains gives a chain when the boundary elements are related.

standard axioms: Quot.sound, propext what this means

Statement uses: List, List.IsChain, Membership.mem, Option, List.getLast?, List.head?, HAppend.hAppend

8 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps

Open to load the checked before-and-after goal states.

lemma isChain_append {α : Type*} {R' : α → α → Prop} : ∀ (l₁ l₂ : List α),
    l₁.IsChain R' → l₂.IsChain R' →
    (∀ a ∈ l₁.getLast?, ∀ b ∈ l₂.head?, R' a b) → (l₁ ++ l₂).IsChain R'
  | [], l₂, _, h₂, _ => by simpa using h₂
  | [a], [], _, _, _ => by simp [List.IsChain.singleton]
  | [a], b :: t, _, h₂, h => .cons_cons (h a (by simp) b (by simp)) h₂
  | a :: b :: s, l₂, h₁, h₂, h =>
      .cons_cons (List.isChain_cons_cons.mp h₁).1
        (isChain_append (b :: s) l₂ (List.isChain_cons_cons.mp h₁).2 h₂ (by simpa using h))

/-- A list whose elements are all divisible by some `r ≥ 2` is an `R`-chain. -/

Mentions: h, Usa2005P1.R

lemma Usa2005P1.isChain_of_forall_dvd A list whose elements are all divisible by some r ≥ 2 is an R-chain line 91 source
Source documentation
A list whose elements are all divisible by some r ≥ 2 is an R-chain.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, List, Membership.mem, Dvd.dvd, List.IsChain, Usa2005P1.R
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma isChain_of_forall_dvd {r : ℕ} (hr : 2 ≤ r) :
    ∀ {l : List ℕ}, (∀ x ∈ l, r ∣ x) → l.IsChain R
  | [], _ => .nil
  | [a], _ => .singleton a
  | a :: b :: t, h =>
      .cons_cons (R_of_dvd_of_dvd hr (h a (by simp)) (h b (by simp)))
        (isChain_of_forall_dvd hr (fun x hx => h x (by simp [hx])))

/-- The list `[d, d*q, d*q^2, ..., d*q^e]`. -/
```
Mentions: Usa2005P1.R, h, Usa2005P1.R_of_dvd_of_dvd
def Usa2005P1.powChain The list [d, d*q, d*q^2, ..., d*q^e] line 100 source
Source documentation
The list [d, d*q, d*q^2, ..., d*q^e].

standard axioms: propext what this means
Statement uses: Nat, List
2 instances, coercions and auxiliary constants left out.
```
def powChain (d q : ℕ) : ℕ → List ℕ
  | 0 => [d]
  | e + 1 => powChain d q e ++ [d * q ^ (e + 1)]
```
lemma Usa2005P1.powChain_ne_nil line 104 source
standard axioms: propext what this means
Statement uses: Nat, Ne, List, Usa2005P1.powChain, List.nil
Proof uses: Nat.recAux, of_eq_true, Not, Eq, List.cons, Eq.trans, False, True, congrArg, not_false_eq_true, HAppend.hAppend, HMul.hMul, HPow.hPow, HAdd.hAdd, OfNat.ofNat, And, congr, eq_false, and_self
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2005P1.mem_powChain line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Membership.mem, List, Usa2005P1.powChain, Exists, And, LE.le, Eq, HMul.hMul, HPow.hPow
Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congr, congrArg, List.cons, List.nil, Or, False, or_false, funext, congrFun', pow_zero, mul_one, iff_self, Eq.mpr, HAdd.hAdd, id and 17 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Usa2005P1.head?_powChain line 124 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Option, List.head?, Usa2005P1.powChain, Option.some
Proof uses: Nat.recAux, of_eq_true, eq_self, Eq.mpr, HAdd.hAdd, OfNat.ofNat, HAppend.hAppend, List, List.cons, HMul.hMul, HPow.hPow, List.nil, id, congrArg, Nat.succ, Usa2005P1.powChain.eq_2, Option.or, List.head?_append, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2005P1.getLast?_powChain line 129 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Option, List.getLast?, Usa2005P1.powChain, Option.some, HMul.hMul, HPow.hPow
Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congrArg, pow_zero, mul_one, eq_self, Eq.mpr, HAdd.hAdd, HAppend.hAppend, List, List.cons, List.nil, id, Nat.succ, Usa2005P1.powChain.eq_2, Option.or, List.getLast?_append
22 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2005P1.isChain_powChain line 135 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, List.IsChain, Usa2005P1.R, Usa2005P1.powChain
Proof uses: Nat.recAux, List.IsChain.singleton, Eq.mpr, HAdd.hAdd, HAppend.hAppend, List, List.cons, HMul.hMul, HPow.hPow, List.nil, id, Eq, congrArg, Nat.succ, Usa2005P1.powChain.eq_2, Usa2005P1.isChain_append, Membership.mem, Option, List.getLast?, List.head? and 8 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2005P1.nodup_powChain line 147 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, List.Nodup, Usa2005P1.powChain
Proof uses: Eq, HMul.hMul, HPow.hPow, Nat.mul_left_cancel, Nat.pow_right_injective, Nat.recAux, of_eq_true, List.cons, List.nil, Eq.trans, And, Not, Membership.mem, List, True, congr, congrArg, False, not_false_eq_true, and_self and 16 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Usa2005P1.eq_of_mul_pow_eq If d * q^j = d' * q^j' with d, d' dividing m and q ∤ m prime, then d = d' and j = j' line 168 source
Source documentation
If d * q^j = d' * q^j' with d, d' dividing m and q ∤ m prime, then d = d' and j = j'.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Not, Dvd.dvd, Ne, OfNat.ofNat, Eq, HMul.hMul, HPow.hPow, And
Proof uses: Finsupp, Nat.factorization, Nat.factorization_eq_zero_of_not_dvd, dvd_trans, pow_ne_zero, Nat.Prime.ne_zero, congrArg, Eq.mp, HAdd.hAdd, Finsupp.single, congr, Eq.trans, Finsupp.single_eq_same, zero_add, Nat.Prime.factorization_pow, Nat.factorization_mul, And.intro, Nat.mul_right_cancel, pow_pos, Nat.Prime.pos and 1 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma eq_of_mul_pow_eq {m q : ℕ} (hq : q.Prime) (hqm : ¬ q ∣ m)
    {d d' j j' : ℕ} (hd : d ∣ m) (hd' : d' ∣ m) (hd0 : d ≠ 0) (hd'0 : d' ≠ 0)
    (h : d * q ^ j = d' * q ^ j') : d = d' ∧ j = j' := by
…
```
Mentions: h
lemma Usa2005P1.isChain_flatMap_powChain Chains, heads and lasts of flatMap (powChain · q e) over a chain l line 187 source
Source documentation
Chains, heads and lasts of flatMap (powChain · q e) over a chain l.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, List.IsChain, Usa2005P1.R, Membership.mem, LE.le, OfNat.ofNat, And, List.flatMap, Usa2005P1.powChain, Eq, Option, List.head?, List.getLast?, Option.map, HMul.hMul, HPow.hPow
20 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma isChain_flatMap_powChain {q e : ℕ} :
    ∀ {l : List ℕ}, l.IsChain R → (∀ x ∈ l, 2 ≤ x) →
      (l.flatMap (fun d => powChain d q e)).IsChain R ∧
      ((l.flatMap (fun d => powChain d q e)).head? = l.head?) ∧
      ((l.flatMap (fun d => powChain d q e)).getLast? =
        (l.getLast?).map (fun d => d * q ^ e))
  | [], _, _ => by simp
  | [d], _, h2 =>
      ⟨by simpa using isChain_powChain (h2 d (by simp)) e, by simp, by simp⟩
  | d₁ :: d₂ :: t, hchain, h2 => by
    have hd₁ : 2 ≤ d₁ := h2 d₁ (by simp)
…
```
Mentions: Usa2005P1.R, Usa2005P1.powChain, Usa2005P1.isChain_powChain
lemma Usa2005P1.goodCircle_mul_prime_pow Documented declaration: goodCircle_mul_prime_pow line 220 source
Source documentation
Key construction step: if the divisors > 1 of m admit a good circle and q is a prime not dividing m, then for any e ≥ 1 the divisors > 1 of m * q^e admit a good circle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Not, Dvd.dvd, List, List.Nodup, LE.le, OfNat.ofNat, List.length, Iff, Membership.mem, And, LT.lt, List.IsChain, Usa2005P1.R, Option, List.getLast?, List.head?, Usa2005P1.GoodCircle, HMul.hMul and 1 more
Proof uses: Ne, List.nil, Eq, False, False.elim, Eq.mp, Eq.trans, Eq.symm, Exists, List.cons, Iff.mp, List.ne_nil_iff_exists_cons, congrArg, zero_add, of_eq_true, Or, True, congr, eq_self, true_or and 183 more
187 instances, coercions and auxiliary constants left out.

Tactic trace: 357 steps (first 200 of 357)
Open to load the checked before-and-after goal states.
```
lemma goodCircle_mul_prime_pow {m q : ℕ} (hq : q.Prime) (hqm : ¬ q ∣ m)
    {l : List ℕ} (hnodup : l.Nodup) (hl2 : 2 ≤ l.length)
    (hmem : ∀ d : ℕ, d ∈ l ↔ d ∣ m ∧ 1 < d)
    (hchain : l.IsChain R)
    (hwrap : ∀ a ∈ l.getLast?, ∀ b ∈ l.head?, R a b)
    (e : ℕ) (he : 1 ≤ e) : GoodCircle (m * q ^ e) := by
…
```
Mentions: Usa2005P1.R, Usa2005P1.GoodCircle
lemma Usa2005P1.goodCircle_prime_pow The divisors > 1 of a prime power p ^ a with 2 ≤ a admit a good circle: any arrangement works, since every such divisor is divisible by p line 527 source
Source documentation
The divisors > 1 of a prime power p ^ a with 2 ≤ a admit a good circle: any arrangement works, since every such divisor is divisible by p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LE.le, OfNat.ofNat, Usa2005P1.GoodCircle, HPow.hPow
Proof uses: Ne, pow_ne_zero, Nat.Prime.ne_zero, Iff, Membership.mem, List, Finset.sort, Finset.filter, LT.lt, Nat.divisors, And, Dvd.dvd, Eq.mpr, Finset, id, Eq, congrArg, propext, Finset.mem_sort, Finset.mem_filter and 30 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
lemma goodCircle_prime_pow {p : ℕ} (hp : p.Prime) {a : ℕ} (ha : 2 ≤ a) :
    GoodCircle (p ^ a) := by
…
```
Mentions: Usa2005P1.GoodCircle
lemma Usa2005P1.two_le_length_of_composite_circle A circle for a composite number has at least two elements line 573 source
Source documentation
A circle for a composite number has at least two elements.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Not, Nat.Prime, List, List.Nodup, Iff, Membership.mem, And, Dvd.dvd, LE.le, List.length
Proof uses: Exists, Nat.exists_prime_and_dvd, Iff.mpr, And.intro, Nat.Prime.one_lt, dvd_refl, Ne, Eq, False, Finset, Insert.insert, Singleton.singleton, List.toFinset, Or, Eq.mp, Eq.trans, congrArg, Eq.mpr, id, Finset.card and 4 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma two_le_length_of_composite_circle {n : ℕ} (hn : 1 < n) (hnp : ¬ n.Prime)
    {l : List ℕ} (hnodup : l.Nodup) (hmem : ∀ d : ℕ, d ∈ l ↔ d ∣ n ∧ 1 < d) :
    2 ≤ l.length := by
…
```
lemma Usa2005P1.not_pq_of_factorization_ge_two If m has a prime factor whose exponent in m is at least 2, then m is not a product of two distinct primes line 591 source
Source documentation
If m has a prime factor whose exponent in m is at least 2, then m is not a product of two distinct primes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LE.le, OfNat.ofNat, Finsupp, Nat.factorization, Not, Exists, And, Ne, Eq, HMul.hMul
Proof uses: False, HAdd.hAdd, Eq.mpr, id, congrArg, Nat.factorization_mul, Nat.Prime.ne_zero, Eq.refl, Finsupp.single, Eq.mp, Nat.Prime.factorization, dite, Finsupp.add_apply, Finsupp.single_eq_same, Finsupp.single_eq_of_ne, Ne.symm, le_refl
31 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma not_pq_of_factorization_ge_two {m p : ℕ} (_hp : p.Prime)
    (hp2 : 2 ≤ m.factorization p) :
    ¬ ∃ r s : ℕ, r.Prime ∧ s.Prime ∧ r ≠ s ∧ m = r * s := by
…
```
lemma Usa2005P1.not_pq_of_three_le_card If m has at least three distinct prime factors, then m is not a product of two distinct primes line 614 source
Source documentation
If m has at least three distinct prime factors, then m is not a product of two distinct primes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Finset.card, Nat.primeFactors, Not, Exists, And, Nat.Prime, Ne, Eq, HMul.hMul
Proof uses: False, Finset, Insert.insert, Singleton.singleton, Eq.mpr, id, congrArg, Union.union, Nat.primeFactors_mul, Nat.Prime.ne_zero, Nat.Prime.primeFactors, Finset.union_singleton, Eq.refl, Finset.card_le_two, Eq.mp
15 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma not_pq_of_three_le_card {m : ℕ} (h3 : 3 ≤ m.primeFactors.card) :
    ¬ ∃ r s : ℕ, r.Prime ∧ s.Prime ∧ r ≠ s ∧ m = r * s := by
…
```
lemma Usa2005P1.mul_ne_self For a non-zero and b ≥ 2, neither a * b nor b * a equals a line 625 source
Source documentation
For a non-zero and b ≥ 2, neither a * b nor b * a equals a.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, And, Ne, HMul.hMul
Proof uses: And.intro, Eq, Eq.mpr, id, congrArg, mul_one, Eq.symm, Nat.mul_left_cancel, one_mul, Nat.mul_right_cancel
16 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma mul_ne_self {a b : ℕ} (ha : 0 < a) (hb : 2 ≤ b) : a * b ≠ a ∧ b * a ≠ a := by
…
```
lemma Usa2005P1.mul_ne_mul_of_ne Cancelling a common positive factor on the right preserves inequality line 637 source
Source documentation
Cancelling a common positive factor on the right preserves inequality.

standard axioms: propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Ne, HMul.hMul
Proof uses: Eq, Nat.mul_right_cancel
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma mul_ne_mul_of_ne {a b c : ℕ} (ha : 0 < a) (h : b ≠ c) : b * a ≠ c * a := by
…
```
Mentions: h
lemma Usa2005P1.ne_of_prime_mul A prime cannot equal a product with another prime on the left line 642 source
Source documentation
A prime cannot equal a product with another prime on the left.

standard axioms: propext what this means
Statement uses: Nat, Nat.Prime, Ne, HMul.hMul
Proof uses: Eq, Eq.symm, Iff.mp, Dvd.dvd, Nat.prime_dvd_prime_iff_eq, Eq.rec, dvd_mul_right
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma ne_of_prime_mul {a b c : ℕ} (ha : a.Prime) (hb : b.Prime) (h : a ≠ b) :
    a ≠ b * c := by
…
```
Mentions: h
lemma Usa2005P1.ne_of_prime_mul_mul A prime cannot equal a product of three numbers when the first is a different prime line 649 source
Source documentation
A prime cannot equal a product of three numbers when the first is a different prime.

standard axioms: propext what this means
Statement uses: Nat, Nat.Prime, Ne, HMul.hMul
Proof uses: Eq, Dvd.dvd, Eq.rec, dvd_mul_of_dvd_left, dvd_mul_right, Eq.symm, Iff.mp, Nat.prime_dvd_prime_iff_eq
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma ne_of_prime_mul_mul {a b : ℕ} (ha : a.Prime) (hb : b.Prime) (h : a ≠ b)
    (c d : ℕ) : a ≠ b * c * d := by
…
```
Mentions: h
lemma Usa2005P1.dvd_mul_prime_prime For distinct primes p and q, the divisors of p * q greater than 1 are exactly p, q and p * q line 657 source
Source documentation
For distinct primes p and q, the divisors of p * q greater than 1 are exactly p, q and p * q.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Dvd.dvd, HMul.hMul, LT.lt, OfNat.ofNat, Or, Eq
Proof uses: Ne, mul_ne_zero, Nat.Prime.ne_zero, Membership.mem, Finset, Nat.divisors, Iff.mpr, And, Nat.mem_divisors, And.intro, Insert.insert, Singleton.singleton, Exists, Eq.mp, Finset.mul, congrArg, propext, Finset.mem_mul, Nat.Prime.divisors, Nat.divisors_mul and 12 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma dvd_mul_prime_prime {p q x : ℕ} (hp : p.Prime) (hq : q.Prime)
    (hxdvd : x ∣ p * q) (hx1 : 1 < x) : x = p ∨ x = q ∨ x = p * q := by
…
```
lemma Usa2005P1.not_goodCircle_mul For distinct primes p q, no circle exists: in any circle the coprime pair p, q would have to be adjacent line 673 source
Source documentation
For distinct primes p q, no circle exists: in any circle the coprime pair p, q would have to be adjacent.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Ne, Not, Usa2005P1.GoodCircle, HMul.hMul
Proof uses: List, And, List.Nodup, List.nil, Iff, Membership.mem, Dvd.dvd, LT.lt, OfNat.ofNat, List.IsChain, Usa2005P1.R, Option, List.getLast?, List.head?, False, Or, Eq, Eq.mpr, id, congrArg and 54 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
```
lemma not_goodCircle_mul {p q : ℕ} (hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q) :
    ¬ GoodCircle (p * q) := by
…
```
Mentions: Usa2005P1.GoodCircle
lemma Usa2005P1.goodCircle_three_primes For pairwise distinct primes p q r, the circle [p*q, q, q*r, r, r*p, p, p*q*r] works line 720 source
Source documentation
For pairwise distinct primes p q r, the circle [p*q, q, q*r, r, r*p, p, p*q*r] works.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Ne, Usa2005P1.GoodCircle, HMul.hMul
Proof uses: OfNat.ofNat, mul_ne_zero, Nat.Prime.ne_zero, LT.lt, lt_of_lt_of_le, Nat.Prime.one_lt, Nat.le_mul_of_pos_right, Nat.Prime.pos, Exists.intro, List, And, List.Nodup, List.nil, Iff, Membership.mem, Dvd.dvd, List.IsChain, Usa2005P1.R, Option, List.getLast? and 86 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 140 steps
Open to load the checked before-and-after goal states.
```
lemma goodCircle_three_primes {p q r : ℕ} (hp : p.Prime) (hq : q.Prime) (hr : r.Prime)
    (hpq : p ≠ q) (hqr : q ≠ r) (hpr : p ≠ r) :
    GoodCircle (p * q * r) := by
…
```
Mentions: Usa2005P1.GoodCircle
lemma Usa2005P1.goodCircle_of_not_pq Main induction: every composite n that is not a product of two distinct primes admits a good circle line 825 source
Source documentation
Main induction: every composite n that is not a product of two distinct primes admits a good circle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Nat.primeFactors, LT.lt, OfNat.ofNat, Not, Nat.Prime, Exists, And, Ne, HMul.hMul, Usa2005P1.GoodCircle
Proof uses: Nat.recAux, Or, Eq.mp, Finset, EmptyCollection.emptyCollection, congrArg, propext, Nat.primeFactors_eq_empty, Finset.card_eq_zero, False.elim, False, Eq.symm, HAdd.hAdd, Finset.prod, HPow.hPow, Finsupp, Nat.factorization, Nat.prod_primeFactors_pow_factorization, Nat.casesAuxOn, Singleton.singleton and 94 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 198 steps
Open to load the checked before-and-after goal states.
```
lemma goodCircle_of_not_pq : ∀ (k : ℕ) (n : ℕ), n.primeFactors.card = k →
    1 < n → ¬ n.Prime →
    (¬ ∃ p q : ℕ, p.Prime ∧ q.Prime ∧ p ≠ q ∧ n = p * q) → GoodCircle n := by
…
```
Mentions: Usa2005P1.GoodCircle
problem Usa2005P1.usa2005_p1 Documented declaration: usa2005_p1 line 1009 source
Source documentation
USA Mathematical Olympiad 2005, Problem 1: the composite positive integers whose divisors greater than 1 can be arranged in a circle with no two adjacent divisors relatively prime are exactly the composite numbers that are not products of two distinct primes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Not, Nat.Prime, Iff, Usa2005P1.GoodCircle, Membership.mem, Set, Usa2005P1.SolutionSet
Proof uses: Iff.intro, And.intro, And, Exists, Ne, Eq, HMul.hMul, False, Usa2005P1.not_goodCircle_mul, Eq.symm, Usa2005P1.goodCircle_of_not_pq, Finset.card, Nat.primeFactors, rfl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
problem usa2005_p1 (n : ℕ) (hn : 1 < n) (hnp : ¬ n.Prime) :
    GoodCircle n ↔ n ∈ SolutionSet := by
…
```
Mentions: Usa2005P1.GoodCircle, Usa2005P1.SolutionSet