`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.

## Instances For

`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.

## Instances For

`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.