`with_annotate_state stx t`

annotates the lexical range of `stx : Syntax`

with
the initial and final state of running tactic `t`

.

## Equations

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

Introduces one or more hypotheses, optionally naming and/or pattern-matching them.
For each hypothesis to be introduced, the remaining main goal's target type must
be a `let`

or function type.

`intro`

by itself introduces one anonymous hypothesis, which can be accessed by e.g.`assumption`

.`intro x y`

introduces two hypotheses and names them. Individual hypotheses can be anonymized via`_`

, or matched against a pattern:`-- ... ⊢ α × β → ... intro (a, b) -- ..., a : α, b : β ⊢ ... ⊢ α × β → ... intro (a, b) -- ..., a : α, b : β ⊢ ... × β → ... intro (a, b) -- ..., a : α, b : β ⊢ ... → ... intro (a, b) -- ..., a : α, b : β ⊢ ... ⊢ ...`

- Alternatively,
`intro`

can be combined with pattern matching much like`fun`

:`intro | n + 1, 0 => tac | ...`

## Equations

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

`intros x...`

behaves like `intro x...`

, but then keeps introducing (anonymous)
hypotheses until goal is not of a function type.

## Equations

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

`rename t => x`

renames the most recent hypothesis whose type matches `t`

(which may contain placeholders) to `x`

, or fails if no such hypothesis could be found.

## Equations

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

`revert x...`

is the inverse of `intro x...`

: it moves the given hypotheses
into the main goal's target type.

## Equations

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

`clear x...`

removes the given hypotheses, or fails if there are remaining
references to a hypothesis.

## Equations

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

`subst x...`

substitutes each `x`

with `e`

in the goal if there is a hypothesis
of type `x = e`

or `e = x`

.
If `x`

is itself a hypothesis of type `y = e`

or `e = y`

, `y`

is substituted instead.

## Equations

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

Applies `subst`

to all hypotheses of the form `h : x = t`

or `h : t = x`

.

## Equations

- Lean.Parser.Tactic.substVars = Lean.ParserDescr.node `Lean.Parser.Tactic.substVars 1024 (Lean.ParserDescr.nonReservedSymbol "subst_vars" false)

`assumption`

tries to solve the main goal using a hypothesis of compatible type, or else fails.
Note also the `‹t›`

term notation, which is a shorthand for `show t by assumption`

.

## Equations

- Lean.Parser.Tactic.assumption = Lean.ParserDescr.node `Lean.Parser.Tactic.assumption 1024 (Lean.ParserDescr.nonReservedSymbol "assumption" false)

`contradiction`

closes the main goal if its hypotheses are "trivially contradictory".

- Inductive type/family with no applicable constructors

```
example (h : False) : p := by contradiction
```

- Injectivity of constructors

```
example (h : none = some true) : p := by contradiction --
```

- Decidable false proposition

```
example (h : 2 + 2 = 3) : p := by contradiction
```

- Contradictory hypotheses

```
example (h : p) (h' : ¬ p) : q := by contradiction
¬ p) : q := by contradiction
```

- Other simple contradictions such as

```
example (x : Nat) (h : x ≠ x) : p := by contradiction
≠ x) : p := by contradiction
```

## Equations

- Lean.Parser.Tactic.contradiction = Lean.ParserDescr.node `Lean.Parser.Tactic.contradiction 1024 (Lean.ParserDescr.nonReservedSymbol "contradiction" false)

`apply e`

tries to match the current goal against the conclusion of `e`

's type.
If it succeeds, then the tactic returns as many subgoals as the number of premises that
have not been fixed by type inference or type class resolution.
Non-dependent premises are added before dependent ones.

The `apply`

tactic uses higher-order pattern matching, type class resolution,
and first-order unification with dependent types.

## Equations

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

`exact e`

closes the main goal if its target type matches that of `e`

.

## Equations

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

`refine e`

behaves like `exact e`

, except that named (`?x`

) or unnamed (`?_`

)
holes in `e`

that are not solved by unification with the main goal's target type
are converted into new goals, using the hole's name, if any, as the goal case name.

## Equations

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

`refine' e`

behaves like `refine e`

, except that unsolved placeholders (`_`

)
and implicit parameters are also converted into new goals.

## Equations

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

If the main goal's target type is an inductive type, `constructor`

solves it with
the first matching constructor, or else fails.

## Equations

