## Equations

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

## Instances For

## Equations

## Instances For

`match`

performs case analysis on one or more expressions.
See Induction and Recursion.
The syntax for the `match`

tactic is the same as term-mode `match`

, except that
the match arms are tactics instead of expressions.

```
example (n : Nat) : n = n := by
match n with
| 0 => rfl
| i+1 => simp
```

## Equations

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

## Instances For

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.

## Equations

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

## Instances For

`decide`

attempts to prove the main goal (with target type `p`

) by synthesizing an instance of `Decidable p`

and then reducing that instance to evaluate the truth value of `p`

.
If it reduces to `isTrue h`

, then `h`

is a proof of `p`

that closes the goal.

Limitations:

- The target is not allowed to contain local variables or metavariables.
If there are local variables, you can try first using the
`revert`

tactic with these local variables to move them into the target, which may allow`decide`

to succeed. - Because this uses kernel reduction to evaluate the term,
`Decidable`

instances defined by well-founded recursion might not work, because evaluating them requires reducing proofs. The kernel can also get stuck reducing`Decidable`

instances with`Eq.rec`

terms for rewriting propositions. These can appear for instances defined using tactics (such as`rw`

and`simp`

). To avoid this, use definitions such as`decidable_of_iff`

instead.

## Examples #

Proving inequalities:

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

Trying to prove a false proposition:

```
example : 1 ≠ 1 := by decide
/-
tactic 'decide' proved that the proposition
1 ≠ 1
is false
-/
```

Trying to prove a proposition whose `Decidable`

instance fails to reduce

```
opaque unknownProp : Prop
open scoped Classical in
example : unknownProp := by decide
/-
tactic 'decide' failed for proposition
unknownProp
since its 'Decidable' instance reduced to
Classical.choice ⋯
rather than to the 'isTrue' constructor.
-/
```

## Properties and relations #

For equality goals for types with decidable equality, usually `rfl`

can be used in place of `decide`

.

```
example : 1 + 1 = 2 := by decide
example : 1 + 1 = 2 := by rfl
```

## Equations

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

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

## Equations

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