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

34 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2018, Problem 4

A site is any point (x, y) in the plane for which x, y ∈ {1, . . . , 20}. Initially, each of the 400 sites is unoccupied. Amy and Ben take turns placing stones on unoccupied sites, with Amy going first; Amy has the additional restriction that no two of her stones may be at a distance equal to √5. They stop once either player cannot move. Find the greatest K such that Amy can ensure that she places at least K stones.

Formalization notes

We use 0-indexed coordinates, so a site is an element of Fin 20 × Fin 20.
Two sites are at distance √5 exactly when they are a knight's move apart: their coordinate differences are 1 and 2 in some order (KnightAdj).
CanEnsure K fuel red blue says that from the position with red stones on red, blue stones on blue, and Amy to move, Amy can ensure that she places at least K stones in total. The fuel parameter bounds the number of rounds left to play; every round occupies two new sites, so CanEnsure K 400 ∅ ∅ (with fuel exceeding any possible length of play) is the exact game-theoretic meaning of "Amy can ensure at least K stones", abbreviated AmyEnsures K.

Imports (5)

Imported by 1 file

Compfiles.lean

abbrev Imo2018P4.Site A site on the board: the 0-indexed version of {1, ..., 20}² line 48 source
Source documentation
A site on the board: the 0-indexed version of {1, ..., 20}².

no axioms what this means
Proof uses: Prod, Fin, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
```
abbrev Site : Type := Fin 20 × Fin 20
```
def Imo2018P4.KnightAdj Two sites are at distance √5 iff they are a knight's move apart, i.e. their coordinate differences are (±1, ±2) or (±2, ±1) line 52 source
Source documentation
Two sites are at distance √5 iff they are a knight's move apart, i.e. their coordinate differences are (±1, ±2) or (±2, ±1).

