classical tacs runs tacs in a scope where Classical.propDecidable is a low priority local instance.

Note that classical is a scoping tactic: it adds the instance only within the scope of the tactic.

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.

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

exists e₁, e₂, ... is shorthand for refine ⟨e₁, e₂, ...⟩; try trivial. It is useful for existential goals.

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

• intro by itself introduces one anonymous hypothesis, which can be accessed by e.g. assumption. It is equivalent to intro _.

• intro x y introduces two hypotheses and names them. Individual hypotheses can be anonymized via _, given a type ascription, or matched against a pattern:

  intro (a, b) -- ..., a : α, b : β ⊢ ...

• intro rfl is short for intro h; subst h, if h is an equality where the left-hand or right-hand side is a variable.

• Alternatively, intro can be combined with pattern matching much like fun:

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

intros repeatedly applies intro to introduce zero or more hypotheses until the goal is no longer a binding expression (i.e., a universal quantifier, function type, implication, or have/let), without performing any definitional reductions (no unfolding, beta, eta, etc.). The introduced hypotheses receive inaccessible (hygienic) names.

intros x y z is equivalent to intro x y z and exists only for historical reasons. The intro tactic should be preferred in this case.

Properties and relations

• intros succeeds even when it introduces no hypotheses.

• repeat intro is like intros, but it performs definitional reductions to expose binders, and as such it may introduce more hypotheses than intros.

• intros is equivalent to intro _ _ … _, with the fewest trailing _ placeholders needed so that the goal is no longer a binding expression. The trailing introductions do not perform any definitional reductions.

Examples

Implications:

Let-bindings:

Does not unfold definitions:

The rintro tactic is a combination of the intros tactic with rcases to allow for destructuring patterns while introducing variables. See rcases for a description of supported patterns. For example, rintro (a | ⟨b, c⟩) ⟨d, e⟩ will introduce two variables, and then do case splits on both of them producing two subgoals, one with variables a d e and the other with b c d e.

rintro, unlike rcases, also supports the form (x y : ty) for introducing and type-ascripting multiple variables at once, similar to binders.

This tactic applies to a goal whose target has the form x ~ x, where ~ is equality, heterogeneous equality or any relation that has a reflexivity lemma tagged with the attribute @[refl].

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

The same as rfl, but without trying eq_refl at the end.

refl 属性将引理标记为某些关系的自反性证明。 这些引理由 rfl、rfl' 和 apply_rfl策略使用。

attr ::= ...
    | refl

• symm 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.

• symm at h will rewrite a hypothesis h : t ~ u to h : u ~ t.

For every hypothesis h : a ~ b where a @[symm] lemma is available, add a hypothesis h_symm : b ~ a.

symm 属性将引理标记为关系对称的证明。 这些引理由 symm 和 symm_saturate策略使用。

attr ::= ...
    | symm

Step-wise reasoning over transitive relations.

calc
  a = b := pab
  b = c := pbc
  ...
  y = z := pyz

proves a = z from the given step-wise proofs. = can be replaced with any relation implementing the typeclass Trans. Instead of repeating the right- hand sides, subsequent left-hand sides can be replaced with _.

calc
  a = b := pab
  _ = c := pbc
  ...
  _ = z := pyz

It is also possible to write the first relation as <lhs>\n _ = <rhs> := <proof>. This is useful for aligning relation symbols, especially on longer identifiers:

calc abc
  _ = bce := pabce
  _ = cef := pbcef
  ...
  _ = xyz := pwxyz

calc works as a term, as a tactic or as a conv tactic.

See Theorem Proving in Lean 4 for more information.

Transitive chaining of proofs, used e.g. by calc.

It takes two relations r and s as "input", and produces an "output" relation t, with the property that r a b and s b c implies t a c. The calc tactic uses this so that when it sees a chain with a ≤ b and b < c it knows that this should be a proof of a < c because there is an instance Trans (·≤·) (·<·) (·<·).

Instance Constructor

