The code doesn't work. I pasted in the full code at the end into Lean Web, and it gives 4 errors and a warning (all in the lemmas).