Comment by SwtCyber

I think you're basically right about the end goal yet the gap between a textbook proof and a Lean proof is much bigger than it looks