# Mathlib tactics

In addition to the tactics found in the core library, mathlib provides a number of specific interactive tactics. Here we document the mostly commonly used ones, as well as some underdocumented tactics from core.## Instance cache tactics

For performance reasons, Lean does not automatically update its database
of class instances during a proof. The group of tactics described below
helps to force such updates. For a simple (but very artificial) example,
consider the function `default`

from the core library. It has type
`Π (α : Sort u) [inhabited α], α`

, so one can use `default α`

only if Lean
can find a registered instance of `inhabited α`

. Because the database of
such instance is not automatically updated during a proof, the following
attempt won't work (Lean will not pick up the instance from the local
context):

```
def my_id (α : Type) : α → α :=
begin
intro x,
have : inhabited α := ⟨x⟩,
exact default α, -- Won't work!
end
```

However, it will work, producing the identity function, if one replaces `have`

by its variant `haveI`

described below.

`resetI`

: Reset the instance cache. This allows any instances currently in the context to be used in typeclass inference.`unfreezingI { tac }`

: Unfreeze local instances while executing the tactic`tac`

.`introI`

/`introsI`

:`intro`

/`intros`

followed by`resetI`

. Like`intro`

/`intros`

, but uses the introduced variable in typeclass inference.`casesI`

: like`cases`

, but can also be used with instance arguments.`substI`

: like`subst`

, but can also substitute in type-class arguments`haveI`

/`letI`

:`have`

/`let`

followed by`resetI`

. Used to add typeclasses to the context so that they can be used in typeclass inference. The syntax`haveI := <proof>`

and`haveI : t := <proof>`

is supported, but`haveI : t, from _`

and`haveI : t, { <proof> }`

are not; in these cases use`have : t, { <proof> }, resetI`

directly.`exactI`

:`resetI`

followed by`exact`

. Like`exact`

, but uses all variables in the context for typeclass inference.

## Related declarations

## Import using

- import tactic.cache
- import tactic.basic

## abel

Evaluate expressions in the language of *additive*, commutative monoids and groups.
It attempts to prove the goal outright if there is no `at`

specifier and the target is an equality, but if this
fails, it falls back to rewriting all monoid expressions into a normal form.
If there is an `at`

specifier, it rewrites the given target into a normal form.

```
example {α : Type*} {a b : α} [add_comm_monoid α] : a + (b + a) = a + a + b := by abel
example {α : Type*} {a b : α} [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel
example {α : Type*} {a b : α} [add_comm_group α] (hyp : a + a - a = b - b) : a = 0 :=
by { abel at hyp, exact hyp }
```

## Related declarations

## Import using

- import tactic.abel
- import tactic

## abstract

`abstract id { t }`

tries to use tactic `t`

to solve the main goal. If it succeeds, it abstracts the goal as an independent definition or theorem with name `id`

. If `id`

is omitted, a name is generated automatically.

## Related declarations

## Import using

- imported by default

## ac_mono

`ac_mono`

reduces the `f x ⊑ f y`

, for some relation `⊑`

and a
monotonic function `f`

to `x ≺ y`

.

`ac_mono*`

unwraps monotonic functions until it can't.

`ac_mono^k`

, for some literal number `k`

applies monotonicity `k`

times.

`ac_mono h`

, with `h`

a hypothesis, unwraps monotonic functions and
uses `h`

to solve the remaining goal. Can be combined with `*`

or `^k`

:
`ac_mono* h`

`ac_mono : p`

asserts `p`

and uses it to discharge the goal result
unwrapping a series of monotonic functions. Can be combined with * or
^k: `ac_mono* : p`

In the case where `f`

is an associative or commutative operator,
`ac_mono`

will consider any possible permutation of its arguments and
use the one the minimizes the difference between the left-hand side
and the right-hand side.

To use it, first import `tactic.monotonicity`

.

`ac_mono`

can be used as follows:

```
example (x y z k m n : ℕ)
(h₀ : z ≥ 0)
(h₁ : x ≤ y) :
(m + x + n) * z + k ≤ z * (y + n + m) + k :=
begin
ac_mono,
-- ⊢ (m + x + n) * z ≤ z * (y + n + m)
ac_mono,
-- ⊢ m + x + n ≤ y + n + m
ac_mono,
end
```

As with `mono*`

, `ac_mono*`

solves the goal in one go and so does
`ac_mono* h₁`

. The latter syntax becomes especially interesting in the
following example:

```
example (x y z k m n : ℕ)
(h₀ : z ≥ 0)
(h₁ : m + x + n ≤ y + n + m) :
(m + x + n) * z + k ≤ z * (y + n + m) + k :=
by ac_mono* h₁.
```

By giving `ac_mono`

the assumption `h₁`

, we are asking `ac_refl`

to
stop earlier than it would normally would.

## Related declarations

## Import using

- import tactic.monotonicity.interactive
- import tactic

## ac_refl

Proves a goal of the form `s = t`

when `s`

and `t`

are expressions built up out of a binary
operation, and equality can be proved using associativity and commutativity of that operation.

## Related declarations

## Import using

- imported by default

## all_goals

`all_goals { t }`

applies the tactic `t`

to every goal, and succeeds if each application succeeds.

## Related declarations

## Import using

- imported by default

## any_goals

`any_goals { t }`

applies the tactic `t`

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

## Related declarations

## Import using

- imported by default

## apply

The `apply`

tactic tries to match the current goal against the conclusion of the type of term. The argument term should be a term well-formed in the local context of the main goal. 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.

## Related declarations

## Import using

- imported by default

## apply_assumption

`apply_assumption`

looks for an assumption of the form `... → ∀ _, ... → head`

where `head`

matches the current goal.

If this fails, `apply_assumption`

will call `symmetry`

and try again.

If this also fails, `apply_assumption`

will call `exfalso`

and try again,
so that if there is an assumption of the form `P → ¬ Q`

, the new tactic state
will have two goals, `P`

and `Q`

.

Optional arguments:

`lemmas`

: a list of expressions to apply, instead of the local constants`tac`

: a tactic to run on each subgoal after applying an assumption; if this tactic fails, the corresponding assumption will be rejected and the next one will be attempted.

## Related declarations

## Import using

- import tactic.solve_by_elim
- import tactic.basic

## apply_auto_param

If the target of the main goal is an `auto_param`

, executes the associated tactic.

## Related declarations

## Import using

- imported by default

## apply_congr

Apply a congruence lemma inside `conv`

mode.

When called without an argument `apply_congr`

will try applying all lemmas marked with `@[congr]`

.
Otherwise `apply_congr e`

will apply the lemma `e`

.

Recall that a goal that appears as `∣ X`

in `conv`

mode
represents a goal of `⊢ X = ?m`

,
i.e. an equation with a metavariable for the right hand side.

To successfully use `apply_congr e`

, `e`

will need to be an equation
(possibly after function arguments),
which can be unified with a goal of the form `X = ?m`

.
The right hand side of `e`

will then determine the metavariable,
and `conv`

will subsequently replace `X`

with that right hand side.

As usual, `apply_congr`

can create new goals;
any of these which are _not_ equations with a metavariable on the right hand side
will be hard to deal with in `conv`

mode.
Thus `apply_congr`

automatically calls `intros`

on any new goals,
and fails if they are not then equations.

In particular it is useful for rewriting inside the operand of a `finset.sum`

,
as it provides an extra hypothesis asserting we are inside the domain.

For example:

```
example (f g : ℤ → ℤ) (S : finset ℤ) (h : ∀ m ∈ S, f m = g m) :
finset.sum S f = finset.sum S g :=
begin
conv_lhs {
-- If we just call `congr` here, in the second goal we're helpless,
-- because we are only given the opportunity to rewrite `f`.
-- However `apply_congr` uses the appropriate `@[congr]` lemma,
-- so we get to rewrite `f x`, in the presence of the crucial `H : x ∈ S` hypothesis.
apply_congr,
skip,
simp [h, H],
}
end
```

In the above example, when the `apply_congr`

tactic is called it gives the hypothesis `H : x ∈ S`

which is then used to rewrite the `f x`

to `g x`

.

## Related declarations

## Import using

- import tactic.converter.apply_congr
- import tactic.basic

## apply_fun

Apply a function to some local assumptions which are either equalities
or inequalities. For instance, if the context contains `h : a = b`

and
some function `f`

then `apply_fun f at h`

turns `h`

into
`h : f a = f b`

. When the assumption is an inequality `h : a ≤ b`

, a side
goal `monotone f`

is created, unless this condition is provided using
`apply_fun f at h using P`

where `P : monotone f`

, or the `mono`

tactic
can prove it.

Typical usage is:

```
open function
example (X Y Z : Type) (f : X → Y) (g : Y → Z) (H : injective $ g ∘ f) :
injective f :=
begin
intros x x' h,
apply_fun g at h,
exact H h
end
```

## Related declarations

## Import using

- import tactic.apply_fun
- import tactic

## apply_instance

This tactic tries to close the main goal `... ⊢ t`

by generating a term of type `t`

using type class resolution.

## Related declarations

## Import using

- imported by default

## apply_opt_param

If the target of the main goal is an `opt_param`

, assigns the default value.

## Related declarations

## Import using

- imported by default

## apply_rules

`apply_rules hs n`

applies the list of lemmas `hs`

and `assumption`

on the
first goal and the resulting subgoals, iteratively, at most `n`

times.
`n`

is optional, equal to 50 by default.
You can pass an `apply_cfg`

option argument as `apply_rules hs n opt`

.
(A typical usage would be with `apply_rules hs n { md := reducible })`

,
which asks `apply_rules`

to not unfold `semireducible`

definitions (i.e. most)
when checking if a lemma matches the goal.)

`hs`

can contain user attributes: in this case all theorems with this
attribute are added to the list of rules.

For instance:

