chore(*): update to lean 3.30.0c (#7264)
There's quite a bit of breakage from no longer reducing `acc.rec` so aggressively. That is, a well-founded definition like `nat.factors` will no longer reduce definitionally. Where you could write `rfl` before, you might now need to write `by rw nat.factors` or `by simp [nat.factors]`.
A more inconvenient side-effect of this change is that `dec_trivial` becomes less powerful, since it also relies on the definitional reduction. For example `nat.factors 1 = []` is no longer true by `dec_trivial` (or `rfl`). Often you can replace `dec_trivial` by `simp` or `norm_num`.
For extremely simple definitions that only use well-founded relations of rank ω, you could consider rewriting them to use structural recursion on a fuel parameter instead. The functions `nat.mod` and `nat.div` in core have been rewritten in this way, please consult the [corresponding Lean PR](https://github.com/leanprover-community/lean/pull/570/files) for details on the implementation.
