## Equations

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

## Equations

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

`lemma`

means the same as `theorem`

. It is used to denote "less important" theorems

## Equations

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

Implementation of the `lemma`

command, by macro expansion to `theorem`

.

## Equations

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

`by_cases p`

makes a case distinction on `p`

,
resulting in two subgoals `h : p ⊢⊢`

and `h : ¬ p ⊢¬ p ⊢⊢`

.

## Equations

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

## Equations

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

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
∀ a b : Nat, a = b → b = a := by
introv h,
exact h.symm
→ b = a := by
introv h,
exact h.symm
```

The state after `introv h`

is

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

```
example : ∀ a b : Nat, a = b → ∀ c, b = c → a = c := by
introv h₁ h₂,
exact h₁.trans h₂
∀ a b : Nat, a = b → ∀ c, b = c → a = c := by
introv h₁ h₂,
exact h₁.trans h₂
→ ∀ c, b = c → a = c := by
introv h₁ h₂,
exact h₁.trans h₂
∀ c, b = c → a = c := by
introv h₁ h₂,
exact h₁.trans h₂
→ 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
⊢ a = c
```

## Equations

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

## Equations

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

## Equations

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

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)

## Equations

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

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)

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.

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