# The `lift_lets`

tactic #

This module defines a tactic `lift_lets`

that can be used to pull `let`

bindings as far out
of an expression as possible.

Configuration for `Lean.Expr.liftLets`

and the `lift_lets`

tactic.

- proofs : Bool
Whether to lift lets out of proofs. The default is not to.

- merge : Bool
Whether to merge let bindings if they have the same type and value. This test is by syntactic equality, not definitional equality. The default is to merge.

## Instances For

Take all the `let`

s in an expression and move them outwards as far as possible.
All top-level `let`

s are added to the local context, and then `f`

is called with the list
of local bindings (each an fvar) and the new expression.

Let bindings are merged if they have the same type and value.

Use `e.liftLets mkLetFVars`

to get a defeq expression with all `let`

s lifted as far as possible.

## Equations

- e.liftLets f config = Lean.Expr.liftLetsAux config e #[] f

## Instances For

## Equations

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

## Instances For

Lift all the `let`

bindings in the type of an expression as far out as possible.

When applied to the main goal, this gives one the ability to `intro`

embedded `let`

expressions.
For example,

```
example : (let x := 1; x) = 1 := by
lift_lets
-- ⊢ let x := 1; x = 1
intro x
sorry
```

During the lifting process, let bindings are merged if they have the same type and value.

## Equations

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