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 tactictac
. 
introI
/introsI
:intro
/intros
followed byresetI
. Likeintro
/intros
, but uses the introduced variable in typeclass inference. 
casesI
: likecases
, but can also be used with instance arguments. 
substI
: likesubst
, but can also substitute in typeclass arguments 
haveI
/letI
/rsufficesI
:have
/let
/rsuffices
followed byresetI
. Used to add typeclasses to the context so that they can be used in typeclass inference. 
exactI
:resetI
followed byexact
. Likeexact
, but uses all variables in the context for typeclass inference.
Related declarations
Import using
 imported by default
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.
abel!
will use a more aggressive reducibility setting to identify atoms.
This can prove goals that abel
cannot, but is more expensive.
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 }
example {α : Type*} {a b : α} [add_comm_group α] : (a + b)  (id a + b) = 0 := by abel!
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 lefthand side
and the righthand 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 wellformed 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. Nondependent premises are added before dependent ones.
The apply
tactic uses higherorder pattern matching, type class resolution, and firstorder 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 constantstac
: 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 an equality or inequality in either a local hypothesis or the goal.
 If we have
h : a = b
, thenapply_fun f at h
will replace this withh : f a = f b
.  If we have
h : a ≤ b
, thenapply_fun f at h
will replace this withh : f a ≤ f b
, and create a subsidiary goalmonotone f
.apply_fun
will automatically attempt to discharge this subsidiary goal usingmono
, or an explicit solution can be provided withapply_fun f at h using P
, whereP : monotone f
.  If the goal is
a ≠ b
,apply_fun f
will replace this withf a ≠ f b
.  If the goal is
a = b
,apply_fun f
will replace this withf a = f b
, and create a subsidiary goalinjective f
.apply_fun
will automatically attempt to discharge this subsidiary goal using local hypotheses, or iff
is actually anequiv
, or an explicit solution can be provided withapply_fun f using P
, whereP : injective f
.  If the goal is
a ≤ b
(or similarly fora < b
), andf
is actually anorder_iso
,apply_fun f
will replace the goal withf a ≤ f b
. Iff
is anything else (e.g. just a function, or anequiv
),apply_fun
will fail.
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 with attrs n
applies the list of lemmas hs
and all lemmas tagged with an
attribute from the list attrs
, as well as the assumption
tactic 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.)
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 with mono_rules
by apply_rules [add_le_add] with 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.
It works for any function f
for which an is_associative f
instance can be found.
example {α : Type*} (f : α → α → α) [is_associative α f] (a b c d x : α) :
let infix ` ~ ` := f in
b ~ c = x → (a ~ b ~ c ~ d) = (a ~ x ~ d) :=
begin
intro h,
assoc_rw h,
end
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
borelize
The behaviour of borelize α
depends on the existing assumptions on α
.
 if
α
is a topological space with instances[measurable_space α] [borel_space α]
, thenborelize α
replaces the former instance byborel α
;  otherwise,
borelize α
adds instancesborel α : measurable_space α
and⟨rfl⟩ : borel_space α
.
Finally, borelize [α, β, γ]
runs borelize α, borelize β, borelize γ
.
Related declarations
Import using
 import measure_theory.constructions.borel_space
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
by_contra'
If the target of the main goal is a proposition p
,
by_contra'
reduces the goal to proving false
using the additional hypothesis h : ¬ p
.
by_contra' h
can be used to name the hypothesis h : ¬ p
.
The hypothesis ¬ p
will be negation normalized using push_neg
.
For instance, ¬ a < b
will be changed to b ≤ a
.
by_contra' h : q
will normalize negations in ¬ p
, normalize negations in q
,
and then check that the two normalized forms are equal.
The resulting hypothesis is the prenormalized form, q
.
If the name h
is not explicitly provided, then this
will be used as name.
This tactic uses classical reasoning.
It is a variant on the tactic by_contra
(tactic.interactive.by_contra
).
Examples:
example : 1 < 2 :=
begin
by_contra' h,
 h : 2 ≤ 1 ⊢ false
end
example : 1 < 2 :=
begin
by_contra' h : ¬ 1 < 2,
 h : ¬ 1 < 2 ⊢ false
