On the contrary, I think the basics are covered pretty well by the official documentation, but it's lacking the more advanced stuff.

I agree; for simple and "beginning intermediate" tasks, Functional Programming in Lean has it all; but the more advanced features are only documented in the source code and doc-strings. There is also a lack of general listings: for data structures, for file access API, for algorithms etc.

Is there an eBNF+PEG or similar grammar for the language parser that a more complete language reference can be generated from?

Does Lean have docstrings with embedded markup like Python?

The Python Language Reference: https://docs.python.org/3/reference/

The Python Language Reference > 10. Full Grammar specification: https://docs.python.org/3/reference/grammar.html

LearnXinYminutes > Where X=Python: https://learnxinyminutes.com/docs/python/

In the language and then the docs, Python's collections.abc Abstract Base Classes did not initially exist. There's now a table of ABCs in the docs: https://docs.python.org/3/library/collections.abc.html#colle...

In Python, they're not interfaces, they're ABCs.