## Stream: new members

### Topic: congr

#### kana (Feb 18 2021 at 19:30):

How to move from a = b goal to f a = f b?

#### Yakov Pechersky (Feb 18 2021 at 19:37):

Do you know that f is injective?

#### kana (Feb 18 2021 at 19:42):

Oh, my bad, I understood why it is not correct in the general case. Thanks

#### Eric Wieser (Feb 18 2021 at 20:08):

apply (_ : function.injective f) would probably do it.

Last updated: May 13 2021 at 21:12 UTC