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