Proof that a local minimum in a spanning tree is also a minimum spanning tree.

Be $G$ a connected graph with weights associated to its edges. Be $T(G)$ the graph that has the spanning trees of $G$ as vertex, and two spanning trees are adjacent to each other if and only if each one of them has only one edge that the other doesn't have. To each vertex of $T(G)$ we associate the weight of the spanning tree that correspond to $G$.

Be $T_1$ any vertex of $T(G)$, that is, any spanning tree of $G$. Proof that $T_1$ is a local minimum if and only if $T_1$ is global minimum.

To put it in another words, proof that $T_1$ has weight minor or equal than all its neighbours in $T(G)$ if and only if $T_1$ is an minimum spanning tree.

Let $T$ be a local minimum spanning tree that is not a global minimum. Let $e_1,\ldots,e_m$ the edges of $T$ ordered by non-decreasing weight. Let $T'$ be a minimum weight spanning tree that coincides with $T$ on the largest possible begin segment, so we may assume $T'$ has edges $e_1,\ldots,e_{n-1},f_n,\ldots,f_m$ (again ordered by non-decreasing weight) and $f_n\ne e_n$. Let $w$ be the weight function in our graph.
We claim that $w(f_n)<w(e_n)$: indeed, if $w(e_n)\leq w(f_n)$ then $e_1,\ldots,e_{n-1},e_n$ would be a valid startup for Kruskal's algorithm and would lead to a minimum weight spanning tree that coincides with $T$ on a larger initial segment.
$T+f_n$ contains exactly one cycle $C$. The edges of $C$ different from $f_n$ cannot all be in $\{e_1,\ldots,e_{n-1}\}$ or we would have a cycle in $T'$. So we find at least one edge $f$ on $C$ that is different from $e_1,\ldots,e_{n-1}$ and $f_n$. But then $w(f)\geq w(e_n)>w(f_n)$, so $T+f_n-f$ is a spanning tree with a smaller total weight that is a neighbour of $T$ in the spanning tree graph. Contradiction.