A very simple one: in Haskell the compiler has knowledge about which functions cause side-effects and which don't. The compiler can skip calling pure functions whose return value ain't used; similarly, the compiler can call a pure function multiple times, instead of saving the return value in memory.

The Haskell compiler can also fairly freely re-arrange in what order things are computed.

A fairly common idiom in Haskell is to just return a tuple of two values, if they are 'thematically' linked; even if computing one is much more expensive than the other. The compiler is smart enough, to only compute one of the values, if you only use one of them. (When I say 'tuple', it could be literally (a, b), or it could be in a struct or whatever.)

Lean knows even more about your code, so you could do more optimisations. But you need to ask Claude for details, I haven't used it as much nor thought as much about it.