Improve the performance of the proofs in the Lean backend

[sonmarcho]

trafficstars

The proofs in the Lean backend are a bit slow for my taste. For instance, until recently, the proofs of the hashmap and the AVL took ~200s each, which is quite a lot. A more reasonable target (according to my intuition) would be less than a minute.

One issue for instance is the simplifier.

The simplifier can be slow at times especially when using simp_all in contexts with big goals. I did some preliminary diagnostics which indicate that it can sometimes perform up to ~10k simplification lemma attempts, which is not reasonable. We should investigate this.

In parallel, this seems to indicate that simp_all is maybe not the best way of "blasting" a proof: for instance, I often use it when what I actually need to do is some sort of congruence closure. Maybe we should investigate other proof styles in consequence.