An easy example of a non-constructive proof without an obvious "fix"?

I wanted to give an easy example of a non-constructive proof, or, more precisely, of a proof which states that an object exists, but gives no obvious recipe to create/find it.

Euclid's proof of the infinitude of primes came to mind, however there is an obvious way to "fix" it: just try all the numbers between the biggest prime and the constructed number, and you'll find a prime in a finite number of steps.

Are there good examples of simple non-constructive proofs which would require a substantial change to be made constructive? (Or better yet, can't be made constructive at all).

Some digit occurs infinitely often in the decimal expansion of $\pi$.

Claim: There exist irrational $x,y$ such that $x^y$ is rational.

Proof: If $\sqrt2^{\sqrt2}$ is rational, take $x=y=\sqrt 2$. Otherwise take $x=\sqrt2^{\sqrt2}, y=\sqrt2$, so that $x^y=2$.

There is a standard kind of example here. Let $T$ be any open question that requires substantial work to resolve. Consider:

There is a natural number $n$ such that $n = 0$ if and only if $T$.

That statement is clearly true, via a "simple" non-constructive proof: if $n = 0$ is not an example, then $n = 1$ is an example. But if we could produce an explicit example, then we would know whether $T$ holds.

A key point is that the proof does not require the axiom of choice, advanced mathematics, or anything other than ordinary classical logic. The nonconstructivity in classical mathematics is a direct consequence of the classical logic that is used. In constructive mathematics, the property that explicit examples can be constructed for provable existential theorems is called the witness property.

It is common for people to point out examples of "nonconstructive" consequences of Zorn's lemma or the axiom of choice, but classical set theory without the axiom of choice is equally nonconstructive.

The intermediate value theorem, in the form that for a continuous function on $f:[a,b]\to\Bbb R$ with $f(a)<0<f(b)$ there exists $x\in(a,b)$ with $f(x)=0$, is not valid constructively.

See for instance here or here. The fundamental difficulty with the obvious classical proof of the IVT is that one cannot prove constructively that for $c\in(a,b)$ either $f(c)\geq0$ or $f(c)\leq0$ holds, whence one cannot decide whether to concentrate on $[a,c]$ or on $[c,b]$ in trying to localise the search for$~x$ with $f(x)=0$, and therefore no sequence of numbers converging to such an $x$ can be constructed.

Definition: A real number $x$ is called normal if for every $b>1$ the digits $0,1,2,...,b-1$ are equally distributed in the $b$-adic expansion of $x$.

Theorem: Normal numbers exist.

The standard proof is non-constructive as it proceeds by showing that the set of non-normal numbers has Lebesgue-measure zero, hence must have non-empty complement.

I don't know if the existence of a computable normal number can be proved, and if yes, if that proof can be made constructive in the sense that one can explicitly write down an algorithm for the construction of a normal number. I'd be most interested in hearing about such a thing in case anyone knows more about it. Until then, I'm not convinced that normal numbers exist in a real sense, but only that they are unavoidable artefacts in a certain logical and set theoretical framework for the real numbers.