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

55 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2020, Problem 3

There are 4n pebbles of weights 1,2,3,...,4n. Each pebble is colored in one of n colors and there are four pebbles of each color. Show that we can arrange the pebbles into two piles such that the total weights of both piles are the same, and each pile contains two pebbles of each color.

Imports (7)

Imported by 1 file

Compfiles.lean

def Imo2020P3.conn In a pseudograph with endpoint functions a b : E → V, the edge e connects v and w line 44 source
Source documentation
In a pseudograph with endpoint functions a b : E → V, the edge e connects v and w.

no axioms what this means
Proof uses: Or, And, Eq
```
def conn (a b : E → V) (e : E) (v w : V) : Prop :=
…
```

inductive Imo2020P3.IsWalk A walk in a pseudograph: the vertex list has one more entry than the edge list line 48 source

Source documentation

A walk in a pseudograph: the vertex list has one more entry than the edge list.

no axioms what this means

Statement uses: List

inductive IsWalk (a b : E → V) : List V → List E → Prop
  | nil (v : V) : IsWalk a b [v] []
  | cons {v w : V} {e : E} {vs : List V} {es : List E} :
      conn a b e v w → IsWalk a b (w :: vs) es → IsWalk a b (v :: w :: vs) (e :: es)

/-- The multiplicity of vertex `x` as an endpoint of edge `e`. -/

Mentions: Imo2020P3.conn

def Imo2020P3.mult The multiplicity of vertex x as an endpoint of edge e line 54 source
Source documentation
The multiplicity of vertex x as an endpoint of edge e.

no axioms what this means
Statement uses: DecidableEq, Nat
Proof uses: HAdd.hAdd, ite, Eq, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
def mult (a b : E → V) (e : E) (x : V) : ℕ :=
…
```
lemma Imo2020P3.mult_conn line 58 source
standard axioms: propext what this means
Statement uses: DecidableEq, Imo2020P3.conn, Eq, Nat, Imo2020P3.mult, HAdd.hAdd, ite, OfNat.ofNat
Proof uses: And, of_eq_true, Eq.trans, True, eq_self, congrArg, add_comm
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Imo2020P3.slotCount Total number of edge-slots of a list of edges at vertex x line 65 source
Source documentation
Total number of edge-slots of a list of edges at vertex x.

standard axioms: propext what this means
Statement uses: DecidableEq, List, Nat
Proof uses: List.sum, List.map, Imo2020P3.mult
3 instances, coercions and auxiliary constants left out.
```
def slotCount (a b : E → V) (es : List E) (x : V) : ℕ :=
…
```
lemma Imo2020P3.IsWalk.vs_ne_nil line 69 source
standard axioms: propext what this means
Statement uses: List, Imo2020P3.IsWalk, Ne, List.nil
Proof uses: Eq, HEq, List.cons, Imo2020P3.IsWalk.nil, of_eq_true, Not, Eq.trans, False, True, congrArg, not_false_eq_true, Eq.symm, Imo2020P3.conn, Imo2020P3.IsWalk.cons, eq_false', False.elim, noConfusion_of_Nat, List.ctorIdx, Eq.refl, HEq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.slotCount_eq In any walk, the slot count at x equals twice the number of interior occurrences of x, plus the endpoint contributions line 76 source
Source documentation
In any walk, the slot count at x equals twice the number of interior occurrences of x, plus the endpoint contributions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Imo2020P3.IsWalk, Ne, List.nil, Eq, Nat, Imo2020P3.slotCount, HAdd.hAdd, HMul.hMul, OfNat.ofNat, List.count, List.dropLast, List.drop, ite, Option, List.head?, Option.some, List.getLast?
Proof uses: Imo2020P3.IsWalk.rec, absurd, List.cons, rfl, Imo2020P3.conn, HEq, Imo2020P3.IsWalk.nil, Imo2020P3.mult, Eq.mpr, id, congrArg, Imo2020P3.mult_conn, List.count_nil, List.head?_cons, List.getLast?_cons_cons, List.getLast?_singleton, congr, ite_congr, Option.some.injEq, Eq.refl and 26 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma slotCount_eq {a b : E → V} {vs : List V} {es : List E} (h : IsWalk a b vs es)
    (hne : es ≠ []) (x : V) :
    slotCount a b es x =
      2 * ((vs.drop 1).dropLast.count x) +
        (if vs.head? = some x then 1 else 0) + (if vs.getLast? = some x then 1 else 0) := by
…
```
Mentions: h, Imo2020P3.IsWalk, Imo2020P3.slotCount
lemma Imo2020P3.slotCount_closed In a closed walk, the slot count at x is twice the number of occurrences of x line 107 source
Source documentation
In a closed walk, the slot count at x is twice the number of occurrences of x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Imo2020P3.IsWalk, Eq, Option, List.head?, List.getLast?, Nat, Imo2020P3.slotCount, HMul.hMul, OfNat.ofNat, List.count, List.dropLast
Proof uses: dite, List.nil, HEq, List.cons, Imo2020P3.IsWalk.nil, of_eq_true, Eq.trans, True, congr, congrArg, List.map, Imo2020P3.mult, List.sum, List.map_nil, List.dropLast_singleton, MulZeroClass.mul_zero, eq_self, Eq.symm, Imo2020P3.conn, Imo2020P3.IsWalk.cons and 34 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma slotCount_closed {a b : E → V} {vs : List V} {es : List E} (h : IsWalk a b vs es)
    (hc : vs.head? = vs.getLast?) (x : V) :
    slotCount a b es x = 2 * vs.dropLast.count x := by
