this is also something that makes me want a more interactive publishing format, though i understand the good reasons to stick to the static quo. if it's easy to see, it shouldn't be too hard to write out in a collapsible sidebar for those interested
Would be cool, just because you could see that the details were actually "omitted for brevity" and not "omitted because they're sketchy". And if you rrrreally want to look through the details, then they're fairly easily available.
Downside, it might have a chilling effect on papers because the scale of writing necessary.
A proof is either providing a new result, or is proving an established result in a new way. Almost always, a proof will need other results, in a way that isn't "interesting" (another term of art). The point of introducing these results as "obvious" is basically to say "here is something which isn't proven by the proof I'm presenting, we need it, but there's no need to derive it to follow this proof", ideally, with a footnote. As language, it is a bit sly: if something is obvious in the normal sense, it will be left out.
It's a problem that the modern style is to elide anything obvious in this sense, rather than in the sense of "anyone who might reasonably read this paper may be expected to know this". But labeling these things as obvious isn't meant in the sense "if you don't know this, you're stupid or uninformed", or in fact "this will be instantly clear as soon as I mention it", it's meant to mean "if you were to follow the breadcrumbs and check up on the 'obvious' thing, it wouldn't help you much in following my proof, so take my word for it. Or, y'know, knock yourself out if this step is interesting to you".
"Trivial" is a term of art (and doesn't mean exactly this) but I'm not sure that "obvious" is.
I think that something already proved is called an immediate corollary if it's a very small step, theorem if it's not that small but well known, a previous result (with a citation!) if not well known, or if you can't cite anything, at least say it's part of "mathematical folklore".
As an elementary example, in an analytic number theory paper one might need to know that for some constant C we have
5x + x^3 + ln(x) < Ce^x
for all positive x. (In practice, one would not need to determine such a C, just know that one exists.)
Such a claim would usually be described as "obvious" or else stated without any justification. I doubt you could find precisely this claim in the literature, but one can find plenty of very similar arguments in textbooks, and anyone doing research in analytic number theory would find this "obvious".