`with_annotate_state stx t`

annotates the lexical range of `stx : Syntax`

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

.

## Instances For

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 : β ⊢ ...`

- Alternatively,
`intro`

can be combined with pattern matching much like`fun`

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

## Instances For

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

## Instances For

`clear x...`

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

## Instances For

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

## Instances For

Applies `subst`

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

or `h : t = x`

.

## Instances For

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

.

## Instances For

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

- Other simple contradictions such as

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

## Instances For

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

## Instances For

`exact e`

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

.

## Instances For

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

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

## Instances For

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

.

## Instances For

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

## Instances For

`all_goals tac`

runs `tac`

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

## Instances For

`any_goals tac`

applies the tactic `tac`

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

## Instances For

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

## Instances For

`done`

succeeds iff there are no remaining goals.

## Instances For

`trace_state`

displays the current state in the info view.

## Instances For

`trace msg`

displays `msg`

in the info view.

## Instances For

`fail_if_success t`

fails if the tactic `t`

succeeds.

## Instances For

`(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 `;`

.

## Instances For

`with_reducible tacs`

excutes `tacs`

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

are unfolded.

## Instances For

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

## Instances For

`with_unfolding_all tacs`

excutes `tacs`

using the `.all`

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

## Instances For

`first | tac | ...`

runs each `tac`

until one succeeds, or else fails.

## Instances For

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

.

## Instances For

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`

.

## Instances For

`try tac`

runs `tac`

and succeeds even if `tac`

failed.

## Instances For

`tac <;> tac'`

runs `tac`

on the main goal and `tac'`

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

.

## Instances For

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

## Instances For

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

## Instances For

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

## Instances For

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.

## Instances For

`admit`

is a shorthand for `exact sorry`

.

## Instances For

`infer_instance`

is an abbreviation for `exact inferInstance`

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

## Instances For

Optional configuration option for tactics

## Instances For

The `*`

location refers to all hypotheses and the goal.

## Instances For

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

denoting the goal.

## Instances For

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

## Instances For

If `thm`

is a theorem `a = b`

, then as a rewrite rule,

`thm`

means to replace`a`

with`b`

, and`← thm`

means to replace`b`

with`a`

.

## Instances For

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

Using `rw (config := {occs := .pos L}) [e]`

,
where `L : List Nat`

, you can control which "occurrences" are rewritten.
(This option applies to each rule, so usually this will only be used with a single rule.)
Occurrences count from `1`

.
At the first occurrence, whether allowed or not,
arguments of the rewrite rule `e`

may be instantiated,
restricting which later rewrites can be found.
`{occs := .neg L}`

allows skipping specified occurrences.

## Instances For

`rw`

is like `rewrite`

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

afterwards.

## Instances For

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.

## Instances For

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

.

## Instances For

The discharger clause of `simp`

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

## Instances For

Use this rewrite rule before entering the subterms

## Instances For

Use this rewrite rule after entering the subterms

## Instances For

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

## Instances For

An erasure specification `-thm`

says to remove `thm`

from the simp set

## Instances For

The simp lemma specification `*`

means to rewrite with all hypotheses

## Instances For

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.

## Instances For

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

## Instances For

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

## Instances For

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.

## Instances For

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

is the main goal after refining.

## Instances For

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

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

produces the hypotheses`h₁ : p`

,`h₂ : q`

, and`h₃ : r`

.

## Instances For

Given a main goal `ctx ⊢ t`

, `suffices h : t' from e`

replaces the main goal with `ctx ⊢ 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.

## Instances For

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

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

produces the hypotheses
`h₁ : p`

, `h₂ : q`

, and `h₃ : r`

.

## Instances For

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

.

## Instances For

`let rec f : t := e`

adds a recursive definition `f`

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

.

## Instances For

Similar to `refine_lift`

, but using `refine'`

## Instances For

Similar to `have`

, but using `refine'`

## Instances For

Similar to `have`

, but using `refine'`

## Instances For

Similar to `let`

, but using `refine'`

## Instances For

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.

## Instances For

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

, `?_`

, or a tactic sequence after the `=>`

.

## Instances For

After `with`

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

## Instances For

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`

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.

## Instances For

A `generalize`

argument, of the form `term = x`

or `h : term = x`

.

## Instances For

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

## Instances For

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

## Instances For

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.

## Instances For

`rename_i x_1 ... x_n`

renames the last `n`

inaccessible names using the given names.

## Instances For

`repeat tac`

repeatedly applies `tac`

to the main goal until it fails.
That is, if `tac`

produces multiple subgoals, only subgoals up to the first failure will be visited.
The `Std`

library provides `repeat'`

which repeats separately in each subgoal.

## Instances For

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

## Instances For

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`

and target `R`

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

or `next`

tactics.

## Instances For

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

## Instances For

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.

## Instances For

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

## Instances For

`fail msg`

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

## Instances For

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

## Instances For

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

## Instances For

The tactic `sleep ms`

sleeps for `ms`

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

## Instances For

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

and `⊢ 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))`

,
`congr`

produces the goals `⊢ x = y`

and `⊢ y = x`

,
while `congr 2`

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

.

## Instances For

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

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

(e.g. `x + 0 ≠ 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) :=
```

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

## Instances For

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

.

## Instances For

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

## Instances For

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

## Instances For

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

## Instances For

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