`exfalso`

converts a goal `⊢ tgt`

into `⊢ False`

by applying `False.elim`

.

## Instances For

`_`

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.

## Instances For

`fail_if_success t`

fails if the tactic `t`

succeeds.

## Instances For

`rwa`

calls `rw`

, then closes any remaining goals using `assumption`

.

## Instances For

Like `exact`

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

## Instances For

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

## Instances For

Given a proof `h`

of `p`

, `absurd h`

changes the goal to `⊢ ¬ p`

.
If `p`

is a negation `¬q`

then the goal is changed to `⊢ q`

instead.

## Instances For

`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₂
⋯
```

## Instances For

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

## Instances For

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

## Instances For

`subst_eqs`

applies `subst`

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

## Instances For

`split_ands`

applies `And.intro`

until it does not make progress.

## Instances For

`fapply e`

is like `apply e`

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

## Instances For

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

## Instances For

`conv`

tactic to close a goal using an equality theorem.

## Instances For

The `conv`

tactic `equals`

claims that the currently focused subexpression is equal
to the given expression, and proves this claim using the given tactic.

```
example (P : (Nat → Nat) → Prop) : P (fun n => n - n) := by
conv in (_ - _) => equals 0 =>
-- current goal: ⊢ n - n = 0
apply Nat.sub_self
-- current goal: P (fun n => 0)
```