Prove: If $T'$ is not a MST one of its edges may be replaced by a lighter edge in order to get a lighter spanning tree
I have a proposal for a proof that doesn't involve &quot;coloring&quot; since it sounds vague.
Let $T' = (V,F')$ be a spanning tree but not a MST of $G=(V,E)$. Let $T = (V,F)$ be a MST of $G$.

You already did the following:
Now go through all $e \in F-F'$ and add $e$ to $T'$. Resulting graph contains a cycle if there is another edge $e'$ on the cycle such that $e\neq e',w(e) &lt; w(e')$ we are done because $T'$ could be augmented.

My approach for the rest using Kruskal's algorithm:
Otherwise we construct a graph $G' = (V,F'\cup (F-F')) = (V, F'\cup F)$.
For all $e \in F-F'$ and for all cycles $e$ lies on (in $G'$) $e$ is clearly one of the edges with the max weight.
Now run Kruskal's algorithm on $G'$ with a modified sorting procedure. Every edge is primarily sorted by its weight and secondary by the boolean if it belongs to $F'$ or not in such a way that for two edges with different weights the edge with the least weight comes first, but if two edges have the same weight the one belonging to $F'$ comes first (if both belong to $F'$ the order doesn't matter).
We are allowed to make this modification to the sorting procedure because Kruskal's algo doesn't care in which order edges with equal weight appear.
The algorithm proceeds to sort all edges in mentioned order. Thus for every cycle in $G'$ all edges in the cycle are considered before the an edge $e\in F- F'$ is considered. Since we know that Kruskal's algo connects two nodes always when they do not create a cycle and we know that edges $F-F'$ are considered last for every cycle the MST found by the algo is $T' = (V,F')$.
Contradiction:
But from our assumption we know that the weighted sum of $T$s edges is clearly lower than that of $T'$s edges and that $T$ is a spanning tree of $G'$. So actually $T$ is the MST of $G'$. Thus we have a contradiction and can conclude that there must be an $e \in F- F'$ such that it augments $T'$.