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

55 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2013, Problem 2

A configuration of 4027 points of the plane is called Colombian if it consists of 2013 red points and 2014 blue points, and no three of the points of the configuration are collinear. By drawing some lines, the plane is divided into several regions. An arrangement of lines is good for a Colombian configuration if the following two conditions are satisfied:

no line passes through any point of the configuration;
no region contains points of both colours.

Find the least value of k such that for any Colombian configuration of 4027 points, there is a good arrangement of k lines.

Imports (2)

Imported by 1 file

Compfiles.lean

abbrev Imo2013P2.Pt line 36 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
structure Imo2013P2.ColombianConfiguration A configuration of 2013 red points and 2014 blue points in the plane, all distinct, such that no three points of the configuration are collinear line 40 source
Source documentation
A configuration of 2013 red points and 2014 blue points in the plane, all distinct, such that no three points of the configuration are collinear.

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure ColombianConfiguration where
…
```
def Imo2013P2.GoodArrangement Documented declaration: GoodArrangement line 61 source
Source documentation
An arrangement of lines (one-dimensional affine subspaces of the plane) is good for a configuration if no line passes through a point of the configuration and every red point is strictly separated from every blue point by at least one of the lines.
(The regions determined by an arrangement of lines are convex, and two points lying on none of the lines belong to the same region if and only if they are strictly on the same side of every line. Therefore, requiring each red-blue pair to be strictly separated by some line is equivalent to requiring that no region contains points of both colours.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.ColombianConfiguration, Nat, Fin, AffineSubspace, Real, Imo2013P2.Pt, OfNat.ofNat, ENNReal
Proof uses: And, Eq, Module.finrank, Subtype, Membership.mem, Submodule, AffineSubspace.direction, Finset, Union.union, Imo2013P2.ColombianConfiguration.red, Imo2013P2.ColombianConfiguration.blue, Not, Exists, AffineSubspace.SOppSide
67 instances, coercions and auxiliary constants left out.
```
def GoodArrangement (cfg : ColombianConfiguration) {k : ℕ}
    (lines : Fin k → AffineSubspace ℝ Pt) : Prop :=
