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

29 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2019, Problem 3

A social network has 2019 users, some pairs of which are friends (friendship is symmetric). If A, B, C are three users such that AB are friends and AC are friends but BC is not, then the administrator may perform the following operation: change the friendships such that BC are friends, but AB and AC are no longer friends. Initially, 1009 users have 1010 friends and 1010 users have 1009 friends. Prove that the administrator can make a sequence of operations such that all users have at most 1 friend.

Imports (4)

Imported by 1 file

Compfiles.lean

def Imo2019P3.Toggle Documented declaration: Toggle line 48 source
Source documentation
The operation of the problem: if a is friends with both b and c, but b and c are not friends, then the friendships ab and ac are deleted and the friendship bc is created. Toggle G G' says that G' is obtained from G by one such operation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph
Proof uses: Exists, And, Ne, SimpleGraph.Adj, Not, Eq, Max.max, SimpleGraph.deleteEdges, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, SimpleGraph.fromEdgeSet
3 instances, coercions and auxiliary constants left out.
```
def Toggle {V : Type*} (G G' : SimpleGraph V) : Prop :=
…
```
lemma Imo2019P3.toggle_adj Adjacency in a toggled graph line 58 source
Source documentation
Adjacency in a toggled graph.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Iff, SimpleGraph.Adj, Max.max, SimpleGraph.deleteEdges, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, SimpleGraph.fromEdgeSet, Or, And, Ne, Eq
Proof uses: Eq.mpr, id, congrArg, propext, SimpleGraph.sup_adj, Not, Membership.mem, SimpleGraph.deleteEdges_adj, SimpleGraph.fromEdgeSet_adj, of_eq_true, Eq.trans, True, congrFun', congr, iff_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma toggle_adj {G : SimpleGraph V} {a b c x y : V} :
    ((G.deleteEdges {s(a, b), s(a, c)}) ⊔ fromEdgeSet {s(b, c)}).Adj x y ↔
      (G.Adj x y ∧ s(x, y) ≠ s(a, b) ∧ s(x, y) ≠ s(a, c)) ∨ (s(x, y) = s(b, c) ∧ x ≠ y) := by
…
```
lemma Imo2019P3.sym2_ne A helper for Sym2 inequality: to show s(x, y) ≠ s(z, w) it suffices to discharge both pairings line 67 source
Source documentation
A helper for Sym2 inequality: to show s(x, y) ≠ s(z, w) it suffices to discharge both pairings.

standard axioms: Quot.sound, propext what this means
Statement uses: Or, Ne, Sym2, Sym2.mk
Proof uses: Eq, And, False, Eq.mp, congrArg, propext, Sym2.eq_iff, Or.elim
2 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma sym2_ne {x y z w : V} (h1 : x ≠ z ∨ y ≠ w) (h2 : x ≠ w ∨ y ≠ z) :
    s(x, y) ≠ s(z, w) := by
…
```
lemma Imo2019P3.toggle_adj_a Adjacency with a in a toggled graph: a keeps exactly its neighbors different from b and c line 78 source
Source documentation
Adjacency with a in a toggled graph: a keeps exactly its neighbors different from b and c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, SimpleGraph.Adj, Iff, Max.max, SimpleGraph.deleteEdges, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, SimpleGraph.fromEdgeSet, And, Ne
Proof uses: SimpleGraph.ne_of_adj, Eq.mpr, Or, Eq, id, congrArg, propext, Imo2019P3.toggle_adj, Iff.intro, And.intro, Eq.refl, Eq.mp, Sym2.eq_iff, absurd, Or.inl, Imo2019P3.sym2_ne, Or.inr
8 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma toggle_adj_a {G : SimpleGraph V} {a b c : V}
    (hab : G.Adj a b) (hac : G.Adj a c) (w : V) :
    ((G.deleteEdges {s(a, b), s(a, c)}) ⊔ fromEdgeSet {s(b, c)}).Adj a w ↔
      G.Adj a w ∧ w ≠ b ∧ w ≠ c := by