```
@[user_attribute]
meta def mono_rules : user_attribute :=
{ name := `mono_rules,
descr := "lemmas usable to prove monotonicity" }
attribute [mono_rules] add_le_add mul_le_mul_of_nonneg_right
lemma my_test {a b c d e : real} (h1 : a ≤ b) (h2 : c ≤ d) (h3 : 0 ≤ e) :
a + c * e + a + c + 0 ≤ b + d * e + b + d + e :=
-- any of the following lines solve the goal:
add_le_add (add_le_add (add_le_add (add_le_add h1 (mul_le_mul_of_nonneg_right h2 h3)) h1 ) h2) h3
by apply_rules [add_le_add, mul_le_mul_of_nonneg_right]
by apply_rules [mono_rules]
by apply_rules mono_rules
```

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## apply_with

Similar to the `apply`

tactic, but allows the user to provide a `apply_cfg`

configuration object.

## Related declarations

## Import using

- imported by default

## assoc_rewrite

`assoc_rewrite [h₀,← h₁] at ⊢ h₂`

behaves like `rewrite [h₀,← h₁] at ⊢ h₂`

with the exception that associativity is used implicitly to make rewriting
possible.

## Related declarations

## Import using

- import tactic.rewrite
- import tactic.basic

## assume

Assuming the target of the goal is a Pi or a let, `assume h : t`

unifies the type of the binder with `t`

and introduces it with name `h`

, just like `intro h`

. If `h`

is absent, the tactic uses the name `this`

. If `t`

is omitted, it will be inferred.

`assume (h₁ : t₁) ... (hₙ : tₙ)`

introduces multiple hypotheses. Any of the types may be omitted, but the names must be present.

## Related declarations

## Import using

- imported by default

## assumption

This tactic looks in the local context for a hypothesis whose type is equal to the goal target. If it finds one, it uses it to prove the goal, and otherwise it fails.

## Related declarations

## Import using

- imported by default

## assumption'

Try to apply `assumption`

to all goals.

## Related declarations

## Import using

- imported by default

## async

Proves the first goal asynchronously as a separate lemma.

## Related declarations

## Import using

- imported by default

## by_cases

`by_cases p`

splits the main goal into two cases, assuming `h : p`

in the first branch, and
`h : ¬ p`

in the second branch. You can specify the name of the new hypothesis using the syntax
`by_cases h : p`

.

If `p`

is not already decidable, `by_cases`

will use the instance `classical.prop_decidable p`

.

## Related declarations

## Import using

- imported by default

## by_contra / by_contradiction

If the target of the main goal is a proposition `p`

, `by_contra h`

reduces the goal to proving
`false`

using the additional hypothesis `h : ¬ p`

. If `h`

is omitted, a name is generated
automatically.

This tactic requires that `p`

is decidable. To ensure that all propositions are decidable via
classical reasoning, use `open_locale classical`

(or `local attribute [instance, priority 10] classical.prop_decidable`

if you are not using
mathlib).

## Related declarations

## Import using

- imported by default

## cancel_denoms

`cancel_denoms`

attempts to remove numerals from the denominators of fractions.
It works on propositions that are field-valued inequalities.

```
variables {α : Type} [linear_ordered_field α] (a b c : α)
example (h : a / 5 + b / 4 < c) : 4*a + 5*b < 20*c :=
begin
cancel_denoms at h,
exact h
end
example (h : a > 0) : a / 5 > 0 :=
begin
cancel_denoms,
exact h
end
```

## Related declarations

## Import using

- import tactic.cancel_denoms
- import tactic

## case

Focuses on a goal ('case') generated by `induction`

, `cases`

or `with_cases`

.

The goal is selected by giving one or more names which must match exactly one goal. A goal is matched if the given names are a suffix of its goal tag. Additionally, each name in the sequence can be abbreviated to a suffix of the corresponding name in the goal tag. Thus, a goal with tag

can be selected with any of these invocations (among others):

Additionally, the form

```
case C : N₀ ... Nₙ {...}
```

can be used to rename hypotheses introduced by the preceding
`cases`

/`induction`

/`with_cases`

, using the names `Nᵢ`

. For example:

```
example (xs : list ℕ) : xs = xs :=
begin
induction xs,
case nil { reflexivity },
case cons : x xs ih {
-- x : ℕ, xs : list ℕ, ih : xs = xs
reflexivity }
end
```

Note that this renaming functionality only work reliably *directly after* an
`induction`

/`cases`

/`with_cases`

. If you need to perform additional work after
an `induction`

or `cases`

(e.g. introduce hypotheses in all goals), use
`with_cases`

.

## Related declarations

## Import using

- imported by default

## cases

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.

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.

`cases e`

, where `e`

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

in the goal, and then cases on the resulting variable.

`cases e with y₁ ... yₙ`

, where `e`

is a variable or an expression, specifies that the sequence of names `y₁ ... yₙ`

should be used for the arguments to the constructors, including implicit arguments. If the list does not include enough names for all of the arguments, additional names are generated automatically. If too many names are given, the extra ones are ignored. Underscores can be used in the list, in which case the corresponding names are generated automatically.

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

## Related declarations

## Import using

- imported by default

## cases_matching / casesm

`cases_matching p`

applies the `cases`

tactic to a hypothesis `h : type`

if `type`

matches the pattern `p`

.

`cases_matching [p_1, ..., p_n]`

applies the `cases`

tactic to a hypothesis `h : type`

if `type`

matches one of the given patterns.

`cases_matching* p`

is a more efficient and compact version
of `focus1 { repeat { cases_matching p } }`

.
It is more efficient because the pattern is compiled once.

`casesm`

is shorthand for `cases_matching`

.

Example: The following tactic destructs all conjunctions and disjunctions in the current context.

```
cases_matching* [_ ∨ _, _ ∧ _]
```

## Related declarations

## Import using

- imported by default

## cases_type

`cases_type I`

applies the`cases`

tactic to a hypothesis`h : (I ...)`

`cases_type I_1 ... I_n`

applies the`cases`

tactic to a hypothesis`h : (I_1 ...)`

or ... or`h : (I_n ...)`

`cases_type* I`

is shorthand for`focus1 { repeat { cases_type I } }`

`cases_type! I`

only applies`cases`

if the number of resulting subgoals is <= 1.

Example: The following tactic destructs all conjunctions and disjunctions in the current context.

```
cases_type* or and
```

## Related declarations

## Import using

- imported by default

## category_theory.reassoc_of

`reassoc_of h`

takes local assumption `h`

and add a `≫ f`

term on the right of
both sides of the equality. Instead of creating a new assumption from the result, `reassoc_of h`

stands for the proof of that reassociated statement. This keeps complicated assumptions that are
used only once or twice from polluting the local context.

In the following, assumption `h`

is needed in a reassociated form. Instead of proving it as a new
goal and adding it as an assumption, we use `reassoc_of h`

as a rewrite rule which works just as
well.

```
example (X Y Z W : C) (x : X ⟶ Y) (y : Y ⟶ Z) (z z' : Z ⟶ W) (w : X ⟶ Z)
(h : x ≫ y = w)
(h' : y ≫ z = y ≫ z') :
x ≫ y ≫ z = w ≫ z' :=
begin
-- reassoc_of h : ∀ {X' : C} (f : W ⟶ X'), x ≫ y ≫ f = w ≫ f
rw [h',reassoc_of h],
end
```

Although `reassoc_of`

is not a tactic or a meta program, its type is generated
through meta-programming to make it usable inside normal expressions.

## Related declarations

## Import using

- import tactic.reassoc_axiom
- import tactic

## cc (congruence closure)

The congruence closure tactic `cc`

tries to solve the goal by chaining
equalities from context and applying congruence (i.e. if `a = b`

, then `f a = f b`

).
It is a finishing tactic, i.e. it is meant to close
the current goal, not to make some inconclusive progress.
A mostly trivial example would be:

```
example (a b c : ℕ) (f : ℕ → ℕ) (h: a = b) (h' : b = c) : f a = f c := by cc
```

As an example requiring some thinking to do by hand, consider:

```
example (f : ℕ → ℕ) (x : ℕ)
(H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) :
f x = x :=
by cc
```

The tactic works by building an equality matching graph. It's a graph where the vertices are terms and they are linked by edges if they are known to be equal. Once you've added all the equalities in your context, you take the transitive closure of the graph and, for each connected component (i.e. equivalence class) you can elect a term that will represent the whole class and store proofs that the other elements are equal to it. You then take the transitive closure of these equalities under the congruence lemmas.

The `cc`

implementation in Lean does a few more tricks: for example it
derives `a=b`

from `nat.succ a = nat.succ b`

, and ```
nat.succ a !=
nat.zero
```

for any `a`

.

The starting reference point is Nelson, Oppen, Fast decision procedures based on congruence closure, Journal of the ACM (1980)

The congruence lemmas for dependent type theory as used in Lean are described in Congruence closure in intensional type theory (de Moura, Selsam IJCAR 2016).

## Related declarations

## Import using

- imported by default

## change

`change u`

replaces the target `t`

of the main goal to `u`

provided that `t`

is well formed with respect to the local context of the main goal and `t`

and `u`

are definitionally equal.

`change u at h`

will change a local hypothesis to `u`

.

`change t with u at h1 h2 ...`

will replace `t`

with `u`

in all the supplied hypotheses (or `*`

), or in the goal if no `at`

clause is specified, provided that `t`

and `u`

are definitionally equal.

## Related declarations

## Import using

- imported by default

## change'

The logic of `change x with y at l`

fails when there are dependencies.
`change'`

mimics the behavior of `change`

, except in the case of `change x with y at l`

.
In this case, it will correctly replace occurences of `x`

with `y`

at all possible hypotheses
in `l`

. As long as `x`

and `y`

are defeq, it should never fail.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## choose

`choose a b h h' using hyp`

takes an hypothesis `hyp`

of the form
`∀ (x : X) (y : Y), ∃ (a : A) (b : B), P x y a b ∧ Q x y a b`

for some `P Q : X → Y → A → B → Prop`

and outputs
into context a function `a : X → Y → A`

, `b : X → Y → B`

and two assumptions:
`h : ∀ (x : X) (y : Y), P x y (a x y) (b x y)`

and
`h' : ∀ (x : X) (y : Y), Q x y (a x y) (b x y)`

. It also works with dependent versions.

`choose! a b h h' using hyp`

does the same, except that it will remove dependency of
the functions on propositional arguments if possible. For example if `Y`

is a proposition
and `A`

and `B`

are nonempty in the above example then we will instead get
`a : X → A`

, `b : X → B`

, and the assumptions
`h : ∀ (x : X) (y : Y), P x y (a x) (b x)`

and
`h' : ∀ (x : X) (y : Y), Q x y (a x) (b x)`

.

Examples:

```
example (h : ∀n m : ℕ, ∃i j, m = n + i ∨ m + j = n) : true :=
begin
choose i j h using h,
guard_hyp i : ℕ → ℕ → ℕ,
guard_hyp j : ℕ → ℕ → ℕ,
guard_hyp h : ∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n,
trivial
end
```

```
example (h : ∀ i : ℕ, i < 7 → ∃ j, i < j ∧ j < i+i) : true :=
begin
choose! f h h' using h,
guard_hyp f : ℕ → ℕ,
guard_hyp h : ∀ (i : ℕ), i < 7 → i < f i,
guard_hyp h' : ∀ (i : ℕ), i < 7 → f i < i + i,
trivial,
end
```

## Related declarations

## Import using

- import tactic.choose
- import tactic.basic

## classical

Make every proposition in the context decidable.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## clear

`clear h₁ ... hₙ`

tries to clear each hypothesis `hᵢ`

from the local context.

## Related declarations

## Import using

- imported by default

## clear'

An improved version of the standard `clear`

tactic. `clear`

is sensitive to the
order of its arguments: `clear x y`

may fail even though both `x`

and `y`

could
be cleared (if the type of `y`

depends on `x`

). `clear'`

lifts this limitation.

```
example {α} {β : α → Type} (a : α) (b : β a) : unit :=
begin
try { clear a b }, -- fails since `b` depends on `a`
clear' a b, -- succeeds
exact ()
end
```

## Related declarations

## Import using

- import tactic.clear
- import tactic.basic

## clear_

Clear all hypotheses starting with `_`

, like `_match`

and `_let_match`

.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## clear_aux_decl

`clear_aux_decl`

clears every `aux_decl`

in the local context for the current goal.
This includes the induction hypothesis when using the equation compiler and
`_let_match`

and `_fun_match`

.

It is useful when using a tactic such as `finish`

, `simp *`

or `subst`

that may use these
auxiliary declarations, and produce an error saying the recursion is not well founded.

```
example (n m : ℕ) (h₁ : n = m) (h₂ : ∃ a : ℕ, a = n ∧ a = m) : 2 * m = 2 * n :=
let ⟨a, ha⟩ := h₂ in
begin
clear_aux_decl, -- subst will fail without this line
subst h₁
end
example (x y : ℕ) (h₁ : ∃ n : ℕ, n * 1 = 2) (h₂ : 1 + 1 = 2 → x * 1 = y) : x = y :=
let ⟨n, hn⟩ := h₁ in
begin
clear_aux_decl, -- finish produces an error without this line
finish
end
```

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## clear_except

`clear_except h₀ h₁`

deletes all the assumptions it can except for `h₀`

and `h₁`

.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## clear_value

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

.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## comp_val

Close goals of the form `n ≠ m`

when `n`

and `m`

have type `nat`

, `char`

, `string`

, `int`

or `fin sz`

, and they are literals. It also closes goals of the form `n < m`

, `n > m`

, `n ≤ m`

and
`n ≥ m`

for `nat`

. If the goal is of the form `n = m`

, then it tries to close it using reflexivity.

In mathlib, consider using `norm_num`

instead for numeric types.

## Related declarations

## Import using

- imported by default

## congr

The `congr`

tactic attempts to identify both sides of an equality goal `A = B`

,
leaving as new goals the subterms of `A`

and `B`

which are not definitionally equal.
Example: suppose the goal is `x * f y = g w * f z`

. Then `congr`

will produce two goals:
`x = g w`

and `y = z`

.

If `x y : t`

, and an instance `subsingleton t`

is in scope, then any goals of the form
`x = y`

are solved automatically.

Note that `congr`

can be over-aggressive at times; the `congr'`

tactic in mathlib
provides a more refined approach, by taking a parameter that limits the recursion depth.

## Related declarations

## Import using

- imported by default

## congr'

Same as the `congr`

tactic, but takes an optional argument which gives
the depth of 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`

. - If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.
- You can use
`congr' with p (: n)?`

to call`ext p (: n)?`

to all subgoals generated by`congr'`

. For example, if the goal is`⊢ f '' s = g '' s`

then`congr' with x`

generates the goal`x : α ⊢ f x = g x`

.

## Related declarations

## Import using

- import tactic.congr
- import tactic.basic

## constructor

This tactic applies to a goal such that its conclusion is an inductive type (say `I`

). It tries to apply each constructor of `I`

until it succeeds.

## Related declarations

## Import using

- imported by default

## continuity / continuity'

`continuity`

solves goals of the form `continuous f`

by applying lemmas tagged with the
`continuity`

user attribute.

```
example {X Y : Type*} [topological_space X] [topological_space Y]
(f₁ f₂ : X → Y) (hf₁ : continuous f₁) (hf₂ : continuous f₂)
(g : Y → ℝ) (hg : continuous g) : continuous (λ x, (max (g (f₁ x)) (g (f₂ x))) + 1) :=
by continuity
```

will discharge the goal, generating a proof term like
`((continuous.comp hg hf₁).max (continuous.comp hg hf₂)).add continuous_const`

You can also use `continuity!`

, which applies lemmas with `{ md := semireducible }`

.
The default behaviour is more conservative, and only unfolds `reducible`

definitions
when attempting to match lemmas with the goal.

`continuity?`

reports back the proof term it found.

## Related declarations

## Import using

- import topology.tactic

## contradiction

The contradiction tactic attempts to find in the current local context a hypothesis that is equivalent to an empty inductive type (e.g. `false`

), a hypothesis of the form `c_1 ... = c_2 ...`

where `c_1`

and `c_2`

are distinct constructors, or two contradictory hypotheses.

## Related declarations

## Import using

- imported by default

## contrapose

Transforms the goal into its contrapositive.

`contrapose`

turns a goal`P → Q`

into`¬ Q → ¬ P`

`contrapose!`

turns a goal`P → Q`

into`¬ Q → ¬ P`

and pushes negations inside`P`

and`Q`

using`push_neg`

`contrapose h`

first reverts the local assumption`h`

, and then uses`contrapose`

and`intro h`

`contrapose! h`

first reverts the local assumption`h`

, and then uses`contrapose!`

and`intro h`

`contrapose h with new_h`

uses the name`new_h`

for the introduced hypothesis

## Related declarations

## Import using

- import tactic.push_neg
- import tactic.basic

## conv

`conv {...}`

allows the user to perform targeted rewriting on a goal or hypothesis,
by focusing on particular subexpressions.

See https://leanprover-community.github.io/extras/conv.html for more details.

Inside `conv`

blocks, mathlib currently additionally provides

`apply_congr`

applies congruence lemmas to step further inside expressions,
and sometimes gives between results than the automatically generated
congruence lemmas used by `congr`

.

Using `conv`

inside a `conv`

block allows the user to return to the previous
state of the outer `conv`

block after it is finished. Thus you can continue
editing an expression without having to start a new `conv`

block and re-scoping
everything. For example:

```
example (a b c d : ℕ) (h₁ : b = c) (h₂ : a + c = a + d) : a + b = a + d :=
by conv {
to_lhs,
conv {
congr, skip,
rw h₁,
},
rw h₂,
}
```

Without `conv`

, the above example would need to be proved using two successive
`conv`

blocks, each beginning with `to_lhs`

.

Also, as a shorthand, `conv_lhs`

and `conv_rhs`

are provided, so that

```
example : 0 + 0 = 0 :=
begin
conv_lhs { simp }
end
```

just means

```
example : 0 + 0 = 0 :=
begin
conv { to_lhs, simp }
end
```

and likewise for `to_rhs`

.

## Related declarations

## Import using

- imported by default

## conv: congr

Navigate into every argument of the current head function.
A target of `| (a * b) * c`

will turn into the two targets `| a * b`

and `| c`

.

## Related declarations

## Import using

- imported by default

## conv: find

Navigate into the first scope matching the expression.

For a target of `| ∀ c, a + (b + c) = 1`

, `find (b + _) { ... }`

will run the tactics within the
`{}`

with a target of `| b + c`

.

## Related declarations

## Import using

- imported by default

## conv: for

Navigate into the numbered scopes matching the expression.

For a target of `| λ c, 10 * c + 20 * c + 30 * c`

, `for (_ * _) [1, 3] { ... }`

will run the
tactics within the `{}`

with first a target of `| 10 * c`

, then a target of `| 30 * c`

.

## Related declarations

## Import using

- imported by default

## conv: funext

Navigate into the contents of top-level `λ`

binders.
A target of `| λ a, a + b`

will turn into the target `| a + b`

and introduce `a`

into the local
context.
If there are multiple binders, all of them will be entered, and if there are none, this tactic is a no-op.

## Related declarations

## Import using

- imported by default

## conv: skip

End conversion of the current goal. This is often what is needed when muscle memory would type `sorry`

.

## Related declarations

## Import using

- imported by default

## conv: to_lhs

Navigate to the left-hand-side of a relation.
A goal of `| a = b`

will turn into the the goal `| a`

.

## Related declarations

## Import using

- imported by default

## conv: to_rhs

Navigate to the right-hand-side of a relation.
A goal of `| a = b`

will turn into the the goal `| b`

.

## Related declarations

## Import using

- imported by default

## convert

The `exact e`

and `refine e`

tactics require a term `e`

whose type is
definitionally equal to the goal. `convert e`

is similar to ```
refine
e
```

, but the type of `e`

is not required to exactly match the
goal. Instead, new goals are created for differences between the type
of `e`

and the goal. For example, in the proof state

the tactic `convert e`

will change the goal to

```
⊢ n + n = 2 * n
```

In this example, the new goal can be solved using `ring`

.

If `x y : t`

, and an instance `subsingleton t`

is in scope, then any goals of the form
`x = y`

are solved automatically.

The syntax `convert ← e`

will reverse the direction of the new goals
(producing `⊢ 2 * n = n + n`

in this example).

Internally, `convert e`

works by creating a new goal asserting that
the goal equals the type of `e`

, then simplifying it using
`congr'`

. The syntax `convert e using n`

can be used to control the
depth of matching (like `congr' n`

). In the example, ```
convert e using
1
```

would produce a new goal `⊢ n + n + 1 = 2 * n + 1`

.

## Related declarations

## Import using

- import tactic.congr
- import tactic.basic

## convert_to

`convert_to g using n`

attempts to change the current goal to `g`

, but unlike `change`

,
it will generate equality proof obligations using `congr' n`

to resolve discrepancies.
`convert_to g`

defaults to using `congr' 1`

.

`ac_change`

is `convert_to`

followed by `ac_refl`

. It is useful for rearranging/reassociating
e.g. sums:

```
example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N :=
begin
ac_change a + d + e + f + c + g + b ≤ _,
-- ⊢ a + d + e + f + c + g + b ≤ N
end
```

## Related declarations

## Import using

- import tactic.congr
- import tactic.basic

## dec_trivial

`dec_trivial`

tries to use decidability to prove a goal
(i.e., using `exact dec_trivial`

).
The variant `dec_trivial!`

will revert all hypotheses on which the target depends,
before it tries `exact dec_trivial`

.

Example:

```
example (n : ℕ) (h : n < 2) : n = 0 ∨ n = 1 :=
by dec_trivial!
```

## Related declarations

## Import using

- import tactic.dec_trivial
- import tactic.basic

## delta

Similar to `dunfold`

, but performs a raw delta reduction, rather than using an equation associated with the defined constants.

## Related declarations

## Import using

- imported by default

## destruct

Assuming `x`

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

splits the main goal, producing one goal for each constructor of the inductive type, in which `x`

is assumed to be a general instance of that constructor. In contrast to `cases`

, the local context is unchanged, i.e. no elements are reverted or introduced.

For example, given `n : nat`

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

and target `Q n`

, `destruct n`

produces one goal with target `n = 0 → Q n`

, and one goal with target `∀ (a : ℕ), (λ (w : ℕ), n = w → Q n) (nat.succ a)`

. Here the name `a`

is chosen automatically.

## Related declarations

## Import using

- imported by default

## dsimp

`dsimp`

is similar to `simp`

, except that it only uses definitional equalities.

## Related declarations

## Import using

- imported by default

## dunfold

Similar to `unfold`

, but only uses definitional equalities.

## Related declarations

## Import using

- imported by default

## eapply

Similar to the `apply`

tactic, but only creates subgoals for non-dependent premises that have not been fixed by type inference or type class resolution.

## Related declarations

## Import using

- imported by default

## econstructor

Similar to `constructor`

, but only non-dependent premises are added as new goals.

## Related declarations

## Import using

- imported by default

## elide / unelide

The `elide n (at ...)`

tactic hides all subterms of the target goal or hypotheses
beyond depth `n`

by replacing them with `hidden`

, which is a variant
on the identity function. (Tactics should still mostly be able to see
through the abbreviation, but if you want to unhide the term you can use
`unelide`

.)

The `unelide (at ...)`

tactic removes all `hidden`

subterms in the target
types (usually added by `elide`

).

## Related declarations

## Import using

- import tactic.elide
- import tactic.basic

## equiv_rw

`equiv_rw e at h`

, where `h : α`

is a hypothesis, and `e : α ≃ β`

,
will attempt to transport `h`

along `e`

, producing a new hypothesis `h : β`

,
with all occurrences of `h`

in other hypotheses and the goal replaced with `e.symm h`

.

`equiv_rw e`

will attempt to transport the goal along an equivalence `e : α ≃ β`

.
In its minimal form it replaces the goal `⊢ α`

with `⊢ β`

by calling `apply e.inv_fun`

.

`equiv_rw`

will also try rewriting under (equiv_)functors, so can turn
a hypothesis `h : list α`

into `h : list β`

or
a goal `⊢ unique α`

into `⊢ unique β`

.

The maximum search depth for rewriting in subexpressions is controlled by
`equiv_rw e {max_depth := n}`

.

## Related declarations

## Import using

- import tactic.equiv_rw
- import tactic

## equiv_rw_type

Solve a goal of the form `t ≃ _`

,
by constructing an equivalence from `e : α ≃ β`

.
This is the same equivalence that `equiv_rw`

would use to rewrite a term of type `t`

.

A typical usage might be:

## Related declarations

## Import using

- import tactic.equiv_rw
- import tactic

## erewrite / erw

A variant of `rw`

that uses the unifier more aggressively, unfolding semireducible definitions.

## Related declarations

## Import using

- imported by default

## exact

This tactic provides an exact proof term to solve the main goal. If `t`

is the goal and `p`

is a term of type `u`

then `exact p`

succeeds if and only if `t`

and `u`

can be unified.

## Related declarations

## Import using

- imported by default

## exacts

Like `exact`

, but takes a list of terms and checks that all goals are discharged after the tactic.

## Related declarations

## Import using

- imported by default

## exfalso

Replaces the target of the main goal by `false`

.

## Related declarations

## Import using

- imported by default

## existsi

`existsi e`

will instantiate an existential quantifier in the target with `e`

and leave the
instantiated body as the new target. More generally, it applies to any inductive type with one
constructor and at least two arguments, applying the constructor with `e`

as the first argument
and leaving the remaining arguments as goals.

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

iteratively does the same for each expression in the list.

Note: in mathlib, the `use`

tactic is an equivalent tactic which sometimes is smarter with
unification.

## Related declarations

## Import using

- imported by default

## ext1 / ext

`ext1 id`

selects and apply one extensionality lemma (with attribute`ext`

), using`id`

, if provided, to name a local constant introduced by the lemma. If`id`

is omitted, the local constant is named automatically, as per`intro`

.`ext`

applies as many extensionality lemmas as possible;`ext ids`

, with`ids`

a list of identifiers, finds extensionality lemmas and applies them until it runs out of identifiers in`ids`

to name the local constants.`ext`

can also be given an`rcases`

pattern in place of an identifier. This will destruct the introduced local constant.

When trying to prove:

```
α β : Type,
f g : α → set β
⊢ f = g
```

applying `ext x y`

yields:

```
α β : Type,
f g : α → set β,
x : α,
y : β
⊢ y ∈ f x ↔ y ∈ g x
```

by applying functional extensionality and set extensionality.

When trying to prove:

```
α β γ : Type
f g : α × β → γ
⊢ f = g
```

applying `ext ⟨a, b⟩`

yields:

```
α β γ : Type,
f g : α × β → γ,
a : α,
b : β
⊢ f (a, b) = g (a, b)
```

by applying functional extensionality and destructing the introduced pair.

A maximum depth can be provided with `ext x y z : 3`

.

## Related declarations

## Import using

- import tactic.ext
- import tactic.basic

## extract_goal

Format the current goal as a stand-alone example. Useful for testing tactics or creating minimal working examples.

`extract_goal`

: formats the statement as an`example`

declaration`extract_goal my_decl`

: formats the statement as a`lemma`

or`def`

declaration called`my_decl`

`extract_goal with i j k:`

only use local constants`i`

,`j`

,`k`

in the declaration

Examples:

```
example (i j k : ℕ) (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k :=
begin
extract_goal,
-- prints:
-- example (i j k : ℕ) (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k :=
-- begin
-- admit,
-- end
extract_goal my_lemma
-- prints:
-- lemma my_lemma (i j k : ℕ) (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k :=
-- begin
-- admit,
-- end
end
example {i j k x y z w p q r m n : ℕ} (h₀ : i ≤ j) (h₁ : j ≤ k) (h₁ : k ≤ p) (h₁ : p ≤ q) : i ≤ k :=
begin
extract_goal my_lemma,
-- prints:
-- lemma my_lemma {i j k x y z w p q r m n : ℕ}
-- (h₀ : i ≤ j)
-- (h₁ : j ≤ k)
-- (h₁ : k ≤ p)
-- (h₁ : p ≤ q) :
-- i ≤ k :=
-- begin
-- admit,
-- end
extract_goal my_lemma with i j k
-- prints:
-- lemma my_lemma {p i j k : ℕ}
-- (h₀ : i ≤ j)
-- (h₁ : j ≤ k)
-- (h₁ : k ≤ p) :
-- i ≤ k :=
-- begin
-- admit,
-- end
end
example : true :=
begin
let n := 0,
have m : ℕ, admit,
have k : fin n, admit,
have : n + m + k.1 = 0, extract_goal,
-- prints:
-- example (m : ℕ) : let n : ℕ := 0 in ∀ (k : fin n), n + m + k.val = 0 :=
-- begin
-- intros n k,
-- admit,
-- end
end
```

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## fail_if_success

Fails if the given tactic succeeds.

## Related declarations

## Import using

- imported by default

## fapply

Similar to the `apply`

tactic, but does not reorder goals.

## Related declarations

## Import using

- imported by default

## fconstructor

Similar to `constructor`

, but does not reorder goals.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## field_simp

The goal of `field_simp`

is to reduce an expression in a field to an expression of the form `n / d`

where neither `n`

nor `d`

contains any division symbol, just using the simplifier (with a carefully
crafted simpset named `field_simps`

) to reduce the number of division symbols whenever possible by
iterating the following steps:

- write an inverse as a division
- in any product, move the division to the right
- if there are several divisions in a product, group them together at the end and write them as a single division
- reduce a sum to a common denominator

If the goal is an equality, this simpset will also clear the denominators, so that the proof
can normally be concluded by an application of `ring`

or `ring_exp`

.

`field_simp [hx, hy]`

is a short form for `simp [-one_div, hx, hy] with field_simps`

Note that this naive algorithm will not try to detect common factors in denominators to reduce the
complexity of the resulting expression. Instead, it relies on the ability of `ring`

to handle
complicated expressions in the next step.

As always with the simplifier, reduction steps will only be applied if the preconditions of the lemmas can be checked. This means that proofs that denominators are nonzero should be included. The fact that a product is nonzero when all factors are, and that a power of a nonzero number is nonzero, are included in the simpset, but more complicated assertions (especially dealing with sums) should be given explicitly. If your expression is not completely reduced by the simplifier invocation, check the denominators of the resulting expression and provide proofs that they are nonzero to enable further progress.

The invocation of `field_simp`

removes the lemma `one_div`

(which is marked as a simp lemma
in core) from the simpset, as this lemma works against the algorithm explained above.

For example,

```
example (a b c d x y : ℂ) (hx : x ≠ 0) (hy : y ≠ 0) :
a + b / x + c / x^2 + d / x^3 = a + x⁻¹ * (y * b / y + (d / x + c) / x) :=
begin
field_simp [hx, hy],
ring
end
See also the `cancel_denoms` tactic, which tries to do a similar simplification for expressions
that have numerals in denominators.
The tactics are not related: `cancel_denoms` will only handle numeric denominators, and will try to
entirely remove (numeric) division from the expression by multiplying by a factor.
```

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## filter_upwards

`filter_upwards [h1, ⋯, hn]`

replaces a goal of the form `s ∈ f`

and terms `h1 : t1 ∈ f, ⋯, hn : tn ∈ f`

with `∀x, x ∈ t1 → ⋯ → x ∈ tn → x ∈ s`

.

`filter_upwards [h1, ⋯, hn] e`

is a short form for `{ filter_upwards [h1, ⋯, hn], exact e }`

.

## Related declarations

## Import using

- import order.filter.basic

## fin_cases

`fin_cases h`

performs case analysis on a hypothesis of the form
`h : A`

, where `[fintype A]`

is available, or
`h ∈ A`

, where `A : finset X`

, `A : multiset X`

or `A : list X`

.

`fin_cases *`

performs case analysis on all suitable hypotheses.

As an example, in

```
example (f : ℕ → Prop) (p : fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val :=
begin
fin_cases *; simp,
all_goals { assumption }
end
```

after `fin_cases p; simp`

, there are three goals, `f 0`

, `f 1`

, and `f 2`

.

## Related declarations

## Import using

- import tactic.fin_cases
- import tactic

## finish / clarify / safe

These tactics do straightforward things: they call the simplifier, split conjunctive assumptions, eliminate existential quantifiers on the left, and look for contradictions. They rely on ematching and congruence closure to try to finish off a goal at the end.

The procedures *do* split on disjunctions and recreate the smt state for each terminal call, so
they are only meant to be used on small, straightforward problems.

`finish`

: solves the goal or fails`clarify`

: makes as much progress as possible while not leaving more than one goal`safe`

: splits freely, finishes off whatever subgoals it can, and leaves the rest

All accept an optional list of simplifier rules, typically definitions that should be expanded.
(The equations and identities should not refer to the local context.) All also accept an optional
list of `ematch`

lemmas, which must be preceded by `using`

.

## Related declarations

## Import using

- import tactic.finish
- import tactic.basic

## focus

`focus { t }`

temporarily hides all goals other than the first, applies `t`

, and then restores the other goals. It fails if there are no goals.

## Related declarations

## Import using

- imported by default

## from

A synonym for `exact`

that allows writing `have/suffices/show ..., from ...`

in tactic mode.

## Related declarations

## Import using

- imported by default

## fsplit

Just like `split`

, `fsplit`

applies the constructor when the type of the target is
an inductive data type with one constructor.
However it does not reorder goals or invoke `auto_param`

tactics.

## Related declarations

## Import using

- import tactic.core
- import tactic.basic

## funext

Apply function extensionality and introduce new hypotheses.
The tactic `funext`

will keep applying new the `funext`

lemma until the goal target is not reducible
to

```
|- ((fun x, ...) = (fun x, ...))
```

The variant `funext h₁ ... hₙ`

applies `funext`

`n`

times, and uses the given identifiers to name
the new hypotheses.

Note also the mathlib tactic `ext`

, which applies as many extensionality lemmas as possible.

## Related declarations

## Import using

- imported by default

## generalize

`generalize : e = x`

replaces all occurrences of `e`

in the target with a new hypothesis `x`

of the same type.

`generalize h : e = x`

in addition registers the hypothesis `h : e = x`

.

## Related declarations

## Import using

- imported by default

## generalize'

`generalize' : e = x`

replaces all occurrences of `e`

in the target with a new hypothesis `x`

of
the same type.

`generalize' h : e = x`

in addition registers the hypothesis `h : e = x`

.

`generalize'`

is similar to `generalize`

. The difference is that `generalize' : e = x`

also
succeeds when `e`

does not occur in the goal. It is similar to `set`

, but the resulting hypothesis
`x`

is not a local definition.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## generalize_hyp

Like `generalize`

but also considers assumptions
specified by the user. The user can also specify to
omit the goal.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## generalizes

Generalizes the target over multiple expressions. For example, given the goal

```
P : ∀ n, fin n → Prop
n : ℕ
f : fin n
⊢ P (nat.succ n) (fin.succ f)
```

you can use `generalizes [n'_eq : nat.succ n = n', f'_eq : fin.succ f == f']`

to
get

```
P : ∀ n, fin n → Prop
n : ℕ
f : fin n
n' : ℕ
n'_eq : n' = nat.succ n
f' : fin n'
f'_eq : f' == fin.succ f
⊢ P n' f'
```

The expressions must be given in dependency order, so
`[f'_eq : fin.succ f == f', n'_eq : nat.succ n = n']`

would fail since the type
of `fin.succ f`

is `nat.succ n`

.

You can choose to omit some or all of the generated equations. For the above
example, `generalizes [nat.succ n = n', fin.succ f == f']`

gets you

```
P : ∀ n, fin n → Prop
n : ℕ
f : fin n
n' : ℕ
f' : fin n'
⊢ P n' f'
```

After generalization, the target type may no longer type check. `generalizes`

will then raise an error.

## Related declarations

## Import using

- import tactic.generalizes
- import tactic.basic

## group

Tactic for normalizing expressions in multiplicative groups, without assuming commutativity, using only the group axioms without any information about which group is manipulated.

(For additive commutative groups, use the `abel`

tactic instead.)

Example:

```
example {G : Type} [group G] (a b c d : G) (h : c = (a*b^2)*((b*b)⁻¹*a⁻¹)*d) : a*c*d⁻¹ = a :=
begin
group at h, -- normalizes `h` which becomes `h : c = d`
rw h, -- the goal is now `a*d*d⁻¹ = a`
group, -- which then normalized and closed
end
```

## Related declarations

## Import using

- import tactic.group
- import tactic

## guard_hyp

`guard_hyp h : t`

fails if the hypothesis `h`

does not have type `t`

.
We use this tactic for writing tests.

## Related declarations

## Import using

- imported by default

## guard_target

`guard_target t`

fails if the target of the main goal is not `t`

.
We use this tactic for writing tests.

## Related declarations

## Import using

- imported by default

## guard_target'

`guard_target' t`

fails if the target of the main goal is not definitionally equal to `t`

.
We use this tactic for writing tests.
The difference with `guard_target`

is that this uses definitional equality instead of
alpha-equivalence.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## h_generalize

`h_generalize Hx : e == x`

matches on `cast _ e`

in the goal and replaces it with
`x`

. It also adds `Hx : e == x`

as an assumption. If `cast _ e`

appears multiple
times (not necessarily with the same proof), they are all replaced by `x`

. `cast`

`eq.mp`

, `eq.mpr`

, `eq.subst`

, `eq.substr`

, `eq.rec`

and `eq.rec_on`

are all treated
as casts.

`h_generalize Hx : e == x with h`

adds hypothesis`α = β`

with`e : α, x : β`

;`h_generalize Hx : e == x with _`

chooses automatically chooses the name of assumption`α = β`

;`h_generalize! Hx : e == x`

reverts`Hx`

;- when
`Hx`

is omitted, assumption`Hx : e == x`

is not added.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## have

`have h : t := p`

adds the hypothesis `h : t`

to the current goal if `p`

a term of type `t`

. If `t`

is omitted, it will be inferred.

`have h : t`

adds the hypothesis `h : t`

to the current goal and opens a new subgoal with target `t`

. The new subgoal becomes the main goal. If `t`

is omitted, it will be replaced by a fresh metavariable.

If `h`

is omitted, the name `this`

is used.

## Related declarations

## Import using

- imported by default

## hint

`hint`

lists possible tactics which will make progress (that is, not fail) against the current goal.

```
example {P Q : Prop} (p : P) (h : P → Q) : Q :=
begin
hint,
/- the following tactics make progress:
----
Try this: solve_by_elim
Try this: finish
Try this: tauto
-/
solve_by_elim,
end
```

You can add a tactic to the list that `hint`

tries by either using

`attribute [hint_tactic] my_tactic`

, if`my_tactic`

is already of type`tactic string`

(`tactic unit`

is allowed too, in which case the printed string will be the name of the tactic), or`add_hint_tactic "my_tactic"`

, specifying a string which works as an interactive tactic.

## Related declarations

## Import using

- import tactic.hint
- import tactic.basic

## induction

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

ire chosen automatically.

`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 with y₁ ... yₙ`

, where `e`

is a variable or an expression, specifies that the sequence of names `y₁ ... yₙ`

should be used for the arguments to the constructors and inductive hypotheses, including implicit arguments. If the list does not include enough names for all of the arguments, additional names are generated automatically. If too many names are given, the extra ones are ignored. Underscores can be used in the list, in which case the corresponding names are generated automatically. Note that for long sequences of names, the `case`

tactic provides a more convenient naming mechanism.

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

`induction h : t`

will introduce an equality of the form `h : t = C x y`

, asserting that the input term is equal to the current constructor case, to the context.

## Related declarations

## Import using

- imported by default

## inhabit

`inhabit α`

tries to derive a `nonempty α`

instance and then upgrades this
to an `inhabited α`

instance.
If the target is a `Prop`

, this is done constructively;
otherwise, it uses `classical.choice`

.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## injection

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.

## Related declarations

## Import using

- imported by default

## injections

`injections with h₁ ... hₙ`

iteratively applies `injection`

to hypotheses using the names `h₁ ... hₙ`

.

## Related declarations

## Import using

- imported by default

## injections_and_clear

Calls `injection`

on each hypothesis, and then, for each hypothesis on which `injection`

succeeds, clears the old hypothesis.

## Related declarations

## Import using

- import tactic.core
- import tactic.basic

## interval_cases

`interval_cases n`

searches for upper and lower bounds on a variable `n`

,
and if bounds are found,
splits into separate cases for each possible value of `n`

.

As an example, in

```
example (n : ℕ) (w₁ : n ≥ 3) (w₂ : n < 5) : n = 3 ∨ n = 4 :=
begin
interval_cases n,
all_goals {simp}
end
```

after `interval_cases n`

, the goals are `3 = 3 ∨ 3 = 4`

and `4 = 3 ∨ 4 = 4`

.

You can also explicitly specify a lower and upper bound to use,
as `interval_cases using hl hu`

.
The hypotheses should be in the form `hl : a ≤ n`

and `hu : n < b`

,
in which case `interval_cases`

calls `fin_cases`

on the resulting fact `n ∈ set.Ico a b`

.

You can also explicitly specify a name to use for the hypothesis added,
as `interval_cases n with hn`

or `interval_cases n using hl hu with hn`

.

In particular, `interval_cases n`

1) inspects hypotheses looking for lower and upper bounds of the form `a ≤ n`

and `n < b`

(although in `ℕ`

, `ℤ`

, and `ℕ+`

bounds of the form `a < n`

and `n ≤ b`

are also allowed),
and also makes use of lower and upper bounds found via `le_top`

and `bot_le`

(so for example if `n : ℕ`

, then the bound `0 ≤ n`

is found automatically), then
2) calls `fin_cases`

on the synthesised hypothesis `n ∈ set.Ico a b`

,
assuming an appropriate `fintype`

instance can be found for the type of `n`

.

The variable `n`

can belong to any type `α`

, with the following restrictions:

- only bounds on which
`expr.to_rat`

succeeds will be considered "explicit" (TODO: generalise this?) - an instance of
`decidable_eq α`

is available, - an explicit lower bound can be found amongst the hypotheses, or from
`bot_le n`

, - an explicit upper bound can be found amongst the hypotheses, or from
`le_top n`

, - if multiple bounds are located, an instance of
`linear_order α`

is available, and - an instance of
`fintype set.Ico l u`

is available for the relevant bounds.

## Related declarations

## Import using

- import tactic.interval_cases
- import tactic

## intro / intros

If the current goal is a Pi/forall `∀ x : t, u`

(resp. `let x := t in u`

) then `intro`

puts
`x : t`

(resp. `x := t`

) in the local context. The new subgoal target is `u`

.

If the goal is an arrow `t → u`

, then it puts `h : t`

in the local context and the new goal
target is `u`

.

If the goal is neither a Pi/forall nor begins with a let binder, the tactic `intro`

applies the
tactic `whnf`

until an introduction can be applied or the goal is not head reducible. In the latter
case, the tactic fails.

The variant `intro z`

uses the identifier `z`

to name the new hypothesis.

The variant `intros`

will keep introducing new hypotheses until the goal target is not a Pi/forall
or let binder.

The variant `intros h₁ ... hₙ`

introduces `n`

new hypotheses using the given identifiers to name
them.

## Related declarations

## Import using

- imported by default

## introv

The tactic `introv`

allows the user to automatically introduce the variables of a theorem and explicitly name the hypotheses involved. The given names are used to name non-dependent hypotheses.

Examples:

```
example : ∀ a b : nat, a = b → b = a :=
begin
introv h,
exact h.symm
end
```

The state after `introv h`

is

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

```
example : ∀ a b : nat, a = b → ∀ c, b = c → a = c :=
begin
introv h₁ h₂,
exact h₁.trans h₂
end
```

The state after `introv h₁ h₂`

is

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

## Related declarations

## Import using

- imported by default

## iterate

`iterate { t }`

repeatedly applies tactic `t`

until `t`

fails. `iterate { t }`

always succeeds.

`iterate n { t }`

applies `t`

`n`

times.

## Related declarations

## Import using

- imported by default

## left / right

`left`

applies the first constructor when the type of the target is an inductive data type with
two constructors.

Similarly, `right`

applies the second constructor.

## Related declarations

## Import using

- imported by default

## let

`let h : t := p`

adds the hypothesis `h : t := p`

to the current goal if `p`

a term of type `t`

.
If `t`

is omitted, it will be inferred.

`let h : t`

adds the hypothesis `h : t := ?M`

to the current goal and opens a new subgoal `?M : t`

.
The new subgoal becomes the main goal. If `t`

is omitted, it will be replaced by a fresh
metavariable.

If `h`

is omitted, the name `this`

is used.

Note the related mathlib tactic `set a := t with h`

, which adds the hypothesis `h : a = t`

to
the local context and replaces `t`

with `a`

everywhere it can.

## Related declarations

## Import using

- imported by default

## library_search

`library_search`

is a tactic to identify existing lemmas in the library. It tries to close the
current goal by applying a lemma from the library, then discharging any new goals using
`solve_by_elim`

.

Typical usage is:

```
example (n m k : ℕ) : n * (m - k) = n * m - n * k :=
by library_search -- Try this: exact nat.mul_sub_left_distrib n m k
```

`library_search`

prints a trace message showing the proof it found, shown above as a comment.
Typically you will then copy and paste this proof, replacing the call to `library_search`

.

## Related declarations

## Import using

- import tactic.suggest
- import tactic.basic

## lift

Lift an expression to another type.

Lift an expression to another type.

- Usage:
`'lift' expr 'to' expr ('using' expr)? ('with' id (id id?)?)?`

. - If
`n : ℤ`

and`hn : n ≥ 0`

then the tactic`lift n to ℕ using hn`

creates a new constant of type`ℕ`

, also named`n`

and replaces all occurrences of the old variable`(n : ℤ)`

with`↑n`

(where`n`

in the new variable). It will remove`n`

and`hn`

from the context.- So for example the tactic
`lift n to ℕ using hn`

transforms the goal`n : ℤ, hn : n ≥ 0, h : P n ⊢ n = 3`

to`n : ℕ, h : P ↑n ⊢ ↑n = 3`

(here`P`

is some term of type`ℤ → Prop`

).

- So for example the tactic
- The argument
`using hn`

is optional, the tactic`lift n to ℕ`

does the same, but also creates a new subgoal that`n ≥ 0`

(where`n`

is the old variable).- So for example the tactic
`lift n to ℕ`

transforms the goal`n : ℤ, h : P n ⊢ n = 3`

to two goals`n : ℕ, h : P ↑n ⊢ ↑n = 3`

and`n : ℤ, h : P n ⊢ n ≥ 0`

.

- So for example the tactic
- You can also use
`lift n to ℕ using e`

where`e`

is any expression of type`n ≥ 0`

. - Use
`lift n to ℕ with k`

to specify the name of the new variable. - Use
`lift n to ℕ with k hk`

to also specify the name of the equality`↑k = n`

. In this case,`n`

will remain in the context. You can use`rfl`

for the name of`hk`

to substitute`n`

away (i.e. the default behavior). - You can also use
`lift e to ℕ with k hk`

where`e`

is any expression of type`ℤ`

. In this case, the`hk`

will always stay in the context, but it will be used to rewrite`e`

in all hypotheses and the target.- So for example the tactic
`lift n + 3 to ℕ using hn with k hk`

transforms the goal`n : ℤ, hn : n + 3 ≥ 0, h : P (n + 3) ⊢ n + 3 = 2 * n`

to the goal`n : ℤ, k : ℕ, hk : ↑k = n + 3, h : P ↑k ⊢ ↑k = 2 * n`

.

- So for example the tactic
- The tactic
`lift n to ℕ using h`

will remove`h`

from the context. If you want to keep it, specify it again as the third argument to`with`

, like this:`lift n to ℕ using h with n rfl h`

. - More generally, this can lift an expression from
`α`

to`β`

assuming that there is an instance of`can_lift α β`

. In this case the proof obligation is specified by`can_lift.cond`

. - Given an instance
`can_lift β γ`

, it can also lift`α → β`

to`α → γ`

; more generally, given`β : Π a : α, Type*`

,`γ : Π a : α, Type*`

, and`[Π a : α, can_lift (β a) (γ a)]`

, it automatically generates an instance`can_lift (Π a, β a) (Π a, γ a)`

.

`lift`

is in some sense dual to the `zify`

tactic. `lift (z : ℤ) to ℕ`

will change the type of an
integer `z`

(in the supertype) to `ℕ`

(the subtype), given a proof that `z ≥ 0`

;
propositions concerning `z`

will still be over `ℤ`

. `zify`

changes propositions about `ℕ`

(the
subtype) to propositions about `ℤ`

(the supertype), without changing the type of any variable.

## Related declarations

## Import using

- import tactic.lift
- import tactic.basic

## linarith

`linarith`

attempts to find a contradiction between hypotheses that are linear (in)equalities.
Equivalently, it can prove a linear inequality by assuming its negation and proving `false`

.

In theory, `linarith`

should prove any goal that is true in the theory of linear arithmetic over
the rationals. While there is some special handling for non-dense orders like `nat`

and `int`

,
this tactic is not complete for these theories and will not prove every true goal. It will solve
goals over arbitrary types that instantiate `linear_ordered_comm_ring`

.

An example:

```
example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
(h3 : 12*y - 4* z < 0) : false :=
by linarith
```

`linarith`

will use all appropriate hypotheses and the negation of the goal, if applicable.

`linarith [t1, t2, t3]`

will additionally use proof terms `t1, t2, t3`

.

`linarith only [h1, h2, h3, t1, t2, t3]`

will use only the goal (if relevant), local hypotheses
`h1`

, `h2`

, `h3`

, and proofs `t1`

, `t2`

, `t3`

. It will ignore the rest of the local context.

`linarith!`

will use a stronger reducibility setting to try to identify atoms. For example,

```
example (x : ℚ) : id x ≥ x :=
by linarith
```

will fail, because `linarith`

will not identify `x`

and `id x`

. `linarith!`

will.
This can sometimes be expensive.

`linarith {discharger := tac, restrict_type := tp, exfalso := ff}`

takes a config object with five
optional arguments:

`discharger`

specifies a tactic to be used for reducing an algebraic equation in the proof stage. The default is`ring`

. Other options currently include`ring SOP`

or`simp`

for basic problems.`restrict_type`

will only use hypotheses that are inequalities over`tp`

. This is useful if you have e.g. both integer and rational valued inequalities in the local context, which can sometimes confuse the tactic.`transparency`

controls how hard`linarith`

will try to match atoms to each other. By default it will only unfold`reducible`

definitions.- If
`split_hypotheses`

is true,`linarith`

will split conjunctions in the context into separate hypotheses. - If
`exfalso`

is false,`linarith`

will fail when the goal is neither an inequality nor`false`

. (True by default.)

A variant, `nlinarith`

, does some basic preprocessing to handle some nonlinear goals.

The option `set_option trace.linarith true`

will trace certain intermediate stages of the `linarith`

routine.

## Related declarations

## Import using

- import tactic.linarith.frontend
- import tactic

## mapply

Similar to the `apply`

tactic, but uses matching instead of unification.
`apply_match t`

is equivalent to `apply_with t {unify := ff}`

## Related declarations

## Import using

- imported by default

## match_target

`match_target t`

fails if target does not match pattern `t`

.

## Related declarations

## Import using

- imported by default

## mono

`mono`

applies a monotonicity rule.`mono*`

applies monotonicity rules repetitively.`mono with x ≤ y`

or`mono with [0 ≤ x,0 ≤ y]`

creates an assertion for the listed propositions. Those help to select the right monotonicity rule.`mono left`

or`mono right`

is useful when proving strict orderings: for`x + y < w + z`

could be broken down into either- left:
`x ≤ w`

and`y < z`

or - right:
`x < w`

and`y ≤ z`

- left:
`mono using [rule1,rule2]`

calls`simp [rule1,rule2]`

before applying mono.- The general syntax is `mono '*'? ('with' hyp | 'with' [hyp1,hyp2])? ('using' [hyp1,hyp2])? mono_cfg?

To use it, first import `tactic.monotonicity`

.

Here is an example of mono:

```
example (x y z k : ℤ)
(h : 3 ≤ (4 : ℤ))
(h' : z ≤ y) :
(k + 3 + x) - y ≤ (k + 4 + x) - z :=
begin
mono, -- unfold `(-)`, apply add_le_add
{ -- ⊢ k + 3 + x ≤ k + 4 + x
mono, -- apply add_le_add, refl
-- ⊢ k + 3 ≤ k + 4
mono },
{ -- ⊢ -y ≤ -z
mono /- apply neg_le_neg -/ }
end
```

More succinctly, we can prove the same goal as:

```
example (x y z k : ℤ)
(h : 3 ≤ (4 : ℤ))
(h' : z ≤ y) :
(k + 3 + x) - y ≤ (k + 4 + x) - z :=
by mono*
```

## Related declarations

## Import using

- import tactic.monotonicity.interactive
- import tactic

## nlinarith

An extension of `linarith`

with some preprocessing to allow it to solve some nonlinear arithmetic
problems. (Based on Coq's `nra`

tactic.) See `linarith`

for the available syntax of options,
which are inherited by `nlinarith`

; that is, `nlinarith!`

and `nlinarith only [h1, h2]`

all work as
in `linarith`

. The preprocessing is as follows:

- For every subterm
`a ^ 2`

or`a * a`

in a hypothesis or the goal, the assumption`0 ≤ a ^ 2`

or`0 ≤ a * a`

is added to the context. - For every pair of hypotheses
`a1 R1 b1`

,`a2 R2 b2`

in the context,`R1, R2 ∈ {<, ≤, =}`

, the assumption`0 R' (b1 - a1) * (b2 - a2)`

is added to the context (non-recursively), where`R ∈ {<, ≤, =}`

is the appropriate comparison derived from`R1, R2`

.

## Related declarations

## Import using

- import tactic.linarith.frontend
- import tactic

## noncomm_ring

A tactic for simplifying identities in not-necessarily-commutative rings.

An example:

```
example {R : Type*} [ring R] (a b c : R) : a * (b + c + c - b) = 2*a*c :=
by noncomm_ring
```

## Related declarations

## Import using

- import tactic.noncomm_ring
- import tactic

## nontriviality

Attempts to generate a `nontrivial α`

hypothesis.

The tactic first looks for an instance using `apply_instance`

.

If the goal is an (in)equality, the type `α`

is inferred from the goal.
Otherwise, the type needs to be specified in the tactic invocation, as `nontriviality α`

.

The `nontriviality`

tactic will first look for strict inequalities amongst the hypotheses,
and use these to derive the `nontrivial`

instance directly.

Otherwise, it will perform a case split on `subsingleton α ∨ nontrivial α`

, and attempt to discharge
the `subsingleton`

goal using `simp [lemmas] with nontriviality`

, where `[lemmas]`

is a list of
additional `simp`

lemmas that can be passed to `nontriviality`

using the syntax
`nontriviality α using [lemmas]`

.

```
example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : 0 < a :=
begin
nontriviality, -- There is now a `nontrivial R` hypothesis available.
assumption,
end
```

```
example {R : Type} [comm_ring R] {r s : R} : r * s = s * r :=
begin
nontriviality, -- There is now a `nontrivial R` hypothesis available.
apply mul_comm,
end
```

```
example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : (2 : ℕ) ∣ 4 :=
begin
nontriviality R, -- there is now a `nontrivial R` hypothesis available.
dec_trivial
end
```

```
def myeq {α : Type} (a b : α) : Prop := a = b
example {α : Type} (a b : α) (h : a = b) : myeq a b :=
begin
success_if_fail { nontriviality α }, -- Fails
nontriviality α using [myeq], -- There is now a `nontrivial α` hypothesis available
assumption
end
```

## Related declarations

## Import using

- import logic.nontrivial
- import tactic

## norm_cast

The `norm_cast`

family of tactics is used to normalize casts inside expressions.
It is basically a simp tactic with a specific set of lemmas to move casts
upwards in the expression.
Therefore it can be used more safely as a non-terminating tactic.
It also has special handling of numerals.

For instance, given an assumption

```
a b : ℤ
h : ↑a + ↑b < (10 : ℚ)
```

writing `norm_cast at h`

will turn `h`

into

```
h : a + b < 10
```

You can also use `exact_mod_cast`

, `apply_mod_cast`

, `rw_mod_cast`

or `assumption_mod_cast`

.
Writing `exact_mod_cast h`

and `apply_mod_cast h`

will normalize the goal and
`h`

before using `exact h`

or `apply h`

.
Writing `assumption_mod_cast`

will normalize the goal and for every
expression `h`

in the context it will try to normalize `h`

and use
`exact h`

.
`rw_mod_cast`

acts like the `rw`

tactic but it applies `norm_cast`

between steps.

`push_cast`

rewrites the expression to move casts toward the leaf nodes.
This uses `norm_cast`

lemmas in the forward direction.
For example, `↑(a + b)`

will be written to `↑a + ↑b`

.
It is equivalent to `simp only with push_cast`

.
It can also be used at hypotheses with `push_cast at h`

and with extra simp lemmas with `push_cast [int.add_zero]`

.

```
example (a b : ℕ) (h1 : ((a + b : ℕ) : ℤ) = 10) (h2 : ((a + b + 0 : ℕ) : ℤ) = 10) :
((a + b : ℕ) : ℤ) = 10 :=
begin
push_cast,
push_cast at h1,
push_cast [int.add_zero] at h2,
end
```

The implementation and behavior of the `norm_cast`

family is described in detail at
https://lean-forward.github.io/norm_cast/norm_cast.pdf.

## Related declarations

## Import using

- import tactic.norm_cast
- import tactic.basic

## norm_digits

A tactic for normalizing expressions of the form `nat.digits a b = l`

where
`a`

and `b`

are numerals.

```
example : nat.digits 10 123 = [3,2,1] := by norm_digits
```

## Related declarations

## Import using

- import data.nat.digits

## norm_num

Normalises numerical expressions. It supports the operations `+`

`-`

`*`

`/`

`^`

and `%`

over
numerical types such as `ℕ`

, `ℤ`

, `ℚ`

, `ℝ`

, `ℂ`

, and can prove goals of the form `A = B`

, `A ≠ B`

,
`A < B`

and `A ≤ B`

, where `A`

and `B`

are
numerical expressions. It also has a relatively simple primality prover.

```
import data.real.basic
example : (2 : ℝ) + 2 = 4 := by norm_num
example : (12345.2 : ℝ) ≠ 12345.3 := by norm_num
example : (73 : ℝ) < 789/2 := by norm_num
example : 123456789 + 987654321 = 1111111110 := by norm_num
example (R : Type*) [ring R] : (2 : R) + 2 = 4 := by norm_num
example (F : Type*) [linear_ordered_field F] : (2 : F) + 2 < 5 := by norm_num
example : nat.prime (2^13 - 1) := by norm_num
example : ¬ nat.prime (2^11 - 1) := by norm_num
example (x : ℝ) (h : x = 123 + 456) : x = 579 := by norm_num at h; assumption
```

The variant `norm_num1`

does not call `simp`

.

Both `norm_num`

and `norm_num1`

can be called inside the `conv`

tactic.

The tactic `apply_normed`

normalises a numerical expression and tries to close the goal with
the result. Compare:

```
def a : ℕ := 2^100
#print a -- 2 ^ 100
def normed_a : ℕ := by apply_normed 2^100
#print normed_a -- 1267650600228229401496703205376
```

## Related declarations

## Import using

- import tactic.norm_num
- import tactic

## nth_rewrite / nth_rewrite_lhs / nth_rewrite_rhs

`nth_rewrite n rules`

performs only the `n`

th possible rewrite using the `rules`

.
The tactics `nth_rewrite_lhs`

and `nth_rewrite_rhs`

are variants
that operate on the left and right hand sides of an equation or iff.

Note: `n`

is zero-based, so `nth_rewrite 0 h`

will rewrite along `h`

at the first possible location.

In more detail, given `rules = [h1, ..., hk]`

,
this tactic will search for all possible locations
where one of `h1, ..., hk`

can be rewritten,
and perform the `n`

th occurrence.

Example: Given a goal of the form `a + x = x + b`

, and hypothesis `h : x = y`

,
the tactic `nth_rewrite 1 h`

will change the goal to `a + x = y + b`

.

The core `rewrite`

has a `occs`

configuration setting intended to achieve a similar
purpose, but this doesn't really work. (If a rule matches twice, but with different
values of arguments, the second match will not be identified.)

## Related declarations

## Import using

- import tactic.nth_rewrite.default
- import tactic

## obtain

The `obtain`

tactic is a combination of `have`

and `rcases`

. See `rcases`

for
a description of supported patterns.

```
obtain ⟨patt⟩ : type,
{ ... }
```

is equivalent to

```
have h : type,
{ ... },
rcases h with ⟨patt⟩
```

The syntax `obtain ⟨patt⟩ : type := proof`

is also supported.

If `⟨patt⟩`

is omitted, `rcases`

will try to infer the pattern.

If `type`

is omitted, `:= proof`

is required.

## Related declarations

## Import using

- import tactic.rcases
- import tactic.basic

## omega

`omega`

attempts to discharge goals in the quantifier-free fragment of linear integer and natural
number arithmetic using the Omega test. In other words, the core procedure of `omega`

works with
goals of the form

```
∀ x₁, ... ∀ xₖ, P
```

where `x₁, ... xₖ`

are integer (resp. natural number) variables, and `P`

is a quantifier-free
formula of linear integer (resp. natural number) arithmetic. For instance:

```
example : ∀ (x y : int), (x ≤ 5 ∧ y ≤ 3) → x + y ≤ 8 := by omega
```

By default, `omega`

tries to guess the correct domain by looking at the goal and hypotheses, and
then reverts all relevant hypotheses and variables (e.g., all variables of type `nat`

and `Prop`

s
in linear natural number arithmetic, if the domain was determined to be `nat`

) to universally close
the goal before calling the main procedure. Therefore, `omega`

will often work even if the goal
is not in the above form:

But this behaviour is not always optimal, since it may revert irrelevant hypotheses or incorrectly
guess the domain. Use `omega manual`

to disable automatic reverts, and `omega int`

or `omega nat`

to specify the domain.

```
example (x y z w : int) (h1 : 3 * y ≥ x) (h2 : z > 19 * w) : 3 * x ≤ 9 * y :=
by {revert h1 x y, omega manual}
example (i : int) (n : nat) (h1 : i = 0) (h2 : n < n) : false := by omega nat
example (n : nat) (h1 : n < 34) (i : int) (h2 : i * 9 = -72) : i = -8 :=
by {revert h2 i, omega manual int}
```

`omega`

handles `nat`

subtraction by repeatedly rewriting goals of the form `P[t-s]`

into
`P[x] ∧ (t = s + x ∨ (t ≤ s ∧ x = 0))`

, where `x`

is fresh. This means that each (distinct)
occurrence of subtraction will cause the goal size to double during DNF transformation.

`omega`

implements the real shadow step of the Omega test, but not the dark and gray shadows.
Therefore, it should (in principle) succeed whenever the negation of the goal has no real solution,
but it may fail if a real solution exists, even if there is no integer/natural number solution.

You can enable `set_option trace.omega true`

to see how `omega`

interprets your goal.

## Related declarations

## Import using

- import tactic.omega.main
- import tactic

## pi_instance

`pi_instance`

constructs an instance of `my_class (Π i : I, f i)`

where we know `Π i, my_class (f i)`

. If an order relation is required,
it defaults to `pi.partial_order`

. Any field of the instance that
`pi_instance`

cannot construct is left untouched and generated as a new goal.

## Related declarations

## Import using

- import tactic.pi_instances
- import tactic

## pretty_cases

Query the proof goal and print the skeleton of a proof by cases.

For example, let us consider the following proof:

```
example {α} (xs ys : list α) (h : xs ~ ys) : true :=
begin
induction h,
pretty_cases,
-- Try this:
-- case list.perm.nil :
-- { admit },
-- case list.perm.cons : h_x h_l₁ h_l₂ h_a h_ih
-- { admit },
-- case list.perm.swap : h_x h_y h_l
-- { admit },
-- case list.perm.trans : h_l₁ h_l₂ h_l₃ h_a h_a_1 h_ih_a h_ih_a_1
-- { admit },
end
```

The output helps the user layout the cases and rename the introduced variables.

## Related declarations

## Import using

- import tactic.pretty_cases
- import tactic.basic

## push_neg

Push negations in the goal of some assumption.

For instance, a hypothesis `h : ¬ ∀ x, ∃ y, x ≤ y`

will be transformed by `push_neg at h`

into
`h : ∃ x, ∀ y, y < x`

. Variables names are conserved.

This tactic pushes negations inside expressions. For instance, given an assumption

```
h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)
```

writing `push_neg at h`

will turn `h`

into

```
h : ∃ ε, ε > 0 ∧ ∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
```

(the pretty printer does *not* use the abreviations `∀ δ > 0`

and `∃ ε > 0`

but this issue
has nothing to do with `push_neg`

).
Note that names are conserved by this tactic, contrary to what would happen with `simp`

using the relevant lemmas. One can also use this tactic at the goal using `push_neg`

,
at every assumption and the goal using `push_neg at *`

or at selected assumptions and the goal
using say `push_neg at h h' ⊢`

as usual.

## Related declarations

## Import using

- import tactic.push_neg
- import tactic.basic

## rcases

`rcases`

is a tactic that will perform `cases`

recursively, according to a pattern. It is used to
destructure hypotheses or expressions composed of inductive types like `h1 : a ∧ b ∧ c ∨ d`

or
`h2 : ∃ x y, trans_rel R x y`

. Usual usage might be `rcases h1 with ⟨ha, hb, hc⟩ | hd`

or
`rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩`

for these examples.

Each element of an `rcases`

pattern is matched against a particular local hypothesis (most of which
are generated during the execution of `rcases`

and represent individual elements destructured from
the input expression). An `rcases`

pattern has the following grammar:

- A name like
`x`

, which names the active hypothesis as`x`

. - A blank
`_`

, which does nothing (letting the automatic naming system used by`cases`

name the hypothesis). - A hyphen
`-`

, which clears the active hypothesis and any dependents. - The keyword
`rfl`

, which expects the hypothesis to be`h : a = b`

, and calls`subst`

on the hypothesis (which has the effect of replacing`b`

with`a`

everywhere or vice versa). - A type ascription
`p : ty`

, which sets the type of the hypothesis to`ty`

and then matches it against`p`

. (Of course,`ty`

must unify with the actual type of`h`

for this to work.) - A tuple pattern
`⟨p1, p2, p3⟩`

, which matches a constructor with many arguments, or a series of nested conjunctions or existentials. For example if the active hypothesis is`a ∧ b ∧ c`

, then the conjunction will be destructured, and`p1`

will be matched against`a`

,`p2`

against`b`

and so on. - An alteration pattern
`p1 | p2 | p3`

, which matches an inductive type with multiple constructors, or a nested disjunction like`a ∨ b ∨ c`

.

A pattern like `⟨a, b, c⟩ | ⟨d, e⟩`

will do a split over the inductive datatype,
naming the first three parameters of the first constructor as `a,b,c`

and the
first two of the second constructor `d,e`

. If the list is not as long as the
number of arguments to the constructor or the number of constructors, the
remaining variables will be automatically named. If there are nested brackets
such as `⟨⟨a⟩, b | c⟩ | d`

then these will cause more case splits as necessary.
If there are too many arguments, such as `⟨a, b, c⟩`

for splitting on
`∃ x, ∃ y, p x`

, then it will be treated as `⟨a, ⟨b, c⟩⟩`

, splitting the last
parameter as necessary.

`rcases`

also has special support for quotient types: quotient induction into Prop works like
matching on the constructor `quot.mk`

.

`rcases h : e with PAT`

will do the same as `rcases e with PAT`

with the exception that an assumption
`h : e = PAT`

will be added to the context.

`rcases? e`

will perform case splits on `e`

in the same way as `rcases e`

,
but rather than accepting a pattern, it does a maximal cases and prints the
pattern that would produce this case splitting. The default maximum depth is 5,
but this can be modified with `rcases? e : n`

.

## Related declarations

## Import using

- import tactic.rcases
- import tactic.basic

## refine

This tactic behaves like `exact`

, but with a big difference: the user can put underscores `_`

in the expression as placeholders for holes that need to be filled, and `refine`

will generate as many subgoals as there are holes.

Note that some holes may be implicit. The type of each hole must either be synthesized by the system or declared by an explicit type ascription like `(_ : nat → Prop)`

.

## Related declarations

## Import using

- imported by default

## refine_struct

`refine_struct { .. }`

acts like `refine`

but works only with structure instance
literals. It creates a goal for each missing field and tags it with the name of the
field so that `have_field`

can be used to generically refer to the field currently
being refined.

As an example, we can use `refine_struct`

to automate the construction semigroup
instances:

```
refine_struct ( { .. } : semigroup α ),
-- case semigroup, mul
-- α : Type u,
-- ⊢ α → α → α
-- case semigroup, mul_assoc
-- α : Type u,
-- ⊢ ∀ (a b c : α), a * b * c = a * (b * c)
```

`have_field`

, used after `refine_struct _`

, poses `field`

as a local constant
with the type of the field of the current goal:

```
refine_struct ({ .. } : semigroup α),
{ have_field, ... },
{ have_field, ... },
```

behaves like

```
refine_struct ({ .. } : semigroup α),
{ have field := @semigroup.mul, ... },
{ have field := @semigroup.mul_assoc, ... },
```

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## refl / reflexivity

This tactic applies to a goal whose target has the form `t ~ u`

where `~`

is a reflexive relation,
that is, a relation which has a reflexivity lemma tagged with the attribute `[refl]`

.
The tactic checks whether `t`

and `u`

are definitionally equal and then solves the goal.

## Related declarations

## Import using

- imported by default

## rename

Rename one or more local hypotheses. The renamings are given as follows:

```
rename x y -- rename x to y
rename x → y -- ditto
rename [x y, a b] -- rename x to y and a to b
rename [x → y, a → b] -- ditto
```

Note that if there are multiple hypotheses called `x`

in the context, then
`rename x y`

will rename *all* of them. If you want to rename only one, use
`dedup`

first.

## Related declarations

## Import using

- imported by default

## rename_var

`rename_var old new`

renames all bound variables named `old`

to `new`

in the goal.
`rename_var old new at h`

does the same in hypothesis `h`

.
This is meant for teaching bound variables only. Such a renaming should never be relevant to Lean.

```
example (P : ℕ → ℕ → Prop) (h : ∀ n, ∃ m, P n m) : ∀ l, ∃ m, P l m :=
begin
rename_var n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
rename_var m n, -- goal is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
exact h -- Lean does not care about those bound variable names
end
```

## Related declarations

## Import using

- import tactic.rename_var
- import tactic.basic

## repeat

`repeat { t }`

applies `t`

to each goal. If the application succeeds,
the tactic is applied recursively to all the generated subgoals until it eventually fails.
The recursion stops in a subgoal when the tactic has failed to make progress.
The tactic `repeat { t }`

never fails.

## Related declarations

## Import using

- imported by default

## replace

Acts like `have`

, but removes a hypothesis with the same name as
this one. For example if the state is `h : p ⊢ goal`

and `f : p → q`

,
then after `replace h := f h`

the goal will be `h : q ⊢ goal`

,
where `have h := f h`

would result in the state `h : p, h : q ⊢ goal`

.
This can be used to simulate the `specialize`

and `apply at`

tactics
of Coq.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## revert

`revert h₁ ... hₙ`

applies to any goal with hypotheses `h₁`

... `hₙ`

. It moves the hypotheses and their dependencies to the target of the goal. This tactic is the inverse of `intro`

.

## Related declarations

## Import using

- imported by default

## revert_after

`revert_after n`

reverts all the hypotheses after `n`

.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## revert_deps

`revert_deps n₁ n₂ ...`

reverts all the hypotheses that depend on one of `n₁, n₂, ...`

It does not revert `n₁, n₂, ...`

themselves (unless they depend on another `nᵢ`

).

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## revert_target_deps

Reverts all local constants on which the target depends (recursively).

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## ring

Tactic for solving equations in the language of *commutative* (semi)rings.
Attempts to prove the goal outright if there is no `at`

specifier and the target is an equality, but if this
fails it falls back to rewriting all ring expressions
into a normal form. When writing a normal form,
`ring SOP`

will use sum-of-products form instead of horner form.
`ring!`

will use a more aggressive reducibility setting to identify atoms.

Based on Proving Equalities in a Commutative Ring Done Right in Coq by Benjamin Grégoire and Assia Mahboubi.

## Related declarations

## Import using

- import tactic.ring
- import tactic

## ring2

`ring2`

solves equations in the language of rings.

It supports only the commutative semiring operations, i.e. it does not normalize subtraction or division.

This variant on the `ring`

tactic uses kernel computation instead
of proof generation. In general, you should use `ring`

instead of `ring2`

.

## Related declarations

## Import using

- import tactic.ring2

## ring_exp

Tactic for evaluating expressions in *commutative* (semi)rings, allowing for variables in the
exponent.

This tactic extends `ring`

: it should solve every goal that `ring`

can solve.
Additionally, it knows how to evaluate expressions with complicated exponents
(where `ring`

only understands constant exponents).
The variants `ring_exp!`

and `ring_exp_eq!`

use a more aggessive reducibility setting to determine
equality of atoms.

For example:

```
example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring_exp
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring_exp
example (x y : ℕ) : x + id y = y + id x := by ring_exp!
```

## Related declarations

## Import using

- import tactic.ring_exp
- import tactic

## rintro

The `rintro`

tactic is a combination of the `intros`

tactic with `rcases`

to
allow for destructuring patterns while introducing variables. See `rcases`

for
a description of supported patterns. For example, `rintro (a | ⟨b, c⟩) ⟨d, e⟩`

will introduce two variables, and then do case splits on both of them producing
two subgoals, one with variables `a d e`

and the other with `b c d e`

.

`rintro`

, unlike `rcases`

, also supports the form `(x y : ty)`

for introducing
and type-ascripting multiple variables at once, similar to binders.

`rintro?`

will introduce and case split on variables in the same way as
`rintro`

, but will also print the `rintro`

invocation that would have the same
result. Like `rcases?`

, `rintro? : n`

allows for modifying the
depth of splitting; the default is 5.

`rintros`

is an alias for `rintro`

.

## Related declarations

## Import using

- import tactic.rcases
- import tactic.basic

## rotate

`rotate`

moves the first goal to the back. `rotate n`

will do this `n`

times.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## rw / rewrite

`rw e`

applies an equation or iff `e`

as a rewrite rule to 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 lemmas associated with `e`

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

.

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

applies the given rules sequentially.

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

`rewrite`

is synonymous with `rw`

.

## Related declarations

## Import using

- imported by default

## scc

`scc`

uses the available equivalences and implications to prove
a goal of the form `p ↔ q`

.

```
example (p q r : Prop) (hpq : p → q) (hqr : q ↔ r) (hrp : r → p) : p ↔ r :=
by scc
```

The variant `scc'`

populates the local context with all equivalences that `scc`

is able to prove.
This is mostly useful for testing purposes.

## Related declarations

## Import using

- import tactic.scc
- import tactic

## set

`set a := t with h`

is a variant of `let a := t`

. It adds the hypothesis `h : a = t`

to
the local context and replaces `t`

with `a`

everywhere it can.

`set a := t with ←h`

will add `h : t = a`

instead.

`set! a := t with h`

does not do any replacing.

```
example (x : ℕ) (h : x = 3) : x + x + x = 9 :=
begin
set y := x with ←h_xy,
/-
x : ℕ,
y : ℕ := x,
h_xy : x = y,
h : y = 3
⊢ y + y + y = 9
-/
end
```

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## show

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

.

## Related declarations

## Import using

- imported by default

## show_term

`show_term { tac }`

runs the tactic `tac`

,
and then prints the term that was constructed.

This is useful for

- constructing term mode proofs from tactic mode proofs, and
- understanding what tactics are doing, and how metavariables are handled.

As an example, in

```
example {P Q R : Prop} (h₁ : Q → P) (h₂ : R) (h₃ : R → Q) : P ∧ R :=
by show_term { tauto }
```

the term mode proof `⟨h₁ (h₃ h₂), eq.mpr rfl h₂⟩`

produced by `tauto`

will be printed.

As another example, if the goal is `ℕ × ℕ`

, `show_term { split, exact 0 }`

will
print `refine (0, _)`

, and afterwards there will be one remaining goal (of type `ℕ`

).
This indicates that `split, exact 0`

partially filled in the original metavariable,
but created a new metavariable for the resulting sub-goal.

## Related declarations

## Import using

- import tactic.show_term
- import tactic.basic

## simp

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

is preceded by left arrow (`←`

or `<-`

), the simplification is performed in the reverse direction. 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 *`

is a shorthand for `simp [*]`

.

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

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

but does not use `[simp]`

lemmas

`simp [-id_1, ... -id_n]`

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 non-dependent hypotheses `h₁ : T₁`

... `hₙ : Tₙ`

. The tactic fails if the target or another hypothesis depends on one of them. The token `⊢`

or `|-`

can be added to the list to include the target.

`simp at *`

simplifies all the hypotheses and the target.

`simp * at *`

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

`simp with attr₁ ... attrₙ`

simplifies the main goal target using the lemmas tagged with any of the attributes `[attr₁]`

, ..., `[attrₙ]`

or `[simp]`

.

## Related declarations

## Import using

- imported by default

## simp_intros

`simp_intros h₁ h₂ ... hₙ`

is similar to `intros h₁ h₂ ... hₙ`

except that each hypothesis is simplified as it is introduced, and each introduced hypothesis is used to simplify later ones and the final target.

As with `simp`

, a list of simplification lemmas can be provided. The modifiers `only`

and `with`

behave as with `simp`

.

## Related declarations

## Import using

- imported by default

## simp_result

`simp_result { tac }`

attempts to run a tactic block `tac`

,
intercepts any results the tactic block would have assigned to the goals,
and runs `simp`

on those results
before assigning the simplified values to the original goals.

You can use the usual interactive syntax for `simp`

, e.g.
`simp_result only [a, b, c] with attr { tac }`

.

`dsimp_result { tac }`

works similarly, internally using `dsimp`

(and so only simplifiying along definitional lemmas).

## Related declarations

## Import using

- import tactic.simp_result
- import tactic.basic

## simp_rw

`simp_rw`

functions as a mix of `simp`

and `rw`

. Like `rw`

, it applies each
rewrite rule in the given order, but like `simp`

it repeatedly applies these
rules and also under binders like `∀ x, ...`

, `∃ x, ...`

and `λ x, ...`

.

Usage:

`simp_rw [lemma_1, ..., lemma_n]`

will rewrite the goal by applying the lemmas in that order. A lemma preceded by`←`

is applied in the reverse direction.`simp_rw [lemma_1, ..., lemma_n] at h₁ ... hₙ`

will rewrite the given hypotheses.`simp_rw [...] at ⊢ h₁ ... hₙ`

rewrites the goal as well as the given hypotheses.`simp_rw [...] at *`

rewrites in the whole context: all hypotheses and the goal.

Lemmas passed to `simp_rw`

must be expressions that are valid arguments to `simp`

.

For example, neither `simp`

nor `rw`

can solve the following, but `simp_rw`

can:

```
example {α β : Type} {f : α → β} {t : set β} : (∀ s, f '' s ⊆ t) = ∀ s : set α, ∀ x ∈ s, x ∈ f ⁻¹' t :=
by simp_rw [set.image_subset_iff, set.subset_def]
```

## Related declarations

## Import using

- import tactic.simp_rw
- import tactic.basic

## simpa

This is a "finishing" tactic modification of `simp`

. It has two forms.

`simpa [rules, ...] using e`

will simplify the goal and the type of`e`

using`rules`

, then try to close the goal using`e`

.Simplifying the type of

`e`

makes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.`simpa [rules, ...]`

will simplify the goal and the type of a hypothesis`this`

if present in the context, then try to close the goal using the`assumption`

tactic.

## Related declarations

## Import using

- import tactic.simpa
- import tactic.basic

## slice

`slice_lhs a b { tac }`

zooms to the left hand side, uses associativity for categorical
composition as needed, zooms in on the `a`

-th through `b`

-th morphisms, and invokes `tac`

.

`slice_rhs a b { tac }`

zooms to the right hand side, uses associativity for categorical
composition as needed, zooms in on the `a`

-th through `b`

-th morphisms, and invokes `tac`

.

## Related declarations

## Import using

- import tactic.slice
- import tactic

## solve1

`solve1 { t }`

applies the tactic `t`

to the main goal and fails if it is not solved.

## Related declarations

## Import using

- imported by default

## solve_by_elim

`solve_by_elim`

calls `apply`

on the main goal to find an assumption whose head matches
and then repeatedly calls `apply`

on the generated subgoals until no subgoals remain,
performing at most `max_depth`

recursive steps.

`solve_by_elim`

discharges the current goal or fails.

`solve_by_elim`

performs back-tracking if subgoals can not be solved.

By default, the assumptions passed to `apply`

are the local context, `rfl`

, `trivial`

,
`congr_fun`

and `congr_arg`

.

The assumptions can be modified with similar syntax as for `simp`

:

`solve_by_elim [h₁, h₂, ..., hᵣ]`

also applies the named lemmas.`solve_by_elim with attr₁ ... attrᵣ`

also applies all lemmas tagged with the specified attributes.`solve_by_elim only [h₁, h₂, ..., hᵣ]`

does not include the local context,`rfl`

,`trivial`

,`congr_fun`

, or`congr_arg`

unless they are explicitly included.`solve_by_elim [-id_1, ... -id_n]`

uses the default assumptions, removing the specified ones.

`solve_by_elim*`

tries to solve all goals together, using backtracking if a solution for one goal
makes other goals impossible.

optional arguments passed via a configuration argument as `solve_by_elim { ... }`

- max_depth: number of attempts at discharging generated sub-goals
- discharger: a subsidiary tactic to try at each step when no lemmas apply
(e.g.
`cc`

may be helpful). - pre_apply: a subsidiary tactic to run at each step before applying lemmas (e.g.
`intros`

). - accept: a subsidiary tactic
`list expr → tactic unit`

that at each step, before any lemmas are applied, is passed the original proof terms as reported by`get_goals`

when`solve_by_elim`

started (but which may by now have been partially solved by previous`apply`

steps). If the`accept`

tactic fails,`solve_by_elim`

will abort searching the current branch and backtrack. This may be used to filter results, either at every step of the search, or filtering complete results (by testing for the absence of metavariables, and then the filtering condition).

## Related declarations

## Import using

- import tactic.solve_by_elim
- import tactic.basic

## sorry / admit

Closes the main goal using `sorry`

.

## Related declarations

## Import using

- imported by default

## specialize

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

## Related declarations

## Import using

- imported by default

## split

Applies the constructor when the type of the target is an inductive data type with one constructor.

## Related declarations

## Import using

- imported by default

## split_ifs

Splits all if-then-else-expressions into multiple goals.

Given a goal of the form `g (if p then x else y)`

, `split_ifs`

will produce
two goals: `p ⊢ g x`

and `¬p ⊢ g y`

.

If there are multiple ite-expressions, then `split_ifs`

will split them all,
starting with a top-most one whose condition does not contain another
ite-expression.

`split_ifs at *`

splits all ite-expressions in all hypotheses as well as the goal.

`split_ifs with h₁ h₂ h₃`

overrides the default names for the hypotheses.

## Related declarations

## Import using

- import tactic.split_ifs
- import tactic.basic

## squeeze_simp / squeeze_simpa / squeeze_dsimp / squeeze_scope

`squeeze_simp`

, `squeeze_simpa`

and `squeeze_dsimp`

perform the same
task with the difference that `squeeze_simp`

relates to `simp`

while
`squeeze_simpa`

relates to `simpa`

and `squeeze_dsimp`

relates to
`dsimp`

. The following applies to `squeeze_simp`

, `squeeze_simpa`

and
`squeeze_dsimp`

.

`squeeze_simp`

behaves like `simp`

(including all its arguments)
and prints a `simp only`

invocation to skip the search through the
`simp`

lemma list.

For instance, the following is easily solved with `simp`

:

```
example : 0 + 1 = 1 + 0 := by simp
```

To guide the proof search and speed it up, we may replace `simp`

with `squeeze_simp`

:

```
example : 0 + 1 = 1 + 0 := by squeeze_simp
-- prints:
-- Try this: simp only [add_zero, eq_self_iff_true, zero_add]
```

`squeeze_simp`

suggests a replacement which we can use instead of
`squeeze_simp`

.

```
example : 0 + 1 = 1 + 0 := by simp only [add_zero, eq_self_iff_true, zero_add]
```

`squeeze_simp only`

prints nothing as it already skips the `simp`

list.

This tactic is useful for speeding up the compilation of a complete file. Steps:

- search and replace
`simp`

with`squeeze_simp`

(the space helps avoid the replacement of`simp`

in`@[simp]`

) throughout the file. - Starting at the beginning of the file, go to each printout in turn, copy
the suggestion in place of
`squeeze_simp`

. - after all the suggestions were applied, search and replace
`squeeze_simp`

with`simp`

to remove the occurrences of`squeeze_simp`

that did not produce a suggestion.

Known limitation(s):

- in cases where
`squeeze_simp`

is used after a`;`

(e.g.`cases x; squeeze_simp`

),`squeeze_simp`

will produce as many suggestions as the number of goals it is applied to. It is likely that none of the suggestion is a good replacement but they can all be combined by concatenating their list of lemmas.`squeeze_scope`

can be used to combine the suggestions:`by squeeze_scope { cases x; squeeze_simp }`

- sometimes,
`simp`

lemmas are also`_refl_lemma`

and they can be used without appearing in the resulting proof.`squeeze_simp`

won't know to try that lemma unless it is called as`squeeze_simp?`

## Related declarations

## Import using

- import tactic.squeeze
- import tactic.basic

## subst

Given hypothesis `h : x = t`

or `h : t = x`

, where `x`

is a local constant, `subst h`

substitutes `x`

by `t`

everywhere in the main goal and then clears `h`

.

## Related declarations

## Import using

- imported by default

## subst_vars

Apply `subst`

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

or `h : t = x`

.

## Related declarations

## Import using

- imported by default

## substs

Multiple `subst`

. `substs x y z`

is the same as `subst x, subst y, subst z`

.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## subtype_instance

builds instances for algebraic substructures

Example:

```
variables {α : Type*} [monoid α] {s : set α}
class is_submonoid (s : set α) : Prop :=
(one_mem : (1:α) ∈ s)
(mul_mem {a b} : a ∈ s → b ∈ s → a * b ∈ s)
instance subtype.monoid {s : set α} [is_submonoid s] : monoid s :=
by subtype_instance
```

## Related declarations

## Import using

- import tactic.subtype_instance
- import tactic

## success_if_fail

Succeeds if the given tactic fails.

## Related declarations

## Import using

- imported by default

## suffices

`suffices h : t`

is the same as `have h : t, tactic.swap`

. In other words, it adds the hypothesis `h : t`

to the current goal and opens a new subgoal with target `t`

.

## Related declarations

## Import using

- imported by default

## suggest

`suggest`

lists possible usages of the `refine`

tactic and leaves the tactic state unchanged.
It is intended as a complement of the search function in your editor, the `#find`

tactic, and
`library_search`

.

`suggest`

takes an optional natural number `num`

as input and returns the first `num`

(or less, if
all possibilities are exhausted) possibilities ordered by length of lemma names.
The default for `num`

is `50`

.

For performance reasons `suggest`

uses monadic lazy lists (`mllist`

). This means that `suggest`

might miss some results if `num`

is not large enough. However, because `suggest`

uses monadic
lazy lists, smaller values of `num`

run faster than larger values.

An example of `suggest`

in action,

```
example (n : nat) : n < n + 1 :=
begin suggest, sorry end
```

prints the list,

```
Try this: exact nat.lt.base n
Try this: exact nat.lt_succ_self n
Try this: refine not_le.mp _
Try this: refine gt_iff_lt.mp _
Try this: refine nat.lt.step _
Try this: refine lt_of_not_ge _
...
```

## Related declarations

## Import using

- import tactic.suggest
- import tactic.basic

## swap

`swap n`

will move the `n`

th goal to the front.
`swap`

defaults to `swap 2`

, and so interchanges the first and second goals.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## symmetry

This tactic applies to a goal whose target has the form `t ~ u`

where `~`

is a symmetric relation, that is, a relation which has a symmetry lemma tagged with the attribute `[symm]`

. It replaces the target with `u ~ t`

.

## Related declarations

## Import using

- imported by default

## tautology

This tactic (with shorthand `tauto`

) breaks down assumptions of the form
`_ ∧ _`

, `_ ∨ _`

, `_ ↔ _`

and `∃ _, _`

and splits a goal of the form `_ ∧ _`

, `_ ↔ _`

or `∃ _, _`

until it can be discharged
using `reflexivity`

or `solve_by_elim`

. This is a finishing tactic: it
either closes the goal or raises an error.

The variants `tautology!`

and `tauto!`

use the law of excluded middle.

For instance, one can write:

```
example (p q r : Prop) [decidable p] [decidable r] : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (r ∨ p ∨ r) := by tauto
```

and the decidability assumptions can be dropped if `tauto!`

is used
instead of `tauto`

.

`tauto {closer := tac}`

will use `tac`

on any subgoals created by `tauto`

that it is unable to solve before failing.

## Related declarations

## Import using

- import tactic.tauto
- import tactic.basic

## tfae

The `tfae`

tactic suite is a set of tactics that help with proving that certain
propositions are equivalent.
In `data/list/basic.lean`

there is a section devoted to propositions of the
form

```
tfae [p1, p2, ..., pn]
```

where `p1`

, `p2`

, through, `pn`

are terms of type `Prop`

.
This proposition asserts that all the `pi`

are pairwise equivalent.
There are results that allow to extract the equivalence
of two propositions `pi`

and `pj`

.

To prove a goal of the form `tfae [p1, p2, ..., pn]`

, there are two
tactics. The first tactic is `tfae_have`

. As an argument it takes an
expression of the form `i arrow j`

, where `i`

and `j`

are two positive
natural numbers, and `arrow`

is an arrow such as `→`

, `->`

, `←`

, `<-`

,
`↔`

, or `<->`

. The tactic `tfae_have : i arrow j`

sets up a subgoal in
which the user has to prove the equivalence (or implication) of `pi`

and `pj`

.

The remaining tactic, `tfae_finish`

, is a finishing tactic. It
collects all implications and equivalences from the local context and
computes their transitive closure to close the
main goal.

`tfae_have`

and `tfae_finish`

can be used together in a proof as
follows:

```
example (a b c d : Prop) : tfae [a,b,c,d] :=
begin
tfae_have : 3 → 1,
{ /- prove c → a -/ },
tfae_have : 2 → 3,
{ /- prove b → c -/ },
tfae_have : 2 ← 1,
{ /- prove a → b -/ },
tfae_have : 4 ↔ 2,
{ /- prove d ↔ b -/ },
-- a b c d : Prop,
-- tfae_3_to_1 : c → a,
-- tfae_2_to_3 : b → c,
-- tfae_1_to_2 : a → b,
-- tfae_4_iff_2 : d ↔ b
-- ⊢ tfae [a, b, c, d]
tfae_finish,
end
```

## Related declarations

## Import using

- import tactic.tfae
- import tactic

## tidy

Use a variety of conservative tactics to solve goals.

`tidy?`

reports back the tactic script it found. As an example

```
example : ∀ x : unit, x = unit.star :=
begin
tidy? -- Prints the trace message: "Try this: intros x, exact dec_trivial"
end
```

The default list of tactics is stored in `tactic.tidy.default_tidy_tactics`

.
This list can be overridden using `tidy { tactics := ... }`

.
(The list must be a `list`

of `tactic string`

, so that `tidy?`

can report a usable tactic script.)

Tactics can also be added to the list by tagging them (locally) with the
`[tidy]`

attribute.

## Related declarations

## Import using

- import tactic.tidy
- import tactic.basic

## trace

`trace a`

displays `a`

in the tracing buffer.

## Related declarations

## Import using

- imported by default

## trace_simp_set

Just construct the simp set and trace it. Used for debugging.

## Related declarations

## Import using

- imported by default

## trace_state

This tactic displays the current state in the tracing buffer.

## Related declarations

## Import using

- imported by default

## transitivity

This tactic applies to a goal whose target has the form `t ~ u`

where `~`

is a transitive relation, that is, a relation which has a transitivity lemma tagged with the attribute `[trans]`

.

`transitivity s`

replaces the goal with the two subgoals `t ~ s`

and `s ~ u`

. If `s`

is omitted, then a metavariable is used instead.

## Related declarations

## Import using

- imported by default

## transport

Given a goal `⊢ S β`

for some type class `S`

, and an equivalence `e : α ≃ β`

.
`transport using e`

will look for a hypothesis `s : S α`

,
and attempt to close the goal by transporting `s`

across the equivalence `e`

.

You can specify the object to transport using `transport s using e`

.

`transport`

works by attempting to copy each of the operations and axiom fields of `s`

,
rewriting them using `equiv_rw e`

and defining a new structure using these rewritten fields.

If it fails to fill in all the new fields, `transport`

will produce new subgoals.
It's probably best to think about which missing `simp`

lemmas would have allowed `transport`

to finish, rather than solving these goals by hand.
(This may require looking at the implementation of `tranport`

to understand its algorithm;
there are several examples of "transport-by-hand" at the end of `test/equiv_rw.lean`

,
which `transport`

is an abstraction of.)

## Related declarations

## Import using

- import tactic.transport
- import tactic

## triv

a weaker version of `trivial`

that tries to solve the goal by reflexivity or by reducing it to true,
unfolding only `reducible`

constants.

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## trivial

Tries to solve the current goal using a canonical proof of `true`

, or the `reflexivity`

tactic, or the `contradiction`

tactic.

## Related declarations

## Import using

- imported by default

## trunc_cases

`trunc_cases e`

performs case analysis on a `trunc`

expression `e`

,
attempting the following strategies:

- when the goal is a subsingleton, calling
`induction e using trunc.rec_on_subsingleton`

, - when the goal does not depend on
`e`

, calling`fapply trunc.lift_on e`

, and using`intro`

and`clear`

afterwards to make the goals look like we used`induction`

, - otherwise, falling through to
`trunc.rec_on`

, and in the new invariance goal calling`cases h_p`

on the useless`h_p : true`

hypothesis, and then attempting to simplify the`eq.rec`

.

`trunc_cases e with h`

names the new hypothesis `h`

.
If `e`

is a local hypothesis already,
`trunc_cases`

defaults to reusing the same name.

`trunc_cases e with h h_a h_b`

will use the names `h_a`

and `h_b`

for the new hypothesis
in the invariance goal if `trunc_cases`

uses `trunc.lift_on`

or `trunc.rec_on`

.

Finally, if the new hypothesis from inside the `trunc`

is a type class,
`trunc_cases`

resets the instance cache so that it is immediately available.

## Related declarations

## Import using

- import tactic.trunc_cases
- import tactic.basic

## try

`try { t }`

tries to apply tactic `t`

, but succeeds whether or not `t`

succeeds.

## Related declarations

## Import using

- imported by default

## type_check

Type check the given expression, and trace its type.

## Related declarations

## Import using

- imported by default

## unfold

Given defined constants `e₁ ... eₙ`

, `unfold e₁ ... eₙ`

iteratively unfolds all occurrences in the target of the main goal, using equational lemmas associated with the definitions.

As with `simp`

, the `at`

modifier can be used to specify locations for the unfolding.

## Related declarations

## Import using

- imported by default

## unfold1

Similar to `unfold`

, but does not iterate the unfolding.

## Related declarations

## Import using

- imported by default

## unfold_cases

This tactic unfolds the definition of a function or `match`

expression.
Then it recursively introduces a distinction by cases. The decision what expression
to do the distinction on is driven by the pattern matching expression.

A typical use case is using `unfold_cases { refl }`

to collapse cases that need to be
considered in a pattern matching.

```
have h : foo x = y, by unfold_cases { refl },
rw h,
```

The tactic expects a goal in the form of an equation, possibly universally quantified.

We can prove a theorem, even if the various case do not directly correspond to the function definition. Here is an example application of the tactic:

```
def foo : ℕ → ℕ → ℕ
| 0 0 := 17
| (n+2) 17 := 17
| 1 0 := 23
| 0 (n+18) := 15
| 0 17 := 17
| 1 17 := 17
| _ (n+18) := 27
| _ _ := 15
example : ∀ x, foo x 17 = 17 :=
begin
unfold_cases { refl },
end
```

The compiler generates 57 cases for `foo`

. However, when we look at the definition, we see
that whenever the function is applied to `17`

in the second argument, it returns `17`

.

Proving this property consists of merely considering all the cases, eliminating invalid ones
and applying `refl`

on the ones which remain.

Further examples can be found in `test/unfold_cases.lean`

.

## Related declarations

## Import using

- import tactic.unfold_cases
- import tactic

## unfold_coes

Unfold coercion-related definitions

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## unfold_projs

This tactic unfolds all structure projections.

## Related declarations

## Import using

- imported by default

## unify_equations

`unify_equations eq₁ ... eqₙ`

performs a form of first-order unification on the
hypotheses `eqᵢ`

. The `eqᵢ`

must be homogeneous or heterogeneous equations.
Unification means that the equations are simplified using various facts about
constructors. For instance, consider this goal:

After `unify_equations h₁ h₂`

, we get

In the example, `unify_equations`

uses the fact that every constructor is
injective to conclude `n = m`

from `h₁`

. Then it replaces every `m`

with `n`

and
moves on to `h₂`

. The types of `f`

and `g`

are now equal, so the heterogeneous
equation turns into a homogeneous one and `g`

is replaced by `f`

. Note that the
equations are processed from left to right, so `unify_equations h₂ h₁`

would not
simplify as much.

In general, `unify_equations`

uses the following steps on each equation until
none of them applies any more:

- Constructor injectivity: if
`nat.succ n = nat.succ m`

then`n = m`

. - Substitution: if
`x = e`

for some hypothesis`x`

, then`x`

is replaced by`e`

everywhere. - No-confusion:
`nat.succ n = nat.zero`

is a contradiction. If we have such an equation, the goal is solved immediately. - Cycle elimination:
`n = nat.succ n`

is a contradiction. - Redundancy: if
`t = u`

but`t`

and`u`

are already definitionally equal, then this equation is removed. - Downgrading of heterogeneous equations: if
`t == u`

but`t`

and`u`

have the same type (up to definitional equality), then the equation is replaced by`t = u`

.

## Related declarations

## Import using

- import tactic.unify_equations
- import tactic.basic

## use

Similar to `existsi`

. `use x`

will instantiate the first term of an `∃`

or `Σ`

goal with `x`

.
It will then try to close the new goal using `triv`

, or try to simplify it by applying `exists_prop`

.
Unlike `existsi`

, `x`

is elaborated with respect to the expected type.
`use`

will alternatively take a list of terms `[x0, ..., xn]`

.

`use`

will work with constructors of arbitrary inductive types.

Examples:

```
example (α : Type) : ∃ S : set α, S = S :=
by use ∅
example : ∃ x : ℤ, x = x :=
by use 42
example : ∃ n > 0, n = n :=
begin
use 1,
-- goal is now 1 > 0 ∧ 1 = 1, whereas it would be ∃ (H : 1 > 0), 1 = 1 after existsi 1.
exact ⟨zero_lt_one, rfl⟩,
end
example : ∃ a b c : ℤ, a + b + c = 6 :=
by use [1, 2, 3]
example : ∃ p : ℤ × ℤ, p.1 = 1 :=
by use ⟨1, 42⟩
example : Σ x y : ℤ, (ℤ × ℤ) × ℤ :=
by use [1, 2, 3, 4, 5]
inductive foo
| mk : ℕ → bool × ℕ → ℕ → foo
example : foo :=
by use [100, tt, 4, 3]
```

## Related declarations

## Import using

- import tactic.interactive
- import tactic.basic

## with_cases

Apply `t`

to the main goal and revert any new hypothesis in the generated goals.
If `t`

is a supported tactic or chain of supported tactics (e.g. `induction`

,
`cases`

, `apply`

, `constructor`

), the generated goals are also tagged with case
tags. You can then use `case`

to focus such tagged goals.

Two typical uses of `with_cases`

:

Applying a custom eliminator:

Enabling the use of

`case`

after a chain of case-splitting tactics:

## Related declarations

## Import using

- imported by default

## wlog

Without loss of generality: reduces to one goal under variables permutations.

Given a goal of the form `g xs`

, a predicate `p`

over a set of variables, as well as variable
permutations `xs_i`

. Then `wlog`

produces goals of the form

The case goal, i.e. the permutation `xs_i`

covers all possible cases:
`⊢ p xs_0 ∨ ⋯ ∨ p xs_n`

The main goal, i.e. the goal reduced to `xs_0`

:
`(h : p xs_0) ⊢ g xs_0`

The invariant goals, i.e. `g`

is invariant under `xs_i`

:
`(h : p xs_i) (this : g xs_0) ⊢ gs xs_i`

Either the permutation is provided, or a proof of the disjunction is provided to compute the
permutation. The disjunction need to be in assoc normal form, e.g. `p₀ ∨ (p₁ ∨ p₂)`

. In many cases
the invariant goals can be solved by AC rewriting using `cc`

etc.

Example:
On a state `(n m : ℕ) ⊢ p n m`

the tactic `wlog h : n ≤ m using [n m, m n]`

produces the following
states:
`(n m : ℕ) ⊢ n ≤ m ∨ m ≤ n`

`(n m : ℕ) (h : n ≤ m) ⊢ p n m`

`(n m : ℕ) (h : m ≤ n) (this : p n m) ⊢ p m n`

`wlog`

supports different calling conventions. The name `h`

is used to give a name to the introduced
case hypothesis. If the name is avoided, the default will be `case`

.

(1) `wlog : p xs0 using [xs0, …, xsn]`

Results in the case goal `p xs0 ∨ ⋯ ∨ ps xsn`

, the main goal `(case : p xs0) ⊢ g xs0`

and the
invariance goals `(case : p xsi) (this : g xs0) ⊢ g xsi`

.

(2) `wlog : p xs0 := r using xs0`

The expression `r`

is a proof of the shape `p xs0 ∨ ⋯ ∨ p xsi`

, it is also used to compute the
variable permutations.

(3) `wlog := r using xs0`

The expression `r`

is a proof of the shape `p xs0 ∨ ⋯ ∨ p xsi`

, it is also used to compute the
variable permutations. This is not as stable as (2), for example `p`

cannot be a disjunction.

(4) `wlog : R x y using x y`

and `wlog : R x y`

Produces the case `R x y ∨ R y x`

. If `R`

is ≤, then the disjunction discharged using linearity.
If `using x y`

is avoided then `x`

and `y`

are the last two variables appearing in the
expression `R x y`

.

## Related declarations

## Import using

- import tactic.wlog
- import tactic

## zify

The `zify`

tactic is used to shift propositions from `ℕ`

to `ℤ`

.
This is often useful since `ℤ`

has well-behaved subtraction.

```
example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b :=
begin
zify,
zify at h,
/-
h : ¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
end
```

`zify`

can be given extra lemmas to use in simplification. This is especially useful in the
presence of nat subtraction: passing `≤`

arguments will allow `push_cast`

to do more work.

```
example (a b c : ℕ) (h : a - b < c) (hab : b ≤ a) : false :=
begin
zify [hab] at h,
/- h : ↑a - ↑b < ↑c -/
end
```

`zify`

makes use of the `@[zify]`

attribute to move propositions,
and the `push_cast`

tactic to simplify the `ℤ`

-valued expressions.

`zify`

is in some sense dual to the `lift`

tactic. `lift (z : ℤ) to ℕ`

will change the type of an
integer `z`

(in the supertype) to `ℕ`

(the subtype), given a proof that `z ≥ 0`

;
propositions concerning `z`

will still be over `ℤ`

. `zify`

changes propositions about `ℕ`

(the
subtype) to propositions about `ℤ`

(the supertype), without changing the type of any variable.

## Related declarations

## Import using

- import tactic.zify
- import tactic