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

27 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1999, Problem 3

Consider an n × n square board, where n is a fixed even positive integer. The board is divided into n^2 unit squares. We say that two different squares on the board are adjacent if they have a common side. N unit squares on the board are marked in such a way that every square (marked or unmarked) on the board is adjacent to at least one marked square. Determine the smallest possible value of N.

Imports (3)

Imported by 1 file

Compfiles.lean

abbrev Imo1999P3.Square line 33 source
no axioms what this means
Statement uses: Nat
Proof uses: Prod, Fin
def Imo1999P3.Adjacent Definition of adjacency: Two squares are adjacent if they share a common side line 36 source
Source documentation
Definition of adjacency: Two squares are adjacent if they share a common side.

no axioms what this means
Statement uses: Nat, Imo1999P3.Square
Proof uses: Imo1999P3.Adjacent.match_1, Fin, Eq, HAdd.hAdd, Int.natAbs, HSub.hSub, Int, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
def Adjacent {n : ℕ} (p1 p2 : Square n) : Prop :=
…
```
Mentions: Imo1999P3.Square
def Imo1999P3.IsValidMarking A set s is a valid marking if every square in the grid is adjacent to some square in s line 41 source
Source documentation
A set s is a valid marking if every square in the grid is adjacent to some square in s.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo1999P3.Square
Proof uses: Exists, And, Membership.mem, Imo1999P3.Adjacent
2 instances, coercions and auxiliary constants left out.
```
def IsValidMarking {n : ℕ} (s : Finset (Square n)) : Prop :=
…
```
Mentions: Imo1999P3.Square
def Imo1999P3.isSw Helper predicate for the internal logic of the construction line 52 source
Source documentation
Helper predicate for the internal logic of the construction. We divide the grid based on parity and modulo 4 conditions.

no axioms what this means
Statement uses: Nat
Proof uses: Or, And, Eq, HMod.hMod, OfNat.ofNat, HAdd.hAdd, LT.lt, LE.le
7 instances, coercions and auxiliary constants left out.
```
def isSw (n : ℕ) (x y : ℕ) : Prop :=
…
```
def Imo1999P3.sw The set "sw" (Marked squares with even coordinate sum) line 59 source
Source documentation
The set "sw" (Marked squares with even coordinate sum).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo1999P3.Square
Proof uses: Finset.filter, Imo1999P3.isSw, Prod.fst, Fin, Prod.snd, Classical.propDecidable, Finset.univ
3 instances, coercions and auxiliary constants left out.
```
noncomputable def sw (n : ℕ) : Finset (Square n) :=
…
```
Mentions: Imo1999P3.Square
def Imo1999P3.sb The set "sb" (Marked squares with odd coordinate sum, symmetric to sw) line 63 source
Source documentation
The set "sb" (Marked squares with odd coordinate sum, symmetric to sw).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo1999P3.Square
Proof uses: Finset.filter, Imo1999P3.isSw, HSub.hSub, OfNat.ofNat, Prod.fst, Fin, Prod.snd, Classical.propDecidable, Finset.univ
6 instances, coercions and auxiliary constants left out.
```
noncomputable def sb (n : ℕ) : Finset (Square n) :=
…
```
Mentions: Imo1999P3.Square
def Imo1999P3.solutionSet The definition of the solution set based on the construction logic line 68 source
Source documentation
The definition of the solution set based on the construction logic. Defined as the union of sw and sb.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo1999P3.Square
Proof uses: Union.union, Fin, Imo1999P3.sw, Imo1999P3.sb
3 instances, coercions and auxiliary constants left out.
```
noncomputable def solutionSet (n : ℕ) : Finset (Square n) :=
…
```
Mentions: Imo1999P3.Square
def Imo1999P3.squaresEvenSum Set of all squares where the sum of coordinates is even line 72 source
Source documentation
Set of all squares where the sum of coordinates is even.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo1999P3.Square
Proof uses: Finset.filter, Eq, HMod.hMod, HAdd.hAdd, Prod.fst, Fin, Prod.snd, OfNat.ofNat, Finset.univ
9 instances, coercions and auxiliary constants left out.
```
noncomputable def squaresEvenSum (n : ℕ) : Finset (Square n) :=
…
```
Mentions: Imo1999P3.Square
def Imo1999P3.squaresOddSum Set of all squares where the sum of coordinates is odd line 76 source
Source documentation
Set of all squares where the sum of coordinates is odd.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo1999P3.Square
Proof uses: Finset.filter, Eq, HMod.hMod, HAdd.hAdd, Prod.fst, Fin, Prod.snd, OfNat.ofNat, Finset.univ
9 instances, coercions and auxiliary constants left out.
```
noncomputable def squaresOddSum (n : ℕ) : Finset (Square n) :=
…
```
Mentions: Imo1999P3.Square
def Imo1999P3.transform The transformation used to map the set sw to a triangular region in Fin k × Fin k line 85 source
Source documentation
The transformation used to map the set sw to a triangular region in Fin k × Fin k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMul.hMul, OfNat.ofNat, Imo1999P3.Square, Prod, Fin
Proof uses: Prod.fst, Prod.snd, dite, HMod.hMod, Fin.mk, HDiv.hDiv, Prod.mk, Not, HSub.hSub
18 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def transform (n k : ℕ) (h_n : n = 2 * k) (p : Square n) : Fin k × Fin k :=
…
```
Mentions: Imo1999P3.Square
lemma Imo1999P3.sum_range_sub_eq_triangular Helper lemma for triangular number summation line 97 source
Source documentation
Helper lemma for triangular number summation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Finset.range, HSub.hSub, HDiv.hDiv, HMul.hMul, HAdd.hAdd, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, EmptyCollection.emptyCollection, Finset, funext, zero_tsub, Finset.sum_const_zero, congrFun', zero_add, mul_one, Nat.zero_div, eq_self, Eq.mpr, id, Finset.sum_range_succ', Finset.sum_congr and 45 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma sum_range_sub_eq_triangular (k : ℕ) : ∑ i ∈ range k, (k - i) = k * (k + 1) / 2 := by
…
```
lemma Imo1999P3.transform_inj_on_sw Lemma: The transformation is injective on the set sw line 112 source
Source documentation
Lemma: The transformation is injective on the set sw.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMul.hMul, OfNat.ofNat, Imo1999P3.Square, Membership.mem, Finset, Imo1999P3.sw, Prod, Fin, Imo1999P3.transform
Proof uses: dite, HMod.hMod, Prod.fst, Fin.mk, HDiv.hDiv, Eq.mpr_prop, Eq.refl, Prod.snd, And, Eq.mp, Prod.mk, Prod.mk.injEq, Not, HSub.hSub, Eq.mpr_not, congrArg, dite_eq_left, congrFun', congr, dite_congr and 17 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
lemma transform_inj_on_sw (n k : ℕ) (h_n : n = 2 * k) :
  ∀ a ∈ sw n, ∀ b ∈ sw n, transform n k h_n a = transform n k h_n b → a = b := by
…
```
Mentions: Imo1999P3.sw, Imo1999P3.transform
lemma Imo1999P3.transform_surjective_on_t Lemma: The transformation maps sw onto t (Surjectivity) line 150 source
Source documentation
Lemma: The transformation maps sw onto t (Surjectivity). For every point p in the triangular set t, there exists a pre-image in sw.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMul.hMul, OfNat.ofNat, Finset, Prod, Fin, Finset.filter, LT.lt, HAdd.hAdd, Prod.fst, Prod.snd, Finset.univ, Membership.mem, Exists, Imo1999P3.Square, And, Imo1999P3.sw, Imo1999P3.transform
Proof uses: dite, HMod.hMod, Prod.mk, Fin.mk, Eq.mp, congrArg, propext, Finset.mem_filter, Exists.intro, And.intro, id, Eq.mpr, Imo1999P3.isSw, Classical.propDecidable, Eq.trans, True, congrFun', true_and, Or.inl, LE.le and 12 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
```
lemma transform_surjective_on_t (n k : ℕ) (h_n : n = 2 * k) :
  let t : Finset (Fin k × Fin k) := univ.filter (λ p => p.1.val + p.2.val < k)
…
```
lemma Imo1999P3.card_sw_eq_triangular Calculate the cardinality of the 'sw' set (White squares in the construction) line 188 source
Source documentation
Calculate the cardinality of the 'sw' set (White squares in the construction). It corresponds to a triangular number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMul.hMul, OfNat.ofNat, Finset.card, Imo1999P3.Square, Imo1999P3.sw, HDiv.hDiv, HAdd.hAdd
Proof uses: Finset, Prod, Fin, Finset.filter, LT.lt, Prod.fst, Prod.snd, Finset.univ, Sigma, Finset.sigma, Finset.range, HSub.hSub, Finset.card_bij, Membership.mem, Sigma.mk, Eq.mpr, And, id, Eq.trans, Sigma.fst and 51 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 66 steps
Open to load the checked before-and-after goal states.
```
lemma card_sw_eq_triangular (n k : ℕ) (h_n : n = 2 * k) :
  (sw n).card = k * (k + 1) / 2 := by
…
```
Mentions: Imo1999P3.sw
lemma Imo1999P3.adjacent_parity_ne Lemma: Adjacent squares always have different parity of the sum of their coordinates line 255 source
Source documentation
Lemma: Adjacent squares always have different parity of the sum of their coordinates.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1999P3.Square, Imo1999P3.Adjacent, Ne, HMod.hMod, HAdd.hAdd, Prod.fst, Fin, Prod.snd, OfNat.ofNat
Proof uses: Int, Or, And, Eq, Int.natAbs, HSub.hSub
21 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma adjacent_parity_ne {n : ℕ} {p m : Square n} (h : Adjacent p m) :
    (p.1.val + p.2.val) % 2 ≠ (m.1.val + m.2.val) % 2 := by
