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

19 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1991, Problem 4

Suppose G is a connected graph with k edges. Prove that it is possible to label the edges 1, 2, ... , k in such a way that at each vertex which belongs to two or more edges, the greatest common divisor of the integers labeling those edges is equal to 1.

Imports (6)

Imported by 1 file

Compfiles.lean

def Imo1991P4.interiorVerts The vertices that a walk visits at an interior position: all w.getVert (i + 1) with i + 1 < w.length line 41 source
Source documentation
The vertices that a walk visits at an interior position: all w.getVert (i + 1) with i + 1 < w.length. At each such vertex two consecutive edges of the walk meet.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, SimpleGraph.Walk, Finset
Proof uses: Finset.image, Nat, SimpleGraph.Walk.getVert, HAdd.hAdd, OfNat.ofNat, Finset.range, HSub.hSub, SimpleGraph.Walk.length
5 instances, coercions and auxiliary constants left out.
```
def interiorVerts {u v : V} (w : G.Walk u v) : Finset V :=
…
```
lemma Imo1991P4.mem_interiorVerts line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, SimpleGraph.Walk, Iff, Membership.mem, Finset, Imo1991P4.interiorVerts, Exists, Nat, And, LT.lt, HSub.hSub, SimpleGraph.Walk.length, OfNat.ofNat, Eq, SimpleGraph.Walk.getVert, HAdd.hAdd
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.image, Finset.range, funext, iff_self
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P4.start_or_interior_or_end Every vertex of a walk is its start, an interior vertex, or its end line 51 source
Source documentation
Every vertex of a walk is its start, an interior vertex, or its end.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, SimpleGraph.Walk, Membership.mem, List, SimpleGraph.Walk.support, Or, Eq, Finset, Imo1991P4.interiorVerts
Proof uses: LT.lt, Nat, List.idxOf, List.length, List.idxOf_lt_length_of_mem, HAdd.hAdd, SimpleGraph.Walk.length, OfNat.ofNat, SimpleGraph.Walk.length_support, SimpleGraph.Walk.getVert, SimpleGraph.Walk.getVert_support_idxOf, rfl, LE.le, Eq.mp, congrArg, Nat.lt_or_eq_of_le, GT.gt, Nat.eq_zero_or_pos, Or.inl, Eq.mpr and 14 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma start_or_interior_or_end {u v : V} {w : G.Walk u v} {x : V} (hx : x ∈ w.support) :
    x = u ∨ x ∈ interiorVerts w ∨ x = v := by
…
```
Mentions: Imo1991P4.interiorVerts
lemma Imo1991P4.exists_maximal_trail A maximal-length trail starting from s₀, which exists whenever s₀ has an incident edge line 72 source
Source documentation
A maximal-length trail starting from s₀, which exists whenever s₀ has an incident edge. It ends at a vertex all of whose incident edges are used by the trail.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Exists, SimpleGraph.Walk, And, SimpleGraph.Walk.IsTrail, LE.le, Nat, OfNat.ofNat, SimpleGraph.Walk.length, Membership.mem, Sym2, List, SimpleGraph.Walk.edges, Sym2.mk
Proof uses: Finset, Finset.filter, Eq, Classical.propDecidable, Finset.range, HAdd.hAdd, Finset.card, SimpleGraph.edgeFinset, rfl, Eq.mpr, id, Eq.trans, congrFun', congrArg, True, LT.lt, true_and, Exists.intro, SimpleGraph.Walk.nil, And.intro and 28 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
lemma exists_maximal_trail {s₀ : V} (h : ∃ x, G.Adj s₀ x) :
    ∃ (t : V) (w : G.Walk s₀ t), w.IsTrail ∧ 1 ≤ w.length ∧
      ∀ x : V, G.Adj t x → s(t, x) ∈ w.edges := by
…
```
Mentions: h
lemma Imo1991P4.find_good Documented declaration: find_good line 115 source
Source documentation
Key walk lemma: from a vertex u that still has an edge outside the trail w, one can walk to a vertex of S, to the start of w, or to an interior vertex of w, using only edges outside the trail.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, SimpleGraph.Walk, SimpleGraph.Adj, Membership.mem, Sym2, List, SimpleGraph.Walk.edges, Sym2.mk, Finset, Or, SimpleGraph.Walk.support, Exists, SimpleGraph.deleteEdges, List.toFinset, And, Eq, Imo1991P4.interiorVerts, SimpleGraph.Reachable
Proof uses: SimpleGraph.Walk.rec, Exists.intro, And.intro, Or.inl, SimpleGraph.Reachable.refl, Imo1991P4.start_or_interior_or_end, Or.inr, Eq.mp, congrArg, absurd, And.left, Not, Set, propext, SimpleGraph.deleteEdges_adj, congrFun', Set.ofPred, List.coe_toFinset, And.right, dite and 7 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
lemma find_good {s₀ t : V} (w : G.Walk s₀ t)
    (hmax : ∀ x : V, G.Adj t x → s(t, x) ∈ w.edges)
    (S : Finset V) {u z : V} (W : G.Walk u z) :
    (z ∈ S ∨ z ∈ w.support) → (∃ x, (G.deleteEdges (↑w.edges.toFinset)).Adj u x) →
    ∃ s', (s' ∈ S ∨ s' = s₀ ∨ s' ∈ interiorVerts w) ∧
      (G.deleteEdges (↑w.edges.toFinset)).Reachable u s' := by
