# Tactics that transform types into definitionally equal types #

This module defines a standard wrapper that can be used to create tactics that change hypotheses and the goal to things that are definitionally equal.

It then provides a number of tactics that transform local hypotheses and/or the target.

This is `Lean.MVarId.changeLocalDecl`

but makes sure to preserve local variable order.

## Equations

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

## Instances For

For the main goal, use `m`

to transform the types of locations specified by `loc?`

.
If `loc?`

is none, then transforms the type of target. `m`

is provided with an expression
with instantiated metavariables as well as, if the location is a local hypothesis, the fvar.

`m`

*must* transform expressions to defeq expressions.
If `checkDefEq = true`

(the default) then `runDefEqTactic`

will throw an error
if the resulting expression is not definitionally equal to the original expression.

## Equations

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

## Instances For

Like `Mathlib.Tactic.runDefEqTactic`

but for `conv`

mode.

## Equations

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

## Instances For

`whnf`

#

`whnf at loc`

puts the given location into weak-head normal form.
This also exists as a `conv`

-mode tactic.

Weak-head normal form is when the outer-most expression has been fully reduced, the expression may contain subexpressions which have not been reduced.

## Equations

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

## Instances For

`beta_reduce`

#

`beta_reduce at loc`

completely beta reduces the given location.
This also exists as a `conv`

-mode tactic.

This means that whenever there is an applied lambda expression such as
`(fun x => f x) y`

then the argument is substituted into the lambda expression
yielding an expression such as `f y`

.

## Equations

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

## Instances For

`beta_reduce at loc`

completely beta reduces the given location.
This also exists as a `conv`

-mode tactic.

This means that whenever there is an applied lambda expression such as
`(fun x => f x) y`

then the argument is substituted into the lambda expression
yielding an expression such as `f y`

.

## Equations

- Mathlib.Tactic.convBeta_reduce = Lean.ParserDescr.node `Mathlib.Tactic.convBeta_reduce 1024 (Lean.ParserDescr.nonReservedSymbol "beta_reduce" false)

## Instances For

`reduce`

#

`reduce at loc`

completely reduces the given location.
This also exists as a `conv`

-mode tactic.

This does the same transformation as the `#reduce`

command.

## Equations

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

## Instances For

`unfold_let`

#

Unfold all the fvars from `fvars`

in `e`

that have local definitions (are "let-bound").

## Equations

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

## Instances For

`unfold_let x y z at loc`

unfolds the local definitions `x`

, `y`

, and `z`

at the given
location, which is known as "zeta reduction."
This also exists as a `conv`

-mode tactic.

If no local definitions are given, then all local definitions are unfolded.
This variant also exists as the `conv`

-mode tactic `zeta`

.

This is similar to the `unfold`

tactic, which instead is for unfolding global definitions.

## Equations

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

## Instances For

`unfold_let x y z at loc`

unfolds the local definitions `x`

, `y`

, and `z`

at the given
location, which is known as "zeta reduction."
This also exists as a `conv`

-mode tactic.

If no local definitions are given, then all local definitions are unfolded.
This variant also exists as the `conv`

-mode tactic `zeta`

.

This is similar to the `unfold`

tactic, which instead is for unfolding global definitions.

## Equations

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

## Instances For

`refold_let`

#

For each fvar, looks for its body in `e`

and replaces it with the fvar.

## Equations

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

## Instances For

`refold_let x y z at loc`

looks for the bodies of local definitions `x`

, `y`

, and `z`

at the given
location and replaces them with `x`

, `y`

, or `z`

. This is the inverse of "zeta reduction."
This also exists as a `conv`

-mode tactic.

## Equations

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

## Instances For

`refold_let x y z at loc`

looks for the bodies of local definitions `x`

, `y`

, and `z`

at the given
location and replaces them with `x`

, `y`

, or `z`

. This is the inverse of "zeta reduction."
This also exists as a `conv`

-mode tactic.

## Equations

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

## Instances For

`unfold_projs`

#

Recursively unfold all the projection applications for class instances.

## Equations

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

## Instances For

`unfold_projs at loc`

unfolds projections of class instances at the given location.
This also exists as a `conv`

-mode tactic.

## Equations

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

## Instances For

`unfold_projs at loc`

unfolds projections of class instances at the given location.
This also exists as a `conv`

-mode tactic.

## Equations