…
```
Mentions: Imo2013P2.ColombianConfiguration, Imo2013P2.Pt
theorem Imo2013P2.Pt.ext line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Eq, Fin, OfNat.ofNat, Nat, Real, WithLp.ofLp, ENNReal
Proof uses: WithLp.ofLp_injective, funext, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, eq_of_heq, List.Mem.tail, False.elim, noConfusion_of_Nat and 3 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.inner_pt line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Eq, Real, Inner.inner, OfNat.ofNat, ENNReal, Nat, Fin, HAdd.hAdd, HMul.hMul, WithLp.ofLp
Proof uses: Eq.mpr, Finset.sum, Finset.univ, id, congrArg, PiLp, PiLp.inner_apply, Fin.sum_univ_two, RingHom, starRingEnd, RCLike.inner_apply, congrFun', congr, conj_trivial, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf and 15 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Imo2013P2.rot90 Rotation by 90 degrees line 84 source
Source documentation
Rotation by 90 degrees.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt
Proof uses: WithLp.toLp, OfNat.ofNat, ENNReal, Fin, Nat, Real, Matrix.vecCons, Neg.neg, WithLp.ofLp, Matrix.vecEmpty
10 instances, coercions and auxiliary constants left out.
```
def rot90 (v : Pt) : Pt := !₂[-(v 1), v 0]
```
Mentions: Imo2013P2.Pt
theorem Imo2013P2.rot90_apply0 line 86 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Eq, Fin, OfNat.ofNat, Nat, Real, WithLp.ofLp, ENNReal, Imo2013P2.rot90, Neg.neg
Proof uses: rfl
17 instances, coercions and auxiliary constants left out.
theorem Imo2013P2.rot90_apply1 line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Eq, Fin, OfNat.ofNat, Nat, Real, WithLp.ofLp, ENNReal, Imo2013P2.rot90
Proof uses: rfl
16 instances, coercions and auxiliary constants left out.
theorem Imo2013P2.inner_rot90_self line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Eq, Real, Inner.inner, OfNat.ofNat, ENNReal, Nat, Fin, Imo2013P2.rot90
Proof uses: Eq.mpr, HAdd.hAdd, HMul.hMul, WithLp.ofLp, id, congrArg, Imo2013P2.inner_pt, Neg.neg, Imo2013P2.rot90_apply0, Imo2013P2.rot90_apply1, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.neg_congr and 32 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2013P2.e₁ The first standard basis vector line 95 source
Source documentation
The first standard basis vector.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt
Proof uses: WithLp.toLp, OfNat.ofNat, ENNReal, Fin, Nat, Real, Matrix.vecCons, Matrix.vecEmpty
10 instances, coercions and auxiliary constants left out.
```
def e₁ : Pt := !₂[1, 0]
```
Mentions: Imo2013P2.Pt
theorem Imo2013P2.inner_e₁ line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Eq, Real, Inner.inner, OfNat.ofNat, ENNReal, Nat, Fin, Imo2013P2.e₁, WithLp.ofLp
Proof uses: Eq.mpr, HAdd.hAdd, HMul.hMul, id, congrArg, Imo2013P2.inner_pt, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add and 9 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.e₁_ne_zero line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ne, Imo2013P2.Pt, Imo2013P2.e₁, OfNat.ofNat, ENNReal, Fin, Nat, Real
Proof uses: Eq, WithLp.ofLp, Eq.mpr, id, congrArg, Eq.refl, False.elim, False, Eq.mp, eq_false, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Nat.cast_zero, Bool, Bool.false
44 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.rot90_ne_zero line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Ne, OfNat.ofNat, ENNReal, Fin, Nat, Real, Imo2013P2.rot90
Proof uses: Eq, WithLp.ofLp, Eq.mpr, id, congrArg, Eq.refl, Imo2013P2.Pt.ext, Eq.mp, Imo2013P2.rot90_apply1, Neg.neg, Imo2013P2.rot90_apply0
34 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.eq_smul_of_inner_rot90_eq_zero line 117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Ne, OfNat.ofNat, ENNReal, Fin, Nat, Real, Eq, Inner.inner, Imo2013P2.rot90, Exists, HSMul.hSMul
Proof uses: Or, WithLp.ofLp, Decidable.byContradiction, Not, Imo2013P2.Pt.ext, id, And.left, Eq.mp, And, Eq.trans, congr, congrArg, And.right, Exists.intro, HDiv.hDiv, Eq.mpr, PiLp, PiLp.smul_apply, HMul.hMul, smul_eq_mul and 102 more
160 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.collinear_triple_of_sub_eq_smul line 140 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Real, Eq, HSub.hSub, OfNat.ofNat, ENNReal, Fin, Nat, HSMul.hSMul, Collinear, Insert.insert, Set, Singleton.singleton
Proof uses: Eq.mpr, Exists, Membership.mem, HVAdd.hVAdd, id, congrArg, propext, collinear_iff_of_mem, Set.mem_insert, Exists.intro, of_eq_true, Eq.trans, True, congrFun', zero_smul, zero_add, Function.Injective.addZeroClass, WithLp, Equiv.add, WithLp.equiv and 7 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.collinear_of_inner_rot90_eq_zero line 149 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Ne, Eq, Real, Inner.inner, OfNat.ofNat, ENNReal, Nat, Fin, Imo2013P2.rot90, HSub.hSub, Collinear, Insert.insert, Set, Singleton.singleton
Proof uses: HSMul.hSMul, Exists, Imo2013P2.eq_smul_of_inner_rot90_eq_zero, Iff.mpr, sub_ne_zero, Imo2013P2.collinear_triple_of_sub_eq_smul
98 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.collinear_of_subset_line line 154 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Imo2013P2.Pt, AffineSubspace, Real, OfNat.ofNat, ENNReal, Fin, Nat, Eq, Module.finrank, Subtype, Membership.mem, Submodule, AffineSubspace.direction, LE.le, Collinear
Proof uses: Eq.mpr, Cardinal, Module.rank, vectorSpan, id, congrArg, propext, collinear_iff_rank_le_one, vectorSpan_mono, Submodule.rank_mono, Eq.symm, Module.finrank_eq_rank, Nat.cast_one, Eq.refl, Eq.mp
96 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def Imo2013P2.perp The line {x | ⟪n, x⟫ = c} line 167 source
Source documentation
The line {x | ⟪n, x⟫ = c}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Real, AffineSubspace, OfNat.ofNat, ENNReal, Fin, Nat
Proof uses: AffineSubspace.mk, Set.ofPred, Eq, Inner.inner, Membership.mem, Set
61 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def perp (n : Pt) (c : ℝ) : AffineSubspace ℝ Pt where
…
```
Mentions: Imo2013P2.Pt
theorem Imo2013P2.mem_perp line 175 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Real, Iff, Membership.mem, AffineSubspace, OfNat.ofNat, ENNReal, Fin, Nat, Imo2013P2.perp, Eq, Inner.inner
Proof uses: Iff.rfl
64 instances, coercions and auxiliary constants left out.
theorem Imo2013P2.direction_perp line 177 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Ne, OfNat.ofNat, ENNReal, Fin, Nat, Real, Eq, Submodule, AffineSubspace.direction, Imo2013P2.perp, LinearMap.ker, RingHom.id, LinearMap, starRingEnd, innerₛₗ
Proof uses: Inner.inner, Iff.mpr, inner_self_ne_zero, Membership.mem, AffineSubspace, HSMul.hSMul, HDiv.hDiv, Eq.mpr, id, congrArg, propext, Imo2013P2.mem_perp, HMul.hMul, real_inner_smul_right, of_eq_true, Eq.trans, True, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, List.nil and 56 more
188 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.finrank_direction_perp line 200 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Ne, OfNat.ofNat, ENNReal, Fin, Nat, Real, Eq, Module.finrank, Subtype, Membership.mem, Submodule, AffineSubspace.direction, Imo2013P2.perp
Proof uses: Eq.mpr, LinearMap.ker, RingHom.id, LinearMap, starRingEnd, innerₛₗ, id, congrArg, Imo2013P2.direction_perp, HAdd.hAdd, LinearMap.range, LinearMap.finrank_range_add_finrank_ker, LE.le, Submodule.finrank_le, Eq.mp, Module.finrank_self, Bot.bot, Exists, And, propext and 15 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.sOppSide_iff The fundamental characterization: x and y are strictly on opposite sides of the line {z | ⟪n, z⟫ = c} iff their inner products with n strictly sandwich c line 223 source
Source documentation
The fundamental characterization: x and y are strictly on opposite sides of the line {z | ⟪n, z⟫ = c} iff their inner products with n strictly sandwich c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AffineSubspace, Real, Imo2013P2.Pt, OfNat.ofNat, ENNReal, Fin, Nat, Iff, Membership.mem, Eq, Inner.inner, AffineSubspace.SOppSide, Or, And, LT.lt
Proof uses: HSub.hSub, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 151 more
246 instances, coercions and auxiliary constants left out.

