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

100 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2025, Problem 1

A line in the plane is called sunny if it is not parallel to any of the x-axis, the y-axis, and the line x + y = 0.

Let n ⩾ 3 be a given integer. Determine all nonnegative integers k such that there exist n distinct lines in the plane satisfying both of the following:

• for all positive integers a and b with a + b ⩽ n + 1, the point (a, b) is on at least one of the lines; and

• exactly k of the n lines are sunny.

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo2025P1.xAxis The x-axis, as an affine subspace line 42 source
Source documentation
The x-axis, as an affine subspace.

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

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def xAxis : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)) where
…
```
def Imo2025P1.yAxis The y-axis, as an affine subspace line 47 source
Source documentation
The y-axis, as an affine subspace.

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

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def yAxis : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)) where
…
```
def Imo2025P1.linexy0 The line x+y=0, as an affine subspace line 52 source
Source comment
The line `x+y=0`, as an affine subspace.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AffineSubspace, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal
Proof uses: AffineSubspace.mk, Set.ofPred, Eq, HAdd.hAdd, WithLp.ofLp, Membership.mem, Set
60 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def linexy0 : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)) where
…
```
def Imo2025P1.Sunny The condition on lines in the problem line 63 source
Source documentation
The condition on lines in the problem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AffineSubspace, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal
Proof uses: And, Not, AffineSubspace.Parallel, Imo2025P1.xAxis, Imo2025P1.yAxis, Imo2025P1.linexy0
52 instances, coercions and auxiliary constants left out.
```
def Sunny (s : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2))) : Prop :=
…
```
def Imo2025P1.sunnyPred The decidable predicate Sunny line 68 source
Source documentation
The decidable predicate Sunny.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidablePred, AffineSubspace, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2025P1.Sunny
Proof uses: Classical.decPred
52 instances, coercions and auxiliary constants left out.
```
noncomputable def sunnyPred : DecidablePred Sunny := Classical.decPred _
…
```
Mentions: Imo2025P1.Sunny
abbrev Imo2025P1.Plane The 2-dimensional plane line 89 source
Source documentation
The 2-dimensional plane

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
```
abbrev Plane := EuclideanSpace ℝ (Fin 2)
```
abbrev Imo2025P1.AffSubOfPlane Affine subspaces of the plane (i.e. ∅, point, line, plane) line 92 source
Source documentation
Affine subspaces of the plane (i.e. ∅, point, line, plane)

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: AffineSubspace, Real, Imo2025P1.Plane, OfNat.ofNat, ENNReal, Fin, Nat
26 instances, coercions and auxiliary constants left out.
```
abbrev AffSubOfPlane := AffineSubspace ℝ Plane
```
Mentions: Imo2025P1.Plane
lemma Imo2025P1.vec_eq Two vectors are equal iff their x and y coordinates are equal line 95 source
Source documentation
Two vectors are equal iff their x and y coordinates are equal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Iff, Eq, WithLp, OfNat.ofNat, ENNReal, Nat, Fin, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty, And
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, WithLp.toLp.injEq, Nat.succ, eq_self, and_true, iff_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma vec_eq (x1 x2 y1 y2 : ℝ) : !₂[x1, y1] = !₂[x2, y2] ↔ (x1 = x2 ∧ y1 = y2) := by simp
```
lemma Imo2025P1.vec_repr_x Get the x coordinate of a vector line 98 source
Source documentation
Get the x coordinate of a vector.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Fin, OfNat.ofNat, Nat, WithLp.ofLp, ENNReal, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty
Proof uses: of_eq_true, eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma vec_repr_x (x y : ℝ) : !₂[x, y] 0 = x := by simp
```
lemma Imo2025P1.vec_repr_y Get the y coordinate of a vector line 100 source
Source documentation
Get the y coordinate of a vector.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Fin, OfNat.ofNat, Nat, WithLp.ofLp, ENNReal, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Matrix.cons_val_fin_one, Nat.succ, eq_self
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma vec_repr_y (x y : ℝ) : !₂[x, y] 1 = y := by simp
```
lemma Imo2025P1.vec_repr Represent a vector as a pair of real numbers line 103 source
Source documentation
Represent a vector as a pair of real numbers

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.Plane, Eq, WithLp.toLp, OfNat.ofNat, ENNReal, Nat, Fin, Real, Matrix.vecCons, WithLp.ofLp, Matrix.vecEmpty
Proof uses: PiLp.ext, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, of_eq_true, HAdd.hAdd, eq_self, eq_of_heq, List.Mem.tail and 10 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma vec_repr (x : Plane) : x = !₂[x 0, x 1] := by
…
```
Mentions: Imo2025P1.Plane
lemma Imo2025P1.vec_mul Multiply a vector by a scalar line 107 source
Source documentation
Multiply a vector by a scalar.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, WithLp, OfNat.ofNat, ENNReal, Nat, Fin, HSMul.hSMul, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty, HMul.hMul
Proof uses: PiLp.ext, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, WithLp.ofLp, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, of_eq_true, eq_self, eq_of_heq, List.Mem.tail and 12 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma vec_mul (k x y : ℝ) : k • !₂[x, y] = !₂[k * x, k * y] := by
…
```
lemma Imo2025P1.vec_sub Compute the difference of two vectors line 111 source
Source documentation
Compute the difference of two vectors

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, WithLp, OfNat.ofNat, ENNReal, Nat, Fin, HSub.hSub, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty
Proof uses: PiLp.ext, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, WithLp.ofLp, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, of_eq_true, eq_self, eq_of_heq, List.Mem.tail and 12 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma vec_sub (x1 y1 x2 y2 : ℝ) : !₂[x1, y1] - !₂[x2, y2] = !₂[x1 - x2, y1 - y2] := by
…
```
def Imo2025P1.line The "line" ax + by + c = 0 line 116 source
Source documentation
The "line" ax + by + c = 0. ("line" means except for the degenerate case a = 0 ∧ b = 0) Note: We don't enforce a ≠ 0 ∨ b ≠ 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Imo2025P1.AffSubOfPlane
Proof uses: AffineSubspace.mk, Imo2025P1.Plane, OfNat.ofNat, ENNReal, Fin, Nat, Set.ofPred, Eq, HAdd.hAdd, HMul.hMul, WithLp.ofLp, Membership.mem, Set
36 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
noncomputable def line (a b c : ℝ) : AffSubOfPlane where
…
```
Mentions: Imo2025P1.AffSubOfPlane
lemma Imo2025P1.point_on_line Check if a point (x, y) belongs to the line a * x + b * y + c = 0 line 129 source
Source documentation
Check if a point (x, y) belongs to the line a * x + b * y + c = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Iff, Membership.mem, WithLp, OfNat.ofNat, ENNReal, Nat, Fin, Imo2025P1.AffSubOfPlane, Imo2025P1.Plane, Imo2025P1.line, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty, Eq, HAdd.hAdd, HMul.hMul
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, AffineSubspace.mk, Set.ofPred, WithLp.ofLp, Set, Matrix.cons_val_fin_one, Nat.succ, iff_self
78 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma point_on_line (x y a b c : ℝ) : !₂[x, y] ∈ line a b c ↔ a * x + b * y + c = 0 := by
…
```
Mentions: Imo2025P1.line
lemma Imo2025P1.line_nonempty The line a * x + b * y + c = 0 is nonempty when a and b are not both zero line 133 source
Source documentation
The line a * x + b * y + c = 0 is nonempty when a and b are not both zero

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Or, Ne, OfNat.ofNat, Set.Nonempty, Imo2025P1.Plane, Imo2025P1.AffSubOfPlane, ENNReal, Fin, Nat, Imo2025P1.line
Proof uses: Eq.mpr, Exists, Membership.mem, id, Eq, congrArg, Set, funext, Exists.intro, WithLp.toLp, Matrix.vecCons, HDiv.hDiv, Neg.neg, Matrix.vecEmpty, HAdd.hAdd, HMul.hMul, WithLp, propext, Imo2025P1.point_on_line
76 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma line_nonempty (a b c : ℝ) (h : a ≠ 0 ∨ b ≠ 0) :
    (SetLike.coe (line a b c)).Nonempty := by
…
```
Mentions: h, Imo2025P1.line
lemma Imo2025P1.line_direction (-b, a) is the direction of the line a * x + b * y + c = 0 when a and b are not both zero line 146 source
Source documentation
(-b, a) is the direction of the line a * x + b * y + c = 0 when a and b are not both zero

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Or, Ne, OfNat.ofNat, Imo2025P1.Plane, Iff, Membership.mem, Submodule, ENNReal, Fin, Nat, AffineSubspace.direction, Imo2025P1.line, Exists, Eq, WithLp, HSMul.hSMul, WithLp.toLp, Matrix.vecCons, Neg.neg and 1 more
Proof uses: Set.Nonempty, Imo2025P1.AffSubOfPlane, Imo2025P1.line_nonempty, Iff.intro, And, AffineSubspace, VSub.vsub, Eq.mp, congrArg, propext, AffineSubspace.mem_direction_iff_eq_vsub, Exists.intro, HDiv.hDiv, HSub.hSub, WithLp.ofLp, Eq.mpr, id, Imo2025P1.vec_repr, HMul.hMul, Imo2025P1.vec_mul and 63 more
131 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma line_direction (a b c : ℝ) (h : a ≠ 0 ∨ b ≠ 0) (w : Plane) :
    w ∈ AffineSubspace.direction (line a b c) ↔ ∃ (k : ℝ), k • !₂[-b, a] = w := by