no axioms what this means
Statement uses: Imo2018P4.Site
Proof uses: Or, And, Eq, Nat, HAdd.hAdd, OfNat.ofNat, Prod.fst, Fin, Prod.snd
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def KnightAdj (a b : Site) : Prop :=
…
```
Mentions: Imo2018P4.Site
instance Imo2018P4.(instance at line 62) line 62 source
def Imo2018P4.amyMoves The sites on which Amy may place a stone: the unoccupied sites at distance different from √5 from every red stone line 67 source
Source documentation
The sites on which Amy may place a stone: the unoccupied sites at distance different from √5 from every red stone.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2018P4.Site
Proof uses: Finset.filter, Membership.mem, Not, Imo2018P4.KnightAdj, Fin, OfNat.ofNat, Nat, SDiff.sdiff, Finset.univ, Union.union
14 instances, coercions and auxiliary constants left out.
```
def amyMoves (red blue : Finset Site) : Finset Site :=
…
```
Mentions: Imo2018P4.Site
def Imo2018P4.benMoves The sites on which Ben may place a stone: all unoccupied sites line 71 source
Source documentation
The sites on which Ben may place a stone: all unoccupied sites.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2018P4.Site
Proof uses: SDiff.sdiff, Fin, OfNat.ofNat, Nat, Finset.univ, Union.union
7 instances, coercions and auxiliary constants left out.
```
def benMoves (red blue : Finset Site) : Finset Site :=
…
```
Mentions: Imo2018P4.Site

inductive Imo2018P4.CanEnsure With fuel rounds left to play, Amy can ensure from the position (red, blue) (with Amy to move) that she places at least K stones in total line 78 source

Source documentation

With fuel rounds left to play, Amy can ensure from the position (red, blue) (with Amy to move) that she places at least K stones in total. (An inductive predicate so that definitions and proofs do not have to unfold a recursion on the fuel parameter.)

standard axioms: Classical.choice, Quot.sound, propext what this means

Statement uses: Nat, Finset, Imo2018P4.Site

inductive CanEnsure (K : ℕ) : ℕ → Finset Site → Finset Site → Prop
  /-- If Amy already has `K` stones, she is done. -/
  | zero {red blue : Finset Site} (h : K ≤ red.card) : CanEnsure K 0 red blue
  /-- If Amy has no legal move, the game stops; she needs to already
  have `K` stones. -/
  | of_no_move {fuel : ℕ} {red blue : Finset Site} (hm : amyMoves red blue = ∅)
      (h : K ≤ red.card) : CanEnsure K (fuel + 1) red blue
  /-- Amy plays `a`; if Ben cannot reply the game stops and she needs
  `K` stones; otherwise she must still ensure `K` stones after every
  reply of Ben. -/
  | of_move {fuel : ℕ} {red blue : Finset Site} {a : Site} (ha : a ∈ amyMoves red blue)
      (hend : benMoves (insert a red) blue = ∅ → K ≤ (insert a red).card)
…

Mentions: Imo2018P4.Site, h, Imo2018P4.amyMoves, Imo2018P4.benMoves

def Imo2018P4.AmyEnsures Amy can ensure that she places at least K stones line 97 source
Source documentation
Amy can ensure that she places at least K stones. (400 rounds of fuel exceeds any possible length of play, since every round occupies two new sites of the 400.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Imo2018P4.CanEnsure, OfNat.ofNat, EmptyCollection.emptyCollection, Finset, Imo2018P4.Site
2 instances, coercions and auxiliary constants left out.
```
def AmyEnsures (K : ℕ) : Prop := CanEnsure K 400 ∅ ∅
…
```
Mentions: Imo2018P4.CanEnsure
def Imo2018P4.blacks The black squares of the checkerboard coloring line 128 source
Source documentation
The black squares of the checkerboard coloring.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2018P4.Site
Proof uses: Finset.filter, Eq, Nat, HMod.hMod, HAdd.hAdd, OfNat.ofNat, Prod.fst, Fin, Prod.snd, Finset.univ
9 instances, coercions and auxiliary constants left out.
```
def blacks : Finset Site := Finset.univ.filter fun c => (c.1.val + c.2.val) % 2 = 0
```
Mentions: Imo2018P4.Site
lemma Imo2018P4.blacks_card line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Imo2018P4.Site, Imo2018P4.blacks, OfNat.ofNat
Proof uses: Finset.univ, Fin, Eq.mpr, Fintype.card, id, congrArg, Finset.card_univ, HMul.hMul, Prod, Fintype.card_prod, Fintype.card_fin, Eq.refl, HAdd.hAdd, Finset.filter, HMod.hMod, Prod.fst, Prod.snd, Not, Finset.card_filter_add_card_filter_not, Finset.card_bij and 21 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
lemma Imo2018P4.not_knightAdj_of_black No two black squares are at knight's move distance line 172 source
Source documentation
No two black squares are at knight's move distance.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2018P4.Site, Membership.mem, Finset, Imo2018P4.blacks, Not, Imo2018P4.KnightAdj
Proof uses: And, Eq, Nat, HAdd.hAdd, OfNat.ofNat, Prod.fst, Fin, Prod.snd, Or, False, Eq.mp, HMod.hMod, Eq.trans, Finset.filter, Finset.univ, True, congrFun', congrArg, true_and
25 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma not_knightAdj_of_black {a b : Site} (ha : a ∈ blacks) (hb : b ∈ blacks) :
    ¬ KnightAdj a b := by
…
```
Mentions: Imo2018P4.Site, Imo2018P4.blacks, Imo2018P4.KnightAdj
lemma Imo2018P4.black_sdiff_subset_amyMoves Every unoccupied black square is a legal move for Amy line 180 source
Source documentation
Every unoccupied black square is a legal move for Amy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2018P4.Site, LE.le, Imo2018P4.blacks, SDiff.sdiff, Fin, OfNat.ofNat, Nat, Union.union, Imo2018P4.amyMoves
Proof uses: Membership.mem, Eq.mpr, And, Finset.univ, Not, Imo2018P4.KnightAdj, id, Eq, Eq.trans, Finset.filter, congrFun', congrArg, And.intro, Finset.mem_univ, And.right, Eq.mp, propext, Finset.mem_sdiff, Imo2018P4.not_knightAdj_of_black, And.left
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma black_sdiff_subset_amyMoves {red blue : Finset Site} (hsub : red ⊆ blacks) :
    blacks \ (red ∪ blue) ⊆ amyMoves red blue := by
