This is a complete and working proof written in Lean.
It only makes use of the standard library.
This approach takes the standard approach to prove that sqrt2 is irrational.
The proof itself is a bit messy and I plan on fixing it in the future.
Any questions contact me at conornewton@gmail.com