The Hermitian matrices form a real vector space where we have a Lebesgue measure. In the set of Hermitian matrices with Lebesgue measure, how does it follow that the set of Hermitian matrices with repeated eigenvalue is of measure zero?
This result feels extremely natural but I do not see an immediate argument for it.
Call $S$ the set of matrices with repeated eigenvalues and fix a hermitian matrix $A\not\in S$. In the vector space of hermitian matrices, any line through $A$ intersects $S$ in at most finitely many points. From this it easily follows that $S$ is negligible (using polar coordinates centered at $A$).
To check the claim, note that a line through $A$ consists of matrices of the form $M(t)=(1-t)A+tB$, for some $B\in S$. Hence, the characteristic polynomial of $M(t)$ has the form $\lambda^n+\sum_{k=0}^{n-1}p_k(t)\lambda^k$ for some polynomials $p_k(t)$.
There is a polynomial expression of the coefficients $a_k$ of a polynomial $\lambda^n+\sum_{k=0}^{n-1}a_k\lambda^k$ which vanishes precisely when it has repeated roots: indeed, calling $\alpha_i$ the roots, you can consider the expression $\prod_{i<j}(\alpha_i-\alpha_j)^2$. Since it's symmetric, it is in fact equal to some $P(a_0,\dots,a_{n-1})$. For our matrices, this means that $M(t)\in S$ precisely when $P(p_0(t),\dots,p_{n-1}(t))=0$. The left-hand side is a polynomial, which is not trivial since it does not vanish at $t=0$. Hence, $M(t)\in S$ only for finitely many $t$.
Here is a (I think) mathematically correct, but clearly morally wrong, answer via extreme overkill.
Upon multiplying by $i$, we may work instead with skew-Hermitian matrices, i.e., with $\mathfrak u(n)$. The usual proof of the Weyl integration formula on $U(n)$ works just as well for $\mathfrak u(n)$, and gives that $$ \tag{W}\label{W} \int_{\mathfrak u(n)} f(X)\mathrm dX = \int_{\mathfrak t} f(Y)\lvert D(Y)\rvert^{1/2}\mathrm dY $$ for all continuous, compactly supported, $U(n)$-fixed functions $f$ on $\mathfrak u(n)$, where $\mathfrak t$ is the subspace of diagonal matrices in $\mathfrak u(n)$ and $D(Y) = \prod_{\alpha \in \Phi(\mathfrak u(n), \mathfrak t)} \alpha(Y)$ equals the product of pairs of differences of eigenvalues of $Y$. In particular, the singular set $S$ is the $0$ set of $D$, hence, as @StevenLandsburg suggested, is closed.
Now I'll use dominated convergence freely. To show that $S$ has measure $0$, it suffices to show that its intersection with every compact subset $K$ of $\mathfrak u(n)$ has measure $0$. Upon replacing such a set $K$ by its $U(n)$-orbit, we may, and do, assume that $K$ is $U(n)$-stable. Now there is a sequence $(f_k)_{k = 1}^\infty$ of continuous, compactly supported functions, all pointwise between $0$ and $1$, such that $f_k$ tends pointwise to the indicator function of $S \cap K$. Since $S$, hence $S \cap K$, is stable under $U(n)$-conjugacy, upon replacing each $f_k$ by the average of its $U(n)$-orbits, we may, and do, assume that the sequence consists of continuous class functions. Then, upon applying \eqref{W} to each such function and taking the limit, we see that $$ \operatorname{meas}(S \cap K) = \int_{S \cap K} \mathrm dX = \int_{\mathfrak t \cap S \cap K} \lvert D(Y)\rvert^{1/2}\mathrm dY = 0. $$
Here is another argument.
The idea is that in any neighbourhood of a matrix with repeated roots, there is one with distinct roots. i.e. we are arguing that matrices with repeated roots are residual, that the matrices with distinct roots are open and dense in the space of matrices.
The idea is to put the matrix into its Jordan form. Then you can take a small perturbation that makes all the diagonal entries distinct (only perturbing the diagonal entries). In this form, you can compute the characteristic polynomial and you see the roots are all distinct (as they are the diagonal entries).
I suppose this is essentially Mizar's argument but in a coordinate system where there is a little less work to do.