Tactic trace: 85 steps
Open to load the checked before-and-after goal states.
```
theorem sOppSide_iff {ℓ : AffineSubspace ℝ Pt} {n : Pt} {c : ℝ}
    (hmem : ∀ z : Pt, z ∈ ℓ ↔ ⟪n, z⟫ = c) (x y : Pt) :
    ℓ.SOppSide x y ↔
      (⟪n, x⟫ < c ∧ c < ⟪n, y⟫) ∨ (⟪n, y⟫ < c ∧ c < ⟪n, x⟫) := by
…
```
Mentions: Imo2013P2.Pt
theorem Imo2013P2.exists_normal Every one-dimensional affine subspace of the plane is the level set of a nonzero linear functional line 295 source
Source documentation
Every one-dimensional affine subspace of the plane is the level set of a nonzero linear functional.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AffineSubspace, Real, Imo2013P2.Pt, OfNat.ofNat, ENNReal, Fin, Nat, Eq, Module.finrank, Subtype, Membership.mem, Submodule, AffineSubspace.direction, Exists, And, Ne, Iff, Inner.inner
Proof uses: Bot.bot, False.elim, False, Eq.mp, Eq.trans, congrFun', congrArg, finrank_bot, AffineSubspace.direction_bot, Set, Set.Nonempty, Iff.mpr, AffineSubspace.nonempty_iff_ne_bot, rfl, Submodule.orthogonal, HAdd.hAdd, Submodule.finrank_add_finrank_orthogonal, EuclideanSpace, finrank_euclideanSpace_fin, Submodule.exists_mem_ne_zero_of_ne_bot and 70 more
195 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
theorem exists_normal {ℓ : AffineSubspace ℝ Pt}
    (hl : Module.finrank ℝ ℓ.direction = 1) :
    ∃ (n : Pt) (c : ℝ), n ≠ 0 ∧ ∀ z : Pt, z ∈ ℓ ↔ ⟪n, z⟫ = c := by
…
```
Mentions: Imo2013P2.Pt
def Imo2013P2.No3Col line 335 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2013P2.Pt
Proof uses: Membership.mem, Ne, Not, Collinear, Real, OfNat.ofNat, ENNReal, Fin, Nat, Insert.insert, Set, Singleton.singleton
32 instances, coercions and auxiliary constants left out.
theorem Imo2013P2.exists_cut Cut a subset Z of S off from the rest of S with a single line, given a linear functional whose values on Z all lie strictly below its values on S \ Z line 342 source
Source documentation
Cut a subset Z of S off from the rest of S with a single line, given a linear functional whose values on Z all lie strictly below its values on S \ Z.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2013P2.Pt, Finset.Nonempty, SDiff.sdiff, OfNat.ofNat, ENNReal, Fin, Nat, Real, Ne, Membership.mem, LE.le, Inner.inner, LT.lt, Exists, AffineSubspace, And, Eq, Module.finrank, Subtype and 4 more
Proof uses: Finset.exists_min_image, HDiv.hDiv, HAdd.hAdd, rfl, Eq.mpr, id, congrArg, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast and 101 more
185 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
theorem exists_cut {S Z : Finset Pt} (hne : (S \ Z).Nonempty)
    {n : Pt} (hn : n ≠ 0) {t : ℝ} (hZ : ∀ p ∈ Z, ⟪n, p⟫ ≤ t)
    (hX : ∀ x ∈ S \ Z, t < ⟪n, x⟫) :
    ∃ ℓ : AffineSubspace ℝ Pt, Module.finrank ℝ ℓ.direction = 1 ∧
      (∀ p ∈ S, p ∉ ℓ) ∧ ∀ p ∈ Z, ∀ x ∈ S \ Z, ℓ.SOppSide p x := by
…
```
Mentions: S, Imo2013P2.Pt
theorem Imo2013P2.exists_strip Cut a pair of points {A, B} of S off from the rest of S with two lines parallel to the segment AB line 366 source
Source documentation
Cut a pair of points {A, B} of S off from the rest of S with two lines parallel to the segment AB.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2013P2.Pt, Imo2013P2.No3Col, Membership.mem, Ne, Finset.Nonempty, SDiff.sdiff, OfNat.ofNat, ENNReal, Fin, Nat, Real, Insert.insert, Singleton.singleton, Exists, AffineSubspace, And, Eq, Module.finrank, Subtype and 5 more
Proof uses: Imo2013P2.rot90, HSub.hSub, rfl, Imo2013P2.rot90_ne_zero, Iff.mpr, sub_ne_zero, Ne.symm, Inner.inner, Imo2013P2.inner_rot90_self, Eq.mpr, id, congrArg, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, Mathlib.Tactic.Ring.of_eq and 124 more
195 instances, coercions and auxiliary constants left out.

