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

133 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2014, Problem 6

A set of lines in the plane is in general position if no two are parallel and no three pass through the same point. A set of lines in general position cuts the plane into regions, some of which have finite area; we call these its finite regions. Prove that for all sufficiently large n, in any set of n lines in general position it is possible to colour at least √n lines blue in such a way that none of its finite regions has a completely blue boundary.

Imports (7)

Imported by 1 file

Compfiles.lean

structure Imo2014P6.Line A line in the plane ℝ × ℝ, given by the equation a * x + b * y + c = 0 with (a, b) ≠ (0, 0) line 37 source
Source documentation
A line in the plane ℝ × ℝ, given by the equation a * x + b * y + c = 0 with (a, b) ≠ (0, 0).

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure Line where
…
```
instance Imo2014P6.(instance at line 43) line 43 source
def Imo2014P6.Line.val The affine function whose zero set is the line line 48 source
Source documentation
The affine function whose zero set is the line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Prod, Real
Proof uses: HAdd.hAdd, HMul.hMul, Imo2014P6.Line.a, Prod.fst, Imo2014P6.Line.b, Prod.snd, Imo2014P6.Line.c
4 instances, coercions and auxiliary constants left out.
```
def val (ℓ : Line) (p : ℝ × ℝ) : ℝ := ℓ.a * p.1 + ℓ.b * p.2 + ℓ.c
```
Mentions: Imo2014P6.Line
def Imo2014P6.Line.set The line as a set of points line 51 source
Source documentation
The line as a set of points.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Set, Prod, Real
Proof uses: Set.ofPred, Eq, Imo2014P6.Line.val, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
```
def set (ℓ : Line) : Set (ℝ × ℝ) := {p | ℓ.val p = 0}
```
Mentions: Imo2014P6.Line
def Imo2014P6.Line.det The determinant of the two normals; nonzero iff the lines are not parallel line 54 source
Source documentation
The determinant of the two normals; nonzero iff the lines are not parallel.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Real
Proof uses: HSub.hSub, HMul.hMul, Imo2014P6.Line.a, Imo2014P6.Line.b
4 instances, coercions and auxiliary constants left out.
```
def det (ℓ m : Line) : ℝ := ℓ.a * m.b - m.a * ℓ.b
```
Mentions: Imo2014P6.Line
def Imo2014P6.Line.interPt The intersection point of two non-parallel lines line 57 source
Source documentation
The intersection point of two non-parallel lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Prod, Real
Proof uses: Prod.mk, HDiv.hDiv, HSub.hSub, HMul.hMul, Imo2014P6.Line.b, Imo2014P6.Line.c, Imo2014P6.Line.det, Imo2014P6.Line.a
7 instances, coercions and auxiliary constants left out.
```
noncomputable def interPt (ℓ m : Line) : ℝ × ℝ :=
…
```
Mentions: Imo2014P6.Line
def Imo2014P6.GeneralPosition A set of lines is in general position if no two are parallel and no three pass through the same point line 64 source
Source documentation
A set of lines is in general position if no two are parallel and no three pass through the same point.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line
Proof uses: And, Membership.mem, Ne, Real, Imo2014P6.Line.det, OfNat.ofNat, Imo2014P6.Line.val, Imo2014P6.Line.interPt
4 instances, coercions and auxiliary constants left out.
```
def GeneralPosition (L : Finset Line) : Prop :=
…
```
Mentions: Imo2014P6.Line
def Imo2014P6.sgn The sign ±1 attached to a side of a line line 69 source
Source documentation
The sign ±1 attached to a side of a line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, Real
Proof uses: ite, Eq, Bool.true, OfNat.ofNat, Neg.neg
4 instances, coercions and auxiliary constants left out.
```
def sgn (b : Bool) : ℝ := if b then 1 else -1
```
def Imo2014P6.Cell The cell of a sign vector σ: the set of points lying on the prescribed side of every line of L line 75 source
Source documentation
The cell of a sign vector σ: the set of points lying on the prescribed side of every line of L. The nonempty cells are exactly the regions into which the lines of L cut the plane, and the bounded nonempty cells are its finite regions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Bool, Set, Prod, Real
Proof uses: Set.ofPred, Membership.mem, GT.gt, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.val, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
def Cell (L : Finset Line) (σ : Line → Bool) : Set (ℝ × ℝ) :=
…
```
Mentions: Imo2014P6.Line
lemma Imo2014P6.Line.val_interPt_left line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Ne, Real, Imo2014P6.Line.det, OfNat.ofNat, Eq, Imo2014P6.Line.val, Imo2014P6.Line.interPt
Proof uses: HAdd.hAdd, HMul.hMul, Imo2014P6.Line.a, HSub.hSub, Imo2014P6.Line.b, Imo2014P6.Line.c, id, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 42 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Line.val_interPt_right line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Ne, Real, Imo2014P6.Line.det, OfNat.ofNat, Eq, Imo2014P6.Line.val, Imo2014P6.Line.interPt
Proof uses: HAdd.hAdd, HMul.hMul, Imo2014P6.Line.a, HSub.hSub, Imo2014P6.Line.b, Imo2014P6.Line.c, id, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 42 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Line.eq_interPt line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Ne, Real, Imo2014P6.Line.det, OfNat.ofNat, Prod, Eq, Imo2014P6.Line.val, Imo2014P6.Line.interPt
Proof uses: HSub.hSub, HMul.hMul, Imo2014P6.Line.a, Imo2014P6.Line.b, HAdd.hAdd, Prod.fst, Prod.snd, Neg.neg, Imo2014P6.Line.c, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat, Nat.rawCast and 57 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
def Imo2014P6.Line.base A distinguished point on the line: the foot of the perpendicular from the origin line 149 source
Source documentation
A distinguished point on the line: the foot of the perpendicular from the origin.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Prod, Real
Proof uses: Prod.mk, HDiv.hDiv, HMul.hMul, Neg.neg, Imo2014P6.Line.c, Imo2014P6.Line.a, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, Imo2014P6.Line.b
13 instances, coercions and auxiliary constants left out.
```
noncomputable def base (ℓ : Line) : ℝ × ℝ :=
…
```
Mentions: Imo2014P6.Line
def Imo2014P6.Line.dir A direction vector of the line: the normal (a, b) rotated by 90 degrees line 153 source
Source documentation
A direction vector of the line: the normal (a, b) rotated by 90 degrees.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Prod, Real
Proof uses: Prod.mk, Neg.neg, Imo2014P6.Line.b, Imo2014P6.Line.a
1 instances, coercions and auxiliary constants left out.
```
def dir (ℓ : Line) : ℝ × ℝ := (-ℓ.b, ℓ.a)
```
Mentions: Imo2014P6.Line
def Imo2014P6.Line.param The standard parametrization of the line by ℝ line 156 source
Source documentation
The standard parametrization of the line by ℝ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Real, Prod
Proof uses: Prod.mk, HAdd.hAdd, Prod.fst, Imo2014P6.Line.base, HMul.hMul, Imo2014P6.Line.dir, Prod.snd
4 instances, coercions and auxiliary constants left out.
```
noncomputable def param (ℓ : Line) (t : ℝ) : ℝ × ℝ :=
…
```
Mentions: Imo2014P6.Line
lemma Imo2014P6.Line.sq_add_sq_pos line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, LT.lt, Real, OfNat.ofNat, HAdd.hAdd, HPow.hPow, Nat, Imo2014P6.Line.a, Imo2014P6.Line.b
Proof uses: Ne, Or, Imo2014P6.Line.hab, sq_pos_of_ne_zero, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero and 48 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Line.val_base line 166 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Line.base, OfNat.ofNat
Proof uses: Ne, HAdd.hAdd, HPow.hPow, Nat, Imo2014P6.Line.a, Imo2014P6.Line.b, ne_of_gt, Imo2014P6.Line.sq_add_sq_pos, id, Eq.mpr, HMul.hMul, HDiv.hDiv, Neg.neg, Imo2014P6.Line.c, inferInstance, CommGroupWithZero, GroupWithZero, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons and 87 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Line.val_param line 172 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Real, Eq, Imo2014P6.Line.val, Imo2014P6.Line.param, OfNat.ofNat
Proof uses: Imo2014P6.Line.base, Imo2014P6.Line.val_base, id, Mathlib.Tactic.LinearCombination.eq_of_eq, HAdd.hAdd, HMul.hMul, Imo2014P6.Line.a, Prod.fst, Imo2014P6.Line.b, Prod.snd, Imo2014P6.Line.c, Neg.neg, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, HSub.hSub, Mathlib.Tactic.Ring.Common.sub_congr, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr and 43 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Line.val_param_eq line 177 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Real, Eq, Imo2014P6.Line.val, Imo2014P6.Line.param, HAdd.hAdd, HMul.hMul, Imo2014P6.Line.det, Imo2014P6.Line.base
Proof uses: id, Mathlib.Tactic.Ring.of_eq, Imo2014P6.Line.a, Prod.fst, Neg.neg, Imo2014P6.Line.b, Prod.snd, Imo2014P6.Line.c, HSub.hSub, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, OfNat.ofNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf and 31 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Line.param_injective line 182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Function.Injective, Real, Prod, Imo2014P6.Line.param
Proof uses: Eq, HAdd.hAdd, Prod.fst, Imo2014P6.Line.base, HMul.hMul, Neg.neg, Imo2014P6.Line.b, Prod.snd, Imo2014P6.Line.a, And, Eq.mp, Prod.mk.injEq, Ne, OfNat.ofNat, Or, Imo2014P6.Line.hab, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl and 59 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Line.mem_set_of_param line 192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Real, Membership.mem, Prod, Set, Imo2014P6.Line.set, Imo2014P6.Line.param
Proof uses: Imo2014P6.Line.val_param
1 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Line.exists_param_of_mem_set line 194 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Prod, Real, Membership.mem, Set, Imo2014P6.Line.set, Exists, Eq, Imo2014P6.Line.param
Proof uses: HAdd.hAdd, HMul.hMul, Imo2014P6.Line.a, Prod.fst, Imo2014P6.Line.b, Prod.snd, Neg.neg, Imo2014P6.Line.c, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat and 103 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.GP.det_ne line 228 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.GeneralPosition, Membership.mem, Ne, Real, Imo2014P6.Line.det, OfNat.ofNat
Proof uses: And.left, Imo2014P6.Line.val, Imo2014P6.Line.interPt
8 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.GP.not_concurrent line 231 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.GeneralPosition, Membership.mem, Ne, Prod, Real, Eq, Imo2014P6.Line.val, OfNat.ofNat, False
Proof uses: Imo2014P6.Line.det, Imo2014P6.GP.det_ne, Imo2014P6.Line.interPt, Imo2014P6.Line.eq_interPt, And.right, Eq.mp, congrArg
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.GP.eq_of_val_eq_zero Any line through the intersection of two distinct lines of L is one of them line 240 source
Source documentation
Any line through the intersection of two distinct lines of L is one of them.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.GeneralPosition, Membership.mem, Ne, Prod, Real, Eq, Imo2014P6.Line.val, OfNat.ofNat, Or
Proof uses: dite, Or.inl, Not, Or.inr, False.elim, Imo2014P6.GP.not_concurrent, Ne.symm
9 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma eq_of_val_eq_zero {ℓ m n : Line} (hℓ : ℓ ∈ L) (hm : m ∈ L) (hn : n ∈ L)
    (hd : ℓ ≠ m) {p : ℝ × ℝ}
    (hp₁ : ℓ.val p = 0) (hp₂ : m.val p = 0) (hp₃ : n.val p = 0) : n = ℓ ∨ n = m := by