Trans.mk.{u, v, w, u_1, u_2, u_3}

Methods

trans : {a : α} → {b : β} → {c : γ} → r a b → s b c → t a c

ac_nf normalizes equalities up to application of an associative and commutative operator.

• ac_nf normalizes all hypotheses and the goal target of the goal.

• ac_nf at l normalizes 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.

Implementation of ac_nf (the full ac_nf calls trivial afterwards).

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

apply e tries to match the current goal against the conclusion of e's type. If it succeeds, then the tactic returns as many subgoals as the number of premises that have not been fixed by type inference or type class resolution. Non-dependent premises are added before dependent ones.

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

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.

refine' e behaves like refine e, except that unsolved placeholders (_) and implicit parameters are also converted into new goals.

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, or congrArg 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 attributes aᵢ (these attributes must be created using register_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 well-behaved when starting with multiple goals.)

Optional arguments passed via a configuration argument as solve_by_elim (config := { ... })

• maxDepth: number of attempts at discharging generated subgoals

• symm: adds all hypotheses derived by symm (defaults to true).

• exfalso: allow calling exfalso and trying again if solve_by_elim fails (defaults to true).

• transparency: change the transparency mode when calling apply. 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 doc-comment for Lean.Meta.Tactic.Backtrack.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.

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.

as_aux_lemma => tac does the same as tac, except that it wraps the resulting expression into an auxiliary lemma. In some cases, this significantly reduces the size of expressions because the proof term is not duplicated.

exfalso converts a goal ⊢ tgt into ⊢ False by applying False.elim.

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

• Inductive type/family with no applicable constructors

  example (h : False) : p := byp:Sort ?u.3h:False⊢ p contradictionAll goals completed! 🐙

• Injectivity of constructors

  example (h : none = some true) : p := byp:Sort ?u.6h:none = some true⊢ p contradictionAll goals completed! 🐙 --

• Decidable false proposition

  example (h : 2 + 2 = 3) : p := byp:Sort ?u.13h:2 + 2 = 3⊢ p contradictionAll goals completed! 🐙

• Contradictory hypotheses

  example (h : p) (h' : ¬ p) : q := byp:Propq:Sort ?u.5h:ph':¬p⊢ q contradictionAll goals completed! 🐙

• Other simple contradictions such as

  example (x : Nat) (h : x ≠ x) : p := byp:Sort ?u.5x:Nath:x ≠ x⊢ p contradictionAll goals completed! 🐙

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, introduce x = y.)

• Otherwise, for a propositional goal P, replace it with ¬ ¬ P (attempting to find a Decidable instance, but otherwise falling back to working classically) and introduce ¬ P.

• For a non-propositional goal use False.elim.

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.

• change tgt' will change the goal from tgt to tgt', assuming these are definitionally equal.

• change t' at h will change hypothesis h : t to have type t', assuming assuming t and t' are definitionally equal.

• change a with b will change occurrences of a to b in the goal, assuming a and b are definitionally equal.

• change a with b at h similarly changes a to b in the type of hypothesis h.

• generalize ([h :] e = x),+ replaces all occurrences es in the main goal with a fresh hypothesis xs. If h is given, h : e = x is introduced as well.

• generalize e = x at h₁ ... hₙ also generalizes occurrences of e inside h₁, ..., hₙ.

• generalize e = x at * will generalize occurrences of e everywhere.

specialize h a₁ ... aₙ is equivalent to replace h := h a₁ ... aₙ. It specializes the local hypothesis h by instantiating universal quantifications and implications using the concrete terms a₁ ... aₙ. The tactic adds a new hypothesis with the same name and tries to remove the original h if possible.

Example: given h : ∀ (n : Nat), p n → q n and h' : p 2, then specialize h 2 h' replaces h with h : q 2.

The tactic also supports instantiating particular universal quantifiers using named argument syntax. Example: given h : ∀ (m n : Nat), p m n, then specialize h (n := 2) replaces h with h : ∀ (m : Nat), p m 2.