- Lean.Parser.Tactic.constructor = Lean.ParserDescr.node `Lean.Parser.Tactic.constructor 1024 (Lean.ParserDescr.nonReservedSymbol "constructor" false)

`case tag => tac`

focuses on the goal with case name`tag`

and solves it using`tac`

, or else fails.`case tag x₁ ... xₙ => tac`

additionally renames the`n`

most recent hypotheses with inaccessible names to the given names.`case tag₁ | tag₂ => tac`

is equivalent to`(case tag₁ => tac); (case tag₂ => tac)`

.

## Equations

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

`case'`

is similar to the `case tag => tac`

tactic, but does not ensure the goal
has been solved after applying `tac`

, nor admits the goal if `tac`

failed.
Recall that `case`

closes the goal using `sorry`

when `tac`

fails, and
the tactic execution is not interrupted.

## Equations

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

`next => tac`

focuses on the next goal and solves it using `tac`

, or else fails.
`next x₁ ... xₙ => tac`

additionally renames the `n`

most recent hypotheses with
inaccessible names to the given names.

## Equations

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

`all_goals tac`

runs `tac`

on each goal, concatenating the resulting goals, if any.

## Equations

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

`any_goals tac`

applies the tactic `tac`

to every goal, and succeeds if at
least one application succeeds.

## Equations

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

`focus tac`

focuses on the main goal, suppressing all other goals, and runs `tac`

on it.
Usually `· tac`

, which enforces that the goal is closed by `tac`

, should be preferred.

## Equations

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

`skip`

does nothing.

## Equations

- Lean.Parser.Tactic.skip = Lean.ParserDescr.node `Lean.Parser.Tactic.skip 1024 (Lean.ParserDescr.nonReservedSymbol "skip" false)

`done`

succeeds iff there are no remaining goals.

## Equations

- Lean.Parser.Tactic.done = Lean.ParserDescr.node `Lean.Parser.Tactic.done 1024 (Lean.ParserDescr.nonReservedSymbol "done" false)

`trace_state`

displays the current state in the info view.

## Equations

- Lean.Parser.Tactic.traceState = Lean.ParserDescr.node `Lean.Parser.Tactic.traceState 1024 (Lean.ParserDescr.nonReservedSymbol "trace_state" false)

`trace msg`

displays `msg`

in the info view.

## Equations

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

`fail_if_success t`

fails if the tactic `t`

succeeds.

## Equations

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

`(tacs)`

executes a list of tactics in sequence, without requiring that
the goal be closed at the end like `· tacs`

. Like `by`

itself, the tactics
can be either separated by newlines or `;`

.

## Equations

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

`with_reducible tacs`

excutes `tacs`

using the reducible transparency setting.
In this setting only definitions tagged as `[reducible]`

are unfolded.

## Equations

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

`with_reducible_and_instances tacs`

excutes `tacs`

using the `.instances`

transparency setting.
In this setting only definitions tagged as `[reducible]`

or type class instances are unfolded.

## Equations

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

`with_unfolding_all tacs`

excutes `tacs`

using the `.all`

transparency setting.
In this setting all definitions that are not opaque are unfolded.

## Equations

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

`first | tac | ...`

runs each `tac`

until one succeeds, or else fails.

## Equations

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

`rotate_left n`

rotates goals to the left by `n`

. That is, `rotate_left 1`

takes the main goal and puts it to the back of the subgoal list.
If `n`

is omitted, it defaults to `1`

.

## Equations

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

Rotate the goals to the right by `n`

. That is, take the goal at the back
and push it to the front `n`

times. If `n`

is omitted, it defaults to `1`

.

## Equations

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

`try tac`

runs `tac`

and succeeds even if `tac`

failed.

## Equations

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

`tac <;> tac'`

runs `tac`

on the main goal and `tac'`

on each produced goal,
concatenating all goals produced by `tac'`

.

## Equations

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

`eq_refl`

is equivalent to `exact rfl`

, but has a few optimizations.

## Equations

- Lean.Parser.Tactic.refl = Lean.ParserDescr.node `Lean.Parser.Tactic.refl 1024 (Lean.ParserDescr.nonReservedSymbol "eq_refl" false)

`rfl`

tries to close the current goal using reflexivity.
This is supposed to be an extensible tactic and users can add their own support
for new reflexive relations.

## Equations

- Lean.Parser.Tactic.tacticRfl = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticRfl 1024 (Lean.ParserDescr.nonReservedSymbol "rfl" false)

`rfl'`

