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

20 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1986, Problem 6

Given a finite set of points in the plane, each with integer coordinates, is it always possible to color the points red or white so that for any straight line L parallel to one of the coordinate axes the difference (in absolute value) between the numbers of white and red points on L is not greater than 1?

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo1986P6.Balanced A signing of a set of points of the plane: ε p = 1 means that p is colored white and ε p = -1 means that p is colored red line 40 source
Source documentation
A signing of a set of points of the plane: ε p = 1 means that p is colored white and ε p = -1 means that p is colored red. The difference between the numbers of white and red points of S lying on a line then equals the sum of ε over the points of S on that line, so the required property of the coloring is that the sum of ε over every row and every column of S has absolute value at most 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: And, Membership.mem, Or, Eq, OfNat.ofNat, Neg.neg, LE.le, abs, Finset.sum, Finset.filter, Prod.fst, Prod.snd
9 instances, coercions and auxiliary constants left out.
```
def Balanced (S : Finset (ℤ × ℤ)) (ε : ℤ × ℤ → ℤ) : Prop :=
…
```
Mentions: S
lemma Imo1986P6.balanced_empty line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1986P6.Balanced, EmptyCollection.emptyCollection, Finset, Prod, Int, OfNat.ofNat
Proof uses: And.intro, Membership.mem, Or, Eq, Neg.neg, And, LE.le, abs, Finset.sum, Finset.filter, Prod.fst, Prod.snd, False.elim, Eq.mp, False, Eq.mpr, id, congrArg, Finset.filter_empty, Finset.sum_empty and 5 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo1986P6.balanced_image_swap The problem is symmetric under swapping the two coordinates line 51 source
Source documentation
The problem is symmetric under swapping the two coordinates.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Imo1986P6.Balanced, Finset.image, Prod.swap, Function.comp
Proof uses: Membership.mem, Or, Eq, OfNat.ofNat, Neg.neg, And, LE.le, abs, Finset.sum, Finset.filter, Prod.fst, Prod.snd, And.intro, Exists, Eq.mp, congrArg, propext, Finset.mem_image, Eq.mpr, id and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma balanced_image_swap {S : Finset (ℤ × ℤ)} {ε : ℤ × ℤ → ℤ} (h : Balanced S ε) :
    Balanced (S.image Prod.swap) (ε ∘ Prod.swap) := by
