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

61 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2017, Problem 6

A point (x,y) ∈ ℤ × ℤ is called primitive if gcd(x,y) = 1. Let S be a finite set of primitive points. Prove that there exists n > 0 and integers a₀,a₁,...,aₙ such that

a₀xⁿ + a₁xⁿ⁻¹y + a₂xⁿ⁻²y² + ... + aₙ₋₁xyⁿ⁻¹ + aₙyⁿ = 1

for each (x,y) ∈ S.

Imports (4)

Imported by 1 file

Compfiles.lean

structure Imo2017P6.HForm A homogeneous polynomial in two variables with integer coefficients, represented by its degree and coefficient function line 38 source
Source documentation
A homogeneous polynomial in two variables with integer coefficients, represented by its degree and coefficient function. Evaluation is ∑ i ∈ range (deg + 1), coeff i * x^i * y^(deg - i).

no axioms what this means
```
structure HForm where
…
```
def Imo2017P6.HForm.eval Evaluation of a homogeneous form at a point line 45 source
Source documentation
Evaluation of a homogeneous form at a point.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P6.HForm, Int
Proof uses: Finset.sum, Nat, Finset.range, HAdd.hAdd, Imo2017P6.HForm.deg, OfNat.ofNat, HMul.hMul, Imo2017P6.HForm.coeff, HPow.hPow, HSub.hSub
12 instances, coercions and auxiliary constants left out.
```
def eval (f : HForm) (x y : ℤ) : ℤ :=
…
```
Mentions: f, Imo2017P6.HForm
def Imo2017P6.HForm.const The constant form line 49 source
Source documentation
The constant form.

no axioms what this means
Statement uses: Int, Imo2017P6.HForm
Proof uses: Imo2017P6.HForm.mk, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
```
def const (c : ℤ) : HForm := ⟨0, fun _ => c⟩
```
Mentions: Imo2017P6.HForm
def Imo2017P6.HForm.linear The linear form α * x + β * y line 52 source
Source documentation
The linear form α * x + β * y.

no axioms what this means
Statement uses: Int, Imo2017P6.HForm
Proof uses: Imo2017P6.HForm.mk, OfNat.ofNat, Nat, ite, Eq
2 instances, coercions and auxiliary constants left out.
```
def linear (α β : ℤ) : HForm := ⟨1, fun i => if i = 0 then β else α⟩
```
Mentions: Imo2017P6.HForm
def Imo2017P6.HForm.trunc Coefficient function truncated above the degree line 55 source
Source documentation
Coefficient function truncated above the degree.

