# Basic tactics and utilities for tactic writing #

This file defines some basic utilities for tactic writing, and also

- the
`introv`

tactic, which allows the user to automatically introduce the variables of a theorem and explicitly name the non-dependent hypotheses, - an
`assumption`

macro, calling the`assumption`

tactic on all goals - the tactics
`match_target`

,`clear_aux_decl`

(clearing all auxiliary declarations from the context) and`clear_value`

(which clears the bodies of given local definitions, changing them into regular hypotheses).

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

Given two arrays of `FVarId`

s, one from an old local context and the other from a new local
context, pushes `FVarAliasInfo`

s into the info tree for corresponding pairs of `FVarId`

s.
Recall that variables linked this way should be considered to be semantically identical.

The effect of this is, for example, the unused variable linter will see that variables from the first array are used if corresponding variables in the second array are used.

## Equations

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

## Instances For

The tactic `introv`

allows the user to automatically introduce the variables of a theorem and
explicitly name the non-dependent hypotheses.
Any dependent hypotheses are assigned their default names.

Examples:

```
example : ∀ a b : Nat, a = b → b = a := by
introv h,
exact h.symm
```

The state after `introv h`

is

```
a b : ℕ,
h : a = b
⊢ b = a
```

```
example : ∀ a b : Nat, a = b → ∀ c, b = c → a = c := by
introv h₁ h₂,
exact h₁.trans h₂
```

The state after `introv h₁ h₂`

is

```
a b : ℕ,
h₁ : a = b,
c : ℕ,
h₂ : b = c
⊢ a = c
```

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

- Mathlib.Tactic.evalIntrov.intro1PStep = Lean.Elab.Tactic.liftMetaTactic fun (goal : Lean.MVarId) => do let __discr ← goal.intro1P match __discr with | (fst, goal) => pure [goal]

## Instances For

Try calling `assumption`

on all goals; succeeds if it closes at least one goal.

## Equations

- Mathlib.Tactic.tacticAssumption' = Lean.ParserDescr.node `Mathlib.Tactic.tacticAssumption' 1024 (Lean.ParserDescr.nonReservedSymbol "assumption'" false)

## Instances For

## Equations

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

## Instances For

This tactic clears all auxiliary declarations from the context.

## Equations

- Mathlib.Tactic.clearAuxDecl = Lean.ParserDescr.node `Mathlib.Tactic.clearAuxDecl 1024 (Lean.ParserDescr.nonReservedSymbol "clear_aux_decl" false)

## Instances For

Clears the value of the local definition `fvarId`

. Ensures that the resulting goal state
is still type correct. Throws an error if it is a local hypothesis without a value.

## Equations

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

## Instances For

`clear_value n₁ n₂ ...`

clears the bodies of the local definitions `n₁, n₂ ...`

, changing them
into regular hypotheses. A hypothesis `n : α := t`

is changed to `n : α`

.

The order of `n₁ n₂ ...`

does not matter, and values will be cleared in reverse order of
where they appear in the context.

## Equations

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