It’s probably just because a zstd implementation in Lean would be more difficult. The whole project depends on being able to have a correctness proof for the implementation, and implementing that for the DEFLATE algorithm is simpler.

https://github.com/kim-em/lean-zstd