It will be incredibly interesting to assess how the mainstream "textbook" approach to the subject compares to the one taken in the Mathlib. In general, formalized math libraries make it comparatively easier to state results with a maximum degree of generality and to refactor proof developments for straightforwardness and elegance.

(Refactoring is of course made easier because the system will always keep track of what follows logically from what. You don't have that when working with pen and paper, so opportunities to rework things are very often neglected.)

It is a natural question also to ask whether it makes sense to teach the Mathlib, "maximum generality" version of real analysis, or at least something approaching that, in an academic course. Same for any other field of proof-based math, of course.