is similar to `rfl`

, but disables smart unfolding and unfolds all kinds of definitions,
theorems included (relevant for declarations defined by well-founded recursion).

## Equations

- Lean.Parser.Tactic.tacticRfl' = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticRfl' 1024 (Lean.ParserDescr.nonReservedSymbol "rfl'" false)

`ac_rfl`

proves equalities up to application of an associative and commutative operator.

```
instance : IsAssociative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
instance : IsCommutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl
```

## Equations

- Lean.Parser.Tactic.acRfl = Lean.ParserDescr.node `Lean.Parser.Tactic.acRfl 1024 (Lean.ParserDescr.nonReservedSymbol "ac_rfl" false)

The `sorry`

tactic closes the goal using `sorryAx`

. This is intended for stubbing out incomplete
parts of a proof while still having a syntactically correct proof skeleton. Lean will give
a warning whenever a proof uses `sorry`

, so you aren't likely to miss it, but
you can double check if a theorem depends on `sorry`

by using
`#print axioms my_thm`

and looking for `sorryAx`

in the axiom list.

## Equations

- Lean.Parser.Tactic.tacticSorry = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticSorry 1024 (Lean.ParserDescr.nonReservedSymbol "sorry" false)

`admit`

is a shorthand for `exact sorry`

.

## Equations

- Lean.Parser.Tactic.tacticAdmit = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticAdmit 1024 (Lean.ParserDescr.nonReservedSymbol "admit" false)

`infer_instance`

is an abbreviation for `exact inferInstance`

.
It synthesizes a value of any target type by typeclass inference.

## Equations

- Lean.Parser.Tactic.tacticInfer_instance = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticInfer_instance 1024 (Lean.ParserDescr.nonReservedSymbol "infer_instance" false)

Optional configuration option for tactics

## Equations

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

The `*`

location refers to all hypotheses and the goal.

## Equations

- Lean.Parser.Tactic.locationWildcard = Lean.ParserDescr.nodeWithAntiquot "locationWildcard" `Lean.Parser.Tactic.locationWildcard (Lean.ParserDescr.symbol "*")

A hypothesis location specification consists of 1 or more hypothesis references
and optionally `⊢⊢`

denoting the goal.

## Equations

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

Location specifications are used by many tactics that can operate on either the hypotheses or the goal. It can have one of the forms:

- 'empty' is not actually present in this syntax, but most tactics use
`(location)?`

matchers. It means to target the goal only. `at h₁ ... hₙ`

: target the hypotheses`h₁`

, ...,`hₙ`

`at h₁ h₂ ⊢⊢`

: target the hypotheses`h₁`

and`h₂`

, and the goal`at *`

: target all hypotheses and the goal

## Equations

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

`change tgt'`

will change the goal from`tgt`

to`tgt'`

, assuming these are definitionally equal.`change t' at h`

will change hypothesis`h : t`

to have type`t'`

, assuming assuming`t`

and`t'`

are definitionally equal.

## Equations

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

`change a with b`

will change occurrences of`a`

to`b`

in the goal, assuming`a`

and`b`

are are definitionally equal.`change a with b at h`

similarly changes`a`

to`b`

in the type of hypothesis`h`

.

## Equations

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

If `thm`

is a theorem `a = b`

, then as a rewrite rule,

`thm`

means to replace`a`

with`b`

, and`← thm← thm`

means to replace`b`

with`a`

.

## Equations

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

`rewrite [e]`

applies identity `e`

as a rewrite rule to the target of the main goal.
If `e`

is preceded by left arrow (`←←`

or `<-`

), the rewrite is applied in the reverse direction.
If `e`

is a defined constant, then the equational theorems associated with `e`

are used.
This provides a convenient way to unfold `e`

.

`rewrite [e₁, ..., eₙ]`

applies the given rules sequentially.`rewrite [e] at l`

rewrites`e`

at location(s)`l`

, where`l`

is either`*`

or a list of hypotheses in the local context. In the latter case, a turnstile`⊢⊢`

or`|-`

can also be used, to signify the target of the goal.

## Equations

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

`rw`

is like `rewrite`

, but also tries to close the goal by "cheap" (reducible) `rfl`

afterwards.

## Equations

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

The `injection`

tactic is based on the fact that constructors of inductive data
types are injections.
That means that if `c`

is a constructor of an inductive datatype, and if `(c t₁)`

and `(c t₂)`