no axioms what this means
Statement uses: Imo2017P6.HForm, Nat, Int
Proof uses: ite, LE.le, Imo2017P6.HForm.deg, Imo2017P6.HForm.coeff, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
def trunc (f : HForm) : ℕ → ℤ := fun i => if i ≤ f.deg then f.coeff i else 0
```
Mentions: f, Imo2017P6.HForm
lemma Imo2017P6.HForm.trunc_of_le line 57 source
no axioms what this means
Statement uses: Imo2017P6.HForm, Nat, LE.le, Imo2017P6.HForm.deg, Eq, Int, Imo2017P6.HForm.trunc, Imo2017P6.HForm.coeff
Proof uses: ite_eq_left, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
lemma Imo2017P6.HForm.trunc_of_lt line 60 source
no axioms what this means
Statement uses: Imo2017P6.HForm, Nat, LT.lt, Imo2017P6.HForm.deg, Eq, Int, Imo2017P6.HForm.trunc, OfNat.ofNat
Proof uses: ite_eq_right, LE.le, Iff.mpr, Not, not_le, Imo2017P6.HForm.coeff
10 instances, coercions and auxiliary constants left out.
lemma Imo2017P6.HForm.eval_const line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Imo2017P6.HForm.eval, Imo2017P6.HForm.const
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.sum, Nat, Finset.range, HAdd.hAdd, Imo2017P6.HForm.deg, OfNat.ofNat, HMul.hMul, Imo2017P6.HForm.coeff, HPow.hPow, HSub.hSub, Singleton.singleton, Finset, congr, zero_add, funext and 5 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.HForm.eval_linear line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Imo2017P6.HForm.eval, Imo2017P6.HForm.linear, HAdd.hAdd, HMul.hMul
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, Finset.sum, Nat, Finset.range, OfNat.ofNat, Imo2017P6.HForm.coeff, HPow.hPow, HSub.hSub, Imo2017P6.HForm.deg, ite, funext, ite_mul, Finset.sum_range_succ, congr, Singleton.singleton, Finset and 30 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.HForm.eval_eq_trunc line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P6.HForm, Int, Eq, Imo2017P6.HForm.eval, Finset.sum, Nat, Finset.range, HAdd.hAdd, Imo2017P6.HForm.deg, OfNat.ofNat, HMul.hMul, Imo2017P6.HForm.trunc, HPow.hPow, HSub.hSub
Proof uses: Finset.sum_congr, Imo2017P6.HForm.coeff, rfl, Finset, Membership.mem, Eq.mpr, id, congrArg, Imo2017P6.HForm.trunc_of_le, Eq.mp, LT.lt, Nat.succ, LE.le, propext, Nat.lt_succ_iff, Finset.mem_range, Eq.refl
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.HForm.cauchy_sum The Cauchy product formula for finite sums with vanishing tails line 78 source
Source documentation
The Cauchy product formula for finite sums with vanishing tails.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LT.lt, Eq, OfNat.ofNat, HMul.hMul, Finset.sum, Finset.range, HAdd.hAdd, HSub.hSub
Proof uses: Prod, Finset.filter, Prod.fst, Prod.snd, SProd.sprod, Finset, Eq.mpr, Finset.HasAntidiagonal.antidiagonal, id, congrArg, Nat.succ, Eq.symm, Finset.Nat.sum_antidiagonal_eq_sum_range_succ, Finset.sum_subset, Membership.mem, Iff.mpr, Finset.HasAntidiagonal.mem_antidiagonal, And.right, Eq.mp, And and 16 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma cauchy_sum (m n : ℕ) (u v : ℕ → ℤ) (hu : ∀ i, m < i → u i = 0)
    (hv : ∀ j, n < j → v j = 0) :
    (∑ i ∈ Finset.range (m + 1), u i) * (∑ j ∈ Finset.range (n + 1), v j) =
    ∑ k ∈ Finset.range (m + n + 1), ∑ i ∈ Finset.range (k + 1), u i * v (k - i) := by
…
```
def Imo2017P6.HForm.mul Multiplication of homogeneous forms (degrees add) line 120 source
Source documentation
Multiplication of homogeneous forms (degrees add).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P6.HForm
Proof uses: Imo2017P6.HForm.mk, HAdd.hAdd, Nat, Imo2017P6.HForm.deg, Finset.sum, Int, Finset.range, OfNat.ofNat, HMul.hMul, Imo2017P6.HForm.trunc, HSub.hSub
8 instances, coercions and auxiliary constants left out.
```
def mul (f g : HForm) : HForm where
…
```
Mentions: f, Imo2017P6.HForm
lemma Imo2017P6.HForm.eval_mul line 124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P6.HForm, Int, Eq, Imo2017P6.HForm.eval, Imo2017P6.HForm.mul, HMul.hMul
Proof uses: Eq.mpr, Finset.sum, Nat, Finset.range, HAdd.hAdd, Imo2017P6.HForm.deg, OfNat.ofNat, Imo2017P6.HForm.trunc, HPow.hPow, HSub.hSub, id, congrArg, Imo2017P6.HForm.eval_eq_trunc, Imo2017P6.HForm.cauchy_sum, LT.lt, Imo2017P6.HForm.trunc_of_lt, MulZeroClass.zero_mul, Eq.refl, congrFun', Finset.sum_congr and 43 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
def Imo2017P6.HForm.pow Powers of a homogeneous form line 152 source
Source documentation
Powers of a homogeneous form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P6.HForm, Nat
2 instances, coercions and auxiliary constants left out.
```
def pow (f : HForm) : ℕ → HForm
  | 0 => const 1
  | n + 1 => mul (pow f n) f
```
Mentions: f, Imo2017P6.HForm, Imo2017P6.HForm.const, Imo2017P6.HForm.mul
lemma Imo2017P6.HForm.pow_deg line 156 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P6.HForm, Nat, Eq, Imo2017P6.HForm.deg, Imo2017P6.HForm.pow, HMul.hMul
6 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.HForm.eval_pow line 163 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P6.HForm, Nat, Int, Eq, Imo2017P6.HForm.eval, Imo2017P6.HForm.pow, HPow.hPow
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Imo2017P6.HForm.add Addition of two forms of the same degree line 170 source
Source documentation
Addition of two forms of the same degree.

