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