For this book specifically, I think the reason is just that Lean is the theorem prover he already knows and uses in his own work [1].
Now as to why he picked Lean a few years ago as his go-to theorem prover, I do think that would be an interesting backstory. As far as I know he hasn't written anything explicit about it.