…
```
lemma Imo2019P3.toggle_adj_b Adjacency with b in a toggled graph: b loses a and gains c line 102 source
Source documentation
Adjacency with b in a toggled graph: b loses a and gains c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Ne, SimpleGraph.Adj, Iff, Max.max, SimpleGraph.deleteEdges, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, SimpleGraph.fromEdgeSet, Or, Eq, And
Proof uses: SimpleGraph.ne_of_adj, Eq.mpr, id, congrArg, propext, Imo2019P3.toggle_adj, Iff.intro, Or.inr, And.intro, Eq.rec, Sym2.eq_swap, Eq.mp, Sym2.eq_iff, Or.inl, rfl, absurd, Imo2019P3.sym2_ne, Ne.symm
9 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma toggle_adj_b {G : SimpleGraph V} {a b c : V} (hbc : b ≠ c)
    (hab : G.Adj a b) (w : V) :
    ((G.deleteEdges {s(a, b), s(a, c)}) ⊔ fromEdgeSet {s(b, c)}).Adj b w ↔
      (w = c ∨ (G.Adj b w ∧ w ≠ a)) := by
…
```
lemma Imo2019P3.toggle_adj_c Adjacency with c in a toggled graph: c loses a and gains b line 127 source
Source documentation
Adjacency with c in a toggled graph: c loses a and gains b.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Ne, SimpleGraph.Adj, Iff, Max.max, SimpleGraph.deleteEdges, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, SimpleGraph.fromEdgeSet, Or, Eq, And
Proof uses: SimpleGraph.ne_of_adj, Eq.mpr, id, congrArg, propext, Imo2019P3.toggle_adj, Iff.intro, Or.inr, And.intro, Eq.rec, Sym2.eq_swap, Eq.mp, Sym2.eq_iff, absurd, Ne.symm, Or.inl, rfl, Imo2019P3.sym2_ne
9 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma toggle_adj_c {G : SimpleGraph V} {a b c : V} (hbc : b ≠ c)
    (hac : G.Adj a c) (w : V) :
    ((G.deleteEdges {s(a, b), s(a, c)}) ⊔ fromEdgeSet {s(b, c)}).Adj c w ↔
      (w = b ∨ (G.Adj c w ∧ w ≠ a)) := by
…
```
lemma Imo2019P3.toggle_adj_of_ne Adjacency with a vertex different from a, b, c is unchanged by a toggle line 152 source
Source documentation
Adjacency with a vertex different from a, b, c is unchanged by a toggle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Ne, Iff, SimpleGraph.Adj, Max.max, SimpleGraph.deleteEdges, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, SimpleGraph.fromEdgeSet
Proof uses: Eq.mpr, Or, And, Eq, id, congrArg, propext, Imo2019P3.toggle_adj, Iff.intro, Eq.mp, Sym2.eq_iff, absurd, Or.inl, And.intro, Imo2019P3.sym2_ne
8 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma toggle_adj_of_ne {G : SimpleGraph V} {a b c v : V}
    (hva : v ≠ a) (hvb : v ≠ b) (hvc : v ≠ c) (w : V) :
    ((G.deleteEdges {s(a, b), s(a, c)}) ⊔ fromEdgeSet {s(b, c)}).Adj v w ↔ G.Adj v w := by
…
```
lemma Imo2019P3.degree_eq_card_filter Degree as the cardinality of a filter line 173 source
Source documentation
Degree as the cardinality of a filter. Stated with an explicit decidability instance so that all synthesized instances agree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Finset.card, Finset.filter, Finset.univ
Proof uses: Eq.mpr, SimpleGraph.neighborFinset, id, congrArg, Eq.symm, SimpleGraph.card_neighborFinset_eq_degree, Finset, SimpleGraph.neighborFinset_eq_filter, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma degree_eq_card_filter (H : SimpleGraph V) [DecidableRel H.Adj] (v : V) :
    H.degree v = #(Finset.univ.filter (H.Adj v)) := by
