apply

Warning

The apply tactic does one very specific thing, which I explain below. I have seen students trying to use this tactic to do all sorts of other things, based solely on the fact that they want to “apply a theorem” or “apply a technique”. The English word “apply” has far more uses than the Lean apply tactic. The apply tactic “argues backwards”, using an implication to reduce the goal to something closer to the hypotheses. apply h is like saying “because of h, it suffices to prove this new simpler thing”.

Summary

If your local context is

h : P → Q
⊢ Q

then apply h changes the goal to ⊢ P.

Note

apply h will not work unless h is of the form P → Q. It will also not work unless the goal is equal to the conclusion of h. You will get an obscure error message if you try using apply in situations which do not conform to the pattern above.

Mathematically, the apply tactic does this: We’re trying to prove Q. If we know that P implies Q then of course it would suffice to prove P instead, because P implies Q. So apply reduces the goal from Q to P. If you like, apply executes the last step of a proof of Q, rather than what many mathematicians would think of as the “next” step.

If instead of an implication you have an iff statement h : P ↔ Q then apply h won’t work. You might want to “apply” h by using the rw (rewrite) tactic.

Examples

  1. If you have a hypothesis which is

h : a ^ 2 = b → a ^ 4 = b ^ 2
⊢ a ^ 4 = b ^ 2

then apply h will change the goal to ⊢ a ^ 2 = b.

  1. apply works up to definitional equality. For example if your local context is

h : ¬P
⊢ false

then apply h works and changes the goal to ⊢ P. This is because h is definitionally equal to P → false.

  1. The apply tactic does actually have one more trick up its sleeve: in the situation

h : P → Q → R
⊢ R

the tactic apply h will work (even though the brackets in h which Lean doesn’t print are P → (Q → R)), and the result will be two goals ⊢ P and ⊢ Q. Mathematically, what is happening is that h says “if P is true, then if Q is true, then R is true”, hence to prove R is true it suffices to prove that P and Q are true.

Further notes

The refine tactic is a more refined version of apply. For example, if h : P → Q and the goal is ⊢ Q then apply h does the same thing as refine h _.