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

51 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1990, Problem 3

Show that for any odd positive integer n, we can always divide the set {n, n+1, n+2, ... , n+32} into two parts, one with 14 numbers and one with 19, so that the numbers in each part can be arranged in a circle, with each number relatively prime to its two neighbours.

Imports (7)

Imported by 1 file

Compfiles.lean

def Usa1990P3.ValidCircle Documented declaration: ValidCircle line 35 source
Source documentation
A circular arrangement a : Fin k → ℕ of k numbers is valid if every entry is relatively prime to its cyclically-next neighbour (and hence also to its cyclically previous neighbour, since Nat.Coprime is symmetric).

standard axioms: propext what this means
Statement uses: Nat, NeZero, Fin
Proof uses: Nat.Coprime, HAdd.hAdd, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
def ValidCircle {k : ℕ} [NeZero k] (a : Fin k → ℕ) : Prop :=
…
```
lemma Usa1990P3.coprime_succ_self' Consecutive integers are coprime line 62 source
Source documentation
Consecutive integers are coprime.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Nat.Coprime, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, id, Eq, congrArg, propext, Nat.coprime_self_add_right, Nat.coprime_one_right
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma coprime_succ_self' (m : ℕ) : Nat.Coprime m (m + 1) := by
…
```
lemma Usa1990P3.coprime_succ_gen n + c is coprime to its successor line 67 source
Source documentation
n + c is coprime to its successor.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Nat.Coprime, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HMul.hMul, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Usa1990P3.coprime_succ_self'
23 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma coprime_succ_gen (n c : ℕ) : Nat.Coprime (n + c) (n + (c + 1)) := by
…
```
lemma Usa1990P3.coprime_add_prime_right If p is prime and does not divide n + c, then n + c and n + c + p are coprime (any common divisor divides their difference p) line 74 source
Source documentation
If p is prime and does not divide n + c, then n + c and n + c + p are coprime (any common divisor divides their difference p).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Not, Dvd.dvd, HAdd.hAdd, Nat.Coprime
Proof uses: Eq, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, OfNat.ofNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_zero_add, propext, Nat.coprime_self_add_right, Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd
22 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma coprime_add_prime_right {p : ℕ} (hp : p.Prime) {n c : ℕ} (h : ¬ p ∣ n + c) :
    Nat.Coprime (n + c) (n + (c + p)) := by
…
```
Mentions: h
lemma Usa1990P3.coprime_add_prime_left The symmetric version of coprime_add_prime_right line 81 source
Source documentation
The symmetric version of coprime_add_prime_right.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Not, Dvd.dvd, HAdd.hAdd, Nat.Coprime
Proof uses: Iff.mpr, Nat.coprime_comm, Usa1990P3.coprime_add_prime_right
6 instances, coercions and auxiliary constants left out.
```
lemma coprime_add_prime_left {p : ℕ} (hp : p.Prime) {n c : ℕ} (h : ¬ p ∣ n + c) :
    Nat.Coprime (n + (c + p)) (n + c) :=
…
```
Mentions: h
lemma Usa1990P3.coprime_add_two Two odd numbers at distance 2 are coprime line 86 source
Source documentation
Two odd numbers at distance 2 are coprime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Dvd.dvd, OfNat.ofNat, HAdd.hAdd, Nat.Coprime
Proof uses: Usa1990P3.coprime_add_prime_right, Nat.prime_two
8 instances, coercions and auxiliary constants left out.
```
lemma coprime_add_two {n c : ℕ} (h : ¬ 2 ∣ n + c) : Nat.Coprime (n + c) (n + (c + 2)) :=
…
```
Mentions: h
def Usa1990P3.offA1 Offsets of the first circle when 13 ∤ n: [n, n+1, …, n+13] line 94 source
Source documentation
Offsets of the first circle when 13 ∤ n: [n, n+1, …, n+13].

