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
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