I'm interested in proofs of claims of the form "Finite objects $A$ and $B$ are isomorphic" which are nonconstructive, in the sense that the proof doesn't exhibit the actual isomorphism at hand.
A stronger (and more precisely specified) requirement would be a case in which it's computationally easy to write a proof, but computationally hard to extract the isomorphism given the proof, e.g. a class of graphs for which one can easily generate triples $(G,H,P)$ with $P$ a proof that $G$ and $H$ are isomorphic but for which there's no (known) efficient algorithm to take in $(G,H,P)$ and return a permutation of the vertices exhibiting the isomorphism.
Some examples of things that would fit the bill, were they to exist:
(give a nonconstructive proof that) all objects of type $X$ are uniquely specified by their values on five specific measurements; observe that $A$ and $B$ align on all such measurements.
The easy-to-compute function of graphs $f(G,H)$ turns out to be equal to the product, over all relabelings of $G$, of the number of edges in the symmetric differences between the edge sets of $H$ and the relabeled copy of $G$. (This occurs because of some cute algebraic cancellation or something, like how one can compute determinants in time $O(n^3)$.) Now we observe that $f(G,H) = 0$ via direct computation, and conclude that a relabeling with no difference at all to $H$ must exist.
Groups $G$ and $H$ of order $n$, specified by their multiplication tables, can be easily shown to embed as subgroups of a larger group $K$, which we can classify and more easily prove things about. But the existence of two non-isomorphic subgroups of order $n$ in $K$ would imply something about its Sylow subgroups that we know to be false.
Are there good examples of this phenomenon? Reasons to think it doesn't happen? I would also be interested in any pointers to literature on related topics here.