…
```
Mentions: S, Imo1991P4.interiorVerts
lemma Imo1991P4.mem_edgeSet_deleteEdges Membership in the edge set of a graph with deleted edges line 160 source
Source documentation
Membership in the edge set of a graph with deleted edges.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Set, Sym2, Iff, Membership.mem, SimpleGraph.edgeSet, SimpleGraph.deleteEdges, And, Not
Proof uses: Sym2.ind, of_eq_true, Sym2.mk, Eq.trans, SimpleGraph.Adj, True, congr, congrArg, SDiff.sdiff, congrFun', SimpleGraph.edgeSet_deleteEdges, iff_self
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma mem_edgeSet_deleteEdges {s : Set (Sym2 V)} {e : Sym2 V} :
    e ∈ (G.deleteEdges s).edgeSet ↔ e ∈ G.edgeSet ∧ e ∉ s := by
…
```
def Imo1991P4.trailLabel The edge labeling given by a trail w (whose edges get the labels n + 1, …, n + w.length, in order) together with a labeling Φ' of the remaining edges line 168 source
Source documentation
The edge labeling given by a trail w (whose edges get the labels n + 1, …, n + w.length, in order) together with a labeling Φ' of the remaining edges.

standard axioms: Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, SimpleGraph.Walk, Nat, Sym2
Proof uses: ite, Membership.mem, List, SimpleGraph.Walk.edges, HAdd.hAdd, OfNat.ofNat, List.idxOf
8 instances, coercions and auxiliary constants left out.
```
def trailLabel {s₀ t : V} (w : G.Walk s₀ t) (n : ℕ) (Φ' : Sym2 V → ℕ) (e : Sym2 V) : ℕ :=
…
```
lemma Imo1991P4.trailLabel_of_mem line 172 source
standard axioms: Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, SimpleGraph.Walk, Nat, Sym2, Membership.mem, List, SimpleGraph.Walk.edges, Eq, Imo1991P4.trailLabel, HAdd.hAdd, OfNat.ofNat, List.idxOf
Proof uses: Eq.mpr, ite, id, congrArg, Imo1991P4.trailLabel.eq_1, ite_eq_left, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P4.trailLabel_of_not_mem line 177 source
standard axioms: Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, SimpleGraph.Walk, Nat, Sym2, Not, Membership.mem, List, SimpleGraph.Walk.edges, Eq, Imo1991P4.trailLabel
Proof uses: Eq.mpr, ite, HAdd.hAdd, OfNat.ofNat, List.idxOf, id, congrArg, Imo1991P4.trailLabel.eq_1, ite_eq_right, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P4.gcd_eq_one_of_consecutive If two elements of a finset have consecutive labels, the gcd of all labels is 1 line 183 source
Source documentation
If two elements of a finset have consecutive labels, the gcd of all labels is 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Sym2, Nat, Membership.mem, Eq, HAdd.hAdd, OfNat.ofNat, Finset.gcd
Proof uses: Dvd.dvd, Finset.gcd_dvd, HSub.hSub, Nat.dvd_sub, Iff.mp, Nat.dvd_one, Eq.mp, congrArg
20 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma gcd_eq_one_of_consecutive {s : Finset (Sym2 V)} {Φ : Sym2 V → ℕ} {e₁ e₂ : Sym2 V}
    (he₁ : e₁ ∈ s) (he₂ : e₂ ∈ s) (h : Φ e₁ + 1 = Φ e₂) :
    s.gcd Φ = 1 := by
