rewriting only once

Stream: new members

[Xindi Ai]

Hi all, is there a way to rewrite something only once? (E.g., when I need to rewrite something on one side of the equation only)
I found this option in the reference manual, which was for Lean 2, and it doesn't seem to work now.

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md

[Kevin Buzzard]

That powerful tool should do the job, although there might be easier solutions in your particular case

[Xindi Ai]

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md

Amazing. Thank you!