#adaptation_note

Adaptation notes are comments that are used to indicate that a piece of code has been changed to accommodate a change in Lean core. They typically require further action/maintenance to be taken in the future.

#check

The #check t tactic elaborates the term t and then pretty prints it with its type as e : ty.

If t is an identifier, then it pretty prints a type declaration form for the global constant t instead. Use #check (t) to pretty print it as an elaborated expression.

Like the #check command, the #check tactic allows stuck typeclass instance problems. These become metavariables in the output.

#count_heartbeats

Count the heartbeats used by a tactic, e.g.: #count_heartbeats simp.

#count_heartbeats!

#count_heartbeats! in tac runs a tactic 10 times, counting the heartbeats used, and logs the range and standard deviation. The tactic #count_heartbeats! n in tac runs it n times instead.

#leansearch

Search LeanSearch from within Lean. Queries should be a string that ends with a . or ?. This works as a command, as a term and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

LeanSearch Search Results • #check Nat.le_of_succ_le_succ • #check Nat.lt_of_succ_lt_succ • #check Nat.succ_lt_succ • #check Nat.succ_le_succ • #check Nat.lt_of_succ_lt • #check Nat.le_succ_of_le#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m." example := LeanSearch Search Results • Nat.le_of_succ_le_succ • Nat.lt_of_succ_lt_succ • Nat.succ_lt_succ • Nat.succ_le_succ • Nat.lt_of_succ_lt • Nat.le_succ_of_le#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m." declaration uses 'sorry'example : 3 ≤ 5 := by⊢ 3 ≤ 5 From: Nat.le_of_succ_le_succ (type: ∀ {n m : Nat}, LE.le n.succ m.succ → LE.le n m) • apply Nat.le_of_succ_le_succ • have : ∀ {n m : Nat}, LE.le n.succ m.succ → LE.le n m := Nat.le_of_succ_le_succFrom: Nat.lt_of_succ_lt_succ (type: ∀ {n m : Nat}, LT.lt n.succ m.succ → LT.lt n m) • apply Nat.lt_of_succ_lt_succ • have : ∀ {n m : Nat}, LT.lt n.succ m.succ → LT.lt n m := Nat.lt_of_succ_lt_succFrom: Nat.succ_lt_succ (type: ∀ {n m : Nat}, LT.lt n m → LT.lt n.succ m.succ) • apply Nat.succ_lt_succ • have : ∀ {n m : Nat}, LT.lt n m → LT.lt n.succ m.succ := Nat.succ_lt_succFrom: Nat.succ_le_succ (type: ∀ {n m : Nat}, LE.le n m → LE.le n.succ m.succ) • apply Nat.succ_le_succ • have : ∀ {n m : Nat}, LE.le n m → LE.le n.succ m.succ := Nat.succ_le_succFrom: Nat.lt_of_succ_lt (type: ∀ {n m : Nat}, LT.lt n.succ m → LT.lt n m) • apply Nat.lt_of_succ_lt • have : ∀ {n m : Nat}, LT.lt n.succ m → LT.lt n m := Nat.lt_of_succ_ltFrom: Nat.le_succ_of_le (type: ∀ {n m : Nat}, LE.le n m → LE.le n m.succ) • apply Nat.le_succ_of_le • have : ∀ {n m : Nat}, LE.le n m → LE.le n m.succ := Nat.le_succ_of_le#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."⊢ 3 ≤ 5 sorryAll goals completed! 🐙

You can modify the LeanSearch URL by setting the LEANSEARCHCLIENT_LEANSEARCH_API_URL environment variable.

#loogle

Search Loogle from within Lean. This can be used as a command, term or tactic as in the following examples. In the case of a tactic, only valid tactics are displayed.

Loogle Search Results • #check List.get • #check List.and • #check List.or • #check List.getLastD • #check List.headD • #check List.flatten#loogle List ?a → ?a example := Loogle Search Results • List.get • List.and • List.or • List.getLastD • List.headD • List.flatten#loogle List ?a → ?a declaration uses 'sorry'example : 3 ≤ 5 := by⊢ 3 ≤ 5 From: Nat.succ_le_succ • apply Nat.succ_le_succ#loogle Nat.succ_le_succ⊢ 3 ≤ 5 sorryAll goals completed! 🐙

Loogle Usage

Loogle finds definitions and lemmas in various ways:

By constant: 🔍 Real.sin finds all lemmas whose statement somehow mentions the sine function.

By lemma name substring: 🔍 "differ" finds all lemmas that have "differ" somewhere in their lemma name.

By subexpression: 🔍 _ * (_ ^ _) finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in 🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map: 🔍 (?a -> ?b) -> List ?a -> List ?b 🔍 List ?a -> (?a -> ?b) -> List ?b

By main conclusion: 🔍 |- tsum _ = _ * tsum _ finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example, 🔍 |- _ < _ → tsum _ < tsum _ will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search 🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _ woould find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