The obtain tactic is a combination of have and rcases. See rcases for a description of supported patterns.

obtain ⟨patt⟩ : type := proof

is equivalent to

have h : type := proof
rcases h with ⟨patt⟩

If ⟨patt⟩ is omitted, rcases will try to infer the pattern.

If type is omitted, := proof is required.

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.

show_term tac runs tac, then prints the generated term in the form "exact X Y Z" or "refine X ?_ Z" (prefixed by expose_names if necessary) if there are remaining subgoals.

(For some tactics, the printed term will not be human readable.)

The norm_cast family of tactics is used to normalize certain coercions (casts) in expressions.

• norm_cast normalizes casts in the target.

• norm_cast at h normalizes casts in hypothesis h.

The tactic is basically a version of simp with a specific set of lemmas to move casts upwards in the expression. Therefore even in situations where non-terminal simp calls are discouraged (because of fragility), norm_cast is considered to be 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 basic tactics that use norm_cast to normalize expressions during their operation, to make them more flexible about the expressions they accept (we say that it is a tactic modulo the effects of norm_cast):

• exact_mod_cast for exact and apply_mod_cast for apply. 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.

• rw_mod_cast for rw. It applies norm_cast between rewrites.

• assumption_mod_cast for assumption. This is effectively norm_cast at *; assumption, but more efficient. It normalizes casts in the goal and, for every hypothesis h in the context, it will try to normalize casts in h and use exact h.

See also push_cast, which moves casts inwards rather than lifting them outwards.

