VertexDistance.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 10 curated AI-written annotations and 7190 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 project documentation, Formal Conjectures paper, arXiv v1

30 declarations, 0 contain sorry, 0 declared as axioms

Imports (5)

Imported by 5 files

def SimpleGraph.distToSet Distance from a vertex to a finite set line 31 source
Source documentation
Distance from a vertex to a finite set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Set, Nat
Proof uses: dite, Finset.Nonempty, Set.toFinset, Membership.mem, Classical.propDecidable, Finset.min', Finset.image, SimpleGraph.dist, Not, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
noncomputable def distToSet (G : SimpleGraph α) (v : α) (S : Set α) : ℕ :=
…
```
Mentions: SimpleGraph.S
def SimpleGraph.averageDistance Average distance of G line 38 source
Source documentation
Average distance of G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Real
Proof uses: ite, GT.gt, Nat, Fintype.card, OfNat.ofNat, HDiv.hDiv, Finset.sum, Finset.univ, SimpleGraph.dist, HMul.hMul, HSub.hSub
17 instances, coercions and auxiliary constants left out.
```
noncomputable def averageDistance (G : SimpleGraph α) : ℝ :=
…
```
def SimpleGraph.isInducedPath Check if a list of vertices forms an induced path in G line 46 source
Source documentation
Check if a list of vertices forms an induced path in G.

no axioms what this means
Statement uses: SimpleGraph, List
Proof uses: And, List.Nodup, Fin, List.length, Iff, SimpleGraph.Adj, List.get, Or, Eq, Nat, HAdd.hAdd, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def isInducedPath (G : SimpleGraph α) (l : List α) : Prop :=
…
```
Mentions: SimpleGraph.l
def SimpleGraph.path The path number of a graph: The number of vertices of a largest induced path of the graph line 50 source
Source documentation
The path number of a graph: The number of vertices of a largest induced path of the graph.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Nat
Proof uses: Finset, Finset.filter, Exists, List, And, Eq, List.toFinset, SimpleGraph.isInducedPath, Classical.propDecidable, Finset.univ, Option.getD, Finset.max, Finset.image, Finset.card, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
noncomputable def path (G : SimpleGraph α) : ℕ :=
…
```
theorem SimpleGraph.length_le_path_of_isInducedPath An explicit induced path witnesses a lower bound for path line 57 source
Source documentation
An explicit induced path witnesses a lower bound for path.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, List, SimpleGraph.isInducedPath, LE.le, Nat, List.length, SimpleGraph.path
Proof uses: id, Finset, Finset.filter, Exists, And, Eq, List.toFinset, Classical.propDecidable, Finset.univ, Membership.mem, Eq.mpr, Eq.trans, True, congrFun', congrArg, true_and, Exists.intro, And.intro, rfl, Finset.image and 26 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem length_le_path_of_isInducedPath (G : SimpleGraph α) (l : List α)
    (hl : G.isInducedPath l) : l.length ≤ path G := by
…
```
Mentions: SimpleGraph.l, SimpleGraph.path
theorem SimpleGraph.path_le_of_isInducedPath_length_le A uniform upper bound on the lengths of induced paths bounds path line 79 source
Source documentation
A uniform upper bound on the lengths of induced paths bounds path.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Nat, List, SimpleGraph.isInducedPath, LE.le, List.length, SimpleGraph.path
Proof uses: id, Finset, Finset.filter, Exists, And, Eq, List.toFinset, Classical.propDecidable, Finset.univ, Option.getD, Finset.max, Finset.image, Finset.card, OfNat.ofNat, WithBot, Finset.max_le, Membership.mem, Iff.mp, Finset.mem_image, Finset.mem_filter and 19 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem path_le_of_isInducedPath_length_le (G : SimpleGraph α) (k : ℕ)
    (h : ∀ l : List α, G.isInducedPath l → l.length ≤ k) : path G ≤ k := by