You can modify the Loogle server URL by setting the LEANSEARCHCLIENT_LOOGLE_API_URL environment variable.

#moogle

Search Moogle from within Lean. Queries should be a string that ends with a . or ?. This works as a command, as a term and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

Moogle Search Results • #check Nat.lt • #check Nat.succ_lt_succ • #check Nat.lt_of_succ_lt_succ • #check Nat.lt_of_succ_lt • #check Nat.lt_succ_of_le • #check LT.lt.nat_succ_le#moogle "If a natural number n is less than m, then the successor of n is less than the successor of m." example := Moogle Search Results • Nat.lt • Nat.succ_lt_succ • Nat.lt_of_succ_lt_succ • Nat.lt_of_succ_lt • Nat.lt_succ_of_le • LT.lt.nat_succ_le#moogle "If a natural number n is less than m, then the successor of n is less than the successor of m." declaration uses 'sorry'example : 3 ≤ 5 := by⊢ 3 ≤ 5 From: Nat.lt (type: ℕ → ℕ → Prop) • have : ℕ → ℕ → Prop := Nat.ltFrom: Nat.succ_lt_succ (type: ∀ {n m : ℕ}, n < m → n.succ < m.succ) • apply Nat.succ_lt_succ • have : ∀ {n m : ℕ}, n < m → n.succ < m.succ := Nat.succ_lt_succFrom: Nat.lt_of_succ_lt_succ (type: ∀ {n m : ℕ}, n.succ < m.succ → n < m) • apply Nat.lt_of_succ_lt_succ • have : ∀ {n m : ℕ}, n.succ < m.succ → n < m := Nat.lt_of_succ_lt_succFrom: Nat.lt_of_succ_lt (type: ∀ {n m : ℕ}, n.succ < m → n < m) • apply Nat.lt_of_succ_lt • have : ∀ {n m : ℕ}, n.succ < m → n < m := Nat.lt_of_succ_ltFrom: Nat.lt_succ_of_le (type: ∀ {n m : ℕ}, n ≤ m → n < m.succ) • apply Nat.lt_succ_of_le • have : ∀ {n m : ℕ}, n ≤ m → n < m.succ := Nat.lt_succ_of_leFrom: LT.lt.nat_succ_le (type: ∀ {n m : ℕ}, n < m → n.succ ≤ m) • apply LT.lt.nat_succ_le • have : ∀ {n m : ℕ}, n < m → n.succ ≤ m := LT.lt.nat_succ_le#moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."⊢ 3 ≤ 5 sorryAll goals completed! 🐙

You can modify the Moogle URL by setting the LEANSEARCHCLIENT_MOOGLE_API_URL environment variable.

#search

Search either Moogle or LeanSearch from within Lean, depending on the option leansearchclient.backend. Queries should be a string that ends with a . or ?. This works as a command, as a term and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

#search "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #search "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #search "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

