Consider this code:

```
From Coq Require Import ZArith.
Notation ℤ := Z.
Open Scope Z_scope.
Hint Resolve Z.sub_add: localHints.
Definition f (x: ℤ): ℤ := x - 100.
Definition g (x: ℤ): {y | f y = x} := ltac:(debug eauto with localHints).
```

It does not type check. But this does:

```
From Coq Require Import ZArith.
Notation ℤ := Z.
Open Scope Z_scope.
Definition f (x: ℤ): ℤ := x - 100.
Definition g (x: ℤ): {y | f y = x} := ltac:(debug eauto using Z.sub_add).
```

I know that `auto`

tries to use `simple eapply`

under the hood and it is not strong enough to solve this goal — `eapply`

without `simple`

is needed. But why does the `using`

option work?

Here is what `debug`

says:

```
Debug: 1 depth=5
Debug: 1.1 depth=4 simple eapply exist
Debug: 1.1.1 depth=4 simple apply Z.sub_add
g is defined
```

When I literally write this down in a proof script, it predictably fails.

```
Definition g (x: ℤ): {y | f y = x}.
Proof.
simple eapply exist.
simple apply Z.sub_add.
```

```
Unable to unify "?M1384 - ?M1383 + ?M1383 = ?M1384" with
"f ?y = x".
```

What is going on?