…
```
lemma Imo2019P3.Toggle.degree_parity A toggle preserves the parity of every degree line 178 source
Source documentation
A toggle preserves the parity of every degree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Imo2019P3.Toggle, Eq, Nat, HMod.hMod, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Classical.propDecidable, SimpleGraph.Adj, OfNat.ofNat
Proof uses: Exists, And, Ne, Not, Max.max, SimpleGraph.deleteEdges, Insert.insert, Sym2, Sym2.mk, Singleton.singleton, SimpleGraph.fromEdgeSet, Finset.card, Finset.filter, Finset.univ, dite, Eq.mpr, id, congrArg, Finset, Finset.erase and 45 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
lemma Toggle.degree_parity {G G' : SimpleGraph V} (hT : Toggle G G') (v : V) :
    G'.degree v % 2 = G.degree v % 2 := by
…
```
Mentions: Imo2019P3.Toggle
lemma Imo2019P3.Toggle.exists_odd_degree A toggle preserves the existence of a vertex of odd degree line 249 source
Source documentation
A toggle preserves the existence of a vertex of odd degree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Imo2019P3.Toggle, Exists, Odd, Nat, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Classical.propDecidable, SimpleGraph.Adj
Proof uses: Exists.intro, Eq.mpr, Eq, HMod.hMod, OfNat.ofNat, id, congrArg, propext, Nat.odd_iff, Imo2019P3.Toggle.degree_parity, Eq.symm
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma Toggle.exists_odd_degree {G G' : SimpleGraph V} (hT : Toggle G G') :
    (∃ v, Odd (G.degree v)) → ∃ v, Odd (G'.degree v) := by
…
```
Mentions: Imo2019P3.Toggle
lemma Imo2019P3.edgeSet_toggle The edge set of a toggled graph line 256 source
Source documentation
The edge set of a toggled graph.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Ne, Eq, Set, Sym2, SimpleGraph.edgeSet, Max.max, SimpleGraph.deleteEdges, Insert.insert, Sym2.mk, Singleton.singleton, SimpleGraph.fromEdgeSet, Union.union, SDiff.sdiff
Proof uses: Eq.mpr, id, congrArg, SimpleGraph.edgeSet_sup, SimpleGraph.edgeSet_deleteEdges, Sym2.diagSet, SimpleGraph.edgeSet_fromEdgeSet, Set.ext, Iff, Membership.mem, Or, And, Not, congr, Eq.trans, congrFun', Iff.intro, Or.inl, And.intro, Or.inr and 8 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma edgeSet_toggle {G : SimpleGraph V} {a b c : V} (hbc : b ≠ c) :
    ((G.deleteEdges {s(a, b), s(a, c)}) ⊔ fromEdgeSet {s(b, c)}).edgeSet
      = (G.edgeSet \ {s(a, b), s(a, c)}) ∪ {s(b, c)} := by
…
```
lemma Imo2019P3.Toggle.edgeFinset_card A toggle removes exactly one edge line 273 source
Source documentation
A toggle removes exactly one edge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Imo2019P3.Toggle, Eq, Nat, HAdd.hAdd, Finset.card, Sym2, SimpleGraph.edgeFinset, Classical.propDecidable, SimpleGraph.Adj, OfNat.ofNat
Proof uses: Exists, And, Ne, Not, Max.max, SimpleGraph.deleteEdges, Insert.insert, Set, Sym2.mk, Singleton.singleton, SimpleGraph.fromEdgeSet, Set.ncard, SimpleGraph.edgeSet, Eq.symm, Set.toFinset, Set.ncard_eq_toFinset_card', Eq.mpr, id, congrArg, Union.union and 27 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma Toggle.edgeFinset_card {G G' : SimpleGraph V} (hT : Toggle G G') :
    G'.edgeFinset.card + 1 = G.edgeFinset.card := by
…
```
Mentions: Imo2019P3.Toggle
lemma Imo2019P3.Toggle.ne_top A graph obtained by a toggle is never complete: a and b are no longer friends line 297 source
Source documentation
A graph obtained by a toggle is never complete: a and b are no longer friends.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Imo2019P3.Toggle, Ne, Top.top
Proof uses: Exists, And, SimpleGraph.Adj, Not, Eq, Max.max, SimpleGraph.deleteEdges, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, SimpleGraph.fromEdgeSet, Eq.mpr, id, congrArg, Iff.mpr, SimpleGraph.top_adj, SimpleGraph.ne_of_adj, And.left and 6 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma Toggle.ne_top {G G' : SimpleGraph V} (hT : Toggle G G') : G' ≠ ⊤ := by
…
```
Mentions: Imo2019P3.Toggle
lemma Imo2019P3.reachable_of_forall_adj_reachable Lifting reachability along adjacencies that remain reachable line 308 source
Source documentation
Lifting reachability along adjacencies that remain reachable.

no axioms what this means
Statement uses: SimpleGraph, SimpleGraph.Adj, SimpleGraph.Reachable
Proof uses: SimpleGraph.Walk, SimpleGraph.Walk.rec, Nonempty.intro, SimpleGraph.Walk.nil, SimpleGraph.Reachable.trans
1 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma reachable_of_forall_adj_reachable {G H : SimpleGraph V} (a : V)
    (hlift : ∀ x y : V, G.Adj x y → H.Reachable x y) :
    ∀ x : V, G.Reachable x a → H.Reachable x a := by
…
```
lemma Imo2019P3.connected_toggle If the endpoints a, c of the deleted edges of a toggle remain reachable in the twice-deleted graph, then the toggle preserves connectedness line 320 source
Source documentation
If the endpoints a, c of the deleted edges of a toggle remain reachable in the twice-deleted graph, then the toggle preserves connectedness.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, Ne, SimpleGraph.Connected, SimpleGraph.Reachable, SimpleGraph.deleteEdges, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, Max.max, SimpleGraph.fromEdgeSet
Proof uses: SimpleGraph.Reachable.mono, le_sup_left, SimpleGraph.Adj, Iff.mpr, Or, SimpleGraph.sup_adj, Or.inr, And, Membership.mem, SimpleGraph.fromEdgeSet_adj, And.intro, Set.mem_singleton, SimpleGraph.Reachable.trans, SimpleGraph.Reachable.symm, SimpleGraph.Adj.reachable, dite, Eq, Eq.mp, congrArg, propext and 17 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma connected_toggle {G : SimpleGraph V} {a b c : V} (hbc : b ≠ c)
    (hconn : G.Connected)
    (hr : (G.deleteEdges {s(a, b), s(a, c)}).Reachable a c) :
    ((G.deleteEdges {s(a, b), s(a, c)}) ⊔ fromEdgeSet {s(b, c)}).Connected := by
…
```
lemma Imo2019P3.exists_adj_crossing A walk from outside a set S to inside S crosses the boundary of S line 352 source
Source documentation
A walk from outside a set S to inside S crosses the boundary of S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Set, SimpleGraph.Walk, Not, Membership.mem, Exists, And, SimpleGraph.Adj
Proof uses: SimpleGraph.Walk.rec, absurd, dite, Classical.propDecidable, Exists.intro, And.intro
2 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma exists_adj_crossing {G : SimpleGraph V} (S : Set V) {u v : V} (p : G.Walk u v) :
    u ∉ S → v ∈ S → ∃ b a : V, b ∉ S ∧ a ∈ S ∧ G.Adj b a := by
…
```
Mentions: S
lemma Imo2019P3.isPath_transfer IsPath is preserved by Walk.transfer line 364 source
Source documentation
IsPath is preserved by Walk.transfer.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, SimpleGraph.Walk, Sym2, Membership.mem, List, SimpleGraph.Walk.edges, Set, SimpleGraph.edgeSet, Iff, SimpleGraph.Walk.IsPath, SimpleGraph.Walk.transfer
Proof uses: Eq.mpr, List.Nodup, SimpleGraph.Walk.support, id, Eq, congrArg, propext, SimpleGraph.Walk.isPath_def, SimpleGraph.Walk.support_transfer, Iff.rfl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma isPath_transfer {G H : SimpleGraph V} {u v : V} {p : G.Walk u v}
    (hp : ∀ e, e ∈ p.edges → e ∈ H.edgeSet) :
    (p.transfer H hp).IsPath ↔ p.IsPath := by
…
```
lemma Imo2019P3.exists_isPath_of_snd_eq If the second vertex of a cycle C at x is y, then deleting the first edge leaves a path from x to y avoiding it line 372 source
Source documentation
If the second vertex of a cycle C at x is y, then deleting the first edge leaves a path from x to y avoiding it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, Eq, SimpleGraph.Walk.snd, Exists, And, SimpleGraph.Walk.IsPath, Not, Membership.mem, Sym2, List, SimpleGraph.Walk.edges, Sym2.mk
Proof uses: SimpleGraph.Walk.Nil, SimpleGraph.Walk.IsCycle.not_nil, SimpleGraph.Walk.tail, Iff.mp, SimpleGraph.Walk.cons, SimpleGraph.Walk.adj_snd, SimpleGraph.Walk.cons_isCycle_iff, Eq.rec, Eq.symm, SimpleGraph.Walk.cons_tail_eq, Exists.intro, SimpleGraph.Walk.reverse, And.intro, SimpleGraph.Walk.IsPath.reverse, Eq.mpr, List.reverse, id, congrArg, SimpleGraph.Walk.edges_reverse, propext and 5 more
4 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma exists_isPath_of_snd_eq {G : SimpleGraph V} {x y : V} {C : G.Walk x x}
    (hC : C.IsCycle) (hy : C.snd = y) :
    ∃ q : G.Walk x y, q.IsPath ∧ s(x, y) ∉ q.edges ∧ ∀ e ∈ q.edges, e ∈ C.edges := by
…
```
lemma Imo2019P3.exists_isPath_of_mem_edges_of_isCycle Removing an edge from a cycle leaves a path between its endpoints, avoiding that edge line 390 source
Source documentation
Removing an edge from a cycle leaves a path between its endpoints, avoiding that edge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, Membership.mem, Sym2, List, SimpleGraph.Walk.edges, Sym2.mk, Ne, Exists, And, SimpleGraph.Walk.IsPath, Not
Proof uses: SimpleGraph.Walk.support, SimpleGraph.Walk.fst_mem_support_of_mem_edges, SimpleGraph.Walk.rotate, SimpleGraph.Walk.IsCycle.rotate, Iff.mpr, List.Perm.mem_iff, List.IsRotated.perm, SimpleGraph.Walk.rotate_edges, Iff.mp, SimpleGraph.Walk.Nil, SimpleGraph.Walk.IsCycle.not_nil, Eq, List.cons, SimpleGraph.Walk.snd, SimpleGraph.Walk.tail, Eq.mpr, SimpleGraph.Walk.cons, SimpleGraph.Walk.adj_snd, id, Eq.rec and 27 more
5 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma exists_isPath_of_mem_edges_of_isCycle {G : SimpleGraph V} {v : V} {C : G.Walk v v}
    (hC : C.IsCycle) {x y : V} (he : s(x, y) ∈ C.edges) (_hxy : x ≠ y) :
    ∃ q : G.Walk x y, q.IsPath ∧ s(x, y) ∉ q.edges ∧ ∀ e ∈ q.edges, e ∈ C.edges := by
…
```
lemma Imo2019P3.mem_edges_of_length_eq_one A length-1 walk from x to y contains the edge s(x, y) line 431 source
Source documentation
A length-1 walk from x to y contains the edge s(x, y).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, SimpleGraph.Walk, Ne, Eq, Nat, SimpleGraph.Walk.length, OfNat.ofNat, Membership.mem, Sym2, List, SimpleGraph.Walk.edges, Sym2.mk
Proof uses: Not, SimpleGraph.Walk.Nil, SimpleGraph.Walk.not_nil_of_ne, SimpleGraph.Walk.snd, SimpleGraph.Walk.tail, HAdd.hAdd, SimpleGraph.Walk.length_tail_add_one, Iff.mp, Exists, SimpleGraph.Walk.exists_length_eq_zero_iff, Exists.intro, SimpleGraph.Walk.mk_start_snd_mem_edges, Eq.mp, congrArg
7 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma mem_edges_of_length_eq_one {G : SimpleGraph V} {x y : V} {q : G.Walk x y}
    (hxy : x ≠ y) (hl : q.length = 1) : s(x, y) ∈ q.edges := by
…
```
lemma Imo2019P3.IsCycle.mem_edges_of_adj A cycle of length equal to the girth is chordless: every edge of G between two vertices of the cycle is already an edge of the cycle line 444 source
Source documentation
A cycle of length equal to the girth is chordless: every edge of G between two vertices of the cycle is already an edge of the cycle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, Eq, Nat, SimpleGraph.girth, SimpleGraph.Walk.length, Membership.mem, List, SimpleGraph.Walk.support, SimpleGraph.Adj, Sym2, SimpleGraph.Walk.edges, Sym2.mk
Proof uses: Decidable.byContradiction, Not, Ne, SimpleGraph.ne_of_adj, SimpleGraph.Walk.rotate, SimpleGraph.Walk.IsCycle.rotate, Eq.mpr, id, congrArg, propext, SimpleGraph.Walk.mem_support_rotate_iff, SimpleGraph.Walk.IsPath, SimpleGraph.Walk.takeUntil, SimpleGraph.Walk.IsCycle.isPath_takeUntil, rfl, SimpleGraph.Walk.dropUntil, SimpleGraph.Walk.append, SimpleGraph.Walk.take_spec, HAdd.hAdd, congr_arg and 33 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 55 steps
Open to load the checked before-and-after goal states.
```
lemma IsCycle.mem_edges_of_adj {G : SimpleGraph V} {v : V} {C : G.Walk v v}
    (hC : C.IsCycle) (hg : G.girth = C.length) {x y : V}
    (hx : x ∈ C.support) (hy : y ∈ C.support) (hxy : G.Adj x y) :
    s(x, y) ∈ C.edges := by
…
```
lemma Imo2019P3.degree_eq_two_of_forall_mem_support On a chordless cycle that spans all vertices, every vertex has degree 2 line 502 source
Source documentation
On a chordless cycle that spans all vertices, every vertex has degree 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, Membership.mem, List, SimpleGraph.Walk.support, SimpleGraph.Adj, Sym2, SimpleGraph.Walk.edges, Sym2.mk, Eq, Nat, SimpleGraph.degree, Set, SimpleGraph.neighborSet, Classical.propDecidable, OfNat.ofNat
Proof uses: SimpleGraph.Walk.rotate, SimpleGraph.Walk.IsCycle.rotate, Not, SimpleGraph.Walk.Nil, SimpleGraph.Walk.IsCycle.not_nil, Iff.mpr, List.Perm.mem_iff, List.IsRotated.perm, SimpleGraph.Walk.rotate_edges, List.cons, SimpleGraph.Walk.snd, SimpleGraph.Walk.tail, Eq.mpr, SimpleGraph.Walk.cons, SimpleGraph.Walk.adj_snd, id, Eq.rec, Eq.refl, Eq.trans, congrArg and 35 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma degree_eq_two_of_forall_mem_support {G : SimpleGraph V} {v : V} {C : G.Walk v v}
    (hC : C.IsCycle)
    (hchord : ∀ x y : V, x ∈ C.support → y ∈ C.support → G.Adj x y → s(x, y) ∈ C.edges)
    (hspan : ∀ z : V, z ∈ C.support) (z : V) :
    G.degree z = 2 := by
…
```
lemma Imo2019P3.isCycle_triangle Three pairwise adjacent vertices form a cycle of length 3 line 548 source
Source documentation
Three pairwise adjacent vertices form a cycle of length 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, SimpleGraph.Adj, And, SimpleGraph.Walk.IsCycle, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, Eq, Nat, SimpleGraph.Walk.length, OfNat.ofNat
Proof uses: Ne, SimpleGraph.ne_of_adj, And.intro, Iff.mpr, SimpleGraph.Walk.IsPath, Not, Membership.mem, Sym2, List, SimpleGraph.Walk.edges, Sym2.mk, SimpleGraph.Walk.cons_isCycle_iff, Eq.mpr, List.Nodup, SimpleGraph.Walk.support, id, congrArg, propext, SimpleGraph.Walk.isPath_def, of_eq_true and 18 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma isCycle_triangle {G : SimpleGraph V} {a b c : V} (hab : G.Adj a b) (hbc : G.Adj b c)
    (hca : G.Adj c a) :
    (Walk.cons hab (Walk.cons hbc (Walk.cons hca Walk.nil))).IsCycle
      ∧ (Walk.cons hab (Walk.cons hbc (Walk.cons hca Walk.nil))).length = 3 := by
…
```
lemma Imo2019P3.exists_notMem_support_of_isCycle If G has a vertex of odd degree, a girth-realizing cycle cannot span all vertices line 570 source
Source documentation
If G has a vertex of odd degree, a girth-realizing cycle cannot span all vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, Eq, Nat, SimpleGraph.girth, SimpleGraph.Walk.length, Exists, Odd, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Classical.propDecidable, SimpleGraph.Adj, Not, List, SimpleGraph.Walk.support
Proof uses: Decidable.byContradiction, False, OfNat.ofNat, Imo2019P3.degree_eq_two_of_forall_mem_support, Imo2019P3.IsCycle.mem_edges_of_adj, Eq.mp, Eq.trans, binderNameHint, forall_congr, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, congrArg
20 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma exists_notMem_support_of_isCycle {G : SimpleGraph V} {v : V} {C : G.Walk v v}
    (hC : C.IsCycle) (hg : G.girth = C.length) (hodd : ∃ z, Odd (G.degree z)) :
    ∃ z, z ∉ C.support := by
…
```
lemma Imo2019P3.exists_toggle_connected Key claim: a connected graph that is not a tree, has a vertex of odd degree, and is not complete admits a toggle after which it is still connected line 583 source
Source documentation
Key claim: a connected graph that is not a tree, has a vertex of odd degree, and is not complete admits a toggle after which it is still connected.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, SimpleGraph.Connected, Not, SimpleGraph.IsTree, Exists, Odd, Nat, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Classical.propDecidable, SimpleGraph.Adj, Ne, Top.top, And, Imo2019P3.Toggle
Proof uses: SimpleGraph.IsAcyclic, SimpleGraph.IsTree.mk, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, Eq, SimpleGraph.girth, SimpleGraph.Walk.length, Iff.mpr, SimpleGraph.exists_girth_eq_length, LE.le, OfNat.ofNat, SimpleGraph.Walk.IsCircuit.three_le_length, SimpleGraph.Walk.IsCycle.isCircuit, LT.lt, GE.ge, Or, Nat.lt_or_ge, SimpleGraph.Walk.Nil, SimpleGraph.Walk.IsCycle.not_nil, SimpleGraph.Walk.snd and 95 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 144 steps
Open to load the checked before-and-after goal states.
```
lemma exists_toggle_connected (G : SimpleGraph V) (hconn : G.Connected) (htree : ¬ G.IsTree)
    (hodd : ∃ v, Odd (G.degree v)) (hne : G ≠ ⊤) :
    ∃ G', Toggle G G' ∧ G'.Connected := by
…
```
Mentions: Imo2019P3.Toggle
lemma Imo2019P3.exists_isTree_of_connected Phase 1: any connected graph with a vertex of odd degree that is not complete can be toggled to a tree line 738 source
Source documentation
Phase 1: any connected graph with a vertex of odd degree that is not complete can be toggled to a tree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, SimpleGraph.Connected, Exists, Odd, Nat, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Classical.propDecidable, SimpleGraph.Adj, Ne, Top.top, And, Relation.ReflTransGen, Imo2019P3.Toggle, SimpleGraph.IsTree
Proof uses: LE.le, Finset.card, Sym2, SimpleGraph.edgeFinset, Nat.recAux, OfNat.ofNat, Eq, SimpleGraph.degree_le_card_edgeFinset, absurd, Eq.mp, congrArg, of_decide_eq_true, Not, id, Bool, Decidable.decide, Bool.true, Eq.refl, HAdd.hAdd, dite and 9 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma exists_isTree_of_connected (G : SimpleGraph V) (hconn : G.Connected)
    (hodd : ∃ v, Odd (G.degree v)) (hne : G ≠ ⊤) :
    ∃ G', Relation.ReflTransGen Toggle G G' ∧ G'.IsTree := by
…
```
Mentions: Imo2019P3.Toggle
lemma Imo2019P3.isAcyclic_toggle A toggle preserves acyclicity line 769 source
Source documentation
A toggle preserves acyclicity.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, Imo2019P3.Toggle, SimpleGraph.IsAcyclic
Proof uses: Exists, And, Ne, SimpleGraph.Adj, Not, Eq, Max.max, SimpleGraph.deleteEdges, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, SimpleGraph.fromEdgeSet, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, dite, False, Membership.mem, List and 58 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
lemma isAcyclic_toggle {G G' : SimpleGraph V} (hT : Toggle G G') (hacyc : G.IsAcyclic) :
    G'.IsAcyclic := by
…
```
Mentions: Imo2019P3.Toggle
lemma Imo2019P3.exists_matching_of_isAcyclic Phase 2: any forest can be toggled to a graph in which every vertex has degree at most 1 line 836 source
Source documentation
Phase 2: any forest can be toggled to a graph in which every vertex has degree at most 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, SimpleGraph.IsAcyclic, Exists, And, Relation.ReflTransGen, Imo2019P3.Toggle, LE.le, Nat, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Classical.propDecidable, SimpleGraph.Adj, OfNat.ofNat
Proof uses: Finset.card, Sym2, SimpleGraph.edgeFinset, Nat.recAux, Exists.intro, And.intro, Relation.ReflTransGen.refl, SimpleGraph.degree_le_card_edgeFinset, HAdd.hAdd, dite, Not, LT.lt, Eq.mp, Eq.trans, congrArg, funext, Finset, SimpleGraph.neighborFinset, Ne, propext and 22 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma exists_matching_of_isAcyclic (G : SimpleGraph V) (hacyc : G.IsAcyclic) :
    ∃ G', Relation.ReflTransGen Toggle G G' ∧ ∀ v, G'.degree v ≤ 1 := by
…
```
Mentions: Imo2019P3.Toggle
problem Imo2019P3.imo2019_p3 line 871 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat, Eq, Finset.card, Finset.filter, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Classical.propDecidable, SimpleGraph.Adj, Finset.univ, Exists, And, Relation.ReflTransGen, Imo2019P3.Toggle, LE.le
Proof uses: Or, Disjoint, Finset, Eq.mpr, Not, id, congrArg, propext, Finset.disjoint_left, Finset.mem_filter, False, Eq.mp, Union.union, Finset.eq_univ_of_card, Fintype.card, HAdd.hAdd, Finset.card_union_of_disjoint, Fintype.card_fin, Eq.refl, Finset.mem_univ and 64 more
73 instances, coercions and auxiliary constants left out.

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