…
```
Mentions: Imo2014P6.Line
lemma Imo2014P6.sgn_ne_zero line 251 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, Ne, Real, Imo2014P6.sgn, OfNat.ofNat
Proof uses: Eq, Bool.false, of_eq_true, Eq.trans, Neg.neg, True, congrFun', congrArg, ite_eq_right_of_eq_false, Bool.true, False, Bool.false_eq_true, eq_false, not_false, eq_true, Not, Mathlib.Meta.NormNum.isInt_eq_false, Int.negOfNat, Int.ofNat, Mathlib.Meta.NormNum.isInt_neg and 11 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.sgn_cases line 253 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, Or, Eq, Real, Imo2014P6.sgn, OfNat.ofNat, Neg.neg
Proof uses: Bool.false, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', ite_eq_right_of_eq_false, Bool.true, Bool.false_eq_true, eq_self, or_true, Eq.symm, ite_eq_left_of_eq_true, true_or, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.sgn_mul_self line 255 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, Eq, Real, HMul.hMul, Imo2014P6.sgn, OfNat.ofNat
Proof uses: Bool.false, of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAddMonoidWithOne, congrFun', congrArg, Neg.neg, congr, ite_eq_right_of_eq_false, Bool.true, False, Bool.false_eq_true, eq_false, not_false, mul_neg, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.isInt_neg, Int.negOfNat and 13 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Line.continuous_val line 257 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Continuous, Prod, Real, Imo2014P6.Line.val
Proof uses: id, Continuous.add_const, HAdd.hAdd, HMul.hMul, Imo2014P6.Line.a, Prod.fst, Imo2014P6.Line.b, Prod.snd, Continuous.fun_add, Continuous.comp', continuous_const_mul, continuous_fst, continuous_snd, Imo2014P6.Line.c
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.isOpen_cell line 261 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Bool, IsOpen, Prod, Real, Imo2014P6.Cell
Proof uses: Eq, Set, Set.iInter, Membership.mem, Set.ofPred, GT.gt, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.val, OfNat.ofNat, Set.ext, of_eq_true, Iff, Eq.trans, LT.lt, True, congr, congrArg, congrFun', funext and 13 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.isClosed_cellCl line 270 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Bool, IsClosed, Prod, Real, Set.ofPred, Membership.mem, GE.ge, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.val, OfNat.ofNat
Proof uses: Eq, Set, Set.iInter, Set.ext, of_eq_true, Iff, Eq.trans, LE.le, True, congr, congrArg, congrFun', funext, forall_congr, implies_congr, Eq.refl, Set.iInter_congr_Prop, Iff.of_eq, iff_self, Eq.mpr and 6 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.closure_cell The closure of a nonempty cell is given by the corresponding weak inequalities line 282 source
Source documentation
The closure of a nonempty cell is given by the corresponding weak inequalities.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Bool, Set.Nonempty, Prod, Real, Imo2014P6.Cell, Eq, Set, closure, Set.ofPred, Membership.mem, GE.ge, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.val, OfNat.ofNat
Proof uses: Set.Subset.antisymm, closure_minimal, le_of_lt, Imo2014P6.isClosed_cellCl, Eq.mpr, GT.gt, Exists, And, LT.lt, Dist.dist, id, congrArg, propext, Metric.mem_closure_iff, dite, Exists.intro, And.intro, Eq.symm, dist_self, Not and 168 more
194 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
```
lemma closure_cell {L : Finset Line} {σ : Line → Bool} (hne : (Cell L σ).Nonempty) :
    closure (Cell L σ) = {p | ∀ ℓ ∈ L, sgn (σ ℓ) * ℓ.val p ≥ 0} := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.Cell, Imo2014P6.sgn
lemma Imo2014P6.frontier_cell The frontier of a cell: its closure minus itself line 321 source
Source documentation
The frontier of a cell: its closure minus itself.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Bool, Eq, Set, Prod, Real, frontier, Imo2014P6.Cell, SDiff.sdiff, closure
Proof uses: IsOpen.frontier_eq, Imo2014P6.isOpen_cell
9 instances, coercions and auxiliary constants left out.
```
lemma frontier_cell (L : Finset Line) (σ : Line → Bool) :
    frontier (Cell L σ) = closure (Cell L σ) \ Cell L σ :=
…
```
Mentions: Imo2014P6.Line, Imo2014P6.Cell
lemma Imo2014P6.mem_frontier_iff A point lies in the frontier of a nonempty cell iff all weak sign conditions hold and it lies on at least one line line 327 source
Source documentation
A point lies in the frontier of a nonempty cell iff all weak sign conditions hold and it lies on at least one line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Bool, Set.Nonempty, Prod, Real, Imo2014P6.Cell, Iff, Membership.mem, Set, frontier, And, GE.ge, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.val, OfNat.ofNat, Exists, Eq
Proof uses: Eq.mpr, SDiff.sdiff, closure, id, congrArg, Imo2014P6.frontier_cell, Set.ofPred, Imo2014P6.closure_cell, Iff.intro, And.intro, And.left, Not, Decidable.byContradiction, Ne, Exists.intro, LT.lt, Or, GT.gt, lt_or_eq_of_le, False.elim and 9 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma mem_frontier_iff {L : Finset Line} {σ : Line → Bool} (hne : (Cell L σ).Nonempty)
    {p : ℝ × ℝ} :
    p ∈ frontier (Cell L σ) ↔
      (∀ ℓ ∈ L, sgn (σ ℓ) * ℓ.val p ≥ 0) ∧ (∃ ℓ ∈ L, ℓ.val p = 0) := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.Cell, Imo2014P6.sgn
def Imo2014P6.ValidBlue The working definition of "no finite region has a completely blue boundary": for every nonempty bounded cell, some line meeting the closure of the cell is not blue line 360 source
Source documentation
The working definition of "no finite region has a completely blue boundary": for every nonempty bounded cell, some line meeting the closure of the cell is not blue.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line
Proof uses: Bool, Set.Nonempty, Prod, Real, Imo2014P6.Cell, Bornology.IsBounded, Exists, And, Membership.mem, Inter.inter, Set, closure, Imo2014P6.Line.set, Not
9 instances, coercions and auxiliary constants left out.
```
def ValidBlue (L B : Finset Line) : Prop :=
…
```
Mentions: Imo2014P6.Line
def Imo2014P6.Line.crossT The parameter value where the standard parametrization of ℓ crosses m line 374 source
Source documentation
The parameter value where the standard parametrization of ℓ crosses m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Real
Proof uses: HDiv.hDiv, Neg.neg, Imo2014P6.Line.val, Imo2014P6.Line.base, Imo2014P6.Line.det
4 instances, coercions and auxiliary constants left out.
```
noncomputable def crossT (ℓ m : Line) : ℝ := - m.val ℓ.base / ℓ.det m
```
Mentions: Imo2014P6.Line
lemma Imo2014P6.Line.val_param_crossT line 376 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Ne, Real, Imo2014P6.Line.det, OfNat.ofNat, Eq, Imo2014P6.Line.val, Imo2014P6.Line.param, Imo2014P6.Line.crossT
Proof uses: Eq.mpr, HAdd.hAdd, HMul.hMul, Imo2014P6.Line.base, id, congrArg, Imo2014P6.Line.val_param_eq, HDiv.hDiv, Neg.neg, Imo2014P6.Line.crossT.eq_1, Eq.symm, mul_div_assoc, mul_div_cancel_left₀, neg_add_cancel, Eq.refl
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Line.crossT_eq_of_val_param_eq_zero line 380 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Ne, Real, Imo2014P6.Line.det, OfNat.ofNat, Eq, Imo2014P6.Line.val, Imo2014P6.Line.param, Imo2014P6.Line.crossT
Proof uses: HMul.hMul, Neg.neg, Imo2014P6.Line.base, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 79 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Line.constraint_iff The sign constraint on m along the parametrization of ℓ, as a bound on t line 389 source
Source documentation
The sign constraint on m along the parametrization of ℓ, as a bound on t.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Bool, Ne, Real, Imo2014P6.Line.det, OfNat.ofNat, Iff, LE.le, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.val, Imo2014P6.Line.param, ite, LT.lt, Imo2014P6.Line.crossT
Proof uses: Eq.mpr, HAdd.hAdd, Imo2014P6.Line.base, id, Eq, congrArg, Imo2014P6.Line.val_param_eq, HSub.hSub, HDiv.hDiv, Neg.neg, inferInstance, CommGroupWithZero, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, List.nil, Prod, Int, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk and 91 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma constraint_iff {σ : Line → Bool} {ℓ m : Line} (hdet : ℓ.det m ≠ 0) (t : ℝ) :
    0 ≤ sgn (σ m) * m.val (ℓ.param t) ↔
      (if 0 < sgn (σ m) * ℓ.det m then ℓ.crossT m ≤ t else t ≤ ℓ.crossT m) := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.sgn