no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat
3 instances, coercions and auxiliary constants left out.
```
def offA1 (i : Fin 14) : ℕ := i.val
```
def Usa1990P3.offB1a Offsets of the second circle when 13 ∤ n and n ≢ 2 [MOD 17]: [n+15, n+14, n+16, n+17, …, n+32] line 98 source
Source documentation
Offsets of the second circle when 13 ∤ n and n ≢ 2 [MOD 17]: [n+15, n+14, n+16, n+17, …, n+32].

no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat
Proof uses: ite, Eq, HAdd.hAdd
6 instances, coercions and auxiliary constants left out.
```
def offB1a (i : Fin 19) : ℕ :=
…
```
def Usa1990P3.offB1b Offsets of the second circle when 13 ∤ n and n ≡ 2 [MOD 17]: [n+14, n+15, …, n+30, n+32, n+31] line 103 source
Source documentation
Offsets of the second circle when 13 ∤ n and n ≡ 2 [MOD 17]: [n+14, n+15, …, n+30, n+32, n+31].

no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat
Proof uses: ite, Eq, HAdd.hAdd
6 instances, coercions and auxiliary constants left out.
```
def offB1b (i : Fin 19) : ℕ :=
…
```
def Usa1990P3.offA2 Offsets of the first circle when 13 ∣ n: [n+19, n+20, …, n+32] line 107 source
Source documentation
Offsets of the first circle when 13 ∣ n: [n+19, n+20, …, n+32].

no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat
Proof uses: HAdd.hAdd
5 instances, coercions and auxiliary constants left out.
```
def offA2 (i : Fin 14) : ℕ := i.val + 19
```
def Usa1990P3.offB2a Offsets of the second circle when 13 ∣ n and n ≢ 16 [MOD 17]: [n+1, n, n+2, n+3, …, n+18] line 111 source
Source documentation
Offsets of the second circle when 13 ∣ n and n ≢ 16 [MOD 17]: [n+1, n, n+2, n+3, …, n+18].

no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat
Proof uses: ite, Eq
4 instances, coercions and auxiliary constants left out.
```
def offB2a (i : Fin 19) : ℕ :=
…
```
def Usa1990P3.offB2b Offsets of the second circle when 13 ∣ n and n ≡ 16 [MOD 17]: [n, n+1, …, n+16, n+18, n+17] line 116 source
Source documentation
Offsets of the second circle when 13 ∣ n and n ≡ 16 [MOD 17]: [n, n+1, …, n+16, n+18, n+17].

no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat
Proof uses: ite, Eq
4 instances, coercions and auxiliary constants left out.
```
def offB2b (i : Fin 19) : ℕ :=
…
```
def Usa1990P3.a1 First circle when 13 ∤ n line 120 source
Source documentation
First circle when 13 ∤ n.

no axioms what this means
Statement uses: Nat, Fin, OfNat.ofNat
Proof uses: HAdd.hAdd, Usa1990P3.offA1
4 instances, coercions and auxiliary constants left out.
```
def a1 (n : ℕ) (i : Fin 14) : ℕ := n + offA1 i
```
Mentions: Usa1990P3.offA1
def Usa1990P3.b1a Second circle when 13 ∤ n and n ≢ 2 [MOD 17] line 123 source
Source documentation
Second circle when 13 ∤ n and n ≢ 2 [MOD 17].

no axioms what this means
Statement uses: Nat, Fin, OfNat.ofNat
Proof uses: HAdd.hAdd, Usa1990P3.offB1a
4 instances, coercions and auxiliary constants left out.
```
def b1a (n : ℕ) (i : Fin 19) : ℕ := n + offB1a i
```
Mentions: Usa1990P3.offB1a
def Usa1990P3.b1b Second circle when 13 ∤ n and n ≡ 2 [MOD 17] line 126 source
Source documentation
Second circle when 13 ∤ n and n ≡ 2 [MOD 17].

