apply function to both sides of equation

Stream: new members

[Vasily Ilin]

If I have h: a=b and f: X \to Y with a b: X, how do I prove f a = f b?

[Stuart Presnell]

example (X Y : Type*) (a b: X) (h: a = b) (f: X → Y) : f a = f b :=
begin
  library_search,   -- suggests   refine congr_arg f h
end

[Vasily Ilin]

Thank you!

[Kyle Miller]

There's also a tactic for this:

example (X Y : Type*) (a b: X) (h: a = b) (f: X → Y) : f a = f b :=
begin
  apply_fun f at h,
  exact h,
end

[Vasily Ilin]

Thanks, Kyle! That's more of what I expected!

[Adam Topaz]

apply_fun can also be used on the goal itself, which will introduce an obligation to prove injectivity (if the tactic can't do it automatically). This is one of my favorite tactics!