def Imo2014P6.lows The lines whose constraint is a lower bound on the parameter along ℓ line 412 source
Source documentation
The lines whose constraint is a lower bound on the parameter along ℓ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Bool
Proof uses: Finset.filter, And, Ne, LT.lt, Real, OfNat.ofNat, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.det, Eq
9 instances, coercions and auxiliary constants left out.
```
noncomputable def lows (L : Finset Line) (σ : Line → Bool) (ℓ : Line) : Finset Line :=
…
```
Mentions: Imo2014P6.Line
def Imo2014P6.upps The lines whose constraint is an upper bound on the parameter along ℓ line 416 source
Source documentation
The lines whose constraint is an upper bound on the parameter along ℓ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Bool
Proof uses: Finset.filter, And, Ne, LT.lt, Real, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.det, OfNat.ofNat, Eq
9 instances, coercions and auxiliary constants left out.
```
noncomputable def upps (L : Finset Line) (σ : Line → Bool) (ℓ : Line) : Finset Line :=
…
```
Mentions: Imo2014P6.Line
lemma Imo2014P6.mem_lows line 419 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Bool, Iff, Membership.mem, Imo2014P6.lows, And, Ne, LT.lt, Real, OfNat.ofNat, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.det
Proof uses: of_eq_true, Not, Eq, Eq.trans, True, congrFun', congrArg, Finset.filter, Finset.filter_congr, Iff.of_eq, Eq.refl, iff_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.mem_upps line 423 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Bool, Iff, Membership.mem, Imo2014P6.upps, And, Ne, LT.lt, Real, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.det, OfNat.ofNat
Proof uses: of_eq_true, Not, Eq, Eq.trans, True, congrFun', congrArg, Finset.filter, Finset.filter_congr, Iff.of_eq, Eq.refl, iff_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.lows_or_upps line 427 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Bool, Imo2014P6.GeneralPosition, Membership.mem, Ne, Or, Imo2014P6.lows, Imo2014P6.upps
Proof uses: Real, Imo2014P6.Line.det, OfNat.ofNat, Imo2014P6.GP.det_ne, Ne.symm, HMul.hMul, Imo2014P6.sgn, mul_ne_zero, Imo2014P6.sgn_ne_zero, LT.lt, lt_or_gt_of_ne, Or.inr, Iff.mpr, And, Imo2014P6.mem_upps, And.intro, Or.inl, Imo2014P6.mem_lows
20 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.param_constraint_iff line 436 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.GeneralPosition, Membership.mem, Bool, Real, Iff, LE.le, OfNat.ofNat, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.val, Imo2014P6.Line.param, And, Imo2014P6.lows, Imo2014P6.Line.crossT, Imo2014P6.upps
Proof uses: Iff.intro, And.intro, Ne, LT.lt, Imo2014P6.Line.det, Iff.mp, Imo2014P6.mem_lows, Eq.mp, ite, congrArg, ite_eq_left, propext, Imo2014P6.Line.constraint_iff, Imo2014P6.GP.det_ne, Ne.symm, Imo2014P6.mem_upps, ite_eq_right, Iff.mpr, Not, not_lt and 12 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.abs_fst_sub_le_dist line 466 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Real, LE.le, abs, HSub.hSub, Prod.fst, Dist.dist
Proof uses: Eq.mpr, Norm.norm, id, Eq, congrArg, dist_eq_norm, Trans.trans, of_eq_true, eq_self, norm_fst_le
32 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.abs_snd_sub_le_dist line 471 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Real, LE.le, abs, HSub.hSub, Prod.snd, Dist.dist
Proof uses: Eq.mpr, Norm.norm, id, Eq, congrArg, dist_eq_norm, Trans.trans, of_eq_true, eq_self, norm_snd_le
32 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
structure Imo2014P6.EdgeCtx A bounded cell of an arrangement in general position, together with a distinguished boundary line ℓ line 478 source
Source documentation
A bounded cell of an arrangement in general position, together with a distinguished boundary line ℓ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line
```
structure EdgeCtx (L : Finset Line) where
…
```
Mentions: Imo2014P6.Line
lemma Imo2014P6.EdgeCtx.exists_abs_le The parameters of points of the closure of the cell on the line ℓ form a bounded set line 491 source
Source documentation
The parameters of points of the closure of the cell on the line ℓ form a bounded set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Exists, Real, Membership.mem, LE.le, OfNat.ofNat, HMul.hMul, Imo2014P6.sgn, Imo2014P6.EdgeCtx.σ, Imo2014P6.Line.val, Imo2014P6.Line.param, Imo2014P6.EdgeCtx.ℓ, abs
Proof uses: Set, Prod, closure, Imo2014P6.Cell, Metric.closedBall, Imo2014P6.Line.base, Bornology.IsBounded.subset_closedBall, Bornology.IsBounded.closure, Imo2014P6.EdgeCtx.hbdd, Eq.mpr, Set.ofPred, GE.ge, id, Eq, congrArg, Imo2014P6.closure_cell, Imo2014P6.EdgeCtx.hne, Ne, Imo2014P6.Line.a, Imo2014P6.Line.b and 32 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma exists_abs_le {L : Finset Line} (E : EdgeCtx L) : ∃ B : ℝ, ∀ t : ℝ,
    (∀ m ∈ L, 0 ≤ sgn (E.σ m) * m.val (E.ℓ.param t)) → |t| ≤ B := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.EdgeCtx, Imo2014P6.sgn
lemma Imo2014P6.EdgeCtx.exists_param_mem Some parameter realizes a point of the closure on ℓ line 522 source
Source documentation
Some parameter realizes a point of the closure on ℓ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Exists, Real, Membership.mem, LE.le, OfNat.ofNat, HMul.hMul, Imo2014P6.sgn, Imo2014P6.EdgeCtx.σ, Imo2014P6.Line.val, Imo2014P6.Line.param, Imo2014P6.EdgeCtx.ℓ
Proof uses: Prod, Set, Inter.inter, closure, Imo2014P6.Cell, Imo2014P6.Line.set, Set.Nonempty, Imo2014P6.EdgeCtx.hedge, Eq, Imo2014P6.Line.exists_param_of_mem_set, Exists.intro, Eq.mp, Set.ofPred, GE.ge, congrArg, Imo2014P6.closure_cell, Imo2014P6.EdgeCtx.hne
23 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma exists_param_mem {L : Finset Line} (E : EdgeCtx L) :
    ∃ t : ℝ, (∀ m ∈ L, 0 ≤ sgn (E.σ m) * m.val (E.ℓ.param t)) := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.EdgeCtx, Imo2014P6.sgn
lemma Imo2014P6.EdgeCtx.upps_nonempty line 530 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Finset.Nonempty, Imo2014P6.upps, Imo2014P6.EdgeCtx.σ, Imo2014P6.EdgeCtx.ℓ
Proof uses: Real, Membership.mem, LE.le, OfNat.ofNat, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.val, Imo2014P6.Line.param, abs, Exists, Imo2014P6.EdgeCtx.exists_abs_le, Imo2014P6.EdgeCtx.exists_param_mem, le_trans, abs_nonneg, Decidable.byContradiction, Not, HAdd.hAdd, Finset.sum, Imo2014P6.lows, Imo2014P6.Line.crossT and 71 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.EdgeCtx.lows_nonempty line 557 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Finset.Nonempty, Imo2014P6.lows, Imo2014P6.EdgeCtx.σ, Imo2014P6.EdgeCtx.ℓ
Proof uses: Real, Membership.mem, LE.le, OfNat.ofNat, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.val, Imo2014P6.Line.param, abs, Exists, Imo2014P6.EdgeCtx.exists_abs_le, Imo2014P6.EdgeCtx.exists_param_mem, le_trans, abs_nonneg, Decidable.byContradiction, Not, HSub.hSub, Neg.neg, HAdd.hAdd, Finset.sum and 74 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
def Imo2014P6.EdgeCtx.Tmin The lower endpoint of the edge, in parameter form line 585 source
Source documentation
The lower endpoint of the edge, in parameter form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Real
Proof uses: Finset.max', Finset.image, Imo2014P6.Line.crossT, Imo2014P6.EdgeCtx.ℓ, Imo2014P6.lows, Imo2014P6.EdgeCtx.σ
3 instances, coercions and auxiliary constants left out.
```
noncomputable def Tmin {L : Finset Line} (E : EdgeCtx L) : ℝ :=
…
```
Mentions: Imo2014P6.Line, Imo2014P6.EdgeCtx
def Imo2014P6.EdgeCtx.Tmax The upper endpoint of the edge, in parameter form line 589 source
Source documentation
The upper endpoint of the edge, in parameter form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Real
Proof uses: Finset.min', Finset.image, Imo2014P6.Line.crossT, Imo2014P6.EdgeCtx.ℓ, Imo2014P6.upps, Imo2014P6.EdgeCtx.σ
3 instances, coercions and auxiliary constants left out.
```
noncomputable def Tmax {L : Finset Line} (E : EdgeCtx L) : ℝ :=
…
```
Mentions: Imo2014P6.Line, Imo2014P6.EdgeCtx
lemma Imo2014P6.EdgeCtx.E_eq_Icc line 592 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Eq, Set, Real, Set.ofPred, Membership.mem, LE.le, OfNat.ofNat, HMul.hMul, Imo2014P6.sgn, Imo2014P6.EdgeCtx.σ, Imo2014P6.Line.val, Imo2014P6.Line.param, Imo2014P6.EdgeCtx.ℓ, Set.Icc, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.EdgeCtx.Tmax
Proof uses: Set.ext, id, Iff, Eq.mpr, And, Imo2014P6.lows, Imo2014P6.Line.crossT, Imo2014P6.upps, congrArg, propext, Imo2014P6.param_constraint_iff, Imo2014P6.EdgeCtx.hGP, Imo2014P6.EdgeCtx.hℓ, Set.mem_Icc, Iff.intro, And.intro, Finset.max'_le, Finset.image, Exists, Eq.mp and 7 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.EdgeCtx.Tmin_le_Tmax line 622 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, LE.le, Real, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.EdgeCtx.Tmax
Proof uses: Membership.mem, OfNat.ofNat, HMul.hMul, Imo2014P6.sgn, Imo2014P6.EdgeCtx.σ, Imo2014P6.Line.val, Imo2014P6.Line.param, Imo2014P6.EdgeCtx.ℓ, Exists, Imo2014P6.EdgeCtx.exists_param_mem, Set, Set.Icc, Eq.mpr, Set.ofPred, id, Eq, congrArg, Eq.symm, Imo2014P6.EdgeCtx.E_eq_Icc, LE.le.trans and 2 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.EdgeCtx.exists_low_cross line 629 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Exists, And, Membership.mem, Imo2014P6.lows, Imo2014P6.EdgeCtx.σ, Imo2014P6.EdgeCtx.ℓ, Eq, Real, Imo2014P6.Line.crossT, Imo2014P6.EdgeCtx.Tmin
Proof uses: Finset.image, Finset.max', Iff.mpr, Finset.Nonempty, Finset.image_nonempty, Imo2014P6.EdgeCtx.lows_nonempty, Finset.max'_mem, Eq.mp, Exists.intro, And.intro
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.EdgeCtx.exists_upp_cross line 637 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Exists, And, Membership.mem, Imo2014P6.upps, Imo2014P6.EdgeCtx.σ, Imo2014P6.EdgeCtx.ℓ, Eq, Real, Imo2014P6.Line.crossT, Imo2014P6.EdgeCtx.Tmax
Proof uses: Finset.image, Finset.min', Iff.mpr, Finset.Nonempty, Finset.image_nonempty, Imo2014P6.EdgeCtx.upps_nonempty, Finset.min'_mem, Eq.mp, Exists.intro, And.intro
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.EdgeCtx.Tmin_lt_Tmax The two endpoints are distinct: they would otherwise give three concurrent lines line 646 source
Source documentation
The two endpoints are distinct: they would otherwise give three concurrent lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, LT.lt, Real, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.EdgeCtx.Tmax
Proof uses: And, Membership.mem, Imo2014P6.lows, Imo2014P6.EdgeCtx.σ, Imo2014P6.EdgeCtx.ℓ, Eq, Imo2014P6.Line.crossT, Exists, Imo2014P6.EdgeCtx.exists_low_cross, Imo2014P6.upps, Imo2014P6.EdgeCtx.exists_upp_cross, Ne, OfNat.ofNat, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.det, Iff.mp, Imo2014P6.mem_lows, Imo2014P6.mem_upps, False.elim and 69 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma Tmin_lt_Tmax {L : Finset Line} (E : EdgeCtx L) : E.Tmin < E.Tmax := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.EdgeCtx
lemma Imo2014P6.EdgeCtx.val_ne_zero_of_mem_Ioo The pullback of the edge along the parametrization contains no crossing in its interior line 671 source
Source documentation
The pullback of the edge along the parametrization contains no crossing in its interior.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Membership.mem, Ne, Imo2014P6.EdgeCtx.ℓ, Real, Set, Set.Ioo, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.EdgeCtx.Tmax, Imo2014P6.Line.val, Imo2014P6.Line.param, OfNat.ofNat
Proof uses: Eq, Imo2014P6.lows, Imo2014P6.EdgeCtx.σ, Imo2014P6.upps, Or, False, Imo2014P6.lows_or_upps, Imo2014P6.EdgeCtx.hGP, Imo2014P6.EdgeCtx.hℓ, Imo2014P6.Line.crossT, Imo2014P6.Line.crossT_eq_of_val_param_eq_zero, Imo2014P6.GP.det_ne, Ne.symm, LE.le, Finset.le_max', Finset.image, Finset.mem_image_of_mem, False.elim, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp and 57 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma val_ne_zero_of_mem_Ioo {L : Finset Line} (E : EdgeCtx L) {m : Line} (hm : m ∈ L)
    (hmℓ : m ≠ E.ℓ) {t : ℝ}
    (ht : t ∈ Set.Ioo E.Tmin E.Tmax) : m.val (E.ℓ.param t) ≠ 0 := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.EdgeCtx
