Commit 2024-11-12 20:44 5ffcbfd5

chore: backports of adaptations for leanprover/lean4#6024 (#18896) leanprover/lean4#6024 fixes a serious elaboration bug which, perversely, was quite helpful. Kyle is investigating replacing the bug with something intentional, but we definitively need to fix the bug in the meantime. This is the backport of changes from lean-pr-testing-6024 which do not have conflicts with master. There are a few more changes that we'll need to handle separately later.