# Simple tactics that are used throughout Batteries. #

`_`

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

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

## Instances For

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.

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

## Equations

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

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

## Equations

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

## Instances For

`split_ands`

applies `And.intro`

until it does not make progress.

## Equations

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

## Instances For

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

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

## Equations

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

## Instances For

Deprecated variant of `trivial`

.

## Equations

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

## Instances For

`conv`

tactic to close a goal using an equality theorem.

## Equations

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

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

## Equations

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