lemma Imo2014P6.EdgeCtx.param_mem_closure_inter The parametrized points of the edge segment lie in the closure of the cell and on the line line 689 source
Source documentation
The parametrized points of the edge segment lie in the closure of the cell and on the line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Real, Membership.mem, Set, Set.Icc, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.EdgeCtx.Tmax, Prod, Inter.inter, closure, Imo2014P6.Cell, Imo2014P6.EdgeCtx.σ, Imo2014P6.Line.set, Imo2014P6.EdgeCtx.ℓ, Imo2014P6.Line.param
Proof uses: And.intro, Eq.mpr, Set.ofPred, GE.ge, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.val, OfNat.ofNat, id, Eq, congrArg, Imo2014P6.closure_cell, Imo2014P6.EdgeCtx.hne, LE.le, Imo2014P6.EdgeCtx.E_eq_Icc, Imo2014P6.Line.val_param
20 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma param_mem_closure_inter {L : Finset Line} (E : EdgeCtx L) {t : ℝ}
    (ht : t ∈ Set.Icc E.Tmin E.Tmax) :
    E.ℓ.param t ∈ closure (Cell L E.σ) ∩ E.ℓ.set := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.EdgeCtx, Imo2014P6.Cell
lemma Imo2014P6.EdgeCtx.exists_line_at_Tmax At the upper endpoint, some other line of the arrangement passes: the line realizing the upper bound line 702 source
Source documentation
At the upper endpoint, some other line of the arrangement passes: the line realizing the upper bound.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Exists, And, Membership.mem, Ne, Imo2014P6.EdgeCtx.ℓ, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Line.param, Imo2014P6.EdgeCtx.Tmax, OfNat.ofNat
Proof uses: Imo2014P6.upps, Imo2014P6.EdgeCtx.σ, Imo2014P6.Line.crossT, Imo2014P6.EdgeCtx.exists_upp_cross, LT.lt, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.det, Iff.mp, Imo2014P6.mem_upps, Exists.intro, And.intro, And.left, And.right, Eq.mpr, id, congrArg, Eq.symm, Imo2014P6.Line.val_param_crossT, Imo2014P6.GP.det_ne and 3 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma exists_line_at_Tmax {L : Finset Line} (E : EdgeCtx L) :
    ∃ m ∈ L, m ≠ E.ℓ ∧ m.val (E.ℓ.param E.Tmax) = 0 := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.EdgeCtx
lemma Imo2014P6.EdgeCtx.exists_line_at_Tmin At the lower endpoint, some other line of the arrangement passes line 711 source
Source documentation
At the lower endpoint, some other line of the arrangement passes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Exists, And, Membership.mem, Ne, Imo2014P6.EdgeCtx.ℓ, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Line.param, Imo2014P6.EdgeCtx.Tmin, OfNat.ofNat
Proof uses: Imo2014P6.lows, Imo2014P6.EdgeCtx.σ, Imo2014P6.Line.crossT, Imo2014P6.EdgeCtx.exists_low_cross, LT.lt, HMul.hMul, Imo2014P6.sgn, Imo2014P6.Line.det, Iff.mp, Imo2014P6.mem_lows, Exists.intro, And.intro, And.left, And.right, Eq.mpr, id, congrArg, Eq.symm, Imo2014P6.Line.val_param_crossT, Imo2014P6.GP.det_ne and 3 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma exists_line_at_Tmin {L : Finset Line} (E : EdgeCtx L) :
    ∃ m ∈ L, m ≠ E.ℓ ∧ m.val (E.ℓ.param E.Tmin) = 0 := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.EdgeCtx
lemma Imo2014P6.EdgeCtx.eq_of_val_at_param At most one other line passes through an endpoint (general position) line 720 source
Source documentation
At most one other line passes through an endpoint (general position).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.EdgeCtx, Membership.mem, Ne, Imo2014P6.EdgeCtx.ℓ, Real, Eq, Imo2014P6.Line.val, Imo2014P6.Line.param, OfNat.ofNat
Proof uses: dite, Not, False.elim, Imo2014P6.GP.not_concurrent, Imo2014P6.EdgeCtx.hGP, Imo2014P6.EdgeCtx.hℓ, Ne.symm, Imo2014P6.Line.val_param
9 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma eq_of_val_at_param {L : Finset Line} (E : EdgeCtx L) {m n : Line} (hm : m ∈ L)
    (hn : n ∈ L) (hmℓ : m ≠ E.ℓ) (hnℓ : n ≠ E.ℓ) {t : ℝ}
    (hmt : m.val (E.ℓ.param t) = 0) (hnt : n.val (E.ℓ.param t) = 0) : m = n := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.EdgeCtx
lemma Imo2014P6.Line.det_comm line 731 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Eq, Real, Imo2014P6.Line.det, Neg.neg
Proof uses: id, Mathlib.Tactic.Ring.of_eq, HSub.hSub, HMul.hMul, Imo2014P6.Line.a, Imo2014P6.Line.b, HAdd.hAdd, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, OfNat.ofNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 29 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
structure Imo2014P6.Witness A witness region for a red line ℓ: a bounded cell of the arrangement whose boundary lines are all blue, except ℓ, which does occur on the boundary line 745 source
Source documentation
A witness region for a red line ℓ: a bounded cell of the arrangement whose boundary lines are all blue, except ℓ, which does occur on the boundary.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line
```
structure Witness (L B : Finset Line) (ℓ : Line) where
…
```
Mentions: Imo2014P6.Line
def Imo2014P6.Witness.ectx The edge context of the red line ℓ line 757 source
Source documentation
The edge context of the red line ℓ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Imo2014P6.EdgeCtx
Proof uses: Imo2014P6.EdgeCtx.mk, Imo2014P6.Witness.σ, Imo2014P6.Witness.hne, Imo2014P6.Witness.hbdd, Imo2014P6.Witness.hℓ
4 instances, coercions and auxiliary constants left out.
```
noncomputable def ectx (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) : EdgeCtx L :=
…
```
Mentions: Imo2014P6.GeneralPosition, Imo2014P6.EdgeCtx
def Imo2014P6.Witness.rT The parameter of the red point r: the endpoint of the red edge at which the clockwise traversal of the boundary leaves the red line line 762 source
Source documentation
The parameter of the red point r: the endpoint of the red edge at which the clockwise traversal of the boundary leaves the red line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Real
Proof uses: ite, Eq, Bool, Imo2014P6.Witness.σ, Bool.true, Imo2014P6.EdgeCtx.Tmax, Imo2014P6.Witness.ectx, Imo2014P6.EdgeCtx.Tmin
5 instances, coercions and auxiliary constants left out.
```
noncomputable def rT (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) : ℝ :=
…
```
Mentions: Imo2014P6.GeneralPosition
def Imo2014P6.Witness.r The red point associated to ℓ line 766 source
Source documentation
The red point associated to ℓ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Prod, Real
Proof uses: Imo2014P6.Line.param, Imo2014P6.Witness.rT
4 instances, coercions and auxiliary constants left out.
```
noncomputable def r (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) : ℝ × ℝ :=
…
```
Mentions: Imo2014P6.GeneralPosition
lemma Imo2014P6.Witness.rT_mem_Icc line 769 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Real, Set, Set.Icc, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.Witness.ectx, Imo2014P6.EdgeCtx.Tmax, Imo2014P6.Witness.rT
Proof uses: Eq.mpr, ite, Eq, Bool, Imo2014P6.Witness.σ, Bool.true, id, congrArg, Imo2014P6.Witness.rT.eq_1, Decidable, Not, ite_eq_right, Iff.mpr, LE.le, Set.left_mem_Icc, Imo2014P6.EdgeCtx.Tmin_le_Tmax, ite_eq_left, Set.right_mem_Icc
11 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Witness.r_mem_closure line 776 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Prod, Real, Set, Inter.inter, closure, Imo2014P6.Cell, Imo2014P6.Witness.σ, Imo2014P6.Line.set, Imo2014P6.Witness.r
Proof uses: Imo2014P6.EdgeCtx.param_mem_closure_inter, Imo2014P6.Witness.ectx, Imo2014P6.Witness.rT, Imo2014P6.Witness.rT_mem_Icc
10 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.rT_ne line 780 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, And, Ne, Real, Imo2014P6.Witness.rT, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.Witness.ectx, Imo2014P6.EdgeCtx.Tmax, False
Proof uses: Eq, Bool, Imo2014P6.Witness.σ, Bool.true, Decidable, Not, And.left, Eq.mp, ite, congr, congrArg, congrFun', ite_eq_right, Imo2014P6.Witness.rT.eq_1, rfl, And.right, ite_eq_left
6 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Witness.exists_g1 The other line through r exists line 790 source
Source documentation
The other line through r exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Exists, And, Ne, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Witness.r, OfNat.ofNat
Proof uses: Eq.mpr, Imo2014P6.Line.param, Imo2014P6.Witness.rT, id, congrArg, Prod, Imo2014P6.Witness.r.eq_1, ite, Bool, Imo2014P6.Witness.σ, Bool.true, Imo2014P6.EdgeCtx.Tmax, Imo2014P6.Witness.ectx, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.Witness.rT.eq_1, Decidable, Not, funext, congrFun', ite_eq_right and 3 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma exists_g1 (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) :
    ∃ g ∈ L, g ≠ ℓ ∧ g.val (W.r hGP hℓL) = 0 := by
