A variation on this is the "not rediscoverable proof". This is a proof of a result which you can verify, and perhaps even understand why it is a proof, but which you could not discover on your own just given the theorem statement. I think this arises from studying an area, and then finding a surprising and unexpected consequence. Perhaps this speaks more to the nature of understanding, in that a deductive consequence come as such a surprise.

The amazing example of this I have found is Lovasz's cancellation theorem for finite structures, from one of his first published papers. Even after having reviewed the proof many times, I still could not imagine how I could come up with it. More technical detail can be found in an answer of Eric Wolsey, with some of my commentary nearby. https://mathoverflow.net/a/269545/ .

Gerhard "Understands Understanding Isn't Very Understandable" Paseman, 2020.06.12.