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

69 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2017, Problem 3

A hunter and an invisible rabbit play a game in the Euclidean plane. The rabbit's starting point, A₀, and the hunter's starting point, B₀, are the same. After n − 1 rounds of the game, the rabbit is at point A_{n−1} and the hunter is at point B_{n−1}. In the n-th round of the game, three things occur in order:

(i) The rabbit moves invisibly to a point Aₙ such that the distance between A_{n−1} and Aₙ is exactly 1. (ii) A tracking device reports a point Pₙ to the hunter. The only guarantee provided by the tracking device to the hunter is that the distance between Pₙ and Aₙ is at most 1. (iii) The hunter moves visibly to a point Bₙ such that the distance between B_{n−1} and Bₙ is exactly 1.

Is it always possible, no matter how the rabbit moves, and no matter what points are reported by the tracking device, for the hunter to choose her moves so that after 10⁹ rounds she can ensure that the distance between her and the rabbit is at most 100?

Imports (10)

Imported by 1 file

Compfiles.lean

abbrev Imo2017P3.Pt Points of the Euclidean plane line 55 source
Source documentation
Points of the Euclidean 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 Pt := EuclideanSpace ℝ (Fin 2)
```
def Imo2017P3.totalRounds The number of rounds in the game line 58 source
Source documentation
The number of rounds in the game.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: HPow.hPow, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def totalRounds : ℕ := 10 ^ 9
```
abbrev Imo2017P3.Strategy A hunter strategy: given the list of points reported by the tracking device in rounds 1, ..., n (in chronological order), choose the hunter's position Bₙ line 64 source
Source documentation
A hunter strategy: given the list of points reported by the tracking device in rounds 1, ..., n (in chronological order), choose the hunter's position Bₙ. The hunter's move may depend only on the reported points, not on the rabbit's actual positions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: List, Imo2017P3.Pt
```
abbrev Strategy := List Pt → Pt
```
Mentions: Imo2017P3.Pt
def Imo2017P3.ValidStrategy A strategy is valid if the hunter starts at the common starting point 0 and moves by exactly 1 in every round, whatever is reported line 68 source
Source documentation
A strategy is valid if the hunter starts at the common starting point 0 and moves by exactly 1 in every round, whatever is reported.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy
Proof uses: And, Eq, Imo2017P3.Pt, List.nil, OfNat.ofNat, ENNReal, Fin, Nat, Real, List, Dist.dist, HAppend.hAppend, List.cons
23 instances, coercions and auxiliary constants left out.
```
def ValidStrategy (σ : Strategy) : Prop :=
…
```
Mentions: Imo2017P3.Strategy
def Imo2017P3.reportList The reports made in rounds 1, ..., n, as a list in chronological order line 72 source
Source documentation
The reports made in rounds 1, ..., n, as a list in chronological order.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2017P3.Pt, List
2 instances, coercions and auxiliary constants left out.
```
def reportList (p : ℕ → Pt) : ℕ → List Pt
  | 0 => []
  | (n + 1) => reportList p n ++ [p (n + 1)]

/-- The hunter's position after round `n` when using strategy `σ` against
the reported points `p 1, ..., p n`. -/
```
Mentions: Imo2017P3.Pt
def Imo2017P3.hunterPos The hunter's position after round n when using strategy σ against the reported points p 1, ..., p n line 78 source
Source documentation
The hunter's position after round n when using strategy σ against the reported points p 1, ..., p n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Nat, Imo2017P3.Pt
Proof uses: Imo2017P3.reportList
```
def hunterPos (σ : Strategy) (p : ℕ → Pt) (n : ℕ) : Pt := σ (reportList p n)
```
Mentions: Imo2017P3.Strategy, Imo2017P3.Pt, Imo2017P3.reportList
def Imo2017P3.ValidRabbit A rabbit path is valid if it starts at the common starting point 0 and moves by exactly 1 in every round line 82 source
Source documentation
A rabbit path is valid if it starts at the common starting point 0 and moves by exactly 1 in every round.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2017P3.Pt
Proof uses: And, Eq, OfNat.ofNat, ENNReal, Fin, Real, Dist.dist, HAdd.hAdd
23 instances, coercions and auxiliary constants left out.
```
def ValidRabbit (A : ℕ → Pt) : Prop :=
…
```
Mentions: Imo2017P3.Pt
def Imo2017P3.ValidReports The reported points are valid for a rabbit path if each report is within distance 1 of the rabbit's actual position line 87 source
Source documentation
The reported points are valid for a rabbit path if each report is within distance 1 of the rabbit's actual position.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2017P3.Pt
Proof uses: LE.le, OfNat.ofNat, Real, Dist.dist, ENNReal, Fin
14 instances, coercions and auxiliary constants left out.
```
def ValidReports (A p : ℕ → Pt) : Prop :=
…
```
Mentions: Imo2017P3.Pt
lemma Imo2017P3.norm_sq_frame Pythagoras in an orthonormal frame line 109 source
Source documentation
Pythagoras in an orthonormal frame.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, Eq, Norm.norm, OfNat.ofNat, ENNReal, Fin, Nat, Inner.inner, And, HPow.hPow, HAdd.hAdd, HSMul.hSMul, HSub.hSub
Proof uses: Eq.mpr, HMul.hMul, id, congrArg, norm_smul, abs, Real.norm_eq_abs, mul_one, sq_abs, Eq.refl, real_inner_smul_left, MulZeroClass.mul_zero, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Meta.NormNum.one_natPow, And.intro, norm_add_sq_real, Mathlib.Tactic.Ring.of_eq and 32 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma norm_sq_frame (u w : Pt) (s : ℝ) (hu : ‖u‖ = 1) (hw : ‖w‖ = 1)
    (huw : ⟪u, w⟫_ℝ = 0) :
    ‖s • u + w‖ ^ 2 = s ^ 2 + 1 ∧ ‖s • u - w‖ ^ 2 = s ^ 2 + 1 := by