…
```
Mentions: h, Imo2020P3.IsWalk, Imo2020P3.slotCount
lemma Imo2020P3.altCount_eq The alternating slot count along a walk, red at positions with parity s line 140 source
Source documentation
The alternating slot count along a walk, red at positions with parity s.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Imo2020P3.IsWalk, Ne, List.nil, Nat, LE.le, OfNat.ofNat, Eq, List.sum, List.mapIdx, ite, HMod.hMod, Imo2020P3.mult, HAdd.hAdd, List.count, List.dropLast, List.drop, And, Option and 5 more
Proof uses: Imo2020P3.IsWalk.rec, absurd, List.cons, rfl, Imo2020P3.conn, HEq, Imo2020P3.IsWalk.nil, Eq.mpr, id, congrArg, List.mapIdx_cons, List.mapIdx_nil, List.sum_cons, List.sum_nil, Imo2020P3.mult_conn, congr, Eq.trans, List.drop_succ_cons, List.drop_zero, List.dropLast_singleton and 42 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma altCount_eq {a b : E → V} {vs : List V} {es : List E} (h : IsWalk a b vs es)
    (hne : es ≠ []) {s : ℕ} (hs : s ≤ 1) (x : V) :
    ((es.mapIdx fun i e => if s = i % 2 then mult a b e x else 0).sum) =
      ((vs.drop 1).dropLast.count x) +
        (if vs.head? = some x ∧ s = 0 then 1 else 0) +
        (if vs.getLast? = some x ∧ s = (es.length - 1) % 2 then 1 else 0) := by
…
```
Mentions: h, Imo2020P3.IsWalk, Imo2020P3.mult
lemma Imo2020P3.altCount_closed In a closed walk of even length, the alternating slot count at x equals the number of occurrences of x among the positions line 177 source
Source documentation
In a closed walk of even length, the alternating slot count at x equals the number of occurrences of x among the positions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Imo2020P3.IsWalk, Eq, Option, List.head?, List.getLast?, Even, Nat, List.length, List.sum, List.mapIdx, ite, HMod.hMod, OfNat.ofNat, Imo2020P3.mult, List.count, List.dropLast
Proof uses: dite, List.nil, HEq, List.cons, Imo2020P3.IsWalk.nil, of_eq_true, Eq.trans, True, congrArg, List.dropLast_singleton, eq_self, Eq.symm, Imo2020P3.conn, Imo2020P3.IsWalk.cons, False.elim, noConfusion_of_Nat, List.ctorIdx, Eq.refl, HEq.refl, Not and 40 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma altCount_closed {a b : E → V} {vs : List V} {es : List E} (h : IsWalk a b vs es)
    (hc : vs.head? = vs.getLast?) (hL : Even es.length) (x : V) :
    ((es.mapIdx fun i e => if i % 2 = 0 then mult a b e x else 0).sum) =
      vs.dropLast.count x := by