Tactic trace: 80 steps
Open to load the checked before-and-after goal states.
```
theorem exists_strip {S : Finset Pt} (h3 : No3Col S) {A B : Pt}
    (hA : A ∈ S) (hB : B ∈ S) (hAB : A ≠ B)
    (hne : (S \ ({A, B} : Finset Pt)).Nonempty) :
    ∃ ℓ₁ ℓ₂ : AffineSubspace ℝ Pt,
      Module.finrank ℝ ℓ₁.direction = 1 ∧ Module.finrank ℝ ℓ₂.direction = 1 ∧
      (∀ p ∈ S, p ∉ ℓ₁ ∧ p ∉ ℓ₂) ∧
      ∀ p ∈ ({A, B} : Finset Pt), ∀ x ∈ S \ ({A, B} : Finset Pt),
        ℓ₁.SOppSide p x ∨ ℓ₂.SOppSide p x := by
…
```
Mentions: S, Imo2013P2.Pt, Imo2013P2.No3Col
theorem Imo2013P2.pair_strips Isolate an even-sized subset C of S into pairs, each pair confined to its own strip between two parallel lines line 434 source
Source documentation
Isolate an even-sized subset C of S into pairs, each pair confined to its own strip between two parallel lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2013P2.Pt, Imo2013P2.No3Col, LE.le, Nat, OfNat.ofNat, Finset.card, Eq, HMul.hMul, Exists, List, AffineSubspace, Real, ENNReal, Fin, And, List.length, Membership.mem, Module.finrank, Subtype and 5 more
Proof uses: Nat.recAux, Exists.intro, List.nil, And.intro, rfl, of_eq_true, Eq.trans, True, forall_congr, False, implies_congr, Eq.refl, implies_true, absurd, EmptyCollection.emptyCollection, Eq.mp, congrArg, Iff.mp, Finset.card_eq_zero, Finset.notMem_empty and 64 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 90 steps
Open to load the checked before-and-after goal states.
```
theorem pair_strips {S : Finset Pt} (h3 : No3Col S) (hcard : 4 ≤ S.card) :
    ∀ (m : ℕ) (C : Finset Pt), C ⊆ S → C.card = 2 * m →
    ∃ L : List (AffineSubspace ℝ Pt), L.length = 2 * m ∧
      (∀ ℓ ∈ L, Module.finrank ℝ ℓ.direction = 1) ∧
      (∀ ℓ ∈ L, ∀ p ∈ S, p ∉ ℓ) ∧
      (∀ p ∈ C, ∀ x ∈ S \ C, ∃ ℓ ∈ L, ℓ.SOppSide p x) := by
…
```
Mentions: S, Imo2013P2.Pt, Imo2013P2.No3Col
theorem Imo2013P2.mtrick Documented declaration: mtrick line 516 source
Source documentation
The "tilting" trick: if all points of S other than z and w lie strictly on the positive side of the line through z and w, then there is a linear functional whose unique minimizer over S is w.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2013P2.Pt, Ne, Eq, Real, Inner.inner, OfNat.ofNat, ENNReal, Nat, Fin, HSub.hSub, Membership.mem, LT.lt, Finset.Nonempty, SDiff.sdiff, Insert.insert, Singleton.singleton, Exists, And
Proof uses: rfl, Iff.mpr, sub_ne_zero, Ne.symm, real_inner_self_pos, And.intro, And.left, Not, Eq.mp, Or, congrArg, propext, not_or, Finset.mem_singleton, Finset.mem_insert, Finset.mem_sdiff, And.right, LE.le, Finset.exists_min_image, Finset.exists_max_image and 98 more
202 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
```
theorem mtrick {S : Finset Pt} {z w : Pt} (hzw : z ≠ w)
    {n₀ : Pt} (horth : ⟪n₀, w - z⟫ = 0)
    (hpos : ∀ x ∈ S, x ≠ z → x ≠ w → 0 < ⟪n₀, x - z⟫)
    (hne : (S \ ({z, w} : Finset Pt)).Nonempty) :
    ∃ n : Pt, n ≠ 0 ∧ ∀ x ∈ S, x ≠ w → ⟪n, w⟫ < ⟪n, x⟫ := by
…
```
Mentions: S, Imo2013P2.Pt
theorem Imo2013P2.exists_hull_edge Documented declaration: exists_hull_edge line 585 source
Source documentation
At the leftmost point z of S (assuming it is the unique leftmost point), there is another point w of S such that the line through z and w supports S: all other points are strictly on its positive side.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2013P2.Pt, Imo2013P2.No3Col, Membership.mem, Ne, LT.lt, Fin, OfNat.ofNat, Nat, Real, WithLp.ofLp, ENNReal, Finset.Nonempty, Finset.erase, Exists, And, Eq, Inner.inner, HSub.hSub
Proof uses: LE.le, HDiv.hDiv, Finset.exists_min_image, Finset.mem_of_mem_erase, Finset.ne_of_mem_erase, Imo2013P2.rot90, rfl, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring and 118 more
192 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
theorem exists_hull_edge {S : Finset Pt} (h3 : No3Col S) {z : Pt} (hz : z ∈ S)
    (hmin : ∀ x ∈ S, x ≠ z → z 0 < x 0) (hne : (S.erase z).Nonempty) :
    ∃ w ∈ S, w ≠ z ∧ ∃ n₀ : Pt, n₀ ≠ 0 ∧ ⟪n₀, w - z⟫ = 0 ∧
      ∀ x ∈ S, x ≠ z → x ≠ w → 0 < ⟪n₀, x - z⟫ := by
