Yeah, I've be _really_ impressed with Lean's support. Wish other provers like Coq and Agda were at the same level (I know how challenging it is to do though).