**Source**: [apply reference - Mehta](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/apply.html#apply "Link to this heading")
The **apply** tactic “<font color="#e36c09">argues backwards</font>”, using an implication to rewrite the goal from the implication conclusion to the implication premise.
**apply h** is like saying:
“because of the given implication and the goal being the implication's conclusion , it suffices to prove the implication's premise."
## Summary
| Initial local context | |
| -------------------------------- | ----------- |
| | h : P → Q |
| | ⊢ Q |
| Operation | |
| | **apply h** |
| Resulting local context changes | |
| | ⊢ 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`. `applyh` will also _not work_ unless the goal is equal to the conclusion `Q` of `h`, and `apply h ath2` 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](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/rw.html#tac-rw) (rewrite) tactic.
## Examples
[Examples - Metha](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/apply.html#examples "Link to this heading")
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`.
2. 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`.
3. `apply` works up to [definitional equality](https://b-mehta.github.io/formalising-mathematics-notes/Part_1/equality.html#defeq). For example if your local context is
4.
h : ¬P
⊢ False
then `apply h` works and changes the goal to `⊢ P`. This is because `h` is definitionally equal to `P → False`.
4. `apply` can also be used in the following situation:
```lean
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.
5. The `apply` tactic does actually have one more trick up its sleeve: in the situation
hPQR : 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
[Further notes - Metha](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/apply.html#further-notes "Link to this heading")
The [refine](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/refine.html#tac-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 ?_`.
# Credits
[[Bhavik Mehta]] : [apply](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/apply.html#apply)
[[dducoff]]: 2025 01 17