…
```
Mentions: h, Imo2025P1.Plane, Imo2025P1.line
lemma Imo2025P1.line_rank The rank of the line a * x + b * y + c = 0 is 1 when a and b are not both zero line 181 source
Source documentation
The rank of the line a * x + b * y + c = 0 is 1 when a and b are not both zero

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Or, Ne, OfNat.ofNat, Eq, Nat, Module.finrank, Subtype, Imo2025P1.Plane, Membership.mem, Submodule, ENNReal, Fin, AffineSubspace.direction, Imo2025P1.line
Proof uses: WithLp, WithLp.toLp, Matrix.vecCons, Neg.neg, Matrix.vecEmpty, Eq.mpr, Exists, HSMul.hSMul, id, congrArg, propext, Imo2025P1.line_direction, Exists.intro, MulAction.one_smul, And, finrank_eq_one_iff', Subtype.mk, And.intro, Not, Eq.trans and 11 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma line_rank (a b c : ℝ) (h : a ≠ 0 ∨ b ≠ 0) : finrank ℝ (line a b c).direction = 1 := by
…
```
Mentions: h, Imo2025P1.line
structure Imo2025P1.LineCoeffs The coeffecients of a line a * x + b * y + c = 0 line 193 source
Source documentation
The coeffecients of a line a * x + b * y + c = 0

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure LineCoeffs where
…
```
def Imo2025P1.line' Build a line from a LineCoeffs line 199 source
Source documentation
Build a line from a LineCoeffs

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.LineCoeffs, Imo2025P1.AffSubOfPlane
Proof uses: Imo2025P1.line, Imo2025P1.LineCoeffs.a, Imo2025P1.LineCoeffs.b, Imo2025P1.LineCoeffs.c
```
noncomputable def line' (coeff : LineCoeffs) := line coeff.a coeff.b coeff.c
```
Mentions: Imo2025P1.LineCoeffs, Imo2025P1.line
def Imo2025P1.edgeCoeffs line 201 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Imo2025P1.LineCoeffs
Proof uses: Imo2025P1.edgeCoeffs.match_1, Unit, Imo2025P1.LineCoeffs.mk, Real, Neg.neg, HAdd.hAdd
11 instances, coercions and auxiliary constants left out.
def Imo2025P1.edgeLine The three lines on the edges of the triangular integer grid, each side having n points: x - 1 = 0; y - 1 = 0; x + y - (n + 1) = 0 line 209 source
Source documentation
The three lines on the edges of the triangular integer grid, each side having n points: x - 1 = 0; y - 1 = 0; x + y - (n + 1) = 0. These lines are named edgeLine n 0, edgeLine n 1, edgeLine n 2, resp.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Imo2025P1.AffSubOfPlane
Proof uses: Imo2025P1.line', Imo2025P1.edgeCoeffs
2 instances, coercions and auxiliary constants left out.
```
noncomputable def edgeLine (n : ℕ) (d : Fin 3) := line' (edgeCoeffs n d)
```
Mentions: Imo2025P1.line', Imo2025P1.edgeCoeffs
lemma Imo2025P1.y_ax_line The y axis is the line x = 0 line 212 source
Source documentation
The y axis is the line x = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Imo2025P1.AffSubOfPlane, Imo2025P1.line, OfNat.ofNat, Real, Imo2025P1.yAxis
Proof uses: of_eq_true, AffineSubspace.mk, EuclideanSpace, Fin, Nat, ENNReal, Set.ofPred, WithLp.ofLp, Membership.mem, Set, Eq.trans, Imo2025P1.Plane, HAdd.hAdd, HMul.hMul, HVAdd.hVAdd, HSMul.hSMul, VSub.vsub, congrArg, funext, congrFun' and 8 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma y_ax_line : line 1 0 0 = yAxis := by
…
```
Mentions: Imo2025P1.line, Imo2025P1.yAxis
lemma Imo2025P1.x_ax_line The x axis is the line y = 0 line 216 source
Source documentation
The x axis is the line y = 0

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Imo2025P1.AffSubOfPlane, Imo2025P1.line, OfNat.ofNat, Real, Imo2025P1.xAxis
Proof uses: of_eq_true, AffineSubspace.mk, EuclideanSpace, Fin, Nat, ENNReal, Set.ofPred, WithLp.ofLp, Membership.mem, Set, Eq.trans, Imo2025P1.Plane, HAdd.hAdd, HMul.hMul, HVAdd.hVAdd, HSMul.hSMul, VSub.vsub, congrArg, funext, congrFun' and 9 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma x_ax_line : line 0 1 0 = xAxis := by
…
```
Mentions: Imo2025P1.line, Imo2025P1.xAxis
lemma Imo2025P1.xy0_line The line x + y = 0 line 220 source
Source documentation
The line x + y = 0

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Imo2025P1.AffSubOfPlane, Imo2025P1.line, OfNat.ofNat, Real, Imo2025P1.linexy0
Proof uses: of_eq_true, AffineSubspace.mk, EuclideanSpace, Fin, Nat, ENNReal, Set.ofPred, HAdd.hAdd, WithLp.ofLp, Membership.mem, Set, Eq.trans, Imo2025P1.Plane, HMul.hMul, HVAdd.hVAdd, HSMul.hSMul, VSub.vsub, congrArg, funext, congrFun' and 7 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma xy0_line : line 1 1 0 = linexy0 := by
…
```
Mentions: Imo2025P1.line, Imo2025P1.linexy0
lemma Imo2025P1.line_para' Preparation lemma for checking if two lines are parallel line 224 source
Source documentation
Preparation lemma for checking if two lines are parallel

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Or, Ne, OfNat.ofNat, Eq, HMul.hMul, Imo2025P1.Plane, Exists, WithLp, ENNReal, Nat, Fin, HSMul.hSMul, WithLp.toLp, Matrix.vecCons, Neg.neg, Matrix.vecEmpty
Proof uses: WithLp.ofLp, And, Eq.mp, congrArg, propext, Imo2025P1.vec_eq, Imo2025P1.vec_repr, Imo2025P1.vec_mul, Exists.intro, HDiv.hDiv, Eq.mpr, id
42 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma line_para' (a b a' b' : ℝ) (h' : a' ≠ 0 ∨ b' ≠ 0)
    (hab : a * b' = a' * b) (w : Plane) :
    (∃ (k : ℝ), k • !₂[-b, a] = w) → (∃ (k : ℝ), k • !₂[-b', a'] = w) := by
…
```
Mentions: Imo2025P1.Plane
lemma Imo2025P1.line_para Two non-degenerate lines a * x + b * y + c = 0 and a' * x + b' * y + c = 0 are parallel iff a * b' = a' * b line 240 source
Source documentation
Two non-degenerate lines a * x + b * y + c = 0 and a' * x + b' * y + c = 0 are parallel iff a * b' = a' * b.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Or, Ne, OfNat.ofNat, Iff, AffineSubspace.Parallel, Imo2025P1.Plane, ENNReal, Fin, Nat, Imo2025P1.line, Eq, HMul.hMul
Proof uses: Eq.mpr, And, Submodule, AffineSubspace.direction, AffineSubspace, Bot.bot, id, congrArg, propext, AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot, Iff.intro, WithLp, WithLp.toLp, Matrix.vecCons, Neg.neg, Matrix.vecEmpty, Membership.mem, Exists, HSMul.hSMul, Imo2025P1.line_direction and 40 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
lemma line_para (a b c a' b' c' : ℝ) (h : a ≠ 0 ∨ b ≠ 0) (h' : a' ≠ 0 ∨ b' ≠ 0) :
    line a b c ∥ line a' b' c' ↔ a * b' = a' * b := by
…
```
Mentions: h, Imo2025P1.line
lemma Imo2025P1.line_para_two_points If the line a * x + b * y + c is parallel to L, and both lines go through (x1, y1), (x2, y2), then a * (x2 - x1) + b * (y2 - y1) = 0 line 277 source
Source documentation
If the line a * x + b * y + c is parallel to L, and both lines go through (x1, y1), (x2, y2), then a * (x2 - x1) + b * (y2 - y1) = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Or, Ne, OfNat.ofNat, Imo2025P1.AffSubOfPlane, AffineSubspace.Parallel, Imo2025P1.Plane, ENNReal, Fin, Nat, Imo2025P1.line, Membership.mem, WithLp, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty, Eq, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: dite, And, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, congrFun', sub_self, eq_self, implies_congr, Eq.refl, congr, MulZeroClass.mul_zero, add_zero, implies_true, Not, Submodule, AffineSubspace.direction and 62 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma line_para_two_points (a b c : ℝ) (h : a ≠ 0 ∨ b ≠ 0) (L : AffSubOfPlane) (x1 y1 x2 y2 : ℝ) :
    line a b c ∥ L → !₂[x1, y1] ∈ L → !₂[x2, y2] ∈ L → a * (x2 - x1) + b * (y2 - y1) = 0 := by
