with_annotate_state stx t
annotates the lexical range of stx : Syntax
with
the initial and final state of running tactic t
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Introduces one or more hypotheses, optionally naming and/or patternmatching them.
For each hypothesis to be introduced, the remaining main goal's target type must
be a let
or function type.
intro
by itself introduces one anonymous hypothesis, which can be accessed by e.g.assumption
.intro x y
introduces two hypotheses and names them. Individual hypotheses can be anonymized via_
, or matched against a pattern: ... ⊢ α × β → ... intro (a, b)  ..., a : α, b : β ⊢ ...
 Alternatively,
intro
can be combined with pattern matching much likefun
:intro  n + 1, 0 => tac  ...
Equations
 One or more equations did not get rendered due to their size.
Instances For
Introduces zero or more hypotheses, optionally naming them.

intros
is equivalent to repeatedly applyingintro
until the goal is not an obvious candidate forintro
, which is to say that so long as the goal is alet
or a pi type (e.g. an implication, function, or universal quantifier), theintros
tactic will introduce an anonymous hypothesis. This tactic does not unfold definitions. 
intros x y ...
is equivalent tointro x y ...
, introducing hypotheses for each supplied argument and unfolding definitions as necessary. Each argument can be either an identifier or a_
. An identifier indicates a name to use for the corresponding introduced hypothesis, and a_
indicates that the hypotheses should be introduced anonymously.
Examples #
Basic properties:
def AllEven (f : Nat → Nat) := ∀ n, f n % 2 = 0
 Introduces the two obvious hypotheses automatically
example : ∀ (f : Nat → Nat), AllEven f → AllEven (fun k => f (k + 1)) := by
intros
/ Tactic state
f✝ : Nat → Nat
a✝ : AllEven f✝
⊢ AllEven fun k => f✝ (k + 1) /
sorry
 Introduces exactly two hypotheses, naming only the first
example : ∀ (f : Nat → Nat), AllEven f → AllEven (fun k => f (k + 1)) := by
intros g _
/ Tactic state
g : Nat → Nat
a✝ : AllEven g
⊢ AllEven fun k => g (k + 1) /
sorry
 Introduces exactly three hypotheses, which requires unfolding `AllEven`
example : ∀ (f : Nat → Nat), AllEven f → AllEven (fun k => f (k + 1)) := by
intros f h n
/ Tactic state
f : Nat → Nat
h : AllEven f
n : Nat
⊢ (fun k => f (k + 1)) n % 2 = 0 /
apply h
Implications:
example (p q : Prop) : p → q → p := by
intros
/ Tactic state
a✝¹ : p
a✝ : q
⊢ p /
assumption
Let bindings:
example : let n := 1; let k := 2; n + k = 3 := by
intros
/ n✝ : Nat := 1
k✝ : Nat := 2
⊢ n✝ + k✝ = 3 /
rfl
Equations
 One or more equations did not get rendered due to their size.
Instances For
rename t => x
renames the most recent hypothesis whose type matches t
(which may contain placeholders) to x
, or fails if no such hypothesis could be found.
Equations
 One or more equations did not get rendered due to their size.
Instances For
clear x...
removes the given hypotheses, or fails if there are remaining
references to a hypothesis.
Equations
 One or more equations did not get rendered due to their size.
Instances For
subst x...
substitutes each x
with e
in the goal if there is a hypothesis
of type x = e
or e = x
.
If x
is itself a hypothesis of type y = e
or e = y
, y
is substituted instead.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Applies subst
to all hypotheses of the form h : x = t
or h : t = x
.
Equations
 Lean.Parser.Tactic.substVars = Lean.ParserDescr.node `Lean.Parser.Tactic.substVars 1024 (Lean.ParserDescr.nonReservedSymbol "subst_vars" false)
Instances For
assumption
tries to solve the main goal using a hypothesis of compatible type, or else fails.
Note also the ‹t›
term notation, which is a shorthand for show t by assumption
.
Equations
 Lean.Parser.Tactic.assumption = Lean.ParserDescr.node `Lean.Parser.Tactic.assumption 1024 (Lean.ParserDescr.nonReservedSymbol "assumption" false)
Instances For
contradiction
closes the main goal if its hypotheses are "trivially contradictory".
 Inductive type/family with no applicable constructors
example (h : False) : p := by contradiction
 Injectivity of constructors
example (h : none = some true) : p := by contradiction 
 Decidable false proposition
example (h : 2 + 2 = 3) : p := by contradiction
 Contradictory hypotheses
