I tried Lean twice and what caused me to stop both times was a severe lack of documentation. That's a shame, because it's an awesome language.
Kinda agree but Mathlib and its documentation makes for a big corpus to learn by example from. Not ideal but it helps.