- Mathlib.Tactic.convUnfold_projs = Lean.ParserDescr.node `Mathlib.Tactic.convUnfold_projs 1024 (Lean.ParserDescr.nonReservedSymbol "unfold_projs" false)

## Instances For

`eta_reduce`

#

Eta reduce everything

## Equations

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

## Instances For

`eta_reduce at loc`

eta reduces all sub-expressions at the given location.
This also exists as a `conv`

-mode tactic.

For example, `fun x y => f x y`

becomes `f`

after eta reduction.

## Equations

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

## Instances For

`eta_reduce at loc`

eta reduces all sub-expressions at the given location.
This also exists as a `conv`

-mode tactic.

For example, `fun x y => f x y`

becomes `f`

after eta reduction.

## Equations

- Mathlib.Tactic.convEta_reduce = Lean.ParserDescr.node `Mathlib.Tactic.convEta_reduce 1024 (Lean.ParserDescr.nonReservedSymbol "eta_reduce" false)

## Instances For

`eta_expand`

#

Eta expand every sub-expression in the given expression.

As a side-effect, beta reduces any pre-existing instances of eta expanded terms.

`eta_expand at loc`

eta expands all sub-expressions at the given location.
It also beta reduces any applications of eta expanded terms, so it puts it
into an eta-expanded "normal form."
This also exists as a `conv`

-mode tactic.

For example, if `f`

takes two arguments, then `f`

becomes `fun x y => f x y`

and `f x`

becomes `fun y => f x y`

.

This can be useful to turn, for example, a raw `HAdd.hAdd`

into `fun x y => x + y`

.

## Equations

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

## Instances For

`eta_expand at loc`

eta expands all sub-expressions at the given location.
It also beta reduces any applications of eta expanded terms, so it puts it
into an eta-expanded "normal form."
This also exists as a `conv`

-mode tactic.

For example, if `f`

takes two arguments, then `f`

becomes `fun x y => f x y`

and `f x`

becomes `fun y => f x y`

.

This can be useful to turn, for example, a raw `HAdd.hAdd`

into `fun x y => x + y`

.

## Equations

- Mathlib.Tactic.convEta_expand = Lean.ParserDescr.node `Mathlib.Tactic.convEta_expand 1024 (Lean.ParserDescr.nonReservedSymbol "eta_expand" false)

## Instances For

`eta_struct`

#

Given an expression that's either a native projection or a registered projection function, gives (1) the name of the structure type, (2) the index of the projection, and (3) the object being projected.

## Equations

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

## Instances For

Checks if the expression is of the form `S.mk x.1 ... x.n`

with `n`

nonzero
and `S.mk`

a structure constructor and returns `x`

.
Each projection `x.i`

can be either a native projection or from a projection function.

`tryWhnfR`

controls whether to try applying `whnfR`

to arguments when none of them
are obviously projections.

Once an obviously correct projection is found, relies on the structure eta rule in `isDefEq`

.

## Equations

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

## Instances For

Check to see if there's an argument at some index `i`

such that it's the `i`

th projection of a some expression.
Returns the expression.

## Equations

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

## Instances For

Finds all occurrences of expressions of the form `S.mk x.1 ... x.n`

where `S.mk`

is a structure constructor and replaces them by `x`

.

## Equations

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

## Instances For

`eta_struct at loc`

transforms structure constructor applications such as `S.mk x.1 ... x.n`

(pretty printed as, for example, `{a := x.a, b := x.b, ...}`

) into `x`

.
This also exists as a `conv`

-mode tactic.

The transformation is known as eta reduction for structures, and it yields definitionally equal expressions.

For example, given `x : α × β`

, then `(x.1, x.2)`

becomes `x`

after this transformation.

## Equations

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

## Instances For

`eta_struct at loc`

transforms structure constructor applications such as `S.mk x.1 ... x.n`

(pretty printed as, for example, `{a := x.a, b := x.b, ...}`

) into `x`

.
This also exists as a `conv`

-mode tactic.

The transformation is known as eta reduction for structures, and it yields definitionally equal expressions.

For example, given `x : α × β`

, then `(x.1, x.2)`

becomes `x`

after this transformation.

## Equations

- Mathlib.Tactic.convEta_struct = Lean.ParserDescr.node `Mathlib.Tactic.convEta_struct 1024 (Lean.ParserDescr.nonReservedSymbol "eta_struct" false)