…
```
Mentions: S, Imo2013P2.Pt, Imo2013P2.No3Col
theorem Imo2013P2.assemble Documented declaration: assemble line 632 source
Source documentation
Given a single line cutting a subset Z of one of the two color classes C off from the rest of the configuration, where C \ Z has 2012 elements, complete it to a good arrangement of 2013 lines using strips.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.ColombianConfiguration, Finset, Imo2013P2.Pt, Or, Eq, Imo2013P2.ColombianConfiguration.red, Imo2013P2.ColombianConfiguration.blue, LE.le, Nat, Finset.card, SDiff.sdiff, OfNat.ofNat, ENNReal, Fin, Real, AffineSubspace, Module.finrank, Subtype, Membership.mem, Submodule and 6 more
Proof uses: rfl, Imo2013P2.No3Col, Imo2013P2.ColombianConfiguration.not_collinear, Eq.mpr, id, congrArg, HAdd.hAdd, Finset.card_union_of_disjoint, Imo2013P2.ColombianConfiguration.red_blue_disjoint, Imo2013P2.ColombianConfiguration.red_card, Imo2013P2.ColombianConfiguration.blue_card, Eq.refl, Finset.subset_union_left, Eq.symm, Finset.subset_union_right, List, And, List.length, HMul.hMul, Imo2013P2.pair_strips and 29 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 71 steps
Open to load the checked before-and-after goal states.
```
theorem assemble (cfg : ColombianConfiguration)
    {C Z : Finset Pt} (hC : C = cfg.red ∨ C = cfg.blue) (hZC : Z ⊆ C)
    (hcards : (C \ Z).card = 2012)
    {ℓ₀ : AffineSubspace ℝ Pt} (hr₀ : Module.finrank ℝ ℓ₀.direction = 1)
    (havoid₀ : ∀ p ∈ cfg.red ∪ cfg.blue, p ∉ ℓ₀)
    (hsep₀ : ∀ p ∈ Z, ∀ x ∈ (cfg.red ∪ cfg.blue) \ Z, ℓ₀.SOppSide p x) :
    ∃ lines : Fin 2013 → AffineSubspace ℝ Pt, GoodArrangement cfg lines := by
…
```
Mentions: Imo2013P2.ColombianConfiguration, Imo2013P2.Pt, Imo2013P2.GoodArrangement
theorem Imo2013P2.upper_bound 2013 lines always suffice line 700 source
Source documentation
2013 lines always suffice.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.ColombianConfiguration, Exists, Fin, OfNat.ofNat, Nat, AffineSubspace, Real, Imo2013P2.Pt, ENNReal, Imo2013P2.GoodArrangement
Proof uses: Finset, Union.union, Imo2013P2.ColombianConfiguration.red, Imo2013P2.ColombianConfiguration.blue, Eq, rfl, Imo2013P2.No3Col, Imo2013P2.ColombianConfiguration.not_collinear, Finset.card, Eq.mpr, id, congrArg, HAdd.hAdd, Finset.card_union_of_disjoint, Imo2013P2.ColombianConfiguration.red_blue_disjoint, Imo2013P2.ColombianConfiguration.red_card, Imo2013P2.ColombianConfiguration.blue_card, Eq.refl, Finset.Nonempty, LT.lt and 153 more
220 instances, coercions and auxiliary constants left out.

Tactic trace: 223 steps (first 200 of 223)
Open to load the checked before-and-after goal states.
```
theorem upper_bound (cfg : ColombianConfiguration) :
    ∃ lines : Fin 2013 → AffineSubspace ℝ Pt, GoodArrangement cfg lines := by