no axioms what this means
Statement uses: Nat, Fin, OfNat.ofNat
Proof uses: HAdd.hAdd, Usa1990P3.offB1b
4 instances, coercions and auxiliary constants left out.
```
def b1b (n : ℕ) (i : Fin 19) : ℕ := n + offB1b i
```
Mentions: Usa1990P3.offB1b
def Usa1990P3.a2 First circle when 13 ∣ n line 129 source
Source documentation
First circle when 13 ∣ n.

no axioms what this means
Statement uses: Nat, Fin, OfNat.ofNat
Proof uses: HAdd.hAdd, Usa1990P3.offA2
4 instances, coercions and auxiliary constants left out.
```
def a2 (n : ℕ) (i : Fin 14) : ℕ := n + offA2 i
```
Mentions: Usa1990P3.offA2
def Usa1990P3.b2a Second circle when 13 ∣ n and n ≢ 16 [MOD 17] line 132 source
Source documentation
Second circle when 13 ∣ n and n ≢ 16 [MOD 17].

no axioms what this means
Statement uses: Nat, Fin, OfNat.ofNat
Proof uses: HAdd.hAdd, Usa1990P3.offB2a
4 instances, coercions and auxiliary constants left out.
```
def b2a (n : ℕ) (i : Fin 19) : ℕ := n + offB2a i
```
Mentions: Usa1990P3.offB2a
def Usa1990P3.b2b Second circle when 13 ∣ n and n ≡ 16 [MOD 17] line 135 source
Source documentation
Second circle when 13 ∣ n and n ≡ 16 [MOD 17].

no axioms what this means
Statement uses: Nat, Fin, OfNat.ofNat
Proof uses: HAdd.hAdd, Usa1990P3.offB2b
4 instances, coercions and auxiliary constants left out.
```
def b2b (n : ℕ) (i : Fin 19) : ℕ := n + offB2b i
…
```
Mentions: Usa1990P3.offB2b
lemma Usa1990P3.offA1_injective line 141 source
no axioms what this means
Statement uses: Function.Injective, Fin, OfNat.ofNat, Nat, Usa1990P3.offA1
Proof uses: Eq, Fin.ext
2 instances, coercions and auxiliary constants left out.
lemma Usa1990P3.offA2_injective line 143 source
standard axioms: propext what this means
Statement uses: Function.Injective, Fin, OfNat.ofNat, Nat, Usa1990P3.offA2
Proof uses: Eq, Fin.ext, Nat.add_right_cancel
3 instances, coercions and auxiliary constants left out.
lemma Usa1990P3.offB1a_injective line 146 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Fin, OfNat.ofNat, Nat, Usa1990P3.offB1a
Proof uses: Eq, Fin.ext, Decidable, Not, Eq.mp, HAdd.hAdd, ite, congrArg, ite_eq_right, congrFun', ite_eq_left
16 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offB1b_injective line 152 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Fin, OfNat.ofNat, Nat, Usa1990P3.offB1b
Proof uses: Eq, Fin.ext, Decidable, Not, Eq.mp, HAdd.hAdd, ite, congrArg, ite_eq_right, congrFun', ite_eq_left
16 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offB2a_injective line 158 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Fin, OfNat.ofNat, Nat, Usa1990P3.offB2a
Proof uses: Eq, Fin.ext, Decidable, Not, Eq.mp, ite, congrArg, ite_eq_right, congrFun', ite_eq_left
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offB2b_injective line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Fin, OfNat.ofNat, Nat, Usa1990P3.offB2b
Proof uses: Eq, Fin.ext, Decidable, Not, Eq.mp, ite, congrArg, ite_eq_right, congrFun', ite_eq_left
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.injective_n_add Adding the same constant preserves injectivity line 171 source
Source documentation
Adding the same constant preserves injectivity.

