Documentation

Mathlib.Tactic.Observe

The observe tactic. #

observe hp : p asserts the proposition p, and tries to prove it using exact?.

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.

Equations
  • One or more equations did not get rendered due to their size.

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.

Equations
  • One or more equations did not get rendered due to their size.

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.

Equations
  • One or more equations did not get rendered due to their size.