…
```
Mentions: SimpleGraph.l, SimpleGraph.path
theorem SimpleGraph.path_le_of_not_exists_inducedPath_succ If G has no induced path on k + 1 vertices, then path G ≤ k line 102 source
Source documentation
If G has no induced path on k + 1 vertices, then path G ≤ k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Nat, Not, Exists, Fin, HAdd.hAdd, OfNat.ofNat, And, Function.Injective, Iff, SimpleGraph.Adj, Or, Eq, LE.le, SimpleGraph.path
Proof uses: SimpleGraph.path_le_of_isInducedPath_length_le, List, SimpleGraph.isInducedPath, Decidable.byContradiction, List.length, List.get, Fin.mk, lt_of_lt_of_le, Fin.isLt, Exists.intro, And.intro, Fin.ext, congrArg, List.Nodup.injective_get, And.left, List.Nodup, id, And.right
13 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem path_le_of_not_exists_inducedPath_succ (G : SimpleGraph α) (k : ℕ)
    (h : ¬ ∃ e : Fin (k + 1) → α, Function.Injective e ∧
      ∀ i j : Fin (k + 1), G.Adj (e i) (e j) ↔
        i.val + 1 = j.val ∨ j.val + 1 = i.val) : path G ≤ k := by
…
```
Mentions: SimpleGraph.path
def SimpleGraph.ecc Auxiliary quantity ecc used in conjecture 34 line 122 source
Source documentation
Auxiliary quantity ecc used in conjecture 34.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Set, Nat
Proof uses: Finset, Finset.filter, Not, Membership.mem, Classical.propDecidable, Finset.univ, dite, Finset.Nonempty, Finset.max', Finset.image, SimpleGraph.distToSet, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
noncomputable def ecc (G : SimpleGraph α) (S : Set α) : ℕ :=
…
```
Mentions: SimpleGraph.S
def SimpleGraph.distMin The minimum distance between distinct vertices of $S$: $\min \{\operatorname{dist}_G(u, v) \mid u, v \in S, u \ne v\}$ line 132 source
Source documentation
The minimum distance between distinct vertices of $S$: $\min \{\operatorname{dist}_G(u, v) \mid u, v \in S, u \ne v\}$. Returns 0 when $S$ contains fewer than two vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Set, Nat
Proof uses: Finset, Prod, Finset.filter, Ne, Prod.fst, Prod.snd, Eq, SProd.sprod, Set.toFinset, Membership.mem, Classical.propDecidable, dite, Finset.Nonempty, Finset.min', Finset.image, SimpleGraph.dist, Not, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
```
noncomputable def distMin (G : SimpleGraph α) (S : Set α) : ℕ :=
…
```
Mentions: SimpleGraph.S
def SimpleGraph.eccSet The eccentricity of a set S: the maximum, over all vertices v of G, of the minimum distance from v to any vertex in S line 147 source
Source documentation
The eccentricity of a set S: the maximum, over all vertices v of G, of the minimum distance from v to any vertex in S. (This includes vertices in S itself, which contribute distance 0.) Returns 0 when S is empty.
Unlike ecc, which restricts the outer maximum to vertices v ∉ S, eccSet does not exclude any vertex; it is the conventional definition of "set eccentricity" used in DeLaVina's WOWII conjectures 142, 145 and 146.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Set, Nat
Proof uses: Finset, Finset.image, SimpleGraph.distToSet, Finset.univ, dite, Finset.Nonempty, Finset.max', Not, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
noncomputable def eccSet (G : SimpleGraph α) (S : Set α) : ℕ :=
…
```
Mentions: SimpleGraph.S
def SimpleGraph.distMaxSet The maximum distance between two vertices of a set S: $\operatorname{dist}_{\max}(S) = \max\{\operatorname{dist}_G(u,v) \mid u, v \in S\}$ line 158 source
Source documentation
The maximum distance between two vertices of a set S: $\operatorname{dist}_{\max}(S) = \max\{\operatorname{dist}_G(u,v) \mid u, v \in S\}$. Returns 0 when S is empty or a singleton.
This is DeLaVina's dist_max(S) invariant ("distance between maximum degree vertices" when S = M), used in WOWII conjecture 18. It is distinct from eccSet, which measures distances from arbitrary vertices to the set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Set, Nat
Proof uses: Finset, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Finset.sup, Prod, SProd.sprod, SimpleGraph.dist, Prod.fst, Prod.snd
5 instances, coercions and auxiliary constants left out.
```
noncomputable def distMaxSet (G : SimpleGraph α) (S : Set α) : ℕ :=
…
```
Mentions: SimpleGraph.S
def SimpleGraph.distAvgSet The average distance between distinct vertices of a set S line 171 source
Source documentation
The average distance between distinct vertices of a set S: $\operatorname{dist}_{\operatorname{avg}}(S)$ is the mean of $\operatorname{dist}_G(u, v)$ over all ordered pairs $(u, v)$ of distinct vertices of $S$. Returns 0 when $S$ contains fewer than two vertices.
This is DeLaVina's dist_avg(S) invariant ("average distance between maximum degree vertices" when S = M), used in WOWII conjecture 23. It is distinct from distavg, which averages the distances from all vertices of G to the set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Set, Real
Proof uses: Finset, Prod, Finset.filter, Ne, Prod.fst, Prod.snd, Eq, SProd.sprod, Set.toFinset, Membership.mem, Classical.propDecidable, ite, Finset.Nonempty, HDiv.hDiv, Finset.sum, SimpleGraph.dist, Finset.card, OfNat.ofNat
13 instances, coercions and auxiliary constants left out.
```
noncomputable def distAvgSet (G : SimpleGraph α) (S : Set α) : ℝ :=
…
```
Mentions: SimpleGraph.S
def SimpleGraph.distavg Average distance from all vertices to a given set line 179 source
Source documentation
Average distance from all vertices to a given set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Set, Real
Proof uses: ite, GT.gt, Nat, Fintype.card, OfNat.ofNat, HDiv.hDiv, Finset.sum, Finset.univ, SimpleGraph.distToSet
11 instances, coercions and auxiliary constants left out.
```
noncomputable def distavg (G : SimpleGraph α) (S : Set α) : ℝ :=
…
```
Mentions: SimpleGraph.S
def SimpleGraph.graphSquare The square of a graph G, denoted G²: two distinct vertices are adjacent iff their distance in G is at most 2 line 192 source
Source documentation
The square of a graph G, denoted G²: two distinct vertices are adjacent iff their distance in G is at most 2.
The bound uses the extended distance SimpleGraph.edist, which is ⊤ for unreachable vertices. The natural-valued SimpleGraph.dist is 0 there, so it would make distinct vertices in different components adjacent: the square of the edgeless graph on two vertices would be the complete graph.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph
Proof uses: SimpleGraph.mk, And, Ne, LE.le, ENat, SimpleGraph.edist, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def graphSquare (G : SimpleGraph α) : SimpleGraph α where
…
```
def SimpleGraph.isInducedC4 Check whether four distinct vertices form an induced 4-cycle in G line 200 source
Source documentation
Check whether four distinct vertices form an induced 4-cycle in G. We test all three perfect-matching pairings of the four vertices to find a cyclic ordering and verify that the induced subgraph has exactly those 4 edges.

no axioms what this means
Statement uses: SimpleGraph, DecidableRel, SimpleGraph.Adj, Bool
Proof uses: Bool.and, Decidable.decide, Bool.not, Bool.or
```
noncomputable def isInducedC4 (G : SimpleGraph α) [DecidableRel G.Adj]
    (a b c d : α) : Bool :=
