> Anyway, regarding the size: it is large but without it modern lean is > somehow useless. Almost everything inside mathlib.
I know what you mean. You have my approval for the update. Not mathlib. I gave my reasons for suggesting to remove lean a while back.