standard axioms: propext what this means
Statement uses: Nat, Fin, Function.Injective, HAdd.hAdd
Proof uses: Eq, Nat.add_left_cancel
4 instances, coercions and auxiliary constants left out.
```
lemma injective_n_add {k : ℕ} {off : Fin k → ℕ} (h : Function.Injective off) (n : ℕ) :
    Function.Injective (fun i ↦ n + off i) :=
…
```
Mentions: h
lemma Usa1990P3.offA1_le line 175 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Usa1990P3.offA1
Proof uses: LT.lt, Fin.isLt, id
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offA1_le32 line 180 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Usa1990P3.offA1
Proof uses: LE.le.trans, Usa1990P3.offA1_le, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offA2_ge line 182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Usa1990P3.offA2
Proof uses: id
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offA2_le32 line 186 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Usa1990P3.offA2
Proof uses: LT.lt, Fin.isLt, id
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offB1a_ge line 191 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Usa1990P3.offB1a
Proof uses: id, Eq, Decidable, ite, HAdd.hAdd, Not, Eq.mpr, congrArg, ite_eq_right, ite_eq_left
12 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offB1a_le32 line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Usa1990P3.offB1a
Proof uses: LT.lt, Fin.isLt, id, Eq, Decidable, ite, HAdd.hAdd, Not, Eq.mpr, congrFun', congrArg, ite_eq_right, ite_eq_left
13 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offB1b_ge line 200 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Usa1990P3.offB1b
Proof uses: id, Eq, Decidable, ite, HAdd.hAdd, Not, Eq.mpr, congrArg, ite_eq_right, ite_eq_left
12 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offB1b_le32 line 204 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Usa1990P3.offB1b
Proof uses: LT.lt, Fin.isLt, id, Eq, Decidable, ite, HAdd.hAdd, Not, Eq.mpr, congrFun', congrArg, ite_eq_right, ite_eq_left
13 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offB2a_le18 line 209 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Usa1990P3.offB2a
Proof uses: LT.lt, Fin.isLt, id, Eq, Decidable, ite, Not, Eq.mpr, congrFun', congrArg, ite_eq_right, ite_eq_left
11 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offB2a_le32 line 214 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Usa1990P3.offB2a
Proof uses: LE.le.trans, Usa1990P3.offB2a_le18, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offB2b_le18 line 216 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Usa1990P3.offB2b
Proof uses: LT.lt, Fin.isLt, id, Eq, Decidable, ite, Not, Eq.mpr, congrFun', congrArg, ite_eq_right, ite_eq_left
11 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.offB2b_le32 line 221 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Usa1990P3.offB2b
Proof uses: LE.le.trans, Usa1990P3.offB2b_le18, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.image_add_off_subset_Icc If all offsets are at most 32, the image of fun i ↦ n + off i lies in Finset.Icc n (n + 32) line 229 source
Source documentation
If all offsets are at most 32, the image of fun i ↦ n + off i lies in Finset.Icc n (n + 32).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, LE.le, OfNat.ofNat, Finset, Finset.image, HAdd.hAdd, Finset.univ, Finset.Icc
Proof uses: Membership.mem, Eq, Exists, Eq.mp, Eq.trans, And, congrArg, funext, True, congrFun', true_and, Eq.mpr, id, And.intro, Nat.le_add_right
28 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma image_add_off_subset_Icc {k : ℕ} (off : Fin k → ℕ) (h : ∀ i, off i ≤ 32) (n : ℕ) :
    Finset.univ.image (fun i ↦ n + off i) ⊆ Finset.Icc n (n + 32) := by