end
```
Related declarations
Import using
 import tactic.by_contra
 import tactic
cancel_denoms
cancel_denoms
attempts to remove numerals from the denominators of fractions.
It works on propositions that are fieldvalued 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
.
Multiple cases can be handled by the same tactic block with
case [A : N₀ ... Nₙ, B : M₀ ... Mₙ] {...}
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 thecases
tactic to a hypothesish : (I ...)
cases_type I_1 ... I_n
applies thecases
tactic to a hypothesish : (I_1 ...)
or ... orh : (I_n ...)
cases_type* I
is shorthand forfocus1 { repeat { cases_type I } }
cases_type! I
only appliescases
if the number of resulting subgoals is <= 1.
Example: The following tactic destructs all conjunctions and disjunctions in the current context.
Related declarations
Import using
 imported by default
category_theory.elementwise_of
With w : ∀ ..., f ≫ g = h
(with universal quantifiers tolerated),
elementwise_of w : ∀ ... (x : X), g (f x) = h x
.
Although elementwise_of
is not a tactic or a meta program, its type is generated
through metaprogramming to make it usable inside normal expressions.
Related declarations
Import using
 import tactic.elementwise
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 metaprogramming 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 two functions 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.
classical!
does this more aggressively, such that even if a decidable instance is already
available for a specific proposition, the noncomputable one will be used instead.
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
coherence
Use the coherence theorem for monoidal categories to solve equations in a monoidal equation, where the two sides only differ by replacing strings of monoidal structural morphisms (that is, associators, unitors, and identities) with different strings of structural morphisms with the same source and target.
That is, coherence
can handle goals of the form
a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'
where a = a'
, b = b'
, and c = c'
can be proved using pure_coherence
.
(If you have very large equations on which coherence
is unexpectedly failing,
you may need to increase the typeclass search depth,
using e.g. set_option class.instance_max_depth 500
.)
Related declarations
Import using
 import category_theory.monoidal.coherence
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
compute_degree_le
compute_degree_le
tries to solve a goal of the form f.nat_degree ≤ d
or f.degree ≤ d
,
where f : R[X]
and d : ℕ
or d : with_bot ℕ
.
If the given degree d
is smaller than the one that the tactic computes,
then the tactic suggests the degree that it computed.
Examples:
open polynomial
open_locale polynomial
variables {R : Type*} [semiring R] {a b c d e : R}
example {F} [ring F] {a : F} {n : ℕ} (h : n ≤ 10) :
nat_degree (X ^ n + C a * X ^ 10 : F[X]) ≤ 10 :=
by compute_degree_le
example : nat_degree (7 * X : R[X]) ≤ 1 :=
by compute_degree_le
example {p : R[X]} {n : ℕ} {p0 : p.nat_degree = 0} :
(p ^ n).nat_degree ≤ 0 :=
by compute_degree_le
```
Related declarations
Import using
 import tactic.compute_degree
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 overaggressive 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
, whilecongr' 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 callext p (: n)?
to all subgoals generated bycongr'
. For example, if the goal is⊢ f '' s = g '' s
thencongr' with x
generates the goalx : α ⊢ f x = g x
.
Related declarations
Import using
 import tactic.congr
 import tactic.basic
congrm
Assume that the goal is of the form lhs = rhs
or lhs ↔ rhs
.
congrm e
takes an expression e
containing placeholders _
and scans e, lhs, rhs
in parallel.
It matches both lhs
and rhs
to the pattern e
, and produces one goal for each placeholder,
stating that the corresponding subexpressions in lhs
and rhs
are equal.
Examples:
example {a b c d : ℕ} :
nat.pred a.succ * (d + (c + a.pred)) = nat.pred b.succ * (b + (c + d.pred)) :=
begin
congrm nat.pred (nat.succ _) * (_ + _),
/ Goals left:
⊢ a = b
⊢ d = b
⊢ c + a.pred = c + d.pred
/
sorry,
sorry,
sorry,
end
example {a b : ℕ} (h : a = b) : (λ y : ℕ, ∀ z, a + a = z) = (λ x, ∀ z, b + a = z) :=
begin
congrm λ x, ∀ w, _ + a = w,
 produces one goal for the underscore: ⊢ a = b
exact h,
end
The tactic also allows for "function underscores", denoted by _₁, ..., _₄
. The index denotes
the number of explicit arguments of the function to be matched.
If e
has a "function underscore" in a location, then the tactic reads off the function f
that
appears in lhs
at the current location, replacing the explicit arguments of f
by the user
inputs to the "function underscore". After that, congrm
continues with its matching.
Related declarations
Import using
 import tactic.congrm
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 goalP → Q
into¬ Q → ¬ P
contrapose!
turns a goalP → Q
into¬ Q → ¬ P
and pushes negations insideP
andQ
usingpush_neg
contrapose h
first reverts the local assumptionh
, and then usescontrapose
andintro h
contrapose! h
first reverts the local assumptionh
, and then usescontrapose!
andintro h
contrapose h with new_h
uses the namenew_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://leanprovercommunity.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 better 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 rescoping
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 toplevel λ
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
noop.
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 lefthandside of a relation.
A goal of  a = b
will turn into the goal  a
.
Related declarations
Import using
 imported by default