…
```
Mentions: h, Imo2020P3.IsWalk, Imo2020P3.mult
lemma Imo2020P3.IsWalk.length line 205 source
standard axioms: propext what this means
Statement uses: List, Imo2020P3.IsWalk, Eq, Nat, List.length, HAdd.hAdd, OfNat.ofNat
Proof uses: Imo2020P3.IsWalk.rec, Eq.refl, List.cons, List.nil, Imo2020P3.conn, of_eq_true, Eq.trans, True, congrFun', congrArg, eq_self
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.IsWalk.append line 212 source
standard axioms: propext what this means
Statement uses: List, Imo2020P3.IsWalk, Eq, Option, List.getLast?, List.head?, HAppend.hAppend, List.tail
Proof uses: Imo2020P3.IsWalk.rec, List.cons, List.nil, False.elim, Eq.mp, False, eq_false', Option.some, Option.none, noConfusion_of_Nat, Option.ctorIdx, Eq.symm, id, Option.some.injEq, Eq.refl, Imo2020P3.conn, List.getLast?_cons_cons, Eq.mpr, congrArg, Imo2020P3.IsWalk.cons and 1 more
6 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.IsWalk.take line 230 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Imo2020P3.IsWalk, Nat, List.take, HAdd.hAdd, OfNat.ofNat
Proof uses: Imo2020P3.IsWalk.rec, Nat.casesAuxOn, Eq, List.cons, List.nil, Imo2020P3.IsWalk.nil, Eq.symm, Eq.mpr, id, congrArg, List.take_of_length_le, of_eq_true, LE.le, List.length, Eq.trans, True, congrFun', zero_add, Function.swap, List.take_nil and 8 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.IsWalk.drop line 249 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Imo2020P3.IsWalk, Nat, LE.le, List.length, List.drop
Proof uses: Imo2020P3.IsWalk.rec, List.nil, Eq, OfNat.ofNat, Eq.mp, List.cons, Imo2020P3.IsWalk.nil, Eq.symm, Imo2020P3.conn, Nat.casesAuxOn, Imo2020P3.IsWalk.cons, HAdd.hAdd, Eq.mpr, id, congrArg, List.drop_succ_cons, Function.swap, Eq.refl
34 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
structure Imo2020P3.CTrail A closed trail in a pseudograph: a closed walk with no repeated edges line 264 source
Source documentation
A closed trail in a pseudograph: a closed walk with no repeated edges.

no axioms what this means
```
structure CTrail (a b : E → V) where
…
```
lemma Imo2020P3.getLast?_drop_of_lt line 272 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, LT.lt, List.length, Eq, Option, List.getLast?, List.drop
Proof uses: Ne, List.nil, Eq.mpr, OfNat.ofNat, id, congrArg, propext, List.ne_nil_iff_length_pos, HSub.hSub, List.length_drop, Option.some, List.getLast, List.getLast?_eq_getLast_of_ne_nil, Eq.rec, Eq.refl, List.getLast_drop
7 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.head?_take_of_pos line 282 source
standard axioms: propext what this means
Statement uses: List, Nat, LT.lt, OfNat.ofNat, Eq, Option, List.head?, List.take
Proof uses: List.nil, of_eq_true, Option.none, Eq.trans, True, congrFun', congrArg, List.take_nil, eq_self, Eq.symm, List.cons, Nat.casesAuxOn, HAdd.hAdd, Option.some, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.getLast?_take_succ line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, LE.le, HAdd.hAdd, OfNat.ofNat, List.length, Eq, Option, List.getLast?, List.take, GetElem?.getElem?, LT.lt
Proof uses: Ne, List.nil, Eq.mpr, id, congrArg, propext, List.ne_nil_iff_length_pos, Min.min, List.length_take, Option.some, List.getLast, List.getLast?_eq_getLast_of_ne_nil, GetElem.getElem, HSub.hSub, List.getLast_eq_getElem, Nat.lt_of_lt_of_le, List.length_take_le', List.getElem_take, GetElem, Eq.rec and 3 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.getLast?_tail_of_ne line 304 source
standard axioms: propext what this means
Statement uses: List, Ne, List.tail, List.nil, Eq, Option, List.getLast?
Proof uses: False.elim, Eq.mp, False, Eq.trans, Not, True, congrArg, eq_self, not_true_eq_false, Eq.symm, List.cons, Eq.refl
2 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Imo2020P3.CTrail.rotate Rotate a closed trail at position k (an index of a vertex occurrence) line 313 source
Source documentation
Rotate a closed trail at position k (an index of a vertex occurrence).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2020P3.CTrail, Nat, LT.lt, List.length, Imo2020P3.CTrail.es
Proof uses: Imo2020P3.CTrail.mk, HAppend.hAppend, List, List.drop, Imo2020P3.CTrail.vs, List.tail, List.take, HAdd.hAdd, OfNat.ofNat, List.rotate
10 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
def CTrail.rotate {a b : E → V} (T : CTrail a b) (k : ℕ) (hk : k < T.es.length) :
    CTrail a b where
…
```
Mentions: Imo2020P3.CTrail
lemma Imo2020P3.list_sum_eq_toFinset_sum line 349 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, List.Nodup, Nat, Eq, List.sum, List.map, Finset.sum, List.toFinset
Proof uses: Eq.symm, List.sum_toFinset
10 instances, coercions and auxiliary constants left out.
lemma Imo2020P3.exists_max_walk A maximal walk from v using only edges of U, with distinct edges line 355 source
Source documentation
A maximal walk from v using only edges of U, with distinct edges.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Exists, List, And, Imo2020P3.IsWalk, Eq, Option, List.head?, Option.some, List.getLast?, List.Nodup, Membership.mem, Imo2020P3.conn
Proof uses: Nat, Finset.filter, List.length, Classical.propDecidable, Finset.range, HAdd.hAdd, Finset.card, OfNat.ofNat, rfl, Eq.mpr, id, congrArg, propext, Finset.mem_filter, And.intro, of_eq_true, Eq.trans, LT.lt, True, Function.swap and 42 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
```
lemma exists_max_walk (a b : E → V) (U : Finset E) (v : V) :
    ∃ vs es y, IsWalk a b vs es ∧ vs.head? = some v ∧ vs.getLast? = some y ∧ es.Nodup ∧
      (∀ e ∈ es, e ∈ U) ∧ (∀ e ∈ U, ∀ w, conn a b e y w → e ∈ es) := by
…
```
Mentions: Imo2020P3.IsWalk, Imo2020P3.conn
lemma Imo2020P3.exists_closed_trail Any edge of U lies in a closed trail within U, provided all U-degrees are even line 410 source
Source documentation
Any edge of U lies in a closed trail within U, provided all U-degrees are even.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Even, Nat, Finset.sum, Imo2020P3.mult, Membership.mem, Exists, Imo2020P3.CTrail, And, List, Imo2020P3.CTrail.es, Ne, List.nil
Proof uses: Imo2020P3.IsWalk, Eq, Option, List.head?, Option.some, List.getLast?, List.Nodup, Imo2020P3.conn, Imo2020P3.exists_max_walk, False, HEq, List.cons, Imo2020P3.IsWalk.nil, Or.inl, And.intro, rfl, False.elim, Eq.mp, Eq.symm, Option.some.injEq and 47 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
```
lemma exists_closed_trail (a b : E → V) (U : Finset E)
    (hU : ∀ x, Even (∑ e ∈ U, mult a b e x)) (e₀ : E) (he₀ : e₀ ∈ U) :
    ∃ T : CTrail a b, (∀ e ∈ T.es, e ∈ U) ∧ T.es ≠ [] := by
…
```
Mentions: Imo2020P3.mult, Imo2020P3.CTrail
lemma Imo2020P3.decompose Decompose an even-degree edge set into edge-disjoint closed trails line 455 source
Source documentation
Decompose an even-degree edge set into edge-disjoint closed trails.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Even, Nat, Finset.sum, Imo2020P3.mult, Exists, List, Imo2020P3.CTrail, And, Membership.mem, Imo2020P3.CTrail.es, Ne, List.nil, List.Pairwise, Disjoint, List.toFinset
Proof uses: Finset.strongInduction, LT.lt, dite, Eq, EmptyCollection.emptyCollection, Exists.intro, And.intro, of_eq_true, Eq.trans, True, forall_congr, False, Not, implies_congr, Eq.refl, implies_true, congrArg, funext, congrFun', false_and and 53 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 74 steps
Open to load the checked before-and-after goal states.
```
lemma decompose (a b : E → V) (U : Finset E) (hU : ∀ x, Even (∑ e ∈ U, mult a b e x)) :
    ∃ F : List (CTrail a b),
      (∀ T ∈ F, ∀ e ∈ T.es, e ∈ U) ∧
      (∀ T ∈ F, T.es ≠ []) ∧
      (∀ e ∈ U, ∃ T ∈ F, e ∈ T.es) ∧
      F.Pairwise (fun T₁ T₂ => Disjoint T₁.es.toFinset T₂.es.toFinset) := by
…
```
Mentions: Imo2020P3.mult, Imo2020P3.CTrail
lemma Imo2020P3.CTrail.rotate_head? line 520 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2020P3.CTrail, Nat, LT.lt, List.length, Imo2020P3.CTrail.es, Eq, Option, GetElem?.getElem?, List, Imo2020P3.CTrail.vs, Option.some, List.head?, Imo2020P3.CTrail.rotate
Proof uses: HAdd.hAdd, OfNat.ofNat, Imo2020P3.IsWalk.length, Imo2020P3.CTrail.walk, id, Eq.mpr, HAppend.hAppend, List.drop, List.tail, List.take, congrArg, List.head?_append_of_ne_nil, Ne, List.nil, propext, List.ne_nil_iff_length_pos, HSub.hSub, List.length_drop, List.head?_drop
12 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.CTrail.rotate_es_toFinset line 529 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Imo2020P3.CTrail, Nat, LT.lt, List.length, Imo2020P3.CTrail.es, Eq, Finset, List.toFinset, Imo2020P3.CTrail.rotate
Proof uses: id, Finset.ext, List.rotate, of_eq_true, Iff, Membership.mem, Eq.trans, List, True, congr, congrArg, iff_self
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Imo2020P3.CTrail.append Append two closed trails that both start at the same vertex v line 536 source
Source documentation
Append two closed trails that both start at the same vertex v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Imo2020P3.CTrail, Eq, Option, List.head?, Imo2020P3.CTrail.vs, Option.some, Disjoint, Finset, List.toFinset, Imo2020P3.CTrail.es
Proof uses: Imo2020P3.CTrail.mk, HAppend.hAppend, List, List.tail
9 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
def CTrail.append {a b : E → V} {v : V} (T₁ T₂ : CTrail a b)
    (h₁ : T₁.vs.head? = some v) (h₂ : T₂.vs.head? = some v)
    (hdj : Disjoint T₁.es.toFinset T₂.es.toFinset) : CTrail a b where