…
```
Mentions: h
lemma Usa1990P3.disjoint_add_off If the offsets of two families are separated by a constant c, their images (after shifting by n) are disjoint line 241 source
Source documentation
If the offsets of two families are separated by a constant c, their images (after shifting by n) are disjoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, LE.le, LT.lt, Disjoint, Finset, Finset.image, HAdd.hAdd, Finset.univ
Proof uses: Eq.mpr, Membership.mem, Not, id, Eq, congrArg, propext, Finset.disjoint_left, Exists, False, Eq.mp, Eq.trans, And, funext, True, congrFun', true_and, Nat.add_left_cancel
23 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma disjoint_add_off {k l : ℕ} {off₁ : Fin k → ℕ} {off₂ : Fin l → ℕ} {c : ℕ}
    (h₁ : ∀ i, off₁ i ≤ c) (h₂ : ∀ j, c < off₂ j) (n : ℕ) :
    Disjoint (Finset.univ.image (fun i ↦ n + off₁ i))
      (Finset.univ.image (fun j ↦ n + off₂ j)) := by
…
```
lemma Usa1990P3.image_union_eq_Icc Two disjoint injective families of 14 and 19 elements inside the 33-element set Finset.Icc n (n + 32) must cover it line 257 source
Source documentation
Two disjoint injective families of 14 and 19 elements inside the 33-element set Finset.Icc n (n + 32) must cover it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Function.Injective, LE.le, Finset, Finset.image, Finset.univ, Finset.Icc, HAdd.hAdd, Disjoint, Eq, Union.union
Proof uses: Finset.eq_of_subset_of_card_le, Finset.union_subset, Eq.mpr, Finset.card, id, congrArg, Finset.card_union_of_disjoint, Finset.card_image_of_injective, Fintype.card, Finset.card_univ, Fintype.card_fin, HSub.hSub, Nat.card_Icc
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma image_union_eq_Icc {n : ℕ} {a : Fin 14 → ℕ} {b : Fin 19 → ℕ}
    (ha : Function.Injective a) (hb : Function.Injective b)
    (hsub₁ : Finset.univ.image a ⊆ Finset.Icc n (n + 32))
    (hsub₂ : Finset.univ.image b ⊆ Finset.Icc n (n + 32))
    (hdisj : Disjoint (Finset.univ.image a) (Finset.univ.image b)) :
    Finset.univ.image a ∪ Finset.univ.image b = Finset.Icc n (n + 32) := by