…
```
Mentions: Imo2018P4.Site, Imo2018P4.blacks, Imo2018P4.amyMoves
def Imo2018P4.lab The label (0–3) of a cell within its 4×4 block, from the pattern 1 2 3 4 3 4 1 2 2 1 4 3 4 3 2 1 (read with 1-indexed labels in the official solution) line 197 source
Source documentation
The label (0–3) of a cell within its 4×4 block, from the pattern
```
1 2 3 4
3 4 1 2
2 1 4 3
4 3 2 1
```
(read with 1-indexed labels in the official solution).
no axioms what this means
Statement uses: Nat
Proof uses: Imo2018P4.lab.match_1, Unit, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
def lab : ℕ → ℕ → ℕ
  | 0, 0 => 0 | 0, 1 => 1 | 0, 2 => 2 | 0, 3 => 3
  | 1, 0 => 2 | 1, 1 => 3 | 1, 2 => 0 | 1, 3 => 1
  | 2, 0 => 1 | 2, 1 => 0 | 2, 2 => 3 | 2, 3 => 2
  | 3, 0 => 3 | 3, 1 => 2 | 3, 2 => 1 | 3, 3 => 0
  | _, _ => 0

/-- Each label is at most `3`. -/
```
lemma Imo2018P4.lab_le Each label is at most 3 line 205 source
Source documentation
Each label is at most 3.

no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, Imo2018P4.lab
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma lab_le : ∀ i j : Fin 4, lab i.val j.val ≤ 3 := by decide
```
Mentions: Imo2018P4.lab
lemma Imo2018P4.lab_opp Opposite cells of a 4×4 block carry the same label line 208 source
Source documentation
Opposite cells of a 4×4 block carry the same label.

no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, Imo2018P4.lab, HSub.hSub
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma lab_opp : ∀ i j : Fin 4, lab (3 - i.val) (3 - j.val) = lab i.val j.val := by
…
```
Mentions: Imo2018P4.lab
lemma Imo2018P4.lab_eq_cases Two cells of a 4×4 block with the same label are either equal, opposite, or a knight's move apart within the block line 213 source
Source documentation
Two cells of a 4×4 block with the same label are either equal, opposite, or a knight's move apart within the block.

no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, Imo2018P4.lab, Or, And, HSub.hSub, HAdd.hAdd
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma lab_eq_cases : ∀ i j i' j' : Fin 4,
    lab i.val j.val = lab i'.val j'.val →
    (i = i' ∧ j = j') ∨ (i.val = 3 - i'.val ∧ j.val = 3 - j'.val) ∨
    ((i.val + 1 = i'.val ∧ j.val + 2 = j'.val) ∨
     (i.val + 2 = i'.val ∧ j.val + 1 = j'.val) ∨
     (i.val + 1 = i'.val ∧ j'.val + 2 = j.val) ∨
     (i.val + 2 = i'.val ∧ j'.val + 1 = j.val) ∨
     (i'.val + 1 = i.val ∧ j.val + 2 = j'.val) ∨
     (i'.val + 2 = i.val ∧ j.val + 1 = j'.val) ∨
     (i'.val + 1 = i.val ∧ j'.val + 2 = j.val) ∨
     (i'.val + 2 = i.val ∧ j'.val + 1 = j.val)) := by
