Question.
What are examples (preferably documented and explicitly commented on from this perspective in the literature, preferably in an article dedicated to this aspect alone) of the following well-known aspect of the usual completeness theorem for first-order logic (summarizing it here slightly flippantly, for brevity)?
If $\mathbb{T}$ is a theory in first-order logic (with $=$) over a language $L$, and if $\sigma$ is any $L$-sentence, and if $\vDash$ denotes entailment w.r.t. a given semantics for $L$, and if $\vdash$ denotes existence of a finite proof w.r.t. a given usual proof system, and if you prove $\mathbb{T}\vDash\sigma$ with no holds barred, then you know the existence-statement $\mathbb{T}\vdash\sigma$ to be true.
Remark.
Motivation for the question is partly expository writing, partly my working on an open problem about triangle-free graphs whose statement is one first-order sentence in a relational language.
It seems especially interesting, in particular for expository purposes, to have notable examples of a first-order syntactic proof having to exist by the completeness theorem but not yet having been found so far (and researchers in the field being aware of that and deploring it), and there being some hope that the shortest syntactic proof is short enough to be found in future (and possible even appreciably simple).
Even though my research-motivation is about a statement which does not even use function-symbols, my exposition does not make any such restriction to purely relational languages, and I would also appreciate examples involving first-order statements which do use function symbols.
In expositions (I will not give examples here since such mentionings would be rather negativistic, to the effect of "Look, Author A does not give an example.") of the usual completeness theorem for first-order logic, one sometimes encounters a discussion pointing out the above consequence of the completeness theorem, but I have not seen any notable example being given in such expositions. It is easy to devise very artificial examples.
The metaphor "with no holds barred" in the above refers to any mathematical theory or logic being allowed to prove that each model of $\mathbb{T}$ is a model of $\sigma$.
This MO thread is similar in spirit, but technically quite different.
All famous examples (that I can think of, that is) of ("elementary" here in an informal sense) elementary statements first being proved by non-elementary methods and later being given an elementary proof do not qualify as examples, for one technical reason or the other. (For example, it would be too much of a stretch to pass off e.g. the elementary proofs given by P. Erdős and A. Selbert of the theorem on the distribution of the primes as an example. The statement each Robbins algebra is a Boolean algebra fits the logical bill, but there the first-proved-by-semantic-non-elementary-methods-bit is totally lacking: the first proof found for this was syntactic. Some other examples I tried do not fit for similar reasons.)