# apply hPQ at hP
[apply reference - Formalising Math - Mehta](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/apply.html#apply "Link to this heading")
Given an implication, hPQ, rewrite its premise, hP, as its conclusion: hQ : Q
apply hPQ at hP; rename' hP => hQ
This operation “<font color="#e36c09">argues forwards</font>”. It expresses <font color="#e36c09">modens ponens</font> in Lean.
The rename' operation is required because after renaming, hP is no longer of type P, but instead of type Q.
## Summary
[Summary reference - Mehta](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/apply.html#summary "Link to this heading")
| Initial local context | | |
| -------------------------------- | -------------------------------------------------------- | ------------------------------------------------------------------- |
| | hPQ : P → Q | Comments |
| | hP : P | |
| Operation | | |
| | apply hPQ at hP; [[rename' - tactic\| rename']] hP => hQ | hP is now of type Q, so renaming it to hQ corrects the mislabeling. |
| Resulting local context changes | | |
| | hQ : Q | hP has disappeared and is replaced by hQ |
# The apply operation as a backwards argument
The apply hPQ at hP tactic is easy to understand since it <font color="#e36c09">argues forward </font>and is an implementation of <font color="#e36c09">modens pones</font> in Lean.
The bare `apply` hPQ tactic is a little harder to understand, since it <font color="#e36c09">argues backward</font>, as a <font color="#e36c09">sufficiency proof</font>.
A Lean programmer might describe the `apply hPQ` operation is saying that :
It is a sufficient goal to focus on the implication premise, P, ⊢ P, when
- the implication, P -> Q, is true and
- the original proof goal was the conclusion , ⊢ Q,
Using this <font color="#e36c09">backwards argument</font>, we say that `apply` _reduces_ the goal from `Q` to P.
A logic student might describe the `apply hPQ` operation is saying that :
Using *modens pones* If we know that
- an implication is true and
- our goal is the prove the conclusion,
Then it is sufficient to prove that the premise is true, which enables us to use *modens pones*: P -> Q, P ⊢ Q
TODO - rewrite:
[Examples from Formalising Math - 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`.
# Credits
[Formalising Mathematics - Mehta](https://b-mehta.github.io/formalising-mathematics-notes/index.html#formalising-mathematics)/[apply](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/apply.html#apply)
[[dducoff]]: 2025 01 17