…
```
Mentions: Imo1999P3.Square, h, Imo1999P3.Adjacent
def Imo1999P3.IsIndependentPoint Condition for a set of points to be "independent" (pairwise distance > 2) line 269 source
Source documentation
Condition for a set of points to be "independent" (pairwise distance > 2). This matches the sw condition.

no axioms what this means
Statement uses: Nat, Imo1999P3.Square
Proof uses: Imo1999P3.isSw, Prod.fst, Fin, Prod.snd
1 instances, coercions and auxiliary constants left out.
```
def IsIndependentPoint (n : ℕ) (p : Square n) : Prop := isSw n p.1 p.2
```
Mentions: Imo1999P3.Square, Imo1999P3.isSw
lemma Imo1999P3.independent_points_cant_share_neighbor Lemma: Independent points cannot share a common neighbor line 273 source
Source documentation
Lemma: Independent points cannot share a common neighbor. If p1, p2 ∈ sw and they both are adjacent to m, then p1 = p2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1999P3.Square, Imo1999P3.IsIndependentPoint, Imo1999P3.Adjacent, Eq
Proof uses: Decidable.byContradiction, Fin, Not, Or, And, HMod.hMod, Prod.fst, OfNat.ofNat, Prod.snd, HAdd.hAdd, LT.lt, LE.le, Imo1999P3.Adjacent.match_1, Int.natAbs, HSub.hSub, Int, False, Prod.mk, Fin.mk, Eq.mp and 4 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma independent_points_cant_share_neighbor (n : ℕ) (p1 p2 m : Square n)
  (h1 : IsIndependentPoint n p1) (h2 : IsIndependentPoint n p2)
  (h_adj1 : Adjacent p1 m) (h_adj2 : Adjacent p2 m) : p1 = p2 := by
…
```
Mentions: Imo1999P3.Square, Imo1999P3.IsIndependentPoint, Imo1999P3.Adjacent
def Imo1999P3.parityTransform Helper: A parity-dependent transformation line 301 source
Source documentation
Helper: A parity-dependent transformation. If target_parity is 0, it keeps points as is. Otherwise (assumed to be 1), it reflects the x-coordinate (n - 1 - x).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1999P3.Square
Proof uses: ite, Eq, OfNat.ofNat, Prod.mk, Fin, Fin.mk, HSub.hSub, Prod.fst, Prod.snd
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def parityTransform (n : ℕ) (target_parity : ℕ) (p : Square n) : Square n :=
…
```
Mentions: Imo1999P3.Square
lemma Imo1999P3.parity_transform_injective Lemma: parityTransform is injective line 310 source
Source documentation
Lemma: parityTransform is injective.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Function.Injective, Imo1999P3.Square, Imo1999P3.parityTransform
Proof uses: Eq, dite, OfNat.ofNat, of_eq_true, Eq.trans, True, congrFun', congrArg, Eq.mp, ite, Prod.mk, Fin, Fin.mk, HSub.hSub, Prod.fst, Prod.snd, congr, ite_eq_left, eq_self, Not and 7 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma parity_transform_injective (n target_parity : ℕ) :
    Function.Injective (parityTransform n target_parity) := by
…
```
Mentions: Imo1999P3.parityTransform
lemma Imo1999P3.card_lower_bound_of_cover Lower Bound Lemma (Revised): If s covers all squares with a specific target parity (0 or 1), then |s| ≥ n(n+2)/8 line 320 source
Source documentation
Lower Bound Lemma (Revised): If s covers all squares with a specific target parity (0 or 1), then |s| ≥ n(n+2)/8.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMul.hMul, OfNat.ofNat, Finset, Imo1999P3.Square, LE.le, HMod.hMod, HAdd.hAdd, Prod.fst, Fin, Prod.snd, Exists, And, Membership.mem, Imo1999P3.Adjacent, GE.ge, Finset.card, HDiv.hDiv
Proof uses: Imo1999P3.sw, Imo1999P3.card_sw_eq_triangular, Imo1999P3.parityTransform, Finset.map, Function.Embedding.mk, Imo1999P3.parity_transform_injective, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.card_map, eq_self, Function.Embedding, Eq.mp, propext, Finset.mem_map, id, dite, ite and 66 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 101 steps
Open to load the checked before-and-after goal states.
```
lemma card_lower_bound_of_cover (n k : ℕ) (h_n : n = 2 * k)
  (s : Finset (Square n)) (target_parity : ℕ)
  (h_tp_range : target_parity ≤ 1)
  (h_cover : ∀ p : Square n, (p.1.val + p.2.val) % 2 = target_parity → ∃ m ∈ s, Adjacent p m)
  : s.card ≥ n * (n + 2) / 8 := by
…
```
Mentions: Imo1999P3.Square, Imo1999P3.Adjacent
lemma Imo1999P3.exists_adjacent_in_sw_of_odd_sum Lemma: For any square q whose coordinate sum is odd, there exists a marked square in sw adjacent to q line 431 source
Source documentation
Lemma: For any square q whose coordinate sum is odd, there exists a marked square in sw adjacent to q. This handles the detailed case analysis for the valid marking construction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Even, Imo1999P3.Square, Eq, HMod.hMod, HAdd.hAdd, Prod.fst, Fin, Prod.snd, Exists, And, Membership.mem, Finset, Imo1999P3.sw, Imo1999P3.Adjacent
Proof uses: Iff.mp, Nat.even_iff, id, Eq.mpr, Finset.filter, Imo1999P3.isSw, Classical.propDecidable, Finset.univ, congrArg, funext, congrFun', Eq.trans, True, true_and, Or, LE.le, dite, Imo1999P3.Adjacent.match_1, Int.natAbs, HSub.hSub and 7 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 77 steps
Open to load the checked before-and-after goal states.
```
lemma exists_adjacent_in_sw_of_odd_sum (n : ℕ) (h_pos : 0 < n) (h_even : Even n)
    (q : Square n) (h_sum_odd : (q.1.val + q.2.val) % 2 = 1) :
    ∃ m ∈ sw n, Adjacent q m := by
…
```
Mentions: Imo1999P3.Square, Imo1999P3.sw, Imo1999P3.Adjacent
lemma Imo1999P3.disjoint_sw_sb Lemma: The sets sw and sb are disjoint line 489 source
Source documentation
Lemma: The sets sw and sb are disjoint. (Points in sw have even sum, points in sb have odd sum relative to the transform).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Even, Disjoint, Finset, Imo1999P3.Square, Imo1999P3.sw, Imo1999P3.sb
Proof uses: Eq.mpr, Membership.mem, Not, id, Eq, congrArg, propext, Finset.disjoint_left, Prod.fst, Fin, Prod.snd, HMod.hMod, HAdd.hAdd, And, LE.le, Imo1999P3.isSw, And.right, Finset.univ, Eq.mp, Finset.filter and 7 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma disjoint_sw_sb (n : ℕ) (h_pos : 0 < n) (h_even : Even n) :
  Disjoint (sw n) (sb n) := by
