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.

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

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.

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

…anprover#6024)

This PR fixes a bug where the monad lift coercion elaborator would
partially unify expressions even if they were not monads. This could be
taken advantage of to propagate information that could help elaboration
make progress, for example the first `change` worked because the monad
lift coercion elaborator was unifying `@Eq _ _` with `@Eq (Nat × Nat)
p`:
```lean
example (p : Nat × Nat) : p = p := by
  change _ = ⟨_, _⟩ -- used to work (yielding `p = (p.fst, p.snd)`), now it doesn't
  change ⟨_, _⟩ = _ -- never worked
```
As such, this is a breaking change; you may need to adjust expressions
to include additional implicit arguments.

We have some adaptation notes referring to [lean4#6024](leanprover/lean4#6024), which changed elaboration subtly; some tricky unifications no longer get solved. I checked every reference to make sure that these still apply. We don't expect that this change gets reverted, so we can turn the remaining adaptation notes into regular comments.

…unity#27348)

We have some adaptation notes referring to [lean4#6024](leanprover/lean4#6024), which changed elaboration subtly; some tricky unifications no longer get solved. I checked every reference to make sure that these still apply. We don't expect that this change gets reverted, so we can turn the remaining adaptation notes into regular comments.

…unity#27348)

We have some adaptation notes referring to [lean4#6024](leanprover/lean4#6024), which changed elaboration subtly; some tricky unifications no longer get solved. I checked every reference to make sure that these still apply. We don't expect that this change gets reverted, so we can turn the remaining adaptation notes into regular comments.

…unity#27348)

We have some adaptation notes referring to [lean4#6024](leanprover/lean4#6024), which changed elaboration subtly; some tricky unifications no longer get solved. I checked every reference to make sure that these still apply. We don't expect that this change gets reverted, so we can turn the remaining adaptation notes into regular comments.