Theorem 3.7.5 — Cayley's Tree Formula

For every natural number $n$ satisfying $2 \le n$, the statement asserts that the number of simple graphs on the vertex set $\{0,1,\dots,n-1\}$ (i.e. $\mathrm{Fin}\ n$) that are trees — meaning, per Mathlib's SimpleGraph.IsTree, that the graph is both connected and acyclic (contains no cycles) — equals $n^{\,n-2}$. Concretely, the quantity on the left is $\operatorname{Nat.card}$ applied to the subtype $\{T : \mathrm{SimpleGraph}(\mathrm{Fin}\ n) \mid T.\mathrm{IsTree}\}$, i.e. the cardinality of the set of all such tree-graphs on this fixed $n$-element vertex set (where a "simple graph" here is an irreflexive symmetric relation on $\mathrm{Fin}\ n$, so no loops and no multi-edges, and two such graphs are counted as distinct objects whenever their edge relations differ, i.e. this counts labeled trees on distinguishable vertices $0,\dots,n-1$, not trees up to isomorphism). Since $\mathrm{SimpleGraph}(\mathrm{Fin}\ n)$ is a finite type for every $n$, this subtype is finite as well, so $\operatorname{Nat.card}$ here denotes the ordinary (finite) cardinality of this set of graphs, not the degenerate value $0$ that $\operatorname{Nat.card}$ assigns to infinite types. The hypothesis $2 \le n$ restricts the claim to $n \ge 2$, so the potentially degenerate cases $n=0$ (empty vertex set) and $n=1$ (single vertex, where $n-2$ would require care as a natural-number subtraction) are excluded from what is being asserted; note also that $n-2$ is natural-number subtraction, which for $n=2$ evaluates to $0$, giving right-hand side $2^0=1$. The proof of this equality is not supplied — the body is sorry, so the statement is asserted but unproved.