Table of Contents - Lean Notes

## Tactics - Table of Contents ### Tactics from apply to intro | **`Tactic`** | **`Description`** | | -------------------------------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | [[apply-tactic\|apply]] *hypothesis* | If `hPimpQ : P → Q`is a hypotheses, and the goal is its conclusion type, `⊢ Q`, then invoking `apply hPimpQ` changes the goal from the conclusion to the premise type, `⊢ P`. Once the premise, `P` has been proven, it follows by `Modus Ponens (MP)` that the conclusion, `Q` is proven. | | [[apply-at-tactic\|apply]] *hypotheses* at *premise* | If there are hypotheses that assume a conditional and its premise, $~~~~~

hPimpQ : P → Q` and `hP : P`, then `Modus Ponens (MP)` can be applied by invoking $~~~~~~$***apply*** `hPimpQ` at `hP`. This will change the type of `hP : P` to the conclusion, `hP : Q`. | | [[assumption-tactic\|assumption]] | Search all of the hypotheses for an *implicit* match with the goal. In contrast to the assumption tactic, the [[exact-tactic 1\|exact]] tactic requires a hypotheses parameter because provides an *explicit* match with the goal. | | [[assumption-loop-tactic\|assumption-loop]] | Loop through the goals to find a match with a hypothesis. | | [[Tactics/by_contra-tactic\|by_contra]] *contrary hypotheses* | If the goal is `⊢ P`, then **`by_contra`** `h_notP : ¬P` provides a proof by contradiction. It constructs the hypothesis `h_notP : ¬P` and changes the goal to false, `⊢ False`. | | [[change-tactic\|change]] *new_goal_equivalent* | If the goal is `⊢ P`, and if `P` and `P_equivalent` are [definitionally equal](https://b-mehta.github.io/formalising-mathematics-notes/Part_1/equality.html#definitional-equality), then **change** `P_equivalent` will change the goal to `P_equivalent. | | [[change-at-tactic#change *new__equivalent_type* at *hypothesis_type*\|change]] *new__equivalent_type* at *hypothesis_type* | If a hypothesis has type `P`, and if `P` and `P_equivalentType` are [definitionally equal](https://b-mehta.github.io/formalising-mathematics-notes/Part_1/equality.html#definitional-equality), then **change** `P_equivalentType` **at** `hP` changes `hP : P` to `hP : P_equivalentType`. | | [[have-tactic\|have]]`hHypotheses :` _Type_ `:= by` _Proof_by_tactics_ | add hypothesis `hHypotheses` to the context after proving it in tactics mode. | | [[have-tactic\|have]]`hHypotheses :` _Type_ `:=` _Proof_by_terms_ | add hypothesis `hHypotheses` to the context after proving it in term mode. | | [[Tactics/intro-tactic\|intro]] *premise hypotheses* | if the goal is a `conditional`, `⊢ P → Q` then the `premise` can be assumed as a hypotheses, `hP : P` and the goal can be reduced to its `conclusion`, `⊢ Q`, by applying **intro*** `(hP : P)`. | | | | --- **`LeanNotes curator:`** [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL) **`Posted Date`**: 2026-08-15