The tactic

```
intro
| pat1 => tac1
| pat2 => tac2
```

is the same as:

```
intro x
match x with
| pat1 => tac1
| pat2 => tac2
```

That is, `intro`

can be followed by match arms and it introduces the values while
doing a pattern match. This is equivalent to `fun`

with match arms in term mode.

## Instances For

`decide`

will attempt to prove a goal of type `p`

by synthesizing an instance
of `Decidable p`

and then evaluating it to `isTrue ..`

. Because this uses kernel
computation to evaluate the term, it may not work in the presence of definitions
by well founded recursion, since this requires reducing proofs.

```
example : 2 + 2 ≠ 5 := by decide
```

## Instances For

`native_decide`

will attempt to prove a goal of type `p`

by synthesizing an instance
of `Decidable p`

and then evaluating it to `isTrue ..`

. Unlike `decide`

, this
uses `#eval`

to evaluate the decidability instance.

This should be used with care because it adds the entire lean compiler to the trusted
part, and the axiom `ofReduceBool`

will show up in `#print axioms`

for theorems using
this method or anything that transitively depends on them. Nevertheless, because it is
compiled, this can be significantly more efficient than using `decide`

, and for very
large computations this is one way to run external programs and trust the result.

```
example : (List.range 1000).length = 1000 := by native_decide
```