a = b \to f a = f b?

Stream: Lean for teaching

[Kevin Buzzard]

Wasn't there some teaching tactic which could be used on hypotheses of the form a = b and turn them into f a = f b? You could do this with a have and a rewrite but then the name changes, and this is one operation for a mathematician. @Patrick Massot didn't you think about this once?

[Bryan Gin-ge Chen]

Do you just want some shorthand for replace h := congr_arg f h or do you need something fancier?

[Kevin Buzzard]

oh maybe we wanted apply f at h or something?

[Bryan Gin-ge Chen]

For what it's worth the replace docstring includes the following: "This can be used to simulate the specialize and apply at tactics of Coq."

[Yury G. Kudryashov]

See https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#apply_fun

[Bryan Gin-ge Chen]

Would it make sense to merge apply_fun into apply in the next version of community Lean? (along with apply' I guess)

[Floris van Doorn]

The behavior I expect for apply f at h (and the behavior of Coq's apply f in h) is:
If f : A -> B then apply f at h replaces the hypothesis h : A by the hypothesis h : B.