It's also useful if your transformations aren't bijective. A lot of hyperreal proofs look like (a) Push your real-valued problem to the hyperreals, (b) Prove so

It's also useful if your transformations aren't bijective. A lot of hyperreal proofs look like (a) Push your real-valued problem to the hyperreals, (b) Prove something interesting, and (c) push some subset/transformation of that interesting thing back down to the reals. As a very concrete example (eliding details for obvious reasons), to prove Kőnig's lemma you can (0) Start with a connected, infinite, locally finite graph, (a) Embed that infinite graph in any properly nonstandard extension thereof, (b) Use the transfer principle to find an infinite "hyper" path (no longer a path because it's indexed by the hypernaturals), and (c) Project that back to a standard path in the subgraph induced by restricting to the original infinite graph. That is precisely the infinite path you were looking for. Not that Kőnig's lemma is hard to prove with standard techniques per se, but it illustrates the point.