1.15. All tactics🔗

#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.succ_lt_succ • #check Nat.succ_le_of_lt • #check Nat.succ_le_succ • #check Nat.le_of_succ_le_succ • #check Nat.lt_succ • #check LT.lt.nat_succ_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.succ_lt_succ • Nat.succ_le_of_lt • Nat.succ_le_succ • Nat.le_of_succ_le_succ • Nat.lt_succ • LT.lt.nat_succ_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.succ_lt_succ (type: ∀ {n m : Nat}, n < m → Nat.succ n < Nat.succ m) • apply Nat.succ_lt_succ • have : ∀ {n m : Nat}, n < m → Nat.succ n < Nat.succ m := Nat.succ_lt_succFrom: Nat.succ_le_of_lt (type: ∀ {n m : Nat}, n < m → Nat.succ n ≤ m) • apply Nat.succ_le_of_lt • have : ∀ {n m : Nat}, n < m → Nat.succ n ≤ m := Nat.succ_le_of_ltFrom: Nat.succ_le_succ (type: ∀ {n m : Nat}, LE.le n m → LE.le (Nat.succ n) (Nat.succ m)) • apply Nat.succ_le_succ • have : ∀ {n m : Nat}, LE.le n m → LE.le (Nat.succ n) (Nat.succ m) := Nat.succ_le_succFrom: Nat.le_of_succ_le_succ (type: ∀ {n m : Nat}, LE.le (Nat.succ n) (Nat.succ m) → LE.le n m) • apply Nat.le_of_succ_le_succ • have : ∀ {n m : Nat}, LE.le (Nat.succ n) (Nat.succ m) → LE.le n m := Nat.le_of_succ_le_succFrom: Nat.lt_succ (type: ∀ {m n : Nat}, m < succ n ↔ m ≤ n) • rw [← Nat.lt_succ]From: LT.lt.nat_succ_le (type: ∀ {n m : ℕ}, n < m → Nat.succ n ≤ m) • apply LT.lt.nat_succ_le • have : ∀ {n m : ℕ}, n < m → Nat.succ n ≤ m := LT.lt.nat_succ_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! 🐙

#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 Nat.sum • #check List.getLastD • #check List.headD#loogle List ?a → ?aAll goals completed! 🐙 example := Loogle Search Results • List.get • List.and • List.or • Nat.sum • List.getLastD • List.headD#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.

#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 • Nat.lt.step • Nat.lt_pred_iff • Nat.lt_of_succ_le • Nat.lt_succ_iff • Nat.succPNat_lt_succPNat • Nat.succ_le_of_lt • Nat.decreasingInduction_succ_left • Nat.decreasingInduction_succ • Nat.lt_of_lt_pred • Nat.sub_le • Nat.sub_lt • Nat.le_of_succ_le • Nat.le_of_pred_lt • Nat.pow_succ#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_leFrom: Nat.lt.step (type: ∀ {n m : ℕ}, n < m → n < m.succ) • apply Nat.lt.step • have : ∀ {n m : ℕ}, n < m → n < m.succ := Nat.lt.stepFrom: Nat.lt_pred_iff (type: ∀ {a b : ℕ}, a < b.pred ↔ a.succ < b) • have : ∀ {a b : ℕ}, a < b.pred ↔ a.succ < b := Nat.lt_pred_iffFrom: Nat.lt_of_succ_le (type: ∀ {n m : ℕ}, n.succ ≤ m → n < m) • apply Nat.lt_of_succ_le • have : ∀ {n m : ℕ}, n.succ ≤ m → n < m := Nat.lt_of_succ_leFrom: Nat.lt_succ_iff (type: ∀ {m n : ℕ}, m < n.succ ↔ m ≤ n) • have : ∀ {m n : ℕ}, m < n.succ ↔ m ≤ n := Nat.lt_succ_iff • rw [← Nat.lt_succ_iff]From: Nat.succPNat_lt_succPNat (type: ∀ {m n : ℕ}, m.succPNat < n.succPNat ↔ m < n) • have : ∀ {m n : ℕ}, m.succPNat < n.succPNat ↔ m < n := Nat.succPNat_lt_succPNatFrom: Nat.succ_le_of_lt (type: ∀ {n m : ℕ}, n < m → n.succ ≤ m) • apply Nat.succ_le_of_lt • have : ∀ {n m : ℕ}, n < m → n.succ ≤ m := Nat.succ_le_of_ltFrom: Nat.lt_of_lt_pred (type: ∀ {m n : ℕ}, m < n - 1 → m < n) • apply Nat.lt_of_lt_pred • have : ∀ {m n : ℕ}, m < n - 1 → m < n := Nat.lt_of_lt_predFrom: Nat.sub_le (type: ∀ (n m : ℕ), n - m ≤ n) • have : ∀ (n m : ℕ), n - m ≤ n := Nat.sub_leFrom: Nat.sub_lt (type: ∀ {n m : ℕ}, 0 < n → 0 < m → n - m < n) • have : ∀ {n m : ℕ}, 0 < n → 0 < m → n - m < n := Nat.sub_ltFrom: Nat.le_of_succ_le (type: ∀ {n m : ℕ}, n.succ ≤ m → n ≤ m) • apply Nat.le_of_succ_le • have : ∀ {n m : ℕ}, n.succ ≤ m → n ≤ m := Nat.le_of_succ_leFrom: Nat.le_of_pred_lt (type: ∀ {n : ℕ} {m : ℕ}, m.pred < n → m ≤ n) • apply Nat.le_of_pred_lt • have : ∀ {n : ℕ} {m : ℕ}, m.pred < n → m ≤ n := Nat.le_of_pred_ltFrom: Nat.pow_succ (type: ∀ (n m : ℕ), n ^ m.succ = n ^ m * n) • have : ∀ (n m : ℕ), n ^ m.succ = n ^ m * n := Nat.pow_succ#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! 🐙

