Comment by jboggan

I think this just has to be the problem statement, there's several lemmas I would expect to see in there. Granted I know very little about Lean but it seems like the question and not the proof outlined in the paper.