conv: to_rhs
Navigate to the righthandside of a relation.
A goal of  a = b
will turn into 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
.
The convert
tactic applies congruence lemmas eagerly before reducing,
therefore it can fail in cases where exact
succeeds:
def p (n : ℕ) := true
example (h : p 0) : p 1 := by exact h  succeeds
example (h : p 0) : p 1 := by convert h  fails, with leftover goal `1 = 0`
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
.
convert_to
is similar to convert
, but convert_to
takes a type (the desired subgoal) while
convert
takes a proof term.
That is, convert_to g using n
is equivalent to convert (_ : g) using n
.
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 nondependent 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 nondependent 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₁ h₂ ⋯
, where each hᵢ : α
is a hypothesis, and e : α ≃ β
,
will attempt to transport each 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 [e₁, e₂, ⋯] at h₁ h₂ ⋯
is equivalent to
{ equiv_rw [e₁, e₂, ⋯] at h₁, equiv_rw [e₁, e₂, ⋯] at h₂, ⋯ }
.
equiv_rw [e₁, e₂, ⋯] at *
will attempt to apply equiv_rw [e₁, e₂, ⋯]
on the goal
and on each expression available in the local context (except on the eᵢ
s themselves),
failing silently when it can't. Failing on a rewrite for a certain eᵢ
at a certain
hypothesis h
doesn't stop equiv_rw
from trying the other equivalences on the list
at h
. This only happens for the wildcard location.
equiv_rw
will also try rewriting under (equiv_)functors, so it 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 attributeext
), usingid
, if provided, to name a local constant introduced by the lemma. Ifid
is omitted, the local constant is named automatically, as perintro
. 
ext
applies as many extensionality lemmas as possible; 
ext ids
, withids
a list of identifiers, finds extensionality lemmas and applies them until it runs out of identifiers inids
to name the local constants. 
ext
can also be given anrcases
pattern in place of an identifier. This will destruct the introduced local constant.
 Placing a
?
afterext
/ext1
(e.g.ext? i ⟨a,b⟩ : 3
) will display a sequence of tactic applications that can replace the call toext
/ext1
. set_option trace.ext true
will trace every attempted lemma application, along with the time it takes for the application to succeed or fail. This is useful for debugging slowext
calls.
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.
In the previous example, applying ext? ⟨a,b⟩
will produce the trace message:
Try this: apply funext, rintro ⟨a, b⟩
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 standalone example. Useful for testing tactics or creating minimal working examples.
extract_goal
: formats the statement as anexample
declarationextract_goal my_decl
: formats the statement as alemma
ordef
declaration calledmy_decl
extract_goal with i j k:
only use local constantsi
,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, mul_eq_zero, hx, hy] with field_simps {discharger := tactic.field_simp.ne_zero}
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.
To check that denominators are nonzero, field_simp
will look for facts in the context, and
will try to apply norm_num
to close numerical goals.
The invocation of field_simp
removes the lemma one_div
from the simpset, as this lemma
works against the algorithm explained above. It also removes
mul_eq_zero : x * y = 0 ↔ x = 0 ∨ y = 0
, as norm_num
can not work on disjunctions to
close goals of the form 24 ≠ 0
, and replaces it with mul_ne_zero : x ≠ 0 → y ≠ 0 → x * y ≠ 0
creating two goals instead of a disjunction.
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,
ring
end
Moreover, the field_simp
tactic can also take care of inverses of units in
a general (commutative) monoid/ring and partial division /ₚ
, see algebra.group.units
for the definition. Analogue to the case above, the lemma one_divp
is removed from the simpset
as this works against the algorithm. If you have objects with a is_unit x
instance like
(x : R) (hx : is_unit x)
, you should lift them with
lift x to Rˣ using id hx, rw is_unit.unit_of_coe_units, clear hx
before using field_simp
.
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.field_simp
 import tactic
filter_upwards
filter_upwards [h₁, ⋯, hₙ]
replaces a goal of the form s ∈ f
and terms
h₁ : t₁ ∈ f, ⋯, hₙ : tₙ ∈ f
with ∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s
.
The list is an optional parameter, []
being its default value.
filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ
is a short form for
{ filter_upwards [h₁, ⋯, hₙ], intros a₁ a₂ ⋯ aₖ }
.
filter_upwards [h₁, ⋯, hₙ] using e
is a short form for
{ filter_upwards [h1, ⋯, hn], exact e }
.
Combining both shortcuts is done by writing filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ using e
.
Note that in this case, the aᵢ
terms can be used in 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 ∈ 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
.
fin_cases h with l
takes a list of descriptions for the cases of h
.
These should be definitionally equal to and in the same order as the
default enumeration of the cases.
For example,
example (x y : ℕ) (h : x ∈ [1, 2]) : x = y :=
begin
fin_cases h with [1, 1+1],
end
produces two cases: 1 = y
and 1 + 1 = y
.
When using fin_cases a
on data a
defined with let
,
the tactic will not be able to clear the variable a
,
and will instead produce hypotheses this : a = ...
.
These hypotheses can be given a name using fin_cases a using ha
.
For example,
produces three goals with hypotheses
ha : a = 0
, ha : a = 1
, and ha : a = 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 failsclarify
: makes as much progress as possible while not leaving more than one goalsafe
: 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
generalize_proofs
Generalize proofs in the goal, naming them with the provided list.
For example:
example : list.nth_le [1, 2] 1 dec_trivial = 2 :=
begin
 ⊢ [1, 2].nth_le 1 _ = 2