…
```
Mentions: h
lemma Imo1991P4.gcd_eq_one_of_eq_one If some element of a finset has label 1, the gcd of all labels is 1 line 195 source
Source documentation
If some element of a finset has label 1, the gcd of all labels is 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Sym2, Nat, Membership.mem, Eq, OfNat.ofNat, Finset.gcd
Proof uses: Dvd.dvd, Finset.gcd_dvd, Iff.mp, Nat.dvd_one, Eq.mp, congrArg
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma gcd_eq_one_of_eq_one {s : Finset (Sym2 V)} {Φ : Sym2 V → ℕ} {e : Sym2 V}
    (he : e ∈ s) (h : Φ e = 1) : s.gcd Φ = 1 := by
…
```
Mentions: h
lemma Imo1991P4.gcd_attach_val The gcd over the attached finset, with the function applied to the underlying values, equals the gcd over the finset itself line 204 source
Source documentation
The gcd over the attached finset, with the function applied to the underlying values, equals the gcd over the finset itself.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Sym2, Nat, Eq, Finset.gcd, Subtype, Membership.mem, Finset.attach, Function.comp
Proof uses: Eq.mpr, Finset.image, id, congrArg, Eq.symm, Finset.gcd_image, Finset.attach_image_val, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma gcd_attach_val {s : Finset (Sym2 V)} {f : Sym2 V → ℕ} :
    s.attach.gcd (f ∘ Subtype.val) = s.gcd f := by
…
```
Mentions: f
lemma Imo1991P4.gcd_interior At an interior vertex of a trail, two consecutive edges meet, so the gcd of the labels at that vertex is 1 line 210 source
Source documentation
At an interior vertex of a trail, two consecutive edges meet, so the gcd of the labels at that vertex is 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Walk, SimpleGraph.Walk.IsTrail, Nat, Sym2, Membership.mem, Finset, Imo1991P4.interiorVerts, Eq, Finset.gcd, SimpleGraph.incidenceFinset, Set, SimpleGraph.neighborSet, Imo1991P4.trailLabel, OfNat.ofNat
Proof uses: And, LT.lt, HSub.hSub, SimpleGraph.Walk.length, SimpleGraph.Walk.getVert, HAdd.hAdd, Exists, Eq.mp, congrArg, propext, Imo1991P4.mem_interiorVerts, List.length, SimpleGraph.Walk.edges, Eq.mpr, id, SimpleGraph.Walk.length_edges, GetElem.getElem, List, SimpleGraph.incidenceSet, SimpleGraph.mem_incidenceFinset and 15 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma gcd_interior {s₀ t : V} {w : G.Walk s₀ t} (htrail : w.IsTrail) {n : ℕ}
    {Φ' : Sym2 V → ℕ} {v : V} (hv : v ∈ interiorVerts w) :
    (G.incidenceFinset v).gcd (trailLabel w n Φ') = 1 := by
…
```
Mentions: Imo1991P4.interiorVerts, Imo1991P4.trailLabel
lemma Imo1991P4.no_trail_edge_at If a vertex v is neither the start, an interior vertex, nor the end of the trail w, then no edge of the trail is incident to v line 232 source
Source documentation
If a vertex v is neither the start, an interior vertex, nor the end of the trail w, then no edge of the trail is incident to v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Walk, Ne, Not, Membership.mem, Finset, Imo1991P4.interiorVerts, Sym2, SimpleGraph.incidenceFinset, Set, SimpleGraph.neighborSet, List, SimpleGraph.Walk.edges
Proof uses: Nat, Exists, LT.lt, List.length, Eq, GetElem.getElem, False, Iff.mp, List.mem_iff_getElem, And.right, SimpleGraph.edgeSet, SimpleGraph.incidenceSet, SimpleGraph.mem_incidenceFinset, SimpleGraph.Walk.getVert, HAdd.hAdd, OfNat.ofNat, Or, Eq.mp, Sym2.mk, congrArg and 21 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma no_trail_edge_at {s₀ t : V} {w : G.Walk s₀ t} {v : V}
    (hvs : v ≠ s₀) (hvi : v ∉ interiorVerts w) (hvt : v ≠ t)
    {e : Sym2 V} (he : e ∈ G.incidenceFinset v) : e ∉ w.edges := by