…
```
lemma Usa1990P3.validCircle_a1 line 273 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Dvd.dvd, OfNat.ofNat, Usa1990P3.ValidCircle, Usa1990P3.a1
Proof uses: id, Fin, Eq, HAdd.hAdd, Fin.last, LT.lt, Or, Nat.Coprime, eq_or_lt_of_le, Fin.le_last, Usa1990P3.coprime_add_prime_left, 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_3, Bool.false and 6 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.validCircle_b1a line 286 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Ne, HMod.hMod, OfNat.ofNat, Usa1990P3.ValidCircle, Usa1990P3.b1a
Proof uses: id, Fin, Eq, HAdd.hAdd, Fin.last, LT.lt, Or, Nat.Coprime, eq_or_lt_of_le, Fin.le_last, Usa1990P3.coprime_add_prime_left, 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_3, Bool.false and 18 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.validCircle_b1b line 315 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Eq, HMod.hMod, OfNat.ofNat, Usa1990P3.ValidCircle, Usa1990P3.b1b
Proof uses: id, Fin, HAdd.hAdd, Fin.last, LT.lt, Or, Nat.Coprime, eq_or_lt_of_le, Fin.le_last, Usa1990P3.coprime_add_prime_left, 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_3, Bool.false, Mathlib.Meta.NormNum.minFacHelper_0 and 16 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.validCircle_a2 line 343 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, OfNat.ofNat, Usa1990P3.ValidCircle, Usa1990P3.a2
Proof uses: id, Fin, Eq, HAdd.hAdd, Fin.last, LT.lt, Or, Nat.Coprime, eq_or_lt_of_le, Fin.le_last, Usa1990P3.coprime_add_prime_left, 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_3, Bool.false and 6 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.validCircle_b2a line 356 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Ne, HMod.hMod, OfNat.ofNat, Usa1990P3.ValidCircle, Usa1990P3.b2a
Proof uses: id, Fin, Eq, HAdd.hAdd, Fin.last, LT.lt, Or, Nat.Coprime, eq_or_lt_of_le, Fin.le_last, Usa1990P3.coprime_add_prime_left, 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_3, Bool.false and 18 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.validCircle_b2b line 386 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Eq, HMod.hMod, OfNat.ofNat, Usa1990P3.ValidCircle, Usa1990P3.b2b
Proof uses: id, Fin, HAdd.hAdd, Fin.last, LT.lt, Or, Nat.Coprime, eq_or_lt_of_le, Fin.le_last, Eq.mpr, congrArg, propext, Nat.coprime_comm, Usa1990P3.coprime_add_prime_right, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4 and 18 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
lemma Usa1990P3.case1a Case 13 ∤ n, n ≢ 2 [MOD 17] line 420 source
Source documentation
Case 13 ∤ n, n ≢ 2 [MOD 17].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Not, Dvd.dvd, OfNat.ofNat, Ne, HMod.hMod, Exists, Fin, And, Function.Injective, Disjoint, Finset, Finset.image, Finset.univ, Eq, Union.union, Finset.Icc, HAdd.hAdd, Usa1990P3.ValidCircle
Proof uses: Usa1990P3.offA1, Usa1990P3.injective_n_add, Usa1990P3.offA1_injective, Usa1990P3.offB1a, Usa1990P3.offB1a_injective, LE.le, Usa1990P3.image_add_off_subset_Icc, Usa1990P3.offA1_le32, Usa1990P3.offB1a_le32, Usa1990P3.a1, Usa1990P3.b1a, Usa1990P3.disjoint_add_off, Usa1990P3.offA1_le, Usa1990P3.offB1a_ge, Exists.intro, And.intro, Usa1990P3.image_union_eq_Icc, Usa1990P3.validCircle_a1, Usa1990P3.validCircle_b1a
32 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma case1a (n : ℕ) (hn : Odd n) (h13 : ¬ 13 ∣ n) (h17 : n % 17 ≠ 2) :
    ∃ a : Fin 14 → ℕ, ∃ b : Fin 19 → ℕ,
      Function.Injective a ∧ Function.Injective b ∧
      Disjoint (Finset.univ.image a) (Finset.univ.image b) ∧
      Finset.univ.image a ∪ Finset.univ.image b = Finset.Icc n (n + 32) ∧
      ValidCircle a ∧ ValidCircle b := by
…
```
Mentions: Usa1990P3.ValidCircle
lemma Usa1990P3.case1b Case 13 ∤ n, n ≡ 2 [MOD 17] line 437 source
Source documentation
Case 13 ∤ n, n ≡ 2 [MOD 17].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Not, Dvd.dvd, OfNat.ofNat, Eq, HMod.hMod, Exists, Fin, And, Function.Injective, Disjoint, Finset, Finset.image, Finset.univ, Union.union, Finset.Icc, HAdd.hAdd, Usa1990P3.ValidCircle
Proof uses: Usa1990P3.offA1, Usa1990P3.injective_n_add, Usa1990P3.offA1_injective, Usa1990P3.offB1b, Usa1990P3.offB1b_injective, LE.le, Usa1990P3.image_add_off_subset_Icc, Usa1990P3.offA1_le32, Usa1990P3.offB1b_le32, Usa1990P3.a1, Usa1990P3.b1b, Usa1990P3.disjoint_add_off, Usa1990P3.offA1_le, Usa1990P3.offB1b_ge, Exists.intro, And.intro, Usa1990P3.image_union_eq_Icc, Usa1990P3.validCircle_a1, Usa1990P3.validCircle_b1b
32 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma case1b (n : ℕ) (hn : Odd n) (h13 : ¬ 13 ∣ n) (h17 : n % 17 = 2) :
    ∃ a : Fin 14 → ℕ, ∃ b : Fin 19 → ℕ,
      Function.Injective a ∧ Function.Injective b ∧
      Disjoint (Finset.univ.image a) (Finset.univ.image b) ∧
      Finset.univ.image a ∪ Finset.univ.image b = Finset.Icc n (n + 32) ∧
      ValidCircle a ∧ ValidCircle b := by