…
```
Mentions: S, h, Imo1986P6.Balanced
lemma Imo1986P6.balanced_of_alone_col Case A: some point P is the only point of S in its column line 72 source
Source documentation
Case A: some point P is the only point of S in its column. Then any balanced signing of S.erase P can be extended to a balanced signing of S by choosing the sign of P so as to balance the row of P.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Eq, Prod.fst, Imo1986P6.Balanced, Finset.erase, Exists
Proof uses: Or, OfNat.ofNat, Neg.neg, And, LE.le, abs, Finset.sum, Finset.filter, Prod.snd, rfl, Exists.intro, Function.update, ite, And.intro, dite, Eq.mpr, id, congrArg, Function.update_self, False and 50 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 77 steps
Open to load the checked before-and-after goal states.
```
lemma balanced_of_alone_col {S : Finset (ℤ × ℤ)} {P : ℤ × ℤ} (hP : P ∈ S)
    (hcol : ∀ Q ∈ S, Q.1 = P.1 → Q = P)
    {ε' : ℤ × ℤ → ℤ} (hε' : Balanced (S.erase P) ε') :
    ∃ ε, Balanced S ε := by
…
```
Mentions: S, P, Imo1986P6.Balanced
lemma Imo1986P6.balanced_of_alone_row Case A, symmetric version: some point P is the only point of S in its row line 143 source
Source documentation
Case A, symmetric version: some point P is the only point of S in its row. Handled by swapping the coordinates and applying balanced_of_alone_col.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Eq, Prod.snd, Nat, LE.le, Finset.card, Exists, Imo1986P6.Balanced, HAdd.hAdd, OfNat.ofNat
Proof uses: Finset.image, Prod.swap, Iff.mpr, And, Finset.mem_image, Exists.intro, And.intro, rfl, Prod.fst, Eq.mp, congrArg, propext, Eq.mpr, id, Eq.refl, Finset.erase, HSub.hSub, Finset.card_erase_of_mem, Finset.card_image_of_injective, Prod.swap_injective and 11 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma balanced_of_alone_row {S : Finset (ℤ × ℤ)} {P : ℤ × ℤ} (hP : P ∈ S)
    (hrow : ∀ Q ∈ S, Q.2 = P.2 → Q = P)
    (n : ℕ) (IH : ∀ T : Finset (ℤ × ℤ), T.card ≤ n → ∃ ε, Balanced T ε)
    (hcard : S.card ≤ n + 1) :
    ∃ ε, Balanced S ε := by
…
```
Mentions: S, P, Imo1986P6.Balanced
structure Imo1986P6.AltPath Documented declaration: AltPath line 177 source
Source documentation
An alternating path in S: a list of at least two distinct points of S such that the step from position i to position i + 1 is horizontal (the two points agree on their second coordinate) when i is even and vertical (the two points agree on their first coordinate) when i is odd.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, List

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
structure AltPath (S : Finset (ℤ × ℤ)) (L : List (ℤ × ℤ)) : Prop where
…
```
Mentions: S
lemma Imo1986P6.AltPath.snoc An alternating path can be extended by appending a fresh point, provided the new last step has the required direction line 187 source
Source documentation
An alternating path can be extended by appending a fresh point, provided the new last step has the required direction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, List, Imo1986P6.AltPath, Membership.mem, Not, And, Even, Nat, HSub.hSub, List.length, OfNat.ofNat, LT.lt, Eq, Prod.snd, GetElem.getElem, Odd, Prod.fst, HAppend.hAppend and 2 more
Proof uses: Imo1986P6.AltPath.mk, Eq.mpr, List.Nodup, Ne, id, congrArg, propext, List.nodup_append, And.intro, Imo1986P6.AltPath.nodup, List.nodup_singleton, False, Eq.rec, Eq.mp, List.mem_singleton, Or, List.mem_append, Imo1986P6.AltPath.mem, LE.le, Imo1986P6.AltPath.len and 13 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
```
lemma AltPath.snoc {S : Finset (ℤ × ℤ)} {L : List (ℤ × ℤ)} (hL : AltPath S L)
    {Q : ℤ × ℤ} (hQ : Q ∈ S) (hQn : Q ∉ L)
    (hlast : (Even (L.length - 1) → ∀ h : L.length - 1 < L.length, (L[L.length - 1]'h).2 = Q.2) ∧
             (Odd (L.length - 1) → ∀ h : L.length - 1 < L.length, (L[L.length - 1]'h).1 = Q.1)) :
    AltPath S (L ++ [Q]) where
…
```
Mentions: S, Imo1986P6.AltPath, h
lemma Imo1986P6.AltPath.step_at The step condition of an alternating path, with the second index given separately (useful when it is not literally i + 1) line 235 source
Source documentation
The step condition of an alternating path, with the second index given separately (useful when it is not literally i + 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, List, Imo1986P6.AltPath, Nat, Eq, HAdd.hAdd, OfNat.ofNat, LT.lt, List.length, And, Even, Prod.snd, GetElem.getElem, Odd, Prod.fst
Proof uses: Eq.rec, Eq.symm, Imo1986P6.AltPath.step
16 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma AltPath.step_at {S : Finset (ℤ × ℤ)} {L : List (ℤ × ℤ)} (hL : AltPath S L)
    (i j : ℕ) (hij : j = i + 1) (h : i + 1 < L.length) :
    (Even i → (L[i]'(by lia)).2 = (L[j]'(by lia)).2) ∧
    (Odd i → (L[i]'(by lia)).1 = (L[j]'(by lia)).1) := by
…
```
Mentions: S, Imo1986P6.AltPath, h
lemma Imo1986P6.AltPath.drop_step The step condition of an alternating path is inherited by a tail of the path, provided the tail starts at an even index line 244 source
Source documentation
The step condition of an alternating path is inherited by a tail of the path, provided the tail starts at an even index.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, List, Imo1986P6.AltPath, Nat, Even, LT.lt, HAdd.hAdd, OfNat.ofNat, List.length, List.drop, And, Eq, Prod.snd, GetElem.getElem, Odd, Prod.fst
Proof uses: Eq.mpr, id, congrArg, List.getElem_drop, Eq.mp, HSub.hSub, List.length_drop, Imo1986P6.AltPath.step, And.intro, And.left, Even.add, And.right, Even.add_odd
20 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma AltPath.drop_step {S : Finset (ℤ × ℤ)} {L : List (ℤ × ℤ)} (hL : AltPath S L)
    {j : ℕ} (hj : Even j) :
    ∀ t : ℕ, (h : t + 1 < (L.drop j).length) →
      (Even t → ((L.drop j)[t]'(by lia)).2 = ((L.drop j)[t + 1]'h).2) ∧
      (Odd t → ((L.drop j)[t]'(by lia)).1 = ((L.drop j)[t + 1]'h).1) := by
…
```
Mentions: S, Imo1986P6.AltPath, h
lemma Imo1986P6.AltPath.exists_max Among the alternating paths in S there is one of maximal length line 259 source
Source documentation
Among the alternating paths in S there is one of maximal length.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Exists, List, Imo1986P6.AltPath, And, LE.le, Nat, List.length
Proof uses: Finset.card, Eq.mpr, List.toFinset, id, Eq, congrArg, Eq.symm, List.toFinset_card_of_nodup, Imo1986P6.AltPath.nodup, Finset.card_le_card, Membership.mem, Imo1986P6.AltPath.mem, Eq.mp, propext, List.mem_toFinset, Exists.intro, And.intro, rfl, Nat.findGreatest, Classical.propDecidable and 2 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma AltPath.exists_max {S : Finset (ℤ × ℤ)} (hbase : ∃ L₀, AltPath S L₀) :
    ∃ L, AltPath S L ∧ ∀ L', AltPath S L' → L'.length ≤ L.length := by
…
```
Mentions: S, Imo1986P6.AltPath
lemma Imo1986P6.getElem_congr Helper: two elements of the same list at equal indices are equal line 280 source
Source documentation
Helper: two elements of the same list at equal indices are equal.

no axioms what this means
Statement uses: List, Nat, LT.lt, List.length, Eq, GetElem.getElem
Proof uses: congrArg, Fin, Fin.mk, List.get, Fin.ext
3 instances, coercions and auxiliary constants left out.
```
lemma getElem_congr {α : Type*} (l : List α) {i j : ℕ} (hi : i < l.length) (hj : j < l.length)
    (h : i = j) : l[i]'hi = l[j]'hj :=
…
```
Mentions: h
lemma Imo1986P6.pair_sum_zero Documented declaration: pair_sum_zero line 290 source
Source documentation
If a list of points with no repetitions has even length and a sign function alternates on each pair of consecutive elements while a "coordinate" function is constant on each pair, then the sum of the signs over the points of the list lying on any fixed level of the coordinate is zero. This is the computation showing that a correctly colored cycle contributes equally many white and red points to every row and every column.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, List.Nodup, Even, Nat, List.length, LT.lt, HAdd.hAdd, HMul.hMul, OfNat.ofNat, And, Eq, List.getD, Prod.mk, Finset.sum, Finset.filter, List.toFinset
Proof uses: LE.le, Nat.recAux, List.nil, Eq.refl, Eq.symm, List.cons, False.elim, Eq.mp, False, Eq.trans, congr, congrArg, and_false, of_eq_true, True, congrFun', EmptyCollection.emptyCollection, Finset, Finset.filter_empty, eq_self and 34 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
lemma pair_sum_zero : ∀ (C : List (ℤ × ℤ)) (f g : ℤ × ℤ → ℤ),
    C.Nodup → Even C.length →
    (∀ t : ℕ, 2 * t + 1 < C.length →
      f (C.getD (2 * t) (0, 0)) + f (C.getD (2 * t + 1) (0, 0)) = 0 ∧
      g (C.getD (2 * t) (0, 0)) = g (C.getD (2 * t + 1) (0, 0))) →
    ∀ c : ℤ, ∑ p ∈ C.toFinset.filter (fun p => g p = c), f p = 0 := by
…
```
Mentions: f
def Imo1986P6.cycSign The sign function attached to an even-length cycle: +1 at even positions, -1 at odd positions line 368 source
Source comment
The sign function attached to an even-length cycle: `+1` at even positions, `-1` at odd positions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int
Proof uses: ite, Exists, Fin, List.length, And, Eq, List.get, Even, Nat, OfNat.ofNat, Neg.neg
9 instances, coercions and auxiliary constants left out.
```
noncomputable def cycSign (C : List (ℤ × ℤ)) : ℤ × ℤ → ℤ :=
…
```
lemma Imo1986P6.cycSign_apply line 371 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, List.Nodup, Fin, List.length, Eq, Imo1986P6.cycSign, List.get, ite, Even, Nat, OfNat.ofNat, Neg.neg
Proof uses: id, dite, Exists, And, Eq.mpr, congrArg, ite_eq_left, Exists.intro, And.intro, rfl, Eq.refl, Not, ite_eq_right, False, Eq.rec, Iff.mp, List.Nodup.get_inj_iff
15 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo1986P6.cycSign_apply' line 378 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, List.Nodup, Nat, LT.lt, List.length, Eq, Imo1986P6.cycSign, GetElem.getElem, ite, Even, OfNat.ofNat, Neg.neg
Proof uses: Eq.trans, Fin.mk, Fin.isLt, List.get, congrArg, Eq.symm, List.get_eq_getElem, Imo1986P6.cycSign_apply
13 instances, coercions and auxiliary constants left out.
lemma Imo1986P6.cycle_balanced A cycle of even length, alternating horizontal and vertical steps and closed by a vertical step, admits a signing that is balanced on every row and column line 385 source
Source documentation
A cycle of even length, alternating horizontal and vertical steps and closed by a vertical step, admits a signing that is balanced on every row and column.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, List.Nodup, Even, Nat, List.length, LT.lt, HAdd.hAdd, OfNat.ofNat, And, Eq, Prod.snd, GetElem.getElem, Odd, Prod.fst, HSub.hSub, Exists, Membership.mem, Finset and 5 more
Proof uses: Exists.intro, Imo1986P6.cycSign, And.intro, id, dite, ite, Fin, List.get, Eq.mpr, False, congr, congrArg, congrFun', ite_eq_left, Eq.trans, eq_false', False.elim, noConfusion_of_Nat, Int.ctorIdx, of_eq_true and 62 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 121 steps
Open to load the checked before-and-after goal states.
```
lemma cycle_balanced (C : List (ℤ × ℤ)) (hnodup : C.Nodup) (hlen : Even C.length)
    (hstep : ∀ i : ℕ, (h : i + 1 < C.length) →
      (Even i → (C[i]'(by lia)).2 = (C[i + 1]'h).2) ∧
      (Odd i → (C[i]'(by lia)).1 = (C[i + 1]'h).1))
    (hclose : ∀ h : 0 < C.length, (C[C.length - 1]'(by lia)).1 = (C[0]'h).1) :
    ∃ ε : ℤ × ℤ → ℤ, (∀ p ∈ C.toFinset, ε p = 1 ∨ ε p = -1) ∧
      (∀ y : ℤ, ∑ p ∈ C.toFinset.filter (fun p => p.2 = y), ε p = 0) ∧
      (∀ x : ℤ, ∑ p ∈ C.toFinset.filter (fun p => p.1 = x), ε p = 0) := by
…
```
Mentions: h
lemma Imo1986P6.exists_cycle Case B: every point of the nonempty set S has another point of S in its row and another one in its column line 481 source
Source documentation
Case B: every point of the nonempty set S has another point of S in its row and another one in its column. Then S contains an alternating cycle of even length at least four, closed by a vertical step.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Finset.Nonempty, Membership.mem, Exists, And, Ne, Eq, Prod.snd, Prod.fst, List, List.Nodup, LE.le, Nat, OfNat.ofNat, List.length, Even, LT.lt, HAdd.hAdd and 3 more
Proof uses: Imo1986P6.AltPath, List.cons, List.nil, Imo1986P6.AltPath.mk, Eq.mpr, Not, id, congrArg, propext, List.nodup_cons, And.intro, Eq.symm, Iff.mp, List.mem_singleton, List.nodup_singleton, Or, Eq.mp, List.mem_cons, of_eq_true, Eq.trans and 55 more
154 instances, coercions and auxiliary constants left out.

Tactic trace: 429 steps (first 200 of 429)
Open to load the checked before-and-after goal states.
```
lemma exists_cycle (S : Finset (ℤ × ℤ)) (hne : S.Nonempty)
    (hrow : ∀ P ∈ S, ∃ Q ∈ S, Q ≠ P ∧ Q.2 = P.2)
    (hcol : ∀ P ∈ S, ∃ Q ∈ S, Q ≠ P ∧ Q.1 = P.1) :
    ∃ C : List (ℤ × ℤ), C.Nodup ∧ (∀ p ∈ C, p ∈ S) ∧ 4 ≤ C.length ∧ Even C.length ∧
      (∀ i : ℕ, (h : i + 1 < C.length) →
        (Even i → (C[i]'(by lia)).2 = (C[i + 1]'h).2) ∧
        (Odd i → (C[i]'(by lia)).1 = (C[i + 1]'h).1)) ∧
      (∀ h : 0 < C.length, (C[C.length - 1]'(by lia)).1 = (C[0]'h).1) := by
…
```
Mentions: S, P, h
lemma Imo1986P6.main_lemma Main induction: every finite set of points with integer coordinates admits a balanced signing line 803 source
Source documentation
Main induction: every finite set of points with integer coordinates admits a balanced signing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Int, LE.le, Finset.card, Exists, Imo1986P6.Balanced
Proof uses: Nat.recAux, OfNat.ofNat, EmptyCollection.emptyCollection, Exists.intro, Imo1986P6.balanced_empty, Eq.symm, Eq.mp, Eq, congrArg, propext, Finset.card_eq_zero, Nat.le_zero, HAdd.hAdd, dite, Finset.Nonempty, And, Membership.mem, Or, Prod.fst, Prod.snd and 57 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 119 steps
Open to load the checked before-and-after goal states.
```
lemma main_lemma : ∀ n : ℕ, ∀ S : Finset (ℤ × ℤ), S.card ≤ n → ∃ ε, Balanced S ε := by
…
```
Mentions: S, Imo1986P6.Balanced
determine Imo1986P6.does_exist line 930 source
no axioms what this means
Statement uses: Bool
Proof uses: Bool.true
problem Imo1986P6.imo1986_p6 IMO 1986, Problem 6 line 941 source
Source documentation
IMO 1986, Problem 6. Given a finite set S of points in the plane with integer coordinates, the points can be colored red or white so that on every line parallel to one of the coordinate axes the numbers of white and red points differ by at most one.
We encode the coloring by a sign function ε : ℤ × ℤ → ℤ with values in {1, -1} (1 = white, -1 = red); the sum of ε over the points of S on a line is then exactly the difference between the numbers of white and red points on that line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, ite, Eq, Bool, Imo1986P6.does_exist, Bool.true, Exists, And, Membership.mem, Or, OfNat.ofNat, Neg.neg, LE.le, abs, Finset.sum, Finset.filter, Prod.fst, Prod.snd and 1 more
Proof uses: Eq.mpr, id, Eq.trans, True, ite_congr, eq_self, Eq.refl, ite_true, Imo1986P6.Balanced, Imo1986P6.main_lemma, Finset.card, le_refl, Nat, Exists.intro
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
problem imo1986_p6 (S : Finset (ℤ × ℤ)) :
    if does_exist then
      ∃ ε : ℤ × ℤ → ℤ,
        (∀ p ∈ S, ε p = 1 ∨ ε p = -1) ∧
        (∀ x : ℤ, |∑ p ∈ S.filter (fun p => p.1 = x), ε p| ≤ 1) ∧
        (∀ y : ℤ, |∑ p ∈ S.filter (fun p => p.2 = y), ε p| ≤ 1)
    else
      ¬ ∃ ε : ℤ × ℤ → ℤ,
        (∀ p ∈ S, ε p = 1 ∨ ε p = -1) ∧
        (∀ x : ℤ, |∑ p ∈ S.filter (fun p => p.1 = x), ε p| ≤ 1) ∧
        (∀ y : ℤ, |∑ p ∈ S.filter (fun p => p.2 = y), ε p| ≤ 1) := by
…
```
Mentions: S, Imo1986P6.does_exist