apply

Warning

The apply tactic does two very specific things, 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.

Used alone, 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”.

Used “at” another hypothesis, it “argues forwards”, using the proof of an implication P → Q to change a hypothesis of P to one of Q.

Summary

If your local context is

h : P → Q
⊢ Q

then apply h changes the goal to ⊢ P.

And if you have two hypotheses like this:

h : P → Q
h2 : P

then apply h at h2 changes h2 to h2 : Q.

Note

apply h and apply h at h' will not work unless h is of the form P → Q. apply h will also not work unless the goal is equal to the conclusion Q of h, and apply h at h2 will not work unless h2 is a proof of the premise P 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, apply ... at ... is easy to understand; we have a hypothesis saying that P implies Q, so we can use it to change a hypothesis P to Q. The bare apply tactic is a little harder to understand. Say 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 two hypotheses like this:

h : x = 3 → y = 4
h2 : x = 3

then apply h at h2 will change h2 to a proof of y = 4.

  1. If your tactic state 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. apply can also be used in the following situation:

import Mathlib.Tactic

example (X Y : Type) (φ ψ : X → Y) (h : ∀ a, φ a = ψ a) (x : X) :
   φ x = ψ x := by
apply h
done

Here h can be thought of as a function which takes as input an element of X and returns a proof, so apply makes sense.

  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 ?_.