For teaching reasons, I'm looking for examples of proofs that use a nontrivial case breakdown in which only one case is ever realized, and yet it is very hard to prove which case is the "real" one. Let me give two examples of what I mean:
Example 1: There exist two irrational numbers $x,y$ such that $x^y$ is rational.
Proof: Consider two cases based on whether or not the number $\sqrt{2}^\sqrt{2}$ is rational. In Case 1, assume it is rational, and so the theorem is satisfied by $x=y=\sqrt{2}$. In Case 2, assume it is irrational, and so we can take $x=\sqrt{2}^\sqrt{2}$ and $y=\sqrt{2}$, giving $x^y = (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^2 = 2.$
The number $\sqrt{2}^\sqrt{2}$ is either rational or it is irrational, so only one case in this proof is the "real" one. Nonetheless, this case breakdown is useful, since it seems to require Gelfond-Schneider (or related machinery) to actually establish which case is realized.
Example 2: The game of Chomp, played on a $100 \times 100$ chocolate bar, has a winning strategy for the first player.
Proof: Consider two cases based on whether or not there is a winning strategy for the first player that begins by chomping the minimal $1 \times 1$ corner square. In Case 1, assume such a winning strategy exists; then clearly Player 1 has a winning strategy. In Case 2, assume not, and so Player 2 has a winning response to the minimal $1 \times 1$ chomp, say by chomping an $a \times b$ block. Then it follows that Player 1 has a winning strategy by chomping an $a \times b$ block as their first move.
Again, the minimal $1 \times 1$ chomp is either winning or it is not, but as far as I know it is open which case is "real." This example generalizes to one subclass of strategy-stealing proofs.
Ideal answers will have the property that the proof is simple, and yet it is very hard (or open) to establish which case is the one that always occurs. Thanks in advance!