Rewrite only one part of expression

Stream: new members

[Winston Yin]

If I start with the hypotheses h1 : f x = g x and h2 : x = y, what can I do to rewrite this hypothesis into f x = g y, where h2 is applied to only one side of the equation?

[Winston Yin]

Would I have to prove a new hypothesis g x = g y and use this to prove f x = g y?

[Eric Rodriguez]

tactic#nth_rewrite

[Adam Topaz]

Or you can use conv_rhs

[Adam Topaz]

Or equivalently conv { to_rhs, ... }

[Adam Topaz]

It's good to know multiple ways to do something, in case you need more flexibility in the future. In this case I would indeed use nth_rewrite

[Winston Yin]

Exactly what I need. Thanks!

[Ruben Van de Velde]

Or

have h3 : f x = g y,
{ rw [h1, h2] },