`conv`

is the syntax category for a "conv tactic", where "conv" is short
for conversion. A conv tactic is a program which receives a target, printed as
`| a`

, and is tasked with coming up with some term `b`

and a proof of `a = b`

.
It is mainly used for doing targeted term transformations, for example rewriting
only on the left side of an equality.

## Equations

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

The `*`

occurrence list means to apply to all occurrences of the pattern.

## Equations

- Lean.Parser.Tactic.Conv.occsWildcard = Lean.ParserDescr.nodeWithAntiquot "occsWildcard" `Lean.Parser.Tactic.Conv.occsWildcard (Lean.ParserDescr.symbol "*")

## Instances For

A list `1 2 4`

of occurrences means to apply to the first, second, and fourth
occurrence of the pattern.

## Equations

- Lean.Parser.Tactic.Conv.occsIndexed = Lean.ParserDescr.nodeWithAntiquot "occsIndexed" `Lean.Parser.Tactic.Conv.occsIndexed (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.const `num))

## Instances For

An occurrence specification, either `*`

or a list of numbers. The default is `[1]`

.

## Equations

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

## Instances For

`with_annotate_state stx t`

annotates the lexical range of `stx : Syntax`

with
the initial and final state of running tactic `t`

.

## Equations

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

## Instances For

`skip`

does nothing.

## Equations

- Lean.Parser.Tactic.Conv.skip = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.skip 1024 (Lean.ParserDescr.nonReservedSymbol "skip" false)

## Instances For

Traverses into the left subterm of a binary operator.
(In general, for an `n`

-ary operator, it traverses into the second to last argument.)

## Equations

- Lean.Parser.Tactic.Conv.lhs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.lhs 1024 (Lean.ParserDescr.nonReservedSymbol "lhs" false)

## Instances For

Traverses into the right subterm of a binary operator.
(In general, for an `n`

-ary operator, it traverses into the last argument.)

## Equations

- Lean.Parser.Tactic.Conv.rhs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.rhs 1024 (Lean.ParserDescr.nonReservedSymbol "rhs" false)

## Instances For

Traverses into the function of a (unary) function application.
For example, `| f a b`

turns into `| f a`

. (Use `arg 0`

to traverse into `f`

.)

## Equations

- Lean.Parser.Tactic.Conv.fun = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.fun 1024 (Lean.ParserDescr.nonReservedSymbol "fun" false)

## Instances For

Reduces the target to Weak Head Normal Form. This reduces definitions
in "head position" until a constructor is exposed. For example, `List.map f [a, b, c]`

weak head normalizes to `f a :: List.map f [b, c]`

.

## Equations

- Lean.Parser.Tactic.Conv.whnf = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.whnf 1024 (Lean.ParserDescr.nonReservedSymbol "whnf" false)

## Instances For

Expands let-declarations and let-variables.

## Equations

- Lean.Parser.Tactic.Conv.zeta = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.zeta 1024 (Lean.ParserDescr.nonReservedSymbol "zeta" false)

## Instances For

Puts term in normal form, this tactic is meant for debugging purposes only.

## Equations

- Lean.Parser.Tactic.Conv.reduce = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.reduce 1024 (Lean.ParserDescr.nonReservedSymbol "reduce" false)

## Instances For

Performs one step of "congruence", which takes a term and produces
subgoals for all the function arguments. For example, if the target is `f x y`

then
`congr`

produces two subgoals, one for `x`

and one for `y`

.

## Equations

- Lean.Parser.Tactic.Conv.congr = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.congr 1024 (Lean.ParserDescr.nonReservedSymbol "congr" false)

## Instances For

`arg i`

traverses into the`i`

'th argument of the target. For example if the target is`f a b c d`

then`arg 1`

traverses to`a`

and`arg 3`

traverses to`c`

.`arg @i`

is the same as`arg i`

but it counts all arguments instead of just the explicit arguments.`arg 0`

traverses into the function. If the target is`f a b c d`

,`arg 0`

traverses into`f`

.

## Equations

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

## Instances For

`change t'`

replaces the target `t`

with `t'`

,
assuming `t`

and `t'`

are definitionally equal.

## Equations

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

## Instances For

`delta id1 id2 ...`

unfolds all occurrences of `id1`

, `id2`

, ... in the target.
Like the `delta`

tactic, this ignores any definitional equations and uses
primitive delta-reduction instead, which may result in leaking implementation details.
Users should prefer `unfold`

for unfolding definitions.

## Equations

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

## Instances For

`unfold id`

unfolds all occurrences of definition`id`

in the target.`unfold id1 id2 ...`

is equivalent to`unfold id1; unfold id2; ...`

.

Definitions can be either global or local definitions.

For non-recursive global definitions, this tactic is identical to `delta`

.
For recursive global definitions, it uses the "unfolding lemma" `id.eq_def`

,
which is generated for each recursive definition, to unfold according to the recursive definition given by the user.
Only one level of unfolding is performed, in contrast to `simp only [id]`

, which unfolds definition `id`

recursively.

This is the `conv`

version of the `unfold`

tactic.

## Equations

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

## Instances For

`pattern pat`

traverses to the first subterm of the target that matches`pat`

.`pattern (occs := *) pat`

traverses to every subterm of the target that matches`pat`

which is not contained in another match of`pat`

. It generates one subgoal for each matching subterm.`pattern (occs := 1 2 4) pat`

matches occurrences`1, 2, 4`

of`pat`

and produces three subgoals. Occurrences are numbered left to right from the outside in.

Note that skipping an occurrence of `pat`

will traverse inside that subexpression, which means
it may find more matches and this can affect the numbering of subsequent pattern matches.
For example, if we are searching for `f _`

in `f (f a) = f b`

:

`occs := 1 2`

(and`occs := *`

) returns`| f (f a)`

and`| f b`

`occs := 2`

returns`| f a`

`occs := 2 3`

returns`| f a`

and`| f b`

`occs := 1 3`

is an error, because after skipping`f b`

there is no third match.

## Equations

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

## Instances For

`rw [thm]`

rewrites the target using `thm`

. See the `rw`

tactic for more information.

## Equations

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

## Instances For

`dsimp`

is the definitional simplifier in `conv`

-mode. It differs from `simp`

in that it only
applies theorems that hold by reflexivity.

Examples:

```
example (a : Nat): (0 + 0) = a - a := by
conv =>
lhs
dsimp
rw [← Nat.sub_self a]
```

## Equations

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

## Instances For

`simp_match`

simplifies match expressions. For example,

```
match [a, b] with
| [] => 0
| hd :: tl => hd
```

simplifies to `a`

.

## Equations

- Lean.Parser.Tactic.Conv.simpMatch = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.simpMatch 1024 (Lean.ParserDescr.nonReservedSymbol "simp_match" false)

## Instances For

Executes the given tactic block without converting `conv`

goal into a regular goal.

## Equations

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

## Instances For

Executes the given conv block without converting regular goal into a `conv`

goal.

## Equations

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

## Instances For

`{ convs }`

runs the list of `convs`

on the current target, and any subgoals that
remain are trivially closed by `skip`

.

## Equations

- Lean.Parser.Tactic.Conv.nestedConv = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.nestedConv 1022 Lean.Parser.Tactic.Conv.convSeqBracketed

## Instances For

`(convs)`

runs the `convs`

in sequence on the current list of targets.
This is pure grouping with no added effects.

## Equations

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

## Instances For

`rfl`

closes one conv goal "trivially", by using reflexivity
(that is, no rewriting).

## Equations

- Lean.Parser.Tactic.Conv.convRfl = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convRfl 1024 (Lean.ParserDescr.nonReservedSymbol "rfl" false)

## Instances For

`done`

succeeds iff there are no goals remaining.

## Equations

- Lean.Parser.Tactic.Conv.convDone = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convDone 1024 (Lean.ParserDescr.nonReservedSymbol "done" false)

## Instances For

`trace_state`

prints the current goal state.

## Equations

- Lean.Parser.Tactic.Conv.convTrace_state = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convTrace_state 1024 (Lean.ParserDescr.nonReservedSymbol "trace_state" false)

## Instances For

`all_goals tac`

runs `tac`

on each goal, concatenating the resulting goals, if any.

## Equations

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

## Instances For

`any_goals tac`

applies the tactic `tac`

to every goal, and succeeds if at
least one application succeeds.

## Equations

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

## Instances For

`case tag => tac`

focuses on the goal with case name`tag`

and solves it using`tac`

, or else fails.`case tag x₁ ... xₙ => tac`

additionally renames the`n`

most recent hypotheses with inaccessible names to the given names.`case tag₁ | tag₂ => tac`

is equivalent to`(case tag₁ => tac); (case tag₂ => tac)`

.

## Equations

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

## Instances For

`case'`

is similar to the `case tag => tac`

tactic, but does not ensure the goal
has been solved after applying `tac`

, nor admits the goal if `tac`

failed.
Recall that `case`

closes the goal using `sorry`

when `tac`

fails, and
the tactic execution is not interrupted.

## Equations

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

## Instances For

`next => tac`

focuses on the next goal and solves it using `tac`

, or else fails.
`next x₁ ... xₙ => tac`

additionally renames the `n`

most recent hypotheses with
inaccessible names to the given names.

## Equations

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

## Instances For

`focus tac`

focuses on the main goal, suppressing all other goals, and runs `tac`

on it.
Usually `· tac`

, which enforces that the goal is closed by `tac`

, should be preferred.

## Equations

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

## Instances For

`conv => cs`

runs `cs`

in sequence on the target `t`

,
resulting in `t'`

, which becomes the new target subgoal.

## Equations

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

## Instances For

`· conv`

focuses on the main conv goal and tries to solve it using `s`

.

## Equations

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

## Instances For

`fail_if_success t`

fails if the tactic `t`

succeeds.

## Equations

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

## Instances For

`rw [rules]`

applies the given list of rewrite rules to the target.
See the `rw`

tactic for more information.

## Equations

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

## Instances For

`erw [rules]`

is a shorthand for `rw (config := { transparency := .default }) [rules]`

.
This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`

which only unfolds `@[reducible]`

definitions).

## Equations

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

## Instances For

`args`

traverses into all arguments. Synonym for `congr`

.

## Equations

- Lean.Parser.Tactic.Conv.convArgs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convArgs 1024 (Lean.ParserDescr.nonReservedSymbol "args" false)

## Instances For

`left`

traverses into the left argument. Synonym for `lhs`

.

## Equations

- Lean.Parser.Tactic.Conv.convLeft = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convLeft 1024 (Lean.ParserDescr.nonReservedSymbol "left" false)

## Instances For

`right`

traverses into the right argument. Synonym for `rhs`

.

## Equations

- Lean.Parser.Tactic.Conv.convRight = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convRight 1024 (Lean.ParserDescr.nonReservedSymbol "right" false)

## Instances For

`intro`

traverses into binders. Synonym for `ext`

.

## Equations

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

## Instances For

## Equations

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

## Instances For

`enter [arg, ...]`

is a compact way to describe a path to a subterm.
It is a shorthand for other conv tactics as follows:

`enter [i]`

is equivalent to`arg i`

.`enter [@i]`

is equivalent to`arg @i`

.`enter [x]`

(where`x`

is an identifier) is equivalent to`ext x`

. For example, given the target`f (g a (fun x => x b))`

,`enter [1, 2, x, 1]`

will traverse to the subterm`b`

.

## Equations

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

## Instances For

The `apply thm`

conv tactic is the same as `apply thm`

the tactic.
There are no restrictions on `thm`

, but strange results may occur if `thm`

cannot be reasonably interpreted as proving one equality from a list of others.

## Equations

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

## Instances For

`try tac`

runs `tac`

and succeeds even if `tac`

failed.

## Equations

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

## Instances For

## Equations

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

## Instances For

`repeat convs`

runs the sequence `convs`

repeatedly until it fails to apply.

## Equations

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

## Instances For

`conv => ...`

allows the user to perform targeted rewriting on a goal or hypothesis,
by focusing on particular subexpressions.

See https://lean-lang.org/theorem_proving_in_lean4/conv.html for more details.

Basic forms:

`conv => cs`

will rewrite the goal with conv tactics`cs`

.`conv at h => cs`

will rewrite hypothesis`h`

.`conv in pat => cs`

will rewrite the first subexpression matching`pat`

(see`pattern`

).

## Equations

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

## Instances For

`norm_cast`

tactic in `conv`

mode.

## Equations

- Lean.Parser.Tactic.Conv.normCast = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.normCast 1024 (Lean.ParserDescr.nonReservedSymbol "norm_cast" false)