Remove mathlib dependency (#9)

Remove mathlib from dependencies and fix all proofs.

Call outs: I had to add `batteries` as a dependency, but all
definitions/theorems needed from `batteries` (e.g. `List.IsPrefix`) have
been upstreamed in
https://github.com/leanprover/lean4/releases/tag/v4.11.0-rc1 (e.g.
leanprover/lean4#4836), so we should be able to
get rid of the `batteries` dependency as well once v4.11.0 is released.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: zhassan-aws