This proof would be a welcome contribution to the library!

The syntax of `proof_wanted`

declarations is just like that of `theorem`

, but without `:=`

or the
proof. Lean checks that `proof_wanted`

declarations are well-formed (e.g. it ensures that all the
mentioned names are in scope, and that the theorem statement is a valid proposition), but they are
discarded afterwards. This means that they cannot be used as axioms.

Typical usage:

```
@[simp] proof_wanted empty_find? [BEq α] [Hashable α] {a : α} :
(∅ : HashMap α β).find? a = none
```

## Equations

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

## Instances For

Elaborate a `proof_wanted`

declaration. The declaration is translated to an axiom during
elaboration, but it's then removed from the environment.

## Equations

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