Comment by brosco

Very cool. Analysis I was the first "real" math textbook that I (an engineer, not a mathematician) felt like I could completely follow and work through, after a few attempts to get through others like Rudin. Hopefully the Lean companion will help make it even more accessible to people who are familiar with math and programming and looking to learn things rigorously.