## Stream: new members

### Topic: Function

#### Ashvni Narayanan (Jun 24 2020 at 17:23):

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 (Jun 24 2020 at 17:24):

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 (Jun 24 2020 at 17:31):

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

Last updated: May 10 2021 at 00:31 UTC