no axioms what this means
Statement uses: Imo2017P6.HForm, Eq, Nat, Imo2017P6.HForm.deg
Proof uses: Imo2017P6.HForm.mk, HAdd.hAdd, Int, Imo2017P6.HForm.coeff
2 instances, coercions and auxiliary constants left out.
```
def add (f g : HForm) (_h : f.deg = g.deg) : HForm :=
…
```
Mentions: f, Imo2017P6.HForm
lemma Imo2017P6.HForm.eval_add line 173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P6.HForm, Eq, Nat, Imo2017P6.HForm.deg, Int, Imo2017P6.HForm.eval, Imo2017P6.HForm.add, HAdd.hAdd
Proof uses: Finset.sum, Finset.range, OfNat.ofNat, HMul.hMul, Imo2017P6.HForm.coeff, HPow.hPow, HSub.hSub, Eq.mpr, id, congrArg, Eq.refl, Eq.symm, Finset.sum_add_distrib, Finset.sum_congr, rfl, Finset, Membership.mem, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr and 21 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def Imo2017P6.HForm.neg Negation of a form line 188 source
Source documentation
Negation of a form.

no axioms what this means
Statement uses: Imo2017P6.HForm
Proof uses: Imo2017P6.HForm.mk, Imo2017P6.HForm.deg, Nat, Neg.neg, Int, Imo2017P6.HForm.coeff
1 instances, coercions and auxiliary constants left out.
```
def neg (f : HForm) : HForm := ⟨f.deg, fun i => -f.coeff i⟩
```
Mentions: f, Imo2017P6.HForm
lemma Imo2017P6.HForm.eval_neg line 190 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P6.HForm, Int, Eq, Imo2017P6.HForm.eval, Imo2017P6.HForm.neg, Neg.neg
Proof uses: Nat, HMul.hMul, Imo2017P6.HForm.coeff, HPow.hPow, HSub.hSub, Imo2017P6.HForm.deg, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, OfNat.ofNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id and 38 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Imo2017P6.HForm.sub Subtraction of two forms of the same degree line 196 source
Source documentation
Subtraction of two forms of the same degree.

standard axioms: propext what this means
Statement uses: Imo2017P6.HForm, Eq, Nat, Imo2017P6.HForm.deg
Proof uses: Imo2017P6.HForm.add, Imo2017P6.HForm.neg
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def sub (f g : HForm) (h : f.deg = g.deg) : HForm := f.add g.neg (by simp [neg, h])
```
Mentions: f, Imo2017P6.HForm, h, Imo2017P6.HForm.neg
lemma Imo2017P6.HForm.sub_deg line 198 source
standard axioms: propext what this means
Statement uses: Imo2017P6.HForm, Eq, Nat, Imo2017P6.HForm.deg, Imo2017P6.HForm.sub
Proof uses: rfl
lemma Imo2017P6.HForm.eval_sub line 200 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P6.HForm, Eq, Nat, Imo2017P6.HForm.deg, Int, Imo2017P6.HForm.eval, Imo2017P6.HForm.sub, HSub.hSub
Proof uses: of_eq_true, Eq.trans, HAdd.hAdd, Neg.neg, True, congr, congrArg, Imo2017P6.HForm.add, Imo2017P6.HForm.neg, Imo2017P6.HForm.eval_add, Imo2017P6.HForm.eval_neg, sub_eq_add_neg, eq_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2017P6.HForm.cmul Scalar multiplication of a form by an integer line 205 source
Source documentation
Scalar multiplication of a form by an integer.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Imo2017P6.HForm
Proof uses: Imo2017P6.HForm.mul, Imo2017P6.HForm.const
```
def cmul (c : ℤ) (f : HForm) : HForm := mul (const c) f
```
Mentions: f, Imo2017P6.HForm, Imo2017P6.HForm.mul, Imo2017P6.HForm.const
lemma Imo2017P6.HForm.cmul_deg line 207 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Imo2017P6.HForm, Eq, Nat, Imo2017P6.HForm.deg, Imo2017P6.HForm.cmul
Proof uses: zero_add
2 instances, coercions and auxiliary constants left out.
lemma Imo2017P6.HForm.eval_cmul line 209 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Imo2017P6.HForm, Eq, Imo2017P6.HForm.eval, Imo2017P6.HForm.cmul, HMul.hMul
Proof uses: id, Eq.mpr, Imo2017P6.HForm.mul, Imo2017P6.HForm.const, congrArg, Imo2017P6.HForm.eval_mul, Imo2017P6.HForm.eval_const, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2017P6.HForm.sum Sum of a family of forms of the same degree line 214 source
Source documentation
Sum of a family of forms of the same degree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2017P6.HForm, Nat, Membership.mem, Eq, Imo2017P6.HForm.deg
Proof uses: Imo2017P6.HForm.mk, Finset.sum, Int, Imo2017P6.HForm.coeff
5 instances, coercions and auxiliary constants left out.
```
def sum {ι : Type*} (s : Finset ι) (F : ι → HForm) (n : ℕ)
    (_h : ∀ i ∈ s, (F i).deg = n) : HForm :=
