lean4 change tactic change?

Stream: lean4

[Ian Benway]

Hi! So it's my understanding that in Lean 3 tactics, we can use change' to change all instances of some expression to something definitionally equal.
I want to do something similar in a Lean 4 tactic. I have an expression x : Expr and a definitionally equivalent y : Expr. So in my context I have something like x + x = x and a goal of x = 0, but I want y + y = y and a goal of y = 0. I'm confused on how Lean 4 change works, and if that's what I have to use to accomplish this.

[James Gallicchio]

I'm not really sure how change' works, but if you can get a hypothesis x = y (perhaps by have : x = y := refl then you can rw [this] at * to the same effect, I think

[Ian Benway]

I like this solution. But in my case, I think I'd like to do so without adding a new hypothesis. Is there any way around that?

[Horatiu Cheval]

rw [(rfl : x = y)]? :)

[Horatiu Cheval]

Not a real answer to the question regarding change, but it should work if x and y are defeq, without adding an additional hypothesis

[Gabriel Ebner]

I think you need to do rw [(id rfl : x = y)], because rfl always has the type x = x.

[Gabriel Ebner]

This is a fairly common pattern actually, although I prefer to use show like simp [fun n => show n.succ = n + 1 from rfl].