…
```
Mentions: Usa1990P3.ValidCircle
lemma Usa1990P3.case2a Case 13 ∣ n, n ≢ 16 [MOD 17] line 454 source
Source documentation
Case 13 ∣ n, n ≢ 16 [MOD 17].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Dvd.dvd, OfNat.ofNat, Ne, HMod.hMod, Exists, Fin, And, Function.Injective, Disjoint, Finset, Finset.image, Finset.univ, Eq, Union.union, Finset.Icc, HAdd.hAdd, Usa1990P3.ValidCircle
Proof uses: Usa1990P3.offA2, Usa1990P3.injective_n_add, Usa1990P3.offA2_injective, Usa1990P3.offB2a, Usa1990P3.offB2a_injective, LE.le, Usa1990P3.image_add_off_subset_Icc, Usa1990P3.offA2_le32, Usa1990P3.offB2a_le32, Usa1990P3.a2, Usa1990P3.b2a, Disjoint.symm, Usa1990P3.disjoint_add_off, Usa1990P3.offB2a_le18, Usa1990P3.offA2_ge, Exists.intro, And.intro, Usa1990P3.image_union_eq_Icc, Usa1990P3.validCircle_a2, Usa1990P3.validCircle_b2a
32 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma case2a (n : ℕ) (hn : Odd n) (h13 : 13 ∣ n) (h17 : n % 17 ≠ 16) :
    ∃ a : Fin 14 → ℕ, ∃ b : Fin 19 → ℕ,
      Function.Injective a ∧ Function.Injective b ∧
      Disjoint (Finset.univ.image a) (Finset.univ.image b) ∧
      Finset.univ.image a ∪ Finset.univ.image b = Finset.Icc n (n + 32) ∧
      ValidCircle a ∧ ValidCircle b := by
…
```
Mentions: Usa1990P3.ValidCircle
lemma Usa1990P3.case2b Case 13 ∣ n, n ≡ 16 [MOD 17] line 471 source
Source documentation
Case 13 ∣ n, n ≡ 16 [MOD 17].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Dvd.dvd, OfNat.ofNat, Eq, HMod.hMod, Exists, Fin, And, Function.Injective, Disjoint, Finset, Finset.image, Finset.univ, Union.union, Finset.Icc, HAdd.hAdd, Usa1990P3.ValidCircle
Proof uses: Usa1990P3.offA2, Usa1990P3.injective_n_add, Usa1990P3.offA2_injective, Usa1990P3.offB2b, Usa1990P3.offB2b_injective, LE.le, Usa1990P3.image_add_off_subset_Icc, Usa1990P3.offA2_le32, Usa1990P3.offB2b_le32, Usa1990P3.a2, Usa1990P3.b2b, Disjoint.symm, Usa1990P3.disjoint_add_off, Usa1990P3.offB2b_le18, Usa1990P3.offA2_ge, Exists.intro, And.intro, Usa1990P3.image_union_eq_Icc, Usa1990P3.validCircle_a2, Usa1990P3.validCircle_b2b
32 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma case2b (n : ℕ) (hn : Odd n) (h13 : 13 ∣ n) (h17 : n % 17 = 16) :
    ∃ a : Fin 14 → ℕ, ∃ b : Fin 19 → ℕ,
      Function.Injective a ∧ Function.Injective b ∧
      Disjoint (Finset.univ.image a) (Finset.univ.image b) ∧
      Finset.univ.image a ∪ Finset.univ.image b = Finset.Icc n (n + 32) ∧
      ValidCircle a ∧ ValidCircle b := by
…
```
Mentions: Usa1990P3.ValidCircle
problem Usa1990P3.usa1990_p3 line 491 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, LT.lt, OfNat.ofNat, Exists, Fin, And, Function.Injective, Disjoint, Finset, Finset.image, Finset.univ, Eq, Union.union, Finset.Icc, HAdd.hAdd, Usa1990P3.ValidCircle
Proof uses: dite, Dvd.dvd, HMod.hMod, Usa1990P3.case2b, Not, Usa1990P3.case2a, Usa1990P3.case1b, Usa1990P3.case1a
30 instances, coercions and auxiliary constants left out.

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