# The `use`

tactic #

The `use`

and `use!`

tactics are for instantiating one-constructor inductive types
just like the `exists`

tactic, but they can be a little more flexible.

`use`

is the more restrained version for mathlib4, and `use!`

is the exuberant version
that more closely matches `use`

from mathlib3.

Note: The `use!`

tactic is almost exactly the mathlib3 `use`

except that it does not try
applying `exists_prop`

. See the failing test in `test/Use.lean`

.

When the goal `mvarId`

is an inductive datatype with a single constructor,
this applies that constructor, then returns metavariables for the non-parameter explicit arguments
along with metavariables for the parameters and implicit arguments.

The first list of returned metavariables correspond to the arguments that `⟨x,y,...⟩`

notation uses.
The second list corresponds to everything else: the parameters and implicit arguments.
The third list consists of those implicit arguments that are instance implicits, which one can
try to synthesize. The third list is a sublist of the second list.

Returns metavariables for all arguments whether or not the metavariables are assigned.

## Instances For

Use the `args`

to refine the goals `gs`

in order, but whenever there is a single
goal remaining then first try applying a single constructor if it's for a single-constructor
inductive type. In `eager`

mode, instead we always first try to refine, and if that fails we
always try to apply such a constructor no matter if it's the last goal.

Returns the remaining explicit goals `gs`

, any goals `acc`

due to `refine`

, and a sublist of these
of instance arguments that we should try synthesizing after the loop.
The new set of goals should be `gs ++ acc`

.

Run the `useLoop`

on the main goal then discharge remaining explicit `Prop`

arguments.

## Instances For

Default discharger to try to use for the `use`

and `use!`

tactics.
This is similar to the `trivial`

tactic but doesn't do things like `contradiction`

or `decide`

.

## Instances For

Returns a `TacticM Unit`

that either runs the tactic sequence from `discharger?`

if it's
non-`none`

, or it does `try with_reducible use_discharger`

.

## Instances For

`use e₁, e₂, ⋯`

is similar to `exists`

, but unlike `exists`

it is equivalent to applying the tactic
`refine ⟨e₁, e₂, ⋯, ?_, ⋯, ?_⟩`

with any number of placeholders (rather than just one) and
then trying to close goals associated to the placeholders with a configurable discharger (rather
than just `try trivial`

).

Examples:

```
example : ∃ x : Nat, x = x := by use 42
example : ∃ x : Nat, ∃ y : Nat, x = y := by use 42, 42
example : ∃ x : String × String, x.1 = x.2 := by use ("forty-two", "forty-two")
```

`use! e₁, e₂, ⋯`

is similar but it applies constructors everywhere rather than just for
goals that correspond to the last argument of a constructor. This gives the effect that
nested constructors are being flattened out, with the supplied values being used along the
leaves and nodes of the tree of constructors.
With `use!`

one can feed in each `42`

one at a time:

```
example : ∃ p : Nat × Nat, p.1 = p.2 := by use! 42, 42
example : ∃ p : Nat × Nat, p.1 = p.2 := by use! (42, 42)
```

The second line makes use of the fact that `use!`

tries refining with the argument before
applying a constructor. Also note that `use`

/`use!`

by default uses a tactic
called `use_discharger`

to discharge goals, so `use! 42`

will close the goal in this example since
`use_discharger`

applies `rfl`

, which as a consequence solves for the other `Nat`

metavariable.

These tactics take an optional discharger to handle remaining explicit `Prop`

constructor arguments.
By default it is `use (discharger := try with_reducible use_discharger) e₁, e₂, ⋯`

.
To turn off the discharger and keep all goals, use `(discharger := skip)`

.
To allow "heavy refls", use `(discharger := try use_discharger)`

.

## Instances For

`use e₁, e₂, ⋯`

is similar to `exists`

, but unlike `exists`

it is equivalent to applying the tactic
`refine ⟨e₁, e₂, ⋯, ?_, ⋯, ?_⟩`

with any number of placeholders (rather than just one) and
then trying to close goals associated to the placeholders with a configurable discharger (rather
than just `try trivial`

).

Examples:

```
example : ∃ x : Nat, x = x := by use 42
example : ∃ x : Nat, ∃ y : Nat, x = y := by use 42, 42
example : ∃ x : String × String, x.1 = x.2 := by use ("forty-two", "forty-two")
```

`use! e₁, e₂, ⋯`

is similar but it applies constructors everywhere rather than just for
goals that correspond to the last argument of a constructor. This gives the effect that
nested constructors are being flattened out, with the supplied values being used along the
leaves and nodes of the tree of constructors.
With `use!`

one can feed in each `42`

one at a time:

```
example : ∃ p : Nat × Nat, p.1 = p.2 := by use! 42, 42
example : ∃ p : Nat × Nat, p.1 = p.2 := by use! (42, 42)
```

The second line makes use of the fact that `use!`

tries refining with the argument before
applying a constructor. Also note that `use`

/`use!`

by default uses a tactic
called `use_discharger`

to discharge goals, so `use! 42`

will close the goal in this example since
`use_discharger`

applies `rfl`

, which as a consequence solves for the other `Nat`

metavariable.

These tactics take an optional discharger to handle remaining explicit `Prop`

constructor arguments.
By default it is `use (discharger := try with_reducible use_discharger) e₁, e₂, ⋯`

.
To turn off the discharger and keep all goals, use `(discharger := skip)`

.
To allow "heavy refls", use `(discharger := try use_discharger)`

.