`exfalso`

converts a goal `⊢ tgt`

into `⊢ False`

by applying `False.elim`

.

## Equations

- Std.Tactic.tacticExfalso = Lean.ParserDescr.node `Std.Tactic.tacticExfalso 1024 (Lean.ParserDescr.nonReservedSymbol "exfalso" false)

`_`

in tactic position acts like the `done`

tactic: it fails and gives the list
of goals if there are any. It is useful as a placeholder after starting a tactic block
such as `by _`

to make it syntactically correct and show the current goal.

## Equations

- Std.Tactic.tactic_ = Lean.ParserDescr.node `Std.Tactic.tactic_ 1024 (Lean.ParserDescr.nonReservedSymbol "_" false)

`fail_if_success t`

fails if the tactic `t`

succeeds.

## Equations

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

`rwa`

calls `rw`

, then closes any remaining goals using `assumption`

.

## Equations

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

Like `exact`

, but takes a list of terms and checks that all goals are discharged after the tactic.

## Equations

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

`by_contra h`

proves `⊢ p`

by contradiction,
introducing a hypothesis `h : ¬p`

and proving `False`

.

- If
`p`

is a negation`¬q`

,`h : q`

will be introduced instead of`¬¬q`

. - If
`p`

is decidable, it uses`Decidable.byContradiction`

instead of`Classical.byContradiction`

. - If
`h`

is omitted, the introduced variable`_: ¬p`

will be anonymous.

## Equations

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

`iterate n tac`

runs `tac`

exactly `n`

times.
`iterate tac`

runs `tac`

repeatedly until failure.

To run multiple tactics, one can do `iterate (tac₁; tac₂; ⋯)`

or

```
iterate
tac₁
tac₂
⋯
```

## Equations

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

`repeat' tac`

runs `tac`

on all of the goals to produce a new list of goals,
then runs `tac`

again on all of those goals, and repeats until `tac`

fails on all remaining goals.

## Equations

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

`repeat1 tac`

applies `tac`

to main goal at least once. If the application succeeds,
the tactic is applied recursively to the generated subgoals until it eventually fails.

## Equations

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

`subst_eqs`

applies `subst`

to all equalities in the context as long as it makes progress.

## Equations

- Std.Tactic.tacticSubst_eqs = Lean.ParserDescr.node `Std.Tactic.tacticSubst_eqs 1024 (Lean.ParserDescr.nonReservedSymbol "subst_eqs" false)

`split_ands`

applies `And.intro`

until it does not make progress.

## Equations

- Std.Tactic.tacticSplit_ands = Lean.ParserDescr.node `Std.Tactic.tacticSplit_ands 1024 (Lean.ParserDescr.nonReservedSymbol "split_ands" false)

`fapply e`

is like `apply e`

but it adds goals in the order they appear,
rather than putting the dependent goals first.

## Equations

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

`eapply e`

is like `apply e`

but it does not add subgoals for variables that appear
in the types of other goals. Note that this can lead to a failure where there are
no goals remaining but there are still metavariables in the term:

```
example (h : ∀ x : Nat, x = x → True) : True := by
eapply h
rfl
-- no goals
-- (kernel) declaration has metavariables '_example'
```

## Equations

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

Tries to solve the goal using a canonical proof of `True`

, or the `rfl`

tactic.
Unlike `trivial`

or `trivial'`

, does not use the `contradiction`

tactic.

## Equations

- Std.Tactic.triv = Lean.ParserDescr.node `Std.Tactic.triv 1024 (Lean.ParserDescr.nonReservedSymbol "triv" false)

`conv`

tactic to close a goal using an equality theorem.

## Equations

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