chore(*): bump to lean 3.34.0 (#9824)
### Backport coercions from Lean 4
Now `has_coe_to_fun` and `has_coe_to_sort` take the output type as an `out_param` argument. This change comes with some changes in the elaboration order, so some proofs/definitions need more type annotations.
### Smarter `by_contra`
Now `by_contra h` does better job if the goal is a negation.
### `open` and current namespace
In
```lean
namespace A
open B _root_.C
end A
```
Lean will try to open `A.B`; if this fails, it will open `B`. It will also open `C`.
`setup_tactic_parser_cmd` command was updated to open appropriate `_root_.*` namespaces.
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
