Apply implication to hypothesis

Stream: Berkeley Lean Seminar

[Thomas Browning]

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]

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

[Pedro Minicz]

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]

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

[Pedro Minicz]

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

[Kevin Buzzard]

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