Lean/mathlib seems a fantastic system, but in my brief experience it fails in a way that is very common between academically oriented software which is the handling of scopes and names; For example some imports introduce definitions in your module scope (sometime transitively) others do not, automatic imports cannot be renamed or captured easily, the utility names/proofs that are created with new inductive types (like for injection etc) are hard to discover.

When learning a new mathy system I am usually very pedantic and while I am sure that these default were chosen intelligently and with consideration I would have liked if the system was more easily discoverable as a new user