example (h : p) (h' : ¬ p) : q := by contradiction
 Other simple contradictions such as
example (x : Nat) (h : x ≠ x) : p := by contradiction
Equations
 Lean.Parser.Tactic.contradiction = Lean.ParserDescr.node `Lean.Parser.Tactic.contradiction 1024 (Lean.ParserDescr.nonReservedSymbol "contradiction" false)
Instances For
Changes the goal to False
, retaining as much information as possible:
 If the goal is
False
, do nothing.  If the goal is an implication or a function type, introduce the argument and restart.
(In particular, if the goal is
x ≠ y
, introducex = y
.)  Otherwise, for a propositional goal
P
, replace it with¬ ¬ P
(attempting to find aDecidable
instance, but otherwise falling back to working classically) and introduce¬ P
.  For a nonpropositional goal use
False.elim
.
Equations
 Lean.Parser.Tactic.falseOrByContra = Lean.ParserDescr.node `Lean.Parser.Tactic.falseOrByContra 1024 (Lean.ParserDescr.nonReservedSymbol "false_or_by_contra" false)
Instances For
apply e
tries to match the current goal against the conclusion of e
's type.
If it succeeds, then the tactic returns as many subgoals as the number of premises that
have not been fixed by type inference or type class resolution.
Nondependent premises are added before dependent ones.
The apply
tactic uses higherorder pattern matching, type class resolution,
and firstorder unification with dependent types.
Equations
 One or more equations did not get rendered due to their size.
Instances For
exact e
closes the main goal if its target type matches that of e
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
refine e
behaves like exact e
, except that named (?x
) or unnamed (?_
)
holes in e
that are not solved by unification with the main goal's target type
are converted into new goals, using the hole's name, if any, as the goal case name.
Equations
 One or more equations did not get rendered due to their size.
Instances For
exfalso
converts a goal ⊢ tgt
into ⊢ False
by applying False.elim
.
Equations
 Lean.Parser.Tactic.tacticExfalso = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticExfalso 1024 (Lean.ParserDescr.nonReservedSymbol "exfalso" false)
Instances For
If the main goal's target type is an inductive type, constructor
solves it with
the first matching constructor, or else fails.
Equations
 Lean.Parser.Tactic.constructor = Lean.ParserDescr.node `Lean.Parser.Tactic.constructor 1024 (Lean.ParserDescr.nonReservedSymbol "constructor" false)
Instances For
Applies the second constructor when the goal is an inductive type with exactly two constructors, or fails otherwise.
example : True ∨ False := by
left
trivial
Equations
 Lean.Parser.Tactic.left = Lean.ParserDescr.node `Lean.Parser.Tactic.left 1024 (Lean.ParserDescr.nonReservedSymbol "left" false)
Instances For
Applies the second constructor when the goal is an inductive type with exactly two constructors, or fails otherwise.
example {p q : Prop} (h : q) : p ∨ q := by
right
exact h
Equations
 Lean.Parser.Tactic.right = Lean.ParserDescr.node `Lean.Parser.Tactic.right 1024 (Lean.ParserDescr.nonReservedSymbol "right" false)
Instances For
case tag => tac
focuses on the goal with case nametag
and solves it usingtac
, or else fails.case tag x₁ ... xₙ => tac
additionally renames then
most recent hypotheses with inaccessible names to the given names.case tag₁  tag₂ => tac
is equivalent to(case tag₁ => tac); (case tag₂ => tac)
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
case'
is similar to the case tag => tac
tactic, but does not ensure the goal
has been solved after applying tac
, nor admits the goal if tac
failed.
Recall that case
closes the goal using sorry
when tac
fails, and
the tactic execution is not interrupted.
Equations
 One or more equations did not get rendered due to their size.
Instances For
next => tac
focuses on the next goal and solves it using tac
, or else fails.
next x₁ ... xₙ => tac
additionally renames the n
most recent hypotheses with
inaccessible names to the given names.
Equations
 One or more equations did not get rendered due to their size.
Instances For
all_goals tac
runs tac
on each goal, concatenating the resulting goals, if any.
Equations
 One or more equations did not get rendered due to their size.
Instances For
any_goals tac
applies the tactic tac
to every goal, and succeeds if at
least one application succeeds.
Equations
 One or more equations did not get rendered due to their size.
Instances For
focus tac
focuses on the main goal, suppressing all other goals, and runs tac
on it.
Usually · tac
, which enforces that the goal is closed by tac
, should be preferred.
Equations
 One or more equations did not get rendered due to their size.
Instances For
skip
does nothing.
Equations
 Lean.Parser.Tactic.skip = Lean.ParserDescr.node `Lean.Parser.Tactic.skip 1024 (Lean.ParserDescr.nonReservedSymbol "skip" false)
Instances For
done
succeeds iff there are no remaining goals.
Equations
 Lean.Parser.Tactic.done = Lean.ParserDescr.node `Lean.Parser.Tactic.done 1024 (Lean.ParserDescr.nonReservedSymbol "done" false)
Instances For
trace_state
displays the current state in the info view.
Equations
 Lean.Parser.Tactic.traceState = Lean.ParserDescr.node `Lean.Parser.Tactic.traceState 1024 (Lean.ParserDescr.nonReservedSymbol "trace_state" false)
Instances For
trace msg
displays msg
in the info view.
Equations
 One or more equations did not get rendered due to their size.
Instances For
fail_if_success t
fails if the tactic t
succeeds.
Equations
 One or more equations did not get rendered due to their size.
Instances For
(tacs)
executes a list of tactics in sequence, without requiring that
the goal be closed at the end like · tacs
. Like by
itself, the tactics
can be either separated by newlines or ;
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
with_reducible tacs
executes tacs
using the reducible transparency setting.
In this setting only definitions tagged as [reducible]
are unfolded.
Equations
 One or more equations did not get rendered due to their size.
Instances For
with_reducible_and_instances tacs
executes tacs
using the .instances
transparency setting.
In this setting only definitions tagged as [reducible]
or type class instances are unfolded.
Equations
 One or more equations did not get rendered due to their size.
Instances For
with_unfolding_all tacs
executes tacs
using the .all
transparency setting.
In this setting all definitions that are not opaque are unfolded.
Equations
 One or more equations did not get rendered due to their size.
Instances For
first  tac  ...
runs each tac
until one succeeds, or else fails.
Equations
 One or more equations did not get rendered due to their size.
Instances For
rotate_left n
rotates goals to the left by n
. That is, rotate_left 1
takes the main goal and puts it to the back of the subgoal list.
If n
is omitted, it defaults to 1
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Rotate the goals to the right by n
. That is, take the goal at the back
and push it to the front n
times. If n
is omitted, it defaults to 1
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
try tac
runs tac
and succeeds even if tac
failed.
Equations
 One or more equations did not get rendered due to their size.
Instances For
tac <;> tac'
runs tac
on the main goal and tac'
on each produced goal,
concatenating all goals produced by tac'
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
eq_refl
is equivalent to exact rfl
, but has a few optimizations.
Equations
 Lean.Parser.Tactic.eqRefl = Lean.ParserDescr.node `Lean.Parser.Tactic.eqRefl 1024 (Lean.ParserDescr.nonReservedSymbol "eq_refl" false)
Instances For
rfl
tries to close the current goal using reflexivity.
This is supposed to be an extensible tactic and users can add their own support
for new reflexive relations.
Remark: rfl
is an extensible tactic. We later add macro_rules
to try different
reflexivity theorems (e.g., Iff.rfl
).
Equations
 Lean.Parser.Tactic.tacticRfl = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticRfl 1024 (Lean.ParserDescr.nonReservedSymbol "rfl" false)
Instances For
rfl'
is similar to rfl
, but disables smart unfolding and unfolds all kinds of definitions,
theorems included (relevant for declarations defined by wellfounded recursion).
Equations
 Lean.Parser.Tactic.tacticRfl' = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticRfl' 1024 (Lean.ParserDescr.nonReservedSymbol "rfl'" false)
Instances For
ac_rfl
proves equalities up to application of an associative and commutative operator.
instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl
Equations
 Lean.Parser.Tactic.acRfl = Lean.ParserDescr.node `Lean.Parser.Tactic.acRfl 1024 (Lean.ParserDescr.nonReservedSymbol "ac_rfl" false)
Instances For
The sorry
tactic closes the goal using sorryAx
. This is intended for stubbing out incomplete
parts of a proof while still having a syntactically correct proof skeleton. Lean will give
a warning whenever a proof uses sorry
, so you aren't likely to miss it, but
you can double check if a theorem depends on sorry
by using
#print axioms my_thm
and looking for sorryAx
in the axiom list.
Equations
 Lean.Parser.Tactic.tacticSorry = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticSorry 1024 (Lean.ParserDescr.nonReservedSymbol "sorry" false)
Instances For
admit
is a shorthand for exact sorry
.
Equations
 Lean.Parser.Tactic.tacticAdmit = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticAdmit 1024 (Lean.ParserDescr.nonReservedSymbol "admit" false)
Instances For
infer_instance
is an abbreviation for exact inferInstance
.
It synthesizes a value of any target type by typeclass inference.
Equations
 Lean.Parser.Tactic.tacticInfer_instance = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticInfer_instance 1024 (Lean.ParserDescr.nonReservedSymbol "infer_instance" false)
Instances For
Optional configuration option for tactics
Equations
 One or more equations did not get rendered due to their size.
Instances For
The *
location refers to all hypotheses and the goal.
Equations
 Lean.Parser.Tactic.locationWildcard = Lean.ParserDescr.nodeWithAntiquot "locationWildcard" `Lean.Parser.Tactic.locationWildcard (Lean.ParserDescr.symbol " *")
Instances For
A hypothesis location specification consists of 1 or more hypothesis references
and optionally ⊢
denoting the goal.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Location specifications are used by many tactics that can operate on either the hypotheses or the goal. It can have one of the forms:
 'empty' is not actually present in this syntax, but most tactics use
(location)?
matchers. It means to target the goal only. at h₁ ... hₙ
: target the hypothesesh₁
, ...,hₙ
at h₁ h₂ ⊢
: target the hypothesesh₁
andh₂
, and the goalat *
: target all hypotheses and the goal
Equations
 One or more equations did not get rendered due to their size.
Instances For
If thm
is a theorem a = b
, then as a rewrite rule,
thm
means to replacea
withb
, and← thm
means to replaceb
witha
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
rewrite [e]
applies identity e
as a rewrite rule to the target of the main goal.
If e
is preceded by left arrow (←
or <
), the rewrite is applied in the reverse direction.
If e
is a defined constant, then the equational theorems associated with e
are used.
This provides a convenient way to unfold e
.
rewrite [e₁, ..., eₙ]
applies the given rules sequentially.rewrite [e] at l
rewritese
at location(s)l
, wherel
is either*
or a list of hypotheses in the local context. In the latter case, a turnstile⊢
or
can also be used, to signify the target of the goal.
Using rw (config := {occs := .pos L}) [e]
,
where L : List Nat
, you can control which "occurrences" are rewritten.
(This option applies to each rule, so usually this will only be used with a single rule.)
Occurrences count from 1
.
At each allowed occurrence, arguments of the rewrite rule e
may be instantiated,
restricting which later rewrites can be found.
(Disallowed occurrences do not result in instantiation.)
{occs := .neg L}
allows skipping specified occurrences.
Equations
 One or more equations did not get rendered due to their size.
Instances For
rw
is like rewrite
, but also tries to close the goal by "cheap" (reducible) rfl
afterwards.
Equations
 One or more equations did not get rendered due to their size.
Instances For
rwa
calls rw
, then closes any remaining goals using assumption
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The injection
tactic is based on the fact that constructors of inductive data
types are injections.
That means that if c
is a constructor of an inductive datatype, and if (c t₁)
and (c t₂)
are two terms that are equal then t₁
and t₂
are equal too.
If q
is a proof of a statement of conclusion t₁ = t₂
, then injection applies
injectivity to derive the equality of all arguments of t₁
and t₂
placed in
the same positions. For example, from (a::b) = (c::d)
we derive a=c
and b=d
.
To use this tactic t₁
and t₂
should be constructor applications of the same constructor.
Given h : a::b = c::d
, the tactic injection h
adds two new hypothesis with types
a = c
and b = d
to the main goal.
The tactic injection h with h₁ h₂
uses the names h₁
and h₂
to name the new hypotheses.
Equations
 One or more equations did not get rendered due to their size.
Instances For
injections
applies injection
to all hypotheses recursively
(since injection
can produce new hypotheses). Useful for destructing nested
constructor equalities like (a::b::c) = (d::e::f)
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The discharger clause of simp
and related tactics.
This is a tactic used to discharge the side conditions on conditional rewrite rules.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Use this rewrite rule before entering the subterms
Equations
 Lean.Parser.Tactic.simpPre = Lean.ParserDescr.nodeWithAntiquot "simpPre" `Lean.Parser.Tactic.simpPre (Lean.ParserDescr.symbol "↓")
Instances For
Use this rewrite rule after entering the subterms
Equations
 Lean.Parser.Tactic.simpPost = Lean.ParserDescr.nodeWithAntiquot "simpPost" `Lean.Parser.Tactic.simpPost (Lean.ParserDescr.symbol "↑")
Instances For
A simp lemma specification is:
 optional
↑
or↓
to specify use before or after entering the subterm  optional
←
to use the lemma backward thm
for the theorem to rewrite with
Equations
 One or more equations did not get rendered due to their size.
Instances For
An erasure specification thm
says to remove thm
from the simp set
Equations
 One or more equations did not get rendered due to their size.
Instances For
The simp lemma specification *
means to rewrite with all hypotheses
Equations
 Lean.Parser.Tactic.simpStar = Lean.ParserDescr.nodeWithAntiquot "simpStar" `Lean.Parser.Tactic.simpStar (Lean.ParserDescr.symbol "*")
Instances For
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 givenhᵢ
's, where thehᵢ
's are expressions. If anhᵢ
is a defined constantf
, then the equational lemmas associated withf
are used. This provides a convenient way to unfoldf
.simp [*]
simplifies the main goal target using the lemmas tagged with the attribute[simp]
and all hypotheses.simp only [h₁, h₂, ..., hₙ]
is likesimp [h₁, h₂, ..., hₙ]
but does not use[simp]
lemmas.simp [id₁, ..., idₙ]
simplifies the main goal target using the lemmas tagged with the attribute[simp]
, but removes the ones namedidᵢ
.simp at h₁ h₂ ... hₙ
simplifies the hypothesesh₁ : T₁
...hₙ : Tₙ
. If the target or another hypothesis depends onhᵢ
, a new simplified hypothesishᵢ
is introduced, but the old one remains in the local context.simp at *
simplifies all the hypotheses and the target.simp [*] at *
simplifies target and all (propositional) hypotheses using the other hypotheses.
Equations
 One or more equations did not get rendered due to their size.
Instances For
simp_all
is a stronger version of simp [*] at *
where the hypotheses and target
are simplified multiple times until no simplification is applicable.
Only nondependent propositional hypotheses are considered.
Equations
 One or more equations did not get rendered due to their size.
Instances For
A simpArg
is either a *
, lemma
or a simp lemma specification
(which includes the ↑
↓
←
specifications for pre, post, reverse rewriting).
Equations
Instances For
The common arguments of simp?
and simp?!
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
simp?
takes the same arguments as simp
, but reports an equivalent call to simp only
that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp?  prints "Try this: simp only [ite_true]"
This command can also be used in simp_all
and dsimp
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
simp?
takes the same arguments as simp
, but reports an equivalent call to simp only
that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp?  prints "Try this: simp only [ite_true]"
This command can also be used in simp_all
and dsimp
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The common arguments of simp_all?
and simp_all?!
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
simp?
takes the same arguments as simp
, but reports an equivalent call to simp only
that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp?  prints "Try this: simp only [ite_true]"
This command can also be used in simp_all
and dsimp
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
simp?
takes the same arguments as simp
, but reports an equivalent call to simp only
that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp?  prints "Try this: simp only [ite_true]"
This command can also be used in simp_all
and dsimp
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The common arguments of dsimp?
and dsimp?!
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
simp?
takes the same arguments as simp
, but reports an equivalent call to simp only
that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp?  prints "Try this: simp only [ite_true]"
This command can also be used in simp_all
and dsimp
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
simp?
takes the same arguments as simp
, but reports an equivalent call to simp only
that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp?  prints "Try this: simp only [ite_true]"
This command can also be used in simp_all
and dsimp
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The arguments to the simpa
family tactics.
Equations
 One or more equations did not get rendered due to their size.
Instances For
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.
Equations
 One or more equations did not get rendered due to their size.
Instances For
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.
Equations
 One or more equations did not get rendered due to their size.
Instances For
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.
Equations
 One or more equations did not get rendered due to their size.
Instances For
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.
Equations
 One or more equations did not get rendered due to their size.
Instances For
delta id1 id2 ...
deltaexpands the definitions id1
, id2
, ....
This is a lowlevel tactic, it will expose how recursive definitions have been
compiled by Lean.
Equations
 One or more equations did not get rendered due to their size.
Instances For
For nonrecursive definitions, this tactic is identical to delta
.
For definitions by pattern matching, it uses "equation lemmas" which are
autogenerated for each match arm.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Auxiliary macro for lifting have/suffices/let/...
It makes sure the "continuation" ?_
is the main goal after refining.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The have
tactic is for adding hypotheses to the local context of the main goal.
have h : t := e
adds the hypothesish : t
ife
is a term of typet
.have h := e
uses the type ofe
fort
.have : t := e
andhave := e
usethis
for the name of the hypothesis.have pat := e
for a patternpat
is equivalent tomatch e with  pat => _
, where_
stands for the tactics that follow this one. It is convenient for types that have only one applicable constructor. For example, givenh : p ∧ q ∧ r
,have ⟨h₁, h₂, h₃⟩ := h
produces the hypothesesh₁ : p
,h₂ : q
, andh₃ : r
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Given a main goal ctx ⊢ t
, suffices h : t' from e
replaces the main goal with ctx ⊢ t'
,
e
must have type t
in the context ctx, h : t'
.
The variant suffices h : t' by tac
is a shorthand for suffices h : t' from by tac
.
If h :
is omitted, the name this
is used.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The let
tactic is for adding definitions to the local context of the main goal.
let x : t := e
adds the definitionx : t := e
ife
is a term of typet
.let x := e
uses the type ofe
fort
.let : t := e
andlet := e
usethis
for the name of the hypothesis.let pat := e
for a patternpat
is equivalent tomatch e with  pat => _
, where_
stands for the tactics that follow this one. It is convenient for types that let only one applicable constructor. For example, givenp : α × β × γ
,let ⟨x, y, z⟩ := p
produces the local variablesx : α
,y : β
, andz : γ
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
show t
finds the first goal whose target unifies with t
. It makes that the main goal,
performs the unification, and replaces the target with the unified version of t
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
let rec f : t := e
adds a recursive definition f
to the current goal.
The syntax is the same as termmode let rec
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Similar to refine_lift
, but using refine'
Equations
 One or more equations did not get rendered due to their size.
Instances For
Similar to have
, but using refine'
Equations
 One or more equations did not get rendered due to their size.
Instances For
Similar to have
, but using refine'
Equations
 One or more equations did not get rendered due to their size.
Instances For
Similar to let
, but using refine'
Equations
 One or more equations did not get rendered due to their size.
Instances For
The left hand side of an induction arm,  foo a b c
or  @foo a b c
where foo
is a constructor of the inductive type and a b c
are the arguments
to the constructor.
Equations
 One or more equations did not get rendered due to their size.
Instances For
In induction alternative, which can have 1 or more cases on the left
and _
, ?_
, or a tactic sequence after the =>
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
After with
, there is an optional tactic that runs on all branches, and
then a list of alternatives.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Assuming x
is a variable in the local context with an inductive type,
induction x
applies induction on x
to the main goal,
producing one goal for each constructor of the inductive type,
in which the target is replaced by a general instance of that constructor
and an inductive hypothesis is added for each recursive argument to the constructor.
If the type of an element in the local context depends on x
,
that element is reverted and reintroduced afterward,
so that the inductive hypothesis incorporates that hypothesis as well.
For example, given n : Nat
and a goal with a hypothesis h : P n
and target Q n
,
induction n
produces one goal with hypothesis h : P 0
and target Q 0
,
and one goal with hypotheses h : P (Nat.succ a)
and ih₁ : P a → Q a
and target Q (Nat.succ a)
.
Here the names a
and ih₁
are chosen automatically and are not accessible.
You can use with
to provide the variables names for each constructor.
induction e
, wheree
is an expression instead of a variable, generalizese
in the goal, and then performs induction on the resulting variable.induction e using r
allows the user to specify the principle of induction that should be used. Herer
should be a term whose result type must be of the formC t
, whereC
is a bound variable andt
is a (possibly empty) sequence of bound variablesinduction e generalizing z₁ ... zₙ
, wherez₁ ... zₙ
are variables in the local context, generalizes overz₁ ... zₙ
before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized. Given
x : Nat
,induction x with  zero => tac₁  succ x' ih => tac₂
uses tactictac₁
for thezero
case, andtac₂
for thesucc
case.
Equations
 One or more equations did not get rendered due to their size.
Instances For
A generalize
argument, of the form term = x
or h : term = x
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
generalize ([h :] e = x),+
replaces all occurrencese
s in the main goal with a fresh hypothesisx
s. Ifh
is given,h : e = x
is introduced as well.generalize e = x at h₁ ... hₙ
also generalizes occurrences ofe
insideh₁
, ...,hₙ
.generalize e = x at *
will generalize occurrences ofe
everywhere.
Equations
 One or more equations did not get rendered due to their size.
Instances For
A cases
argument, of the form e
or h : e
(where h
asserts that
e = cᵢ a b
for each constructor cᵢ
of the inductive).
Equations
 One or more equations did not get rendered due to their size.
Instances For
Assuming x
is a variable in the local context with an inductive type,
cases x
splits the main goal, producing one goal for each constructor of the
inductive type, in which the target is replaced by a general instance of that constructor.
If the type of an element in the local context depends on x
,
that element is reverted and reintroduced afterward,
so that the case split affects that hypothesis as well.
cases
detects unreachable cases and closes them automatically.
For example, given n : Nat
and a goal with a hypothesis h : P n
and target Q n
,
cases n
produces one goal with hypothesis h : P 0
and target Q 0
,
and one goal with hypothesis h : P (Nat.succ a)
and target Q (Nat.succ a)
.
Here the name a
is chosen automatically and is not accessible.
You can use with
to provide the variables names for each constructor.
cases e
, wheree
is an expression instead of a variable, generalizese
in the goal, and then cases on the resulting variable. Given
as : List α
,cases as with  nil => tac₁  cons a as' => tac₂
, uses tactictac₁
for thenil
case, andtac₂
for thecons
case, anda
andas'
are used as names for the new variables introduced. cases h : e
, wheree
is a variable or an expression, performs cases one
as above, but also adds a hypothesish : e = ...
to each hypothesis, where...
is the constructor instance for that particular case.
Equations
 One or more equations did not get rendered due to their size.
Instances For
rename_i x_1 ... x_n
renames the last n
inaccessible names using the given names.
Equations
 One or more equations did not get rendered due to their size.
Instances For
repeat tac
repeatedly applies tac
to the main goal until it fails.
That is, if tac
produces multiple subgoals, only subgoals up to the first failure will be visited.
The Std
library provides repeat'
which repeats separately in each subgoal.
Equations
 One or more equations did not get rendered due to their size.
Instances For
trivial
tries different simple tactics (e.g., rfl
, contradiction
, ...)
to close the current goal.
You can use the command macro_rules
to extend the set of tactics used. Example:
macro_rules  `(tactic trivial) => `(tactic simp)
Equations
 Lean.Parser.Tactic.tacticTrivial = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticTrivial 1024 (Lean.ParserDescr.nonReservedSymbol "trivial" false)
Instances For
The split
tactic is useful for breaking nested ifthenelse and match
expressions into separate cases.
For a match
expression with n
cases, the split
tactic generates at most n
subgoals.
For example, given n : Nat
, and a target if n = 0 then Q else R
, split
will generate
one goal with hypothesis n = 0
and target Q
, and a second goal with hypothesis
¬n = 0
and target R
. Note that the introduced hypothesis is unnamed, and is commonly
renamed used the case
or next
tactics.
Equations
 One or more equations did not get rendered due to their size.
Instances For
stop
is a helper tactic for "discarding" the rest of a proof:
it is defined as repeat sorry
.
It is useful when working on the middle of a complex proofs,
and less messy than commenting the remainder of the proof.
Equations
 One or more equations did not get rendered due to their size.
Instances For
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
from arguments a₁
... aₙ
.
The tactic adds a new hypothesis with the same name h := h a₁ ... aₙ
and tries to clear the previous one.
Equations
 One or more equations did not get rendered due to their size.
Instances For
unhygienic tacs
runs tacs
with name hygiene disabled.
This means that tactics that would normally create inaccessible names will instead
make regular variables. Warning: Tactics may change their variable naming
strategies at any time, so code that depends on autogenerated names is brittle.
Users should try not to use unhygienic
if possible.
example : ∀ x : Nat, x = x := by unhygienic
intro  x would normally be intro'd as inaccessible
exact Eq.refl x  refer to x
Equations
 One or more equations did not get rendered due to their size.
Instances For
fail msg
is a tactic that always fails, and produces an error using the given message.
Equations
 One or more equations did not get rendered due to their size.
Instances For
checkpoint tac
acts the same as tac
, but it caches the input and output of tac
,
and if the file is reelaborated and the input matches, the tactic is not rerun and
its effects are reapplied to the state. This is useful for improving responsiveness
when working on a long tactic proof, by wrapping expensive tactics with checkpoint
.
See the save
tactic, which may be more convenient to use.
(TODO: do this automatically and transparently so that users don't have to use this combinator explicitly.)
Equations
 One or more equations did not get rendered due to their size.
Instances For
save
is defined to be the same as skip
, but the elaborator has
special handling for occurrences of save
in tactic scripts and will transform
by tac1; save; tac2
to by (checkpoint tac1); tac2
, meaning that the effect of tac1
will be cached and replayed. This is useful for improving responsiveness
when working on a long tactic proof, by using save
after expensive tactics.
(TODO: do this automatically and transparently so that users don't have to use this combinator explicitly.)
Equations
 Lean.Parser.Tactic.save = Lean.ParserDescr.node `Lean.Parser.Tactic.save 1024 (Lean.ParserDescr.nonReservedSymbol "save" false)
Instances For
The tactic sleep ms
sleeps for ms
milliseconds and does nothing.
It is used for debugging purposes only.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Apply congruence (recursively) to goals of the form ⊢ f as = f bs
and ⊢ HEq (f as) (f bs)
.
The optional parameter is the depth of the recursive applications.
This is useful when congr
is too aggressive in breaking down the goal.
For example, given ⊢ f (g (x + y)) = f (g (y + x))
,
congr
produces the goals ⊢ x = y
and ⊢ y = x
,
while congr 2
produces the intended ⊢ x + y = y + x
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
In tactic mode, if h : t then tac1 else tac2
can be used as alternative syntax for:
by_cases h : t
· tac1
· tac2
It performs case distinction on h : t
or h : ¬t
and tac1
and tac2
are the subproofs.
You can use ?_
or _
for either subproof to delay the goal to after the tactic, but
if a tactic sequence is provided for tac1
or tac2
then it will require the goal to be closed
by the end of the block.
Equations
 One or more equations did not get rendered due to their size.
Instances For
In tactic mode, if t then tac1 else tac2
is alternative syntax for:
by_cases t
· tac1
· tac2
It performs case distinction on h† : t
or h† : ¬t
, where h†
is an anonymous
hypothesis, and tac1
and tac2
are the subproofs. (It doesn't actually use
nondependent if
, since this wouldn't add anything to the context and hence would be
useless for proving theorems. To actually insert an ite
application use
refine if t then ?_ else ?_
.)
Equations
 One or more equations did not get rendered due to their size.
Instances For
The tactic nofun
is shorthand for exact nofun
: it introduces the assumptions, then performs an
empty pattern match, closing the goal if the introduced pattern is impossible.
Equations
 Lean.Parser.Tactic.tacticNofun = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticNofun 1024 (Lean.ParserDescr.nonReservedSymbol "nofun" false)
Instances For
The tactic nomatch h
is shorthand for exact nomatch h
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Acts like have
, but removes a hypothesis with the same name as
this one if possible. For example, if the state is:
f : α → β
h : α
⊢ goal
Then after replace h := f h
the state will be:
f : α → β
h : β
⊢ goal
whereas have h := f h
would result in:
f : α → β
h† : α
h : β
⊢ goal
This can be used to simulate the specialize
and apply at
tactics of Coq.
Equations
 One or more equations did not get rendered due to their size.
Instances For
repeat' tac
runs tac
on all of the goals to produce a new list of goals,
then runs tac
again on all of those goals, and repeats until tac
fails on all remaining goals.
Equations
 One or more equations did not get rendered due to their size.
Instances For
repeat1' tac
applies tac
to main goal at least once. If the application succeeds,
the tactic is applied recursively to the generated subgoals until it eventually fails.
Equations
 One or more equations did not get rendered due to their size.
Instances For
and_intros
applies And.intro
until it does not make progress.
Equations
 Lean.Parser.Tactic.tacticAnd_intros = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticAnd_intros 1024 (Lean.ParserDescr.nonReservedSymbol "and_intros" false)
Instances For
subst_eq
repeatedly substitutes according to the equality proof hypotheses in the context,
replacing the left side of the equality with the right, until no more progress can be made.
Equations
 Lean.Parser.Tactic.substEqs = Lean.ParserDescr.node `Lean.Parser.Tactic.substEqs 1024 (Lean.ParserDescr.nonReservedSymbol "subst_eqs" false)
Instances For
The run_tac doSeq
tactic executes code in TacticM Unit
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
haveI
behaves like have
, but inlines the value instead of producing a let_fun
term.
Equations
 One or more equations did not get rendered due to their size.
Instances For
letI
behaves like let
, but inlines the value instead of producing a let_fun
term.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The omega
tactic, for resolving integer and natural linear arithmetic problems.
It is not yet a full decision procedure (no "dark" or "grey" shadows), but should be effective on many problems.
We handle hypotheses of the form x = y
, x < y
, x ≤ y
, and k ∣ x
for x y
in Nat
or Int
(and k
a literal), along with negations of these statements.
We decompose the sides of the inequalities as linear combinations of atoms.
If we encounter x / k
or x % k
for literal integers k
we introduce new auxiliary variables
and the relevant inequalities.
On the first pass, we do not perform case splits on natural subtraction.
If omega
fails, we recursively perform a case split on
a natural subtraction appearing in a hypothesis, and try again.
The options
omega (config :=
{ splitDisjunctions := true, splitNatSub := true, splitNatAbs := true, splitMinMax := true })
can be used to:
splitDisjunctions
: split any disjunctions found in the context, if the problem is not otherwise solvable.splitNatSub
: for each appearance of((a  b : Nat) : Int)
, split ona ≤ b
if necessary.splitNatAbs
: for each appearance ofInt.natAbs a
, split on0 ≤ a
if necessary.splitMinMax
: for each occurrence ofmin a b
, split onmin a b = a ∨ min a b = b
Currently, all of these are on by default.
Equations
 One or more equations did not get rendered due to their size.
Instances For
bv_omega
is omega
with an additional preprocessor that turns statements about BitVec
into statements about Nat
.
Currently the preprocessor is implemented as try simp only [bv_toNat] at *
.
bv_toNat
is a @[simp]
attribute that you can (cautiously) add to more theorems.
Equations
 Lean.Parser.Tactic.tacticBv_omega = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticBv_omega 1024 (Lean.ParserDescr.nonReservedSymbol "bv_omega" false)
Instances For
assumption_mod_cast
is a variant of assumption
that solves the goal
using a hypothesis. Unlike assumption
, it first preprocesses the goal and
each hypothesis to move casts as far outwards as possible, so it can be used
in more situations.
Concretely, it runs norm_cast
on the goal. For each local hypothesis h
, it also
normalizes h
with norm_cast
and tries to use that to close the goal.
Equations
 One or more equations did not get rendered due to their size.
Instances For
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 even in situations where nonterminal simp
calls are discouraged (because of fragility),
norm_cast
is considered safe.
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
There are also variants of exact
, apply
, rw
, and assumption
that
work modulo norm_cast
 in other words, they apply norm_cast
to make
them more flexible. They are called exact_mod_cast
, apply_mod_cast
,
rw_mod_cast
, and assumption_mod_cast
, respectively.
Writing exact_mod_cast h
and apply_mod_cast h
will normalize casts
in the goal and h
before using exact h
or apply h
.
Writing assumption_mod_cast
will normalize casts in the goal and, for
every hypothesis h
in the context, it will try to normalize casts in h
and use
exact h
.
rw_mod_cast
acts like the rw
tactic but it applies norm_cast
between steps.
See also push_cast
, which moves casts inwards rather than lifting them outwards.
Equations
 One or more equations did not get rendered due to their size.
Instances For
push_cast
rewrites the goal to move casts inward, 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
Equations
 One or more equations did not get rendered due to their size.
Instances For
norm_cast_add_elim foo
registers foo
as an elimlemma in norm_cast
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
symm
applies to a goal whose target has the formt ~ u
where~
is a symmetric relation, that is, a relation which has a symmetry lemma tagged with the attribute [symm]. It replaces the target withu ~ t
.symm at h
will rewrite a hypothesish : t ~ u
toh : u ~ t
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
For every hypothesis h : a ~ b
where a @[symm]
lemma is available,
add a hypothesis h_symm : b ~ a
.
Equations
 Lean.Parser.Tactic.symmSaturate = Lean.ParserDescr.node `Lean.Parser.Tactic.symmSaturate 1024 (Lean.ParserDescr.nonReservedSymbol "symm_saturate" false)
Instances For
Syntax for omitting a local hypothesis in solve_by_elim
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Syntax for including all local hypotheses in solve_by_elim
.
Equations
 Lean.Parser.Tactic.SolveByElim.star = Lean.ParserDescr.nodeWithAntiquot "star" `Lean.Parser.Tactic.SolveByElim.star (Lean.ParserDescr.symbol "*")
Instances For
Syntax for adding or removing a term, or *
, in solve_by_elim
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Syntax for adding and removing terms in solve_by_elim
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Syntax for using all lemmas labelled with an attribute in solve_by_elim
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
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 maxDepth
(defaults to 6) 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
,
congrFun
and congrArg
.
The assumptions can be modified with similar syntax as for simp
:
solve_by_elim [h₁, h₂, ..., hᵣ]
also applies the given expressions.solve_by_elim only [h₁, h₂, ..., hᵣ]
does not include the local context,rfl
,trivial
,congrFun
, orcongrArg
unless they are explicitly included.solve_by_elim [h₁, ... hₙ]
removes the given local hypotheses.solve_by_elim using [a₁, ...]
uses all lemmas which have been labelled with the attributesaᵢ
(these attributes must be created usingregister_label_attr
).
solve_by_elim*
tries to solve all goals together, using backtracking if a solution for one goal
makes other goals impossible.
(Adding or removing local hypotheses may not be wellbehaved when starting with multiple goals.)
Optional arguments passed via a configuration argument as solve_by_elim (config := { ... })
maxDepth
: number of attempts at discharging generated subgoalssymm
: adds all hypotheses derived bysymm
(defaults totrue
).exfalso
: allow callingexfalso
and trying again ifsolve_by_elim
fails (defaults totrue
).transparency
: change the transparency mode when callingapply
. Defaults to.default
, but it is often useful to change to.reducible
, so semireducible definitions will not be unfolded when trying to apply a lemma.
See also the doccomment for Std.Tactic.BacktrackConfig
for the options
proc
, suspend
, and discharge
which allow further customization of solve_by_elim
.
Both apply_assumption
and apply_rules
are implemented via these hooks.
Equations
 One or more equations did not get rendered due to their size.
Instances For
apply_assumption
looks for an assumption of the form ... → ∀ _, ... → head
where head
matches the current goal.
You can specify additional rules to apply using apply_assumption [...]
.
By default apply_assumption
will also try rfl
, trivial
, congrFun
, and congrArg
.
If you don't want these, or don't want to use all hypotheses, use apply_assumption only [...]
.
You can use apply_assumption [h]
to omit a local hypothesis.
You can use apply_assumption using [a₁, ...]
to use all lemmas which have been labelled
with the attributes aᵢ
(these attributes must be created using register_label_attr
).
apply_assumption
will use consequences of local hypotheses obtained via symm
.
If apply_assumption
fails, it will call exfalso
and try again.
Thus if there is an assumption of the form P → ¬ Q
, the new tactic state
will have two goals, P
and Q
.
You can pass a further configuration via the syntax apply_rules (config := {...}) lemmas
.
The options supported are the same as for solve_by_elim
(and include all the options for apply
).
Equations
 One or more equations did not get rendered due to their size.
Instances For
apply_rules [l₁, l₂, ...]
tries to solve the main goal by iteratively
applying the list of lemmas [l₁, l₂, ...]
or by applying a local hypothesis.
If apply
generates new goals, apply_rules
iteratively tries to solve those goals.
You can use apply_rules [h]
to omit a local hypothesis.
apply_rules
will also use rfl
, trivial
, congrFun
and congrArg
.
These can be disabled, as can local hypotheses, by using apply_rules only [...]
.
You can use apply_rules using [a₁, ...]
to use all lemmas which have been labelled
with the attributes aᵢ
(these attributes must be created using register_label_attr
).
You can pass a further configuration via the syntax apply_rules (config := {...})
.
The options supported are the same as for solve_by_elim
(and include all the options for apply
).
apply_rules
will try calling symm
on hypotheses and exfalso
on the goal as needed.
This can be disabled with apply_rules (config := {symm := false, exfalso := false})
.
You can bound the iteration depth using the syntax apply_rules (config := {maxDepth := n})
.
Unlike solve_by_elim
, apply_rules
does not perform backtracking, and greedily applies
a lemma from the list until it gets stuck.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Searches environment for definitions or theorems that can solve the goal using exact
with conditions resolved by solve_by_elim
.
The optional using
clause provides identifiers in the local context that must be
used by exact?
when closing the goal. This is most useful if there are multiple
ways to resolve the goal, and one wants to guide which lemma is used.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Searches environment for definitions or theorems that can refine the goal using apply
with conditions resolved when possible with solve_by_elim
.
The optional using
clause provides identifiers in the local context that must be
used when closing the goal.
Equations
 One or more equations did not get rendered due to their size.
Instances For
show_term tac
runs tac
, then prints the generated term in the form
"exact X Y Z" or "refine X ?_ Z" if there are remaining subgoals.
(For some tactics, the printed term will not be human readable.)
Equations
 One or more equations did not get rendered due to their size.
Instances For
show_term e
elaborates e
, then prints the generated term.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The command by?
will print a suggestion for replacing the proof block with a proof term
using show_term
.
Equations
 Lean.Parser.Tactic.by? = Lean.ParserDescr.node `Lean.Parser.Tactic.by? 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "by?") (Lean.ParserDescr.const `tacticSeq))
Instances For
Theorems tagged with the simp
attribute are used by the simplifier
(i.e., the simp
tactic, and its variants) to simplify expressions occurring in your goals.
We call theorems tagged with the simp
attribute "simp theorems" or "simp lemmas".
Lean maintains a database/index containing all active simp theorems.
Here is an example of a simp theorem.
@[simp] theorem ne_eq (a b : α) : (a ≠ b) = Not (a = b) := rfl
This simp theorem instructs the simplifier to replace instances of the term
a ≠ b
(e.g. x + 0 ≠ y
) with Not (a = b)
(e.g., Not (x + 0 = y)
).
The simplifier applies simp theorems in one direction only:
if A = B
is a simp theorem, then simp
replaces A
s with B
s,
but it doesn't replace B
s with A
s. Hence a simp theorem should have the
property that its righthand side is "simpler" than its lefthand side.
In particular, =
and ↔
should not be viewed as symmetric operators in this situation.
The following would be a terrible simp theorem (if it were even allowed):
@[simp] lemma mul_right_inv_bad (a : G) : 1 = a * a⁻¹ := ...
Replacing 1 with a * a⁻¹ is not a sensible default direction to travel. Even worse would be a theorem that causes expressions to grow without bound, causing simp to loop forever.
By default the simplifier applies simp
theorems to an expression e
after its subexpressions have been simplified.
We say it performs a bottomup simplification.
You can instruct the simplifier to apply a theorem before its subexpressions
have been simplified by using the modifier ↓
. Here is an example
@[simp↓] theorem not_and_eq (p q : Prop) : (¬ (p ∧ q)) = (¬p ∨ ¬q) :=
When multiple simp theorems are applicable, the simplifier uses the one with highest priority. If there are several with the same priority, it is uses the "most recent one". Example:
@[simp high] theorem cond_true (a b : α) : cond true a b = a := rfl
@[simp low+1] theorem or_true (p : Prop) : (p ∨ True) = True :=
propext < Iff.intro (fun _ => trivial) (fun _ => Or.inr trivial)
@[simp 100] theorem ite_self {d : Decidable c} (a : α) : ite c a a = a := by
cases d <;> rfl
Equations
 One or more equations did not get rendered due to their size.
Instances For
The possible norm_cast
kinds: elim
, move
, or squash
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The norm_cast
attribute should be given to lemmas that describe the
behaviour of a coercion with respect to an operator, a relation, or a particular
function.
It only concerns equality or iff lemmas involving ↑
, ⇑
and ↥
, describing the behavior of
the coercion functions.
It does not apply to the explicit functions that define the coercions.
Examples:
@[norm_cast] theorem coe_nat_inj' {m n : ℕ} : (↑m : ℤ) = ↑n ↔ m = n
@[norm_cast] theorem coe_int_denom (n : ℤ) : (n : ℚ).denom = 1
@[norm_cast] theorem cast_id : ∀ n : ℚ, ↑n = n
@[norm_cast] theorem coe_nat_add (m n : ℕ) : (↑(m + n) : ℤ) = ↑m + ↑n
@[norm_cast] theorem cast_coe_nat (n : ℕ) : ((n : ℤ) : α) = n
@[norm_cast] theorem cast_one : ((1 : ℚ) : α) = 1
Lemmas tagged with @[norm_cast]
are classified into three categories: move
, elim
, and
squash
. They are classified roughly as follows:
 elim lemma: LHS has 0 head coes and ≥ 1 internal coe
 move lemma: LHS has 1 head coe and 0 internal coes, RHS has 0 head coes and ≥ 1 internal coes
 squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
norm_cast
uses move
and elim
lemmas to factor coercions toward the root of an expression
and to cancel them from both sides of an equation or relation. It uses squash
lemmas to clean
up the result.
It is typically not necessary to specify these categories, as norm_cast
lemmas are
automatically classified by default. The automatic classification can be overridden by
giving an optional elim
, move
, or squash
parameter to the attribute.
@[simp, norm_cast elim] lemma nat_cast_re (n : ℕ) : (n : ℂ).re = n := by
rw [← of_real_nat_cast, of_real_re]
Don't do this unless you understand what you are doing.
Equations
 One or more equations did not get rendered due to their size.
Instances For
‹t›
resolves to an (arbitrary) hypothesis of type t
.
It is useful for referring to hypotheses without accessible names.
t
may contain holes that are solved by unification with the expected type;
in particular, ‹_›
is a shortcut for by assumption
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
get_elem_tactic_trivial
is an extensible tactic automatically called
by the notation arr[i]
to prove any side conditions that arise when
constructing the term (e.g. the index is in bounds of the array).
The default behavior is to just try trivial
(which handles the case
where i < arr.size
is in the context) and simp_arith
and omega
(for doing linear arithmetic in the index).
Equations
 tacticGet_elem_tactic_trivial = Lean.ParserDescr.node `tacticGet_elem_tactic_trivial 1024 (Lean.ParserDescr.nonReservedSymbol "get_elem_tactic_trivial" false)
Instances For
get_elem_tactic
is the tactic automatically called by the notation arr[i]
to prove any side conditions that arise when constructing the term
(e.g. the index is in bounds of the array). It just delegates to
get_elem_tactic_trivial
and gives a diagnostic error message otherwise;
users are encouraged to extend get_elem_tactic_trivial
instead of this tactic.
Equations
 tacticGet_elem_tactic = Lean.ParserDescr.node `tacticGet_elem_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "get_elem_tactic" false)
