mathlib documentation

tactic.observe

observe #

The observe tactic is mainly intended for demo/educational purposes. Calling observe hp : p is equivalent to have hp : p, { library_search }.

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

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.

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

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.