push_cast rewrites the goal to move certain coercions (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.

• push_cast moves casts inward in the goal.

• push_cast at h moves casts inward in the hypothesis h. It can be used with extra simp lemmas with, for example, push_cast [Int.add_zero].

Example:

See also norm_cast.

Normalize casts in the goal and the given expression, then close the goal with exact.

Normalize casts in the goal and the given expression, then apply the expression to the goal.

Rewrites with the given rules, normalizing casts prior to each step.

assumption_mod_cast is a variant of assumption that solves the goal using a hypothesis. Unlike assumption, it first pre-processes 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.

Extracts let and have expressions from within the target or a local hypothesis, introducing new local definitions.

• extract_lets extracts all the lets from the target.

• extract_lets x y z extracts all the lets from the target and uses x, y, and z for the first names. Using _ for a name leaves it unnamed.

• extract_lets x y z at h operates on the local hypothesis h instead of the target.

For example, given a local hypotheses if the form h : let x := v; b x, then extract_lets z at h introduces a new local definition z := v and changes h to be h : b z.

Lifts let and have expressions within a term as far out as possible. It is like extract_lets +lift, but the top-level lets at the end of the procedure are not extracted as local hypotheses.

• lift_lets lifts let expressions in the target.

• lift_lets at h lifts let expressions at the given local hypothesis.

For example,

example : (let x := 1; x) = 1 := by
  lift_lets
  -- ⊢ let x := 1; x = 1
  ...

Transforms let expressions into have expressions when possible.

• let_to_have transforms lets in the target.

• let_to_have at h transforms lets in the given local hypothesis.

• clear_value x... clears the values of the given local definitions. A local definition x : α := v becomes a hypothesis x : α.

• clear_value (h : x = _) adds a hypothesis h : x = v before clearing the value of x. This is short for have h : x = v := rfl; clear_value x. Any value definitionally equal to v can be used in place of _.

• clear_value * clears values of all hypotheses that can be cleared. Fails if none can be cleared.

These syntaxes can be combined. For example, clear_value x y * ensures that x and y are cleared while trying to clear all other local definitions, and clear_value (hx : x = _) y * with hx does the same while first adding the hx : x = v hypothesis.

Applies extensionality lemmas that are registered with the @[ext] attribute.

• ext pat* applies extensionality theorems as much as possible, using the patterns pat* to introduce the variables in extensionality theorems using rintro. For example, the patterns are used to name the variables introduced by lemmas such as funext.

• Without patterns,ext applies extensionality lemmas as much as possible but introduces anonymous hypotheses whenever needed.

• ext pat* : n applies ext theorems only up to depth n.

The ext1 pat* tactic is like ext pat* except that it only applies a single extensionality theorem.

Unused patterns will generate warning. Patterns that don't match the variables will typically result in the introduction of anonymous hypotheses.

ext1 pat* is like ext pat* except that it only applies a single extensionality theorem rather than recursively applying as many extensionality theorems as possible.

The pat* patterns are processed using the rintro tactic. If no patterns are supplied, then variables are introduced anonymously using the intros tactic.

Apply a single extensionality theorem to the current goal.

Apply function extensionality and introduce new hypotheses. The tactic funext will keep applying 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. Patterns can be used like in the intro tactic. Example, given a goal

  |-  ((fun x : Nat × Bool => ...) = (fun x => ...))

funext (a, b) applies funext once and performs pattern matching on the newly introduced pair.

grind is a tactic inspired by modern SMT solvers. Picture a virtual whiteboard: every time grind discovers a new equality, inequality, or logical fact, it writes it on the board, groups together terms known to be equal, and lets each reasoning engine read from and contribute to the shared workspace. These engines work together to handle equality reasoning, apply known theorems, propagate new facts, perform case analysis, and run specialized solvers for domains like linear arithmetic and commutative rings.

See the reference manual's chapter on grind for more information.

grind is not designed for goals whose search space explodes combinatorially, think large pigeonhole instances, graph‑coloring reductions, high‑order N‑queens boards, or a 200‑variable Sudoku encoded as Boolean constraints. Such encodings require thousands (or millions) of case‑splits that overwhelm grind’s branching search.

For bit‑level or combinatorial problems, consider using bv_decide. bv_decide calls a state‑of‑the‑art SAT solver (CaDiCaL) and then returns a compact, machine‑checkable certificate.

Equality reasoning

grind uses congruence closure to track equalities between terms. When two terms are known to be equal, congruence closure automatically deduces equalities between more complex expressions built from them. For example, if a = b, then congruence closure will also conclude that f a = f b for any function f. This forms the foundation for efficient equality reasoning in grind. Here is an example:

Applying theorems using E-matching

To apply existing theorems, grind uses a technique called E-matching, which finds matches for known theorem patterns while taking equalities into account. Combined with congruence closure, E-matching helps grind discover non-obvious consequences of theorems and equalities automatically.

Consider the following functions and theorems:

The theorem gf asserts that g (f x) = x for all natural numbers x. The attribute [grind =] instructs grind to use the left-hand side of the equation, g (f x), as a pattern for E-matching. Suppose we now have a goal involving:

example {a b} (h : f b = a) : g a = b := by
  grind

Although g a is not an instance of the pattern g (f x), it becomes one modulo the equation f b = a. By substituting a with f b in g a, we obtain the term g (f b), which matches the pattern g (f x) with the assignment x := b. Thus, the theorem gf is instantiated with x := b, and the new equality g (f b) = b is asserted. grind then uses congruence closure to derive the implied equality g a = g (f b) and completes the proof.

The pattern used to instantiate theorems affects the effectiveness of grind. For example, the pattern g (f x) is too restrictive in the following case: the theorem gf will not be instantiated because the goal does not even contain the function symbol g.

example (h₁ : f b = a) (h₂ : f c = a) : b = c := by
  grind

You can use the command grind_pattern to manually select a pattern for a given theorem. In the following example, we instruct grind to use f x as the pattern, allowing it to solve the goal automatically:

grind_pattern gf => f x

example {a b c} (h₁ : f b = a) (h₂ : f c = a) : b = c := by
  grind

You can enable the option trace.grind.ematch.instance to make grind print a trace message for each theorem instance it generates.

You can also specify a multi-pattern to control when grind should apply a theorem. A multi-pattern requires that all specified patterns are matched in the current context before the theorem is applied. This is useful for theorems such as transitivity rules, where multiple premises must be simultaneously present for the rule to apply. The following example demonstrates this feature using a transitivity axiom for a binary relation R:

By specifying the multi-pattern R x y, R y z, we instruct grind to instantiate Rtrans only when both R x y and R y z are available in the context. In the example, grind applies Rtrans to derive R a c from R a b and R b c, and can then repeat the same reasoning to deduce R a d from R a c and R c d.

Instead of using grind_pattern to explicitly specify a pattern, you can use the @[grind] attribute or one of its variants, which will use a heuristic to generate a (multi-)pattern. The complete list is available in the reference manual. The main ones are:

• @[grind →] will select a multi-pattern from the hypotheses of the theorem (i.e. it will use the theorem for forwards reasoning). In more detail, it will traverse the hypotheses of the theorem from left-to-right, and each time it encounters a minimal indexable (i.e. has a constant as its head) subexpression which "covers" (i.e. fixes the value of) an argument which was not previously covered, it will add that subexpression as a pattern, until all arguments have been covered.

• @[grind ←] will select a multi-pattern from the conclusion of theorem (i.e. it will use the theorem for backwards reasoning). This may fail if not all the arguments to the theorem appear in the conclusion.

• @[grind] will traverse the conclusion and then the hypotheses left-to-right, adding patterns as they increase the coverage, stopping when all arguments are covered.

• @[grind =] checks that the conclusion of the theorem is an equality, and then uses the left-hand-side of the equality as a pattern. This may fail if not all of the arguments appear in the left-hand-side.

Here is the previous example again but using the attribute [grind →]

To control theorem instantiation and avoid generating an unbounded number of instances, grind uses a generation counter. Terms in the original goal are assigned generation zero. When grind applies a theorem using terms of generation ≤ n, any new terms it creates are assigned generation n + 1. This limits how far the tactic explores when applying theorems and helps prevent an excessive number of instantiations.

Key options:

• grind (ematch := <num>) controls the number of E-matching rounds.

• grind [<name>, ...] instructs grind to use the declaration name during E-matching.

• grind only [<name>, ...] is like grind [<name>, ...] but does not use theorems tagged with @[grind].

• grind (gen := <num>) sets the maximum generation.

Linear integer arithmetic (lia)

grind can solve goals that reduce to linear integer arithmetic (LIA) using an integrated decision procedure called lia. It understands

• equalities   p = 0

• inequalities  p ≤ 0

• disequalities p ≠ 0

• divisibility  d ∣ p

The solver incrementally assigns integer values to variables; when a partial assignment violates a constraint it adds a new, implied constraint and retries. This model-based search is complete for LIA.

Key options:

• grind -lia disable the solver (useful for debugging)

• grind +qlia accept rational models (shrinks the search space but is incomplete for ℤ)

Examples:

Algebraic solver (ring)

grind ships with an algebraic solver nick-named ring for goals that can be phrased as polynomial equations (or disequations) over commutative rings, semirings, or fields.

Works out of the box All core numeric types and relevant Mathlib types already provide the required type-class instances, so the solver is ready to use in most developments.

What it can decide:

• equalities of the form p = q

• disequalities p ≠ q

• basic reasoning under field inverses (a / b := a * b⁻¹)

• goals that mix ring facts with other grind engines

Key options:

• grind -ring turn the solver off (useful when debugging)

• grind (ringSteps := n) cap the number of steps performed by this procedure.

Examples

Other options

• grind (splits := <num>) caps the depth of the search tree. Once a branch performs num splits grind stops splitting further in that branch.

• grind -splitIte disables case splitting on if-then-else expressions.

• grind -splitMatch disables case splitting on match expressions.

• grind +splitImp instructs grind to split on any hypothesis A → B whose antecedent A is propositional.

• grind -linarith disables the linear arithmetic solver for (ordered) modules and rings.

Additional Examples