feat(lean_examples): use grind for some of the proofs

[abentkamp]

I have experimented with grind on the lean_chacha example. I haven't replaced all of the proofs, only some of them. For the grind annotations that really belong into the Lean repo, I have created a MissingLean folder that I hope to (partially) upstream into the Lean repo some time.

What I hope to get from grind:

• less manual tinkering with the proof script
• less proof breakage
• less need for [simp] annotations that don't really simplify, but rather make more complicated such as https://github.com/cryspen/hax/blob/main/hax-lib/proof-libs/lean/Hax/Lib.lean#L288-L310

It's not clear to me if grind really gives us that, but I am hopeful.

Cons:

• quite slow (maybe we can speed things up by simping or subst_eqs before invoking grind?)
• library must be annotated with @[grind]

[maximebuyse]

I don't completely get the implications of this, but we can try this and reverting shouldn't be hard if we change our minds.