are two terms that are equal then `t₁`

and `t₂`

are equal too.
If `q`

is a proof of a statement of conclusion `t₁ = t₂`

, then injection applies
injectivity to derive the equality of all arguments of `t₁`

and `t₂`

placed in
the same positions. For example, from `(a::b) = (c::d)`

we derive `a=c`

and `b=d`

.
To use this tactic `t₁`

and `t₂`

should be constructor applications of the same constructor.
Given `h : a::b = c::d`

, the tactic `injection h`

adds two new hypothesis with types
`a = c`

and `b = d`

to the main goal.
The tactic `injection h with h₁ h₂`

uses the names `h₁`

and `h₂`

to name the new hypotheses.

## Equations

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

`injections`

applies `injection`

to all hypotheses recursively
(since `injection`

can produce new hypotheses). Useful for destructing nested
constructor equalities like `(a::b::c) = (d::e::f)`

.

## Equations

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

The discharger clause of `simp`

and related tactics.
This is a tactic used to discharge the side conditions on conditional rewrite rules.

## Equations

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

Use this rewrite rule before entering the subterms

## Equations

- Lean.Parser.Tactic.simpPre = Lean.ParserDescr.nodeWithAntiquot "simpPre" `Lean.Parser.Tactic.simpPre (Lean.ParserDescr.symbol "↓")

Use this rewrite rule after entering the subterms

## Equations

- Lean.Parser.Tactic.simpPost = Lean.ParserDescr.nodeWithAntiquot "simpPost" `Lean.Parser.Tactic.simpPost (Lean.ParserDescr.symbol "↑")

A simp lemma specification is:

- optional
`↑↑`

or`↓↓`

to specify use before or after entering the subterm - optional
`←←`

to use the lemma backward `thm`

for the theorem to rewrite with

## Equations

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

An erasure specification `-thm`

says to remove `thm`

from the simp set

## Equations

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

The simp lemma specification `*`

means to rewrite with all hypotheses

## Equations

- Lean.Parser.Tactic.simpStar = Lean.ParserDescr.nodeWithAntiquot "simpStar" `Lean.Parser.Tactic.simpStar (Lean.ParserDescr.symbol "*")

The `simp`

tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:

`simp`

simplifies the main goal target using lemmas tagged with the attribute`[simp]`

.`simp [h₁, h₂, ..., hₙ]`

simplifies the main goal target using the lemmas tagged with the attribute`[simp]`

and the given`hᵢ`

's, where the`hᵢ`

's are expressions. If an`hᵢ`

is a defined constant`f`

, then the equational lemmas associated with`f`

are used. This provides a convenient way to unfold`f`

.`simp [*]`

simplifies the main goal target using the lemmas tagged with the attribute`[simp]`

and all hypotheses.`simp only [h₁, h₂, ..., hₙ]`

is like`simp [h₁, h₂, ..., hₙ]`

but does not use`[simp]`

lemmas.`simp [-id₁, ..., -idₙ]`

simplifies the main goal target using the lemmas tagged with the attribute`[simp]`

, but removes the ones named`idᵢ`

.`simp at h₁ h₂ ... hₙ`

simplifies the hypotheses`h₁ : T₁`

...`hₙ : Tₙ`

. If the target or another hypothesis depends on`hᵢ`

, a new simplified hypothesis`hᵢ`

is introduced, but the old one remains in the local context.`simp at *`

simplifies all the hypotheses and the target.`simp [*] at *`

simplifies target and all (propositional) hypotheses using the other hypotheses.

## Equations

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

`simp_all`

is a stronger version of `simp [*] at *`

where the hypotheses and target
are simplified multiple times until no simplication is applicable.
Only non-dependent propositional hypotheses are considered.

## Equations

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

`delta id1 id2 ...`

delta-expands the definitions `id1`

, `id2`

, ....
This is a low-level tactic, it will expose how recursive definitions have been
compiled by Lean.

## Equations

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

`unfold id`

unfolds definition`id`

.`unfold id1 id2 ...`

is equivalent to`unfold id1; unfold id2; ...`

.

For non-recursive definitions, this tactic is identical to `delta`

.
For definitions by pattern matching, it uses "equation lemmas" which are
autogenerated for each match arm.

## Equations

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

Auxiliary macro for lifting have/suffices/let/...
It makes sure the "continuation" `?_`

is the main goal after refining.

## Equations

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

`have h : t := e`

adds the hypothesis `h : t`

to the current goal if `e`

a term
of type `t`

.

- If
`t`

is omitted, it will be inferred. - If
`h`

is omitted, the name`this`

is used. - The variant
`have pattern := e`

is equivalent to`match e with | pattern => _`

, and it is convenient for types that have only one applicable constructor. For example, given`h : p ∧ q ∧ r∧ q ∧ r∧ r`

,`have ⟨h₁, h₂, h₃⟩ := h`

produces the hypotheses`h₁ : p`

,`h₂ : q`

, and`h₃ : r`

.

## Equations

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

Given a main goal `ctx ⊢ t⊢ t`

, `suffices h : t' from e`