generalize_proofs h,
 h : 1 < [1, 2].length
 ⊢ [1, 2].nth_le 1 h = 2
end
Related declarations
Import using
 import tactic.generalize_proofs
 import tactic.basic
generalizes
Generalizes the target over multiple expressions. For example, given the goal
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
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
alphaequivalence.
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α = β
withe : α, x : β
;h_generalize Hx : e == x with _
chooses automatically chooses the name of assumptionα = β
;h_generalize! Hx : e == x
revertsHx
; when
Hx
is omitted, assumptionHx : 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
, ifmy_tactic
is already of typetactic string
(tactic unit
is allowed too, in which case the printed string will be the name of the tactic), oradd_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
 inspects hypotheses looking for lower and upper bounds of the form
a ≤ n
andn < b
(although inℕ
,ℤ
, andℕ+
bounds of the forma < n
andn ≤ b
are also allowed), and also makes use of lower and upper bounds found viale_top
andbot_le
(so for example ifn : ℕ
, then the bound0 ≤ n
is found automatically), then  calls
fin_cases
on the synthesised hypothesisn ∈ set.Ico a b
, assuming an appropriatefintype
instance can be found for the type ofn
.
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 nondependent 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
itauto
A decision procedure for intuitionistic propositional logic. Unlike finish
and tauto!
this
tactic never uses the law of excluded middle (without the !
option), and the proof search is
tailored for this use case. (itauto!
will work as a classical SAT solver, but the algorithm is
not very good in this situation.)
example (p : Prop) : ¬ (p ↔ ¬ p) := by itauto
itauto [a, b]
will additionally attempt case analysis on a
and b
assuming that it can derive
decidable a
and decidable b
. itauto *
will case on all decidable propositions that it can
find among the atomic propositions, and itauto! *
will case on all propositional atoms.
Warning: This can blow up the proof search, so it should be used sparingly.
Related declarations
Import using
 import tactic.itauto
 import tactic.basic
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
.
If it succeeds, it prints a trace message exact ...
which can replace the invocation
of library_search
.
Typical usage is:
example (n m k : ℕ) : n * (m  k) = n * m  n * k :=
by library_search  Try this: exact mul_tsub n m k
library_search using h₁ h₂
will only show solutions
that make use of the local hypotheses h₁
and h₂
.
By default library_search
only unfolds reducible
definitions
when attempting to match lemmas against the goal.
Previously, it would unfold most definitions, sometimes giving surprising answers, or slow answers.
The old behaviour is still available via library_search!
.
You can add additional lemmas to be used along with local hypotheses
after the application of a library lemma,
using the same syntax as for solve_by_elim
, e.g.
example {a b c d: nat} (h₁ : a < c) (h₂ : b < d) : max (c + d) (a + b) = (c + d) :=
begin
library_search [add_lt_add],  Says: `Try this: exact max_eq_left_of_lt (add_lt_add h₁ h₂)`
end
You can also use library_search with attr
to include all lemmas with the attribute attr
.
Related declarations
Import using
 import tactic.suggest
 import tactic.basic
lift
Lift an expression to another type.
 Usage:
'lift' expr 'to' expr ('using' expr)? ('with' id (id id?)?)?
.  If
n : ℤ
andhn : n ≥ 0
then the tacticlift n to ℕ using hn
creates a new constant of typeℕ
, also namedn
and replaces all occurrences of the old variable(n : ℤ)
with↑n
(wheren
in the new variable). It will removen
andhn
from the context. So for example the tactic
lift n to ℕ using hn
transforms the goaln : ℤ, hn : n ≥ 0, h : P n ⊢ n = 3
ton : ℕ, h : P ↑n ⊢ ↑n = 3
(hereP
is some term of typeℤ → Prop
).
 So for example the tactic
 The argument
using hn
is optional, the tacticlift n to ℕ
does the same, but also creates a new subgoal thatn ≥ 0
(wheren
is the old variable). This subgoal will be placed at the top of the goal list. So for example the tactic
lift n to ℕ
transforms the goaln : ℤ, h : P n ⊢ n = 3
to two goalsn : ℤ, h : P n ⊢ n ≥ 0
andn : ℕ, h : P ↑n ⊢ ↑n = 3
.
 So for example the tactic
 You can also use
lift n to ℕ using e
wheree
is any expression of typen ≥ 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 userfl
for the name ofhk
to substituten
away (i.e. the default behavior).  You can also use
lift e to ℕ with k hk
wheree
is any expression of typeℤ
. In this case, thehk
will always stay in the context, but it will be used to rewritee
in all hypotheses and the target. So for example the tactic
lift n + 3 to ℕ using hn with k hk
transforms the goaln : ℤ, hn : n + 3 ≥ 0, h : P (n + 3) ⊢ n + 3 = 2 * n
to the goaln : ℤ, k : ℕ, hk : ↑k = n + 3, h : P ↑k ⊢ ↑k = 2 * n
.
 So for example the tactic
 The tactic