…
```
Mentions: Imo2018P4.lab
def Imo2018P4.cyc The 4-cycle (one of 100) that a site belongs to: its 4×4 block together with its label within the block line 228 source
Source documentation
The 4-cycle (one of 100) that a site belongs to: its 4×4 block together with its label within the block.

no axioms what this means
Statement uses: Imo2018P4.Site, Nat
Proof uses: HAdd.hAdd, HMul.hMul, HDiv.hDiv, OfNat.ofNat, Prod.fst, Fin, Prod.snd, Imo2018P4.lab, HMod.hMod
10 instances, coercions and auxiliary constants left out.
```
def cyc (c : Site) : ℕ :=
…
```
Mentions: Imo2018P4.Site
lemma Imo2018P4.cyc_lt_100 line 231 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2018P4.Site, LT.lt, Nat, Imo2018P4.cyc, OfNat.ofNat
Proof uses: Prod.fst, Fin, Fin.isLt, Prod.snd, LE.le, Imo2018P4.lab, HMod.hMod, Imo2018P4.lab_le, Fin.mk, Nat.mod_lt, id
10 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Imo2018P4.oppCoord The opposite coordinate within a 4×4 block: i ↦ 3 − i within the block line 243 source
Source documentation
The opposite coordinate within a 4×4 block: i ↦ 3 − i within the block.

no axioms what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, HMul.hMul, OfNat.ofNat, HDiv.hDiv, HSub.hSub, HMod.hMod
11 instances, coercions and auxiliary constants left out.
```
def oppCoord (x : ℕ) : ℕ := 4 * (x / 4) + (3 - x % 4)
```
lemma Imo2018P4.oppCoord_lt line 245 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Imo2018P4.oppCoord
Proof uses: id
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2018P4.opp The opposite site of a site in its 4-cycle: the two sites of the cycle that are not a knight's move apart line 250 source
Source documentation
The opposite site of a site in its 4-cycle: the two sites of the cycle that are not a knight's move apart.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2018P4.Site
Proof uses: Prod.mk, Fin, OfNat.ofNat, Nat, Fin.mk, Imo2018P4.oppCoord, Prod.fst, Prod.snd
4 instances, coercions and auxiliary constants left out.
```
def opp (c : Site) : Site :=
…
```
Mentions: Imo2018P4.Site
lemma Imo2018P4.opp_ne line 253 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2018P4.Site, Ne, Imo2018P4.opp
Proof uses: Eq, Nat, OfNat.ofNat, Prod.fst, Fin, Eq.mpr, id, congrArg, Eq.refl, HAdd.hAdd, HMul.hMul, HDiv.hDiv, HSub.hSub, HMod.hMod
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2018P4.opp_opp line 259 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2018P4.Site, Eq, Imo2018P4.opp
Proof uses: Nat, LT.lt, OfNat.ofNat, Imo2018P4.oppCoord, id, Decidable.byContradiction, HAdd.hAdd, HMul.hMul, HDiv.hDiv, HSub.hSub, HMod.hMod, Not, Prod.ext, Fin, Fin.ext, Prod.fst, Fin.isLt, Prod.snd
15 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2018P4.cyc_opp line 267 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2018P4.Site, Eq, Nat, Imo2018P4.cyc, Imo2018P4.opp
Proof uses: LT.lt, OfNat.ofNat, Prod.fst, Fin, Fin.isLt, Prod.snd, And, HDiv.hDiv, HMod.hMod, HSub.hSub, id, Decidable.byContradiction, HAdd.hAdd, HMul.hMul, Not, Imo2018P4.lab, Eq.mpr, congrArg, And.right, Imo2018P4.lab_opp and 4 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Imo2018P4.eq_or_opp_or_adj_of_cyc_eq Two sites in the same 4-cycle are either equal, opposite, or a knight's move apart line 289 source
Source documentation
Two sites in the same 4-cycle are either equal, opposite, or a knight's move apart.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2018P4.Site, Eq, Nat, Imo2018P4.cyc, Or, Imo2018P4.opp, Imo2018P4.KnightAdj
Proof uses: LT.lt, OfNat.ofNat, Prod.fst, Fin, Fin.isLt, Prod.snd, LE.le, Imo2018P4.lab, HMod.hMod, Imo2018P4.lab_le, Fin.mk, Nat.mod_lt, And, HDiv.hDiv, HSub.hSub, HAdd.hAdd, Imo2018P4.lab_eq_cases, congrArg, Or.inl, Prod.ext and 5 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 91 steps
Open to load the checked before-and-after goal states.
```
lemma eq_or_opp_or_adj_of_cyc_eq :
    ∀ a b : Site, cyc a = cyc b → a = b ∨ a = opp b ∨ KnightAdj a b := by