replaces the main goal with `ctx ⊢ t'⊢ t'`

,
`e`

must have type `t`

in the context `ctx, h : t'`

.

The variant `suffices h : t' by tac`

is a shorthand for `suffices h : t' from by tac`

.
If `h :`

is omitted, the name `this`

is used.

## Equations

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

`let h : t := e`

adds the hypothesis `h : t := e`

to the current goal if `e`

a term of type `t`

.
If `t`

is omitted, it will be inferred.
The variant `let pattern := e`

is equivalent to `match e with | pattern => _`

,
and it is convenient for types that have only applicable constructor.
Example: given `h : p ∧ q ∧ r∧ q ∧ r∧ r`

, `let ⟨h₁, h₂, h₃⟩ := h`

produces the hypotheses
`h₁ : p`

, `h₂ : q`

, and `h₃ : r`

.

## Equations

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

`show t`

finds the first goal whose target unifies with `t`

. It makes that the main goal,
performs the unification, and replaces the target with the unified version of `t`

.

## Equations

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

`let rec f : t := e`

adds a recursive definition `f`

to the current goal.
The syntax is the same as term-mode `let rec`

.

## Equations

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

Similar to `refine_lift`

, but using `refine'`

## Equations

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

Similar to `have`

, but using `refine'`

## Equations

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

Similar to `have`

, but using `refine'`

## Equations

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

Similar to `let`

, but using `refine'`

## Equations

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

The left hand side of an induction arm, `| foo a b c`

or `| @foo a b c`

where `foo`

is a constructor of the inductive type and `a b c`

are the arguments
to the contstructor.

## Equations

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

In induction alternative, which can have 1 or more cases on the left
and `_`

, `?_`

, or a tactic sequence after the `=>`

.

## Equations

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

After `with`

, there is an optional tactic that runs on all branches, and
then a list of alternatives.

## Equations

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

Assuming `x`

is a variable in the local context with an inductive type,
`induction x`

applies induction on `x`

to the main goal,
producing one goal for each constructor of the inductive type,
in which the target is replaced by a general instance of that constructor
and an inductive hypothesis is added for each recursive argument to the constructor.
If the type of an element in the local context depends on `x`

,
that element is reverted and reintroduced afterward,
so that the inductive hypothesis incorporates that hypothesis as well.

For example, given `n : Nat`

and a goal with a hypothesis `h : P n`

and target `Q n`

,
`induction n`

produces one goal with hypothesis `h : P 0`

and target `Q 0`

,
and one goal with hypotheses `h : P (Nat.succ a)`

and `ih₁ : P a → Q a→ Q a`

and target `Q (Nat.succ a)`

.
Here the names `a`

and `ih₁`

are chosen automatically and are not accessible.
You can use `with`

to provide the variables names for each constructor.

`induction e`

, where`e`

is an expression instead of a variable, generalizes`e`

in the goal, and then performs induction on the resulting variable.`induction e using r`

allows the user to specify the principle of induction that should be used. Here`r`

should be a theorem whose result type must be of the form`C t`

, where`C`

is a bound variable and`t`

is a (possibly empty) sequence of bound variables`induction e generalizing z₁ ... zₙ`

, where`z₁ ... zₙ`

are variables in the local context, generalizes over`z₁ ... zₙ`

before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized.- Given
`x : Nat`

,`induction x with | zero => tac₁ | succ x' ih => tac₂`

uses tactic`tac₁`

for the`zero`

case, and`tac₂`

for the`succ`

case.

## Equations

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

A `generalize`

argument, of the form `term = x`

or `h : term = x`

.

## Equations

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

`generalize ([h :] e = x),+`

replaces all occurrences`e`

s in the main goal with a fresh hypothesis`x`

s. If`h`

is given,`h : e = x`