…
```
Mentions: Imo2013P2.ColombianConfiguration, Imo2013P2.Pt, Imo2013P2.GoodArrangement
def Imo2013P2.ang The angle of the j-th vertex of a regular 4027-gon line 935 source
Source documentation
The angle of the j-th vertex of a regular 4027-gon.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HDiv.hDiv, HMul.hMul, OfNat.ofNat, Real.pi
10 instances, coercions and auxiliary constants left out.
```
noncomputable def ang (j : ℕ) : ℝ := 2 * Real.pi * j / 4027
```
theorem Imo2013P2.ang_nonneg line 937 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, OfNat.ofNat, Imo2013P2.ang
Proof uses: id, Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos, HMul.hMul, Real.pi, mul_nonneg, le_of_lt, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Real.pi_pos, Nat.cast_nonneg'
41 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.ang_lt_ang line 941 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Real, Imo2013P2.ang
Proof uses: id, div_lt_div_of_pos_right, HMul.hMul, OfNat.ofNat, Real.pi, mul_lt_mul_of_pos_left, Nat.strictMono_cast, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Real.pi_pos
44 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.ang_le_ang line 945 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, Imo2013P2.ang
Proof uses: LT.lt, Eq, Or, LE.le.lt_or_eq, LT.lt.le, Imo2013P2.ang_lt_ang, Eq.mpr, id, congrArg, le_refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.ang_lt_two_pi line 950 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Real, Imo2013P2.ang, HMul.hMul, Real.pi
Proof uses: Trans.trans, Eq, Imo2013P2.ang_lt_ang, id, of_eq_true, HDiv.hDiv, Eq.trans, True, congrFun', congrArg, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, IsUnit.mul_div_cancel_right, IsUnit, Ne, eq_true, Mathlib.Meta.NormNum.isNat_eq_false and 5 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2013P2.pt The j-th vertex of a regular 4027-gon inscribed in the unit circle line 955 source
Source documentation
The j-th vertex of a regular 4027-gon inscribed in the unit circle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2013P2.Pt
Proof uses: WithLp.toLp, OfNat.ofNat, ENNReal, Fin, Real, Matrix.vecCons, Real.cos, Imo2013P2.ang, Real.sin, Matrix.vecEmpty
6 instances, coercions and auxiliary constants left out.
```
noncomputable def pt (j : ℕ) : Pt := !₂[Real.cos (ang j), Real.sin (ang j)]
```
Mentions: Imo2013P2.Pt, Imo2013P2.ang
theorem Imo2013P2.pt_apply0 line 957 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Fin, OfNat.ofNat, Real, WithLp.ofLp, ENNReal, Imo2013P2.pt, Real.cos, Imo2013P2.ang
Proof uses: rfl
16 instances, coercions and auxiliary constants left out.
theorem Imo2013P2.pt_apply1 line 959 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Fin, OfNat.ofNat, Real, WithLp.ofLp, ENNReal, Imo2013P2.pt, Real.sin, Imo2013P2.ang
Proof uses: rfl
16 instances, coercions and auxiliary constants left out.
theorem Imo2013P2.inner_pt_eq line 961 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Nat, Eq, Real, Inner.inner, OfNat.ofNat, ENNReal, Fin, Imo2013P2.pt, HAdd.hAdd, HMul.hMul, WithLp.ofLp, Real.cos, Imo2013P2.ang, Real.sin
Proof uses: Eq.mpr, id, congrArg, Imo2013P2.inner_pt, Imo2013P2.pt_apply0, Imo2013P2.pt_apply1, Eq.refl
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.pt_inj line 965 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Imo2013P2.Pt, Imo2013P2.pt
Proof uses: Fin, Real, WithLp.ofLp, ENNReal, Eq.mpr, id, congrArg, Eq.refl, Real.cos, HSub.hSub, Imo2013P2.ang, HAdd.hAdd, HMul.hMul, Real.sin, Real.cos_sub, Mathlib.Tactic.LinearCombination.eq_of_eq, HPow.hPow, Real.sin_sq_add_cos_sq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq and 80 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.dist_pt_zero line 989 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Dist.dist, Imo2013P2.Pt, OfNat.ofNat, ENNReal, Fin, Imo2013P2.pt
Proof uses: Eq.mpr, Norm.norm, id, congrArg, dist_zero_right, Real.sqrt, Inner.inner, norm_eq_sqrt_real_inner, HAdd.hAdd, HMul.hMul, WithLp.ofLp, Real.cos, Imo2013P2.ang, Real.sin, Imo2013P2.inner_pt_eq, Imo2013P2.pt_apply0, Imo2013P2.pt_apply1, Mathlib.Tactic.LinearCombination.eq_of_eq, HPow.hPow, Real.sin_sq_add_cos_sq and 57 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Imo2013P2.redPts The red points: vertices with odd indices line 997 source
Source documentation
The red points: vertices with odd indices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2013P2.Pt
Proof uses: Finset.image, Nat, OfNat.ofNat, ENNReal, Fin, Real, Imo2013P2.pt, HAdd.hAdd, HMul.hMul, Finset.range
14 instances, coercions and auxiliary constants left out.
```
noncomputable def redPts : Finset Pt :=
…
```
Mentions: Imo2013P2.Pt
def Imo2013P2.bluePts The blue points: vertices with even indices line 1001 source
Source documentation
The blue points: vertices with even indices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2013P2.Pt
Proof uses: Finset.image, Nat, OfNat.ofNat, ENNReal, Fin, Real, Imo2013P2.pt, HMul.hMul, Finset.range
12 instances, coercions and auxiliary constants left out.
```
noncomputable def bluePts : Finset Pt :=
…
```
Mentions: Imo2013P2.Pt
theorem Imo2013P2.redPts_card line 1004 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Imo2013P2.Pt, Imo2013P2.redPts, OfNat.ofNat
Proof uses: Eq.mpr, Finset.image, ENNReal, Fin, Real, Imo2013P2.pt, HAdd.hAdd, HMul.hMul, Finset.range, id, congrArg, Finset, Imo2013P2.redPts.eq_1, Finset.card_image_of_injOn, Membership.mem, Set, Imo2013P2.pt_inj, Eq.mp, Set.Iio, LT.lt and 5 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.bluePts_card line 1011 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Imo2013P2.Pt, Imo2013P2.bluePts, OfNat.ofNat
Proof uses: Eq.mpr, Finset.image, ENNReal, Fin, Real, Imo2013P2.pt, HMul.hMul, Finset.range, id, congrArg, Finset, Imo2013P2.bluePts.eq_1, Finset.card_image_of_injOn, Membership.mem, Set, Imo2013P2.pt_inj, Eq.mp, Set.Iio, LT.lt, propext and 4 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.red_blue_disjoint line 1018 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Disjoint, Finset, Imo2013P2.Pt, Imo2013P2.redPts, Imo2013P2.bluePts
Proof uses: Eq.mpr, Membership.mem, Not, id, Eq, congrArg, propext, Finset.disjoint_left, Nat, And, Finset.range, OfNat.ofNat, Imo2013P2.pt, HAdd.hAdd, HMul.hMul, Exists, False, Eq.mp, Finset.image, ENNReal and 8 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem Imo2013P2.mem_pts line 1029 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Membership.mem, Finset, Union.union, OfNat.ofNat, ENNReal, Fin, Nat, Real, Imo2013P2.redPts, Imo2013P2.bluePts, Exists, And, LT.lt, Eq, Imo2013P2.pt
Proof uses: Or, Eq.mp, congrArg, propext, Finset.mem_union, Finset.range, HAdd.hAdd, HMul.hMul, Finset.image, Finset.mem_image, Imo2013P2.redPts.eq_1, Exists.intro, And.intro, Finset.mem_range, rfl, Imo2013P2.bluePts.eq_1
38 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
def Imo2013P2.lowerCfg The Colombian configuration witnessing the lower bound: the vertices of a regular 4027-gon, colored red at odd indices and blue at even indices line 1043 source
Source documentation
The Colombian configuration witnessing the lower bound: the vertices of a regular 4027-gon, colored red at odd indices and blue at even indices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.ColombianConfiguration
Proof uses: Imo2013P2.ColombianConfiguration.mk, Imo2013P2.redPts, Imo2013P2.bluePts, Imo2013P2.redPts_card, Imo2013P2.bluePts_card, Imo2013P2.red_blue_disjoint
1 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
noncomputable def lowerCfg : ColombianConfiguration where
…
```
Mentions: Imo2013P2.ColombianConfiguration
theorem Imo2013P2.sinusoid_roots A sinusoid r ↦ n 0 * cos r + n 1 * sin r with n ≠ 0 takes any value at most twice on an interval shorter than a full period line 1064 source
Source documentation
A sinusoid r ↦ n 0 * cos r + n 1 * sin r with n ≠ 0 takes any value at most twice on an interval shorter than a full period.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Ne, OfNat.ofNat, ENNReal, Fin, Nat, Real, LT.lt, HSub.hSub, HMul.hMul, Real.pi, Eq, HAdd.hAdd, WithLp.ofLp, Real.cos, Real.sin, False
Proof uses: Real.pi_pos, HDiv.hDiv, Real.sin_pos_of_pos_of_lt_pi, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf and 108 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
theorem sinusoid_roots {n : Pt} (hn : n ≠ 0) {c : ℝ} {r₁ r₂ r₃ : ℝ}
    (h₁₂ : r₁ < r₂) (h₂₃ : r₂ < r₃) (hspan : r₃ - r₁ < 2 * Real.pi)
    (e₁ : n 0 * Real.cos r₁ + n 1 * Real.sin r₁ = c)
    (e₂ : n 0 * Real.cos r₂ + n 1 * Real.sin r₂ = c)
    (e₃ : n 0 * Real.cos r₃ + n 1 * Real.sin r₃ = c) : False := by
