# Zulip Chat Archive

## Stream: Lean for teaching

### Topic: a = b \to f a = f b?

#### Kevin Buzzard (Jan 31 2020 at 04:22):

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 (Jan 31 2020 at 04:38):

Do you just want some shorthand for `replace h := congr_arg f h`

or do you need something fancier?

#### Kevin Buzzard (Jan 31 2020 at 04:45):

oh maybe we wanted `apply f at h`

or something?

#### Bryan Gin-ge Chen (Jan 31 2020 at 04:52):

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 (Jan 31 2020 at 04:55):

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

#### Bryan Gin-ge Chen (Jan 31 2020 at 05:11):

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 (Jan 31 2020 at 22:25):

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`

.

Last updated: Dec 20 2023 at 11:08 UTC