It's nice to see theorem proving gain some momentum in a mainstream mathematics topic such as analysis.

In PLT, we already had a flagship book (The Formal Semantics of Programming Languages by Winskel) formally verified (kind of, it's not a 1-to-1 transcription) using Isabelle (http://concrete-semantics.org) back in the mid 2010s, when tools began to be very polished.

IMHO, if someone is interested in theorem proving, that's a much simpler starting point. Theorems in analysis are already pretty hard on their own.