…
```
Mentions: Imo2017P6.HForm
lemma Imo2017P6.HForm.sum_deg line 218 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2017P6.HForm, Nat, Membership.mem, Eq, Imo2017P6.HForm.deg, Imo2017P6.HForm.sum
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma Imo2017P6.HForm.eval_sum line 221 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2017P6.HForm, Nat, Membership.mem, Eq, Imo2017P6.HForm.deg, Int, Imo2017P6.HForm.eval, Imo2017P6.HForm.sum, Finset.sum
Proof uses: Eq.mpr, Finset.range, HAdd.hAdd, OfNat.ofNat, HMul.hMul, Imo2017P6.HForm.coeff, HPow.hPow, HSub.hSub, id, congrFun', congrArg, funext, Eq.trans, Finset.sum_mul, Finset.sum_comm, Finset.sum_congr, rfl, Eq.refl
25 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.HForm.exists_prod Products of families of homogeneous forms exist with the expected degree and evaluation line 232 source
Source documentation
Products of families of homogeneous forms exist with the expected degree and evaluation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2017P6.HForm, Exists, And, Eq, Nat, Imo2017P6.HForm.deg, Finset.sum, Int, Imo2017P6.HForm.eval, Finset.prod
Proof uses: Finset.induction_on, Classical.propDecidable, Exists.intro, EmptyCollection.emptyCollection, Imo2017P6.HForm.const, OfNat.ofNat, And.intro, Eq.mpr, id, congrArg, Finset.sum_empty, Eq.refl, Imo2017P6.HForm.eval_const, Finset.prod_empty, Not, Membership.mem, Insert.insert, Imo2017P6.HForm.mul, HAdd.hAdd, Finset.sum_insert and 5 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma exists_prod {ι : Type*} (s : Finset ι) (F : ι → HForm) :
    ∃ G : HForm, G.deg = ∑ i ∈ s, (F i).deg ∧
      ∀ x y, G.eval x y = ∏ i ∈ s, (F i).eval x y := by
…
```
Mentions: Imo2017P6.HForm, Imo2017P6.HForm.eval
lemma Imo2017P6.HForm.eval_neg_of_even Evaluation at the antipode of a form of even degree line 249 source
Source documentation
Evaluation at the antipode of a form of even degree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P6.HForm, Even, Nat, Imo2017P6.HForm.deg, Int, Eq, Imo2017P6.HForm.eval, Neg.neg
Proof uses: Finset.sum_congr, Finset.range, HAdd.hAdd, OfNat.ofNat, HMul.hMul, Imo2017P6.HForm.coeff, HPow.hPow, HSub.hSub, rfl, Finset, Membership.mem, Eq.mpr, id, congrArg, Nat.add_sub_cancel', Eq.mp, LT.lt, Nat.succ, LE.le, propext and 44 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma eval_neg_of_even (f : HForm) (hfe : Even f.deg) (x y : ℤ) :
    f.eval (-x) (-y) = f.eval x y := by
