First of all, I want to make clear what I'm NOT asking. I'm not hoping to do a rehash of the implications of nonstandard analysis on calculus. Rather, I'm interested in its use in "harder" math. I'm currently reading through Goldblatt's Lectures on the Hyperreals and working on the later sections, wherein he discusses ways of rephrasing other areas of math in nonstandard language (e.g. Loeb measures). I'm trying to understand what the purpose of this is.
I understand that nonstandard doesn't get us new results, that is there's nothing we can prove in a nonstandard framework that we can't prove over old-fashioned ZFC. I also understand that generally nonstandard allows us to see the spaces we work in "more intuitively", e.g. Loeb measures allow us to see Lebesgue measure in a more finitary light, but I don't have much of a sense for what this more intuition looks like when we're actually trying to prove statements.
So what is the use of nonstandard analysis in its broadest sense? To those of y'all who study/use/teach it, what do you see it as buying you over "standard" analysis?
I'm just going to give a fragment of an answer. "what do you see it as buying you over 'standard' analysis?" Here's one small insight that I think might never have come about without Robinson's NSA: