Simple function lemma

Stream: new members

[Julian Sutherland]

I find myself frequently wanting to use the following straightforward lemma that holds for any function f:

  lemma eq_lemma : ∀ {α β : Type} {a b : α} (f : α → β), a = b → f a = f b :=
    begin
      intros α β a b g a_eq_b,
      rw a_eq_b,
    end

Is there already such a lemma in mathlib or init or an appropriate tactic?

[Patrick Johnson]

docs#congr_arg

[Julian Sutherland]

Perfect, thank you! :)