Thanks for your contribution! Please make sure to follow our Commit Convention.

But change isn't implemented...? Are you talking about the change conv? The implementation of the change tactic is in Mathlib.Tactic.Basic.

Oh dear, very sorry to have caused this nonetheless!

If I PR core or std4 in the future, I'll be sure to build Mathlib to make sure that only expected breakages occur. I look forward to the automatically posted build reports, however, as a full Mathlib build is quite a bit for my laptop to handle! :) (Though I suppose I could convince CI to do it on a branch/PR.)

I'll start investigating this tomorrow. Will the PR release for #2435 still work? (I've briefly tried elan install leanprover/lean4-pr-releases:pr-release-2435, but am met with an error.)

Also: can/should #2435 be reopened, or should I make a new one (possibly with a new branch)?

Couldn't resist taking a peek: what's happening (at least in the first example) is that change makes an intermediate fresh natural mvar to simulate a goal when elaborating a local hypothesis. Nothing actually depends on this mvar, so if you simply throw it away—as you might when throwing away all natural mvars!—you don't get any kernel error. As of 2435, we no longer throw it away, and it appears as a spurious unsolved goal. This shouldn't be difficult to fix—assuming there aren't other issues. I'll try to open a mathlib4 PR when I next get the chance (in 12 hours or so). :)

But change isn't implemented...? Are you talking about the change conv? The implementation of the change tactic is in Mathlib.Tactic.Basic.

Ah, okay, indeed that makes it harder to catch in Lean itself, and I feel less bad about this. With this toolchain many of the uses of change in mathlib are duplicating goals.