is introduced as well.`generalize e = x at h₁ ... hₙ`

also generalizes occurrences of`e`

inside`h₁`

, ...,`hₙ`

.`generalize e = x at *`

will generalize occurrences of`e`

everywhere.

## Equations

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

A `cases`

argument, of the form `e`

or `h : e`

(where `h`

asserts that
`e = cᵢ a b`

for each constructor `cᵢ`

of the inductive).

## Equations

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

Assuming `x`

is a variable in the local context with an inductive type,
`cases x`

splits the main goal, producing one goal for each constructor of the
inductive type, in which the target is replaced by a general instance of that constructor.
If the type of an element in the local context depends on `x`

,
that element is reverted and reintroduced afterward,
so that the case split affects that hypothesis as well.
`cases`

detects unreachable cases and closes them automatically.

For example, given `n : Nat`

and a goal with a hypothesis `h : P n`

and target `Q n`

,
`cases n`

produces one goal with hypothesis `h : P 0`

and target `Q 0`

,
and one goal with hypothesis `h : P (Nat.succ a)`

and target `Q (Nat.succ a)`

.
Here the name `a`

is chosen automatically and is not accessible.
You can use `with`

to provide the variables names for each constructor.

`cases e`

, where`e`

is an expression instead of a variable, generalizes`e`

in the goal, and then cases on the resulting variable.- Given
`as : List α`

,`cases as with | nil => tac₁ | cons a as' => tac₂`

, uses tactic`tac₁`

for the`nil`

case, and`tac₂`

for the`cons`

case, and`a`

and`as'`

are used as names for the new variables introduced. `cases h : e`

, where`e`

is a variable or an expression, performs cases on`e`

as above, but also adds a hypothesis`h : e = ...`

to each hypothesis, where`...`

is the constructor instance for that particular case.

## Equations

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

`rename_i x_1 ... x_n`

renames the last `n`

inaccessible names using the given names.

## Equations

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

`repeat tac`

applies `tac`

to main goal. If the application succeeds,
the tactic is applied recursively to the generated subgoals until it eventually fails.

## Equations

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

`trivial`

tries different simple tactics (e.g., `rfl`

, `contradiction`

, ...)
to close the current goal.
You can use the command `macro_rules`

to extend the set of tactics used. Example:

```
macro_rules | `(tactic| trivial) => `(tactic| simp)
```

## Equations

- Lean.Parser.Tactic.tacticTrivial = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticTrivial 1024 (Lean.ParserDescr.nonReservedSymbol "trivial" false)

The `split`

tactic is useful for breaking nested if-then-else and `match`

expressions into separate cases.
For a `match`

expression with `n`

cases, the `split`

tactic generates at most `n`

subgoals.

For example, given `n : Nat`

, and a target `if n = 0 then Q else R`

, `split`

will generate
one goal with hypothesis `n = 0`

and target `Q`

, and a second goal with hypothesis
`¬n = 0¬n = 0`

and target `R`

. Note that the introduced hypothesis is unnamed, and is commonly
renamed used the `case`

or `next`

tactics.

`split`

will split the goal (target).`split at h`

will split the hypothesis`h`

.

## Equations

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

`dbg_trace "foo"`

prints `foo`

when elaborated.
Useful for debugging tactic control flow:

```
example : False ∨ True := by
first
| apply Or.inl; trivial; dbg_trace "left"
| apply Or.inr; trivial; dbg_trace "right"
∨ True := by
first
| apply Or.inl; trivial; dbg_trace "left"
| apply Or.inr; trivial; dbg_trace "right"
```

## Equations

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

`stop`

is a helper tactic for "discarding" the rest of a proof:
it is defined as `repeat sorry`

.
It is useful when working on the middle of a complex proofs,
and less messy than commenting the remainder of the proof.

## Equations

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

The tactic `specialize h a₁ ... aₙ`

works on local hypothesis `h`

.
The premises of this hypothesis, either universal quantifications or
non-dependent implications, are instantiated by concrete terms coming
from arguments `a₁`

... `aₙ`

.
The tactic adds a new hypothesis with the same name `h := h a₁ ... aₙ`

and tries to clear the previous one.

## Equations

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

`unhygienic tacs`

runs `tacs`

with name hygiene disabled.
This means that tactics that would normally create inaccessible names will instead
make regular variables. **Warning**: Tactics may change their variable naming
strategies at any time, so code that depends on autogenerated names is brittle.
Users should try not to use `unhygienic`

