1.1. Interactive

observe

observe hp : p asserts the proposition p, and tries to prove it using exact?. If no proof is found, the tactic fails. In other words, this tactic is equivalent to have hp : p := by exact?.

If hp is omitted, then the placeholder this is used.

The variant observe? hp : p will emit a trace message of the form have hp : p := proof_term. This may be particularly useful to speed up proofs.

exact?

Searches environment for definitions or theorems that can solve the goal using exact with conditions resolved by solve_by_elim.

The optional using clause provides identifiers in the local context that must be used by exact? when closing the goal. This is most useful if there are multiple ways to resolve the goal, and one wants to guide which lemma is used.

apply?

Searches environment for definitions or theorems that can refine the goal using apply with conditions resolved when possible with solve_by_elim.

The optional using clause provides identifiers in the local context that must be used when closing the goal.

rw?

rw? tries to find a lemma which can rewrite the goal.

rw? should not be left in proofs; it is a search tool, like apply?.

Suggestions are printed as rw [h] or rw [← h].

You can use rw? [-my_lemma, -my_theorem] to prevent rw? using the named lemmas.

hint

The hint tactic tries every tactic registered using register_hint tac, and reports any that succeed.