rewrite only right hand side

Stream: general

[Danny Ofek]

I have an equation x = f(f(x)) and a goal f(x) \leq x.
I want to replace x on the right hand side by f(f(x)) in the goal but when I attempt to use the rw command it replaces x in both sides of the inequality. Anyone knows how to do this? Spent half an hour on this already and I am quite frustrated.

Thanks,
Danny

[David Renshaw]

There's conv https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/extras/conv.md

[Eric Rodriguez]

conv_rhs, nth_rewrite?

[David Renshaw]

ah... I was struggling to remember the name of nth_rewrite.

[Danny Ofek]

Couldn't get conv to work (it does not seem to affect the goal after the begin .... end environment) but the nth_rewrite worked! Thank you!