…
```
Mentions: h, Imo2025P1.AffSubOfPlane, Imo2025P1.line
lemma Imo2025P1.line_eq_check If the lines a * x + b * y + c = 0 and a' * x + b' * y + c = 0 are equal, then a * b' = a' * b ∧ a * c' = a' * c ∧ b * c' = b' * c line 299 source
Source documentation
If the lines a * x + b * y + c = 0 and a' * x + b' * y + c = 0 are equal, then a * b' = a' * b ∧ a * c' = a' * c ∧ b * c' = b' * c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Or, Ne, OfNat.ofNat, Eq, Imo2025P1.AffSubOfPlane, Imo2025P1.line, And, HMul.hMul
Proof uses: Eq.mpr, AffineSubspace.Parallel, Imo2025P1.Plane, ENNReal, Fin, Nat, id, congrArg, Eq.symm, propext, Imo2025P1.line_para, AffineSubspace.Parallel.refl, And.intro, dite, of_eq_true, Eq.trans, True, congr, congrFun', MulZeroClass.zero_mul and 141 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
lemma line_eq_check (a b c a' b' c' : ℝ) (h : a ≠ 0 ∨ b ≠ 0) (h' : a' ≠ 0 ∨ b' ≠ 0)
    (heq : line a b c = line a' b' c') :
    a * b' = a' * b ∧ a * c' = a' * c ∧ b * c' = b' * c := by
…
```
Mentions: h, Imo2025P1.line
lemma Imo2025P1.line_contains Preparation lemma for get_line_eq line 325 source
Source documentation
Preparation lemma for get_line_eq.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.AffSubOfPlane, Eq, Nat, Module.finrank, Real, Subtype, Imo2025P1.Plane, Membership.mem, Submodule, OfNat.ofNat, ENNReal, Fin, AffineSubspace.direction, Ne, LE.le
Proof uses: Eq.mpr, AffineSubspace, id, congrArg, propext, AffineSubspace.le_def', And, Exists, HSMul.hSMul, Eq.mp, finrank_eq_one_iff', Subtype.mk, VSub.vsub, AffineSubspace.vsub_mem_direction, HSub.hSub, Eq.symm, sub_eq_zero, congrFun', Eq.trans, zero_smul and 54 more
182 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma line_contains (L L' : AffSubOfPlane) (hL : finrank ℝ L.direction = 1) (a b : Plane) :
    (a ≠ b → a ∈ L → b ∈ L → a ∈ L' → b ∈ L' → L ≤ L') := by
…
```
Mentions: Imo2025P1.AffSubOfPlane, Imo2025P1.Plane
lemma Imo2025P1.get_line_eq If both of the two non-degenerate lines L and L' go through two different points a and b, then L = L' line 346 source
Source documentation
If both of the two non-degenerate lines L and L' go through two different points a and b, then L = L'.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.AffSubOfPlane, Eq, Nat, Module.finrank, Real, Subtype, Imo2025P1.Plane, Membership.mem, Submodule, OfNat.ofNat, ENNReal, Fin, AffineSubspace.direction, Ne
Proof uses: LE.le.antisymm, Imo2025P1.line_contains
67 instances, coercions and auxiliary constants left out.
```
lemma get_line_eq
    (L L' : AffSubOfPlane) (hL : finrank ℝ L.direction = 1) (hL' : finrank ℝ L'.direction = 1)
    (a b : Plane) (hab : a ≠ b)
    (ha : a ∈ L) (hb : b ∈ L) (ha' : a ∈ L') (hb' : b ∈ L') : L = L' :=
…
```
Mentions: Imo2025P1.AffSubOfPlane, Imo2025P1.Plane
def Imo2025P1.eqAffSubOfPlane The decidable equality predicate L = L' for (L L' : AffSubOfPlane) line 356 source
Source documentation
The decidable equality predicate L = L' for (L L' : AffSubOfPlane).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Imo2025P1.AffSubOfPlane
Proof uses: Classical.decEq
```
noncomputable def eqAffSubOfPlane : DecidableEq AffSubOfPlane := Classical.decEq _
```
Mentions: Imo2025P1.AffSubOfPlane
lemma Imo2025P1.sunny_slope Check if the line a * x + b * y + c = 0 is sunny or not line 359 source
Source documentation
Check if the line a * x + b * y + c = 0 is sunny or not.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Or, Ne, OfNat.ofNat, Iff, Imo2025P1.Sunny, Imo2025P1.line, And
Proof uses: id, Eq.mpr, Not, AffineSubspace.Parallel, EuclideanSpace, Fin, Nat, ENNReal, Imo2025P1.xAxis, Imo2025P1.yAxis, Imo2025P1.linexy0, Eq, congrArg, Imo2025P1.AffSubOfPlane, Eq.symm, Imo2025P1.x_ax_line, Imo2025P1.y_ax_line, Imo2025P1.xy0_line, HMul.hMul, Imo2025P1.Plane and 13 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma sunny_slope (a b c : ℝ) (h : a ≠ 0 ∨ b ≠ 0) :
    Sunny (line a b c) ↔ a ≠ 0 ∧ b ≠ 0 ∧ a ≠ b := by
…
```
Mentions: h, Imo2025P1.Sunny, Imo2025P1.line
def Imo2025P1.grid The integer grid consisting of (a, b), where a, b are positive integers and a + b ≤ n + 1 line 368 source
Source documentation
The integer grid consisting of (a, b), where a, b are positive integers and a + b ≤ n + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set, Imo2025P1.Plane
Proof uses: Set.ofPred, Exists, And, Eq, Fin, OfNat.ofNat, Real, WithLp.ofLp, ENNReal, LT.lt, LE.le, HAdd.hAdd
14 instances, coercions and auxiliary constants left out.
```
def grid (n : ℕ) : Set Plane :=
…
```
Mentions: Imo2025P1.Plane
lemma Imo2025P1.point_in_grid Check if (a, b) is in grid n for natural numbers a, b line 372 source
Source documentation
Check if (a, b) is in grid n for natural numbers a, b.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Membership.mem, WithLp, OfNat.ofNat, ENNReal, Fin, Real, Set, Imo2025P1.Plane, Imo2025P1.grid, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty, And, LT.lt, LE.le, HAdd.hAdd
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Set.ofPred, Exists, Eq, WithLp.ofLp, funext, congr, Matrix.cons_val_fin_one, Nat.succ, iff_self
43 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma point_in_grid (n : ℕ) (a b : ℕ) :
    !₂[(a : ℝ), (b : ℝ)] ∈ grid n ↔ 0 < a ∧ 0 < b ∧ a + b ≤ n + 1 := by simp [grid]
```
Mentions: Imo2025P1.grid
structure Imo2025P1.coverConfig The configuration of a finise set of lines going through a set of points in the plane line 376 source
Source documentation
The configuration of a finise set of lines going through a set of points in the plane.

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure coverConfig where
…
```
lemma Imo2025P1.coverConfig.nS_leq_n line 394 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverConfig, LE.le, Nat, Imo2025P1.coverConfig.nS, Imo2025P1.coverConfig.n
Proof uses: Eq.mpr, Finset.card, AffineSubspace, Real, EuclideanSpace, Fin, OfNat.ofNat, ENNReal, Finset.filter, Imo2025P1.Sunny, Imo2025P1.sunnyPred, Imo2025P1.coverConfig.lines, id, Eq, congrArg, Eq.symm, Imo2025P1.coverConfig.sunny_count, Imo2025P1.AffSubOfPlane, Imo2025P1.coverConfig.lines_count, of_eq_true
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2025P1.shiftSet shiftSet v g is the result of shifting every point in g by the vector v line 399 source
Source documentation
shiftSet v g is the result of shifting every point in g by the vector v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.Plane, Set
Proof uses: Set.image, AffineEquiv, Real, OfNat.ofNat, ENNReal, Fin, Nat, AffineEquiv.constVAdd
29 instances, coercions and auxiliary constants left out.
```
def shiftSet (v : Plane) (g : Set Plane) : Set Plane :=
…
```
Mentions: Imo2025P1.Plane
def Imo2025P1.gridShift line 402 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Imo2025P1.Plane
Proof uses: Imo2025P1.edgeCoeffs.match_1, Unit, WithLp.toLp, ENNReal, Real, Matrix.vecCons, Neg.neg, Matrix.vecEmpty
12 instances, coercions and auxiliary constants left out.
lemma Imo2025P1.grid_shift After removing an edge from grid (n + 1) and appropriate shifting, the resulting set is grid n line 412 source
Source documentation
After removing an edge from grid (n + 1) and appropriate shifting, the resulting set is grid n. Remove edgeLine (n + 1) 0 (i.e. left edge) -> shift by (-1, 0). Remove edgeLine (n + 1) 1 (i.e. bottom edge) -> shift by (0, -1). Remove edgeLine (n + 1) 2 (i.e. diagonal edge) -> shift by (0, 0) (i.e. no shift).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Eq, Set, Imo2025P1.Plane, Imo2025P1.shiftSet, Imo2025P1.gridShift, SDiff.sdiff, Imo2025P1.grid, HAdd.hAdd, Imo2025P1.AffSubOfPlane, Real, ENNReal, Imo2025P1.edgeLine
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, And, Exists, Neg.neg, WithLp.ofLp, LT.lt, LE.le, Not, id, congr, congrArg, Eq.trans, Set.ofPred, Set.preimage, congrFun', Set.image, AffineEquiv and 77 more
209 instances, coercions and auxiliary constants left out.

Tactic trace: 125 steps
Open to load the checked before-and-after goal states.
```
lemma grid_shift (n : ℕ) (d : Fin 3) :
    shiftSet (gridShift d) (grid (n + 1) \ (edgeLine (n + 1) d)) = grid n := by
…
```
Mentions: Imo2025P1.shiftSet, Imo2025P1.gridShift, Imo2025P1.grid, Imo2025P1.edgeLine
lemma Imo2025P1.grid_remove_diag After removing the diagonal edge from grid (n + 1) , the resulting set is grid n line 500 source
Source documentation
After removing the diagonal edge from grid (n + 1) , the resulting set is grid n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Set, Imo2025P1.Plane, SDiff.sdiff, Imo2025P1.grid, HAdd.hAdd, OfNat.ofNat, Imo2025P1.AffSubOfPlane, Real, ENNReal, Fin, Imo2025P1.edgeLine
Proof uses: Eq.mpr, Imo2025P1.shiftSet, Imo2025P1.gridShift, id, congrArg, Eq.symm, Imo2025P1.grid_shift, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty, Imo2025P1.gridShift.eq_3, rfl, Set.preimage, Neg.neg, Eq.trans, Set.image, AffineEquiv, AffineEquiv.constVAdd, Set.image_congr, Membership.mem and 14 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma grid_remove_diag (n : ℕ) : grid (n + 1) \ (edgeLine (n + 1) 2) = grid n := by
…
```
Mentions: Imo2025P1.grid, Imo2025P1.edgeLine
def Imo2025P1.shiftLineMap shiftLineMap v L shifts the line L by the vector v line 508 source
Source documentation
shiftLineMap v L shifts the line L by the vector v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.Plane, Imo2025P1.AffSubOfPlane
Proof uses: AffineSubspace.map, Real, OfNat.ofNat, ENNReal, Fin, Nat, AffineEquiv.constVAdd
27 instances, coercions and auxiliary constants left out.
```
noncomputable def shiftLineMap (v : Plane) (L : AffSubOfPlane) : AffSubOfPlane :=
…
```
Mentions: Imo2025P1.Plane, Imo2025P1.AffSubOfPlane
lemma Imo2025P1.affine_trans The preparation lemma on composing two line-shifts line 512 source
Source documentation
The preparation lemma on composing two line-shifts.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AffineEquiv, Real, Imo2025P1.Plane, OfNat.ofNat, ENNReal, Fin, Nat, Eq, AffineMap, AffineEquiv.trans, AffineMap.comp
Proof uses: of_eq_true, eq_self
54 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma affine_trans (e : Plane ≃ᵃ[ℝ] Plane) (e' : Plane ≃ᵃ[ℝ] Plane) :
    (AffineEquiv.trans e e').toAffineMap = e'.toAffineMap.comp e.toAffineMap := by simp
```
Mentions: Imo2025P1.Plane
def Imo2025P1.shiftLine shiftLineMap v is the injective map AffSubOfPlane ↪ AffSubOfPlane that shifts by the vector v line 517 source
Source documentation
shiftLineMap v is the injective map AffSubOfPlane ↪ AffSubOfPlane that shifts by the vector v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.Plane, Function.Embedding, Imo2025P1.AffSubOfPlane
Proof uses: Function.Embedding.mk, Imo2025P1.shiftLineMap
1 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
noncomputable def shiftLine (v : Plane) : AffSubOfPlane ↪ AffSubOfPlane := ⟨
…
```
Mentions: Imo2025P1.Plane, Imo2025P1.AffSubOfPlane
lemma Imo2025P1.shift_para The shift of a line is parallel to the original line line 529 source
Source documentation
The shift of a line is parallel to the original line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.Plane, Imo2025P1.AffSubOfPlane, AffineSubspace.Parallel, Real, OfNat.ofNat, ENNReal, Fin, Nat, Function.Embedding, Imo2025P1.shiftLine
Proof uses: id, Exists.intro, Eq, AffineSubspace, AffineSubspace.map, AffineEquiv.constVAdd, Eq.refl
57 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma shift_para (v : Plane) (L : AffSubOfPlane) :  L ∥ shiftLine v L := by
…
```
Mentions: Imo2025P1.Plane, Imo2025P1.AffSubOfPlane, Imo2025P1.shiftLine
def Imo2025P1.shiftLines shiftLines v lines is the collection of shiftLine v L for L ∈ lines line 533 source
Source documentation
shiftLines v lines is the collection of shiftLine v L for L ∈ lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.Plane, Finset, Imo2025P1.AffSubOfPlane
Proof uses: Finset.map, Imo2025P1.shiftLine
```
noncomputable def shiftLines (v : Plane) (lines : Finset AffSubOfPlane) : Finset AffSubOfPlane :=
…
```
Mentions: Imo2025P1.Plane, Imo2025P1.AffSubOfPlane
lemma Imo2025P1.shift_line_inv shiftLine (-v) is the inverse of shiftLine v line 537 source
Source documentation
shiftLine (-v) is the inverse of shiftLine v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.Plane, Imo2025P1.AffSubOfPlane, Eq, Function.Embedding, Imo2025P1.shiftLine, Neg.neg, OfNat.ofNat, ENNReal, Fin, Nat, Real
Proof uses: id, Eq.mpr, AffineSubspace.map, AffineEquiv.constVAdd, AffineMap.comp, congrArg, AffineSubspace, AffineSubspace.map_map, AffineEquiv.trans, AffineMap, Eq.symm, Imo2025P1.affine_trans, HAdd.hAdd, AffineEquiv, AffineEquiv.constVAdd_add, of_eq_true, Eq.trans, True, congrFun', AffineMap.id and 5 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma shift_line_inv (v : Plane) (L : AffSubOfPlane) : (shiftLine (-v)) ((shiftLine v) L) = L := by
…
```
Mentions: Imo2025P1.Plane, Imo2025P1.AffSubOfPlane, Imo2025P1.shiftLine
lemma Imo2025P1.shift_sunny If L is sunny, then so is its shift line 543 source
Source documentation
If L is sunny, then so is its shift.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.Plane, Imo2025P1.AffSubOfPlane, Imo2025P1.Sunny, Function.Embedding, Imo2025P1.shiftLine
Proof uses: id, And, Not, AffineSubspace.Parallel, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2025P1.xAxis, Imo2025P1.yAxis, Imo2025P1.linexy0, And.intro, AffineSubspace.Parallel.trans, Imo2025P1.shift_para
31 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma shift_sunny (v : Plane) (L : AffSubOfPlane) : Sunny L → Sunny (shiftLine v L) := by
…
```
Mentions: Imo2025P1.Plane, Imo2025P1.AffSubOfPlane, Imo2025P1.Sunny, Imo2025P1.shiftLine
def Imo2025P1.coverConfig.shift Shift a coverConfig by the vector v line 549 source
Source documentation
Shift a coverConfig by the vector v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverConfig, Imo2025P1.Plane
Proof uses: Imo2025P1.coverConfig.mk, Imo2025P1.shiftLines, Imo2025P1.coverConfig.lines, Imo2025P1.shiftSet, Imo2025P1.coverConfig.g, Imo2025P1.coverConfig.n, Imo2025P1.coverConfig.nS
4 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
```
noncomputable def coverConfig.shift (C : coverConfig) (v : Plane) : coverConfig where
…
```
Mentions: Imo2025P1.coverConfig, Imo2025P1.Plane
def Imo2025P1.coverConfig.removeLine Remove a line L from a coverConfig line 595 source
Source documentation
Remove a line L from a coverConfig.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverConfig, Imo2025P1.AffSubOfPlane, Membership.mem, Finset, Imo2025P1.coverConfig.lines, Not, Imo2025P1.Sunny
Proof uses: Imo2025P1.coverConfig.mk, DecidableEq, Imo2025P1.eqAffSubOfPlane, Finset.erase, SDiff.sdiff, Set, Imo2025P1.Plane, Imo2025P1.coverConfig.g, Real, OfNat.ofNat, ENNReal, Fin, Nat, HSub.hSub, Imo2025P1.coverConfig.n, Imo2025P1.coverConfig.nS
39 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
noncomputable def coverConfig.removeLine (C : coverConfig) (L : AffSubOfPlane) (hL : L ∈ C.lines)
(hS : ¬Sunny L) : coverConfig where
…
```
Mentions: Imo2025P1.coverConfig, Imo2025P1.AffSubOfPlane, Imo2025P1.Sunny
structure Imo2025P1.coverGridConfig A coverConfig with the additional requirement that the set of points to be covered is grid n line 624 source
Source documentation
A coverConfig with the additional requirement that the set of points to be covered is grid n

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure coverGridConfig extends coverConfig where
…
```
Mentions: Imo2025P1.coverConfig
def Imo2025P1.coverGridConfig.edgeLine The three edge lines of a the grid point to be covered in a coverGridConfig line 629 source
Source documentation
The three edge lines of a the grid point to be covered in a coverGridConfig

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridConfig, Fin, OfNat.ofNat, Nat, Imo2025P1.AffSubOfPlane
Proof uses: Imo2025P1.edgeLine, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig
1 instances, coercions and auxiliary constants left out.
```
noncomputable def coverGridConfig.edgeLine (C : coverGridConfig) :=
…
```
Mentions: Imo2025P1.coverGridConfig
def Imo2025P1.reduce If a coverGridConfig contains a line on the edge, remove the edge and shift it to a smaller coverGridConfig line 634 source
Source documentation
If a coverGridConfig contains a line on the edge, remove the edge and shift it to a smaller coverGridConfig

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridConfig, Fin, OfNat.ofNat, Nat, Membership.mem, Imo2025P1.AffSubOfPlane, Finset, Imo2025P1.coverConfig.lines, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.coverGridConfig.edgeLine
Proof uses: Imo2025P1.coverConfig, Imo2025P1.coverConfig.shift, Imo2025P1.coverConfig.removeLine, Imo2025P1.reduce.edge_not_sunny, Imo2025P1.gridShift, Imo2025P1.coverGridConfig.mk
7 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
noncomputable def reduce (C : coverGridConfig) (d : Fin 3) (hd : C.edgeLine d ∈ C.lines) :
    coverGridConfig where
…
```
Mentions: Imo2025P1.coverGridConfig
lemma Imo2025P1.coverGridConfig.reduce_count Applying coverGridConfig.reduce decrements n by 1 and doesn't change nS line 650 source
Source documentation
Applying coverGridConfig.reduce decrements n by 1 and doesn't change nS.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridConfig, Fin, OfNat.ofNat, Nat, Membership.mem, Imo2025P1.AffSubOfPlane, Finset, Imo2025P1.coverConfig.lines, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.coverGridConfig.edgeLine, And, Eq, Imo2025P1.coverConfig.n, Imo2025P1.reduce, HSub.hSub, Imo2025P1.coverConfig.nS
Proof uses: of_eq_true, Eq.trans, True, congr, congrArg, eq_self, and_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridConfig.reduce_count (C : coverGridConfig) (d : Fin 3) (hd : C.edgeLine d ∈ C.lines) :
    (reduce C d hd).n = C.n - 1 ∧ (reduce C d hd).nS = C.nS := by
…
```
Mentions: Imo2025P1.coverGridConfig, Imo2025P1.reduce
lemma Imo2025P1.not_colinear Given reals numbers M > 0 and a, b, c ∈ (0, M), the points (1, a + 1), (b + 1, 1), (c + 1, M - c + 1) are not colinear line 656 source
Source documentation
Given reals numbers M > 0 and a, b, c ∈ (0, M), the points (1, a + 1), (b + 1, 1), (c + 1, M - c + 1) are not colinear.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.AffSubOfPlane, Real, Eq, Nat, Module.finrank, Subtype, Imo2025P1.Plane, Membership.mem, Submodule, OfNat.ofNat, ENNReal, Fin, AffineSubspace.direction, GT.gt, LT.lt, WithLp, WithLp.toLp, Matrix.vecCons, HAdd.hAdd, Matrix.vecEmpty and 2 more
Proof uses: Imo2025P1.line, Neg.neg, HMul.hMul, Imo2025P1.get_line_eq, Imo2025P1.line_rank, Or.inl, Ne, ne_of_gt, And.left, Eq.mp, And, congrArg, propext, Imo2025P1.vec_eq, False.elim, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast and 78 more
165 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
```
lemma not_colinear (L : AffSubOfPlane) (M a b c : ℝ) :
    finrank ℝ L.direction = 1 → M > 0 → 0 < a → a < M → 0 < b → b < M → 0 < c → c < M →
    !₂[1, a + 1] ∈ L → !₂[b + 1, 1] ∈ L → !₂[c + 1, M - c + 1] ∈ L → False := by
…
```
Mentions: Imo2025P1.AffSubOfPlane
lemma Imo2025P1.not_colinear_nat Given natural numbers M > 0 and a, b, c ∈ (0, M), the points (1, a + 1), (b + 1, 1), (c + 1, M - c + 1) are not colinear line 688 source
Source documentation
Given natural numbers M > 0 and a, b, c ∈ (0, M), the points (1, a + 1), (b + 1, 1), (c + 1, M - c + 1) are not colinear.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.AffSubOfPlane, Nat, Eq, Module.finrank, Real, Subtype, Imo2025P1.Plane, Membership.mem, Submodule, OfNat.ofNat, ENNReal, Fin, AffineSubspace.direction, GT.gt, LT.lt, WithLp, WithLp.toLp, Matrix.vecCons, HAdd.hAdd, Matrix.vecEmpty and 2 more
Proof uses: GE.ge, Eq.mpr, Eq.refl, Imo2025P1.not_colinear, id, Eq.trans, congrArg, Eq.symm, Nat.cast_zero, congrFun', Nat.succ, congr, Nat.cast_one
115 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma not_colinear_nat (L : AffSubOfPlane) (M a b c : ℕ) :
    finrank ℝ L.direction = 1 → M > 0 → 0 < a → a < M → 0 < b → b < M → 0 < c → c < M →
    (!₂[1, (a + 1 : ℕ)] : Plane) ∈ L →
    (!₂[(b + 1 : ℕ), 1] : Plane) ∈ L →
    (!₂[(c + 1 : ℕ), (M - c + 1 : ℕ)] : Plane) ∈ L →
    False := by
…
```
Mentions: Imo2025P1.AffSubOfPlane, Imo2025P1.Plane
lemma Imo2025P1.n_minus_plus If n : ℕ and n > 1, if n' : ℕ and n' = n - 1, then (n' : ℝ) + (1 : ℝ) = (n : ℝ) line 699 source
Source documentation
If n : ℕ and n > 1, if n' : ℕ and n' = n - 1, then (n' : ℝ) + (1 : ℝ) = (n : ℝ).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Eq, Real, HAdd.hAdd, HSub.hSub
Proof uses: Eq.mpr, id, Eq.trans, congrFun', congrArg, Eq.symm, Nat.cast_one
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma n_minus_plus (n : ℕ) (hn : n > 1) : (n - 1 : ℕ) + (1 : ℝ) = n := by norm_cast; lia
```
lemma Imo2025P1.line_sunny_two_points If L goes through (x1, y1) and (x2, y2), and x1 ≠ x2, y1 ≠ y2, x2 - x1 ≠ y1 - y2, then L is sunny line 703 source
Source documentation
If L goes through (x1, y1) and (x2, y2), and x1 ≠ x2, y1 ≠ y2, x2 - x1 ≠ y1 - y2, then L is sunny.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.AffSubOfPlane, Real, Membership.mem, WithLp, OfNat.ofNat, ENNReal, Nat, Fin, Imo2025P1.Plane, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty, Ne, HSub.hSub, Imo2025P1.Sunny
Proof uses: Eq.mpr, And, Not, AffineSubspace.Parallel, EuclideanSpace, Imo2025P1.line, id, Eq, congr, Imo2025P1.xAxis, Imo2025P1.yAxis, Imo2025P1.linexy0, congrArg, AffineSubspace, And.intro, HAdd.hAdd, HMul.hMul, Imo2025P1.line_para_two_points, of_eq_true, Or and 64 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma line_sunny_two_points (L : AffSubOfPlane) (x1 y1 x2 y2 : ℝ)
    (h1 : !₂[x1, y1] ∈ L) (h2 : !₂[x2, y2] ∈ L)
    (hx : x1 ≠ x2) (hy : y1 ≠ y2) (hxy : x2 - x1 ≠ y1 - y2) : Sunny L := by
…
```
Mentions: Imo2025P1.AffSubOfPlane, Imo2025P1.Sunny
def Imo2025P1.coverGridConfig.findLine coverGridConfig.findLine chooses a line in lines that goes through x line 714 source
Source documentation
coverGridConfig.findLine chooses a line in lines that goes through x

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridConfig, Imo2025P1.Plane, Membership.mem, Set, Imo2025P1.coverConfig.g, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.AffSubOfPlane
Proof uses: Classical.choose, And, Finset, Imo2025P1.coverConfig.lines, Real, OfNat.ofNat, ENNReal, Fin, Nat
32 instances, coercions and auxiliary constants left out.
```
noncomputable def coverGridConfig.findLine (C : coverGridConfig) (x : Plane) (hx : x ∈ C.g) :=
…
```
Mentions: Imo2025P1.coverGridConfig, Imo2025P1.Plane
lemma Imo2025P1.coverGridConfig.find_line_correct coverGridConfig.findLine chooses a line in lines that goes through x line 718 source
Source documentation
coverGridConfig.findLine chooses a line in lines that goes through x

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridConfig, Imo2025P1.Plane, Membership.mem, Set, Imo2025P1.coverConfig.g, Imo2025P1.coverGridConfig.tocoverConfig, And, Imo2025P1.AffSubOfPlane, Finset, Imo2025P1.coverConfig.lines, Imo2025P1.coverGridConfig.findLine, Real, OfNat.ofNat, ENNReal, Fin, Nat
Proof uses: Classical.choose, Imo2025P1.coverConfig.lines_cover, Classical.choose_spec, id
60 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridConfig.find_line_correct (C : coverGridConfig) (x : Plane) (hx : x ∈ C.g) :
    C.findLine x hx ∈ C.lines ∧ x ∈ C.findLine x hx := by
…
```
Mentions: Imo2025P1.coverGridConfig, Imo2025P1.Plane
lemma Imo2025P1.coverGridConfig.find_same_line Documented declaration: find_same_line line 726 source
Source documentation
If findLine finds the same line that goes through different points x and y, and if the non-degenerate line a * x + b * y + c = 0 passes through x and y, then a * x + b * y + c = 0 is in lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridConfig, Imo2025P1.Plane, Membership.mem, Set, Imo2025P1.coverConfig.g, Imo2025P1.coverGridConfig.tocoverConfig, Real, Ne, Eq, Imo2025P1.AffSubOfPlane, Imo2025P1.coverGridConfig.findLine, Or, OfNat.ofNat, ENNReal, Fin, Nat, Imo2025P1.line, Finset, Imo2025P1.coverConfig.lines
Proof uses: id, of_eq_true, Module.finrank, Subtype, Submodule, AffineSubspace.direction, Imo2025P1.get_line_eq, Imo2025P1.coverConfig.lines_rank, Imo2025P1.line_rank, Eq.mpr, congrArg, Eq.symm
71 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridConfig.find_same_line (C : coverGridConfig) (x y : Plane)
    (hx : x ∈ C.g) (hy : y ∈ C.g) (a b c : ℝ) (hxy : x ≠ y)
    (hEq : C.findLine x hx = C.findLine y hy)
    (hab : a ≠ 0 ∨ b ≠ 0)
    (hxL : x ∈ line a b c) (hyL : y ∈ line a b c) :
    line a b c ∈ C.lines := by
…
```
Mentions: Imo2025P1.coverGridConfig, Imo2025P1.Plane, Imo2025P1.line
def Imo2025P1.coverGridConfig.edgePoint The points on the three edges of a coverGridConfig line 742 source
Source documentation
The points on the three edges of a coverGridConfig

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridConfig, Fin, OfNat.ofNat, Nat, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.Plane
Proof uses: Imo2025P1.edgeCoeffs.match_1, Unit, WithLp.toLp, ENNReal, Real, Matrix.vecCons, HAdd.hAdd, Matrix.vecEmpty, HSub.hSub
14 instances, coercions and auxiliary constants left out.
```
def coverGridConfig.edgePoint (C : coverGridConfig) (d : Fin 3) (k : Fin C.n) : Plane :=
…
```
Mentions: Imo2025P1.coverGridConfig, Imo2025P1.Plane
lemma Imo2025P1.coverGridConfig.edge_point_in_grid The points on the three edges of a coverGridConfig are in its grid line 749 source
Source documentation
The points on the three edges of a coverGridConfig are in its grid.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridConfig, Fin, OfNat.ofNat, Nat, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Membership.mem, Imo2025P1.Plane, Set, Imo2025P1.coverConfig.g, Imo2025P1.coverGridConfig.edgePoint
Proof uses: Eq.mpr, Imo2025P1.grid, id, Eq, congrArg, Imo2025P1.coverGridConfig.g_is_grid, List, List.Mem, List.finRange, HEq, Finset, Fintype.elems, Fintype.complete, Imo2025P1.edgeCoeffs.match_1, Unit, WithLp.toLp, ENNReal, Real, Matrix.vecCons, HAdd.hAdd and 21 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridConfig.edge_point_in_grid (C : coverGridConfig) (d : Fin 3) (i : Fin C.n) :
    C.edgePoint d i ∈ C.g := by
…
```
Mentions: Imo2025P1.coverGridConfig
lemma Imo2025P1.coverGridConfig.edge_point_on_line The points on the three edges of a coverGridConfig are on their edge lines line 756 source
Source documentation
The points on the three edges of a coverGridConfig are on their edge lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridConfig, Fin, OfNat.ofNat, Nat, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Membership.mem, Imo2025P1.Plane, Imo2025P1.AffSubOfPlane, Real, ENNReal, Imo2025P1.coverGridConfig.edgeLine, Imo2025P1.coverGridConfig.edgePoint
Proof uses: List, List.Mem, Eq, List.finRange, HEq, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Eq.mpr, HAdd.hAdd, HMul.hMul, Neg.neg, id, of_eq_true and 67 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridConfig.edge_point_on_line (C : coverGridConfig) (d : Fin 3) (i : Fin C.n) :
    C.edgePoint d i ∈ C.edgeLine d := by
…
```
Mentions: Imo2025P1.coverGridConfig
def Imo2025P1.coverGridConfig.findLineEdge coverGridConfig.findLineEdge chooses a line in lines that goes through C.edgePoint d i using the function coverGridConfig.findLine line 766 source
Source documentation
coverGridConfig.findLineEdge chooses a line in lines that goes through C.edgePoint d i using the function coverGridConfig.findLine.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridConfig, Fin, OfNat.ofNat, Nat, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.AffSubOfPlane
Proof uses: Imo2025P1.coverGridConfig.findLine, Imo2025P1.coverGridConfig.edgePoint, Imo2025P1.coverGridConfig.edge_point_in_grid
2 instances, coercions and auxiliary constants left out.
```
noncomputable def coverGridConfig.findLineEdge (C : coverGridConfig) (d : Fin 3) (i : Fin C.n) :=
…
```
Mentions: Imo2025P1.coverGridConfig
lemma Imo2025P1.coverGridConfig.find_line_edge_correct coverGridConfig.findLineEdge chooses a line in lines that goes through C.edgePoint d i line 770 source
Source documentation
coverGridConfig.findLineEdge chooses a line in lines that goes through C.edgePoint d i

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridConfig, Fin, OfNat.ofNat, Nat, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, And, Membership.mem, Imo2025P1.AffSubOfPlane, Finset, Imo2025P1.coverConfig.lines, Imo2025P1.coverGridConfig.findLineEdge, Imo2025P1.Plane, Real, ENNReal, Imo2025P1.coverGridConfig.edgePoint
Proof uses: Eq.mpr, Imo2025P1.coverGridConfig.findLine, Imo2025P1.coverGridConfig.edge_point_in_grid, id, Eq, congrArg, Imo2025P1.coverGridConfig.findLineEdge.eq_1, Imo2025P1.coverGridConfig.find_line_correct
58 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridConfig.find_line_edge_correct (C : coverGridConfig) (d : Fin 3) (i : Fin C.n) :
    C.findLineEdge d i ∈ C.lines ∧ C.edgePoint d i ∈ C.findLineEdge d i := by
…
```
Mentions: Imo2025P1.coverGridConfig
structure Imo2025P1.coverGridNoEdgeConfig A coverGridConfig with the additional requirements that n > 1 and lines doesn't contain an edge line 777 source
Source documentation
A coverGridConfig with the additional requirements that n > 1 and lines doesn't contain an edge. Note: we need n > 1 to have three corners in the grid.

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure coverGridNoEdgeConfig extends coverGridConfig where
…
```
Mentions: Imo2025P1.coverGridConfig
lemma Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_line_inj If lines does not contain an edge line of grid n, then on every edge, the lines chosen by findLineEdge are distinct line 785 source
Source documentation
If lines does not contain an edge line of grid n, then on every edge, the lines chosen by findLineEdge are distinct.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, Fin, OfNat.ofNat, Nat, Function.Injective, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig, Imo2025P1.AffSubOfPlane, Imo2025P1.coverGridConfig.findLineEdge
Proof uses: id, Eq, Decidable.byContradiction, Not, Membership.mem, Finset, Imo2025P1.coverConfig.lines, Imo2025P1.edgeLine, Imo2025P1.Plane, Imo2025P1.coverGridConfig.edgePoint, Imo2025P1.coverGridConfig.find_same_line, Imo2025P1.coverGridConfig.edge_point_in_grid, Imo2025P1.LineCoeffs.a, Imo2025P1.edgeCoeffs, Imo2025P1.LineCoeffs.b, Imo2025P1.LineCoeffs.c, Ne, List, List.Mem, List.finRange and 48 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridNoEdgeConfig.cover_no_edge_line_inj (C : coverGridNoEdgeConfig) (d : Fin 3) :
    Function.Injective (C.findLineEdge d) := by
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig
lemma Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_line_surj If lines does not contain an edge line of grid n, then for every edge, every line in lines must be chosen by a point on that edge line 807 source
Source documentation
If lines does not contain an edge line of grid n, then for every edge, every line in lines must be chosen by a point on that edge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, Fin, OfNat.ofNat, Nat, Eq, Finset, Imo2025P1.AffSubOfPlane, Finset.map, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig, Function.Embedding.mk, Imo2025P1.coverGridConfig.findLineEdge, Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_line_inj, Finset.univ, Imo2025P1.coverConfig.lines
Proof uses: Eq.mpr, id, congrArg, rfl, Finset.card, of_eq_true, Eq.trans, True, congrFun', Finset.card_map, Fintype.card_fin, eq_self, LE.le, Membership.mem, Exists, Eq.mp, And, Function.Embedding, funext, true_and and 5 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridNoEdgeConfig.cover_no_edge_line_surj (C : coverGridNoEdgeConfig) (d : Fin 3) :
    Finset.map
      ⟨ C.findLineEdge d,
        C.cover_no_edge_line_inj d⟩
      Finset.univ = C.lines := by
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig
def Imo2025P1.edgeEndpointCornerId line 828 source
standard axioms: propext what this means
Statement uses: Fin, OfNat.ofNat, Nat
Proof uses: Imo2025P1.edgeEndpointCornerId.match_1, Unit
4 instances, coercions and auxiliary constants left out.
def Imo2025P1.coverGridNoEdgeConfig.edgeEndpointIndex line 836 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, Fin, OfNat.ofNat, Nat, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig
Proof uses: Imo2025P1.coverGridNoEdgeConfig.edgeEndpointIndex.match_1, Unit, Fin.mk, HSub.hSub
6 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Imo2025P1.coverGridNoEdgeConfig.cornerPoint The points on the three corners of grid n line 842 source
Source documentation
The points on the three corners of grid n

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, Fin, OfNat.ofNat, Nat, Imo2025P1.Plane
Proof uses: Imo2025P1.edgeCoeffs.match_1, Unit, Imo2025P1.coverGridConfig.edgePoint, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig, Imo2025P1.coverGridNoEdgeConfig.edgeEndpointIndex
5 instances, coercions and auxiliary constants left out.
```
def coverGridNoEdgeConfig.cornerPoint (C : coverGridNoEdgeConfig) (c : Fin 3) : Plane :=
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig, Imo2025P1.Plane
lemma Imo2025P1.coverGridNoEdgeConfig.corner_point_on_edge Every corner of grid n belongs to two edgle lines line 849 source
Source documentation
Every corner of grid n belongs to two edgle lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, Fin, OfNat.ofNat, Nat, Eq, Imo2025P1.Plane, Imo2025P1.coverGridNoEdgeConfig.cornerPoint, Imo2025P1.edgeEndpointCornerId, Imo2025P1.coverGridConfig.edgePoint, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig, Imo2025P1.coverGridNoEdgeConfig.edgeEndpointIndex
Proof uses: id, Real, HAdd.hAdd, HSub.hSub, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.n_minus_plus, Imo2025P1.coverGridNoEdgeConfig.hn, eq_sub_of_add_eq', List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, Imo2025P1.edgeCoeffs.match_1, Imo2025P1.edgeEndpointCornerId.match_1, Unit and 36 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridNoEdgeConfig.corner_point_on_edge (C : coverGridNoEdgeConfig)
  (d : Fin 3) (r : Fin 2) :
    C.cornerPoint (edgeEndpointCornerId d r) = C.edgePoint d (C.edgeEndpointIndex r) := by
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig, Imo2025P1.edgeEndpointCornerId
def Imo2025P1.coverGridNoEdgeConfig.findLineCorner coverGridNoEdgeConfig.findLineCorner C c chooses a line in lines that goes through C.cornerPoint c using the function findLine line 860 source
Source documentation
coverGridNoEdgeConfig.findLineCorner C c chooses a line in lines that goes through C.cornerPoint c using the function findLine.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, Fin, OfNat.ofNat, Nat, Imo2025P1.AffSubOfPlane
Proof uses: Imo2025P1.edgeCoeffs.match_1, Unit, Imo2025P1.coverGridConfig.findLineEdge, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig, Imo2025P1.coverGridNoEdgeConfig.edgeEndpointIndex
5 instances, coercions and auxiliary constants left out.
```
noncomputable def coverGridNoEdgeConfig.findLineCorner (C : coverGridNoEdgeConfig)
  (c : Fin 3) := match c with
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig
lemma Imo2025P1.coverGridNoEdgeConfig.find_line_corner_correct coverGridNoEdgeConfig.findLineCorner C c chooses a line in lines that goes through C.cornerPoint c line 868 source
Source documentation
coverGridNoEdgeConfig.findLineCorner C c chooses a line in lines that goes through C.cornerPoint c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, Fin, OfNat.ofNat, Nat, And, Membership.mem, Imo2025P1.AffSubOfPlane, Finset, Imo2025P1.coverConfig.lines, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig, Imo2025P1.coverGridNoEdgeConfig.findLineCorner, Imo2025P1.Plane, Real, ENNReal, Imo2025P1.coverGridNoEdgeConfig.cornerPoint
Proof uses: List, List.Mem, Eq, List.finRange, HEq, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, id, Imo2025P1.coverGridConfig.find_line_edge_correct, Imo2025P1.coverGridNoEdgeConfig.edgeEndpointIndex, eq_of_heq, List.Mem.tail, False.elim, noConfusion_of_Nat and 3 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridNoEdgeConfig.find_line_corner_correct (C : coverGridNoEdgeConfig)
  (c : Fin 3) :
    C.findLineCorner c ∈ C.lines ∧
    C.cornerPoint c ∈ C.findLineCorner c := by
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig
lemma Imo2025P1.coverGridNoEdgeConfig.find_line_corner_eq_edge The line chosen by findLineCorner at each of the three corners equals to the line chosen by findLineEdge at corresponding points on two edge lines line 877 source
Source documentation
The line chosen by findLineCorner at each of the three corners equals to the line chosen by findLineEdge at corresponding points on two edge lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, Fin, OfNat.ofNat, Nat, Eq, Imo2025P1.AffSubOfPlane, Imo2025P1.coverGridNoEdgeConfig.findLineCorner, Imo2025P1.edgeEndpointCornerId, Imo2025P1.coverGridConfig.findLineEdge, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig, Imo2025P1.coverGridNoEdgeConfig.edgeEndpointIndex
Proof uses: id, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, Imo2025P1.edgeCoeffs.match_1, Imo2025P1.edgeEndpointCornerId.match_1, Unit, Imo2025P1.coverGridConfig.findLine, Imo2025P1.coverGridConfig.edgePoint, Imo2025P1.coverGridConfig.edge_point_in_grid, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl and 19 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridNoEdgeConfig.find_line_corner_eq_edge (C : coverGridNoEdgeConfig)
  (d : Fin 3) (r : Fin 2) :
    C.findLineCorner (edgeEndpointCornerId d r) = C.findLineEdge d (C.edgeEndpointIndex r) := by
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig, Imo2025P1.edgeEndpointCornerId
lemma Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_corner_distinct The three points chosen by findLineCorner are distinct line 888 source
Source documentation
The three points chosen by findLineCorner are distinct.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, And, Ne, Imo2025P1.AffSubOfPlane, Imo2025P1.coverGridNoEdgeConfig.findLineCorner, OfNat.ofNat, Fin, Nat
Proof uses: Imo2025P1.edgeEndpointCornerId, Eq.mpr, Imo2025P1.coverGridConfig.findLineEdge, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig, Imo2025P1.coverGridNoEdgeConfig.edgeEndpointIndex, id, Eq, congrArg, Imo2025P1.coverGridNoEdgeConfig.find_line_corner_eq_edge, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_line_inj, GT.gt, Imo2025P1.coverGridNoEdgeConfig.hn, Eq.mp, HSub.hSub, Fin.mk.injEq, And.intro
12 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridNoEdgeConfig.cover_no_edge_corner_distinct (C : coverGridNoEdgeConfig) :
    C.findLineCorner 0 ≠ C.findLineCorner 1 ∧
    C.findLineCorner 0 ≠ C.findLineCorner 2 ∧
    C.findLineCorner 1 ≠ C.findLineCorner 2 := by
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig
lemma Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_corner_inj findLineCorner is injective line 903 source
Source documentation
findLineCorner is injective.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, Function.Injective, Fin, OfNat.ofNat, Nat, Imo2025P1.AffSubOfPlane, Imo2025P1.coverGridNoEdgeConfig.findLineCorner
Proof uses: And, Ne, Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_corner_distinct, Eq, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Eq.refl, eq_of_heq and 7 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridNoEdgeConfig.cover_no_edge_corner_inj (C : coverGridNoEdgeConfig) :
    Function.Injective C.findLineCorner := by
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig
def Imo2025P1.coverGridNoEdgeConfig.corner_set The image set of findLineCorner line 910 source
Source documentation
The image set of findLineCorner.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, Finset, Imo2025P1.AffSubOfPlane
Proof uses: Finset.map, Fin, OfNat.ofNat, Nat, Function.Embedding.mk, Imo2025P1.coverGridNoEdgeConfig.findLineCorner, Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_corner_inj, Finset.univ
2 instances, coercions and auxiliary constants left out.
```
noncomputable def coverGridNoEdgeConfig.corner_set (C : coverGridNoEdgeConfig) :
    Finset AffSubOfPlane :=
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig, Imo2025P1.AffSubOfPlane
lemma Imo2025P1.coverGridNoEdgeConfig.corner_set_members The members of the corner_set, i.e., The image set of findLineCorner line 915 source
Source documentation
The members of the corner_set, i.e., The image set of findLineCorner

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, Fin, OfNat.ofNat, Nat, Membership.mem, Imo2025P1.AffSubOfPlane, Finset, Imo2025P1.coverGridNoEdgeConfig.corner_set, Imo2025P1.coverGridNoEdgeConfig.findLineCorner
Proof uses: of_eq_true, Finset.map, Function.Embedding.mk, Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_corner_inj, Finset.univ, Eq.trans, True
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridNoEdgeConfig.corner_set_members (C : coverGridNoEdgeConfig) (d : Fin 3) :
    C.findLineCorner d ∈ C.corner_set := by
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig
lemma Imo2025P1.coverGridNoEdgeConfig.corner_set_card The cardinality of the corner_set, i.e., The image set of findLineCorner line 920 source
Source documentation
The cardinality of the corner_set, i.e., The image set of findLineCorner

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, Eq, Nat, Finset.card, Imo2025P1.AffSubOfPlane, Imo2025P1.coverGridNoEdgeConfig.corner_set, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.map, Fin, Function.Embedding.mk, Imo2025P1.coverGridNoEdgeConfig.findLineCorner, Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_corner_inj, Finset.univ, Finset.card_map, Fintype.card_fin, eq_self
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridNoEdgeConfig.corner_set_card (C : coverGridNoEdgeConfig) :
    #C.corner_set = 3 := by
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig
lemma Imo2025P1.coverGridNoEdgeConfig.corner_set_subset_lines corner_set (i.e., The image set of findLineCorner) is a subset of lines line 925 source
Source documentation
corner_set (i.e., The image set of findLineCorner) is a subset of lines

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, LE.le, Finset, Imo2025P1.AffSubOfPlane, Imo2025P1.coverGridNoEdgeConfig.corner_set, Imo2025P1.coverConfig.lines, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig
Proof uses: Eq.mpr, Membership.mem, Fin, OfNat.ofNat, Nat, Eq, Imo2025P1.coverGridNoEdgeConfig.findLineCorner, id, Eq.trans, Finset.map, Function.Embedding.mk, Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_corner_inj, Finset.univ, Exists, implies_congr, And, Function.Embedding, congrArg, funext, True and 10 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridNoEdgeConfig.corner_set_subset_lines (C : coverGridNoEdgeConfig) :
    C.corner_set ⊆ C.lines := by
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig
lemma Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_3_lines If a coverGridNoEdgeConfig has n = 3, then nS = 3 line 935 source
Source documentation
If a coverGridNoEdgeConfig has n = 3, then nS = 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, Eq, Nat, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig, OfNat.ofNat, Imo2025P1.coverConfig.nS
Proof uses: Finset, Imo2025P1.AffSubOfPlane, Imo2025P1.coverGridNoEdgeConfig.corner_set, Imo2025P1.coverConfig.lines, Finset.eq_of_subset_of_card_le, Imo2025P1.coverGridNoEdgeConfig.corner_set_subset_lines, Eq.mpr, LE.le, Finset.card, id, congrArg, Imo2025P1.coverConfig.lines_count, Imo2025P1.coverGridNoEdgeConfig.corner_set_card, le_refl, Fin, Imo2025P1.edgeCoeffs.match_1, Unit, Imo2025P1.coverGridConfig.findLineEdge, Fin.mk, Imo2025P1.coverGridNoEdgeConfig.findLineCorner and 91 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 78 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridNoEdgeConfig.cover_no_edge_3_lines (C : coverGridNoEdgeConfig)
    (hn3 : C.n = 3) : C.nS = 3 := by
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig
lemma Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_4_impossible It is impossible to have a coverGridNoEdgeConfig with n ≥ 4 line 995 source
Source documentation
It is impossible to have a coverGridNoEdgeConfig with n ≥ 4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, GE.ge, Nat, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig, OfNat.ofNat, False
Proof uses: DecidableEq, Imo2025P1.AffSubOfPlane, Imo2025P1.eqAffSubOfPlane, LE.le, Finset.card, SDiff.sdiff, Finset, Imo2025P1.coverConfig.lines, Imo2025P1.coverGridNoEdgeConfig.corner_set, Trans.trans, Eq, HSub.hSub, rfl, Eq.mpr, id, congrArg, Imo2025P1.coverConfig.lines_count, Imo2025P1.coverGridNoEdgeConfig.corner_set_card, le_refl, Eq.symm and 63 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridNoEdgeConfig.cover_no_edge_4_impossible (C : coverGridNoEdgeConfig)
    (hn4 : C.n ≥ 4) : False := by
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig
lemma Imo2025P1.coverGridNoEdgeConfig.cover_edge A coverGridNoEdgeConfig must satisfy n = 3 ∧ nS = 3 line 1060 source
Source documentation
A coverGridNoEdgeConfig must satisfy n = 3 ∧ nS = 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridNoEdgeConfig, And, Eq, Nat, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig, OfNat.ofNat, Imo2025P1.coverConfig.nS
Proof uses: GE.ge, Trans.trans, Finset.card, Imo2025P1.AffSubOfPlane, Imo2025P1.coverGridNoEdgeConfig.corner_set, Imo2025P1.coverConfig.lines, Eq.symm, Imo2025P1.coverConfig.lines_count, Finset.card_le_card, Imo2025P1.coverGridNoEdgeConfig.corner_set_subset_lines, Imo2025P1.coverGridNoEdgeConfig.corner_set_card, dite, Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_3_lines, Not, Or, Decidable.not_or_of_imp, False.elim, And.intro, False, Imo2025P1.coverGridNoEdgeConfig.cover_no_edge_4_impossible
8 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridNoEdgeConfig.cover_edge (C : coverGridNoEdgeConfig) : C.n = 3 ∧ C.nS = 3 := by
…
```
Mentions: Imo2025P1.coverGridNoEdgeConfig
lemma Imo2025P1.coverGridConfig.any_cover A coverGridNoEdgeConfig must satisfy nS ≤ n and nS ∈ {0, 1, 3} line 1074 source
Source documentation
A coverGridNoEdgeConfig must satisfy nS ≤ n and nS ∈ {0, 1, 3}. Proved by induction on n of the above fact for all coverGridNoEdgeConfig.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.coverGridConfig, And, LE.le, Nat, Imo2025P1.coverConfig.nS, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.coverConfig.n, Or, Eq, OfNat.ofNat
Proof uses: Nat.recAux, Imo2025P1.coverConfig.nS_leq_n, HAdd.hAdd, dite, Not, Exists, Fin, Membership.mem, Imo2025P1.AffSubOfPlane, Finset, Imo2025P1.coverConfig.lines, Imo2025P1.coverGridConfig.edgeLine, Classical.propDecidable, Imo2025P1.reduce, HSub.hSub, Imo2025P1.coverGridConfig.reduce_count, Imo2025P1.coverGridNoEdgeConfig, Imo2025P1.coverGridNoEdgeConfig.mk, Eq.mp, Imo2025P1.coverGridNoEdgeConfig.tocoverGridConfig and 2 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma coverGridConfig.any_cover (C : coverGridConfig) :
    (C.nS ≤ C.n ∧ (C.nS = 0 ∨ C.nS = 1 ∨ C.nS = 3)) := by
…
```
Mentions: Imo2025P1.coverGridConfig
structure Imo2025P1.strongCoverGridConfig A coverGridConfig with the additional requirements every line in lines goes through at least one point in g line 1102 source
Source documentation
A coverGridConfig with the additional requirements every line in lines goes through at least one point in g. This is used to inductively construct covers of grid n with exactly 0, 1, or 3 sunny lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure strongCoverGridConfig extends coverGridConfig where
…
```
Mentions: Imo2025P1.coverGridConfig
def Imo2025P1.zeroSunny A strongCoverGridConfig with n = 0 and nS = 0 line 1106 source
Source documentation
A strongCoverGridConfig with n = 0 and nS = 0

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.strongCoverGridConfig
Proof uses: Imo2025P1.strongCoverGridConfig.mk, Imo2025P1.coverGridConfig.mk, Imo2025P1.coverConfig.mk, EmptyCollection.emptyCollection, Finset, Imo2025P1.AffSubOfPlane, Set, Imo2025P1.Plane, OfNat.ofNat, Nat
9 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
def zeroSunny : strongCoverGridConfig where
…
```
Mentions: Imo2025P1.strongCoverGridConfig
def Imo2025P1.oneSunny A strongCoverGridConfig with n = 1 and nS = 1 line 1124 source
Source documentation
A strongCoverGridConfig with n = 1 and nS = 1

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.strongCoverGridConfig
Proof uses: Imo2025P1.strongCoverGridConfig.mk, Imo2025P1.coverGridConfig.mk, Imo2025P1.coverConfig.mk, Singleton.singleton, Imo2025P1.AffSubOfPlane, Finset, Imo2025P1.line, Neg.neg, Real, OfNat.ofNat, Imo2025P1.grid, Nat
13 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
noncomputable def oneSunny : strongCoverGridConfig where
…
```
Mentions: Imo2025P1.strongCoverGridConfig
def Imo2025P1.threeSunnyLineCoeffs The LineCoeffs of a 3 sunny solution line 1156 source
Source documentation
The LineCoeffs of a 3 sunny solution

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Imo2025P1.LineCoeffs
Proof uses: Imo2025P1.edgeCoeffs.match_1, Unit, Imo2025P1.LineCoeffs.mk, Neg.neg, Real
11 instances, coercions and auxiliary constants left out.
```
def threeSunnyLineCoeffs : Fin 3 → LineCoeffs
  | 0 => ⟨-1, 1, 0⟩
  | 1 => ⟨2, 1, -5⟩
  | 2 => ⟨1, 2, -5⟩

/-- The lines of a 3 sunny solution -/
```
Mentions: Imo2025P1.LineCoeffs, solution
def Imo2025P1.threeSunnyLine The lines of a 3 sunny solution line 1162 source
Source documentation
The lines of a 3 sunny solution

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Imo2025P1.AffSubOfPlane
Proof uses: Imo2025P1.line', Imo2025P1.threeSunnyLineCoeffs
2 instances, coercions and auxiliary constants left out.
```
noncomputable def threeSunnyLine (d : Fin 3) := line' (threeSunnyLineCoeffs d)
```
Mentions: Imo2025P1.line', Imo2025P1.threeSunnyLineCoeffs
lemma Imo2025P1.threeSunnyLineInj The lines of a 3 sunny solution are distinct line 1165 source
Source documentation
The lines of a 3 sunny solution are distinct.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Fin, OfNat.ofNat, Nat, Imo2025P1.AffSubOfPlane, Imo2025P1.threeSunnyLine
Proof uses: Eq, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Eq.refl, eq_of_heq, List.Mem.tail, Eq.mpr, False and 43 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma threeSunnyLineInj : Function.Injective threeSunnyLine := by
…
```
Mentions: Imo2025P1.threeSunnyLine
def Imo2025P1.threeSunnyLines The set of lines of a 3 sunny solution line 1177 source
Source documentation
The set of lines of a 3 sunny solution

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2025P1.AffSubOfPlane
Proof uses: Finset.map, Fin, OfNat.ofNat, Nat, Function.Embedding.mk, Imo2025P1.threeSunnyLine, Imo2025P1.threeSunnyLineInj, Finset.univ
2 instances, coercions and auxiliary constants left out.
```
noncomputable def threeSunnyLines :=
…
```
lemma Imo2025P1.threeSunnyLinesMem The members of the set of lines of a 3 sunny solution line 1181 source
Source documentation
The members of the set of lines of a 3 sunny solution

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.AffSubOfPlane, Iff, Membership.mem, Finset, Imo2025P1.threeSunnyLines, Or, Eq, Imo2025P1.threeSunnyLine, OfNat.ofNat, Fin, Nat
Proof uses: Eq.mpr, Exists, id, congrFun', congrArg, Eq.trans, Finset.map, Function.Embedding.mk, Imo2025P1.threeSunnyLineInj, Finset.univ, And, Function.Embedding, funext, True, true_and, Iff.intro, List, List.Mem, List.finRange, HEq and 21 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma threeSunnyLinesMem (L : AffSubOfPlane) : L ∈ threeSunnyLines ↔
    (L = threeSunnyLine 0) ∨ (L = threeSunnyLine 1) ∨ (L = threeSunnyLine 2) := by
…
```
Mentions: Imo2025P1.AffSubOfPlane, Imo2025P1.threeSunnyLines, Imo2025P1.threeSunnyLine
lemma Imo2025P1.grid3Points The points in grid 3 line 1190 source
Source documentation
The points in grid 3

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.Plane, Iff, Membership.mem, Set, Imo2025P1.grid, OfNat.ofNat, Nat, Or, Eq, WithLp.toLp, ENNReal, Fin, Real, Matrix.vecCons, Matrix.vecEmpty
Proof uses: Eq.mpr, Exists, And, WithLp.ofLp, LT.lt, LE.le, HAdd.hAdd, id, congrFun', congrArg, Set.ofPred, funext, Iff.intro, Imo2025P1.vec_repr, WithLp, propext, Imo2025P1.vec_eq, Eq.trans, congr, Eq.symm and 17 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma grid3Points (x : Plane) : x ∈ grid 3 ↔
    (x = !₂[1, 1] ∨ x = !₂[1, 2] ∨ x = !₂[1, 3] ∨
     x = !₂[2, 1] ∨ x = !₂[2, 2] ∨ x = !₂[3, 1]) := by
…
```
Mentions: Imo2025P1.Plane, Imo2025P1.grid
def Imo2025P1.threeSunny A strongCoverGridConfig with n = 3 and nS = 3 line 1209 source
Source documentation
A strongCoverGridConfig with n = 3 and nS = 3

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.strongCoverGridConfig
Proof uses: Imo2025P1.strongCoverGridConfig.mk, Imo2025P1.coverGridConfig.mk, Imo2025P1.coverConfig.mk, Imo2025P1.threeSunnyLines, Imo2025P1.grid, OfNat.ofNat, Nat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
noncomputable def threeSunny : strongCoverGridConfig where
…
```
Mentions: Imo2025P1.strongCoverGridConfig
def Imo2025P1.strongCoverGridConfig.extend Add a diagonal line x + y = n + 2 to a countAndStrongCover line 1254 source
Source documentation
Add a diagonal line x + y = n + 2 to a countAndStrongCover

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P1.strongCoverGridConfig
Proof uses: Imo2025P1.strongCoverGridConfig.mk, Imo2025P1.coverGridConfig.mk, Imo2025P1.coverConfig.mk, Finset.cons, Imo2025P1.AffSubOfPlane, Imo2025P1.edgeLine, HAdd.hAdd, Nat, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.strongCoverGridConfig.tocoverGridConfig, OfNat.ofNat, Fin, Imo2025P1.coverConfig.lines, Imo2025P1.strongCoverGridConfig.extend.hNew, Imo2025P1.grid, Imo2025P1.coverConfig.nS
11 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
noncomputable def strongCoverGridConfig.extend (C : strongCoverGridConfig) :
    strongCoverGridConfig where
…
```
Mentions: Imo2025P1.strongCoverGridConfig
lemma Imo2025P1.existsStrongCover It is possible to have a strongCoverGridConfig, whenever nS ≤ n and nS = 0 ∨ nS = 1 ∨ nS = 3 line 1316 source
Source documentation
It is possible to have a strongCoverGridConfig, whenever nS ≤ n and nS = 0 ∨ nS = 1 ∨ nS = 3

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Or, Eq, OfNat.ofNat, Exists, Imo2025P1.strongCoverGridConfig, And, Imo2025P1.coverConfig.n, Imo2025P1.coverGridConfig.tocoverConfig, Imo2025P1.strongCoverGridConfig.tocoverGridConfig, Imo2025P1.coverConfig.nS
Proof uses: Nat.recAux, Exists.intro, Imo2025P1.zeroSunny, Eq.mpr, id, Eq.trans, True, congrFun', congrArg, eq_self, true_and, HAdd.hAdd, dite, Imo2025P1.strongCoverGridConfig.extend, Not, Eq.symm, of_eq_true, congr, and_self, Imo2025P1.oneSunny and 1 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma existsStrongCover (n nS : ℕ) :
    nS ≤ n → (nS = 0 ∨ nS = 1 ∨ nS = 3) →
    ∃ (C : strongCoverGridConfig), C.n = n ∧ C.nS = nS := by
…
```
Mentions: Imo2025P1.strongCoverGridConfig
determine Imo2025P1.answer line 1340 source
no axioms what this means
Statement uses: Nat, Set.Ici, OfNat.ofNat, Set
Proof uses: Insert.insert, Singleton.singleton
8 instances, coercions and auxiliary constants left out.
problem Imo2025P1.imo2025_p1 The final theorem: answer is {0, 1, 3} line 1343 source
Source documentation
The final theorem: answer is {0, 1, 3}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.Ici, OfNat.ofNat, Eq, Set, Set.ofPred, Exists, Finset, AffineSubspace, Real, EuclideanSpace, Fin, ENNReal, DecidablePred, Imo2025P1.Sunny, Imo2025P1.sunnyPred, And, Finset.card, Membership.mem, Module.finrank and 12 more
Proof uses: id, Set.ext, Insert.insert, Singleton.singleton, Eq.mpr, Iff, Or, congrArg, Eq.trans, Iff.intro, Imo2025P1.coverGridConfig, Imo2025P1.coverGridConfig.mk, Imo2025P1.coverConfig.mk, Imo2025P1.grid, Imo2025P1.Plane, WithLp.ofLp, Imo2025P1.AffSubOfPlane, Eq.mp, congrFun', funext and 28 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
problem imo2025_p1 (n : Set.Ici 3) :
    {k | ∃ lines : Finset (AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2))),
      have := sunnyPred;
…
```
Mentions: Imo2025P1.sunnyPred