…
```
Mentions: Imo2013P2.Pt, Imo2013P2.e₁
theorem Imo2013P2.exists_root_pair Documented declaration: exists_root_pair line 1109 source
Source documentation
If a line {x | ⟪n, x⟫ = c} strictly separates the adjacent vertices pt j and pt (j+1), then the sinusoid r ↦ ⟪n, (cos r, sin r)⟫ takes the value c somewhere strictly between their angles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Real, Nat, Or, And, LT.lt, Inner.inner, OfNat.ofNat, ENNReal, Fin, Imo2013P2.pt, HAdd.hAdd, Exists, Membership.mem, Set, Set.Ioo, Imo2013P2.ang, Eq, HMul.hMul, WithLp.ofLp and 2 more
Proof uses: Imo2013P2.ang_lt_ang, Nat.lt_succ_self, Continuous, Continuous.comp', Prod, Prod.mk, Prod.fst, Prod.snd, continuous_add, Continuous.prodMk, Continuous.const_mul, Real.continuous_cos, Real.continuous_sin, Eq.mp, congrArg, Imo2013P2.inner_pt_eq, intermediate_value_Ioo, LT.lt.le, Continuous.continuousOn, Set.Icc and 1 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem exists_root_pair {n : Pt} {c : ℝ} {j : ℕ}
    (h : ⟪n, pt j⟫ < c ∧ c < ⟪n, pt (j + 1)⟫ ∨
         ⟪n, pt (j + 1)⟫ < c ∧ c < ⟪n, pt j⟫) :
    ∃ r ∈ Set.Ioo (ang j) (ang (j + 1)),
      n 0 * Real.cos r + n 1 * Real.sin r = c := by
…
```
Mentions: Imo2013P2.Pt, h, Imo2013P2.pt, Imo2013P2.ang
theorem Imo2013P2.seps_card_le_two A single line strictly separates at most two of the 4026 adjacent vertex pairs of the regular 4027-gon line 1124 source
Source documentation
A single line strictly separates at most two of the 4026 adjacent vertex pairs of the regular 4027-gon.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2013P2.Pt, Ne, OfNat.ofNat, ENNReal, Fin, Nat, Real, Finset, Membership.mem, LT.lt, Or, And, Inner.inner, Imo2013P2.pt, HAdd.hAdd, LE.le, Finset.card
Proof uses: Decidable.byContradiction, Not, Exists, False, Iff.mp, Finset.two_lt_card, Eq.mp, Set, Set.Ioo, Imo2013P2.ang, Eq, HMul.hMul, WithLp.ofLp, Real.cos, Real.sin, Imo2013P2.exists_root_pair, LT.lt.trans, LT.lt.trans_le, And.right, congrArg and 65 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
theorem seps_card_le_two {n : Pt} (hn : n ≠ 0) {c : ℝ} {s : Finset ℕ}
    (hs : ∀ j ∈ s, j < 4026)
    (hsep : ∀ j ∈ s, ⟪n, pt j⟫ < c ∧ c < ⟪n, pt (j + 1)⟫ ∨
                     ⟪n, pt (j + 1)⟫ < c ∧ c < ⟪n, pt j⟫) :
    s.card ≤ 2 := by