…
```
Mentions: Imo1991P4.interiorVerts
lemma Imo1991P4.degree_endpoint_le_one If all edges of the trail are incident to the endpoint t (maximality) and t is neither the start nor an interior vertex, then at most one edge is incident to t line 253 source
Source documentation
If all edges of the trail are incident to the endpoint t (maximality) and t is neither the start nor an interior vertex, then at most one edge is incident to t.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Walk, Membership.mem, Sym2, List, SimpleGraph.Walk.edges, Sym2.mk, Ne, Not, Finset, Imo1991P4.interiorVerts, LE.le, Nat, Finset.card, SimpleGraph.incidenceFinset, Set and 2 more
Proof uses: Eq.mpr, Eq, id, congrArg, propext, Finset.card_le_one, SimpleGraph.edgeSet, Exists, LT.lt, List.length, And, GetElem.getElem, HSub.hSub, Iff.mp, Sym2.mem_iff_exists, List.mem_iff_getElem, Eq.mp, SimpleGraph.mem_edgeSet, SimpleGraph.Walk.getVert, HAdd.hAdd and 23 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
lemma degree_endpoint_le_one {s₀ t : V} {w : G.Walk s₀ t}
    (hmax : ∀ x : V, G.Adj t x → s(t, x) ∈ w.edges)
    (hts : t ≠ s₀) (hti : t ∉ interiorVerts w) :
    (G.incidenceFinset t).card ≤ 1 := by
…
```
Mentions: Imo1991P4.interiorVerts
lemma Imo1991P4.incidenceFinset_deleteEdges_of_none If no trail edge is incident to v, deleting the trail edges does not change the incidence finset of v line 288 source
Source documentation
If no trail edge is incident to v, deleting the trail edges does not change the incidence finset of v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Walk, Sym2, Membership.mem, Finset, SimpleGraph.incidenceFinset, Set, SimpleGraph.neighborSet, Not, List, SimpleGraph.Walk.edges, Eq, SimpleGraph.deleteEdges, List.toFinset
Proof uses: Finset.ext, Eq.mpr, Iff, SimpleGraph.incidenceSet, id, congrArg, propext, SimpleGraph.mem_incidenceFinset, Iff.intro, SimpleGraph.edgeSet, And.intro, Iff.mpr, And, Imo1991P4.mem_edgeSet_deleteEdges, congrFun', Set.ofPred, List.coe_toFinset, And.left, Iff.mp
24 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma incidenceFinset_deleteEdges_of_none {s₀ t : V} {w : G.Walk s₀ t} {v : V}
    (hnone : ∀ e ∈ G.incidenceFinset v, e ∉ w.edges) :
    G.incidenceFinset v = (G.deleteEdges (↑w.edges.toFinset)).incidenceFinset v := by
