Applying a function to both sides of an equation

Stream: new members

[Tung Tran]

I'm looking for a lemma that can do the following: $?a = ?b \to ?f ?a = ?f ?b$. Is there such a lemma or do we have to go around the problem? Thanks in advance!

[Andrew Yang]

Its docs#congr_arg .

[Andrew Yang]

This also gives you the answer

example (α β) (f : α → β) (x : α) (y = x) : f y = f x := by library_search