lift n to ℕ using h
will removeh
from the context. If you want to keep it, specify it again as the third argument towith
, 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 ofcan_lift α β
. In this case the proof obligation is specified bycan_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 instancecan_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 nondense 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 isring
. Other options currently includering SOP
orsimp
for basic problems.restrict_type
will only use hypotheses that are inequalities overtp
. 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 hardlinarith
will try to match atoms to each other. By default it will only unfoldreducible
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 norfalse
. (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
linear_combination
linear_combination
attempts to simplify the target by creating a linear combination
of a list of equalities and subtracting it from the target.
The tactic will create a linear
combination by adding the equalities together from left to right, so the order
of the input hypotheses does matter. If the normalize
field of the
configuration is set to false, then the tactic will simply set the user up to
prove their target using the linear combination instead of normalizing the subtraction.
Note: The left and right sides of all the equalities should have the same
type, and the coefficients should also have this type. There must be
instances of has_mul
and add_group
for this type.
 Input:

input
: the linear combination of proofs of equalities, given as a sum/difference of coefficients multiplied by expressions. The coefficients may be arbitrary preexpressions; if a coefficient is an application of+
or
it should be surrounded by parentheses. The expressions can be arbitrary proof terms proving equalities. Most commonly they are hypothesis namesh1, h2, ...
.If a coefficient is omitted, it is taken to be
1
. 
config
: alinear_combination_config
, which determines the tactic used for normalization; by default, this value is the standard configuration for a linear_combination_config. In the standard configuration,normalize
is set to tt (meaning this tactic is set to use normalization), andnormalization_tactic
is set toring_nf SOP
.

Example Usage:
example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) :
x*y = 2*y + 1 :=
by linear_combination 1*h1  2*h2
example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) :
x*y = 2*y + 1 :=
by linear_combination h1  2*h2
example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) :
x*y = 2*y + 1 :=
begin
linear_combination 2*h2,
/ Goal: x * y + x * 2  1 = 0 /
end
example (x y z : ℝ) (ha : x + 2*y  z = 4) (hb : 2*x + y + z = 2)
(hc : x + 2*y + z = 2) :
3*x  3*y  4*z = 2 :=
by linear_combination ha  hb  2*hc
example (x y : ℚ) (h1 : x + y = 3) (h2 : 3*x = 7) :
x*x*y + y*x*y + 6*x = 3*x*y + 14 :=
by linear_combination x*y*h1 + 2*h2
example (x y : ℤ) (h1 : x = 3) (h2 : y = 10) :
2*x = 6 :=
begin
linear_combination 2*h1 with {normalize := ff},
simp,
norm_cast
end
constants (qc : ℚ) (hqc : qc = 2*qc)
example (a b : ℚ) (h : ∀ p q : ℚ, p = q) : 3*a + qc = 3*b + 2*qc :=
by linear_combination 3 * h a b + hqc
```
Related declarations
Import using
 import tactic.linear_combination
 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
measurability / measurability'
measurability
solves goals of the form measurable f
, ae_measurable f μ
,
ae_strongly_measurable f μ
or measurable_set s
by applying lemmas tagged with the
measurability
user attribute.
You can also use measurability!
, 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.
measurability?
reports back the proof term it found.
Related declarations
Import using
 import measure_theory.tactic
mono
mono
applies a monotonicity rule.mono*
applies monotonicity rules repetitively.mono with x ≤ y
ormono with [0 ≤ x,0 ≤ y]
creates an assertion for the listed propositions. Those help to select the right monotonicity rule.mono left
ormono right
is useful when proving strict orderings: forx + y < w + z
could be broken down into either left:
x ≤ w
andy < z
or  right:
x < w
andy ≤ z
 left:
mono using [rule1,rule2]
callssimp [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
move_add
Calling move_add [a, ← b, c]
, recursively looks inside the goal for expressions involving a sum.
Whenever it finds one, it moves the summands that unify to a, b, c
, removing all parentheses.
Repetitions are allowed, and are processed following the userspecified ordering.
The terms preceded by a ←
get placed to the left, the ones without the arrow get placed to the
right. Unnamed terms stay in place. Due to reparenthesizing, doing move_add
with no argument
may change the goal. Also, the order in which the terms are provided matters: the tactic reads
them from left to right. This is especially important if there are multiple matches for the typed
terms in the given expressions.
A single call of move_add
moves terms across different sums in the same expression.
Here is an example.
import tactic.move_add
example {a b c d : ℕ} (h : c = d) : c + b + a = b + a + d :=
begin
move_add [← a, b],  Goal: `a + c + b = a + d + b`  both sides changed
congr,
exact h
end
example {a b c d : ℕ} (h : c = d) : c + b * c + a * c = a * d + d + b * d :=
begin
move_add [_ * c, ← _ * c],  Goal: `a * c + c + b * c = a * d + d + b * d`
 the first `_ * c` unifies with `b * c` and moves to the right
 the second `_ * c` unifies with `a * c` and moves to the left
congr;
assumption
end
The list of expressions that move_add
takes is optional and a single expression can be passed
without brackets. Thus move_add ← f
and move_add [← f]
mean the same.
Finally, move_add
can also target one or more hypotheses. If hp₁, hp₂
are in the
local context, then move_add [f, ← g] at hp₁ hp₂
performs the rearranging at hp₁
and hp₂
.
As usual, passing ⊢
refers to acting on the goal.
Reporting suboptimal usage #
The tactic could fail to prove the reordering. One potential cause is when there are multiple matches for the rearrangements and an earlier rewrite makes a subsequent one fail. Another possibility is that the rearranged expression changes the Type of some expression and the tactic gets stumped. Please, report bugs and failures in the Zulip chat!
There are three kinds of unwanted use for move_add
that result in errors, where the tactic fails
and flags the unwanted use.
move_add [vars]? at *
reports globally unused variables and whether all goals are unchanged, not each unchanged goal. If a target of
move_add [vars]? at targets
is left unchanged by the tactic, then this will be flagged (unless we are usingat *
).  If a userprovided expression never unifies, then the variable is flagged.
In these cases, the tactic produces an error, reporting unused inputs and unchanged targets as appropriate.
For instance, move_add ← _
always fails reporting an unchanged goal, but never an unused variable.
Comparison with existing tactics #

tactic.interactive.abel
performs a "reduction to normal form" that allows it to close goals involving sums with higher success rate thanmove_add
. If the goal is an equality of two sums that are simply obtained by reparenthesizing and permuting summands, thenmove_add [appropriate terms]
can close the goal. Compared toabel
,move_add
has the advantage of allowing the user to specify the beginning and the end of the final sum, so that from there the user can continue with the proof. 
tactic.interactive.ac_change
supports a wide variety of operations. At the moment,move_add
works with addition,move_mul
works with multiplication. There is the possibility of supporting other operations, using the noninteractive tactictactic.move_op
. Still, on several experiments,move_add
had a much quicker performance thanac_change
. Also, formove_add
the user need only specify a few terms: the tactic itself takes care of producing the full rearrangement and proving it "behind the scenes".
Remark: #
It is still possible that the same output of move_add [exprs]
can be achieved by a proper sublist
of [exprs]
, even if the tactic does not flag anything. For instance, giving the full reordering
of the expressions in the target that we want to achieve will not complain that there are unused
variables, since all the userprovided variables have been matched. Of course, specifying the order
of allbutthelast variable suffices to determine the permutation. E.g., with a goal of
a + b = 0
, applying either one of move_add [b,a]
, or move_add a
, or move_add ← b
has the
same effect and changes the goal to b + a = 0
. These are all valid uses of move_add
.
Related declarations
Import using
 import tactic.move_add
move_mul
See the docstring for tactic.interactive.move_add
and mentally
replace addition with multiplication throughout. ;)
Related declarations
Import using
 import tactic.move_add
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
ora * a
in a hypothesis or the goal, the assumption0 ≤ a ^ 2
or0 ≤ a * a
is added to the context.  For every pair of hypotheses
a1 R1 b1
,a2 R2 b2
in the context,R1, R2 ∈ {<, ≤, =}
, the assumption0 R' (b1  a1) * (b2  a2)
is added to the context (nonrecursively), whereR ∈ {<, ≤, =}
is the appropriate comparison derived fromR1, R2
.
Related declarations
Import using
 import tactic.linarith.frontend
 import tactic
noncomm_ring
A tactic for simplifying identities in notnecessarilycommutative 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 tactic.nontriviality
 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 nonterminating 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://leanforward.github.io/norm_cast/norm_cast.pdf.
Related declarations
Import using
 import tactic.norm_cast
 import tactic.basic
norm_fin
Rewrites occurrences of fin expressions to normal form anywhere in the goal.
The norm_num
extension will only rewrite fin expressions if they appear in equalities and
inequalities. For example if the goal is P (2 + 2 : fin 3)
then norm_num
will not do anything
but norm_fin
will reduce the goal to P 1
.
example : (5 : fin 7) = fin.succ (fin.succ 3) := by norm_num
example (P : fin 7 → Prop) (h : P 5) : P (fin.succ (fin.succ 3)) := by norm_fin; exact h
Related declarations
Import using
 import tactic.norm_fin
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.
Addon tactics marked as @[norm_num]
can extend the behavior of norm_num
to include other
functions. This is used to support several other functions on nat
like prime
, min_fac
and
factors
.
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 zerobased, 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
observe
observe hp : p
asserts the proposition p
, and tries to prove it using library_search
.
If no proof is found, the tactic fails.
In other words, this tactic is equivalent to have hp : p, { library_search }
.
If hp
is omitted, then the placeholder this
is used.
The variant observe? hp : p
will emit a trace message of the form have hp : p := proof_term
.
This may be particularly useful to speed up proofs.
Related declarations
Import using
 import tactic.observe
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 quantifierfree 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 quantifierfree
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[ts]
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
polyrith
Attempts to prove polynomial equality goals through polynomial arithmetic
on the hypotheses (and additional proof terms if the user specifies them).
It proves the goal by generating an appropriate call to the tactic
linear_combination
. If this call succeeds, the call to linear_combination
is suggested to the user.
polyrith
will use all relevant hypotheses in the local context.polyrith [t1, t2, t3]
will add proof terms t1, t2, t3 to the local context.polyrith only [h1, h2, h3, t1, t2, t3]
will use only local hypothesesh1
,h2
,h3
, and proofst1
,t2
,t3
. It will ignore the rest of the local context.
Notes:
 This tactic only works with a working internet connection, since it calls Sage using the SageCell web API at https://sagecell.sagemath.org/. Many thanks to the Sage team and organization for allowing this use.
 This tactic assumes that the user has
python3
installed and available on the path. (Test by opening a terminal and executingpython3 version
.) It also assumes that therequests
library is installed:python3 m pip install requests
.
Examples:
example (x y : ℚ) (h1 : x*y + 2*x = 1) (h2 : x = y) :
x*y = 2*y + 1 :=
by polyrith
 Try this: linear_combination h1  2 * h2
example (x y z w : ℚ) (hzw : z = w) : x*z + 2*y*z = x*w + 2*y*w :=
by polyrith
 Try this: linear_combination (2 * y + x) * hzw
constant scary : ∀ a b : ℚ, a + b = 0
example (a b c d : ℚ) (h : a + b = 0) (h2: b + c = 0) : a + b + c + d = 0 :=
by polyrith only [scary c d, h]
 Try this: linear_combination scary c d + h
```
Related declarations
Import using
 import tactic.polyrith
 import tactic
