Zulip Chat Archive

Stream: general

Topic: rewrite only right hand side

Danny Ofek (Dec 11 2021 at 00:19):

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.


David Renshaw (Dec 11 2021 at 00:23):

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

Eric Rodriguez (Dec 11 2021 at 00:28):

conv_rhs, nth_rewrite?

David Renshaw (Dec 11 2021 at 00:30):

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

Danny Ofek (Dec 11 2021 at 00:35):

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!

Last updated: Aug 03 2023 at 10:10 UTC