As an abstract rule of thumb, how much would one have to beef up on logic before attempting to screw around analysis and something like Lean?

None at all. Hit the natural numbers game that was referenced and you can start proving basic things like 2+2=4, n+0=n on up to associativity, commutativity, etc of basic operations, etc.