classical

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

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

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

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

intro

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

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:

example (p q : Prop) : p → q → p := byp:Propq:Prop⊢ p → q → p introsp:Propq:Propa✝¹:pa✝:q⊢ p /- Tactic state a✝¹ : p a✝ : q ⊢ p -/ assumptionAll goals completed! 🐙

Let-bindings:

example : let n := 1; let k := 2; n + k = 3 := by⊢ let n := 1; let k := 2; n + k = 3 introsn✝:Nat := 1k✝:Nat := 2⊢ n✝ + k✝ = 3 /- n✝ : Nat := 1 k✝ : Nat := 2 ⊢ n✝ + k✝ = 3 -/ rflAll goals completed! 🐙

Does not unfold definitions:

def AllEven (f : Nat → Nat) := ∀ n, f n % 2 = 0 declaration uses `sorry`example : ∀ (f : Nat → Nat), AllEven f → AllEven (fun k => f (k + 1)) := by⊢ ∀ (f : Nat → Nat), AllEven f → AllEven fun k => f (k + 1) introsf✝:Nat → Nata✝:AllEven f✝⊢ AllEven fun k => f✝ (k + 1) /- Tactic state f✝ : Nat → Nat a✝ : AllEven f✝ ⊢ AllEven fun k => f✝ (k + 1) -/ sorryAll goals completed! 🐙

rintro

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

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

rfl

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'

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

apply_rfl

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

The refl attribute marks a lemma as a proof of reflexivity for some relation. These lemmas are used by the rfl, rfl', and apply_rfl tactics.

attr ::= ...
    | refl

symm

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

symm_saturate

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

The symm attribute marks a lemma as a proof that a relation is symmetric. These lemmas are used by the symm and symm_saturate tactics.

attr ::= ...
    | symm

calc

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.

ac_nf

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.

instance : Std.Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩ instance : Std.Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩ example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := bya:Natb:Natc:Natd:Nat⊢ a + b + c + d = d + (b + c) + a ac_nfAll goals completed! 🐙 -- goal: a + (b + (c + d)) = a + (b + (c + d))

ac_nf0

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

exact

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

apply

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

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.