if possible.

```
example : ∀ x : Nat, x = x := by unhygienic
intro -- x would normally be intro'd as inaccessible
exact Eq.refl x -- refer to x
∀ x : Nat, x = x := by unhygienic
intro -- x would normally be intro'd as inaccessible
exact Eq.refl x -- refer to x
```

## Equations

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

`fail msg`

is a tactic that always fails, and produces an error using the given message.

## Equations

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

`checkpoint tac`

acts the same as `tac`

, but it caches the input and output of `tac`

,
and if the file is re-elaborated and the input matches, the tactic is not re-run and
its effects are reapplied to the state. This is useful for improving responsiveness
when working on a long tactic proof, by wrapping expensive tactics with `checkpoint`

.

See the `save`

tactic, which may be more convenient to use.

(TODO: do this automatically and transparently so that users don't have to use this combinator explicitly.)

## Equations

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

`save`

is defined to be the same as `skip`

, but the elaborator has
special handling for occurrences of `save`

in tactic scripts and will transform
`by tac1; save; tac2`

to `by (checkpoint tac1); tac2`

, meaning that the effect of `tac1`

will be cached and replayed. This is useful for improving responsiveness
when working on a long tactic proof, by using `save`

after expensive tactics.

(TODO: do this automatically and transparently so that users don't have to use this combinator explicitly.)

## Equations

- Lean.Parser.Tactic.save = Lean.ParserDescr.node `Lean.Parser.Tactic.save 1024 (Lean.ParserDescr.nonReservedSymbol "save" false)

The tactic `sleep ms`

sleeps for `ms`

milliseconds and does nothing.
It is used for debugging purposes only.

## Equations

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

`exists e₁, e₂, ...`

is shorthand for `refine ⟨e₁, e₂, ...⟩; try trivial`

.
It is useful for existential goals.

## Equations

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

Apply congruence (recursively) to goals of the form `⊢ f as = f bs⊢ f as = f bs`

and `⊢ HEq (f as) (f bs)⊢ HEq (f as) (f bs)`

.
The optional parameter is the depth of the recursive applications.
This is useful when `congr`

is too aggressive in breaking down the goal.
For example, given `⊢ f (g (x + y)) = f (g (y + x))⊢ f (g (x + y)) = f (g (y + x))`

,
`congr`

produces the goals `⊢ x = y⊢ x = y`

and `⊢ y = x⊢ y = x`

,
while `congr 2`

produces the intended `⊢ x + y = y + x⊢ x + y = y + x`

.

## Equations

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

Theorems tagged with the `simp`

attribute are by the simplifier
(i.e., the `simp`

tactic, and its variants) to simplify expressions occurring in your goals.
We call theorems tagged with the `simp`

attribute "simp theorems" or "simp lemmas".
Lean maintains a database/index containing all active simp theorems.
Here is an example of a simp theorem.

```
@[simp] theorem ne_eq (a b : α) : (a ≠ b) = Not (a = b) := rfl
≠ b) = Not (a = b) := rfl
```

This simp theorem instructs the simplifier to replace instances of the term
`a ≠ b≠ b`

(e.g. `x + 0 ≠ y≠ y`

) with `Not (a = b)`

(e.g., `Not (x + 0 = y)`

).
The simplifier applies simp theorems in one direction only:
if `A = B`

is a simp theorem, then `simp`

replaces `A`

s with `B`

s,
but it doesn't replace `B`

s with `A`

s. Hence a simp theorem should have the
property that its right-hand side is "simpler" than its left-hand side.
In particular, `=`

and `↔↔`

should not be viewed as symmetric operators in this situation.
The following would be a terrible simp theorem (if it were even allowed):

```
@[simp] lemma mul_right_inv_bad (a : G) : 1 = a * a⁻¹ := ...
⁻¹ := ...
```

Replacing 1 with a * a⁻¹ is not a sensible default direction to travel. Even worse would be a theorem that causes expressions to grow without bound, causing simp to loop forever.

By default the simplifier applies `simp`

theorems to an expression `e`

after its sub-expressions have been simplified.
We say it performs a bottom-up simplification.
You can instruct the simplifier to apply a theorem before its sub-expressions
have been simplified by using the modifier `↓↓`

. Here is an example

```
@[simp↓] theorem not_and_eq (p q : Prop) : (¬ (p ∧ q)) = (¬p ∨ ¬q) :=
↓] theorem not_and_eq (p q : Prop) : (¬ (p ∧ q)) = (¬p ∨ ¬q) :=
¬ (p ∧ q)) = (¬p ∨ ¬q) :=
∧ q)) = (¬p ∨ ¬q) :=
¬p ∨ ¬q) :=
∨ ¬q) :=
¬q) :=
```

When multiple simp theorems are applicable, the simplifier uses the one with highest priority. If there are several with the same priority, it is uses the "most recent one". Example:

```
@[simp high] theorem cond_true (a b : α) : cond true a b = a := rfl
@[simp low+1] theorem or_true (p : Prop) : (p ∨ True) = True :=
propext <| Iff.intro (fun _ => trivial) (fun _ => Or.inr trivial)
@[simp 100] theorem ite_self {d : Decidable c} (a : α) : ite c a a = a := by
cases d <;> rfl
∨ True) = True :=
propext <| Iff.intro (fun _ => trivial) (fun _ => Or.inr trivial)
@[simp 100] theorem ite_self {d : Decidable c} (a : α) : ite c a a = a := by
cases d <;> rfl
```

## Equations

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

`‹t›`

resolves to an (arbitrary) hypothesis of type `t`

.
It is useful for referring to hypotheses without accessible names.
`t`

may contain holes that are solved by unification with the expected type;
in particular, `‹_›`

is a shortcut for `by assumption`

.

## Equations

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

`get_elem_tactic_trivial`

is an extensible tactic automatically called
by the notation `arr[i]`

to prove any side conditions that arise when
constructing the term (e.g. the index is in bounds of the array).
The default behavior is to just try `trivial`

(which handles the case
where `i < arr.size`

is in the context) and `simp_arith`

(for doing linear arithmetic in the index).

## Equations

- tacticGet_elem_tactic_trivial = Lean.ParserDescr.node `tacticGet_elem_tactic_trivial 1024 (Lean.ParserDescr.nonReservedSymbol "get_elem_tactic_trivial" false)