Instances For
The syntax arr[i]
gets the i
'th element of the collection arr
.
If there are proof side conditions to the application, they will be automatically
inferred by the get_elem_tactic
tactic.
The actual behavior of this class is typedependent, but here are some important implementations:
arr[i] : α
wherearr : Array α
andi : Nat
ori : USize
: does array indexing with no bounds check and a proof side goali < arr.size
.l[i] : α
wherel : List α
andi : Nat
: index into a list, with proof side goali < l.length
.stx[i] : Syntax
wherestx : Syntax
andi : Nat
: get a syntax argument, no side goal (returns.missing
out of range)
There are other variations on this syntax:
arr[i]
: proves the proof side goal byget_elem_tactic
arr[i]!
: panics if the side goal is falsearr[i]?
: returnsnone
if the side goal is falsearr[i]'h
: usesh
to prove the side goal
Equations
 One or more equations did not get rendered due to their size.
Instances For
The syntax arr[i]
gets the i
'th element of the collection arr
.
If there are proof side conditions to the application, they will be automatically
inferred by the get_elem_tactic
tactic.
The actual behavior of this class is typedependent, but here are some important implementations:
arr[i] : α
wherearr : Array α
andi : Nat
ori : USize
: does array indexing with no bounds check and a proof side goali < arr.size
.l[i] : α
wherel : List α
andi : Nat
: index into a list, with proof side goali < l.length
.stx[i] : Syntax
wherestx : Syntax
andi : Nat
: get a syntax argument, no side goal (returns.missing
out of range)
There are other variations on this syntax:
arr[i]
: proves the proof side goal byget_elem_tactic
arr[i]!
: panics if the side goal is falsearr[i]?
: returnsnone
if the side goal is falsearr[i]'h
: usesh
to prove the side goal
Equations
 One or more equations did not get rendered due to their size.
Instances For
Searches environment for definitions or theorems that can be substituted in for `exact?% to solve the goal.
Equations
 Lean.Parser.Syntax.exact? = Lean.ParserDescr.node `Lean.Parser.Syntax.exact? 1024 (Lean.ParserDescr.symbol "exact?%")