…
```
Mentions: Imo1999P3.sw, Imo1999P3.sb
lemma Imo1999P3.card_sw_eq_card_sb Lemma: Symmetry implies |sw| = |sb| line 512 source
Source documentation
Lemma: Symmetry implies |sw| = |sb|. The map x ↦ n - 1 - x is a bijection swapping the two sets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Imo1999P3.Square, Imo1999P3.sw, Imo1999P3.sb
Proof uses: Prod.mk, Fin, Fin.mk, HSub.hSub, OfNat.ofNat, Prod.fst, Prod.snd, Finset.card_bijective, Eq.mpr, Function.Bijective, And, Function.Injective, Function.Surjective, id, congrArg, Function.Bijective.eq_1, And.intro, Prod.ext, Fin.ext, Eq.mp and 24 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma card_sw_eq_card_sb (n : ℕ) :
  (sw n).card = (sb n).card := by
…
```
Mentions: Imo1999P3.sw, Imo1999P3.sb
theorem Imo1999P3.imo1999_p3_sufficiency line 533 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Even, HDiv.hDiv, HMul.hMul, HAdd.hAdd, Finset, Imo1999P3.Square, Imo1999P3.solutionSet, And, Eq, Finset.card, Imo1999P3.IsValidMarking
Proof uses: HMod.hMod, Iff.mp, Nat.even_iff, And.intro, Union.union, Fin, Imo1999P3.sw, Imo1999P3.sb, rfl, Disjoint, Imo1999P3.disjoint_sw_sb, Imo1999P3.card_sw_eq_card_sb, Eq.mpr, id, congrArg, Imo1999P3.card_sw_eq_triangular, Eq.symm, Nat.mul_add, Nat.mul_assoc, Nat.mul_left_comm and 35 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 71 steps
Open to load the checked before-and-after goal states.
theorem Imo1999P3.imo1999_p3_necessity line 614 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Even, Finset, Imo1999P3.Square, Imo1999P3.IsValidMarking, GE.ge, Finset.card, HDiv.hDiv, HMul.hMul, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq, HMod.hMod, Iff.mp, Nat.even_iff, Finset.filter, Prod.fst, Fin, Prod.snd, Disjoint, Eq.mpr, Membership.mem, Not, id, congrArg, propext, Finset.disjoint_left, And.right, Eq.mp, And, Finset.mem_filter and 61 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 87 steps
Open to load the checked before-and-after goal states.
determine Imo1999P3.solution_value line 693 source
no axioms what this means
Statement uses: Nat
Proof uses: HDiv.hDiv, HMul.hMul, HAdd.hAdd, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
problem Imo1999P3.imo1999_p3 line 695 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Even, IsLeast, Set.ofPred, Exists, Finset, Imo1999P3.Square, And, Imo1999P3.IsValidMarking, Eq, Finset.card, Imo1999P3.solution_value
Proof uses: And.intro, Membership.mem, Set, lowerBounds, id, Exists.intro, Imo1999P3.solutionSet, And.symm, HDiv.hDiv, HMul.hMul, HAdd.hAdd, Imo1999P3.imo1999_p3_sufficiency, LE.le, GE.ge, Imo1999P3.imo1999_p3_necessity, Eq.mpr, congrArg, Eq.symm
16 instances, coercions and auxiliary constants left out.

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