there is a practical reason to get rid of the fantasy reals and restrict oneself to normal reals or some other new invention:

Since Lean has become more popular as a proving system I've stumbled upon one very annoying feature of reals: they are not computably comparable. The system says you can never know whether two arbitrary real numbers are the same because you don't have enough time to compare them.