…
```
Mentions: Imo2014P6.GeneralPosition
lemma Imo2014P6.Witness.g1_unique The other line through r is unique line 798 source
Source documentation
The other line through r is unique.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Ne, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Witness.r, OfNat.ofNat
Proof uses: Imo2014P6.EdgeCtx.eq_of_val_at_param, Imo2014P6.Witness.ectx, Imo2014P6.Witness.rT
8 instances, coercions and auxiliary constants left out.
```
lemma g1_unique (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) {g g' : Line}
    (hg : g ∈ L) (hg' : g' ∈ L) (hgℓ : g ≠ ℓ) (hg'ℓ : g' ≠ ℓ)
    (hgr : g.val (W.r hGP hℓL) = 0) (hg'r : g'.val (W.r hGP hℓL) = 0) : g = g' :=
…
```
Mentions: Imo2014P6.GeneralPosition, Imo2014P6.Line
def Imo2014P6.Witness.g1 The other line through r (a blue line) line 804 source
Source documentation
The other line through r (a blue line).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem
Proof uses: Classical.choose, And, Ne, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Witness.r, OfNat.ofNat, Imo2014P6.Witness.exists_g1
6 instances, coercions and auxiliary constants left out.
```
noncomputable def g1 (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) : Line :=
…
```
Mentions: Imo2014P6.GeneralPosition, Imo2014P6.Line
lemma Imo2014P6.Witness.g1_mem line 807 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Imo2014P6.Witness.g1
Proof uses: And.left, Classical.choose, And, Ne, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Witness.r, OfNat.ofNat, Imo2014P6.Witness.exists_g1, Classical.choose_spec
6 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.g1_ne line 810 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Ne, Imo2014P6.Witness.g1
Proof uses: And.left, Classical.choose, And, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Witness.r, OfNat.ofNat, Imo2014P6.Witness.exists_g1, And.right, Classical.choose_spec
6 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.g1_val_r line 813 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Witness.g1, Imo2014P6.Witness.r, OfNat.ofNat
Proof uses: And.right, Ne, Classical.choose, And, Imo2014P6.Witness.exists_g1, Classical.choose_spec
8 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.r_mem_g1 line 817 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Prod, Real, Set, Inter.inter, closure, Imo2014P6.Cell, Imo2014P6.Witness.σ, Imo2014P6.Line.set, Imo2014P6.Witness.g1, Imo2014P6.Witness.r
Proof uses: And.intro, And.left, Imo2014P6.Witness.r_mem_closure, Imo2014P6.Witness.g1_val_r
15 instances, coercions and auxiliary constants left out.
def Imo2014P6.Witness.g1ctx The edge context of the blue line g₁ line 822 source
Source documentation
The edge context of the blue line g₁.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Imo2014P6.EdgeCtx
Proof uses: Imo2014P6.EdgeCtx.mk, Imo2014P6.Witness.σ, Imo2014P6.Witness.g1, Imo2014P6.Witness.hne, Imo2014P6.Witness.hbdd, Imo2014P6.Witness.g1_mem
5 instances, coercions and auxiliary constants left out.
```
noncomputable def g1ctx (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) : EdgeCtx L :=
…
```
Mentions: Imo2014P6.GeneralPosition, Imo2014P6.EdgeCtx
lemma Imo2014P6.Witness.ectx_σ line 826 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Eq, Bool, Imo2014P6.EdgeCtx.σ, Imo2014P6.Witness.ectx, Imo2014P6.Witness.σ
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.ectx_ℓ line 829 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Eq, Imo2014P6.EdgeCtx.ℓ, Imo2014P6.Witness.ectx
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.g1ctx_σ line 832 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Eq, Bool, Imo2014P6.EdgeCtx.σ, Imo2014P6.Witness.g1ctx, Imo2014P6.Witness.σ
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.g1ctx_ℓ line 835 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Eq, Imo2014P6.EdgeCtx.ℓ, Imo2014P6.Witness.g1ctx, Imo2014P6.Witness.g1
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.g1_blue line 838 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Imo2014P6.Witness.g1
Proof uses: Insert.insert, Imo2014P6.Witness.hbd, Imo2014P6.Witness.g1_mem, Exists.intro, Prod, Real, Set, Inter.inter, closure, Imo2014P6.Cell, Imo2014P6.Witness.σ, Imo2014P6.Line.set, Imo2014P6.Witness.r, Imo2014P6.Witness.r_mem_g1, Eq, Or, Iff.mp, Finset.mem_insert, absurd, Imo2014P6.Witness.g1_ne
13 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Witness.exists_s_r The parameter of r in the parametrization of g₁ line 845 source
Source documentation
The parameter of r in the parametrization of g₁.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Exists, Real, And, Eq, Prod, Imo2014P6.Line.param, Imo2014P6.Witness.g1, Imo2014P6.Witness.r, Set, Set.Icc, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.Witness.g1ctx, Imo2014P6.EdgeCtx.Tmax
Proof uses: Imo2014P6.Line.exists_param_of_mem_set, Imo2014P6.Witness.g1_val_r, Exists.intro, And.intro, closure, Imo2014P6.Cell, Imo2014P6.Witness.σ, And.left, Imo2014P6.Line.set, Imo2014P6.Witness.r_mem_closure, Eq.mpr, Set.ofPred, LE.le, OfNat.ofNat, HMul.hMul, Imo2014P6.sgn, Imo2014P6.EdgeCtx.σ, Imo2014P6.Line.val, Imo2014P6.EdgeCtx.ℓ, id and 7 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma exists_s_r (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) :
    ∃ s : ℝ, (W.g1 hGP hℓL).param s = W.r hGP hℓL ∧
      s ∈ Set.Icc (W.g1ctx hGP hℓL).Tmin (W.g1ctx hGP hℓL).Tmax := by
…
```
Mentions: Imo2014P6.GeneralPosition
lemma Imo2014P6.Witness.r_eq_g1_param The consistency lemma: r is the clockwise-first endpoint of the g₁-edge, i.e. b and r are two clockwise-consecutive vertices of the region line 858 source
Source documentation
The consistency lemma: r is the clockwise-first endpoint of the g₁-edge, i.e. b and r are two clockwise-consecutive vertices of the region.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Eq, Prod, Real, Imo2014P6.Witness.r, Imo2014P6.Line.param, Imo2014P6.Witness.g1, ite, Bool, Imo2014P6.Witness.σ, Bool.true, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.Witness.g1ctx, Imo2014P6.EdgeCtx.Tmax
Proof uses: And, Set, Set.Icc, Exists, Imo2014P6.Witness.exists_s_r, Ne, Imo2014P6.Line.det, OfNat.ofNat, Imo2014P6.GP.det_ne, Imo2014P6.Witness.g1_mem, Ne.symm, Imo2014P6.Witness.g1_ne, Imo2014P6.Line.val, HMul.hMul, HSub.hSub, Imo2014P6.Witness.rT, HAdd.hAdd, Imo2014P6.Line.base, Imo2014P6.Line.val_param_eq, Imo2014P6.Witness.g1_val_r and 123 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 132 steps
Open to load the checked before-and-after goal states.
```
lemma r_eq_g1_param (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) :
    W.r hGP hℓL = (W.g1 hGP hℓL).param
      (if W.σ (W.g1 hGP hℓL) then (W.g1ctx hGP hℓL).Tmin else (W.g1ctx hGP hℓL).Tmax) := by
…
```
Mentions: Imo2014P6.GeneralPosition
def Imo2014P6.Witness.bT The parameter of the blue point b in the parametrization of g₁: the other endpoint of the g₁-edge line 997 source
Source documentation
The parameter of the blue point b in the parametrization of g₁: the other endpoint of the g₁-edge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Real
Proof uses: ite, Eq, Bool, Imo2014P6.Witness.σ, Imo2014P6.Witness.g1, Bool.true, Imo2014P6.EdgeCtx.Tmax, Imo2014P6.Witness.g1ctx, Imo2014P6.EdgeCtx.Tmin
5 instances, coercions and auxiliary constants left out.
```
noncomputable def bT (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) : ℝ :=
…
```
Mentions: Imo2014P6.GeneralPosition
def Imo2014P6.Witness.b The blue point associated to ℓ: the next vertex of the region after r in clockwise order line 1002 source
Source documentation
The blue point associated to ℓ: the next vertex of the region after r in clockwise order.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Prod, Real
Proof uses: Imo2014P6.Line.param, Imo2014P6.Witness.g1, Imo2014P6.Witness.bT
4 instances, coercions and auxiliary constants left out.
```
noncomputable def b (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) : ℝ × ℝ :=
…
```
Mentions: Imo2014P6.GeneralPosition
lemma Imo2014P6.Witness.bT_mem_Icc line 1005 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Real, Set, Set.Icc, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.Witness.g1ctx, Imo2014P6.EdgeCtx.Tmax, Imo2014P6.Witness.bT
Proof uses: Eq.mpr, ite, Eq, Bool, Imo2014P6.Witness.σ, Imo2014P6.Witness.g1, Bool.true, id, congrArg, Imo2014P6.Witness.bT.eq_1, Decidable, Not, ite_eq_right, Iff.mpr, LE.le, Set.left_mem_Icc, Imo2014P6.EdgeCtx.Tmin_le_Tmax, ite_eq_left, Set.right_mem_Icc
11 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Witness.b_mem_closure line 1012 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Prod, Real, Set, Inter.inter, closure, Imo2014P6.Cell, Imo2014P6.Witness.σ, Imo2014P6.Line.set, Imo2014P6.Witness.g1, Imo2014P6.Witness.b
Proof uses: Imo2014P6.EdgeCtx.param_mem_closure_inter, Imo2014P6.Witness.g1ctx, Imo2014P6.Witness.bT, Imo2014P6.Witness.bT_mem_Icc
10 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.b_ne_r line 1016 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Ne, Prod, Real, Imo2014P6.Witness.b, Imo2014P6.Witness.r
Proof uses: Eq.mpr, Imo2014P6.Line.param, Imo2014P6.Witness.g1, Imo2014P6.Witness.bT, id, Eq, congrArg, Imo2014P6.Witness.b.eq_1, ite, Bool, Imo2014P6.Witness.σ, Bool.true, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.Witness.g1ctx, Imo2014P6.EdgeCtx.Tmax, Imo2014P6.Witness.r_eq_g1_param, LT.lt, Imo2014P6.EdgeCtx.Tmin_lt_Tmax, False, Bool.false and 59 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Witness.exists_g2 The other line through b exists line 1035 source
Source documentation
The other line through b exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Exists, And, Ne, Imo2014P6.Witness.g1, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Witness.b, OfNat.ofNat
Proof uses: Eq.mpr, Imo2014P6.Line.param, Imo2014P6.Witness.bT, id, congrArg, Prod, Imo2014P6.Witness.b.eq_1, ite, Bool, Imo2014P6.Witness.σ, Bool.true, Imo2014P6.EdgeCtx.Tmax, Imo2014P6.Witness.g1ctx, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.Witness.bT.eq_1, Decidable, Not, funext, congrFun', ite_eq_right and 3 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma exists_g2 (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) :
    ∃ g ∈ L, g ≠ W.g1 hGP hℓL ∧ g.val (W.b hGP hℓL) = 0 := by
…
```
Mentions: Imo2014P6.GeneralPosition
def Imo2014P6.Witness.g2 The other line through b (another blue line) line 1043 source
Source documentation
The other line through b (another blue line).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem
Proof uses: Classical.choose, And, Ne, Imo2014P6.Witness.g1, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Witness.b, OfNat.ofNat, Imo2014P6.Witness.exists_g2
6 instances, coercions and auxiliary constants left out.
```
noncomputable def g2 (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) : Line :=
…
```
Mentions: Imo2014P6.GeneralPosition, Imo2014P6.Line
lemma Imo2014P6.Witness.g2_mem line 1046 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Imo2014P6.Witness.g2
Proof uses: And.left, Classical.choose, And, Ne, Imo2014P6.Witness.g1, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Witness.b, OfNat.ofNat, Imo2014P6.Witness.exists_g2, Classical.choose_spec
6 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.g2_ne_g1 line 1049 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Ne, Imo2014P6.Witness.g2, Imo2014P6.Witness.g1
Proof uses: And.left, Classical.choose, And, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Witness.b, OfNat.ofNat, Imo2014P6.Witness.exists_g2, And.right, Classical.choose_spec
6 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.g2_val_b line 1052 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Witness.g2, Imo2014P6.Witness.b, OfNat.ofNat
Proof uses: And.right, Ne, Classical.choose, And, Imo2014P6.Witness.g1, Imo2014P6.Witness.exists_g2, Classical.choose_spec
8 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.g2_ne_red line 1056 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Ne, Imo2014P6.Witness.g2
Proof uses: Eq, Real, Imo2014P6.Line.det, Imo2014P6.Witness.g1, OfNat.ofNat, Imo2014P6.GP.det_ne, Imo2014P6.Witness.g1_mem, Ne.symm, Imo2014P6.Witness.g1_ne, Imo2014P6.Line.val, Imo2014P6.Witness.b, Imo2014P6.Witness.g2_val_b, Eq.mp, congrArg, And.right, Prod, Set, closure, Imo2014P6.Cell, Imo2014P6.Witness.σ and 11 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Witness.b_mem_g2 line 1071 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Prod, Real, Set, Inter.inter, closure, Imo2014P6.Cell, Imo2014P6.Witness.σ, Imo2014P6.Line.set, Imo2014P6.Witness.g2, Imo2014P6.Witness.b
Proof uses: And.intro, And.left, Imo2014P6.Witness.g1, Imo2014P6.Witness.b_mem_closure, Imo2014P6.Witness.g2_val_b
15 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.g2_blue line 1075 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Imo2014P6.Witness.g2
Proof uses: Insert.insert, Imo2014P6.Witness.hbd, Imo2014P6.Witness.g2_mem, Exists.intro, Prod, Real, Set, Inter.inter, closure, Imo2014P6.Cell, Imo2014P6.Witness.σ, Imo2014P6.Line.set, Imo2014P6.Witness.b, Imo2014P6.Witness.b_mem_g2, Eq, Or, Iff.mp, Finset.mem_insert, absurd, Imo2014P6.Witness.g2_ne_red
13 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Witness.eq_of_val_b_eq_zero The two blue lines through b are exactly g₁ and g₂ line 1082 source
Source documentation
The two blue lines through b are exactly g₁ and g₂.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Eq, Real, Imo2014P6.Line.val, Imo2014P6.Witness.b, OfNat.ofNat, Or, Imo2014P6.Witness.g1, Imo2014P6.Witness.g2
Proof uses: Imo2014P6.GP.eq_of_val_eq_zero, Imo2014P6.Witness.g1_mem, Imo2014P6.Witness.g2_mem, Ne.symm, Imo2014P6.Witness.g2_ne_g1, And.right, Prod, Set, closure, Imo2014P6.Cell, Imo2014P6.Witness.σ, Imo2014P6.Line.set, Imo2014P6.Witness.b_mem_closure, Imo2014P6.Witness.g2_val_b
13 instances, coercions and auxiliary constants left out.
```
lemma eq_of_val_b_eq_zero (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) {m : Line}
    (hm : m ∈ L) (hmv : m.val (W.b hGP hℓL) = 0) :
    m = W.g1 hGP hℓL ∨ m = W.g2 hGP hℓL :=
…
```
Mentions: Imo2014P6.GeneralPosition, Imo2014P6.Line
def Imo2014P6.Witness.g2ctx The edge context of the blue line g₂ line 1089 source
Source documentation
The edge context of the blue line g₂.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Imo2014P6.EdgeCtx
Proof uses: Imo2014P6.EdgeCtx.mk, Imo2014P6.Witness.σ, Imo2014P6.Witness.g2, Imo2014P6.Witness.hne, Imo2014P6.Witness.hbdd, Imo2014P6.Witness.g2_mem
5 instances, coercions and auxiliary constants left out.
```
noncomputable def g2ctx (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) : EdgeCtx L :=
…
```
Mentions: Imo2014P6.GeneralPosition, Imo2014P6.EdgeCtx
lemma Imo2014P6.Witness.g2ctx_σ line 1093 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Eq, Bool, Imo2014P6.EdgeCtx.σ, Imo2014P6.Witness.g2ctx, Imo2014P6.Witness.σ
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.g2ctx_ℓ line 1096 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Eq, Imo2014P6.EdgeCtx.ℓ, Imo2014P6.Witness.g2ctx, Imo2014P6.Witness.g2
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
def Imo2014P6.Witness.s_r The parameter of r in the parametrization of g₁ line 1100 source
Source documentation
The parameter of r in the parametrization of g₁.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Real
Proof uses: ite, Eq, Bool, Imo2014P6.Witness.σ, Imo2014P6.Witness.g1, Bool.true, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.Witness.g1ctx, Imo2014P6.EdgeCtx.Tmax
5 instances, coercions and auxiliary constants left out.
```
noncomputable def s_r (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) : ℝ :=
…
```
Mentions: Imo2014P6.GeneralPosition
def Imo2014P6.Witness.s_b The parameter of b in the parametrization of g₁ line 1104 source
Source documentation
The parameter of b in the parametrization of g₁.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Real
Proof uses: ite, Eq, Bool, Imo2014P6.Witness.σ, Imo2014P6.Witness.g1, Bool.true, Imo2014P6.EdgeCtx.Tmax, Imo2014P6.Witness.g1ctx, Imo2014P6.EdgeCtx.Tmin
5 instances, coercions and auxiliary constants left out.
```
noncomputable def s_b (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) : ℝ :=
…
```
Mentions: Imo2014P6.GeneralPosition
lemma Imo2014P6.Witness.r_eq_param_s_r line 1107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Eq, Prod, Real, Imo2014P6.Witness.r, Imo2014P6.Line.param, Imo2014P6.Witness.g1, Imo2014P6.Witness.s_r
Proof uses: Imo2014P6.Witness.r_eq_g1_param
4 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.b_eq_param_s_b line 1111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Eq, Prod, Real, Imo2014P6.Witness.b, Imo2014P6.Line.param, Imo2014P6.Witness.g1, Imo2014P6.Witness.s_b
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.s_bT line 1114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Eq, Real, Imo2014P6.Witness.s_b, Imo2014P6.Witness.bT
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma Imo2014P6.Witness.s_r_ne_s_b line 1117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Ne, Real, Imo2014P6.Witness.s_r, Imo2014P6.Witness.s_b
Proof uses: LT.lt, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.Witness.g1ctx, Imo2014P6.EdgeCtx.Tmax, Imo2014P6.EdgeCtx.Tmin_lt_Tmax, Bool, Eq, Imo2014P6.Witness.σ, Imo2014P6.Witness.g1, Bool.false, Eq.mpr, ite, Bool.true, id, congrArg, Imo2014P6.Witness.s_r.eq_1, Imo2014P6.Witness.s_b.eq_1, Not, congr, ite_eq_right_of_eq_false and 55 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2014P6.Witness.mem_Ioo_of_between A parameter strictly between s_r and s_b lies in the interior of the g₁-edge line 1124 source
Source documentation
A parameter strictly between s_r and s_b lies in the interior of the g₁-edge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Real, LT.lt, HMul.hMul, HSub.hSub, Imo2014P6.Witness.s_r, Imo2014P6.Witness.s_b, OfNat.ofNat, Set, Set.Ioo, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.Witness.g1ctx, Imo2014P6.EdgeCtx.Tmax
Proof uses: And, Or, Iff.mp, mul_neg_iff, HAdd.hAdd, Bool, Eq, Imo2014P6.Witness.σ, Imo2014P6.Witness.g1, Bool.false, Eq.mpr, id, And.intro, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 50 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma mem_Ioo_of_between (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) {t : ℝ}
    (ht : (t - W.s_r hGP hℓL) * (t - W.s_b hGP hℓL) < 0) :
    t ∈ Set.Ioo (W.g1ctx hGP hℓL).Tmin (W.g1ctx hGP hℓL).Tmax := by
…
```
Mentions: Imo2014P6.GeneralPosition
lemma Imo2014P6.Witness.g1_edge_uncut The g₁-edge contains no crossing of another line in its interior line 1136 source
Source documentation
The g₁-edge contains no crossing of another line in its interior.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Ne, Imo2014P6.Witness.g1, Real, Set, Set.Ioo, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.Witness.g1ctx, Imo2014P6.EdgeCtx.Tmax, Imo2014P6.Line.val, Imo2014P6.Line.param, OfNat.ofNat
Proof uses: Imo2014P6.EdgeCtx.val_ne_zero_of_mem_Ioo
10 instances, coercions and auxiliary constants left out.
```
lemma g1_edge_uncut (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) {m : Line} (hm : m ∈ L)
    (hm1 : m ≠ W.g1 hGP hℓL) {t : ℝ}
    (ht : t ∈ Set.Ioo (W.g1ctx hGP hℓL).Tmin (W.g1ctx hGP hℓL).Tmax) :
    m.val ((W.g1 hGP hℓL).param t) ≠ 0 :=
…
```
Mentions: Imo2014P6.GeneralPosition, Imo2014P6.Line
lemma Imo2014P6.Witness.g2_edge_uncut The g₂-edge contains no crossing of another line in its interior line 1143 source
Source documentation
The g₂-edge contains no crossing of another line in its interior.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Membership.mem, Ne, Imo2014P6.Witness.g2, Real, Set, Set.Ioo, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.Witness.g2ctx, Imo2014P6.EdgeCtx.Tmax, Imo2014P6.Line.val, Imo2014P6.Line.param, OfNat.ofNat
Proof uses: Imo2014P6.EdgeCtx.val_ne_zero_of_mem_Ioo
10 instances, coercions and auxiliary constants left out.
```
lemma g2_edge_uncut (hGP : GeneralPosition L) (hℓL : ℓ ∈ L) {m : Line} (hm : m ∈ L)
    (hm2 : m ≠ W.g2 hGP hℓL) {t : ℝ}
    (ht : t ∈ Set.Ioo (W.g2ctx hGP hℓL).Tmin (W.g2ctx hGP hℓL).Tmax) :
    m.val ((W.g2 hGP hℓL).param t) ≠ 0 :=
…
```
Mentions: Imo2014P6.GeneralPosition, Imo2014P6.Line
lemma Imo2014P6.opp_sides Documented declaration: opp_sides line 1154 source
Source documentation
Two distinct red points associated to the same blue point along the same blue line must lie on opposite sides of the blue point: on the same side, the nearer region's side would be crossed by the farther region's red line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.GeneralPosition, Imo2014P6.Witness, Membership.mem, Not, Eq, Imo2014P6.Witness.g1, Prod, Real, Imo2014P6.Witness.b, Ne, Imo2014P6.Witness.r, LT.lt, HMul.hMul, HSub.hSub, Imo2014P6.Witness.s_r, Imo2014P6.Witness.s_b, OfNat.ofNat
Proof uses: Imo2014P6.Line.param, Eq.mpr, id, congrArg, Eq.refl, Imo2014P6.Witness.b_eq_param_s_b, Trans.trans, Eq.symm, Imo2014P6.Line.param_injective, Imo2014P6.Witness.s_r_ne_s_b, Imo2014P6.Witness.r_eq_param_s_r, Decidable.byContradiction, mul_ne_zero, Iff.mpr, sub_ne_zero, lt_of_le_of_ne', le_of_not_gt, Eq.mp, Imo2014P6.Witness.g1_blue, Imo2014P6.Line.val and 74 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 66 steps
Open to load the checked before-and-after goal states.
```
lemma opp_sides {L B : Finset Line} (hGP : GeneralPosition L)
    {ℓi ℓj : Line} (Wi : Witness L B ℓi) (Wj : Witness L B ℓj)
    (hiL : ℓi ∈ L) (hjL : ℓj ∈ L) (hiB : ℓi ∉ B) (hjB : ℓj ∉ B)
    (hgq : Wi.g1 hGP hiL = Wj.g1 hGP hjL)
    (hq : Wi.b hGP hiL = Wj.b hGP hjL)
    (hrr : Wi.r hGP hiL ≠ Wj.r hGP hjL) :
    (Wi.s_r hGP hiL - Wi.s_b hGP hiL) * (Wj.s_r hGP hjL - Wi.s_b hGP hiL) < 0 := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.GeneralPosition, Imo2014P6.Witness
lemma Imo2014P6.turn_at_blue_pt The key turning argument: the region of the third red line must turn at q towards one of the two red points, forcing three concurrent lines line 1234 source
Source documentation
The key turning argument: the region of the third red line must turn at q towards one of the two red points, forcing three concurrent lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.GeneralPosition, Imo2014P6.Witness, Membership.mem, Not, Ne, Eq, Imo2014P6.Witness.g1, Prod, Real, Imo2014P6.Witness.b, LT.lt, HMul.hMul, HSub.hSub, Imo2014P6.Witness.s_r, Imo2014P6.Witness.s_b, OfNat.ofNat, False
Proof uses: rfl, Imo2014P6.Witness.g1_mem, Imo2014P6.Witness.g1_blue, Imo2014P6.Line.val, And.right, Set, closure, Imo2014P6.Cell, Imo2014P6.Witness.σ, Imo2014P6.Line.set, Imo2014P6.Witness.b_mem_closure, Eq.rec, Eq.mp, congrArg, Imo2014P6.Witness.g2, Imo2014P6.Witness.g2_val_b, Eq.mpr, id, Or, Imo2014P6.Witness.eq_of_val_b_eq_zero and 150 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 243 steps (first 200 of 243)
Open to load the checked before-and-after goal states.
```
lemma turn_at_blue_pt {L B : Finset Line} (hGP : GeneralPosition L)
    {ℓₖ ℓi ℓj : Line} (W : Witness L B ℓₖ) (Wi : Witness L B ℓi) (Wj : Witness L B ℓj)
    (hkL : ℓₖ ∈ L) (hiL : ℓi ∈ L) (hjL : ℓj ∈ L)
    (hkB : ℓₖ ∉ B) (hiB : ℓi ∉ B) (hjB : ℓj ∉ B)
    (hki : ℓₖ ≠ ℓi) (hkj : ℓₖ ≠ ℓj)
    (hgq : Wi.g1 hGP hiL = Wj.g1 hGP hjL)
    (hq : Wi.b hGP hiL = Wj.b hGP hjL)
    (hqW : W.b hGP hkL = Wi.b hGP hiL)
    (hgW : Wi.g1 hGP hiL ≠ W.g1 hGP hkL)
    (hopp : (Wi.s_r hGP hiL - Wi.s_b hGP hiL) * (Wj.s_r hGP hjL - Wi.s_b hGP hiL) < 0) :
    False := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.GeneralPosition, Imo2014P6.Witness
lemma Imo2014P6.Line.eq_of_two_mem Two distinct points determine a line (in general position) line 1472 source
Source documentation
Two distinct points determine a line (in general position).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.GeneralPosition, Membership.mem, Prod, Real, Ne, Eq, Imo2014P6.Line.val, OfNat.ofNat
Proof uses: Decidable.byContradiction, Not, Imo2014P6.Line.det, Imo2014P6.GP.det_ne, Imo2014P6.Line.interPt, Imo2014P6.Line.eq_interPt, Eq.trans, Eq.symm
9 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma Line.eq_of_two_mem {L : Finset Line} (hGP : GeneralPosition L) {g g' : Line}
    (hg : g ∈ L) (hg' : g' ∈ L) {p q : ℝ × ℝ} (hpq : p ≠ q)
    (hgp : g.val p = 0) (hgq : g.val q = 0) (hg'p : g'.val p = 0) (hg'q : g'.val q = 0) :
    g = g' := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.GeneralPosition
lemma Imo2014P6.Line.interPt_comm line 1482 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2014P6.Line, Ne, Real, Imo2014P6.Line.det, OfNat.ofNat, Eq, Prod, Imo2014P6.Line.interPt
Proof uses: Eq.mpr, Neg.neg, id, congrArg, Imo2014P6.Line.det_comm, Iff.mpr, neg_ne_zero, Eq.symm, Imo2014P6.Line.eq_interPt, Imo2014P6.Line.val_interPt_right, Imo2014P6.Line.val_interPt_left
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Imo2014P6.assocB The association map from red lines to blue points, for a choice of witnesses line 1489 source
Source documentation
The association map from red lines to blue points, for a choice of witnesses.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Membership.mem, SDiff.sdiff, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Prod, Real
Proof uses: dite, Imo2014P6.Witness.b, Not, Prod.mk, OfNat.ofNat
12 instances, coercions and auxiliary constants left out.
```
noncomputable def assocB (L B : Finset Line) (W : ∀ m ∈ L \ B, Witness L B m)
    (hGP : GeneralPosition L) (ℓ : Line) : ℝ × ℝ :=
…
```
Mentions: Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition
lemma Imo2014P6.Witness.s_b_eq_s_b On the same blue line through the same blue point, the parameter of b is the same for two witnesses line 1497 source
Source documentation
On the same blue line through the same blue point, the parameter of b is the same for two witnesses.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.GeneralPosition, Imo2014P6.Witness, Membership.mem, Eq, Imo2014P6.Witness.g1, Prod, Real, Imo2014P6.Witness.b, Imo2014P6.Witness.s_b
Proof uses: Imo2014P6.Line.param, Eq.mpr, id, congrArg, Eq.refl, Imo2014P6.Witness.b_eq_param_s_b, Trans.trans, Eq.symm, Imo2014P6.Line.param_injective
5 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma s_b_eq_s_b {L B : Finset Line} (hGP : GeneralPosition L)
    {ℓi ℓj : Line} (Wi : Witness L B ℓi) (Wj : Witness L B ℓj)
    (hiL : ℓi ∈ L) (hjL : ℓj ∈ L)
    (hgq : Wi.g1 hGP hiL = Wj.g1 hGP hjL)
    (hq : Wi.b hGP hiL = Wj.b hGP hjL) :
    Wi.s_b hGP hiL = Wj.s_b hGP hjL := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.GeneralPosition, Imo2014P6.Witness
lemma Imo2014P6.fiber_card_le_two The key counting lemma: at most two red lines are associated to the same blue point line 1519 source
Source documentation
The key counting lemma: at most two red lines are associated to the same blue point.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Membership.mem, SDiff.sdiff, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Prod, Real, LE.le, Nat, Finset.card, Finset.filter, Eq, Imo2014P6.assocB, OfNat.ofNat
Proof uses: Decidable.byContradiction, Not, LT.lt, Nat.lt_of_not_le, rfl, Finset.Nonempty, False, Iff.mp, Finset.card_pos, Eq.mp, congrArg, Finset.erase, Eq.mpr, HSub.hSub, id, Finset.card_erase_of_mem, And, Exists, Ne, Finset.one_lt_card and 116 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 118 steps
Open to load the checked before-and-after goal states.
```
lemma fiber_card_le_two (L B : Finset Line) (W : ∀ m ∈ L \ B, Witness L B m)
    (hGP : GeneralPosition L) (q : ℝ × ℝ) :
    ((L \ B).filter fun ℓ => assocB L B W hGP ℓ = q).card ≤ 2 := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Imo2014P6.assocB
lemma Imo2014P6.exists_boundary_line Every bounded nonempty cell has a boundary line: follow a ray from an interior point; since the cell is bounded, some constraint must stop the ray line 1668 source
Source documentation
Every bounded nonempty cell has a boundary line: follow a ray from an interior point; since the cell is bounded, some constraint must stop the ray.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Bool, Set.Nonempty, Prod, Real, Imo2014P6.Cell, Bornology.IsBounded, Exists, And, Membership.mem, Inter.inter, Set, closure, Imo2014P6.Line.set
Proof uses: LE.le, Metric.closedBall, Bornology.IsBounded.subset_closedBall, Bornology.IsBounded.closure, Eq, Imo2014P6.Line.val, HAdd.hAdd, HSMul.hSMul, Prod.mk, OfNat.ofNat, HMul.hMul, Imo2014P6.Line.a, Eq.mpr, Prod.fst, Imo2014P6.Line.b, Prod.snd, Imo2014P6.Line.c, id, congrFun', congrArg and 168 more
225 instances, coercions and auxiliary constants left out.

Tactic trace: 87 steps
Open to load the checked before-and-after goal states.
```
lemma exists_boundary_line {L : Finset Line} {σ : Line → Bool} (hne : (Cell L σ).Nonempty)
    (hbdd : Bornology.IsBounded (Cell L σ)) :
    ∃ m ∈ L, (closure (Cell L σ) ∩ m.set).Nonempty := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.Cell
lemma Imo2014P6.validBlue_empty The empty blue set is valid line 1750 source
Source documentation
The empty blue set is valid.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.ValidBlue, EmptyCollection.emptyCollection
Proof uses: Bool, Set.Nonempty, Prod, Real, Imo2014P6.Cell, Bornology.IsBounded, And, Membership.mem, Inter.inter, Set, closure, Imo2014P6.Line.set, Exists, Not, Imo2014P6.exists_boundary_line, Exists.intro, And.intro, of_eq_true, Eq.trans, False and 3 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma validBlue_empty (L : Finset Line) : ValidBlue L ∅ := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.ValidBlue
lemma Imo2014P6.exists_maximal_valid A maximal valid blue set exists line 1756 source
Source documentation
A maximal valid blue set exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Exists, And, LE.le, Imo2014P6.ValidBlue, Membership.mem, Not, Insert.insert
Proof uses: Finset.Nonempty, Finset.filter, Classical.propDecidable, Finset.powerset, Exists.intro, EmptyCollection.emptyCollection, Iff.mpr, Finset.mem_filter, And.intro, Finset.empty_mem_powerset, Imo2014P6.validBlue_empty, Nat, Finset.image, Finset.card, Finset.image_nonempty, Finset.max', Eq, rfl, Finset.max'_mem, Eq.mp and 16 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma exists_maximal_valid (L : Finset Line) :
    ∃ B ⊆ L, ValidBlue L B ∧ ∀ m ∈ L, m ∉ B → ¬ ValidBlue L (insert m B) := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.ValidBlue
lemma Imo2014P6.exists_witness Every red line has a witness region line 1778 source
Source documentation
Every red line has a witness region.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.ValidBlue, Membership.mem, Not, Insert.insert, Nonempty, Imo2014P6.Witness
Proof uses: Exists, Bool, And, Set.Nonempty, Prod, Real, Imo2014P6.Cell, Bornology.IsBounded, Inter.inter, Set, closure, Imo2014P6.Line.set, Classical.byContradiction, Exists.intro, And.intro, Decidable.byContradiction, Eq, Or, Iff.mp, Finset.mem_insert and 7 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma exists_witness (L : Finset Line) {B : Finset Line} (hBV : ValidBlue L B)
    (hmax : ∀ m ∈ L, m ∉ B → ¬ ValidBlue L (insert m B))
    {ℓ : Line} (hℓL : ℓ ∈ L) (hℓB : ℓ ∉ B) : Nonempty (Witness L B ℓ) := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.ValidBlue, Imo2014P6.Witness
def Imo2014P6.redWitness The choice of a witness region for every red line line 1804 source
Source documentation
The choice of a witness region for every red line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.ValidBlue, Membership.mem, Not, Insert.insert, SDiff.sdiff, Imo2014P6.Witness
Proof uses: Classical.choice
11 instances, coercions and auxiliary constants left out.
```
noncomputable def redWitness (L : Finset Line) {B : Finset Line} (hBV : ValidBlue L B)
    (hmax : ∀ m ∈ L, m ∉ B → ¬ ValidBlue L (insert m B))
    {m : Line} (hm : m ∈ L \ B) : Witness L B m :=
…
```
Mentions: Imo2014P6.Line, Imo2014P6.ValidBlue, Imo2014P6.Witness
def Imo2014P6.bluePts The blue points: the intersection points of pairs of distinct blue lines line 1810 source
Source documentation
The blue points: the intersection points of pairs of distinct blue lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Prod, Real
Proof uses: Finset.image, Imo2014P6.Line.interPt, Prod.fst, Prod.snd, Finset.offDiag
2 instances, coercions and auxiliary constants left out.
```
noncomputable def bluePts (B : Finset Line) : Finset (ℝ × ℝ) :=
…
```
Mentions: Imo2014P6.Line
lemma Imo2014P6.two_mul_card_bluePts Each blue point has at least two preimages among the ordered pairs of blue lines line 1814 source
Source documentation
Each blue point has at least two preimages among the ordered pairs of blue lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.GeneralPosition, LE.le, Nat, HMul.hMul, OfNat.ofNat, Finset.card, Prod, Real, Imo2014P6.bluePts, HSub.hSub
Proof uses: Eq.mpr, Finset.offDiag, id, Eq, congrArg, Eq.symm, Finset.offDiag_card, Finset.image, Imo2014P6.Line.interPt, Prod.fst, Prod.snd, Imo2014P6.bluePts.eq_1, Finset.mul_card_image_le_card, Membership.mem, And, Exists, Finset.filter, Eq.mp, Ne, propext and 16 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma two_mul_card_bluePts {L : Finset Line} {B : Finset Line}
    (hGP : GeneralPosition L) (hBL : B ⊆ L) :
    2 * (bluePts B).card ≤ B.card * B.card - B.card := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.GeneralPosition, Imo2014P6.bluePts
lemma Imo2014P6.assocB_mem_bluePts The association map sends red lines into the blue points line 1844 source
Source documentation
The association map sends red lines into the blue points.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, LE.le, Membership.mem, SDiff.sdiff, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Prod, Real, Imo2014P6.bluePts, Imo2014P6.assocB
Proof uses: Eq.mpr, dite, Imo2014P6.Witness.b, Not, Prod.mk, OfNat.ofNat, id, Eq, congrArg, Imo2014P6.assocB.eq_1, dite_eq_left, And.left, Iff.mp, And, Finset.mem_sdiff, rfl, Imo2014P6.Line.val, Imo2014P6.Witness.g1, And.right, Set and 28 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma assocB_mem_bluePts (L : Finset Line) {B : Finset Line} (hBL : B ⊆ L)
    (W : ∀ m ∈ L \ B, Witness L B m)
    (hGP : GeneralPosition L) {ℓ : Line} (hℓ : ℓ ∈ L \ B) :
    assocB L B W hGP ℓ ∈ bluePts B := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Imo2014P6.assocB, Imo2014P6.bluePts
lemma Imo2014P6.card_red_le The number of red lines is at most twice the number of blue points line 1864 source
Source documentation
The number of red lines is at most twice the number of blue points.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Membership.mem, SDiff.sdiff, Imo2014P6.Witness, Imo2014P6.GeneralPosition, LE.le, Nat, Finset.card, HMul.hMul, OfNat.ofNat, Prod, Real, Finset.image, Imo2014P6.assocB
Proof uses: Finset.card_le_mul_card_image, Imo2014P6.fiber_card_le_two
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma card_red_le (L B : Finset Line) (W : ∀ m ∈ L \ B, Witness L B m)
    (hGP : GeneralPosition L) :
    (L \ B).card ≤ 2 * ((L \ B).image (assocB L B W hGP)).card := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.Witness, Imo2014P6.GeneralPosition, Imo2014P6.assocB
lemma Imo2014P6.main_counting The grand count: n ≤ k² line 1871 source
Source documentation
The grand count: n ≤ k².

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.GeneralPosition, LE.le, Membership.mem, SDiff.sdiff, Imo2014P6.Witness, Nat, Finset.card, HPow.hPow, OfNat.ofNat
Proof uses: HMul.hMul, Prod, Real, Finset.image, Imo2014P6.assocB, Imo2014P6.card_red_le, Imo2014P6.bluePts, Finset.card_le_card, And, Eq, Exists, Eq.mp, Imo2014P6.assocB_mem_bluePts, HSub.hSub, Imo2014P6.two_mul_card_bluePts, Finset.card_sdiff_of_subset, HAdd.hAdd, Nat.sub_add_cancel, Nat.le_mul_self, Eq.symm and 1 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma main_counting {L : Finset Line} {B : Finset Line} (hGP : GeneralPosition L) (hBL : B ⊆ L)
    (W : ∀ m ∈ L \ B, Witness L B m) : L.card ≤ B.card ^ 2 := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.GeneralPosition, Imo2014P6.Witness
lemma Imo2014P6.not_frontier_subset_of_validBlue If no finite region has a completely blue boundary in the working sense, then no finite region has a completely blue boundary in the geometric sense line 1889 source
Source documentation
If no finite region has a completely blue boundary in the working sense, then no finite region has a completely blue boundary in the geometric sense.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.GeneralPosition, LE.le, Imo2014P6.ValidBlue, Bool, Set.Nonempty, Prod, Real, Imo2014P6.Cell, Bornology.IsBounded, Not, Set, frontier, Set.iUnion, Membership.mem, Imo2014P6.Line.set
Proof uses: And, Inter.inter, closure, Exists, Imo2014P6.EdgeCtx, Imo2014P6.EdgeCtx.mk, Eq, rfl, LT.lt, Imo2014P6.EdgeCtx.Tmin, Imo2014P6.EdgeCtx.Tmax, Imo2014P6.EdgeCtx.Tmin_lt_Tmax, Set.image, Imo2014P6.Line.param, Imo2014P6.EdgeCtx.ℓ, Set.Icc, Set.Infinite, Set.Infinite.image, Function.Injective.injOn, Imo2014P6.Line.param_injective and 42 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
```
lemma not_frontier_subset_of_validBlue {L : Finset Line} {B : Finset Line}
    (hGP : GeneralPosition L) (hBL : B ⊆ L)
    (hBV : ValidBlue L B) {σ : Line → Bool} (hne : (Cell L σ).Nonempty)
    (hbdd : Bornology.IsBounded (Cell L σ)) :
    ¬ (frontier (Cell L σ) ⊆ ⋃ ℓ ∈ B, ℓ.set) := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.GeneralPosition, Imo2014P6.ValidBlue, Imo2014P6.Cell
lemma Imo2014P6.main_result The main result: one can colour at least √n lines line 1940 source
Source documentation
The main result: one can colour at least √n lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2014P6.Line, Imo2014P6.GeneralPosition, Exists, And, LE.le, Real, Real.sqrt, Finset.card, Imo2014P6.ValidBlue
Proof uses: Membership.mem, Not, Insert.insert, Imo2014P6.exists_maximal_valid, Exists.intro, And.intro, SDiff.sdiff, Imo2014P6.Witness, Imo2014P6.redWitness, Nat, HPow.hPow, OfNat.ofNat, Imo2014P6.main_counting, cast, Eq.symm, Eq.trans, congrArg, Real.sqrt_le_sqrt, Eq.mp, Real.sqrt_sq and 1 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma main_result (L : Finset Line) (hGP : GeneralPosition L) :
    ∃ B : Finset Line, B ⊆ L ∧ Real.sqrt L.card ≤ B.card ∧ ValidBlue L B := by
…
```
Mentions: Imo2014P6.Line, Imo2014P6.GeneralPosition, Imo2014P6.ValidBlue
problem Imo2014P6.imo2014_p6 line 1952 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Nat, GE.ge, Finset, Imo2014P6.Line, Eq, Finset.card, Imo2014P6.GeneralPosition, And, LE.le, Real, Real.sqrt, Bool, Set.Nonempty, Prod, Imo2014P6.Cell, Bornology.IsBounded, Not, Set, frontier and 3 more
Proof uses: Exists.intro, OfNat.ofNat, Imo2014P6.ValidBlue, Imo2014P6.main_result, And.intro, Eq.mp, congrArg, Imo2014P6.not_frontier_subset_of_validBlue
35 instances, coercions and auxiliary constants left out.

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