# The `on_goal`

, `pick_goal`

, and `swap`

tactics. #

`pick_goal n`

moves the `n`

-th goal to the front. If `n`

is negative this is counted from the back.

`on_goal n => tacSeq`

focuses on the `n`

-th goal and runs a tactic block `tacSeq`

.
If `tacSeq`

does not close the goal any resulting subgoals are inserted back into the list of goals.
If `n`

is negative this is counted from the back.

`swap`

is a shortcut for `pick_goal 2`

, which interchanges the 1st and 2nd goals.

If the current goals are `g₁ ⋯ gᵢ ⋯ gₙ`

, `splitGoalsAndGetNth i`

returns
`(gᵢ, [g₁, ⋯, gᵢ₋₁], [gᵢ₊₁, ⋯, gₙ])`

.

If `reverse`

is passed as `true`

, the `i`

-th goal is picked by counting backwards.
For instance, `splitGoalsAndGetNth 1 true`

puts the last goal in the first component
of the returned term.

## Equations

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

## Instances For

`pick_goal n`

will move the `n`

-th goal to the front.

`pick_goal -n`

will move the `n`

-th goal (counting from the bottom) to the front.

See also `Tactic.rotate_goals`

, which moves goals from the front to the back and vice-versa.

## Equations

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

## Instances For

`swap`

is a shortcut for `pick_goal 2`

, which interchanges the 1st and 2nd goals.

## Equations

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

## Instances For

`on_goal n => tacSeq`

creates a block scope for the `n`

-th goal and tries the sequence
of tactics `tacSeq`

on it.

`on_goal -n => tacSeq`

does the same, but the `n`

-th goal is chosen by counting from the
bottom.

The goal is not required to be solved and any resulting subgoals are inserted back into the list of goals, replacing the chosen goal.

## Equations

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