Hi.
Can you elaborate some more on the motivation? Minimalism is certainly a virtue, but surely something can be said for convenience of reading. Syntax sugar doesn't add new concepts, so it adds little in the way of a mental burden (and it can be desugared from the AST by the parser, keeping tools simple), and IF it is intuitive it can assist with readability. Free tuples are a great example. Not only is the syntax intuitive, but it is so in line with ordinary mathematical notation that even if not taught, users may guess it is supported and try it.
Using a LET to simplify nested comprehensions requires the spec writer to name some intermediary set that may not be meaningful on its own, and requires the reader to at least read the name and maybe ponder its significance. It's not a show-stopper, but it does add some small mental road-bump.
As to standard modules, I can think of some more reasons. By given common idioms standard names they can make it easier to read other people's specs without studying their definitions. They can also ensure that the definitions are correct. Finally, they can then serve as a common ground for reusable theorem modules. Obviously, it's not a good idea that have the standard modules contain any possibly useful definition, but some very common idioms could be added. For example, I think many definitions in the standard TLAPS modules may be candidates.
Ron