Is there a clean non-contrived theorem that can only be proven by contradiction?

I know (see Can every proof by contradiction also be shown without contradiction? that there are some theorems that can be proven by contradiction (relying on the law of the excluded middle, that for any proposition $A$, the axiom "either $A$ or not $A$ must hold" is available, but cannot be proven without that axiom schema.

I'm looking for the simplest, cleanest theorem that can't be proven without resorting to proof by contradiction (but has been proven by contradiction).

I'm looking for some theorem that might occur to somebody whose purpose in life was not just to demonstrate that proof by contradiction is sometimes necessary.

I'd be particularly impressed if somebody explains why they know that this theorem can't be proven with just "intuitionist" logic (which does not use the laaw of the excluded middle).

There are two implicit issues with this question. Because this is the second time in the last few days that a question of this kind has been asked, I want to explain the issues in detail, which can't be done in a comment.

Issue 1: Breaking up is hard to do

In most of the standard classical foundational systems, it isn't simple to break up with the law of the excluded middle.

For example, if you take ZFC with a typical deductive system, and then just remove the law of the excluded middle from the deductive system, the rest of the system will still prove the law of the excluded middle, and so in this sense you never need to directly use the law of the excluded middle in a proof, because you can just prove the cases you need directly from the other axioms and deductive rules.

One formal reflection of this phenomenon is called Diaconescu's theorem (also called the Goodman–Myhill theorem). The fundamental issue is that systems like ZFC are so steeped in classical logic that is it very hard to cut out the classical logic while leaving the rest of the axioms unchanged.

So, you really need to start with a system that is built from the ground up to be "constructive", rather than starting with a classical system and cutting out the law of the excluded middle. These "constructive" systems are also somewhat often called "intuitionistic", by the way.

For example, you could ask "What theorem is provable in ZFC set theory but not IZF set theory?" or "What theorem is provable in Peano arithmetic but not Heyting arithmetic?". Each of those is a much more meaningful question which can have specific and precise answers.

Issue 2: Proof by Contradiction is not the same as Proof by Excluded Middle

Many systems that do not include the law of the excluded middle do include the rule of proof by contradiction. That rule says that if we can prove $A \land \lnot A$ for some sentence $A$, then we can conclude any other sentence $B$ that we like. This rule is included, for example, in Heyting arithmetic, which is a well established foundational system for constructive mathematics, and which does not include the law of the excluded middle.

To get a sense of how the law of the excluded middle works, it may be better to think of the law of the excluded middle as allowing for proof by cases. In this form, the law of the excluded middle says that if you can prove $A \to B$ and also prove $\lnot A \to B$ then you can conclude $B$, even without knowing whether $A$ or $\lnot A$ is provable on its own. (This is equivalent over a very weak constructive logic to the usual statement that $C \lor \lnot C$ is provable for every sentence $C$.) This way of looking at excluded middle helps show how it differs from proof by contradiction.

Here is another way to see a difference. In classical mathematics, if we assume $C$, derive a contradiction, and then conclude $\lnot C$, we call that a "proof by contradiction". Similarly, if we assume $\lnot C$, derive a contradiction, and then conclude $C$, we also call that "proof by contradiction". However, only the second of those conclusions requires the law of the excluded middle relative to constructive reasoning. The first example in this paragraph is actually a direct constructive proof of $\lnot C$, because in constructive systems $\lnot C$ is shorthand for "$C$ implies a contradiction". So not everything that we call a "proof by contradiction" in classical mathematics actually uses the proof rule of "proof by contradiction". Some usual ways that we think about classical logic, though, can hide this issue. There is a nice blog post by Andrej Bauer on this topic.