In tactic mode, if the query string is not supplied, then [LeanStateSearch](https://premise-search.com) is queried based on the goal state.

#statesearch

Search LeanStateSearch from within Lean. Your current main goal is sent as query. The revision to search can be set using the statesearch.revision option. The number of results can be set using the statesearch.queries option.

Hint: If you want to modify the query, you need to use the web interface.

set_option statesearch.queries 1
set_option statesearch.revision "v4.16.0"

example : 0 ≤ 1 := by
  #statesearch
  sorry

You can modify the LeanStateSearch URL by setting the LEANSEARCHCLIENT_LEANSTATESEARCH_API_URL environment variable.

(

(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 ;.

<;>

t <;> [t1; t2; ...; tn] focuses on the first goal and applies t, which should result in n subgoals. It then applies each ti to the corresponding goal and collects the resulting subgoals.

<;>

tac <;> tac' runs tac on the main goal and tac' on each produced goal, concatenating all goals produced by tac'.

Lean.Parser.Tactic.introMatch

The tactic

intro
| pat1 => tac1
| pat2 => tac2

is the same as:

intro x
match x with
| pat1 => tac1
| pat2 => tac2

That is, intro can be followed by match arms and it introduces the values while doing a pattern match. This is equivalent to fun with match arms in term mode.

Lean.Parser.Tactic.match

match performs case analysis on one or more expressions. See Induction and Recursion. The syntax for the match tactic is the same as term-mode match, except that the match arms are tactics instead of expressions.

example (n : Nat) : n = n := byn:ℕ⊢ n = n match n with | 0 =>n:ℕ⊢ 0 = 0 rflAll goals completed! 🐙 | i+1 =>n:ℕi:ℕ⊢ i + 1 = i + 1 simpAll goals completed! 🐙

Lean.Parser.Tactic.open

open Foo in tacs (the tactic) acts like open Foo at command level, but it opens a namespace only within the tactics tacs.

Lean.Parser.Tactic.set_option

set_option opt val in tacs (the tactic) acts like set_option opt val at the command level, but it sets the option only within the tactics tacs.

Lean.Parser.Tactic.tacDepIfThenElse

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.

Lean.Parser.Tactic.tacIfThenElse

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

Lean.cdot

·tac focuses on the main goal and tries to solve it using tac, or else fails.

_

_ in tactic position acts like the done tactic: it fails and gives the list of goals if there are any. It is useful as a placeholder after starting a tactic block such as by _ to make it syntactically correct and show the current goal.

abel

Tactic for evaluating equations in the language of additive, commutative monoids and groups.

abel and its variants work as both tactics and conv tactics.

• abel1 fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.

• abel_nf rewrites all group expressions into a normal form.

  • In tactic mode, abel_nf at h can be used to rewrite in a hypothesis.

  • abel_nf (config := cfg) allows for additional configuration:

    • red: the reducibility setting (overridden by !)

    • zetaDelta: if true, local let variables can be unfolded (overridden by !)

    • recursive: if true, abel_nf will also recurse into atoms

• abel!, abel1!, abel_nf! will use a more aggressive reducibility setting to identify atoms.

For example:

example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := byα:Type u_1inst✝:AddCommMonoid αa:αb:α⊢ a + (b + a) = a + a + b abelAll goals completed! 🐙 example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := byα:Type u_1inst✝:AddCommGroup αa:α⊢ 3 • a = a + 2 • a abelAll goals completed! 🐙

Future work

• In mathlib 3, abel accepted additional optional arguments:

  syntax "abel" (&" raw" <|> &" term")? (location)? : tactic
  

  It is undecided whether these features should be restored eventually.

absurd

Given a proof h of p, absurd h changes the goal to ⊢ ¬ p. If p is a negation ¬q then the goal is changed to ⊢ q instead.

ac_change

ac_change g using n is convert_to g using n followed by ac_rfl. It is useful for rearranging/reassociating e.g. sums:

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

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 : 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_nf
 -- goal: a + (b + (c + d)) = a + (b + (c + d))

ac_nf0

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

ac_rfl

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

admit

admit is a synonym for sorry.

aesop

aesop <clause>* tries to solve the current goal by applying a set of rules registered with the @[aesop] attribute. See its README for a tutorial and a reference.

The variant aesop? prints the proof it found as a Try this suggestion.

Clauses can be used to customise the behaviour of an Aesop call. Available clauses are:

• (add <phase> <priority> <builder> <rule>) adds a rule. <phase> is unsafe, safe or norm. <priority> is a percentage for unsafe rules and an integer for safe and norm rules. <rule> is the name of a declaration or local hypothesis. <builder> is the rule builder used to turn <rule> into an Aesop rule. Example: (add unsafe 50% apply Or.inl).

• (erase <rule>) disables a globally registered Aesop rule. Example: (erase Aesop.BuiltinRules.assumption).

• (rule_sets := [<ruleset>,*]) enables or disables named sets of rules for this Aesop call. Example: (rule_sets := [-builtin, MyRuleSet]).

• (config { <opt> := <value> }) adjusts Aesop's search options. See Aesop.Options.

• (simp_config { <opt> := <value> }) adjusts options for Aesop's built-in simp rule. The given options are directly passed to simp. For example, (simp_config := { zeta := false }) makes Aesop use simp (config := { zeta := false }).

aesop?

aesop <clause>* tries to solve the current goal by applying a set of rules registered with the @[aesop] attribute. See its README for a tutorial and a reference.

The variant aesop? prints the proof it found as a Try this suggestion.

Clauses can be used to customise the behaviour of an Aesop call. Available clauses are:

• (add <phase> <priority> <builder> <rule>) adds a rule. <phase> is unsafe, safe or norm. <priority> is a percentage for unsafe rules and an integer for safe and norm rules. <rule> is the name of a declaration or local hypothesis. <builder> is the rule builder used to turn <rule> into an Aesop rule. Example: (add unsafe 50% apply Or.inl).

• (erase <rule>) disables a globally registered Aesop rule. Example: (erase Aesop.BuiltinRules.assumption).

• (rule_sets := [<ruleset>,*]) enables or disables named sets of rules for this Aesop call. Example: (rule_sets := [-builtin, MyRuleSet]).

• (config { <opt> := <value> }) adjusts Aesop's search options. See Aesop.Options.

• (simp_config { <opt> := <value> }) adjusts options for Aesop's built-in simp rule. The given options are directly passed to simp. For example, (simp_config := { zeta := false }) makes Aesop use simp (config := { zeta := false }).

aesop_cat

A thin wrapper for aesop which adds the CategoryTheory rule set and allows aesop to look through semireducible definitions when calling intros. This tactic fails when it is unable to solve the goal, making it suitable for use in auto-params.

aesop_cat?

We also use aesop_cat? to pass along a Try this suggestion when using aesop_cat

aesop_cat_nonterminal

A variant of aesop_cat which does not fail when it is unable to solve the goal. Use this only for exploration! Nonterminal aesop is even worse than nonterminal simp.

aesop_graph

A variant of the aesop tactic for use in the graph library. Changes relative to standard aesop:

• We use the SimpleGraph rule set in addition to the default rule sets.

• We instruct Aesop's intro rule to unfold with default transparency.

• We instruct Aesop to fail if it can't fully solve the goal. This allows us to use aesop_graph for auto-params.

aesop_graph?

Use aesop_graph? to pass along a Try this suggestion when using aesop_graph

aesop_graph_nonterminal

A variant of aesop_graph which does not fail if it is unable to solve the goal. Use this only for exploration! Nonterminal Aesop is even worse than nonterminal simp.

aesop_mat

The aesop_mat tactic attempts to prove a set is contained in the ground set of a matroid. It uses a [Matroid] ruleset, and is allowed to fail.

algebraize

Tactic that, given RingHoms, adds the corresponding Algebra and (if possible) IsScalarTower instances, as well as Algebra corresponding to RingHom properties available as hypotheses.

Example: given f : A →+* B and g : B →+* C, and hf : f.FiniteType, algebraize [f, g] will add the instances Algebra A B, Algebra B C, and Algebra.FiniteType A B.

See the algebraize tag for instructions on what properties can be added.

The tactic also comes with a configuration option properties. If set to true (default), the tactic searches through the local context for RingHom properties that can be converted to Algebra properties. The macro algebraize_only calls algebraize -properties, so in other words it only adds Algebra and IsScalarTower instances.

algebraize_only

Version of algebraize, which only adds Algebra instances and IsScalarTower instances, but does not try to add any instances about any properties tagged with @[algebraize], like for example Finite or IsIntegral.

all_goals

all_goals tac runs tac on each goal, concatenating the resulting goals. If the tactic fails on any goal, the entire all_goals tactic fails.

See also any_goals tac.

and_intros

and_intros applies And.intro until it does not make progress.

any_goals

any_goals tac applies the tactic tac to every goal, concatenating the resulting goals for successful tactic applications. If the tactic fails on all of the goals, the entire any_goals tactic fails.

This tactic is like all_goals try tac except that it fails if none of the applications of tac succeeds.

apply

apply t at i will use forward reasoning with t at the hypothesis i. Explicitly, if t : α₁ → ⋯ → αᵢ → ⋯ → αₙ and i has type αᵢ, then this tactic will add metavariables/goals for any terms of αⱼ for j = 1, …, i-1, then replace the type of i with αᵢ₊₁ → ⋯ → αₙ by applying those metavariables and the original i.

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.

apply

apply (config := cfg) e is like apply e but allows you to provide a configuration cfg : ApplyConfig to pass to the underlying apply operation.

apply?

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.

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

apply_ext_theorem

Apply a single extensionality theorem to the current goal.

apply_fun

Apply a function to an equality or inequality in either a local hypothesis or the goal.

• If we have h : a = b, then apply_fun f at h will replace this with h : f a = f b.

• If we have h : a ≤ b, then apply_fun f at h will replace this with h : f a ≤ f b, and create a subsidiary goal Monotone f. apply_fun will automatically attempt to discharge this subsidiary goal using mono, or an explicit solution can be provided with apply_fun f at h using P, where P : Monotone f.

• If we have h : a < b, then apply_fun f at h will replace this with h : f a < f b, and create a subsidiary goal StrictMono f and behaves as in the previous case.

• If we have h : a ≠ b, then apply_fun f at h will replace this with h : f a ≠ f b, and create a subsidiary goal Injective f and behaves as in the previous two cases.

• If the goal is a ≠ b, apply_fun f will replace this with f a ≠ f b.

• If the goal is a = b, apply_fun f will replace this with f a = f b, and create a subsidiary goal injective f. apply_fun will automatically attempt to discharge this subsidiary goal using local hypotheses, or if f is actually an Equiv, or an explicit solution can be provided with apply_fun f using P, where P : Injective f.

• If the goal is a ≤ b (or similarly for a < b), and f is actually an OrderIso, apply_fun f will replace the goal with f a ≤ f b. If f is anything else (e.g. just a function, or an Equiv), apply_fun will fail.

Typical usage is:

open Function example (X Y Z : Type) (f : X → Y) (g : Y → Z) (H : Injective <| g ∘ f) : Injective f := byX:TypeY:TypeZ:Typef:X → Yg:Y → ZH:Injective (g ∘ f)⊢ Injective f intro x x' hX:TypeY:TypeZ:Typef:X → Yg:Y → ZH:Injective (g ∘ f)x:Xx':Xh:f x = f x'⊢ x = x' apply_fun g at hX:TypeY:TypeZ:Typef:X → Yg:Y → ZH:Injective (g ∘ f)x:Xx':Xh:g (f x) = g (f x')⊢ x = x' exact H hAll goals completed! 🐙

The function f is handled similarly to how it would be handled by refine in that f can contain placeholders. Named placeholders (like ?a or ?_) will produce new goals.

apply_gmonoid_gnpowRec_succ_tac

A tactic to for use as an optional value for GMonoid.gnpow_succ'.

apply_gmonoid_gnpowRec_zero_tac

A tactic to for use as an optional value for GMonoid.gnpow_zero'.

apply_mod_cast

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

apply_rewrite

apply_rewrite [rules] is a shorthand for grewrite +implicationHyp [rules].

apply_rfl

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

apply_rules

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.

apply_rw

apply_rw [rules] is a shorthand for grw +implicationHyp [rules].

arith_mult

arith_mult solves goals of the form IsMultiplicative f for f : ArithmeticFunction R by applying lemmas tagged with the user attribute arith_mult.

arith_mult?

arith_mult solves goals of the form IsMultiplicative f for f : ArithmeticFunction R by applying lemmas tagged with the user attribute arith_mult, and prints out the generated proof term.

array_get_dec

This tactic, added to the decreasing_trivial toolbox, proves that sizeOf arr[i] < sizeOf arr, which is useful for well founded recursions over a nested inductive like inductive T | mk : Array T → T.

array_mem_dec

This tactic, added to the decreasing_trivial toolbox, proves that sizeOf a < sizeOf arr provided that a ∈ arr which is useful for well founded recursions over a nested inductive like inductive T | mk : Array T → T.

as_aux_lemma

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.

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.

assumption'

Try calling assumption on all goals; succeeds if it closes at least one goal.

assumption_mod_cast

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.

attempt_all

Helper internal tactic for implementing the tactic try?.

aux_group₁

Auxiliary tactic for the group tactic. Calls the simplifier only.

aux_group₂

Auxiliary tactic for the group tactic. Calls ring_nf to normalize exponents.

bddDefault

Sets are automatically bounded or cobounded in complete lattices. To use the same statements in complete and conditionally complete lattices but let automation fill automatically the boundedness proofs in complete lattices, we use the tactic bddDefault in the statements, in the form (hA : BddAbove A := by bddDefault).

beta_reduce

beta_reduce at loc completely beta reduces the given location. This also exists as a conv-mode tactic.

This means that whenever there is an applied lambda expression such as (fun x => f x) y then the argument is substituted into the lambda expression yielding an expression such as f y.

bicategory

Use the coherence theorem for bicategories to solve equations in a bicategory, where the two sides only differ by replacing strings of bicategory structural morphisms (that is, associators, unitors, and identities) with different strings of structural morphisms with the same source and target.

That is, bicategory can handle goals of the form a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c' where a = a', b = b', and c = c' can be proved using bicategory_coherence.

bicategory_coherence

Coherence tactic for bicategories. Use pure_coherence instead, which is a frontend to this one.

bicategory_coherence

Close the goal of the form η.hom = θ.hom, where η and θ are 2-isomorphisms made up only of associators, unitors, and identities.

example {B : Type} [Bicategory B] {a : B} :
  (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom := by
  bicategory_coherence

bicategory_nf

Normalize the both sides of an equality.

bitwise_assoc_tac

Proving associativity of bitwise operations in general essentially boils down to a huge case distinction, so it is shorter to use this tactic instead of proving it in the general case.

borelize

The behaviour of borelize α depends on the existing assumptions on α.

• if α is a topological space with instances [MeasurableSpace α] [BorelSpace α], then borelize α replaces the former instance by borel α;

• otherwise, borelize α adds instances borel α : MeasurableSpace α and ⟨rfl⟩ : BorelSpace α.

Finally, borelize α β γ runs borelize α; borelize β; borelize γ.

bound

bound tactic for proving inequalities via straightforward recursion on expression structure.

An example use case is

lemma le_sqr_add (c z : ℝ) (cz : ‖c‖ ≤ ‖z‖) (z3 : 3 ≤ ‖z‖) : 2 * ‖z‖ ≤ ‖z^2 + c‖ := byc:ℝz:ℝcz:‖c‖ ≤ ‖z‖z3:3 ≤ ‖z‖⊢ 2 * ‖z‖ ≤ ‖z ^ 2 + c‖ calc ‖z^2 + c‖ _ ≥ ‖z^2‖ - ‖c‖ := byc:ℝz:ℝcz:‖c‖ ≤ ‖z‖z3:3 ≤ ‖z‖⊢ ‖z ^ 2 + c‖ ≥ ‖z ^ 2‖ - ‖c‖ boundAll goals completed! 🐙 _ ≥ ‖z^2‖ - ‖z‖ := byc:ℝz:ℝcz:‖c‖ ≤ ‖z‖z3:3 ≤ ‖z‖⊢ ‖z ^ 2‖ - ‖c‖ ≥ ‖z ^ 2‖ - ‖z‖ boundAll goals completed! 🐙 _ ≥ (‖z‖ - 1) * ‖z‖ := byc:ℝz:ℝcz:‖c‖ ≤ ‖z‖z3:3 ≤ ‖z‖⊢ ‖z ^ 2‖ - ‖z‖ ≥ (‖z‖ - 1) * ‖z‖ rw [mul_comm, mul_sub_one, ← pow_two, ← norm_pow]All goals completed! 🐙 _ ≥ 2 * ‖z‖ := byc:ℝz:ℝcz:‖c‖ ≤ ‖z‖z3:3 ≤ ‖z‖⊢ (‖z‖ - 1) * ‖z‖ ≥ 2 * ‖z‖ boundAll goals completed! 🐙

bound is built on top of aesop, and uses

1. Apply lemmas registered via the @[bound] attribute

2. Forward lemmas registered via the @[bound_forward] attribute

3. Local hypotheses from the context

4. Optionally: additional hypotheses provided as bound [h₀, h₁] or similar. These are added to the context as if by have := hᵢ.

The functionality of bound overlaps with positivity and gcongr, but can jump back and forth between 0 ≤ x and x ≤ y-type inequalities. For example, bound proves 0 ≤ c → b ≤ a → 0 ≤ a * c - b * c by turning the goal into b * c ≤ a * c, then using mul_le_mul_of_nonneg_right. bound also contains lemmas for goals of the form 1 ≤ x, 1 < x, x ≤ 1, x < 1. Conversely, gcongr can prove inequalities for more types of relations, supports all positivity functionality, and is likely faster since it is more specialized (not built atop aesop).

bv_check

This tactic works just like bv_decide but skips calling a SAT solver by using a proof that is already stored on disk. It is called with the name of an LRAT file in the same directory as the current Lean file:

bv_check "proof.lrat"

bv_decide

Close fixed-width BitVec and Bool goals by obtaining a proof from an external SAT solver and verifying it inside Lean. The solvable goals are currently limited to

• the Lean equivalent of QF_BV

• automatically splitting up structures that contain information about BitVec or Bool

example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by⊢ ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b introsa✝:BitVec 64b✝:BitVec 64⊢ (a✝ &&& b✝) + (a✝ ^^^ b✝) = a✝ ||| b✝ bv_decideAll goals completed! 🐙

If bv_decide encounters an unknown definition it will be treated like an unconstrained BitVec variable. Sometimes this enables solving goals despite not understanding the definition because the precise properties of the definition do not matter in the specific proof.

If bv_decide fails to close a goal it provides a counter-example, containing assignments for all terms that were considered as variables.

In order to avoid calling a SAT solver every time, the proof can be cached with bv_decide?.

If solving your problem relies inherently on using associativity or commutativity, consider enabling the bv.ac_nf option.

Note: bv_decide uses ofReduceBool and thus trusts the correctness of the code generator.

Note: include import Std.Tactic.BVDecide

bv_decide

Close fixed-width BitVec and Bool goals by obtaining a proof from an external SAT solver and verifying it inside Lean. The solvable goals are currently limited to

• the Lean equivalent of QF_BV

• automatically splitting up structures that contain information about BitVec or Bool

example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by⊢ ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b introsa✝:BitVec 64b✝:BitVec 64⊢ (a✝ &&& b✝) + (a✝ ^^^ b✝) = a✝ ||| b✝ bv_decideAll goals completed! 🐙

If bv_decide encounters an unknown definition it will be treated like an unconstrained BitVec variable. Sometimes this enables solving goals despite not understanding the definition because the precise properties of the definition do not matter in the specific proof.

If bv_decide fails to close a goal it provides a counter-example, containing assignments for all terms that were considered as variables.

In order to avoid calling a SAT solver every time, the proof can be cached with bv_decide?.

If solving your problem relies inherently on using associativity or commutativity, consider enabling the bv.ac_nf option.

Note: bv_decide uses ofReduceBool and thus trusts the correctness of the code generator.

Note: include import Std.Tactic.BVDecide

bv_decide?

Suggest a proof script for a bv_decide tactic call. Useful for caching LRAT proofs.

Note: include import Std.Tactic.BVDecide

bv_decide?

Suggest a proof script for a bv_decide tactic call. Useful for caching LRAT proofs.

Note: include import Std.Tactic.BVDecide

bv_normalize

Run the normalization procedure of bv_decide only. Sometimes this is enough to solve basic BitVec goals already.

Note: include import Std.Tactic.BVDecide

bv_normalize

Run the normalization procedure of bv_decide only. Sometimes this is enough to solve basic BitVec goals already.

Note: include import Std.Tactic.BVDecide

bv_omega

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 [bitvec_to_nat] at *. bitvec_to_nat is a @[simp] attribute that you can (cautiously) add to more theorems.

by_cases

by_cases (h :)? p splits the main goal into two cases, assuming h : p in the first branch, and h : ¬ p in the second branch.

by_contra

by_contra h proves ⊢ p by contradiction, introducing a hypothesis h : ¬p and proving False.

• If p is a negation ¬q, h : q will be introduced instead of ¬¬q.

• If p is decidable, it uses Decidable.byContradiction instead of Classical.byContradiction.

• If h is omitted, the introduced variable _: ¬p will be anonymous.

by_contra!

If the target of the main goal is a proposition p, by_contra! reduces the goal to proving False using the additional hypothesis this : ¬ p. by_contra! h can be used to name the hypothesis h : ¬ p. The hypothesis ¬ p will be negation normalized using push_neg. For instance, ¬ a < b will be changed to b ≤ a. by_contra! h : q will normalize negations in ¬ p, normalize negations in q, and then check that the two normalized forms are equal. The resulting hypothesis is the pre-normalized form, q. If the name h is not explicitly provided, then this will be used as name. This tactic uses classical reasoning. It is a variant on the tactic by_contra. Examples:

example : 1 < 2 := by
  by_contra! h
  -- h : 2 ≤ 1 ⊢ False

example : 1 < 2 := by
  by_contra! h : ¬ 1 < 2
  -- h : ¬ 1 < 2 ⊢ False

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.

calc?

Create a calc proof.

cancel_denoms

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

variable [LinearOrderedField α] (a b c : α)

example (h : a / 5 + b / 4 < c) : 4*a + 5*b < 20*c := by
  cancel_denoms at h
  exact h

example (h : a > 0) : a / 5 > 0 := by
  cancel_denoms
  exact h

case

• case _ : t => tac finds the first goal that unifies with t and then solves it using tac or else fails. Like show, it changes the type of the goal to t. The _ can optionally be a case tag, in which case it only looks at goals whose tag would be considered by case (goals with an exact tag match, followed by goals with the tag as a suffix, followed by goals with the tag as a prefix).

• case _ n₁ ... nₘ : t => tac additionally names the m most recent hypotheses with inaccessible names to the given names. The names are renamed before matching against t. The _ can optionally be a case tag.

• case _ : t := e is short for case _ : t => exact e.

• case _ : t₁ | _ : t₂ | ... => tac is equivalent to (case _ : t₁ => tac); (case _ : t₂ => tac); ... but with all matching done on the original list of goals -- each goal is consumed as they are matched, so patterns may repeat or overlap.

• case _ : t will make the matched goal be the first goal. case _ : t₁ | _ : t₂ | ... makes the matched goals be the first goals in the given order.

• case _ : t := _ and case _ : t := ?m are the same as case _ : t but in the ?m case the goal tag is changed to m. In particular, the goal becomes metavariable ?m.

case

• case tag => tac focuses on the goal with case name tag and solves it using tac, or else fails.

• case tag x₁ ... xₙ => tac additionally renames the n most recent hypotheses with inaccessible names to the given names.

• case tag₁ | tag₂ => tac is equivalent to (case tag₁ => tac); (case tag₂ => tac).

case'

case' _ : t => tac is similar to the case _ : t => tac tactic, but it does not ensure the goal has been solved after applying tac, nor does it admit the goal if tac failed. Recall that case closes the goal using sorry when tac fails, and the tactic execution is not interrupted.

case'

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.

cases

Assuming x is a variable in the local context with an inductive type, cases x splits the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor. If the type of an element in the local context depends on x, that element is reverted and reintroduced afterward, so that the case split affects that hypothesis as well. 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, where e is an expression instead of a variable, generalizes e in the goal, and then cases on the resulting variable.

• Given as : List α, cases as with | nil => tac₁ | cons a as' => tac₂, uses tactic tac₁ for the nil case, and tac₂ for the cons case, and a and as' are used as names for the new variables introduced.

• cases h : e, where e is a variable or an expression, performs cases on e as above, but also adds a hypothesis h : e = ... to each hypothesis, where ... is the constructor instance for that particular case.

cases'

The cases' tactic is similar to the cases tactic in Lean 4 core, but the syntax for giving names is different:

example (h : p ∨ q) : q ∨ p := byp:Propq:Proph:p ∨ q⊢ q ∨ p cases h with | inl hp =>inlp:Propq:Prophp:p⊢ q ∨ p exact Or.inr hpAll goals completed! 🐙 | inr hq =>inrp:Propq:Prophq:q⊢ q ∨ p exact Or.inl hqAll goals completed! 🐙 example (h : p ∨ q) : q ∨ p := byp:Propq:Proph:p ∨ q⊢ q ∨ p cases' h with hp hqinlp:Propq:Prophp:p⊢ q ∨ pinrp:Propq:Prophq:q⊢ q ∨ p ·inlp:Propq:Prophp:p⊢ q ∨ p exact Or.inr hpAll goals completed! 🐙 ·inrp:Propq:Prophq:q⊢ q ∨ p exact Or.inl hqAll goals completed! 🐙 example (h : p ∨ q) : q ∨ p := byp:Propq:Proph:p ∨ q⊢ q ∨ p rcases h with hp | hqinlp:Propq:Prophp:p⊢ q ∨ pinrp:Propq:Prophq:q⊢ q ∨ p ·inlp:Propq:Prophp:p⊢ q ∨ p exact Or.inr hpAll goals completed! 🐙 ·inrp:Propq:Prophq:q⊢ q ∨ p exact Or.inl hqAll goals completed! 🐙

Prefer cases or rcases when possible, because these tactics promote structured proofs.

cases_first_enat

Finds the first ENat in the context and applies the cases tactic to it. Then simplifies expressions involving ⊤ using the enat_to_nat_top simp set.

cases_type

• cases_type I applies the cases tactic to a hypothesis h : (I ...)

• cases_type I_1 ... I_n applies the cases tactic to a hypothesis h : (I_1 ...) or ... or h : (I_n ...)

• cases_type* I is shorthand for · repeat cases_type I

• cases_type! I only applies cases if the number of resulting subgoals is <= 1.

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

cases_type* Or And

cases_type!

• cases_type I applies the cases tactic to a hypothesis h : (I ...)

• cases_type I_1 ... I_n applies the cases tactic to a hypothesis h : (I_1 ...) or ... or h : (I_n ...)

• cases_type* I is shorthand for · repeat cases_type I

• cases_type! I only applies cases if the number of resulting subgoals is <= 1.

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

cases_type* Or And

casesm

• casesm p applies the cases tactic to a hypothesis h : type if type matches the pattern p.

• casesm p_1, ..., p_n applies the cases tactic to a hypothesis h : type if type matches one of the given patterns.

• casesm* p is a more efficient and compact version of · repeat casesm p. It is more efficient because the pattern is compiled once.

• casesm! p only applies cases if the number of resulting subgoals is <= 1.

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

casesm* _ ∨ _, _ ∧ _

casesm!

• casesm p applies the cases tactic to a hypothesis h : type if type matches the pattern p.

• casesm p_1, ..., p_n applies the cases tactic to a hypothesis h : type if type matches one of the given patterns.

• casesm* p is a more efficient and compact version of · repeat casesm p. It is more efficient because the pattern is compiled once.

• casesm! p only applies cases if the number of resulting subgoals is <= 1.

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

casesm* _ ∨ _, _ ∧ _

cat_disch

A tactic for discharging easy category theory goals, widely used as an autoparameter. Currently this defaults to the aesop_cat wrapper around aesop, but by setting the option mathlib.tactic.category.grind to true, it will use the grind tactic instead.

cc

The congruence closure tactic cc tries to solve the goal by chaining equalities from context and applying congruence (i.e. if a = b, then f a = f b). It is a finishing tactic, i.e. it is meant to close the current goal, not to make some inconclusive progress. A mostly trivial example would be:

example (a b c : ℕ) (f : ℕ → ℕ) (h : a = b) (h' : b = c) : f a = f c := bya:ℕb:ℕc:ℕf:ℕ → ℕh:a = bh':b = c⊢ f a = f c The tactic `cc` is deprecated since 2025-07-31, please use `grind` instead. Please report any regressions at https://github.com/leanprover/lean4/issues/. Note that `cc` supports some goals that `grind` doesn't, but these rely on higher-order unification and can result in unpredictable performance. If a downstream library is relying on this functionality, please report this in an issue and we'll help find a solution.ccAll goals completed! 🐙

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

example (f : ℕ → ℕ) (x : ℕ) (H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) : f x = x := byf:ℕ → ℕx:ℕH1:f (f (f x)) = xH2:f (f (f (f (f x)))) = x⊢ f x = x The tactic `cc` is deprecated since 2025-07-31, please use `grind` instead. Please report any regressions at https://github.com/leanprover/lean4/issues/. Note that `cc` supports some goals that `grind` doesn't, but these rely on higher-order unification and can result in unpredictable performance. If a downstream library is relying on this functionality, please report this in an issue and we'll help find a solution.ccAll goals completed! 🐙

cfc_cont_tac

A tactic used to automatically discharge goals relating to the continuous functional calculus, specifically concerning continuity of the functions involved.

cfc_tac

A tactic used to automatically discharge goals relating to the continuous functional calculus, specifically whether the element satisfies the predicate.

cfc_zero_tac

A tactic used to automatically discharge goals relating to the non-unital continuous functional calculus, specifically concerning whether f 0 = 0.

change

• 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

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