…
```
Mentions: Imo2020P3.CTrail
lemma Imo2020P3.CTrail.exists_rotate_index line 553 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2020P3.CTrail, Ne, List, Imo2020P3.CTrail.es, List.nil, Membership.mem, Imo2020P3.CTrail.vs, Exists, Nat, And, LT.lt, List.length, Eq, Option, GetElem?.getElem?, Option.some
Proof uses: Fin, List.get, List.get_of_mem, Fin.mk, HAdd.hAdd, OfNat.ofNat, Imo2020P3.IsWalk.length, Imo2020P3.CTrail.walk, dite, Exists.intro, And.intro, Eq.mpr, GetElem.getElem, id, congrArg, List.getElem?_eq_getElem, Eq.refl, Not, Nat.pos_of_ne_zero, List.eq_nil_of_length_eq_zero and 8 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
instance Imo2020P3.(instance at line 575) line 575 source
lemma Imo2020P3.two_le_length line 579 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Membership.mem, Ne, LE.le, Nat, OfNat.ofNat, List.length
Proof uses: List.rec, List.nil, False.elim, Eq.mp, False, List.cons, Eq.mpr, HAdd.hAdd, id, Eq, congrArg, List.length_cons, Or, propext, List.mem_cons, absurd, rfl, LT.lt, List.length_pos_of_mem
14 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.merge_disjoint Merge trails sharing vertices until the family is vertex-disjoint line 599 source
Source documentation
Merge trails sharing vertices until the family is vertex-disjoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Nat, List, Imo2020P3.CTrail, Eq, List.length, Exists, And, Membership.mem, Imo2020P3.CTrail.es, Ne, List.nil, List.Pairwise, Disjoint, Finset, List.toFinset, Imo2020P3.CTrail.vs
Proof uses: Nat.strongRecOn, LT.lt, dite, Classical.propDecidable, Option, GetElem?.getElem?, Option.some, Imo2020P3.CTrail.exists_rotate_index, List.head?, Imo2020P3.CTrail.rotate, Imo2020P3.CTrail.rotate_head?, Eq.mpr, id, congrArg, Imo2020P3.CTrail.rotate_es_toFinset, List.Pairwise.forall, Imo2020P3.CTrail.append, rfl, HAppend.hAppend, LE.le and 70 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 118 steps
Open to load the checked before-and-after goal states.
```
lemma merge_disjoint (a b : E → V) :
    ∀ n : ℕ, ∀ F : List (CTrail a b), F.length = n →
    (∀ e, ∃ T ∈ F, e ∈ T.es) →
    (∀ T ∈ F, T.es ≠ []) →
    F.Pairwise (fun T₁ T₂ => Disjoint T₁.es.toFinset T₂.es.toFinset) →
    ∃ F' : List (CTrail a b),
      (∀ e, ∃ T ∈ F', e ∈ T.es) ∧
      (∀ T ∈ F', T.es ≠ []) ∧
      F'.Pairwise (fun T₁ T₂ => Disjoint T₁.es.toFinset T₂.es.toFinset) ∧
      F'.Pairwise (fun T₁ T₂ => Disjoint T₁.vs.toFinset T₂.vs.toFinset) := by
…
```
Mentions: Imo2020P3.CTrail
lemma Imo2020P3.mult_sum line 710 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Eq, Nat, Finset.sum, Finset.univ, Imo2020P3.mult, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, ite, Finset.sum_add_distrib, congr, Membership.mem, Finset, Finset.sum_ite_eq, ite_eq_left_of_eq_true, eq_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.IsWalk.mem_vs_of_mem_es line 714 source
standard axioms: propext what this means
Statement uses: List, Imo2020P3.IsWalk, Membership.mem, And
Proof uses: Imo2020P3.IsWalk.rec, List.nil, False.elim, List.cons, Eq.mp, False, Imo2020P3.conn, Eq, Or, congrArg, propext, List.mem_cons, And.intro, List.mem_cons_self, List.mem_cons_of_mem
7 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
instance Imo2020P3.(instance at line 727) line 727 source
lemma Imo2020P3.even_length_of_mem line 731 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, List, Imo2020P3.CTrail, Exists, And, Membership.mem, Imo2020P3.CTrail.es, List.Pairwise, Disjoint, Finset, List.toFinset, Imo2020P3.CTrail.vs, Eq, Nat, Finset.sum, Finset.univ, Imo2020P3.mult, OfNat.ofNat, Even and 1 more
Proof uses: Imo2020P3.slotCount, HMul.hMul, Imo2020P3.list_sum_eq_toFinset_sum, Imo2020P3.CTrail.nodup, Eq.mpr, id, congrArg, Finset.sum_congr, rfl, Finset.sum_comm, Finset.card, congrFun', Eq.trans, HSMul.hSMul, Eq.refl, Imo2020P3.mult_sum, Finset.sum_const, nsmul_eq_mul, List.toFinset_card_of_nodup, Mathlib.Tactic.Ring.of_eq and 52 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.mapIdx_eq_map_idxOf line 799 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, List.Nodup, Nat, Eq, List.mapIdx, List.map, List.idxOf
Proof uses: List.rec, List.nil, Eq.refl, List.cons, List.Nodup.of_cons, Eq.mpr, OfNat.ofNat, HAdd.hAdd, id, congrArg, List.mapIdx_cons, List.map_cons, List.idxOf_cons_eq, rfl, Eq.rec, List.map_congr_left, Membership.mem, Ne, And.left, Not and 7 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem Imo2020P3.two_factor Every 4-regular pseudograph has a 2-factor: a 2-coloring of its edges such that every vertex sees exactly two half-edges of each color line 818 source
Source documentation
Every 4-regular pseudograph has a 2-factor: a 2-coloring of its edges such that every vertex sees exactly two half-edges of each color.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Eq, Nat, Finset.sum, Finset.univ, Imo2020P3.mult, OfNat.ofNat, Exists, Bool, ite, Bool.true
Proof uses: List, Imo2020P3.CTrail, And, Membership.mem, Imo2020P3.CTrail.es, Finset, Ne, List.nil, List.Pairwise, Disjoint, List.toFinset, Imo2020P3.decompose, Eq.mpr, Even, id, congrArg, Exists.intro, HAdd.hAdd, rfl, Imo2020P3.CTrail.vs and 64 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 91 steps
Open to load the checked before-and-after goal states.
```
theorem two_factor (a b : E → V) (hdeg : ∀ x, (∑ e : E, mult a b e x) = 4) :
    ∃ red : E → Bool, ∀ x : V, (∑ e : E, if red e then mult a b e x else 0) = 2 := by
…
```
Mentions: Imo2020P3.mult
def Imo2020P3.apeb The lighter pebble of pair k line 907 source
Source documentation
The lighter pebble of pair k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat
Proof uses: Fin.mk
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def apeb : Fin (2 * n) → Fin (4 * n) := fun k => ⟨k.val, by lia⟩
```
def Imo2020P3.bpeb The heavier pebble of pair k line 910 source
Source documentation
The heavier pebble of pair k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat
Proof uses: Fin.mk, HSub.hSub
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def bpeb : Fin (2 * n) → Fin (4 * n) := fun k => ⟨4 * n - 1 - k.val, by lia⟩
```
lemma Imo2020P3.apeb_inj line 912 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Function.Injective, Fin, HMul.hMul, OfNat.ofNat, Imo2020P3.apeb
Proof uses: Eq, Iff.mp, Fin.ext_iff, Fin.ext
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.bpeb_inj line 915 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Function.Injective, Fin, HMul.hMul, OfNat.ofNat, Imo2020P3.bpeb
Proof uses: Eq, Iff.mp, Fin.ext_iff, Fin.ext
8 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.apeb_ne_bpeb line 922 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Ne, Imo2020P3.apeb, Imo2020P3.bpeb
Proof uses: Eq, Iff.mp, Fin.ext_iff
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Imo2020P3.pairOf The pair (one of the 2n complementary pairs) that pebble j belongs to line 929 source
Source documentation
The pair (one of the 2n complementary pairs) that pebble j belongs to.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat
Proof uses: dite, LT.lt, Fin.mk, Not, HSub.hSub
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def pairOf : Fin (4 * n) → Fin (2 * n) := fun j =>
…
```
lemma Imo2020P3.pairOf_apeb line 932 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Eq, Imo2020P3.pairOf, Imo2020P3.apeb
Proof uses: id, Eq.mpr, Fin.mk, dite, LT.lt, Not, HSub.hSub, congrArg, Imo2020P3.pairOf.eq_1, Fin.isLt, dite_eq_left, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.pairOf_bpeb line 936 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Eq, Imo2020P3.pairOf, Imo2020P3.bpeb
Proof uses: id, Eq.mpr, Fin.mk, HSub.hSub, dite, LT.lt, Not, congrArg, Imo2020P3.pairOf.eq_1, dite_eq_right, Fin.ext
15 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.pairOf_mem_pair line 941 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Or, Eq, Imo2020P3.apeb, Imo2020P3.pairOf, Imo2020P3.bpeb
Proof uses: dite, LT.lt, Or.inl, Eq.mpr, Fin.mk, Not, HSub.hSub, id, congrArg, Imo2020P3.pairOf.eq_1, dite_eq_left, Fin.ext, rfl, Or.inr, dite_eq_right
13 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def Imo2020P3.pgA The pseudograph on colors whose edges are the complementary pairs line 951 source
Source documentation
The pseudograph on colors whose edges are the complementary pairs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat
Proof uses: Imo2020P3.apeb
6 instances, coercions and auxiliary constants left out.
```
def pgA : Fin (2 * n) → Fin n := fun k => c (apeb k)
```
Mentions: Imo2020P3.apeb
def Imo2020P3.pgB line 952 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat
Proof uses: Imo2020P3.bpeb
6 instances, coercions and auxiliary constants left out.
lemma Imo2020P3.univ_eq_map_union line 954 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Fin, HMul.hMul, OfNat.ofNat, Finset.univ, Union.union, Finset.map, Function.Embedding.mk, Imo2020P3.apeb, Imo2020P3.apeb_inj, Imo2020P3.bpeb, Imo2020P3.bpeb_inj
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, True, Or, Exists, And, id, congr, congrArg, Eq.trans, Function.Embedding, funext, congrFun', Iff.intro, dite, LT.lt, Or.inl, Exists.intro and 8 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.disjoint_map_map line 969 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Disjoint, Finset, Fin, HMul.hMul, OfNat.ofNat, Finset.map, Function.Embedding.mk, Imo2020P3.apeb, Imo2020P3.apeb_inj, Finset.univ, Imo2020P3.bpeb, Imo2020P3.bpeb_inj
Proof uses: Eq.mpr, Membership.mem, Not, id, Eq, congrArg, propext, Finset.disjoint_left, Exists, False, Eq.mp, Eq.trans, And, Function.Embedding, funext, True, congrFun', true_and, Imo2020P3.apeb_ne_bpeb, Eq.symm
20 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.pg_deg line 978 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Eq, Finset.card, Finset.filter, Finset.univ, Finset.sum, Imo2020P3.mult, Imo2020P3.pgA, Imo2020P3.pgB
Proof uses: Eq.mpr, HAdd.hAdd, ite, Imo2020P3.apeb, Imo2020P3.bpeb, id, congrArg, Finset.sum_congr, rfl, Finset, Membership.mem, Imo2020P3.mult.eq_1, Imo2020P3.pgA.eq_1, Imo2020P3.pgB.eq_1, Eq.refl, Finset.sum_add_distrib, Eq.mp, Function.Embedding, Function.Embedding.mk, Imo2020P3.apeb_inj and 10 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.weight_sum line 987 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Bool, Eq, Finset.sum, Finset.filter, Imo2020P3.pairOf, Bool.true, Finset.univ, HAdd.hAdd, Finset.card
Proof uses: Set.PairwiseDisjoint, Finset, Insert.insert, Imo2020P3.apeb, Singleton.singleton, Imo2020P3.bpeb, Membership.mem, Set, Ne, Eq.mpr, Function.onFun, Disjoint, id, congrArg, Function.onFun.eq_1, Not, propext, Finset.disjoint_left, Or, False and 30 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.red_card line 1024 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Eq, Finset.card, Finset.filter, Finset.univ, Bool, Finset.sum, ite, Bool.true, Imo2020P3.mult, Imo2020P3.pgA, Imo2020P3.pgB
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, HSMul.hSMul, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Finset.sum_const, Fintype.card_fin, nsmul_eq_mul, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 32 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P3.compl_filter_pairOf line 1044 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Bool, Eq, Finset, Compl.compl, Finset.filter, Imo2020P3.pairOf, Bool.true, Finset.univ, Bool.not
Proof uses: Finset.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Bool.false, True, congr, congrArg, And, congrFun', Not, Finset.compl_filter, Finset.filter_congr, Iff.of_eq, Bool.not_eq_true, true_and, Bool.not_true, iff_self
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
problem Imo2020P3.imo2020_p3 line 1054 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HMul.hMul, OfNat.ofNat, Eq, Finset.card, Finset.filter, Finset.univ, Exists, Finset, And, Finset.sum, HAdd.hAdd, Compl.compl
Proof uses: Bool, ite, Bool.true, Imo2020P3.mult, Imo2020P3.pgA, Imo2020P3.pgB, Imo2020P3.two_factor, Imo2020P3.pg_deg, Imo2020P3.red_card, Exists.intro, Imo2020P3.pairOf, And.intro, Eq.mpr, Bool.not, id, congrArg, Imo2020P3.compl_filter_pairOf, Imo2020P3.weight_sum, HMul, Eq.rec and 57 more
41 instances, coercions and auxiliary constants left out.

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