Comment by JPC21

Second this. What I also wonder about is how closely the TeX write-up and the Lean formalization line-up.