Comment by cubefox

I suppose this is the longest Lean proof by a wide margin.