That being said, nequo's request is not unreasonable; given Lean's advanced metaprogramming facilities, their request should be easy to implement.

The nice thing nequo's example illustrates is rank polymorphism: list comprehensions work with lists, products of two, three, four,... lists with the same easy notation : `[n-ary function | x_1 <- List_1, ..., x_n <- List_n]`. It is quite nice to have this, especially for complex numerical operations.

Note also that unlike Lean 3, in Lean 4 `List` does not inherently implement `Applicative` or `Monad`, so your code cannot work as is.

Haskell has always been a language where there are many ways to skin any particular cat, for reasons from ergonomics to expressiveness to theoretical niceness or practicality. "Learn the idioms" has nothing to do with it. Why didn't you just use do-notation instead, for example, than write some applicative mess where it isn't needed?

It's not rocket science why someone would ask this. I don't always use list comprehensions. But sometimes I do. They have open arity and the syntax doesn't as often require things like parenthesis to handle fixity conflicts between other (non-applicative) operators. They are asking about list comprehensions, just because they think it's nice. It is a very simple question and talking about applicative is irrelevant.

That's perfectly fine Haskell, but I wouldn't say that using Applicative is much of a Lean idiom. Especially in the mathlib, people prefer using custom notation that looks like math notation or using the underlying functions directly rather than by using generic point-free notations. For example, you'll see `⨆ i, s i` for a supremum across the values of `s`, vs a point-free version.