The code is currently not very consistently formatted. It makes sense to follow Mathlib's style conventions, so we should go over the code and change it to be in line with Mathlib style.