In the following tables, name always refers to a name already known to Lean
while new_name is a new name provided by the user;
expr means an expression,
for example the name of an object in the context,
an arithmetic expression that is a function of such objects,
a hypothesis in the context,
or a lemma applied to any of these;
proposition is an expression of the type Prop (e.g. 0 < x).
When one of these words appears twice in the same cell,
the appearances do not designate the same name or the same expression.
The following table shows usual responses to logical symbols based on their placement.
| Logical symbol | Appears in goal | Appears in hypothesis |
|---|---|---|
∀ (for all) |
intro new_name |
apply expr or specialize name expr |
∃ (there exists) |
use expr |
obtain ⟨new_name, new_name⟩ := expr |
→ (implies) |
intro new_name |
apply expr or specialize name expr |
↔ (if and only if) |
constructor |
rw [expr] or rw [←expr] |
∧ (and) |
constructor |
obtain ⟨new_name, new_name⟩ := expr |
∨ (or) |
left or right |
cases expr with | inl new_name => ... | inr new_name => ... |
¬ (not) |
intro new_name |
apply expr or specialize name expr |
In the left-hand column, the parts in parentheses are optional. The effect of these parts in the right-hand column is also written in parentheses.
| Tactic | Effect |
|---|---|
exact expr |
assert that the goal can be satisfied by expr |
refine |
TODO |
convert expr |
prove the goal by transforming it to an existing fact expr and create goals for propositions used in the transformation that were not proved automatically |
convert_to proposition |
transform the goal into the goal proposition and create additional goals for propositions used in the transformation that were not proved automatically |
have new_name : proposition |
introduce a name new_name asserting that proposition is true; at the same time, create and focus a goal for proposition |
unfold name (at hyp) |
unfold the definition of name in the goal (or in the hypothesis hyp) |
rw [expr] (at hyp) |
in the goal (or in the hypothesis hyp), replace (all occurrences of) the left-hand side of the equality or equivalence expr by its right-hand side |
rw [←expr] (at hyp) |
in the goal (or in the hypothesis hyp), replace (all occurrences of) the right-hand side of the equality or equivalence expr by its left-hand side |
rw [expr, expr, ←expr, ←expr, expr] |
perform several rewritings in a sequence (can again be used in the goal or in given hypothesis; any subset of expr can again be applied from right to left) |
calc |
start a proof by calculation (i.e., a sequence of propositions that, when combined together using transitivity, will prove the goal) |
gcongr |
TODO |
by_cases new_name : proposition |
split the proof into two branches depending on whether proposition is true or false, using new_name as name for the respective hypothesis in both branches |
exfalso |
apply the rule "False implies anything" a.k.a. "ex falso quodlibet" (replaces the goal by False) |
by_contra new_name |
start a proof by contradiction, using new_name as name for the hypothesis that is the negation of the goal |
push_neg (at hyp) |
push negations in the goal (or in the hypothesis hyp),e.g. change ¬ ∀ x, proposition to ∃ x, ¬ proposition |
linarith |
prove the goal by a linear combination of hypotheses (includes arguments based on transitivity) |
ring |
prove the goal by combining the axioms of a commutative (semi)ring |
simp (at hyp) |
simplify the goal (or the hypothesis hyp) by combining some standard equalities and equivalences |
simp? (at hyp) |
show which equalities and equivalences would be used to simplify the goal (or the hypothesis hyp); give a list of expressions that can be used inside simp only [...] (at hyp) |
exact? |
search for a single existing lemma which closes the goal, also using local hypotheses |
apply? |
search for lemmas whose conclusion matches the goal; suggest those that may be used with apply or refine |
rw? (at hyp) |
search for lemmas that can rewrite the goal (or the hypothesis hyp), irrespective of their practicality |
aesop |
try to solve the goal using magic |
aesop? |
try to solve the goal using magic and show what kind of magic was used (usually produces unreadable output but the names of relevant lemmas are there) |