changeWith tactic

Stream: lean4

[Wuyang]

My Lean 4 is at v4.13.0-rc3.

From the github, it shows the changeWith tactic is available: https://github.com/leanprover/lean4/blob/v4.13.0-rc3/src/Init/Tactics.lean#L469

However, when I try to use this tactic (change a with b), Lean 4 shows "tactic 'Lean.Parser.Tactic.changeWith' has not been implemented"

Does anyone know why?

[Kyle Miller]

The answer is just that it hasn't been implemented yet. I've been working on a replacement, and it might make it into the next release, or the one after that at the latest.

[Wuyang]

@Kyle Miller do you mean the changeWith is now just a placeholder?

[Daniel Weber]

That's the syntax definition, but there's no implementation

[Wuyang]

@Kyle Miller @Daniel Weber Thanks!!
I plan to use it for the change of variables in integration.
Could you by any chance share any local implementation on this? Or do we have any other better solution for this purpose?

[Kyle Miller]

It's possible you could use rw [show a = b from rfl] or dsimp only [show a = b from rfl] in the meantime.