…
```
Mentions: Imo2018P4.Site, Imo2018P4.cyc, Imo2018P4.opp, Imo2018P4.KnightAdj
def Imo2018P4.BenInv Ben's invariant: every 4-cycle contains at most one red stone, and the blue stones are exactly the opposite sites of the red stones line 353 source
Source documentation
Ben's invariant: every 4-cycle contains at most one red stone, and the blue stones are exactly the opposite sites of the red stones.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2018P4.Site
Proof uses: And, Membership.mem, Imo2018P4.opp, Eq, Nat, Imo2018P4.cyc
2 instances, coercions and auxiliary constants left out.
```
def BenInv (red blue : Finset Site) : Prop :=
…
```
Mentions: Imo2018P4.Site
lemma Imo2018P4.benInv_empty line 357 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2018P4.BenInv, EmptyCollection.emptyCollection, Finset, Imo2018P4.Site
Proof uses: And.intro, Membership.mem, Imo2018P4.opp, And, Eq, Nat, Imo2018P4.cyc, absurd, Finset.notMem_empty
4 instances, coercions and auxiliary constants left out.
lemma Imo2018P4.card_le_100_of_benInv Under Ben's invariant there is at most one red stone per 4-cycle, hence at most 100 red stones line 364 source
Source documentation
Under Ben's invariant there is at most one red stone per 4-cycle, hence at most 100 red stones.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Imo2018P4.Site, Imo2018P4.BenInv, LE.le, Nat, Finset.card, OfNat.ofNat
Proof uses: Set.InjOn, Imo2018P4.cyc, Membership.mem, Set, Eq, And.right, Imo2018P4.opp, And, Eq.mpr, Finset.image, id, congrArg, Eq.symm, Finset.card_image_of_injOn, Finset.range, Finset.card_range, Finset.card_le_card, Exists, Eq.mp, propext and 5 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma card_le_100_of_benInv {red blue : Finset Site} (h : BenInv red blue) :
    red.card ≤ 100 := by
…
```
Mentions: Imo2018P4.Site, h, Imo2018P4.BenInv
lemma Imo2018P4.insert_union_insert line 376 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2018P4.Site, Finset, Eq, Union.union, Fin, OfNat.ofNat, Nat, Insert.insert
Proof uses: Eq.mpr, id, congrArg, Finset.insert_union, Finset.union_insert, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2018P4.canEnsure_of_card_le Once Amy has K stones she keeps them: the game can only add red stones line 382 source
Source documentation
Once Amy has K stones she keeps them: the game can only add red stones.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2018P4.Site, LE.le, Finset.card, Imo2018P4.CanEnsure
Proof uses: Nat.recAux, Imo2018P4.CanEnsure.zero, dite, HAdd.hAdd, OfNat.ofNat, Eq, Imo2018P4.amyMoves, EmptyCollection.emptyCollection, Fin, Imo2018P4.CanEnsure.of_no_move, Not, Membership.mem, Finset.Nonempty, Finset.nonempty_of_ne_empty, Insert.insert, Finset.card_le_card, Finset.subset_insert, Imo2018P4.CanEnsure.of_move, Imo2018P4.benMoves, LE.le.trans
14 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma canEnsure_of_card_le {K : ℕ} :
    ∀ {fuel : ℕ} {red blue : Finset Site}, K ≤ red.card → CanEnsure K fuel red blue := by
