Lean is actually pretty speedy as is, and it enables much harder optimizations[1]

[1] https://github.com/kim-em/lean-zip#verification-enables-perf...