The intended use of cheat is to temporarily plug gaps in large theory
developments in order to sketch the bigger picture before filling in the
details. It can be useful as a kind of high-level SUFF_TAC: cheat on a
difficult lemma, see whether it works as intended for the main theorem, then go
back and prove the lemma properly.
The usual caveats associated with mk_oracle_thm apply: cheating exposes you
to the possibility of false theorems and contradictions. To be sure a theorem
was proved without cheating, check its tags.