…
```
Mentions: Imo2013P2.Pt, Imo2013P2.pt
theorem Imo2013P2.lower_bound Documented declaration: lower_bound line 1164 source
Source documentation
No good arrangement for lowerCfg has fewer than 2013 lines: each of the 4026 adjacent opposite-colored vertex pairs must be separated by some line, and each line separates at most two of them.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, AffineSubspace, Real, Imo2013P2.Pt, OfNat.ofNat, ENNReal, Imo2013P2.GoodArrangement, Imo2013P2.lowerCfg, LE.le
Proof uses: Eq, Module.finrank, Subtype, Membership.mem, Submodule, AffineSubspace.direction, And, Finset, Union.union, Imo2013P2.ColombianConfiguration.red, Imo2013P2.ColombianConfiguration.blue, Not, Exists, AffineSubspace.SOppSide, LT.lt, Imo2013P2.pt, HAdd.hAdd, HMul.hMul, id, Eq.mpr and 58 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 73 steps
Open to load the checked before-and-after goal states.
```
theorem lower_bound {k : ℕ} (lines : Fin k → AffineSubspace ℝ Pt)
    (h : GoodArrangement lowerCfg lines) : 2013 ≤ k := by
…
```
Mentions: Imo2013P2.Pt, h, Imo2013P2.GoodArrangement, Imo2013P2.lowerCfg
determine Imo2013P2.solution_value line 1229 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Imo2013P2.imo2013_p2 line 1231 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Imo2013P2.ColombianConfiguration, Exists, Fin, AffineSubspace, Real, Imo2013P2.Pt, OfNat.ofNat, ENNReal, Imo2013P2.GoodArrangement, Imo2013P2.solution_value
Proof uses: And.intro, Membership.mem, Set, lowerBounds, Imo2013P2.upper_bound, Imo2013P2.lowerCfg, LE.le, Imo2013P2.lower_bound
56 instances, coercions and auxiliary constants left out.

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