# The `extract_lets at`

tactic #

This module defines a tactic `extract_lets ... at h`

that can be used to (in essence) do `cases`

on a `let`

expression.

Given a local hypothesis whose type is a `let`

expression, then lift the `let`

bindings to be
a new local definition.

## Equations

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

## Instances For

Check that `t`

is a `let`

and then do what's necessary to lift it over the binding
described by `mk`

.

## Equations

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

## Instances For

A more limited version of `Lean.MVarId.introN`

that ensures the goal is a
nested `let`

expression.

## Equations

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

## Instances For

The `extract_lets at h`

tactic takes a local hypothesis of the form `h : let x := v; b`

and introduces a new local definition `x := v`

while changing `h`

to be `h : b`

. It can be thought
of as being a `cases`

tactic for `let`

expressions. It can also be thought of as being like
`intros at h`

for `let`

expressions.

For example, if `h : let x := 1; x = x`

, then `extract_lets x at h`

introduces `x : Nat := 1`

and
changes `h`

to `h : x = x`

.

Just like `intros`

, the `extract_lets`

tactic either takes a list of names, in which case
that specifies the number of `let`

bindings that must be extracted, or it takes no names, in which
case all the `let`

bindings are extracted.

The tactic `extract_lets`

(without `at`

) or `extract_lets at h ⊢`

acts as a weaker
form of `intros`

on the goal that only introduces obvious `let`

s.

## Equations

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

## Instances For

The `extract_lets at h`

tactic takes a local hypothesis of the form `h : let x := v; b`

and introduces a new local definition `x := v`

while changing `h`

to be `h : b`

. It can be thought
of as being a `cases`

tactic for `let`

expressions. It can also be thought of as being like
`intros at h`

for `let`

expressions.

For example, if `h : let x := 1; x = x`

, then `extract_lets x at h`

introduces `x : Nat := 1`

and
changes `h`

to `h : x = x`

.

Just like `intros`

, the `extract_lets`

tactic either takes a list of names, in which case
that specifies the number of `let`

bindings that must be extracted, or it takes no names, in which
case all the `let`

bindings are extracted.

The tactic `extract_lets`

(without `at`

) or `extract_lets at h ⊢`

acts as a weaker
form of `intros`

on the goal that only introduces obvious `let`

s.

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