positivity
Tactic solving goals of the form 0 ≤ x
, 0 < x
and x ≠ 0
. The tactic works recursively
according to the syntax of the expression x
, if the atoms composing the expression all have
numeric lower bounds which can be proved positive/nonnegative/nonzero by norm_num
. This tactic
either closes the goal or fails.
Examples:
example {a : ℤ} (ha : 3 < a) : 0 ≤ a ^ 3 + a := by positivity
example {a : ℤ} (ha : 1 < a) : 0 < (3:ℤ) + a := by positivity
example {b : ℤ} : 0 ≤ max (3) (b ^ 2) := by positivity
```
Related declarations
Import using
 import tactic.positivity
 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
qify
The qify
tactic is used to shift propositions from ℕ
or ℤ
to ℚ
.
This is often useful since ℚ
has wellbehaved division and subtraction.
example (a b c : ℕ) (x y z : ℤ) (h : ¬ x*y*z < 0) : c < a + 3*b :=
begin
qify,
qify at h,
/
h : ¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
/
end
qify
can be given extra lemmas to use in simplification. This is especially useful in the
presence of subtraction and division: passing ≤
or ∣
arguments will allow push_cast
to do more work.
example (a b c : ℕ) (h : a  b < c) (hab : b ≤ a) : false :=
begin
qify [hab] at h,
/ h : ↑a  ↑b < ↑c /
end
example (a b c : ℕ) (h : a / b = c) (hab : b ∣ a) : false :=
begin
qify [hab] at h,
/ h : ↑a / ↑b = ↑c /
end
qify
makes use of the @[qify]
attribute to move propositions,
and the push_cast
tactic to simplify the ℚ
valued expressions.
Related declarations
Import using
 import tactic.qify
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 asx
.  A blank
_
, which does nothing (letting the automatic naming system used bycases
name the hypothesis).  A hyphen

, which clears the active hypothesis and any dependents.  The keyword
rfl
, which expects the hypothesis to beh : a = b
, and callssubst
on the hypothesis (which has the effect of replacingb
witha
everywhere or vice versa).  A type ascription
p : ty
, which sets the type of the hypothesis toty
and then matches it againstp
. (Of course,ty
must unify with the actual type ofh
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 isa ∧ b ∧ c
, then the conjunction will be destructured, andp1
will be matched againsta
,p2
againstb
and so on.  A
@
before a tuple pattern as in@⟨p1, p2, p3⟩
will bind all arguments in the constructor, while leaving the@
off will only use the patterns on the explicit arguments.  An alteration pattern
p1  p2  p3
, which matches an inductive type with multiple constructors, or a nested disjunction likea ∨ 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 of 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
rewrite_search
Search for a chain of rewrites to prove an equation or iff statement.
Collects rewrite rules, runs a graph search to find a chain of rewrites to prove the current target, and generates a string explanation for it.
Takes an optional list of rewrite rules specified in the same way as the rw
tactic accepts.
Related declarations
Import using
 import tactic.rewrite_search.frontend
ring
Tactic for solving equations in the language of commutative (semi)rings.
ring!
will use a more aggressive reducibility setting to identify atoms.
If the goal is not solvable, it falls back to rewriting all ring expressions
into a normal form, with a suggestion to use ring_nf
instead, if this is the intent.
See also ring1
, which is the same as ring
but without the fallback behavior.
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 typeascripting 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.
See also tactic.interactive.swap
, which moves the n
th goal to the front.
Related declarations
Import using
 import tactic.interactive
 import tactic.basic
rsuffices
The rsuffices
tactic is an alternative version of suffices
, that allows the usage
of any syntax that would be valid in an obtain
block. This tactic just calls obtain
on the expression, and then rotate 1
.
Related declarations
Import using
 import tactic.rcases
 import tactic.basic
rsufficesI
The rsufficesI
tactic is an instancecache aware version of rsuffices
; it resets the instance
cache on the resulting goals.
Related declarations
Import using
 import tactic.rcases
 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 subgoal.
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 nondependent 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 nondependent 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 (nondependent 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 ofe
usingrules
, then try to close the goal usinge
.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 hypothesisthis
if present in the context, then try to close the goal using theassumption
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 backtracking 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
, orcongr_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 subgoals
 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 byget_goals
whensolve_by_elim
started (but which may by now have been partially solved by previousapply
steps). If theaccept
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
. Takes an optional ignored tactic block.
The ignored tactic block is useful for "commenting out" part of a proof during development:
begin
split,
sorry { expensive_tactic },
end
```
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 nondependent 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 ifthenelseexpressions 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 iteexpressions, then split_ifs
will split them all,
starting with a topmost one whose condition does not contain another
iteexpression.
split_ifs at *
splits all iteexpressions 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
withsqueeze_simp
(the space helps avoid the replacement ofsimp
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
withsimp
to remove the occurrences ofsqueeze_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 assqueeze_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'
If the expression q
is a local variable with type x = t
or t = x
, where x
is a local
constant, tactic.interactive.subst' q
substitutes x
by t
everywhere in the main goal and
then clears q
.
If q
is another local variable, then we find a local constant with type q = t
or t = q
and
substitute t
for q
.
Like tactic.interactive.subst
, but fails with a nicer error message if the substituted variable is
a local definition. It is trickier to fix this in core, since tactic.is_local_def
is in mathlib.
Related declarations
Import using
 import tactic.interactive
 import tactic.basic
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
.
suggest using h₁ h₂
will only show solutions that make use of the local hypotheses h₁
and h₂
.
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.
See also tactic.interactive.rotate
, which moves the first n
goals to the back.
Related declarations
Import using
 import tactic.interactive
 import tactic.basic
swap_var
swap_var [x y, P ↔ Q]
swaps the names x
and y
, P
and Q
.
Such a swapping can be used as a weak wlog
if the tactic proofs use the same names.
example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q :=
begin
split,
work_on_goal 1 { swap_var [P Q] },
all_goals { exact ‹P› }
end
Related declarations
Import using
 import tactic.swap_var
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 "transportbyhand" at the end of test/equiv_rw.lean
,
which transport
is an abstraction of.)
Related declarations
Import using
 import tactic.transport
 import tactic
