Zulip Chat Archive

Stream: Berkeley Lean Seminar

Topic: Apply implication to hypothesis


Thomas Browning (May 26 2020 at 20:13):

Suppose that I have a hypothesis h : succ a = succ b. How would I apply succ_inj to this hypothesis? apply succ_inj a b at h doesn't seem to work.

Pedro Minicz (May 26 2020 at 20:18):

You can use have h' := succ_inj h. Apply is just a fancy function application.

Pedro Minicz (May 26 2020 at 20:19):

There may be other, more elegant alternatives, but I can't remember. apply f at h is something I think should be possible. Some discussion about it has happened here before (let's hope it eventually gets implemented).

Patrick Lutz (May 26 2020 at 20:22):

You can also use replace if you want to have h refer to the new hypothesis

Pedro Minicz (May 26 2020 at 20:23):

Yes! refine succ_inj h is another option (the more elegant one I wasn't remembering earlier).

Kevin Buzzard (May 27 2020 at 11:17):

Patrick Massot (another mathematician) wanted this so wrote his own tactic, tactic#apply_fun


Last updated: Dec 20 2023 at 11:08 UTC