…
```
Mentions: Imo2018P4.Site, Imo2018P4.CanEnsure
lemma Imo2018P4.canEnsure_mono Ensuring more stones is harder line 396 source
Source documentation
Ensuring more stones is harder.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2018P4.Site, Imo2018P4.CanEnsure, LE.le
Proof uses: Imo2018P4.CanEnsure.rec, Finset.card, Imo2018P4.CanEnsure.zero, LE.le.trans, Eq, Imo2018P4.amyMoves, EmptyCollection.emptyCollection, Imo2018P4.CanEnsure.of_no_move, Membership.mem, Imo2018P4.benMoves, Insert.insert, Fin, OfNat.ofNat, Imo2018P4.CanEnsure.of_move
10 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma canEnsure_mono {fuel : ℕ} {red blue : Finset Site} {K K' : ℕ}
    (h : CanEnsure K fuel red blue) (hle : K' ≤ K) : CanEnsure K' fuel red blue := by
…
```
Mentions: Imo2018P4.Site, h, Imo2018P4.CanEnsure
lemma Imo2018P4.canEnsure_of_black Amy's strategy: always play on a black square line 407 source
Source documentation
Amy's strategy: always play on a black square. With the potential 2 * red.card + (blacks \ (red ∪ blue)).card Amy ensures half of what remains of the 200 black squares.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2018P4.Site, LE.le, Imo2018P4.blacks, Finset.card, Imo2018P4.benMoves, HMul.hMul, OfNat.ofNat, HAdd.hAdd, SDiff.sdiff, Fin, Union.union, Imo2018P4.CanEnsure
Proof uses: Nat.recAux, Eq, EmptyCollection.emptyCollection, Iff.mp, Finset.card_eq_zero, Nat.le_zero, Finset.sdiff_subset_sdiff, Finset.univ, Finset.subset_univ, le_rfl, Finset.subset_empty, Eq.mp, congrArg, Imo2018P4.CanEnsure.zero, Finset.card_empty, dite, Imo2018P4.canEnsure_of_card_le, Not, Membership.mem, Finset.Nonempty and 39 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 74 steps
Open to load the checked before-and-after goal states.
```
lemma canEnsure_of_black {K : ℕ} :
    ∀ {fuel : ℕ} {red blue : Finset Site},
      red ⊆ blacks → (benMoves red blue).card ≤ fuel →
      2 * K ≤ 2 * red.card + (blacks \ (red ∪ blue)).card →
      CanEnsure K fuel red blue := by
…
```
Mentions: Imo2018P4.Site, Imo2018P4.blacks, Imo2018P4.benMoves, Imo2018P4.CanEnsure
lemma Imo2018P4.not_canEnsure_101_of_benInv Ben's strategy: always reply with the opposite site of the 4-cycle in which Amy just played line 493 source
Source documentation
Ben's strategy: always reply with the opposite site of the 4-cycle in which Amy just played. Then every 4-cycle contains at most one red stone, so Amy places at most 100 stones.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2018P4.Site, Imo2018P4.BenInv, Not, Imo2018P4.CanEnsure, OfNat.ofNat
Proof uses: Nat.recAux, LE.le, Finset.card, Imo2018P4.card_le_100_of_benInv, Eq, HEq, False, Imo2018P4.CanEnsure.zero, Imo2018P4.amyMoves, EmptyCollection.emptyCollection, HAdd.hAdd, False.elim, Imo2018P4.CanEnsure.of_no_move, noConfusion_of_Nat, Nat.ctorIdx, Nat.succ, Nat.add, Membership.mem, Imo2018P4.benMoves, Insert.insert and 40 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 85 steps
Open to load the checked before-and-after goal states.
```
lemma not_canEnsure_101_of_benInv :
    ∀ {fuel : ℕ} {red blue : Finset Site},
      BenInv red blue → ¬ CanEnsure 101 fuel red blue := by
…
```
Mentions: Imo2018P4.Site, Imo2018P4.BenInv, Imo2018P4.CanEnsure
determine Imo2018P4.answer line 566 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Imo2018P4.imo2018_p4 line 568 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsGreatest, Nat, Set.ofPred, Imo2018P4.AmyEnsures, Imo2018P4.answer
Proof uses: Imo2018P4.CanEnsure, OfNat.ofNat, EmptyCollection.emptyCollection, Finset, Imo2018P4.Site, Imo2018P4.canEnsure_of_black, Finset.empty_subset, Imo2018P4.blacks, Eq, Finset.card, Imo2018P4.benMoves, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.univ, Fin, HMul.hMul, SDiff.sdiff and 28 more
26 instances, coercions and auxiliary constants left out.

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