…
```
lemma Imo1991P4.gcd_transfer Transfer of the gcd computation to the graph with the trail edges deleted line 301 source
Source documentation
Transfer of the gcd computation to the graph with the trail edges deleted.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Walk, Nat, Sym2, Membership.mem, Finset, SimpleGraph.incidenceFinset, Set, SimpleGraph.neighborSet, Not, List, SimpleGraph.Walk.edges, Eq, Finset.gcd, Imo1991P4.trailLabel, SimpleGraph.deleteEdges and 1 more
Proof uses: Imo1991P4.incidenceFinset_deleteEdges_of_none, Eq.mpr, id, congrArg, Finset.gcd_congr, rfl, Imo1991P4.trailLabel_of_not_mem, Eq.rec, Eq.symm
28 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma gcd_transfer {s₀ t : V} {w : G.Walk s₀ t} {n : ℕ} {Φ' : Sym2 V → ℕ} {v : V}
    (hnone : ∀ e ∈ G.incidenceFinset v, e ∉ w.edges) :
    (G.incidenceFinset v).gcd (trailLabel w n Φ') =
      ((G.deleteEdges (↑w.edges.toFinset)).incidenceFinset v).gcd Φ' := by
…
```
Mentions: Imo1991P4.trailLabel
theorem Imo1991P4.exists_labeling Documented declaration: exists_labeling line 314 source
Source documentation
Main induction: in any graph where every component that contains an edge meets the set S, the edges can be labeled with n + 1, …, n + k in such a way that at every vertex outside S of degree at least two the gcd of the labels is 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nat, SimpleGraph, DecidableRel, SimpleGraph.Adj, Finset, Eq, Finset.card, Sym2, SimpleGraph.edgeFinset, Exists, And, Membership.mem, SimpleGraph.Reachable, Set, SimpleGraph.edgeSet, LE.le, HAdd.hAdd, OfNat.ofNat and 5 more
Proof uses: Nat.strong_induction_on, LT.lt, dite, EmptyCollection.emptyCollection, Iff.mp, Finset.card_eq_zero, Finset.notMem_empty, Eq.rec, Iff.mpr, SimpleGraph.mem_edgeFinset, Exists.intro, And.intro, absurd, Eq.mpr, id, congrArg, Eq.symm, SimpleGraph.card_incidenceFinset_eq_degree, propext, Finset.ext and 75 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 142 steps
Open to load the checked before-and-after goal states.
```
theorem exists_labeling : ∀ (k : ℕ) (H : SimpleGraph V) [DecidableRel H.Adj] (S : Finset V),
    H.edgeFinset.card = k →
    (∀ u v : V, H.Adj u v → ∃ s ∈ S, H.Reachable u s) →
    ∀ n : ℕ, ∃ Φ : Sym2 V → ℕ,
      (∀ e ∈ H.edgeSet, n + 1 ≤ Φ e ∧ Φ e ≤ n + k) ∧
      (∀ e₁ ∈ H.edgeSet, ∀ e₂ ∈ H.edgeSet, Φ e₁ = Φ e₂ → e₁ = e₂) ∧
      (∀ v : V, v ∉ S → 2 ≤ H.degree v → (H.incidenceFinset v).gcd Φ = 1) := by
…
```
Mentions: S
problem Imo1991P4.imo1991_p4 line 449 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, Exists, Sym2, SimpleGraph.edgeSet, Nat, And, LE.le, OfNat.ofNat, Fintype.card, Function.Injective, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Eq and 11 more
Proof uses: Finset.card, Set.toFinset_card, dite, EmptyCollection.emptyCollection, Finset.card_eq_zero, Not, Finset.notMem_empty, Eq.rec, Iff.mpr, Exists.intro, And.intro, absurd, Subtype.property, Eq.mpr, id, congrArg, Eq.symm, SimpleGraph.card_incidenceFinset_eq_degree, propext, Finset.ext and 85 more
73 instances, coercions and auxiliary constants left out.

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