Function

Stream: new members

[Ashvni Narayanan]

This is a general question. Suppose I have some space K, and a function from K to \Z. For elements a,b,c in K, I have the relation h : ab = c. I want to show that f(ab) = f(c). How can I show this? I tried rw h, but I get the error

rewrite tactic failed, did not find instance of the pattern in the target expression
 a * b

Any help is appreciated. Thank you!

[Bhavik Mehta]

rw h should work here - can you post a #mwe? If you really, really can't get it to work, two things you could try are tactic#conv or tactic#congr

[Ashvni Narayanan]

Ah, the congr tactic works, but the problem seems to be elsewhere. Thank you!