triv
Tries to solve the goal using a canonical proof of true
or the reflexivity
tactic.
Unlike trivial
or trivial'
, does not the contradiction
tactic.
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
trivial'
A weaker version of trivial
that tries to solve the goal using a canonical proof of true
or the
reflexivity
tactic (unfolding only reducible
constants, so can fail faster than trivial
),
and otherwise tries the contradiction
tactic.
Related declarations
Import using
 import tactic.interactive
 import tactic.basic
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
, callingfapply trunc.lift_on e
, and usingintro
andclear
afterwards to make the goals look like we usedinduction
,  otherwise, falling through to
trunc.rec_on
, and in the new invariance goal callingcases h_p
on the uselessh_p : true
hypothesis, and then attempting to simplify theeq.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 coercionrelated 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 firstorder 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
thenn = m
.  Substitution: if
x = e
for some hypothesisx
, thenx
is replaced bye
everywhere.  Noconfusion:
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
butt
andu
are already definitionally equal, then this equation is removed.  Downgrading of heterogeneous equations: if
t == u
butt
andu
have the same type (up to definitional equality), then the equation is replaced byt = 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 trivial'
, 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 casesplitting tactics:
Related declarations
Import using
 imported by default
wlog
wlog h : P
will add an assumption h : P
to the main goal,
and add a side goal that requires showing that the case h : ¬ P
can be reduced to the case
where P
holds (typically by symmetry).
The side goal will be at the top of the stack. In this side goal, there will be two assumptions:
h : ¬ P
: the assumption thatP
does not holdthis
: which is the statement that in the old contextP
suffices to prove the goal. By default, the namethis
is used, but the idiomwith H
can be added to specify the name:wlog h : P with H
.
Typically, it is useful to use the variant wlog h : P generalizing x y
,
to revert certain parts of the context before creating the new goal.
In this way, the wlogclaim this
can be applied to x
and y
in different orders
(exploiting symmetry, which is the typical use case).
By default, the entire context is reverted.
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 wellbehaved 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