…
```
Mentions: SimpleGraph.b, c
def SimpleGraph.countInducedC4 Count of induced C₄ subgraphs of G line 218 source
Source documentation
Count of induced C₄ subgraphs of G. We count ordered 4-tuples (a,b,c,d) of distinct vertices for which isInducedC4 G a b c d = true, then divide by 24 = 4!.
Why 24 (and not 8)? isInducedC4 tests all three perfect-matching pairings of the four vertices, so any of the 4! = 24 orderings of a fixed unordered induced 4-cycle satisfies the predicate. Dividing by 8 (the size of the dihedral group D₄) would overcount each induced 4-cycle by a factor of 3 — once for each of the three cyclic structures isInducedC4 accepts.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat
Proof uses: HDiv.hDiv, Finset.sum, Finset.univ, ite, And, Ne, Eq, Bool, SimpleGraph.isInducedC4, Bool.true, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
noncomputable def countInducedC4 (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
…
```
def SimpleGraph.bfs_dist_aux line 223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat, Finset
2 instances, coercions and auxiliary constants left out.
def SimpleGraph.computable_dist Computable graph distance via BFS line 231 source
Source documentation
Computable graph distance via BFS. Returns 0 if u = v or if v is unreachable from u.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat
Proof uses: ite, Eq, OfNat.ofNat, SimpleGraph.bfs_dist_aux, Fintype.card, SimpleGraph.bfsStep, Singleton.singleton, Finset
2 instances, coercions and auxiliary constants left out.
```
def computable_dist (G : SimpleGraph α) [DecidableRel G.Adj] (u v : α) : ℕ :=
…
```
def SimpleGraph.computableDistMin A computable version of distMin for a Finset of vertices line 236 source
Source documentation
A computable version of distMin for a Finset of vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Finset, Nat
Proof uses: Prod, Finset.filter, Ne, Prod.fst, Prod.snd, Eq, SProd.sprod, dite, Finset.Nonempty, Finset.min', Finset.image, SimpleGraph.computable_dist, Not, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
def computableDistMin (G : SimpleGraph α) [DecidableRel G.Adj] (S : Finset α) : ℕ :=
…
```
Mentions: SimpleGraph.S
def SimpleGraph.computable_avg_dist Computable average distance as a rational line 243 source
Source documentation
Computable average distance as a rational.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Rat
Proof uses: ite, GT.gt, Nat, Fintype.card, OfNat.ofNat, HDiv.hDiv, Finset.sum, Finset.univ, SimpleGraph.computable_dist, HMul.hMul, HSub.hSub
13 instances, coercions and auxiliary constants left out.
```
def computable_avg_dist (G : SimpleGraph α) [DecidableRel G.Adj] : ℚ :=
…
```
lemma SimpleGraph.mem_iterate_bfsStep_dist_le line 250 source
lemma SimpleGraph.dist_le_mem_iterate_bfsStep line 275 source
theorem SimpleGraph.dist_eq_computable line 302 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, SimpleGraph.dist, SimpleGraph.computable_dist
Proof uses: id, dite, ite, OfNat.ofNat, SimpleGraph.bfs_dist_aux, Fintype.card, SimpleGraph.bfsStep, Singleton.singleton, Finset, Eq.mpr, congrArg, if_pos, of_eq_true, Eq.trans, True, congrFun', SimpleGraph.dist_self, eq_self, Not, if_neg and 53 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 55 steps
Open to load the checked before-and-after goal states.
theorem SimpleGraph.distMin_eq_computableDistMin computableDistMin agrees with distMin on a finite vertex set line 361 source
Source documentation
computableDistMin agrees with distMin on a finite vertex set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Finset, Eq, Nat, SimpleGraph.distMin, SimpleGraph.computableDistMin
Proof uses: id, Prod, Finset.filter, Ne, Prod.fst, Prod.snd, SProd.sprod, Set.toFinset, Membership.mem, Set, Classical.propDecidable, dite, Finset.Nonempty, Finset.min', Finset.image, SimpleGraph.dist, Not, OfNat.ofNat, Eq.mpr, SimpleGraph.computable_dist and 22 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem distMin_eq_computableDistMin (G : SimpleGraph α) [DecidableRel G.Adj]
    (S : Finset α) : distMin G (S : Set α) = computableDistMin G S := by
…
```
Mentions: SimpleGraph.S, SimpleGraph.distMin, SimpleGraph.computableDistMin
theorem SimpleGraph.avg_dist_eq_computable line 376 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Real, SimpleGraph.averageDistance, SimpleGraph.computable_avg_dist
Proof uses: id, ite, GT.gt, Nat, Fintype.card, OfNat.ofNat, HDiv.hDiv, Finset.sum, Finset.univ, SimpleGraph.dist, HMul.hMul, HSub.hSub, dite, Rat, SimpleGraph.computable_dist, Eq.mpr, congr, congrArg, if_pos, Eq.trans and 64 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
def SimpleGraph.distEven distEven G v counts the vertices at even distance from v in G line 396 source
Source documentation
distEven G v counts the vertices at even distance from v in G. This is DeLaVina's dist_even(v) invariant appearing in several WOWII conjectures. Distance zero is even, so v itself is always counted.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Nat
Proof uses: Finset.card, Finset.filter, Even, SimpleGraph.dist, Finset.univ
2 instances, coercions and auxiliary constants left out.
```
noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ :=
…
```
def SimpleGraph.evenDistancePairs The set of pairs of distinct vertices with even distance > 0 line 400 source
Source documentation
The set of pairs of distinct vertices with even distance > 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Finset, Prod
Proof uses: Finset.filter, And, Eq, Nat, HMod.hMod, SimpleGraph.dist, Prod.fst, Prod.snd, OfNat.ofNat, GT.gt, Finset.univ
8 instances, coercions and auxiliary constants left out.
```
noncomputable def evenDistancePairs (G : SimpleGraph α) : Finset (α × α) :=
…
```
def SimpleGraph.minEvenDistance Minimum even distance between distinct vertices in G line 405 source
Source documentation
Minimum even distance between distinct vertices in G. Only positive even distances are considered. Returns 0 if no such distance exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Nat
Proof uses: dite, Finset.Nonempty, Prod, SimpleGraph.evenDistancePairs, Finset.min', Finset.image, SimpleGraph.dist, Prod.fst, Prod.snd, Not, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
noncomputable def minEvenDistance (G : SimpleGraph α) : ℕ :=
…
```
def SimpleGraph.maxEvenDistance Maximum even distance between distinct vertices in G line 414 source
Source documentation
Maximum even distance between distinct vertices in G. Only positive even distances are considered. Returns 0 if no such distance exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Nat
Proof uses: dite, Finset.Nonempty, Prod, SimpleGraph.evenDistancePairs, Finset.max', Finset.image, SimpleGraph.dist, Prod.fst, Prod.snd, Not, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
noncomputable def maxEvenDistance (G : SimpleGraph α) : ℕ :=
…
```
def SimpleGraph.averageEvenDistance Average even distance between distinct vertices in G line 423 source
Source documentation
Average even distance between distinct vertices in G. Only positive even distances are considered. Returns 0 if no such distance exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Rat
Proof uses: ite, GT.gt, Nat, Finset.card, Prod, SimpleGraph.evenDistancePairs, OfNat.ofNat, HDiv.hDiv, Finset.sum, SimpleGraph.dist, Prod.fst, Prod.snd
9 instances, coercions and auxiliary constants left out.
```
noncomputable def averageEvenDistance (G : SimpleGraph α) : ℚ :=
…
```