(

(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 => rflAll goals completed! 🐙 | 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 expressions in abelian groups.

• abel! will use a more aggressive reducibility setting to determine equality of atoms.

• abel1 fails if the target is not an equality.

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! 🐙

abel

Unsupported legacy syntax from mathlib3, which allowed passing additional terms to abel.

abel!

Unsupported legacy syntax from mathlib3, which allowed passing additional terms to abel!.

abel!

Tactic for evaluating expressions in abelian groups.

• abel! will use a more aggressive reducibility setting to determine equality of atoms.

• abel1 fails if the target is not an equality.

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! 🐙

abel1

Tactic for solving equations in the language of additive, commutative monoids and groups. This version of abel fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.

abel1! will use a more aggressive reducibility setting to identify atoms. This can prove goals that abel cannot, but is more expensive.

abel1!

Tactic for solving equations in the language of additive, commutative monoids and groups. This version of abel fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.

abel1! will use a more aggressive reducibility setting to identify atoms. This can prove goals that abel cannot, but is more expensive.

abel_nf

Simplification tactic for expressions in the language of abelian groups, which rewrites all group expressions into a normal form.

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

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

  • red: the reducibility setting (overridden by !)

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

• abel_nf works as both a tactic and a conv tactic. In tactic mode, abel_nf at h can be used to rewrite in a hypothesis.

abel_nf!

Simplification tactic for expressions in the language of abelian groups, which rewrites all group expressions into a normal form.

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

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

  • red: the reducibility setting (overridden by !)

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

• abel_nf works as both a tactic and a conv tactic. In tactic mode, abel_nf at h can be used to rewrite in a hypothesis.

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 (config := {properties := false}), 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, concating 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 (config := cfg) e is like apply e but allows you to provide a configuration cfg : ApplyConfig to pass to the underlying apply operation.

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?

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 intros 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_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.

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.

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.

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 η = θ, 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

-- Calc example: A weak lower bound for `z ↦ z^2 + c`
lemma le_sqr_add {c z : ℂ} (cz : abs c ≤ abs z) (z3 : 3 ≤ abs z) :
    2 * abs z ≤ abs (z^2 + c) := by
  calc abs (z^2 + c)
    _ ≥ abs (z^2) - abs c := by bound
    _ ≥ abs (z^2) - abs z := by bound
    _ ≥ (abs z - 1) * abs z := by rw [mul_comm, mul_sub_one, ← pow_two, ← abs.map_pow]
    _ ≥ 2 * abs z := by bound

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.

bv_decide?

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

bv_normalize

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

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 [bv_toNat] at *. bv_toNat 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.

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α:Type u_1inst✝:LinearOrderedField αa:αb:αc:αh:a / 5 + b / 4 < c⊢ 4 * a + 5 * b < 20 * c cancel_denoms at hα:Type u_1inst✝:LinearOrderedField αa:αb:αc:αh:4 * a + 5 * b < 20 * c⊢ 4 * a + 5 * b < 20 * c exact hAll goals completed! 🐙 example (h : a > 0) : a / 5 > 0 := byα:Type u_1inst✝:LinearOrderedField αa:αb:αc:αh:a > 0⊢ a / 5 > 0 cancel_denomsα:Type u_1inst✝:LinearOrderedField αa:αb:αc:αh:a > 0⊢ 0 < a exact hAll goals completed! 🐙

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

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.

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 => exact Or.inr hpAll goals completed! 🐙 | inr hq => 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_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* _ ∨ _, _ ∧ _

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

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? term unifies term with the current goal, then suggests explicit change syntax that uses the resulting unified term.

If term is not present, change? suggests the current goal itself. This is useful after tactics which transform the goal while maintaining definitional equality, such as dsimp; those preceding tactic calls can then be deleted.

example : (fun x : Nat => x) 0 = 1 := by
  change? 0 = _  -- `Try this: change 0 = 1`

check_compositions

For each composition f ≫ g in the goal, which internally is represented as CategoryStruct.comp C inst X Y Z f g, infer the types of f and g and check whether their sources and targets agree with X, Y, and Z at "instances and reducible" transparency, reporting any discrepancies.

An example:

example (j : J) :
    colimit.ι ((F ⋙ G) ⋙ H) j ≫ (preservesColimitIso (G ⋙ H) F).inv =
      H.map (G.map (colimit.ι F j)) := by

  -- We know which lemma we want to use, and it's even a simp lemma, but `rw`
  -- won't let us apply it
  fail_if_success rw [ι_preservesColimitIso_inv]
  fail_if_success rw [ι_preservesColimitIso_inv (G ⋙ H)]
  fail_if_success simp only [ι_preservesColimitIso_inv]

  -- This would work:
  -- erw [ι_preservesColimitIso_inv (G ⋙ H)]

  -- `check_compositions` checks if the two morphisms we're composing are
  -- composed by abusing defeq, and indeed it tells us that we are abusing
  -- definitional associativity of composition of functors here: it prints
  -- the following.

  -- info: In composition
  --   colimit.ι ((F ⋙ G) ⋙ H) j ≫ (preservesColimitIso (G ⋙ H) F).inv
  -- the source of
  --   (preservesColimitIso (G ⋙ H) F).inv
  -- is
  --   colimit (F ⋙ G ⋙ H)
  -- but should be
  --   colimit ((F ⋙ G) ⋙ H)

  check_compositions

  -- In this case, we can "fix" this by reassociating in the goal, but
  -- usually at this point the right thing to do is to back off and
  -- check how we ended up with a bad goal in the first place.
  dsimp only [Functor.assoc]

  -- This would work now, but it is not needed, because simp works as well
  -- rw [ι_preservesColimitIso_inv]

  simp

checkpoint

checkpoint tac acts the same as tac, but it caches the input and output of tac, and if the file is re-elaborated and the input matches, the tactic is not re-run 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.)

choose

• choose a b h h' using hyp takes a hypothesis hyp of the form ∀ (x : X) (y : Y), ∃ (a : A) (b : B), P x y a b ∧ Q x y a b for some P Q : X → Y → A → B → Prop and outputs into context a function a : X → Y → A, b : X → Y → B and two assumptions: h : ∀ (x : X) (y : Y), P x y (a x y) (b x y) and h' : ∀ (x : X) (y : Y), Q x y (a x y) (b x y). It also works with dependent versions.

• choose! a b h h' using hyp does the same, except that it will remove dependency of the functions on propositional arguments if possible. For example if Y is a proposition and A and B are nonempty in the above example then we will instead get a : X → A, b : X → B, and the assumptions h : ∀ (x : X) (y : Y), P x y (a x) (b x) and h' : ∀ (x : X) (y : Y), Q x y (a x) (b x).

The using hyp part can be omitted, which will effectively cause choose to start with an intro hyp.

Examples:

example (h : ∀ n m : ℕ, ∃ i j, m = n + i ∨ m + j = n) : True := byh:∀ (n m : ℕ), ∃ i j, m = n + i ∨ m + j = n⊢ True choose i j h using hi:ℕ → ℕ → ℕj:ℕ → ℕ → ℕh:∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n⊢ True guard_hyp i : ℕ → ℕ → ℕi:ℕ → ℕ → ℕj:ℕ → ℕ → ℕh:∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n⊢ True guard_hyp j : ℕ → ℕ → ℕi:ℕ → ℕ → ℕj:ℕ → ℕ → ℕh:∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n⊢ True guard_hyp h : ∀ (n m : ℕ), m = n + i n m ∨ m + j n m = ni:ℕ → ℕ → ℕj:ℕ → ℕ → ℕh:∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n⊢ True trivialAll goals completed! 🐙 example (h : ∀ i : ℕ, i < 7 → ∃ j, i < j ∧ j < i+i) : True := byh:∀ i < 7, ∃ j, i < j ∧ j < i + i⊢ True choose! f h h' using hf:ℕ → ℕh:∀ i < 7, i < f ih':∀ i < 7, f i < i + i⊢ True guard_hyp f : ℕ → ℕf:ℕ → ℕh:∀ i < 7, i < f ih':∀ i < 7, f i < i + i⊢ True guard_hyp h : ∀ (i : ℕ), i < 7 → i < f if:ℕ → ℕh:∀ i < 7, i < f ih':∀ i < 7, f i < i + i⊢ True guard_hyp h' : ∀ (i : ℕ), i < 7 → f i < i + if:ℕ → ℕh:∀ i < 7, i < f ih':∀ i < 7, f i < i + i⊢ True trivialAll goals completed! 🐙

choose!

• choose a b h h' using hyp takes a hypothesis hyp of the form ∀ (x : X) (y : Y), ∃ (a : A) (b : B), P x y a b ∧ Q x y a b for some P Q : X → Y → A → B → Prop and outputs into context a function a : X → Y → A, b : X → Y → B and two assumptions: h : ∀ (x : X) (y : Y), P x y (a x y) (b x y) and h' : ∀ (x : X) (y : Y), Q x y (a x y) (b x y). It also works with dependent versions.

• choose! a b h h' using hyp does the same, except that it will remove dependency of the functions on propositional arguments if possible. For example if Y is a proposition and A and B are nonempty in the above example then we will instead get a : X → A, b : X → B, and the assumptions h : ∀ (x : X) (y : Y), P x y (a x) (b x) and h' : ∀ (x : X) (y : Y), Q x y (a x) (b x).

The using hyp part can be omitted, which will effectively cause choose to start with an intro hyp.

Examples:

example (h : ∀ n m : ℕ, ∃ i j, m = n + i ∨ m + j = n) : True := byh:∀ (n m : ℕ), ∃ i j, m = n + i ∨ m + j = n⊢ True choose i j h using hi:ℕ → ℕ → ℕj:ℕ → ℕ → ℕh:∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n⊢ True guard_hyp i : ℕ → ℕ → ℕi:ℕ → ℕ → ℕj:ℕ → ℕ → ℕh:∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n⊢ True guard_hyp j : ℕ → ℕ → ℕi:ℕ → ℕ → ℕj:ℕ → ℕ → ℕh:∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n⊢ True guard_hyp h : ∀ (n m : ℕ), m = n + i n m ∨ m + j n m = ni:ℕ → ℕ → ℕj:ℕ → ℕ → ℕh:∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n⊢ True trivialAll goals completed! 🐙 example (h : ∀ i : ℕ, i < 7 → ∃ j, i < j ∧ j < i+i) : True := byh:∀ i < 7, ∃ j, i < j ∧ j < i + i⊢ True choose! f h h' using hf:ℕ → ℕh:∀ i < 7, i < f ih':∀ i < 7, f i < i + i⊢ True guard_hyp f : ℕ → ℕf:ℕ → ℕh:∀ i < 7, i < f ih':∀ i < 7, f i < i + i⊢ True guard_hyp h : ∀ (i : ℕ), i < 7 → i < f if:ℕ → ℕh:∀ i < 7, i < f ih':∀ i < 7, f i < i + i⊢ True guard_hyp h' : ∀ (i : ℕ), i < 7 → f i < i + if:ℕ → ℕh:∀ i < 7, i < f ih':∀ i < 7, f i < i + i⊢ True trivialAll goals completed! 🐙

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.

clean

(Deprecated) clean t is a macro for exact clean% t.

clean_wf

This tactic is used internally by lean before presenting the proof obligations from a well-founded definition to the user via decreasing_by. It is not necessary to use this tactic manually.

clear

Clears all hypotheses it can, except those provided after a minus sign. Example:

clear * - h₁ h₂

clear

clear x... removes the given hypotheses, or fails if there are remaining references to a hypothesis.

clear!

A variant of clear which clears not only the given hypotheses but also any other hypotheses depending on them

clear_

Clear all hypotheses starting with _, like _match and _let_match.

clear_aux_decl

This tactic clears all auxiliary declarations from the context.

clear_value

clear_value n₁ n₂ ... clears the bodies of the local definitions n₁, n₂ ..., changing them into regular hypotheses. A hypothesis n : α := t is changed to n : α.

The order of n₁ n₂ ... does not matter, and values will be cleared in reverse order of where they appear in the context.

coherence

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

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

(If you have very large equations on which coherence is unexpectedly failing, you may need to increase the typeclass search depth, using e.g. set_option synthInstance.maxSize 500.)

compareOfLessAndEq_rfl

This attempts to prove that a given instance of compare is equal to compareOfLessAndEq by introducing the arguments and trying the following approaches in order:

1. seeing if rfl works

2. seeing if the compare at hand is nonetheless essentially compareOfLessAndEq, but, because of implicit arguments, requires us to unfold the defs and split the ifs in the definition of compareOfLessAndEq

3. seeing if we can split by cases on the arguments, then see if the defs work themselves out (useful when compare is defined via a match statement, as it is for Bool)

compute_degree

compute_degree is a tactic to solve goals of the form

• natDegree f = d,

• degree f = d,

• natDegree f ≤ d,

• degree f ≤ d,

• coeff f d = r, if d is the degree of f.

The tactic may leave goals of the form d' = d, d' ≤ d, or r ≠ 0, where d' in ℕ or WithBot ℕ is the tactic's guess of the degree, and r is the coefficient's guess of the leading coefficient of f.

compute_degree applies norm_num to the left-hand side of all side goals, trying to close them.

The variant compute_degree! first applies compute_degree. Then it uses norm_num on all the remaining goals and tries assumption.

compute_degree!

compute_degree is a tactic to solve goals of the form

• natDegree f = d,

• degree f = d,

• natDegree f ≤ d,

• degree f ≤ d,

• coeff f d = r, if d is the degree of f.

The tactic may leave goals of the form d' = d, d' ≤ d, or r ≠ 0, where d' in ℕ or WithBot ℕ is the tactic's guess of the degree, and r is the coefficient's guess of the leading coefficient of f.

compute_degree applies norm_num to the left-hand side of all side goals, trying to close them.

The variant compute_degree! first applies compute_degree. Then it uses norm_num on all the remaining goals and tries assumption.

congr

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.

congr

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.

congr

Apply congruence (recursively) to goals of the form ⊢ f as = f bs and ⊢ HEq (f as) (f bs).

• congr n controls 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.

• If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.

• You can use congr with p (: n)? to call ext p (: n)? to all subgoals generated by congr. For example, if the goal is ⊢ f '' s = g '' s then congr with x generates the goal x : α ⊢ f x = g x.

congr!

Equates pieces of the left-hand side of a goal to corresponding pieces of the right-hand side by recursively applying congruence lemmas. For example, with ⊢ f as = g bs we could get two goals ⊢ f = g and ⊢ as = bs.

Syntax:

congr!
congr! n
congr! with x y z
congr! n with x y z

Here, n is a natural number and x, y, z are rintro patterns (like h, rfl, ⟨x, y⟩, _, -, (h | h), etc.).

The congr! tactic is similar to congr but is more insistent in trying to equate left-hand sides to right-hand sides of goals. Here is a list of things it can try:

• If R in ⊢ R x y is a reflexive relation, it will convert the goal to ⊢ x = y if possible. The list of reflexive relations is maintained using the @[refl] attribute. As a special case, ⊢ p ↔ q is converted to ⊢ p = q during congruence processing and then returned to ⊢ p ↔ q form at the end.

• If there is a user congruence lemma associated to the goal (for instance, a @[congr]-tagged lemma applying to ⊢ List.map f xs = List.map g ys), then it will use that.

• It uses a congruence lemma generator at least as capable as the one used by congr and simp. If there is a subexpression that can be rewritten by simp, then congr! should be able to generate an equality for it.

• It can do congruences of pi types using lemmas like implies_congr and pi_congr.

• Before applying congruences, it will run the intros tactic automatically. The introduced variables can be given names using a with clause. This helps when congruence lemmas provide additional assumptions in hypotheses.

• When there is an equality between functions, so long as at least one is obviously a lambda, we apply funext or Function.hfunext, which allows for congruence of lambda bodies.

• It can try to close goals using a few strategies, including checking definitional equality, trying to apply Subsingleton.elim or proof_irrel_heq, and using the assumption tactic.

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.

The congr! tactic also takes a configuration option, for example

congr! (config := {transparency := .default}) 2

This overrides the default, which is to apply congruence lemmas at reducible transparency.

The congr! tactic is aggressive with equating two sides of everything. There is a predefined configuration that uses a different strategy: Try

congr! (config := .unfoldSameFun)

This only allows congruences between functions applications of definitionally equal functions, and it applies congruence lemmas at default transparency (rather than just reducible). This is somewhat like congr.

See Congr!.Config for all options.