…
```
Mentions: Imo2017P3.Pt
lemma Imo2017P3.core_ineq The analytic heart of the phase lemma: with n ≥ 4d steps, the squared distance grows by at least 1/2 line 122 source
Source documentation
The analytic heart of the phase lemma: with n ≥ 4d steps, the squared distance grows by at least 1/2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, HMul.hMul, Nat, HSub.hSub, HDiv.hDiv, HAdd.hAdd, HPow.hPow
Proof uses: LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.isInt_neg and 143 more
163 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma core_ineq (n d h₁ h₂ s : ℝ) (hn : 1 ≤ n) (hd : 0 ≤ d) (hnd : 4 * d ≤ n)
    (hs : n - 1 / n ≤ s) (_hs' : s ≤ n) (hH : (h₁ + d) ^ 2 + h₂ ^ 2 ≤ n ^ 2) :
    d ^ 2 + 1 / 2 ≤ (h₁ - s) ^ 2 + h₂ ^ 2 + 1 := by
…
```
lemma Imo2017P3.frame_exists An orthonormal frame adapted to the pair (a, b): u points from b to a line 153 source
Source documentation
An orthonormal frame adapted to the pair (a, b): u points from b to a.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Exists, And, Eq, Real, Norm.norm, OfNat.ofNat, ENNReal, Fin, Nat, Inner.inner, HAdd.hAdd, HSMul.hSMul, HSub.hSub, Dist.dist
Proof uses: HMul.hMul, WithLp.ofLp, Eq.mpr, Finset.sum, Finset.univ, id, congrArg, PiLp, PiLp.inner_apply, Fin.sum_univ_two, of_eq_true, Eq.trans, True, congrFun', congr, RingHom, starRingEnd, Real.ringHom_apply, mul_comm, eq_self and 119 more
238 instances, coercions and auxiliary constants left out.

