How is readability valued in the mathlib

Stream: maths

[Golol]

I am not used to tactic style proofs yet and I am wondering if a tactic style or (detailed) term style proof is considered more readable for an experienced user.
Furthermore, are proofs in the mathlib supposed to be easily readable or instead short and concise?
I think I understand dependent type theory in lean well enough to get started soon but I am struggling to understand the fundamentals of topological or measure spaces for example, as they are implemeneted in the mathlib.
Do people just remember all these small lemmas? Do you only look for a lemma when you need one?
Thanks for the help.

[Ruben Van de Velde]

That's a lot of questions at once - I guess one first thing to note is that readability without the benefit of seeing the tactic state (as you get when looking at a proof in vscode or emacs) is not considered important, so don't assume you can learn much from just looking at the code

[Ruben Van de Velde]

For the small lemmas, the idea is that the naming convention should be consistent enough that you can (mostly) guess the name of the lemma you need, and autocompletion can do the rest if needed. If that doesn't work, library_search and suggest can (sometimes) find relevant lemmas

[Bryan Gin-ge Chen]

#naming

[Kevin Buzzard]

Many of the topological space lemmas have very short proofs using filters. I tend not to look at proofs, if I need a lemma I guess its name and then find it with ctrl-space autocompletion

[Golol]

Okay guys, thanks for the information!

[Floris van Doorn]

About readability: We try to make statements as readable as we can, but don't spend much efforts to make proofs readable.

[Floris van Doorn]

If you are struggling to understand the Lean definitions of concepts, your best bet is to read the documentation around it (module docs and doc strings). If they don't explain it well enough to you, please ask questions here, and once you understand what is going on, improve the doc strings!