`get_elem_tactic`

is the tactic automatically called by the notation `arr[i]`

to prove any side conditions that arise when constructing the term
(e.g. the index is in bounds of the array). It just delegates to
`get_elem_tactic_trivial`

and gives a diagnostic error message otherwise;
users are encouraged to extend `get_elem_tactic_trivial`

instead of this tactic.

## Equations

- tacticGet_elem_tactic = Lean.ParserDescr.node `tacticGet_elem_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "get_elem_tactic" false)

The syntax `arr[i]`

gets the `i`

'th element of the collection `arr`

.
If there are proof side conditions to the application, they will be automatically
inferred by the `get_elem_tactic`

tactic.

The actual behavior of this class is type-dependent, but here are some important implementations:

`arr[i] : α`

where`arr : Array α`

and`i : Nat`

or`i : USize`

: does array indexing with no bounds check and a proof side goal`i < arr.size`

.`l[i] : α`

where`l : List α`

and`i : Nat`

: index into a list, with proof side goal`i < l.length`

.`stx[i] : Syntax`

where`stx : Syntax`

and`i : Nat`

: get a syntax argument, no side goal (returns`.missing`

out of range)

There are other variations on this syntax:

`arr[i]`

: proves the proof side goal by`get_elem_tactic`

`arr[i]!`

: panics if the side goal is false`arr[i]?`

: returns`none`

if the side goal is false`arr[i]'h`

: uses`h`

to prove the side goal

## Equations

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

The syntax `arr[i]`

gets the `i`

'th element of the collection `arr`

.
If there are proof side conditions to the application, they will be automatically
inferred by the `get_elem_tactic`

tactic.

The actual behavior of this class is type-dependent, but here are some important implementations:

`arr[i] : α`

where`arr : Array α`

and`i : Nat`

or`i : USize`

: does array indexing with no bounds check and a proof side goal`i < arr.size`

.`l[i] : α`

where`l : List α`

and`i : Nat`

: index into a list, with proof side goal`i < l.length`

.`stx[i] : Syntax`

where`stx : Syntax`

and`i : Nat`

: get a syntax argument, no side goal (returns`.missing`

out of range)

There are other variations on this syntax:

`arr[i]`

: proves the proof side goal by`get_elem_tactic`

`arr[i]!`

: panics if the side goal is false`arr[i]?`

: returns`none`

if the side goal is false`arr[i]'h`

: uses`h`

to prove the side goal

## Equations

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