Tactic trace: 77 steps
Open to load the checked before-and-after goal states.
```
lemma frame_exists (a b : Pt) :
    ∃ u w : Pt, ‖u‖ = 1 ∧ ‖w‖ = 1 ∧ ⟪u, w⟫_ℝ = 0 ∧
      (∀ v : Pt, v = ⟪v, u⟫_ℝ • u + ⟪v, w⟫_ℝ • w) ∧ b = a - dist a b • u := by
…
```
Mentions: Imo2017P3.Pt
lemma Imo2017P3.phase_geom Phase lemma (geometry) line 218 source
Source documentation
Phase lemma (geometry). If the rabbit is at a, the hunter at b, and the rabbit runs for n ≥ 4 · dist a b rounds to one of the two points a + s • u ± w (with s ≈ n), while the device reports points on the line, then the hunter, wherever it goes within n steps of b, ends at distance at least √(dist a b² + 1/2) from one of the two points.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, Eq, Norm.norm, OfNat.ofNat, ENNReal, Fin, Nat, Inner.inner, HAdd.hAdd, HSMul.hSMul, HSub.hSub, Dist.dist, LE.le, HMul.hMul, HDiv.hDiv, Real.sqrt, HPow.hPow, Max.max
Proof uses: rfl, Eq.mpr, id, congrArg, norm_smul, abs, Real.norm_eq_abs, mul_one, sq_abs, Eq.refl, real_inner_smul_left, real_inner_smul_right, MulZeroClass.mul_zero, norm_add_sq_real, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.symm and 111 more
225 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma phase_geom (a b H : Pt) (u w : Pt) (n s : ℝ)
    (hu : ‖u‖ = 1) (hw : ‖w‖ = 1) (huw : ⟪u, w⟫_ℝ = 0)
    (hspan : ∀ v : Pt, v = ⟪v, u⟫_ℝ • u + ⟪v, w⟫_ℝ • w)
    (hb : b = a - dist a b • u)
    (hn : 1 ≤ n) (hnd : 4 * dist a b ≤ n)
    (hs : n - 1 / n ≤ s) (hs' : s ≤ n)
    (hH : dist b H ≤ n) :
    Real.sqrt (dist a b ^ 2 + 1 / 2) ≤
      max (dist H (a + s • u + w)) (dist H (a + s • u - w)) := by
…
```
Mentions: Imo2017P3.Pt
lemma Imo2017P3.sqrt_est Bounds for √(n² - 1) line 277 source
Source documentation
Bounds for √(n² - 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, And, HSub.hSub, HDiv.hDiv, Real.sqrt, HPow.hPow, Nat
Proof uses: LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, 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.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.neg_add and 109 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma sqrt_est (n : ℝ) (hn : 1 ≤ n) : n - 1 / n ≤ Real.sqrt (n ^ 2 - 1) ∧
    Real.sqrt (n ^ 2 - 1) ≤ n := by
…
```
def Imo2017P3.totalPhases Total number of phases: 20000 phases of 400 rounds, one phase of 3600 rounds, then maintenance phases of 400 rounds; in total exactly 10^9 rounds line 298 source
Source documentation
Total number of phases: 20000 phases of 400 rounds, one phase of 3600 rounds, then maintenance phases of 400 rounds; in total exactly 10^9 rounds.

no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
def totalPhases : ℕ := 2499992
```
def Imo2017P3.phaseLen The length of phase j line 301 source
Source documentation
The length of phase j.

no axioms what this means
Statement uses: Nat
Proof uses: ite, Eq, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
```
def phaseLen (j : ℕ) : ℕ := if j = 20000 then 3600 else 400
```
structure Imo2017P3.PState The state of the adversary's construction at the start of a phase: the rabbit's position a, the list L of reports made so far, and the phase index j line 306 source
Source documentation
The state of the adversary's construction at the start of a phase: the rabbit's position a, the list L of reports made so far, and the phase index j.

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure PState where
…
```
def Imo2017P3.maintSeq Running one maintenance round: the rabbit runs directly away from the hunter and the device reports the rabbit's position honestly line 313 source
Source documentation
Running one maintenance round: the rabbit runs directly away from the hunter and the device reports the rabbit's position honestly.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.Pt, List, Nat, Prod
2 instances, coercions and auxiliary constants left out.
```
def maintSeq (σ : Strategy) (a : Pt) (L : List Pt) : ℕ → Pt × List Pt
  | 0 => (a, L)
  | (k + 1) =>
    let prev := maintSeq σ a L k
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.Pt
def Imo2017P3.escReps The reports made during an escape phase: the device reports the point on the line through the previous positions, at the same fractional distance as the rabbit line 323 source
Source documentation
The reports made during an escape phase: the device reports the point on the line through the previous positions, at the same fractional distance as the rabbit.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, Nat
Proof uses: HAdd.hAdd, OfNat.ofNat, ENNReal, Fin, HSMul.hSMul, HDiv.hDiv
24 instances, coercions and auxiliary constants left out.
```
def escReps (a : Pt) (u : Pt) (t n : ℝ) (k : ℕ) : Pt := a + ((k : ℝ) / n) • (t • u)
```
Mentions: Imo2017P3.Pt
def Imo2017P3.escPath The rabbit's path during an escape phase when it chooses the point a + t • u + w line 327 source
Source documentation
The rabbit's path during an escape phase when it chooses the point a + t • u + w.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, Nat
Proof uses: HAdd.hAdd, OfNat.ofNat, ENNReal, Fin, HSMul.hSMul, HDiv.hDiv
24 instances, coercions and auxiliary constants left out.
```
def escPath (a : Pt) (u w : Pt) (t n : ℝ) (k : ℕ) : Pt := a + ((k : ℝ) / n) • (t • u + w)
```
Mentions: Imo2017P3.Pt
def Imo2017P3.escPathY The rabbit's path during an escape phase when it chooses the point a + t • u - w line 331 source
Source documentation
The rabbit's path during an escape phase when it chooses the point a + t • u - w.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, Nat
Proof uses: HAdd.hAdd, OfNat.ofNat, ENNReal, Fin, HSMul.hSMul, HDiv.hDiv, HSub.hSub
28 instances, coercions and auxiliary constants left out.
```
def escPathY (a : Pt) (u w : Pt) (t n : ℝ) (k : ℕ) : Pt := a + ((k : ℝ) / n) • (t • u - w)
```
Mentions: Imo2017P3.Pt
def Imo2017P3.escStep Documented declaration: escStep line 336 source
Source documentation
One escape phase with frame {u, w}: the rabbit runs to one of the two points a + t • u ± w (choosing the one farther from where the hunter ends up), while the device reports points on the line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.PState, Imo2017P3.Pt, Prod, Nat
Proof uses: Real, Real.sqrt, HSub.hSub, HPow.hPow, Imo2017P3.phaseLen, Imo2017P3.PState.j, OfNat.ofNat, List, HAppend.hAppend, Imo2017P3.PState.L, List.ofFn, Fin, Imo2017P3.escReps, Imo2017P3.PState.a, HAdd.hAdd, ite, LE.le, Dist.dist, ENNReal, HSMul.hSMul and 4 more
42 instances, coercions and auxiliary constants left out.
```
def escStep (σ : Strategy) (s : PState) (u w : Pt) : PState × (ℕ → Pt) × (ℕ → Pt) :=
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.PState, Imo2017P3.Pt
def Imo2017P3.phaseStep One phase of the construction line 349 source
Source documentation
One phase of the construction. Given the state at the start of the phase, produce the state at its end, the rabbit's positions during the phase (as a function of the offset k = 0, ..., phaseLen j), and the reports made (as a function of the offset k = 1, ..., phaseLen j).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.PState, Prod, Nat, Imo2017P3.Pt
Proof uses: dite, And, LE.le, Real, Dist.dist, OfNat.ofNat, ENNReal, Fin, Imo2017P3.PState.a, Imo2017P3.PState.L, Imo2017P3.PState.j, Imo2017P3.escStep, Classical.choose, Exists, Eq, Norm.norm, Inner.inner, HAdd.hAdd, HSMul.hSMul, HSub.hSub and 8 more
52 instances, coercions and auxiliary constants left out.
```
def phaseStep (σ : Strategy) (s : PState) : PState × (ℕ → Pt) × (ℕ → Pt) :=
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.PState, Imo2017P3.Pt
def Imo2017P3.States The state at the start of phase j line 360 source
Source documentation
The state at the start of phase j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Nat, Imo2017P3.PState
2 instances, coercions and auxiliary constants left out.
```
def States (σ : Strategy) : ℕ → PState
  | 0 => ⟨0, [], 0⟩
  | (j + 1) => (phaseStep σ (States σ j)).1

/-- The rabbit's positions during phase `j` (offsets `0, ..., phaseLen j`). -/
```
Mentions: Imo2017P3.Strategy, Imo2017P3.PState, Imo2017P3.phaseStep, Imo2017P3.phaseLen
def Imo2017P3.Paths The rabbit's positions during phase j (offsets 0, ..., phaseLen j) line 365 source
Source documentation
The rabbit's positions during phase j (offsets 0, ..., phaseLen j).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Nat, Imo2017P3.Pt
Proof uses: Prod.fst, Prod.snd, Imo2017P3.PState, Prod, Imo2017P3.phaseStep, Imo2017P3.States
```
def Paths (σ : Strategy) (j : ℕ) : ℕ → Pt := (phaseStep σ (States σ j)).2.1
```
Mentions: Imo2017P3.Strategy, Imo2017P3.Pt, Imo2017P3.phaseStep, Imo2017P3.States
def Imo2017P3.Reps The reports made during phase j (offsets 1, ..., phaseLen j) line 368 source
Source documentation
The reports made during phase j (offsets 1, ..., phaseLen j).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Nat, Imo2017P3.Pt
Proof uses: Prod.snd, Imo2017P3.PState, Prod, Imo2017P3.phaseStep, Imo2017P3.States
```
def Reps (σ : Strategy) (j : ℕ) : ℕ → Pt := (phaseStep σ (States σ j)).2.2
```
Mentions: Imo2017P3.Strategy, Imo2017P3.Pt, Imo2017P3.phaseStep, Imo2017P3.States
def Imo2017P3.startRound The first round of phase j line 371 source
Source documentation
The first round of phase j.

no axioms what this means
Statement uses: Nat
2 instances, coercions and auxiliary constants left out.
```
def startRound : ℕ → ℕ
  | 0 => 0
  | (j + 1) => startRound j + phaseLen j

/-- The phase containing round `n`. -/
```
Mentions: Imo2017P3.phaseLen
def Imo2017P3.phaseOf The phase containing round n line 376 source
Source documentation
The phase containing round n.

no axioms what this means
Statement uses: Nat
2 instances, coercions and auxiliary constants left out.
```
def phaseOf : ℕ → ℕ
  | 0 => 0
  | (n + 1) =>
    if n + 1 < startRound (phaseOf n + 1) then phaseOf n else phaseOf n + 1

/-- The rabbit's position after round `n`. -/
```
Mentions: Imo2017P3.startRound
def Imo2017P3.rabbit The rabbit's position after round n line 382 source
Source documentation
The rabbit's position after round n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Nat, Imo2017P3.Pt
Proof uses: Imo2017P3.Paths, Imo2017P3.phaseOf, HSub.hSub, Imo2017P3.startRound
2 instances, coercions and auxiliary constants left out.
```
def rabbit (σ : Strategy) (n : ℕ) : Pt :=
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.Pt
def Imo2017P3.reports The point reported in round n line 386 source
Source documentation
The point reported in round n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Nat, Imo2017P3.Pt
Proof uses: ite, Eq, OfNat.ofNat, ENNReal, Fin, Real, Imo2017P3.Reps, Imo2017P3.phaseOf, HSub.hSub, Imo2017P3.startRound
18 instances, coercions and auxiliary constants left out.
```
def reports (σ : Strategy) (n : ℕ) : Pt :=
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.Pt
lemma Imo2017P3.phaseLen_pos line 392 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Imo2017P3.phaseLen
Proof uses: id, dite, ite, Eq, Eq.mpr, congrArg, ite_eq_left, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Not, ite_eq_right
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.phaseLen_ge line 396 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2017P3.phaseLen
Proof uses: id, dite, ite, Eq, Eq.mpr, congrArg, ite_eq_left, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Not, ite_eq_right
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.startRound_succ line 400 source
no axioms what this means
Statement uses: Nat, Eq, Imo2017P3.startRound, HAdd.hAdd, OfNat.ofNat, Imo2017P3.phaseLen
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma Imo2017P3.startRound_strictMono line 402 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: StrictMono, Nat, Imo2017P3.startRound
Proof uses: strictMono_nat_of_lt_succ, Eq.mpr, LT.lt, HAdd.hAdd, OfNat.ofNat, Imo2017P3.phaseLen, id, Eq, congrArg, Imo2017P3.startRound_succ, Imo2017P3.phaseLen_pos
8 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.startRound_eq_of_le line 409 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Imo2017P3.startRound, HMul.hMul
Proof uses: Nat.recAux, Eq.refl, HAdd.hAdd, Ne, Eq.mpr, Imo2017P3.phaseLen, id, congrArg, Imo2017P3.startRound_succ, congrFun', Decidable, ite_eq_right, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.atom_pf and 14 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.startRound_two line 418 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Imo2017P3.startRound, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, Imo2017P3.phaseLen, id, congrArg, Imo2017P3.startRound_succ, HMul.hMul, Imo2017P3.startRound_eq_of_le, le_rfl, of_eq_true, Eq.trans, True, congrFun', ite_eq_left_of_eq_true, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.startRound_eq_of_ge line 422 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Imo2017P3.startRound, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: Nat.le_induction, Eq.mpr, id, congrArg, Imo2017P3.startRound_two, Eq.refl, Ne, Imo2017P3.phaseLen, Imo2017P3.startRound_succ, congrFun', Decidable, ite_eq_right
19 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.startRound_total line 432 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Imo2017P3.startRound, Imo2017P3.totalPhases, Imo2017P3.totalRounds
Proof uses: Eq.mpr, HAdd.hAdd, OfNat.ofNat, HMul.hMul, HSub.hSub, id, congrArg, Imo2017P3.startRound_eq_of_ge, of_eq_true, LE.le, eq_true_of_decide, Eq.refl, Bool, Bool.true, Eq.trans, True, Mathlib.Meta.NormNum.IsNat.to_eq, HPow.hPow, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.isNat_ofNat and 8 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.phaseOf_succ line 436 source
no axioms what this means
Statement uses: Nat, Eq, Imo2017P3.phaseOf, HAdd.hAdd, OfNat.ofNat, ite, LT.lt, Imo2017P3.startRound
Proof uses: rfl
8 instances, coercions and auxiliary constants left out.
lemma Imo2017P3.phaseOf_spec line 440 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, LE.le, Imo2017P3.startRound, Imo2017P3.phaseOf, LT.lt, HAdd.hAdd, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', Imo2017P3.startRound.eq_1, Imo2017P3.phaseLen, ite_eq_right_of_eq_false, Eq, zero_add, and_self, Eq.mpr, ite, id, Imo2017P3.phaseOf_succ, dite, ite_eq_left, And.intro and 13 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.phaseOf_unique line 456 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Imo2017P3.startRound, LT.lt, HAdd.hAdd, OfNat.ofNat, Eq, Imo2017P3.phaseOf
Proof uses: And, Imo2017P3.phaseOf_spec, Or, lt_trichotomy, False.elim, Iff.mpr, StrictMono.le_iff_le, Imo2017P3.startRound_strictMono, Eq.symm
22 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.dist_strategy_append The hunter moves at most one list-element per round: chaining the validity condition over an appended list of reports line 470 source
Source documentation
The hunter moves at most one list-element per round: chaining the validity condition over an appended list of reports.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, List, Imo2017P3.Pt, LE.le, Real, Dist.dist, OfNat.ofNat, ENNReal, Fin, Nat, HAppend.hAppend, List.length
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, List.append_nil, dist_self, CharP.cast_eq_zero, Eq, List.cons, List.append_assoc, eq_self, Eq.mpr, id, HAdd.hAdd, List.length_cons, And.right, dist_triangle and 51 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma dist_strategy_append (σ : Strategy) (hσ : ValidStrategy σ) (L : List Pt)
    (l : List Pt) :
    dist (σ L) (σ (L ++ l)) ≤ (l.length : ℝ) := by
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.Pt
lemma Imo2017P3.escReps_zero line 484 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, Eq, Imo2017P3.escReps, OfNat.ofNat, Nat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, ENNReal, Fin, HSMul.hSMul, HDiv.hDiv, CharP.cast_eq_zero, zero_div, zero_smul, add_zero, Function.Injective.addZeroClass, WithLp, Equiv.add, WithLp.equiv, Equiv.zero, Equiv and 2 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.escPath_zero line 487 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, Eq, Imo2017P3.escPath, OfNat.ofNat, Nat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, ENNReal, Fin, HSMul.hSMul, HDiv.hDiv, CharP.cast_eq_zero, zero_div, smul_add, congr, zero_smul, add_zero, Function.Injective.addZeroClass, WithLp, Equiv.add, WithLp.equiv and 4 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.escPathY_zero line 490 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, Eq, Imo2017P3.escPathY, OfNat.ofNat, Nat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, ENNReal, Fin, HSMul.hSMul, HDiv.hDiv, HSub.hSub, CharP.cast_eq_zero, zero_div, zero_smul, add_zero, Function.Injective.addZeroClass, WithLp, Equiv.add, WithLp.equiv, Equiv.zero and 3 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.escPath_step line 493 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, LT.lt, OfNat.ofNat, Eq, Norm.norm, ENNReal, Fin, Nat, HAdd.hAdd, HSMul.hSMul, Dist.dist, Imo2017P3.escPath
Proof uses: HSub.hSub, HDiv.hDiv, id, Eq.mpr, congrArg, Nat.cast_add, Nat.cast_one, add_sub_add_left_eq_sub, Eq.symm, sub_smul, add_div, add_sub_cancel_left, Eq.refl, dist_comm, dist_eq_norm, HMul.hMul, norm_smul, abs, Real.norm_eq_abs, abs_of_pos and 4 more
146 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.escPathY_step line 503 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, LT.lt, OfNat.ofNat, Eq, Norm.norm, ENNReal, Fin, Nat, HSub.hSub, HSMul.hSMul, Dist.dist, Imo2017P3.escPathY, HAdd.hAdd
Proof uses: HDiv.hDiv, id, Eq.mpr, congrArg, Nat.cast_add, Nat.cast_one, add_sub_add_left_eq_sub, Eq.symm, sub_smul, add_div, add_sub_cancel_left, Eq.refl, dist_comm, dist_eq_norm, HMul.hMul, norm_smul, abs, Real.norm_eq_abs, abs_of_pos, Iff.mpr and 3 more
146 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.escReps_dist line 513 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, LT.lt, OfNat.ofNat, Eq, Norm.norm, ENNReal, Fin, Nat, LE.le, Dist.dist, Imo2017P3.escReps, Imo2017P3.escPath
Proof uses: HSub.hSub, Neg.neg, HSMul.hSMul, HDiv.hDiv, id, HAdd.hAdd, Eq.mpr, congrArg, add_sub_add_left_eq_sub, Eq.symm, smul_sub, sub_add_eq_sub_sub, sub_self, zero_sub, smul_neg, Eq.refl, dist_eq_norm, norm_neg, HMul.hMul, norm_smul and 9 more
139 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.escReps_distY line 524 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, LT.lt, OfNat.ofNat, Eq, Norm.norm, ENNReal, Fin, Nat, LE.le, Dist.dist, Imo2017P3.escReps, Imo2017P3.escPathY
Proof uses: HSub.hSub, HSMul.hSMul, HDiv.hDiv, id, HAdd.hAdd, Eq.mpr, congrArg, add_sub_add_left_eq_sub, Eq.symm, smul_sub, sub_sub_self, Eq.refl, dist_eq_norm, HMul.hMul, norm_smul, abs, Real.norm_eq_abs, abs_of_nonneg, div_nonneg, Nat.cast_nonneg and 4 more
128 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.escPath_end line 535 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, Nat, LT.lt, OfNat.ofNat, Eq, Imo2017P3.escPath, HAdd.hAdd, ENNReal, Fin, HSMul.hSMul
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HDiv.hDiv, div_self, ne_of_gt, smul_add, congr, one_smul, eq_self
87 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.escPathY_end line 539 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Pt, Real, Nat, LT.lt, OfNat.ofNat, Eq, Imo2017P3.escPathY, HAdd.hAdd, ENNReal, Fin, HSub.hSub, HSMul.hSMul
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HDiv.hDiv, div_self, ne_of_gt, one_smul, eq_self
78 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.escStep_spec Specification of one escape phase (with the frame made explicit) line 544 source
Source documentation
Specification of one escape phase (with the frame made explicit).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.PState, Imo2017P3.Pt, LE.le, Real, Dist.dist, OfNat.ofNat, ENNReal, Fin, Nat, Imo2017P3.PState.a, Imo2017P3.PState.L, Eq, Norm.norm, Inner.inner, HAdd.hAdd, HSMul.hSMul, HSub.hSub, Imo2017P3.phaseLen and 12 more
Proof uses: id, Real.sqrt, Imo2017P3.escReps, ite, Imo2017P3.escPath, Imo2017P3.escPathY, Prod.mk, Imo2017P3.PState.mk, Eq.mpr, congrArg, rfl, cast, Eq.symm, Imo2017P3.phaseLen_ge, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, Neg.neg, Mathlib.Tactic.Ring.of_eq and 148 more
238 instances, coercions and auxiliary constants left out.

Tactic trace: 82 steps
Open to load the checked before-and-after goal states.
```
lemma escStep_spec (σ : Strategy) (hσ : ValidStrategy σ) (s : PState) (u w : Pt)
    (hd : dist s.a (σ s.L) ≤ 100)
    (hu1 : ‖u‖ = 1) (hw1 : ‖w‖ = 1) (huw : ⟪u, w⟫_ℝ = 0)
    (hspan : ∀ v : Pt, v = ⟪v, u⟫_ℝ • u + ⟪v, w⟫_ℝ • w)
    (hb : σ s.L = s.a - dist s.a (σ s.L) • u) :
    let n := phaseLen s.j
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.PState, Imo2017P3.Pt, Imo2017P3.phaseLen
lemma Imo2017P3.phaseStep_spec_escape Specification of one phase, escape case line 632 source
Source documentation
Specification of one phase, escape case.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.PState, LE.le, Real, Dist.dist, Imo2017P3.Pt, OfNat.ofNat, ENNReal, Fin, Nat, Imo2017P3.PState.a, Imo2017P3.PState.L, Imo2017P3.PState.j, Imo2017P3.phaseLen, And, Eq, Prod.fst, Prod.snd, Prod and 8 more
Proof uses: Norm.norm, Classical.choose, Exists, Inner.inner, HSMul.hSMul, HSub.hSub, Imo2017P3.frame_exists, Classical.choose_spec, id, Eq.mpr, dite, Imo2017P3.escStep, Not, Prod.mk, Imo2017P3.PState.mk, Imo2017P3.maintSeq, congrArg, dite_eq_left, And.intro, Imo2017P3.escStep_spec
98 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma phaseStep_spec_escape (σ : Strategy) (hσ : ValidStrategy σ) (s : PState)
    (hd : dist s.a (σ s.L) ≤ 100) (hj : s.j ≤ 20000) :
    let n := phaseLen s.j
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.PState, Imo2017P3.phaseLen
lemma Imo2017P3.maintSeq_succ_fst line 647 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.Pt, List, Nat, Eq, Prod.fst, Imo2017P3.maintSeq, HAdd.hAdd, OfNat.ofNat, ENNReal, Fin, Real, HSMul.hSMul, Inv.inv, Dist.dist, Prod.snd, HSub.hSub
Proof uses: rfl
32 instances, coercions and auxiliary constants left out.
lemma Imo2017P3.maintSeq_succ_snd line 653 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.Pt, List, Nat, Eq, Prod.snd, Imo2017P3.maintSeq, HAdd.hAdd, OfNat.ofNat, HAppend.hAppend, List.cons, ENNReal, Fin, Real, Prod.fst, HSMul.hSMul, Inv.inv, Dist.dist, HSub.hSub, List.nil
Proof uses: rfl
34 instances, coercions and auxiliary constants left out.
lemma Imo2017P3.maintSeq_spec Specification of the maintenance iteration: honest reports, unit steps, and the distance from the hunter never decreases line 662 source
Source documentation
Specification of the maintenance iteration: honest reports, unit steps, and the distance from the hunter never decreases.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.Pt, List, LE.le, Real, OfNat.ofNat, Nat, Dist.dist, ENNReal, Fin, And, Eq, Prod.snd, Imo2017P3.maintSeq, HAppend.hAppend, List.ofFn, Prod.fst, HAdd.hAdd, LT.lt
Proof uses: Nat.recAux, And.intro, of_eq_true, Eq.trans, True, congrArg, List.nil, List.ofFn_zero, HSMul.hSMul, Inv.inv, HSub.hSub, List.append_nil, eq_self, absurd, Nat.not_lt_zero, le_refl, le_trans, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp and 113 more
190 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
lemma maintSeq_spec (σ : Strategy) (hσ : ValidStrategy σ) (a : Pt) (L : List Pt)
    (hd : 100 ≤ dist a (σ L)) (k : ℕ) :
    (maintSeq σ a L k).2 =
        L ++ List.ofFn (fun i : Fin k => (maintSeq σ a L (i + 1)).1) ∧
      (∀ i, i < k → dist ((maintSeq σ a L i).1) ((maintSeq σ a L (i + 1)).1) = 1) ∧
      dist a (σ L) ≤ dist ((maintSeq σ a L k).1) (σ ((maintSeq σ a L k).2)) := by
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.Pt, Imo2017P3.maintSeq
lemma Imo2017P3.phaseStep_spec_maint Specification of one phase, maintenance case line 735 source
Source documentation
Specification of one phase, maintenance case.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.PState, LE.le, Real, OfNat.ofNat, Nat, Dist.dist, Imo2017P3.Pt, ENNReal, Fin, Imo2017P3.PState.a, Imo2017P3.PState.L, Not, And, Imo2017P3.PState.j, Imo2017P3.phaseLen, Eq, Prod.fst, Prod.snd and 7 more
Proof uses: Imo2017P3.maintSeq, Imo2017P3.maintSeq_spec, le_trans, id, Eq.mpr, dite, Imo2017P3.escStep, Classical.choose, Exists, Norm.norm, Inner.inner, HSMul.hSMul, HSub.hSub, Prod.mk, Imo2017P3.PState.mk, congrArg, dite_eq_right, And.intro, rfl, of_eq_true and 4 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma phaseStep_spec_maint (σ : Strategy) (hσ : ValidStrategy σ) (s : PState)
    (hd : 100 ≤ dist s.a (σ s.L))
    (hbr : ¬ (dist s.a (σ s.L) ≤ 100 ∧ s.j ≤ 20000)) :
    let n := phaseLen s.j
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.PState, Imo2017P3.phaseLen
lemma Imo2017P3.phaseStep_escape_eq line 756 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.PState, And, LE.le, Real, Dist.dist, Imo2017P3.Pt, OfNat.ofNat, ENNReal, Fin, Nat, Imo2017P3.PState.a, Imo2017P3.PState.L, Imo2017P3.PState.j, Eq, Prod, Imo2017P3.phaseStep, Imo2017P3.escStep, Classical.choose, Exists and 7 more
Proof uses: id, Eq.mpr, dite, Not, Prod.mk, Imo2017P3.PState.mk, Prod.fst, List, Imo2017P3.maintSeq, Imo2017P3.phaseLen, Prod.snd, congrArg, dite_eq_left, Eq.refl
100 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.states_j line 763 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Nat, Eq, Imo2017P3.PState.j, Imo2017P3.States
Proof uses: Nat.recAux, Eq.refl, OfNat.ofNat, id, HAdd.hAdd, dite, Prod.fst, Imo2017P3.PState, Prod, Imo2017P3.Pt, Imo2017P3.phaseStep, And, LE.le, Real, Dist.dist, ENNReal, Fin, Imo2017P3.PState.a, Imo2017P3.PState.L, Eq.mpr and 27 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.phaseStep_spec The branch-independent part of the phase specification line 779 source
Source documentation
The branch-independent part of the phase specification.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.PState, Not, And, LE.le, Real, Dist.dist, Imo2017P3.Pt, OfNat.ofNat, ENNReal, Fin, Nat, Imo2017P3.PState.a, Imo2017P3.PState.L, Imo2017P3.PState.j, Imo2017P3.phaseLen, Eq, Prod.fst, Prod.snd and 7 more
Proof uses: dite, HPow.hPow, HDiv.hDiv, Imo2017P3.phaseStep_spec_escape, And.left, And.right, And.intro, Imo2017P3.phaseStep_spec_maint
58 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma phaseStep_spec (σ : Strategy) (hσ : ValidStrategy σ) (s : PState)
    (hdm : ¬ (dist s.a (σ s.L) ≤ 100 ∧ s.j ≤ 20000) → 100 ≤ dist s.a (σ s.L)) :
    let n := phaseLen s.j
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.PState, Imo2017P3.phaseLen
lemma Imo2017P3.invariant The invariant: after phase j the squared distance is at least min 10000 (j/2), and after phase 20000 it exceeds 100 line 795 source
Source documentation
The invariant: after phase j the squared distance is at least min 10000 (j/2), and after phase 20000 it exceeds 100.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Nat, And, LE.le, Real, Min.min, OfNat.ofNat, HDiv.hDiv, HPow.hPow, Dist.dist, Imo2017P3.Pt, ENNReal, Fin, Imo2017P3.PState.a, Imo2017P3.States, Imo2017P3.PState.L, LT.lt
Proof uses: Nat.recAux, And.intro, Eq.mpr, Imo2017P3.PState.mk, List.nil, id, Eq, congrArg, Imo2017P3.PState, rfl, of_eq_true, Eq.trans, True, congr, congrFun', CharP.cast_eq_zero, zero_div, inf_of_le_right, And.left, List and 151 more
186 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
```
lemma invariant (σ : Strategy) (hσ : ValidStrategy σ) (j : ℕ) :
    min 10000 ((j : ℝ) / 2) ≤ dist ((States σ j).a) (σ (States σ j).L) ^ 2 ∧
    (20000 < j → 100 < dist ((States σ j).a) (σ (States σ j).L)) := by
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.States
lemma Imo2017P3.hdm_of The maintenance mode hypothesis is always satisfiable line 853 source
Source documentation
The maintenance mode hypothesis is always satisfiable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Nat, Not, And, LE.le, Real, Dist.dist, Imo2017P3.Pt, OfNat.ofNat, ENNReal, Fin, Imo2017P3.PState.a, Imo2017P3.States, Imo2017P3.PState.L, Imo2017P3.PState.j
Proof uses: Or, Eq.mp, congrArg, propext, not_and_or, le_of_lt, Iff.mp, LT.lt, not_le, Eq, Imo2017P3.states_j, And.right, Min.min, HDiv.hDiv, HPow.hPow, Imo2017P3.invariant
49 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma hdm_of (σ : Strategy) (hσ : ValidStrategy σ) (j : ℕ)
    (hbr : ¬ (dist (States σ j).a (σ (States σ j).L) ≤ 100 ∧ (States σ j).j ≤ 20000)) :
    100 ≤ dist (States σ j).a (σ (States σ j).L) := by
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.States
lemma Imo2017P3.reportList_succ line 862 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2017P3.Pt, Eq, List, Imo2017P3.reportList, HAdd.hAdd, OfNat.ofNat, HAppend.hAppend, List.cons, List.nil
Proof uses: rfl
8 instances, coercions and auxiliary constants left out.
lemma Imo2017P3.reportList_add line 865 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2017P3.Pt, Eq, List, Imo2017P3.reportList, HAdd.hAdd, HAppend.hAppend, List.ofFn, Fin, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, add_zero, List.nil, List.ofFn_zero, List.append_nil, eq_self, Eq.mpr, id, List.cons, Imo2017P3.reportList_succ, List.append_assoc, HAppend, Eq.rec, Eq.refl, List.concat and 5 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.reportList_eq line 877 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Nat, Eq, List, Imo2017P3.Pt, Imo2017P3.reportList, Imo2017P3.reports, Imo2017P3.startRound, Imo2017P3.PState.L, Imo2017P3.States
Proof uses: Nat.recAux, Eq.refl, OfNat.ofNat, Eq.mpr, HAdd.hAdd, Imo2017P3.phaseLen, id, congrArg, Imo2017P3.startRound_succ, HAppend.hAppend, List.ofFn, Fin, Imo2017P3.reportList_add, Prod.fst, Imo2017P3.PState, Prod, Imo2017P3.phaseStep, rfl, Prod.snd, Imo2017P3.PState.a and 25 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.rabbit_valid line 905 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.ValidRabbit, Imo2017P3.rabbit
Proof uses: And.intro, Eq, Imo2017P3.Pt, OfNat.ofNat, Nat, ENNReal, Fin, Real, Dist.dist, HAdd.hAdd, Imo2017P3.Paths, Imo2017P3.PState.a, Imo2017P3.States, And.left, Prod.fst, Prod.snd, Imo2017P3.PState, Prod, Imo2017P3.phaseStep, And and 29 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.reports_valid line 956 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.ValidReports, Imo2017P3.rabbit, Imo2017P3.reports
Proof uses: Nat, LE.le, OfNat.ofNat, Imo2017P3.startRound, Imo2017P3.phaseOf, HSub.hSub, LT.lt, HAdd.hAdd, And, Real, Dist.dist, Imo2017P3.Pt, ENNReal, Fin, Imo2017P3.phaseOf_spec, Eq, Prod.fst, Prod.snd, Imo2017P3.PState, Prod and 32 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
lemma Imo2017P3.adversary The adversary wins: for every valid hunter strategy, the rabbit and the tracking device can force the distance after 10⁹ rounds to exceed 100 line 1012 source
Source documentation
The adversary wins: for every valid hunter strategy, the rabbit and the tracking device can force the distance after 10⁹ rounds to exceed 100.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Exists, Nat, Imo2017P3.Pt, And, Imo2017P3.ValidRabbit, Imo2017P3.ValidReports, LT.lt, Real, OfNat.ofNat, Dist.dist, ENNReal, Fin, Imo2017P3.totalRounds, Imo2017P3.hunterPos
Proof uses: Exists.intro, Imo2017P3.rabbit, Imo2017P3.reports, And.intro, Imo2017P3.rabbit_valid, Imo2017P3.reports_valid, Eq, Imo2017P3.phaseOf, Imo2017P3.totalPhases, Imo2017P3.phaseOf_unique, Eq.mpr, LE.le, Imo2017P3.startRound, id, congrArg, Imo2017P3.startRound_total, le_refl, HAdd.hAdd, Imo2017P3.phaseLen, Imo2017P3.startRound_succ and 32 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma adversary (σ : Strategy) (hσ : ValidStrategy σ) :
    ∃ A p : ℕ → Pt, ValidRabbit A ∧ ValidReports A p ∧
      100 < dist (A totalRounds) (hunterPos σ p totalRounds) := by
…
```
Mentions: Imo2017P3.Strategy, Imo2017P3.ValidStrategy, Imo2017P3.Pt, Imo2017P3.ValidRabbit, Imo2017P3.ValidReports, Imo2017P3.totalRounds, Imo2017P3.hunterPos
determine Imo2017P3.does_exist The answer to the question "can the hunter always ensure that the distance between her and the rabbit becomes at most 100?" line 1040 source
Source documentation
The answer to the question "can the hunter always ensure that the distance between her and the rabbit becomes at most 100?"

no axioms what this means
Statement uses: Bool
Proof uses: Bool.false
```
determine does_exist : Bool := false
```
problem Imo2017P3.imo2017_p3 line 1042 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ite, Eq, Bool, Imo2017P3.does_exist, Bool.true, Exists, Imo2017P3.Strategy, And, Imo2017P3.ValidStrategy, Nat, Imo2017P3.Pt, Imo2017P3.ValidRabbit, Imo2017P3.ValidReports, LE.le, Real, Dist.dist, OfNat.ofNat, ENNReal, Fin, Imo2017P3.totalRounds and 2 more
Proof uses: id, False, LT.lt, Imo2017P3.adversary, absurd, Iff.mpr, not_le
38 instances, coercions and auxiliary constants left out.

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