…
```
Mentions: f, Imo2017P6.HForm
def Imo2017P6.canon Canonical orientation of a nonzero lattice point: exactly one of s, -s satisfies canon s line 266 source
Source documentation
Canonical orientation of a nonzero lattice point: exactly one of s, -s satisfies canon s.

no axioms what this means
Statement uses: Prod, Int
Proof uses: Or, LT.lt, OfNat.ofNat, Prod.fst, And, Eq, Prod.snd
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def canon (s : ℤ × ℤ) : Prop := 0 < s.1 ∨ (s.1 = 0 ∧ 0 < s.2)
```
instance Imo2017P6.(instance at line 268) line 268 source
lemma Imo2017P6.canon_iff_not_neg line 272 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Ne, Prod.mk, OfNat.ofNat, Iff, Imo2017P6.canon, Not, Neg.neg
Proof uses: Eq, Prod.fst, rfl, Prod.snd, And, Prod.ext, And.left, And.right, id, Eq.mpr, Or, LT.lt, congrArg, Iff.intro, False, dite, Or.inr, And.intro, False.elim, Or.inl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
def Imo2017P6.rep Representative of the antipodal class of s, chosen inside S whenever possible line 298 source
Source documentation
Representative of the antipodal class of s, chosen inside S whenever possible.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: ite, And, Imo2017P6.canon, Membership.mem, Neg.neg
9 instances, coercions and auxiliary constants left out.
```
def rep (S : Finset (ℤ × ℤ)) (s : ℤ × ℤ) : ℤ × ℤ :=
…
```
Mentions: S
lemma Imo2017P6.rep_mem line 301 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2017P6.rep
Proof uses: id, dite, ite, And, Imo2017P6.canon, Neg.neg, Eq.mpr, Eq, congrArg, ite_eq_left, Not, ite_eq_right, And.right
11 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.rep_eq_self_or_neg line 310 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Or, Eq, Imo2017P6.rep, Neg.neg
Proof uses: id, dite, ite, And, Imo2017P6.canon, Membership.mem, Eq.mpr, congrArg, ite_eq_left, Or.inl, rfl, Not, ite_eq_right, Or.symm, ite_eq_or_eq
11 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.rep_neg line 318 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Neg.neg, Ne, Prod.mk, OfNat.ofNat, Eq, Imo2017P6.rep
Proof uses: Iff, Imo2017P6.canon, Not, Imo2017P6.canon_iff_not_neg, dite, Iff.mp, id, Eq.mpr, ite, And, congrArg, ite_eq_left, And.intro, Eq.refl, ite_eq_right, And.left, neg_neg, Decidable.byContradiction, Iff.mpr
26 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.rep_idem line 341 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Ne, Prod.mk, OfNat.ofNat, Eq, Imo2017P6.rep
Proof uses: Neg.neg, Or, Imo2017P6.rep_eq_self_or_neg, Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Imo2017P6.rep_mem, Eq.mp, Trans.trans, Imo2017P6.rep_neg
10 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Imo2017P6.T The set of antipodal class representatives of S line 353 source
Source documentation
The set of antipodal class representatives of S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: Finset.image, Imo2017P6.rep
2 instances, coercions and auxiliary constants left out.
```
def T (S : Finset (ℤ × ℤ)) : Finset (ℤ × ℤ) := S.image (rep S)
```
Mentions: S, Imo2017P6.rep
lemma Imo2017P6.T_subset line 355 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, LE.le, Imo2017P6.T
Proof uses: Membership.mem, And, Eq, Imo2017P6.rep, Exists, Eq.mp, Finset.image, congrArg, propext, Finset.mem_image, Imo2017P6.T.eq_1, Imo2017P6.rep_mem
10 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.rep_mem_T line 361 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2017P6.T, Imo2017P6.rep
Proof uses: Finset.mem_image_of_mem
6 instances, coercions and auxiliary constants left out.
lemma Imo2017P6.rep_spec line 364 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Or, Eq, Imo2017P6.rep, Neg.neg
Proof uses: Imo2017P6.rep_eq_self_or_neg, Or.inl, Eq.symm, Or.inr, Eq.mpr, id, congrArg, neg_neg, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.ne_zero_of_isCoprime line 370 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, IsCoprime, Prod.fst, Prod.snd, Ne, Prod.mk, OfNat.ofNat
Proof uses: Eq, False, id, False.elim, Eq.mp, Nat, Int.gcd, Eq.trans, congrFun', congrArg, Int.gcd_self, propext, Int.isCoprime_iff_gcd_eq_one, Eq.symm
11 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.T_ne_neg line 377 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, IsCoprime, Prod.fst, Prod.snd, Imo2017P6.T, Ne, Neg.neg
Proof uses: Eq, And, Imo2017P6.rep, Exists, False, Eq.mp, Finset.image, congrArg, propext, Finset.mem_image, Imo2017P6.T.eq_1, Prod.mk, OfNat.ofNat, Imo2017P6.ne_zero_of_isCoprime, Imo2017P6.rep_mem, Trans.trans, Eq.symm, Imo2017P6.rep_idem, Eq.mpr, id and 2 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.eq_or_neg_of_mul_eq If two primitive points have cross-product zero, they are equal or antipodal line 396 source
Source documentation
If two primitive points have cross-product zero, they are equal or antipodal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, IsCoprime, Eq, HMul.hMul, Or, And, Neg.neg
Proof uses: Dvd.dvd, IsCoprime.dvd_of_dvd_mul_left, Exists.intro, Eq.mpr, id, congrArg, mul_comm, Eq.symm, IsCoprime.symm, Nat, Int.natAbs, Iff.mpr, Int.natAbs_dvd_natAbs, Iff.mp, Int.natAbs_eq_natAbs_iff, Nat.dvd_antisymm, Or.inl, And.intro, OfNat.ofNat, Mathlib.Tactic.LinearCombination.eq_of_eq and 58 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 66 steps
Open to load the checked before-and-after goal states.
```
lemma eq_or_neg_of_mul_eq {x₁ y₁ x₂ y₂ : ℤ} (h₁ : IsCoprime x₁ y₁) (h₂ : IsCoprime x₂ y₂)
    (h : x₁ * y₂ = x₂ * y₁) : (x₁ = x₂ ∧ y₁ = y₂) ∨ (x₁ = -x₂ ∧ y₁ = -y₂) := by
…
```
Mentions: h
lemma Imo2017P6.det_ne_zero Points of distinct classes in T have nonzero determinant line 440 source
Source documentation
Points of distinct classes in T have nonzero determinant.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, IsCoprime, Prod.fst, Prod.snd, Imo2017P6.T, Ne, HSub.hSub, HMul.hMul, OfNat.ofNat
Proof uses: Eq, Imo2017P6.T_subset, Iff.mp, sub_eq_zero, Trans.trans, mul_comm, And, Neg.neg, Or, False, Imo2017P6.eq_or_neg_of_mul_eq, Prod.ext, Eq.symm, Eq.mpr, id, congrArg, neg_neg, Eq.refl, Imo2017P6.T_ne_neg
42 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma det_ne_zero {S : Finset (ℤ × ℤ)} (hS : ∀ s ∈ S, IsCoprime s.1 s.2) {t t' : ℤ × ℤ}
    (ht : t ∈ T S) (ht' : t' ∈ T S) (hne : t' ≠ t) :
    t'.2 * t.1 - t'.1 * t.2 ≠ 0 := by
…
```
Mentions: S, Imo2017P6.T
def Imo2017P6.Xf The coordinate form x line 458 source
Source documentation
The coordinate form x.

no axioms what this means
Statement uses: Imo2017P6.HForm
Proof uses: Imo2017P6.HForm.linear, OfNat.ofNat, Int
1 instances, coercions and auxiliary constants left out.
```
def Xf : HForm := HForm.linear 1 0
```
Mentions: Imo2017P6.HForm, Imo2017P6.HForm.linear
def Imo2017P6.Yf The coordinate form y line 461 source
Source documentation
The coordinate form y.

no axioms what this means
Statement uses: Imo2017P6.HForm
Proof uses: Imo2017P6.HForm.linear, OfNat.ofNat, Int
1 instances, coercions and auxiliary constants left out.
```
def Yf : HForm := HForm.linear 0 1
```
Mentions: Imo2017P6.HForm, Imo2017P6.HForm.linear
lemma Imo2017P6.Xf_eval line 463 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Imo2017P6.HForm.eval, Imo2017P6.Xf
Proof uses: Eq.mpr, Imo2017P6.HForm.linear, OfNat.ofNat, id, congrArg, Imo2017P6.HForm, Imo2017P6.Xf.eq_1, HAdd.hAdd, HMul.hMul, Imo2017P6.HForm.eval_linear, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf and 12 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.Yf_eval line 467 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Imo2017P6.HForm.eval, Imo2017P6.Yf
Proof uses: Eq.mpr, Imo2017P6.HForm.linear, OfNat.ofNat, id, congrArg, Imo2017P6.HForm, Imo2017P6.Yf.eq_1, HAdd.hAdd, HMul.hMul, Imo2017P6.HForm.eval_linear, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf and 13 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.Xf_deg line 471 source
no axioms what this means
Statement uses: Eq, Nat, Imo2017P6.HForm.deg, Imo2017P6.Xf, OfNat.ofNat
Proof uses: rfl
1 instances, coercions and auxiliary constants left out.
lemma Imo2017P6.Yf_deg line 473 source
no axioms what this means
Statement uses: Eq, Nat, Imo2017P6.HForm.deg, Imo2017P6.Yf, OfNat.ofNat
Proof uses: rfl
1 instances, coercions and auxiliary constants left out.
lemma Imo2017P6.not_coprime_of_both_dvd line 475 source
standard axioms: propext what this means
Statement uses: Int, IsCoprime, Dvd.dvd, OfNat.ofNat
Proof uses: Exists, Eq, HAdd.hAdd, HMul.hMul, Eq.mpr, id, congrArg, Eq.symm, Dvd.dvd.linear_comb
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.two_not_dvd_quad_zmod In ZMod 2, the form x² + xy + y² does not vanish at a primitive point line 482 source
Source documentation
In ZMod 2, the form x² + xy + y² does not vanish at a primitive point.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, IsCoprime, Ne, ZMod, OfNat.ofNat, Nat, HAdd.hAdd, HPow.hPow, HMul.hMul
Proof uses: Eq, Not, And, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, False, Dvd.dvd, Iff.mp, ZMod.intCast_zmod_eq_zero_iff_dvd, Imo2017P6.not_coprime_of_both_dvd, False.elim, Eq.mp, eq_false, Mathlib.Meta.NormNum.isInt_dvd_false, Int.ofNat, Mathlib.Meta.NormNum.IsNat.to_isInt and 8 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma two_not_dvd_quad_zmod {x y : ℤ} (h : IsCoprime x y) :
    ((x ^ 2 + x * y + y ^ 2 : ℤ) : ZMod 2) ≠ 0 := by
…
```
Mentions: h
lemma Imo2017P6.odd_not_dvd_powsum_zmod In ZMod p for an odd prime p, the form x^(p-1) + y^(p-1) does not vanish at a primitive point line 497 source
Source documentation
In ZMod p for an odd prime p, the form x^(p-1) + y^(p-1) does not vanish at a primitive point.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Ne, OfNat.ofNat, Int, IsCoprime, ZMod, HAdd.hAdd, HPow.hPow, HSub.hSub
Proof uses: LE.le, Nat.Prime.two_le, Fact, Fact.mk, Eq, Not, Dvd.dvd, Iff.mp, ZMod.intCast_zmod_eq_zero_iff_dvd, Imo2017P6.not_coprime_of_both_dvd, Nat.le_of_dvd, one_pos, Eq.mp, congrArg, propext, Int.natCast_dvd_natCast, Eq.mpr, id, Eq.trans, congrFun' and 21 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
```
lemma odd_not_dvd_powsum_zmod {p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2) {x y : ℤ}
    (h : IsCoprime x y) : ((x ^ (p - 1) + y ^ (p - 1) : ℤ) : ZMod p) ≠ 0 := by
…
```
Mentions: h
def Imo2017P6.Gform The local form used modulo the prime p: x² + xy + y² for p = 2 and x^(p-1) + y^(p-1) for odd p line 540 source
Source documentation
The local form used modulo the prime p: x² + xy + y² for p = 2 and x^(p-1) + y^(p-1) for odd p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2017P6.HForm
Proof uses: ite, Eq, OfNat.ofNat, Imo2017P6.HForm.add, Imo2017P6.HForm.pow, Imo2017P6.Xf, Imo2017P6.HForm.mul, Imo2017P6.Yf, HSub.hSub
7 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
def Gform (p : ℕ) : HForm :=
…
```
Mentions: Imo2017P6.HForm
lemma Imo2017P6.Gform_deg line 549 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo2017P6.HForm.deg, Imo2017P6.Gform, ite, OfNat.ofNat, HSub.hSub
Proof uses: Eq.mpr, Imo2017P6.HForm, Imo2017P6.HForm.add, Imo2017P6.HForm.pow, Imo2017P6.Xf, Imo2017P6.HForm.mul, Imo2017P6.Yf, id, congrArg, Imo2017P6.Gform.eq_1, dite, congr, ite_eq_left, HMul.hMul, Imo2017P6.HForm.pow_deg, Imo2017P6.Xf_deg, Eq.refl, Not, ite_eq_right, mul_one
18 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.Gform_eval_zmod line 557 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Int, IsCoprime, Ne, ZMod, Imo2017P6.HForm.eval, Imo2017P6.Gform, OfNat.ofNat
Proof uses: Eq.mpr, ite, Imo2017P6.HForm, Eq, Imo2017P6.HForm.add, Imo2017P6.HForm.pow, Imo2017P6.Xf, Imo2017P6.HForm.mul, Imo2017P6.Yf, HSub.hSub, id, congrArg, Imo2017P6.Gform.eq_1, dite, ite_eq_left, rfl, HAdd.hAdd, Imo2017P6.HForm.eval_add, HPow.hPow, Imo2017P6.HForm.eval_pow and 10 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P6.exists_g Documented declaration: exists_g line 571 source
Source documentation
The key construction: a homogeneous form g of positive even degree whose value at every point of T S is nonzero and not divisible by any prime dividing D (the product of all inter-class determinants).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, IsCoprime, Prod.fst, Prod.snd, Finset.Nonempty, Imo2017P6.T, Exists, Imo2017P6.HForm, And, Even, Nat, Imo2017P6.HForm.deg, LT.lt, OfNat.ofNat, Ne, Imo2017P6.HForm.eval, Nat.Prime and 6 more
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, Imo2017P6.det_ne_zero, And.right, Eq.mp, propext, Finset.mem_erase, And.left, Finset.prod_ne_zero_iff, Iff.mpr, Nat.primeFactors, Int.natAbs, Exists.intro, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast and 153 more
194 instances, coercions and auxiliary constants left out.

Tactic trace: 181 steps
Open to load the checked before-and-after goal states.
```
lemma exists_g (S : Finset (ℤ × ℤ)) (hS : ∀ s ∈ S, IsCoprime s.1 s.2)
    (_hne : (T S).Nonempty) :
    ∃ g : HForm, Even g.deg ∧ 0 < g.deg ∧
      (∀ t ∈ T S, g.eval t.1 t.2 ≠ 0) ∧
      (∀ t ∈ T S, ∀ p : ℕ, p.Prime →
        (p : ℤ) ∣ (∏ t ∈ T S, ∏ t' ∈ (T S).erase t, (t'.2 * t.1 - t'.1 * t.2)) →
        ¬ (p : ℤ) ∣ g.eval t.1 t.2) := by
…
```
Mentions: S, Imo2017P6.T, Imo2017P6.HForm
problem Imo2017P6.imo2017_p6 line 761 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Eq, GCDMonoid.gcd, Prod.fst, Prod.snd, OfNat.ofNat, Exists, Nat, And, LT.lt, Finset.sum, Finset.range, HAdd.hAdd, HMul.hMul, HPow.hPow, HSub.hSub
Proof uses: IsCoprime, Eq.mpr, Int.gcd, id, congrArg, propext, Int.isCoprime_iff_gcd_eq_one, cast, Eq.trans, Eq.symm, Nat.cast_one, Eq.mp, Int.coe_gcd, dite, Finset.Nonempty, Imo2017P6.T, Imo2017P6.HForm, Even, Imo2017P6.HForm.deg, Ne and 164 more
178 instances, coercions and auxiliary constants left out.

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