Kinda agree but Mathlib and its documentation makes for a big corpus to learn by example from. Not ideal but it helps.

https://github.com/leanprover-community/mathlib