A Lean companion to Analysis I