Basic guide to tactics

This guide might be of use when you are in a situation where you know exactly what you want to do “in real life” in your proof, but don’t know how to do it in Lean. For example, you might be faced with a hypothesis of the form p ∧ q and you need a proof of p, or you might be faced with a goal of the form p ∨ q which you want to deduce from a proof of p.

How to use the guide

Let’s say that you know your next step involves p ∧ q in some way. Which tactic you use depends on whether p ∧ q is a hypothesis (i.e. you have the assumption H : p ∧ q in your local context) or the goal (i.e. what you are trying to prove). If it is a hypothesis then you need to eliminate it, whereas if it is the goal then you need to introduce it.

Once you have established whether you want to introduce or eliminate it, find the function in the list below and you will see the tactic you need. Click on the link to see an example of usage.

Type of term	To introduce	To eliminate
P → Q	intro	function application
P ∧ Q	split	cases
P ∨ Q	left, right	cases
∃ a : X, H	existsi	cases
∀ a : X, H	intro	function application
P ↔ Q	split	cases
¬ P	intro	function application

Note for functions: There are two ways that one might want to use a hypothesis H : P → Q (or a ∀ or ¬, which Lean stores internally as a function). If you also have a term of type P, then you can apply the function with have HQ : Q := H HP if Q : Prop (or let HQ : Q := H HP if Q : Type). If however your goal is Q, the target of the function, and you want to change the goal to P, you can use the apply tactic directly. In the case of hypotheses of the form ¬ P, apply is a very cute tactic to use; see the example above.

The eliminators follow a pattern – the inductive types are all eliminated with the cases tactic, and the function types (Pi types) are all eliminated via function application. Similarly the function types are all introduced with the intro tactic, however there is more of an art to introducing inductive types.