The concise notation and omitted steps are to increase legibility. You are focused on things that the author is intentionally telling you are not important, and you are likely missing the things they're trying to say (e.g. the "shape" of an expression vs the names/super concrete meanings of variables). One of the challenges with Lean is that it requires a lot more effort to write things in a way that communicates what you're actually trying to say.

You need to think of mathematical writing as being both symbols/words and also a picture. You're meant to see patterns in what is in front of you. The short names are necessary for the picture. Without them you can't see it. It's like you've zoomed into the individual pixels; the information is all there but you'll never make sense of it that way. You're meant to read the "zoomed out" view where you have short placeholders as names.

And anyone who's tried to write or read Lean will also tell you that understanding a complicated mathematical proof doesn't necessarily get any easier when it's completely formalised.

Had the same problem with browser extension for a while. I made Explayn because of it: a browser extension that explains any highlighted word, sentence, or formula in place, so readers can understand content without leaving the page. https://chromewebstore.google.com/detail/enjakhegoldmloghmce... Figured it might save you some time.