Tactics

The tactic language is a special-purpose programming language for constructing proofs, indicated using the keyword by.

clear_

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

Tags:
Defined in module:: Mathlib.Tactic.Clear_

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.

Tags:
Defined in module:: Mathlib.Combinatorics.Matroid.Basic

infer_param

Close a goal of the form optParam α a or autoParam α stx by using a.

Tags:
Defined in module:: Mathlib.Tactic.InferParam

pnat_to_nat

pnat_to_nat shifts all PNats in the context to Nat, rewriting propositions about them. A typical use case is pnat_to_nat; lia.

Tags:
Defined in module:: Mathlib.Tactic.PNatToNat

pnat_positivity

For each x : PNat in the context, add the hypothesis 0 < (↑x : ℕ).

Tags:
Defined in module:: Mathlib.Tactic.PNatToNat

mem_tac

mem_tac tries to prove goals of the form x ∈ 𝒜 i when x has the form of:

y ^ n where i = n • j and y ∈ 𝒜 j.
a natural number n.

Tags:
Defined in module:: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

fail_if_no_progress

fail_if_no_progress tacs evaluates tacs, and fails if no progress is made on the main goal or the local context at reducible transparency.

Tags:
Defined in module:: Mathlib.Tactic.FailIfNoProgress

mv_bisim

tactic for proof by bisimulation

Tags:
Defined in module:: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

qify

The qify tactic is used to shift propositions from ℕ or ℤ to ℚ. This is often useful since ℚ has well-behaved division.

example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b := by
  qify
  qify at h
  /-
  h : ¬↑x * ↑y * ↑z < 0
  ⊢ ↑c < ↑a + 3 * ↑b
  -/
  sorry

qify can be given extra lemmas to use in simplification. This is especially useful in the presence of nat subtraction: passing ≤ arguments will allow push_cast to do more work.

example (a b c : ℤ) (h : a / b = c) (hab : b ∣ a) (hb : b ≠ 0) : a = c * b := by
  qify [hab] at h hb ⊢
  exact (div_eq_iff hb).1 h

qify makes use of the @[zify_simps] and @[qify_simps] attributes to move propositions, and the push_cast tactic to simplify the ℚ-valued expressions.

Tags:
Defined in module:: Mathlib.Tactic.Qify

rw??

rw?? is an interactive tactic that suggests rewrites for any expression selected by the user. To use it, shift-click an expression in the goal or a hypothesis that you want to rewrite. Clicking on one of the rewrite suggestions will paste the relevant rewrite tactic into the editor.

The rewrite suggestions are grouped and sorted by the pattern that the rewrite lemmas match with. Rewrites that don't change the goal and rewrites that create the same goal as another rewrite are filtered out, as well as rewrites that have new metavariables in the replacement expression. To see all suggestions, click on the filter button (▼) in the top right.

Tags:
Defined in module:: Mathlib.Tactic.Widget.LibraryRewrite

#find

#find t finds definitions and theorems whose result type matches the term t, and prints them as info lines. Use holes in t to indicate arbitrary subexpressions, for example #find _ ∧ _ will match any conjunction. #find is also available as a command. #find will not affect the goal by itself and should be removed from the finished proof.

There is also the find tactic which looks for lemmas which are applyable against the current goal.

Examples:

#find _ + _ = _ + _
#find ?n + _ = _ + ?n
#find (_ : Nat) + _ = _ + _
#find Nat → Nat

Tags:
Defined in module:: Mathlib.Tactic.Find

find

find finds definitions and theorems whose result type matches the current goal exactly, and prints them as info lines. In other words, find lists definitions and theorems that are applyable against the current goal. find will not affect the goal by itself and should be removed from the finished proof.

For a command or tactic that takes the type to search for as an argument, see #find.

Example:

example : True := by
  find
  -- True.intro: True
  -- trivial: True
  -- ...

Tags:
Defined in module:: Mathlib.Tactic.Find

wlog

wlog h : P adds an assumption h : P to the main goal, and adds a side goal that requires showing that the case h : ¬ P can be reduced to the case where P holds (typically by symmetry). The side goal will be at the top of the stack. In this side goal, there will be two additional assumptions:

h : ¬ P: the assumption that P does not hold
this: which is the statement that in the old context P suffices to prove the goal. By default, the entire context is reverted to produce this.

wlog h : P with H gives the name H to the statement that P proves the goal.
wlog h : P generalizing x y ... reverts certain parts of the context before creating the new goal. In this way, the wlog-claim this can be applied to x and y in different orders (exploiting symmetry, which is the typical use case).
wlog! h : P also calls push Not at the generated hypothesis h. wlog! h : P ∧ Q will transform ¬ (P ∧ Q) to P → ¬ Q
wlog! +distrib h : P also calls push +distrib Not at the generated hypothesis h. wlog! +distrib h : P ∧ Q will transform ¬ (P ∧ Q) to ¬P ∨ ¬Q.

Tags:
Defined in module:: Mathlib.Tactic.WLOG

whisker_simps

Simp lemmas for rewriting a 2-morphism into a normal form.

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.BicategoryCoherence

grw

grw [e] works just like rw [e], but e can be a relation other than = or ↔.

For example:

variable {a b c d n : ℤ}

example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
  grw [h₁, h₂]

example (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := by
  grw [h]

example (h₁ : a ∣ b) (h₂ : b ∣ a ^ 2 * c) : a ∣ b ^ 2 * c := by
  grw [h₁] at *
  exact h₂

To replace the RHS with the LHS of the given relation, use the ← notation (just like in rw):

example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
  grw [← h₂, ← h₁]

The strict inequality a < b is turned into the non-strict inequality a ≤ b to rewrite with it. A future version of grw may get special support for making better use of strict inequalities.

To rewrite only in the n-th position, use nth_grw n. This is useful when grw tries to rewrite in a position that is not valid for the given relation.

To be able to use grw, the relevant lemmas need to be tagged with @[gcongr]. To rewrite inside a transitive relation, you can also give it an IsTrans instance.

To let grw unfold more aggressively, as in erw, use grw (transparency := default).

Tags:
Defined in module:: Mathlib.Tactic.GRewrite.Elab

nth_grewrite

nth_grewrite is just like nth_rewrite, but for grewrite.

Tags:
Defined in module:: Mathlib.Tactic.GRewrite.Elab

apply_rw

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

Tags:
Defined in module:: Mathlib.Tactic.GRewrite.Elab

grewrite

grewrite [e] is like grw [e], but it doesn't try to close the goal with rfl. This is analogous to rw and rewrite, where rewrite doesn't try to close the goal with rfl.

Tags:
Defined in module:: Mathlib.Tactic.GRewrite.Elab

nth_grw

nth_grw is just like nth_rw, but for grw.

Tags:
Defined in module:: Mathlib.Tactic.GRewrite.Elab

apply_rewrite

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

Tags:
Defined in module:: Mathlib.Tactic.GRewrite.Elab

interval_cases

interval_cases n searches for upper and lower bounds on a variable n, and if bounds are found, splits into separate cases for each possible value of n.

As an example, in

example (n : ℕ) (w₁ : n ≥ 3) (w₂ : n < 5) : n = 3 ∨ n = 4 := by
  interval_cases n
  all_goals simp

after interval_cases n, the goals are 3 = 3 ∨ 3 = 4 and 4 = 3 ∨ 4 = 4.

You can also explicitly specify a lower and upper bound to use, as interval_cases using hl, hu. The hypotheses should be in the form hl : a ≤ n and hu : n < b, in which case interval_cases calls fin_cases on the resulting fact n ∈ Set.Ico a b.

You can specify a name h for the new hypothesis, as interval_cases h : n or interval_cases h : n using hl, hu.

Tags:
Defined in module:: Mathlib.Tactic.IntervalCases

set

set a := t with h is a variant of let a := t. It adds the hypothesis h : a = t to the local context and replaces t with a everywhere it can.

set a := t with ← h will add h : t = a instead.

set! a := t with h does not do any replacing.

example (x : Nat) (h : x + x - x = 3) : x + x - x = 3 := by
  set y := x with ← h2
  sorry
/-
x : Nat
y : Nat := x
h : y + y - y = 3
h2 : x = y
⊢ y + y - y = 3
-/

Tags:
Defined in module:: Mathlib.Tactic.Set

#adaptation_note

#adaptation_note /-- comment -/ adds an adaptation note to the current file. 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.

This syntax works as a command, or inline in tactic or term mode.

Tags:
Defined in module:: Mathlib.Tactic.AdaptationNote

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

Tags:
Defined in module:: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

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

Tags:
Defined in module:: Mathlib.Tactic.CancelDenoms.Core

ghost_simp

A macro for a common simplification when rewriting with ghost component equations.

Tags:
Defined in module:: Mathlib.RingTheory.WittVector.IsPoly

ghost_calc

ghost_calc is a tactic for proving identities between polynomial functions. Typically, when faced with a goal like

∀ (x y : 𝕎 R), verschiebung (x * frobenius y) = verschiebung x * y

you can

call ghost_calc
do a small amount of manual work -- maybe nothing, maybe rintro, etc
call ghost_simp

and this will close the goal.

ghost_calc cannot detect whether you are dealing with unary or binary polynomial functions. You must give it arguments to determine this. If you are proving a universally quantified goal like the above, call ghost_calc _ _. If the variables are introduced already, call ghost_calc x y. In the unary case, use ghost_calc _ or ghost_calc x.

ghost_calc is a light wrapper around type class inference. All it does is apply the appropriate extensionality lemma and try to infer the resulting goals. This is subtle and Lean's elaborator doesn't like it because of the HO unification involved, so it is easier (and prettier) to put it in a tactic script.

Tags:
Defined in module:: Mathlib.RingTheory.WittVector.IsPoly

rename_bvar

rename_bvar old → new renames all bound variables named old to new in the target.
rename_bvar old → new at h does the same in hypothesis h.

example (P : ℕ → ℕ → Prop) (h : ∀ n, ∃ m, P n m) : ∀ l, ∃ m, P l m := by
  rename_bvar n → q at h -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
  rename_bvar m → n -- target is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
  exact h -- Lean does not care about those bound variable names

Note: name clashes are resolved automatically.

Tags:
Defined in module:: Mathlib.Tactic.RenameBVar

try_this

Produces the text Try this: <tac> with the given tactic, and then executes it.

Tags:
Defined in module:: Mathlib.Tactic.TryThis

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

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.CheckCompositions

aesop_cat?

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

Tags:
Defined in module:: Mathlib.CategoryTheory.Category.Basic

rfl_cat

rfl_cat is a macro for intros; rfl which is attempted in aesop_cat before doing the more expensive aesop tactic.

This gives a speedup because simp (called by aesop) can be very slow. https://github.com/leanprover-community/mathlib4/pull/25475 contains measurements from June 2025.

Implementation notes:

refine id ?_: In some cases it is important that the type of the proof matches the expected type exactly. e.g. if the goal is 2 = 1 + 1, the rfl tactic will give a proof of type 2 = 2. Starting a proof with refine id ?_ is a trick to make sure that the proof has exactly the expected type, in this case 2 = 1 + 1. See also https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/changing.20a.20proof.20can.20break.20a.20later.20proof
apply_rfl: rfl is a macro that attempts both eq_refl and apply_rfl. Since apply_rfl subsumes eq_refl, we can use apply_rfl instead. This fails twice as fast as rfl.

Tags:
Defined in module:: Mathlib.CategoryTheory.Category.Basic

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.

Tags:
Defined in module:: Mathlib.CategoryTheory.Category.Basic

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.

Tags:
Defined in module:: Mathlib.CategoryTheory.Category.Basic

sorry_if_sorry

Close the main goal with sorry if its type contains sorry, and fail otherwise.

Tags:
Defined in module:: Mathlib.CategoryTheory.Category.Basic

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.

Tags:
Defined in module:: Mathlib.CategoryTheory.Category.Basic

finiteness

finiteness proves goals of the form *** < ∞ and (equivalently) *** ≠ ∞ in the extended nonnegative reals (ℝ≥0∞). If the goal cannot be proven, finiteness prints a warning and shows its intermediate progress.

This tactic is based on aesop. It calls assumption, intros, positivity, and any lemma or rule added to the finiteness ruleset, except that all simp rules are disabled.

This tactic is extensible. By adding more rules, finiteness can prove more goals. For example:

@[aesop (rule_sets := [finiteness]) safe 50] lemma ...
add_aesop_rules safe tactic (rule_sets := [finiteness]) (by ...) (Note that a simp rule cannot be added this way, since all simp rules are disabled.)
finiteness (clause) customizes the aesop call using the given clause. See aesop documentation for detailed explanation. Note that finiteness disables simp, so finiteness (add simp [lemma1, lemma2]) does not do anything more than a bare finiteness.
finiteness [t₁, ..., tₙ] adds the terms t₁, ..., tₙ as local hypotheses before applying the search rules.
finiteness? additionally shows the proof that finiteness found.
finiteness_nonterminal is a version of finiteness that does not report a warning if it fails to close the goal.

Tags:
Defined in module:: Mathlib.Tactic.Finiteness

rsuffices

The rsuffices tactic is an alternative version of suffices, that allows the usage of any syntax that would be valid in an obtain block. This tactic just calls obtain on the expression, and then rotate_left.

Tags:
Defined in module:: Mathlib.Tactic.RSuffices

simp_intro

The simp_intro tactic is a combination of simp and intro: it will simplify the types of variables as it introduces them and uses the new variables to simplify later arguments and the goal.

simp_intro x y z introduces variables named x y z
simp_intro x y z .. introduces variables named x y z and then keeps introducing _ binders
simp_intro (config := cfg) (discharger := tac) x y .. only [h₁, h₂]: simp_intro takes the same options as simp (see simp)

example : x + 0 = y → x = z := by
  simp_intro h
  -- h: x = y ⊢ y = z
  sorry

Tags:
Defined in module:: Mathlib.Tactic.SimpIntro

#defeq_abuse

WARNING: #defeq_abuse is an experimental tool intended to assist with breaking changes to transparency handling. Its syntax may change at any time, and it may not behave as expected. Please report unexpected behavior on Zulip.

#defeq_abuse in tac runs tac with backward.isDefEq.respectTransparency both true and false. If the tactic succeeds with false but fails with true, it identifies the specific isDefEq checks that fail with the stricter setting.

The tactic still executes (using the permissive setting if needed), so proofs remain valid during debugging.

Tags:
Defined in module:: Mathlib.Tactic.DefEqAbuse

module

Given a goal parseable as a linear combination ⊢ a • x + ... + b • y = c • x + ... + d • y, module proves the equalities of the scalars for each respective atom, by ring normalization. This means the example goal above is solved if ring can prove ⊢ a = c (from x), ..., ⊢ b = d (from y).

module is equivalent to match_scalars <;> ring1. If ring1 fails to prove one of the equalities, you can instead use match_scalars followed by specialized proofs for each scalar.

Examples:

example [AddCommMonoid M] [CommSemiring R] [Module R M] (a b : R) (x : M) :
    a • x + b • x = (b + a) • x := by
  module

example [AddCommMonoid M] [Field K] [CharZero K] [Module K M] (x : M) :
    (2:K)⁻¹ • x + (3:K)⁻¹ • x + (6:K)⁻¹ • x = x := by
  module

example [AddCommGroup M] [CommRing R] [Module R M] (a : R) (v w : M) :
    (1 + a ^ 2) • (v + w) - a • (a • v - w) = v + (1 + a + a ^ 2) • w := by
  module

example [AddCommGroup M] [CommRing R] [Module R M] (a b μ ν : R) (x y : M) :
    (μ - ν) • a • x = (a • μ • x + b • ν • y) - ν • (a • x + b • y) := by
  module

Tags:
Defined in module:: Mathlib.Tactic.Module

match_scalars

Given a goal parseable as a linear combination ⊢ a • x + ... + b • y = c • x + ... + d • y, match_scalars splits up the goal into equalities of the scalars for each respective atom. This means the example goal above is replaced by goals ⊢ a = c (from x), ..., ⊢ b = d (from y).

The module tactic is equivalent to match_scalars <;> ring1.

match_scalars can parse into expressions made of the operators +, -, • and the numeral 0. Any other subexpressions (including variables) are treated as atoms. If the goal is an equality in the type M, then match_scalars requires an AddCommMonoid M instance. If the goal contains a scalar multiplication (a : R) • (x : M), this requires a Semiring R and Module R M instance. If any of the instances are missing, match_scalars fails.

The scalar type for the goals produced by the match_scalars tactic is the largest scalar type encountered; for example, if ℕ, ℚ and a characteristic-zero field K all occur as scalars, then the goals produced are equalities in K with the appropriate casts (from ℕ, ℤ, ℚ) and algebraMaps (otherwise) inserted. Inserted casts are simplified by lemmas tagged @[push_cast]. If the set of scalar types encountered is not totally ordered (in the sense that for all rings R, S encountered, it holds that either Algebra R S or Algebra S R), then match_scalars fails.

Examples:

example [AddCommMonoid M] [Semiring R] [Module R M] (a b : R) (x : M) :
    a • x + b • x = (b + a) • x := by
  match_scalars
  -- one goal: `⊢ a * 1 + b * 1 = (b + a) * 1`

example [AddCommGroup M] [Ring R] [Module R M] (a b : R) (x : M) :
    a • (a • x - b • y) + (b • a • y + b • b • x) = x := by
  match_scalars
  -- two goals:
  -- `⊢ a * (a * 1) + b * (b * 1) = 1` (from the `x` atom)
  -- `⊢ a * -(b * 1) + b * (a * 1) = 0` (from the `y` atom)

example [AddCommGroup M] [Ring R] [Module R M] (a : R) (x : M) :
    -(2:R) • a • x = a • (-2:ℤ) • x := by
  match_scalars
  -- one goal: `⊢ -2 * (a * 1) = a * (-2 * 1)`

Tags:
Defined in module:: Mathlib.Tactic.Module

bicategory_nf

Normalize the both sides of an equality.

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.Bicategory.Basic

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.

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.Bicategory.Basic

recover

recover tacs applies the tactic (sequence) tacs and then re-adds goals that were incorrectly marked as closed. This helps to debug issues where a tactic closes goals without solving them (i.e. goals were removed from the MetaM state without the metavariable being assigned), resulting in the error "(kernel) declaration has metavariables".

Tags:
Defined in module:: Mathlib.Tactic.Recover

discrete_cases

A simple tactic to run cases on any Discrete α hypotheses.

Tags:
Defined in module:: Mathlib.CategoryTheory.Discrete.Basic

pi_lower_bound

Create a proof of a < π for a fixed rational number a, given a witness, which is a sequence of rational numbers √2 < r 1 < r 2 < ... < r n < 2 satisfying the property that √(2 + r i) ≤ r(i+1), where r 0 = 0 and √(2 - r n) ≥ a/2^(n+1).

Tags:
Defined in module:: Mathlib.Analysis.Real.Pi.Bounds

pi_upper_bound

Create a proof of π < a for a fixed rational number a, given a witness, which is a sequence of rational numbers √2 < r 1 < r 2 < ... < r n < 2 satisfying the property that √(2 + r i) ≥ r(i+1), where r 0 = 0 and √(2 - r n) ≤ (a - 1/4^n) / 2^(n+1).

Tags:
Defined in module:: Mathlib.Analysis.Real.Pi.Bounds

ring_nf

ring_nf simplifies expressions in the language of commutative (semi)rings, which rewrites all ring expressions into a normal form, allowing variables in the exponents.

ring_nf works as both a tactic and a conv tactic.

See also the ring tactic for solving a goal which is an equation in the language of commutative (semi)rings.

ring_nf! will use a more aggressive reducibility setting to identify atoms.
ring_nf (config := cfg) allows for additional configuration (see RingNF.Config):
- red: the reducibility setting (overridden by !)
- zetaDelta: if true, local let variables can be unfolded (overridden by !)
- recursive: if true, ring_nf will also recurse into atoms
ring_nf at l1 l2 ... can be used to rewrite at the given locations.

Examples: This can be used non-terminally to normalize ring expressions in the goal such as ⊢ P (x + x + x) ~> ⊢ P (x * 3), as well as being able to prove some equations that ring cannot because they involve ring reasoning inside a subterm, such as sin (x + y) + sin (y + x) = 2 * sin (x + y).

Tags:
Defined in module:: Mathlib.Tactic.Ring.RingNF

ring

ring solves equations in commutative (semi)rings, allowing for variables in the exponent. If the goal is not appropriate for ring (e.g. not an equality) ring_nf will be suggested. See also ring1, which fails if the goal is not an equality.

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

Examples:

example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring
example (x y : ℕ) : x + id y = y + id x := by ring!
example (x : ℕ) (h : x * 2 > 5): x + x > 5 := by ring; assumption -- suggests ring_nf

Tags:
Defined in module:: Mathlib.Tactic.Ring.RingNF

isBoundedDefault

Filters 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 isBoundedDefault in the statements, in the form (hf : f.IsBounded (≥) := by isBoundedDefault).

Tags:
Defined in module:: Mathlib.Order.Filter.IsBounded

unit_interval

A tactic that solves 0 ≤ ↑x, 0 ≤ 1 - ↑x, ↑x ≤ 1, and 1 - ↑x ≤ 1 for x : I.

Tags:
Defined in module:: Mathlib.Topology.UnitInterval

aux_group₂

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

Tags:
Defined in module:: Mathlib.Tactic.Group

aux_group₁

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

Tags:
Defined in module:: Mathlib.Tactic.Group

group

group normalizes expressions in multiplicative groups that occur in the goal. group does not assume commutativity, instead using only the group axioms without any information about which group is manipulated. If the goal is an equality, and after normalization the two sides are equal, group closes the goal.

For additive commutative groups, use the abel tactic instead.

group at l1 l2 ... normalizes at the given locations.

Example:

example {G : Type} [Group G] (a b c d : G) (h : c = (a*b^2)*((b*b)⁻¹*a⁻¹)*d) : a*c*d⁻¹ = a := by
  group at h -- normalizes `h` which becomes `h : c = d`
  rw [h]     -- the goal is now `a*d*d⁻¹ = a`
  group      -- which then normalized and closed

Tags:
Defined in module:: Mathlib.Tactic.Group

field_simp

field_simp normalizes expressions in (semi-)fields by rewriting them to a common denominator, i.e. to reduce them to expressions of the form n / d where neither n nor d contains any division symbol. The field_simp tactic will also clear denominators in field (in)equalities, by cross-multiplying.

A very common pattern is field_simp; ring (clear denominators, then the resulting goal is solvable by the axioms of a commutative ring). The finishing tactic field is a shorthand for this pattern.

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging fails. These denominators are made out of denominators appearing in the input expression, by repeatedly taking products or divisors. The default discharger can be non-universal, i.e. can be specific to the field at hand (order properties, explicit ≠ 0 hypotheses, CharZero if that is known, etc). See field_simp_discharge for full details of the default discharger algorithm.

field_simp at l1 l2 ... can be used to normalize at the given locations.
field_simp (disch := tac) uses the tactic sequence tac to discharge nonzeroness/positivity proofs.
field_simp [t₁, ..., tₙ] provides terms t₁, ..., tₙ to the discharger for nonzeroness/positivity proofs.

Examples:

-- `x / (1 - y) / (1 + y / (1 - y))` is reduced to `x / (1 - y + y)`
example (x y z : ℚ) (hy : 1 - y ≠ 0) :
    ⌊x / (1 - y) / (1 + y / (1 - y))⌋ < 3 := by
  field_simp
  -- new goal: `⊢ ⌊x / (1 - y + y)⌋ < 3`
  sorry

-- `field_simp` will clear the `x` denominators in the following equation
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
    (x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
  field_simp
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
  sorry

Tags:
Defined in module:: Mathlib.Tactic.FieldSimp

nontriviality

nontriviality α generates a proof of Nontrivial α and adds this as a hypothesis.

The tactic first tries to find a proof of Nontrivial α using instance synthesis. If this fails, it will derive this proof using a < b, a ≠ b or a > b hypotheses in the local context. Otherwise it will perform a case split on Subsingleton α ∨ Nontrivial α, and attempt to prove Subsingleton α implies the main goal using simp [nontriviality]. If the Subsingleton goal cannot be closed automatically, nontriviality fails.

This tactic is extensible: tag a lemma with @[nontriviality] to use it in the simp set for the Subsingleton case. All @[simp] lemmas are automatically used too.

nontriviality (without the argument α) infers the type from the main goal, if the goal is an (in)equality.
nontriviality using h₁, h₂, ..., hₙ uses h₁, ..., hₙ as extra arguments to simp in the Subsingleton case. This supports the typical simp argument syntax: nontriviality using ← h rewrites right-to-left with this argument; nontriviality using -h removes a lemma from the default simp set for this tactic invocation. nontriviality using * adds all local hypotheses to the simp set.

Examples:

example {R : Type} [OrderedRing R] {a : R} (h : 0 < a) : 0 < a := by
  nontriviality -- There is now a `Nontrivial R` hypothesis available.
  assumption

example {R : Type} [CommRing R] {r s : R} : r * s = s * r := by
  nontriviality -- There is now a `Nontrivial R` hypothesis available.
  apply mul_comm

example {R : Type} [OrderedRing R] {a : R} (h : 0 < a) : (2 : ℕ) ∣ 4 := by
  nontriviality R -- there is now a `Nontrivial R` hypothesis available.
  dec_trivial

def myeq {α : Type} (a b : α) : Prop := a = b

example {α : Type} (a b : α) (h : a = b) : myeq a b := by
  success_if_fail nontriviality α -- Fails
  nontriviality α using myeq -- There is now a `Nontrivial α` hypothesis available
  assumption

Tags:
Defined in module:: Mathlib.Tactic.Nontriviality.Core

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.

Tags:
Defined in module:: Mathlib.Tactic.ArithMult

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.

Tags:
Defined in module:: Mathlib.Tactic.ArithMult

field

field solves equality goals in (semi-)fields. The goal must be an equality which is universal, in the sense that it is true in any field in which the appropriate denominators don't vanish. (That is, it is a consequence purely of the field axioms.)

The field tactic is built from the tactics field_simp (which clears the denominators) and ring (which proves equality goals universally true in commutative (semi-)rings). If field fails to prove your goal, you may still be able to prove your goal by running the field_simp and ring_nf normalizations in some order.

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging fails. These denominators are made out of denominators appearing in the input expression, by repeatedly taking products or divisors. The default discharger can be non-universal, i.e. can be specific to the field at hand (order properties, explicit ≠ 0 hypotheses, CharZero if that is known, etc). See Mathlib.Tactic.FieldSimp.discharge for full details of the default discharger algorithm.

field (disch := tac) uses the tactic sequence tac to discharge nonzeroness proofs.
field [t₁, ..., tₙ] provides terms t₁, ..., tₙ to the discharger for nonzeroness proofs.

Examples:

example {x y : ℚ} (hx : x + y ≠ 0) : x / (x + y) + y / (x + y) = 1 := by field
example {a b : ℝ} (ha : a ≠ 0) : a / (a * b) - 1 / b = 0 := by field

-- The user can also provide additional terms to help with nonzeroness proofs:
example {K : Type*} [Field K] (hK : ∀ x : K, x ^ 2 + 1 ≠ 0) (x : K) :
    1 / (x ^ 2 + 1) + x ^ 2 / (x ^ 2 + 1) = 1 := by
  field [hK]

example {a b : ℚ} (H : b + a ≠ 0) : a / (a + b) + b / (b + a) = 1 := by
  -- `field` cannot prove this on its own.
  fail_if_success field
  -- But running `ring_nf` and `field_simp` in a different order works:
  ring_nf at *
  field

Tags:
Defined in module:: Mathlib.Tactic.Field

reduce_mod_char

The tactic reduce_mod_char looks for numeric expressions in characteristic p and reduces these to lie between 0 and p.

For example:

example : (5 : ZMod 4) = 1 := by reduce_mod_char
example : (X ^ 2 - 3 * X + 4 : (ZMod 4)[X]) = X ^ 2 + X := by reduce_mod_char

It also handles negation, turning it into multiplication by p - 1, and similarly subtraction.

This tactic uses the type of the subexpression to figure out if it is indeed of positive characteristic, for improved performance compared to trying to synthesise a CharP instance. The variant reduce_mod_char! also tries to use CharP R n hypotheses in the context. (Limitations of the typeclass system mean the tactic can't search for a CharP R n instance if n is not yet known; use have : CharP R n := inferInstance; reduce_mod_char! as a workaround.)

Tags:
Defined in module:: Mathlib.Tactic.ReduceModChar

swap_var

swap_var swap_rule₁, swap_rule₂, ⋯ applies swap_rule₁ then swap_rule₂ then ⋯.

A swap_rule is of the form x y or x ↔ y, and "applying it" means swapping the variable name x by y and vice-versa on all hypotheses and the goal.

example {P Q : Prop} (q : P) (p : Q) : P ∧ Q := by
  swap_var p ↔ q
  exact ⟨p, q⟩

Tags:
Defined in module:: Mathlib.Tactic.SwapVar

nlinarith

An extension of linarith with some preprocessing to allow it to solve some nonlinear arithmetic problems. (Based on Coq's nra tactic.) See linarith for the available syntax of options, which are inherited by nlinarith; that is, nlinarith! and nlinarith only [h1, h2] all work as in linarith. The preprocessing is as follows:

For every subterm a ^ 2 or a * a in a hypothesis or the goal, the assumption 0 ≤ a ^ 2 or 0 ≤ a * a is added to the context.
For every pair of hypotheses a1 R1 b1, a2 R2 b2 in the context, R1, R2 ∈ {<, ≤, =}, the assumption 0 R' (b1 - a1) * (b2 - a2) is added to the context (non-recursively), where R ∈ {<, ≤, =} is the appropriate comparison derived from R1, R2.

Tags:
Defined in module:: Mathlib.Tactic.Linarith.Frontend

linarith?

linarith? behaves like linarith but, on success, it prints a suggestion of the form linarith only [...] listing a minimized set of hypotheses used in the final proof. Use linarith?! for the higher-reducibility variant and set the minimize flag in the configuration to control whether greedy minimization is performed.

Tags:
Defined in module:: Mathlib.Tactic.Linarith.Frontend

linarith

linarith attempts to find a contradiction between hypotheses that are linear (in)equalities. Equivalently, it can prove a linear inequality by assuming its negation and proving False.

In theory, linarith should prove any goal that is true in the theory of linear arithmetic over the rationals. While there is some special handling for non-dense orders like Nat and Int, this tactic is not complete for these theories and will not prove every true goal. It will solve goals over arbitrary types that instantiate CommRing, LinearOrder and IsStrictOrderedRing.

An example:

example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0) : False := by
  linarith

linarith will use all appropriate hypotheses and the negation of the goal, if applicable. Disequality hypotheses require case splitting and are not normally considered (see the splitNe option below).

linarith [t1, t2, t3] will additionally use proof terms t1, t2, t3.

linarith only [h1, h2, h3, t1, t2, t3] will use only the goal (if relevant), local hypotheses h1, h2, h3, and proofs t1, t2, t3. It will ignore the rest of the local context.

linarith! will use a stronger reducibility setting to try to identify atoms. For example,

example (x : ℚ) : id x ≥ x := by
  linarith

will fail, because linarith will not identify x and id x. linarith! will. This can sometimes be expensive.

linarith (config := { .. }) takes a config object with five optional arguments:

discharger specifies a tactic to be used for reducing an algebraic equation in the proof stage. The default is ring. Other options include simp for basic problems.
transparency controls how hard linarith will try to match atoms to each other. By default it will only unfold reducible definitions.
If splitHypotheses is true, linarith will split conjunctions in the context into separate hypotheses.
If splitNe is true, linarith will case split on disequality hypotheses. For a given x ≠ y hypothesis, linarith is run with both x < y and x > y, and so this runs linarith exponentially many times with respect to the number of disequality hypotheses. (false by default.)
If exfalso is false, linarith will fail when the goal is neither an inequality nor False. (true by default.)
If minimize is false, linarith? will report all hypotheses appearing in its initial proof without attempting to drop redundancies. (true by default.)
restrict_type (not yet implemented in mathlib4) will only use hypotheses that are inequalities over tp. This is useful if you have e.g. both integer- and rational-valued inequalities in the local context, which can sometimes confuse the tactic.

A variant, nlinarith, does some basic preprocessing to handle some nonlinear goals.

The option set_option trace.linarith true will trace certain intermediate stages of the linarith routine.

Tags:
Defined in module:: Mathlib.Tactic.Linarith.Frontend

witt_truncateFun_tac

A macro tactic used to prove that truncateFun respects ring operations.

Tags:
Defined in module:: Mathlib.RingTheory.WittVector.Truncated

apply

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

Tags:
Defined in module:: Mathlib.Tactic.ApplyAt

init_ring

init_ring is an auxiliary tactic that discharges goals factoring init over ring operations.

Tags:
Defined in module:: Mathlib.RingTheory.WittVector.InitTail

ac_change

ac_change t on a goal ⊢ t' changes the goal to ⊢ t and adds new goals for proving the equality t' = t using congruence, then tries proving these goals by associativity and commutativity. The goals are created like congr! would. In other words, ac_change t is like convert_to t followed by ac_refl.

Like refine e, any holes (?_ or ?x) in t that are not solved by unification are converted into new goals, using the hole's name, if any, as the goal case name. Like congr!, convert_to introduces variables while applying congruence rules. These can be pattern-matched, like rintro would, using the with keyword.

ac_change t using n, where n is a positive numeral, controls the depth with which congruence is applied. For example, if the main goal is ⊢ Prime ((a * b + 1) + c), then ac_change Prime ((1 + a * b) + c) using 2 solves the side goals, and ac_change Prime ((1 + a * b) + c) using 3 (or more) results in two (impossible) goals ⊢ 1 = a * b and ⊢ a * b = 1. The default value for n is 1.

Example:

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

Tags:
Defined in module:: Mathlib.Tactic.Convert

convert_to

convert_to t on a goal ⊢ t' changes the goal to ⊢ t and adds new goals for proving the equality t' = t using congruence. The goals are created like congr! would. Any remaining congruence goals come before the main goal. Like refine e, any holes (?_ or ?x) in t that are not solved by unification are converted into new goals, using the hole's name, if any, as the goal case name. Like congr!, convert_to introduces variables while applying congruence rules. These can be pattern-matched, like rintro would, using the with keyword.

convert e, where e is a term of type t, uses e to close the new main goal. In other words, convert e works like convert_to t; refine e. Both tactics use the same options.

convert_to ty at h changes the type of the local hypothesis h to ty. If later local hypotheses or the goal depend on h, then convert_to t at h may leave a copy of h.
convert_to ← t creates equality goals in the opposite direction (with the original goal type on the right).
convert_to t using n, where n is a positive numeral, controls the depth with which congruence is applied. For example, if the main goal is ⊢ Prime (n + n + 1), then convert_to Prime (2 * n + 1) using 2 results in one goal, ⊢ n + n = 2 * n, and convert_to Prime (2 * n + 1) using 3 (or more) results in two (impossible) goals ⊢ HAdd.hAdd = HMul.hMul and ⊢ n = 2. The default value for n is 1.
convert_to t with x ⟨y₁, y₂⟩ (z₁ | z₂) names or pattern-matches the variables introduced by congruence rules, like rintro x ⟨y₁, y₂⟩ (z₁ | z₂) would.
convert_to (config := cfg) t uses the configuration options in cfg to control the congruence rules (see Congr!.Config).

Tags:
Defined in module:: Mathlib.Tactic.Convert

convert

convert e, where the term e is inferred to have type t, replaces the main goal ⊢ t' with new goals for proving the equality t' = t using congruence. The goals are created like congr! would. Like refine e, any holes (?_ or ?x) in e that are not solved by unification are converted into new goals, using the hole's name, if any, as the goal case name. Like congr!, convert introduces variables while applying congruence rules. These can be pattern-matched, like rintro would, using the with keyword.

See also convert_to t, where t specifies the expected type, instead of a proof term of type t. In other words, convert_to t works like convert (?_ : t). Both tactics use the same options.

convert ← e creates equality goals in the opposite direction (with the goal type on the right).
convert e using n, where n is a positive numeral, controls the depth with which congruence is applied. For example, if the main goal is ⊢ Prime (n + n + 1) and e : Prime (2 * n + 1), then convert e using 2 results in one goal, ⊢ n + n = 2 * n, and convert e using 3 (or more) results in two (impossible) goals ⊢ HAdd.hAdd = HMul.hMul and ⊢ n = 2. By default, the depth is unlimited.
convert e with x ⟨y₁, y₂⟩ (z₁ | z₂) names or pattern-matches the variables introduced by congruence rules, like rintro x ⟨y₁, y₂⟩ (z₁ | z₂) would.
convert (config := cfg) e uses the configuration options in cfg to control the congruence rules (see Congr!.Config).

Examples:

-- `convert using` controls the depth of congruence.
example {n : ℕ} (e : Prime (2 * n + 1)) :
    Prime (n + n + 1) := by
  convert e using 2
  -- One goal: ⊢ n + n = 2 * n
  ring

-- `convert` can fail where `exact` succeeds.
example (h : p 0) : p 1 := by
  fail_if_success
    convert h -- fails, left-over goal 1 = 0
    done
  exact h -- succeeds

-- `convert with` names introduced variables.
example (p q : Nat → Prop) (h : ∀ ε > 0, p ε) :
    ∀ ε > 0, q ε := by
  convert h using 2 with ε hε
  -- Goal now looks like:
  -- hε : ε > 0
  -- ⊢ q ε ↔ p ε
  sorry

Tags:
Defined in module:: Mathlib.Tactic.Convert

specialize_all

specialize_all x runs specialize h x for all hypotheses h where this tactic succeeds.

Tags:
Defined in module:: Mathlib.Tactic.TautoSet

tauto_set

tauto_set attempts to prove tautologies involving hypotheses and goals of the form X ⊆ Y or X = Y, where X, Y are expressions built using ∪, ∩, , and ᶜ from finitely many variables of type Set α. It also unfolds expressions of the form Disjoint A B and symmDiff A B.

Examples:

example {α} (A B C D : Set α) (h1 : A ⊆ B) (h2 : C ⊆ D) : C \ B ⊆ D \ A := by
  tauto_set

example {α} (A B C : Set α) (h1 : A ⊆ B ∪ C) : (A ∩ B) ∪ (A ∩ C) = A := by
  tauto_set

Tags:
Defined in module:: Mathlib.Tactic.TautoSet

volume_tac

The tactic exact volume, to be used in optional (autoParam) arguments.

Tags:
Defined in module:: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

valid

A wrapper for omega which prefaces it with some quick and useful attempts

Tags:
Defined in module:: Mathlib.CategoryTheory.ComposableArrows.Basic

nth_rw

nth_rw is a variant of rw that only changes the n₁, ..., nₖᵗʰ occurrence of the expression to be rewritten. Like rw, and unlike nth_rewrite, it will try to close the goal by trying rfl afterwards. nth_rw n₁ ... nₖ [eq₁, eq₂,..., eqₘ] will rewrite the n₁, ..., nₖᵗʰ occurrence of each of the m equalities eqᵢin that order. Occurrences are counted beginning with 1 in order of precedence. For example,

example (h : a = 1) : a + a + a + a + a = 5 := by
  nth_rw 2 3 [h]
/-
a: ℕ
h: a = 1
⊢ a + 1 + 1 + a + a = 5
-/

Notice that the second and third occurrences of a from the left have been rewritten by nth_rw.

To understand the importance of order of precedence, consider the example below

example (a b c : Nat) : (a + b) + c = (b + a) + c := by
  nth_rewrite 2 [Nat.add_comm] -- ⊢ (b + a) + c = (b + a) + c

Here, although the occurrence parameter is 2, (a + b) is rewritten to (b + a). This happens because in order of precedence, the first occurrence of _ + _ is the one that adds a + b to c. The occurrence in a + b counts as the second occurrence.

If a term t is introduced by rewriting with eqᵢ, then this instance of t will be counted as an occurrence of t for all subsequent rewrites of t with eqⱼ for j > i. This behaviour is illustrated by the example below

example (h : a = a + b) : a + a + a + a + a = 0 := by
  nth_rw 3 [h, h]
/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b + b) + a + a = 0
-/

Here, the first nth_rw with h introduces an additional occurrence of a in the goal. That is, the goal state after the first rewrite looks like below

/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b) + a + a = 0
-/

This new instance of a also turns out to be the third occurrence of a. Therefore, the next nth_rw with h rewrites this a.

Further, nth_rw will close the remaining goal with rfl if possible.

Tags:
Defined in module:: Mathlib.Tactic.NthRewrite

nth_rewrite

nth_rewrite is a variant of rewrite that only changes the n₁, ..., nₖᵗʰ occurrence of the expression to be rewritten. nth_rewrite n₁ ... nₖ [eq₁, eq₂,..., eqₘ] will rewrite the n₁, ..., nₖᵗʰ occurrence of each of the m equalities eqᵢin that order. Occurrences are counted beginning with 1 in order of precedence.

For example,

example (h : a = 1) : a + a + a + a + a = 5 := by
  nth_rewrite 2 3 [h]
/-
a: ℕ
h: a = 1
⊢ a + 1 + 1 + a + a = 5
-/

Notice that the second and third occurrences of a from the left have been rewritten by nth_rewrite.

To understand the importance of order of precedence, consider the example below

example (a b c : Nat) : (a + b) + c = (b + a) + c := by
  nth_rewrite 2 [Nat.add_comm] -- ⊢ (b + a) + c = (b + a) + c

example (h : a = a + b) : a + a + a + a + a = 0 := by
  nth_rewrite 3 [h, h]
/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b + b) + a + a = 0
-/

Here, the first nth_rewrite with h introduces an additional occurrence of a in the goal. That is, the goal state after the first rewrite looks like below

/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b) + a + a = 0
-/

This new instance of a also turns out to be the third occurrence of a. Therefore, the next nth_rewrite with h rewrites this a.

Tags:
Defined in module:: Mathlib.Tactic.NthRewrite

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 : ‖c‖ ≤ ‖z‖) (z3 : 3 ≤ ‖z‖) :
    2 * ‖z‖ ≤ ‖z^2 + c‖ := by
  calc ‖z^2 + c‖
    _ ≥ ‖z^2‖ - ‖c‖ := by bound
    _ ≥ ‖z^2‖ - ‖z‖ := by  bound
    _ ≥ (‖z‖ - 1) * ‖z‖ := by
      rw [mul_comm, mul_sub_one, ← pow_two, ← norm_pow]
    _ ≥ 2 * ‖z‖ := by bound

bound is built on top of aesop, and uses

Apply lemmas registered via the @[bound] attribute
Forward lemmas registered via the @[bound_forward] attribute
Local hypotheses from the context
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).

Tags:
Defined in module:: Mathlib.Tactic.Bound

smul_tac

Solve equations for K⟮X⟯ by applying RatFunc.induction_on.

Tags:
Defined in module:: Mathlib.FieldTheory.RatFunc.Basic

frac_tac

Solve equations for K⟮X⟯ by working in FractionRing K[X].

Tags:
Defined in module:: Mathlib.FieldTheory.RatFunc.Basic

peel

Peels matching quantifiers off of a given term and the goal and introduces the relevant variables.

peel e peels all quantifiers (at reducible transparency), using this for the name of the peeled hypothesis.
peel e with h is peel e but names the peeled hypothesis h. If h is _ then uses this for the name of the peeled hypothesis.
peel n e peels n quantifiers (at default transparency).
peel n e with x y z ... h peels n quantifiers, names the peeled hypothesis h, and uses x, y, z, and so on to name the introduced variables; these names may be _. If h is _ then uses this for the name of the peeled hypothesis. The length of the list of variables does not need to equal n.
peel e with x₁ ... xₙ h is peel n e with x₁ ... xₙ h.

There are also variants that apply to an iff in the goal:

peel n peels n quantifiers in an iff.
peel with x₁ ... xₙ peels n quantifiers in an iff and names them.

Given p q : ℕ → Prop, h : ∀ x, p x, and a goal ⊢ : ∀ x, q x, the tactic peel h with x h' will introduce x : ℕ, h' : p x into the context and the new goal will be ⊢ q x. This works with ∃, as well as ∀ᶠ and ∃ᶠ, and it can even be applied to a sequence of quantifiers. Note that this is a logically weaker setup, so using this tactic is not always feasible.

For a more complex example, given a hypothesis and a goal:

h : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε
⊢ ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) ≤ ε

(which differ only in </≤), applying peel h with ε hε N n hn h_peel will yield a tactic state:

h : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε
ε : ℝ
hε : 0 < ε
N n : ℕ
hn : N ≤ n
h_peel : 1 / (n + 1 : ℝ) < ε
⊢ 1 / (n + 1 : ℝ) ≤ ε

and the goal can be closed with exact h_peel.le. Note that in this example, h and the goal are logically equivalent statements, but peel cannot be immediately applied to show that the goal implies h.

In addition, peel supports goals of the form (∀ x, p x) ↔ ∀ x, q x, or likewise for any other quantifier. In this case, there is no hypothesis or term to supply, but otherwise the syntax is the same. So for such goals, the syntax is peel 1 or peel with x, and after which the resulting goal is p x ↔ q x. The congr! tactic can also be applied to goals of this form using congr! 1 with x. While congr! applies congruence lemmas in general, peel can be relied upon to only apply to outermost quantifiers.

Finally, the user may supply a term e via ... using e in order to close the goal immediately. In particular, peel h using e is equivalent to peel h; exact e. The using syntax may be paired with any of the other features of peel.

This tactic works by repeatedly applying lemmas such as forall_imp, Exists.imp, Filter.Eventually.mp, Filter.Frequently.mp, and Filter.Eventually.of_forall.

Tags:
Defined in module:: Mathlib.Tactic.Peel

ring1

ring1 solves the goal when it is an equality in commutative (semi)rings, allowing variables in the exponent.

This version of ring fails if the target is not an equality.

ring1! uses a more aggressive reducibility setting to determine equality of atoms.

Extensions:

- ring1_nf additionally uses ring_nf to simplify in atoms.
- ring1_nf! will use a more aggressive reducibility setting to determine equality of atoms.* ring1_nf additionally uses ring_nf to simplify in atoms.
ring1_nf! will use a more aggressive reducibility setting to determine equality of atoms.

Tags:
Defined in module:: Mathlib.Tactic.Ring.Basic

conv_rhs

conv_rhs => cs runs the conv tactic sequence cs on the right hand side of the target.

In general, for an n-ary operator as the target, it traverses into the last argument. It is a synonym for conv => arg -1; cs.

conv_rhs at h => cs runs cs on the right hand side of hypothesis h.
conv_rhs in pat => cs first looks for a subexpression matching pat (see the pattern conv tactic) and then traverses into the right hand side of this subexpression. This syntax also supports the occs clause for the pattern.

Tags:
Defined in module:: Mathlib.Tactic.Conv

conv_lhs

conv_lhs => cs runs the conv tactic sequence cs on the left hand side of the target.

In general, for an n-ary operator as the target, it traverses into the second to last argument. It is a synonym for conv => arg -2; cs.

conv_lhs at h => cs runs cs on the left hand side of hypothesis h.
conv_lhs in pat => cs first looks for a subexpression matching pat (see also the pattern conv tactic) and then traverses into the left hand side of this subexpression. This syntax also supports the occs clause for the pattern.

Tags:
Defined in module:: Mathlib.Tactic.Conv

clear!

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

Tags:
Defined in module:: Mathlib.Tactic.ClearExclamation

conv?

Display a widget panel allowing to generate a conv call zooming to the subexpression selected in the goal or in the type of a local hypothesis or let-decl.

Tags:
Defined in module:: Mathlib.Tactic.Widget.Conv

substs

Applies the subst tactic to all given hypotheses from left to right.

Tags:
Defined in module:: Mathlib.Tactic.Substs

existsi

existsi e₁, e₂, ⋯ instantiates existential quantifiers in the main goal by using e₁, e₂, ... as witnesses. existsi e₁, e₂, ⋯ is equivalent to refine ⟨e₁, e₂, ⋯, ?_⟩.

See also exists: exists e₁, e₂, ⋯ is equivalent to existsi e₁, e₂, ⋯; try trivial.

Examples:

example : ∃ x : Nat, x = x := by
  existsi 42
  rfl

example : ∃ x : Nat, ∃ y : Nat, x = y := by
  existsi 42, 42
  rfl

Tags:
Defined in module:: Mathlib.Tactic.ExistsI

noncomm_ring

noncomm_ring simplifies expressions in not-necessarily-commutative rings in the main goal then tries closing it by "cheap" (reducible) rfl. This tactic supports the operators +, *, -, ^ and • (for scalar multiplication by natural numbers or integers).

If the ring is commutative, prefer the ring tactic instead, which is more powerful and efficient. The tactic is implemented as a combination of simp only [...] and abel. The precise invocation of simp only can be customized using the options listed below.

Limitation: numeric powers are unfolded entirely with pow_succ and can easily exceed the maximum recursion depth.

noncomm_ring [h] adds the term h as simplification lemma, rewriting from left to right. Multiple arguments can be combined as noncomm_ring [h₁, ..., hₙ].
noncomm_ring [← h] adds the term h as simplification lemma, rewriting from right to left.
noncomm_ring [*] simplifies using all hypotheses in the local context.
noncomm_ring (config := cfg) uses cfg as configuration for the simplification step. See Lean.Meta.Simp.Config for more details.
noncomm_ring (discharger := tac) uses the tactic sequence tac to discharge assumptions to the simplification lemmas. This only applies to user-supplied lemmas, since the default lemmas used by noncomm_ring do not require a discharger.

Example:

example {R : Type*} [Ring R] (a b c : R) : a * (b + c + c - b) = 2 * a * c := by
  noncomm_ring

Tags:
Defined in module:: Mathlib.Tactic.NoncommRing

replace

Acts like have, but removes a hypothesis with the same name as this one if possible. For example, if the state is:

Then after replace h : β the state will be:

case h
f : α → β
h : α
⊢ β

f : α → β
h : β
⊢ goal

whereas have h : β would result in:

case h
f : α → β
h : α
⊢ β

f : α → β
h✝ : α
h : β
⊢ goal

Tags:
Defined in module:: Mathlib.Tactic.Replace

observe

observe hp : p asserts the proposition p as a hypothesis named hp, and tries to prove it using exact?. If no proof is found, the tactic fails. In other words, this tactic is equivalent to have hp : p := by exact?.

observe : p uses the name this for the new hypothesis.
observe? hp : p will emit a trace message of the form have hp : p := proof_term. This may be particularly useful to speed up proofs.

Tags:
Defined in module:: Mathlib.Tactic.Observe

measurability

The tactic measurability solves goals of the form Measurable f, AEMeasurable f, StronglyMeasurable f, AEStronglyMeasurable f μ, or MeasurableSet s by applying lemmas tagged with the measurability user attribute.

Note that measurability uses fun_prop for solving measurability of functions, so statements about Measurable, AEMeasurable, StronglyMeasurable and AEStronglyMeasurable should be tagged with fun_prop rather that measurability. The measurability attribute is equivalent to fun_prop in these cases for backward compatibility with the earlier implementation.

Tags:
Defined in module:: Mathlib.Tactic.Measurability

measurability?

The tactic measurability? solves goals of the form Measurable f, AEMeasurable f, StronglyMeasurable f, AEStronglyMeasurable f μ, or MeasurableSet s by applying lemmas tagged with the measurability user attribute, and suggests a faster proof script that can be substituted for the tactic call in case of success.

Tags:
Defined in module:: Mathlib.Tactic.Measurability

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.

Tags:
Defined in module:: Mathlib.Tactic.ENatToNat

enat_to_nat

enat_to_nat shifts all ENats in the context to Nat, rewriting propositions about them. A typical use case is enat_to_nat; lia.

Tags:
Defined in module:: Mathlib.Tactic.ENatToNat

fconstructor

fconstructor, on a goal which is an inductive type, solves it by applying the first matching constructor, creating new goals for all arguments to the constructor in the same order. This is like constructor except the goals are not reordered.

Tags:
Defined in module:: Mathlib.Tactic.Constructor

econstructor

econstructor, on a goal which is an inductive type, solves it by applying the first matching constructor, creating new goals for non-dependent arguments to the constructor in the same order. This is like constructor except only non-dependent arguments are shown as new goals.

Tags:
Defined in module:: Mathlib.Tactic.Constructor

sleep_heartbeats

do nothing for at least n heartbeats

Tags:
Defined in module:: Mathlib.Util.SleepHeartbeats

toFinite_tac

A tactic (for use in default params) that applies Set.toFinite to synthesize a Set.Finite term.

Tags:
Defined in module:: Mathlib.Data.Set.Card

to_encard_tac

A tactic useful for transferring proofs for encard to their corresponding card statements

Tags:
Defined in module:: Mathlib.Data.Set.Card

abel

abel solves 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.
- abel_nf at h rewrites 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 also recurses into atoms.
abel!, abel1!, abel_nf! use a more aggressive reducibility setting to identify atoms.

Examples:

example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel

Tags:
Defined in module:: Mathlib.Tactic.Abel

fin_omega

fin_omega is a preprocessor for omega to handle inequalities in Fin. It rewrites all hypotheses and the goal, turning statements about addition, subtraction and inequalities in Fin n into statements that omega can use/solve. Note that this involves a lot of case splitting, so may be slow.

Tags:
Defined in module:: Mathlib.Data.Fin.Basic

monoidal

Use the coherence theorem for monoidal categories to solve equations in a monoidal category, 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, monoidal 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 monoidal_coherence.

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.Monoidal.Basic

monoidal_nf

Normalize the both sides of an equality.

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.Monoidal.Basic

introv

The tactic introv allows the user to automatically introduce the variables of a theorem and explicitly name the non-dependent hypotheses. Any dependent hypotheses are assigned their default names.

Examples:

example : ∀ a b : Nat, a = b → b = a := by
  introv h,
  exact h.symm

The state after introv h is

a b : ℕ,
h : a = b
⊢ b = a

example : ∀ a b : Nat, a = b → ∀ c, b = c → a = c := by
  introv h₁ h₂,
  exact h₁.trans h₂

The state after introv h₁ h₂ is

a b : ℕ,
h₁ : a = b,
c : ℕ,
h₂ : b = c
⊢ a = c

Tags:
Defined in module:: Mathlib.Tactic.Basic

match_target

Deprecated: use guard_target =~ t instead.

Tags:
Defined in module:: Mathlib.Tactic.Basic

assumption'

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

Tags:
Defined in module:: Mathlib.Tactic.Basic

clear_aux_decl

This tactic clears all auxiliary declarations from the context.

Tags:
Defined in module:: Mathlib.Tactic.Basic

tauto

tauto breaks down assumptions of the form _ ∧ _, _ ∨ _, _ ↔ _ and ∃ _, _ and splits a goal of the form _ ∧ _, _ ↔ _ or ∃ _, _ until it can be discharged using rfl or solve_by_elim. This is a finishing tactic: it either closes the goal or raises an error.

The Lean 3 version of this tactic by default attempted to avoid classical reasoning where possible. This Lean 4 version makes no such attempt. The itauto tactic is designed for that purpose.

Tags:
Defined in module:: Mathlib.Tactic.Tauto

rify

The rify tactic is used to shift propositions from ℕ, ℤ or ℚ to ℝ. Although less useful than its cousins zify and qify, it can be useful when your goal or context already involves real numbers.

In the example below, assumption hn is about natural numbers, hk is about integers and involves casting a natural number to ℤ, and the conclusion is about real numbers. The proof uses rify to lift both assumptions to ℝ before calling linarith.

example {n : ℕ} {k : ℤ} (hn : 8 ≤ n) (hk : 2 * k ≤ n + 2) :
    (0 : ℝ) < n - k - 1 := by
  rify at hn hk /- Now have hn : 8 ≤ (n : ℝ)   hk : 2 * (k : ℝ) ≤ (n : ℝ) + 2 -/
  linarith

rify makes use of the @[zify_simps], @[qify_simps] and @[rify_simps] attributes to move propositions, and the push_cast tactic to simplify the ℝ-valued expressions.

rify can be given extra lemmas to use in simplification. This is especially useful in the presence of nat subtraction: passing ≤ arguments will allow push_cast to do more work.

example (a b c : ℕ) (h : a - b < c) (hab : b ≤ a) : a < b + c := by
  rify [hab] at h ⊢
  linarith

Note that zify or qify would work just as well in the above example (and zify is the natural choice since it is enough to get rid of the pathological ℕ subtraction).

Tags:
Defined in module:: Mathlib.Tactic.Rify

rewrite!

rewrite! is like rewrite, but can also insert casts to adjust types that depend on the LHS of a rewrite. It is available as an ordinary tactic and a conv tactic.

The sort of casts that are inserted is controlled by the castMode configuration option. By default, only proof terms are casted; by proof irrelevance, this adds no observable complexity.

With rewrite! +letAbs (castMode := .all), casts are inserted whenever necessary. This means that the 'motive is not type correct' error never occurs, at the expense of creating potentially complicated terms.

Tags:
Defined in module:: Mathlib.Tactic.DepRewrite

rw!

rw! is like rewrite!, but also cleans up introduced refl-casts after every substitution. It is available as an ordinary tactic and a conv tactic.

Tags:
Defined in module:: Mathlib.Tactic.DepRewrite

filter_upwards

filter_upwards [h₁, ⋯, hₙ] replaces a goal of the form s ∈ f and terms h₁ : t₁ ∈ f, ⋯, hₙ : tₙ ∈ f with ∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s. The list is an optional parameter, [] being its default value.

filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ is a short form for { filter_upwards [h₁, ⋯, hₙ], intro a₁ a₂ ⋯ aₖ }.

filter_upwards [h₁, ⋯, hₙ] using e is a short form for { filter_upwards [h1, ⋯, hn], exact e }.

Combining both shortcuts is done by writing filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ using e. Note that in this case, the aᵢ terms can be used in e.

Tags:
Defined in module:: Mathlib.Order.Filter.Defs

use

use e₁, e₂, ⋯ instantiates all existential quantifiers in the main goal by using e₁, e₂, ... as witnesses, creates goals for all the remaining witnesses, and tries to discharge these goals automatically.

use is similar to exists or existsi, but unlike exists it is equivalent to applying the tactic refine ⟨e₁, e₂, ⋯, ?_, ⋯, ?_⟩ with any number of placeholders (rather than just one) and then trying to close goals associated to the placeholders with a configurable discharger (rather than just try trivial).

use! e₁, e₂, ⋯ applies constructors everywhere rather than just for goals that correspond to the last argument of a constructor. This gives the effect that nested constructors are being flattened out, with the supplied values being used along the leaves and nodes of the tree of constructors.
use (discharger := tac) e₁, e₂, ... calls tac as a discharger, on all remaining Prop-valued goals. If this option is omitted, use calls try with_reducible use_discharger as default discharger. To turn off the discharger and keep all goals, use (discharger := skip). To allow "heavy refls", use (discharger := try use_discharger). If tac fails on the new goal, use (discharger := tac) fails (hint: you might want to use (discharger := try tac) instead).

Examples:

example : ∃ x : Nat, x = x := by use 42

example : ∃ x : Nat, ∃ y : Nat, x = y := by use 42, 42

example : Nonempty Nat := by use 5

example : Nonempty (PNat ≃ Nat) := by
  use PNat.natPred, Nat.succPNat
  · exact PNat.succPNat_natPred
  · intro; rfl

-- With `use!` one can feed in each `42` one at a time:
example : ∃ n : {n : Nat // n % 2 = 0}, n.val > 10 := by use! 20; simp

example : ∃ p : Nat × Nat, p.1 = p.2 := by use! (42, 42)
/-
The second line makes use of the fact that `use!` tries refining with the argument before
applying a constructor. Also note that `use`/`use!` by default uses a tactic
called `use_discharger` to discharge goals, so `use! 42` will close the goal in this example since
`use_discharger` applies `rfl`, which as a consequence solves for the other `Nat` metavariable.
-/

Tags:
Defined in module:: Mathlib.Tactic.Use

use_discharger

use_discharger is used by use to discharge side goals.

This is an extensible tactic using macro_rules. By default it can:

rewrite a goal ∃ _ : p, q into p ∧ q if p is in Prop;
solve the goal p ∧ q by creating subgoals p and q;
apply rfl;
solve a goal by applying an assumption;
solve the goal True.

Tags:
Defined in module:: Mathlib.Tactic.Use

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 normalized using push Not. For instance, ¬ a < b will be changed to b ≤ a. by_contra! can be used with rcases patterns. For instance, by_contra! rfl on ⊢ s.Nonempty will substitute the equality s = ∅, and by_contra! ⟨hp, hq⟩ on ⊢ ¬ p ∨ ¬ q will introduce hp : p and hq : q. 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

Tags:
Defined in module:: Mathlib.Tactic.ByContra

clean

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

Tags:
Defined in module:: Mathlib.Tactic.Clean

gcongr?

Display a widget panel allowing to generate a gcongr call with holes specified by selecting subexpressions in the goal.

Tags:
Defined in module:: Mathlib.Tactic.Widget.GCongr

subsingleton

The subsingleton tactic tries to prove a goal of the form x = y or x ≍ y using the fact that the types involved are subsingletons (a type with exactly zero or one terms). To a first approximation, it does apply Subsingleton.elim. As a nicety, subsingleton first runs the intros tactic.

If the goal is an equality, it either closes the goal or fails.
subsingleton [inst1, inst2, ...] can be used to add additional Subsingleton instances to the local context. This can be more flexible than have := inst1; have := inst2; ...; subsingleton since the tactic does not require that all placeholders be solved for.

Techniques the subsingleton tactic can apply:

proof irrelevance
heterogeneous proof irrelevance (via proof_irrel_heq)
using Subsingleton (via Subsingleton.elim)
proving BEq instances are equal if they are both lawful (via lawful_beq_subsingleton)

Properties #

The tactic is careful not to accidentally specialize Sort _ to Prop, avoiding the following surprising behavior of apply Subsingleton.elim:

example (α : Sort _) (x y : α) : x = y := by apply Subsingleton.elim

The reason this example goes through is that it applies the ∀ (p : Prop), Subsingleton p instance, specializing the universe level metavariable in Sort _ to 0.

Tags:
Defined in module:: Mathlib.Tactic.Subsingleton

extract_goal

extract_goal formats the current goal as a stand-alone theorem or definition after cleaning up the local context of irrelevant variables.

A variable is relevant if (1) it occurs in the target type, (2) there is a relevant variable that depends on it, or (3) the type of the variable is a proposition that depends on a relevant variable. If the target is False, then for convenience extract_goal includes all variables.

The tactic tries to produce an output that can be copy-pasted and just work, but its success depends on whether the expressions are amenable to being unambiguously pretty printed. The tactic responds to pretty printing options. For example, set_option pp.all true in extract_goal gives the pp.all form.

extract_goal * formats the current goal without cleaning up the local context.
extract_goal a b c ... formats the current goal after removing everything that the given variables a, b, c, ... do not depend on.
extract_goal ... using name uses the name name for the theorem or definition rather than the autogenerated name.

Tags:
Defined in module:: Mathlib.Tactic.ExtractGoal

type_check

Type check the given expression, and trace its type.

Tags:
Defined in module:: Mathlib.Tactic.TypeCheck

gcongr_discharger

gcongr_discharger is used by gcongr to discharge side goals.

This is an extensible tactic using macro_rules. By default it calls positivity (after importing the positivity tactic). Example: macro_rules | `(tactic| gcongr_discharger) => `(tactic| positivity).

Tags:
Defined in module:: Mathlib.Tactic.GCongr.Core

gcongr

gcongr applies "generalized congruence" rules to recursively reduce a goal of form ⊢ R (f a₁ ... aₙ) (f b₁ ... bₙ) to (possibly multiple) goal(s) ⊢ Rᵢ aᵢ bᵢ, keeping only the distinct pairs aᵢ ≠ bᵢ, where Rᵢ is a possibly different relation (depending on the precise rule). The relations R, Rᵢ can be any two-argument relation, including · → ·.

This tactic is extensible: to add a "generalized congruence" rule, tag a theorem with the attribute @[gcongr].

If a "generalized congruence" lemma has a side goal, gcongr will try to discharge it using gcongr_discharger, which is an extensible tactic based on positivity. Side goals not discharged in this way are left for the user.

gcongr with x y ... z names the variables that are introduced by descending into binders (for example sums or suprema).
gcongr n, where n is a natural number literal, limits the depth of the recursive applications. This is useful if gcongr is too aggressive in breaking down the goal.
gcongr t, where t is a term with ?_ holes, performs congruence up to the holes in t. In other words, gcongr f ?_ turns a goal ⊢ R (f x) (f y) into ⊢ R x y (but no further). This is useful if gcongr is too aggressive in breaking down the goal.

Examples:

example {a b x c d : ℝ} (h1 : a + 1 ≤ b + 1) (h2 : c + 2 ≤ d + 2) :
    x ^ 2 * a + c ≤ x ^ 2 * b + d := by
  -- LHS and RHS both have the form x ^ 2 * ?_ + ?_
  gcongr
  · -- New goal: ⊢ a ≤ b
    linarith
  · -- ⊢ New goal: c ≤ d
    linarith
-- Resulting proof term is:
--   add_le_add (mul_le_mul_of_nonneg_left ?_ (Even.pow_nonneg (even_two_mul 1) x)) ?_
-- where `add_le_add` and `mul_le_mul_of_nonneg_left` are generalized congruence lemmas
-- and the side goal `0 ≤ x ^ 2` is discharged by `gcongr_discharger`.

example {a b c d x : ℝ} (h : a + c + 1 ≤ b + d + 1) :
    x ^ 2 * (a + c) + 5 ≤ x ^ 2 * (b + d) + 5 := by
  -- Using a pattern to limit the depth.
  gcongr x ^ 2 * ?_ + 5 -- or `gcongr 2`
  -- New goal: ⊢ a + c ≤ b + d
  linarith

-- Descending into binders (here: ⨆).
example {f g : ℕ → ℝ≥0∞} (h : ∀ n, f n ≤ g n) : ⨆ n, f n ≤ ⨆ n, g n := by
  gcongr with i
  exact h i

Tags:
Defined in module:: Mathlib.Tactic.GCongr.Core

rel

rel [h₁, ..., hₙ] uses "generalized congruence" rules to solve a goal of form ⊢ R (f a₁ ... aₙ) (f b₁ ... bₙ) by substituting with the terms hᵢ : Rᵢ aᵢ bᵢ. The relations R, Rᵢ can be any two-argument relation, including · → ·.

This tactic is extensible: to add a "generalized congruence" rule, tag a theorem with the attribute @[gcongr].

If a "generalized congruence" lemma has a side goal, rel will try to discharge it using gcongr_discharger, which is an extensible tactic based on positivity. If side goals cannot be discharged, or the terms h₁, ..., hₙ cannot solve the goals, the tactic fails.

Examples:

example {a b x c d : ℝ} (h1 : a ≤ b) (h2 : c ≤ d) :
    x ^ 2 * a + c ≤ x ^ 2 * b + d := by
  rel [h1, h2]
-- In this example we "substitute" the hypotheses `a ≤ b` and `c ≤ d` into the LHS `x ^ 2 * a + c`
-- of the goal and obtain the RHS `x ^ 2 * b + d`, thus proving the goal.
-- This constructs the proof term:
--   add_le_add (mul_le_mul_of_nonneg_left h1 (pow_bit0_nonneg x 1)) h2
-- using the generalized congruence lemmas `add_le_add` and `mul_le_mul_of_nonneg_left`.

Tags:
Defined in module:: Mathlib.Tactic.GCongr.Core

erw?

erw? [r, ...] calls erw [r, ...] (at hypothesis h if written erw [r, ...] at h), and then attempts to identify any subexpression which would block the use of rw instead. It does so by identifying subexpressions which are defeq, but not at reducible transparency.

Tags:
Defined in module:: Mathlib.Tactic.ErwQuestion

mfld_set_tac

A very basic tactic to show that sets showing up in manifolds coincide or are included in one another.

Tags:
Defined in module:: Mathlib.Logic.Equiv.PartialEquiv

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 := by
  intro x x' h
  apply_fun g at h
  exact H h

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.

Tags:
Defined in module:: Mathlib.Tactic.ApplyFun

use_finite_instance

Try using Set.toFinite to dispatch a Set.Finite goal.

Tags:
Defined in module:: Mathlib.LinearAlgebra.Dual.Basis

fun_prop

fun_prop solves a goal of the form P f, where P is a predicate and f is a function, by decomposing f into a composition of elementary functions, and proving P on each of those by matching against a set of @[fun_prop] lemmas.

If fun_prop fails to solve a goal with the error "No theorems found", you can solve this issue by importing or adding new theorems tagged with the @[fun_prop] attribute. See the module documentation for Mathlib/Tactic/FunProp.lean for a detailed explanation.

fun_prop (disch := tac) uses tac to solve potential side goals. Setting this option is required to solve ContinuousAt/On/Within goals.
fun_prop [c, ...] will unfold the constant(s) c, ... before decomposing f.
fun_prop (config := cfg) sets advanced configuration options using cfg : FunProp.Config (see FunProp.Config for details). These options can be combined: fun_prop (config := cfg) (disch := tac) [c]

Examples:

example : Continuous (fun x : ℝ ↦ x * sin x) := by fun_prop

-- Specify a discharger to solve `ContinuousAt`/`Within`/`On` goals:
example (y : ℝ) (hy : y ≠ 0) : ContinuousAt (fun x : ℝ ↦ 1/x) y := by
  fun_prop (disch := assumption)

example (y : ℝ) (hy : y ≠ 0) : ContinuousAt (fun x => x * (Real.log x) ^ 2 - Real.exp x / x) y := by
  fun_prop (disch := aesop)

Tags:
Defined in module:: Mathlib.Tactic.FunProp.Elab

contrapose

contrapose transforms the main goal into its contrapositive. If the goal has the form ⊢ P → Q, then contrapose turns it into ⊢ ¬ Q → ¬ P. If the goal has the form ⊢ P ↔ Q, then contrapose turns it into ⊢ ¬ P ↔ ¬ Q.

contrapose h on a goal of the form h : P ⊢ Q turns the goal into h : ¬ Q ⊢ ¬ P. This is equivalent to revert h; contrapose; intro h.
contrapose h with new_h uses the name new_h for the introduced hypothesis. This is equivalent to revert h; contrapose; intro new_h.
contrapose!, contrapose! h and contrapose! h with new_h push negation deeper into the goal after contraposing (but before introducing the new hypothesis). See the push Not tactic for more details on the pushing algorithm.
contrapose! (config := cfg) controls the options for negation pushing. All options for Mathlib.Tactic.Push.Config are supported:
- contrapose! +distrib rewrites ¬ (p ∧ q) into ¬ p ∨ ¬ q instead of p → ¬ q.

Examples:

variables (P Q R : Prop)

example (H : ¬ Q → ¬ P) : P → Q := by
  contrapose
  exact H

example (H : ¬ P ↔ ¬ Q) : P ↔ Q := by
  contrapose
  exact H

example (H : ¬ Q → ¬ P) (h : P) : Q := by
  contrapose h
  exact H h

example (H : ¬ R → P → ¬ Q) : (P ∧ Q) → R := by
  contrapose!
  exact H

example (H : ¬ R → ¬ P ∨ ¬ Q) : (P ∧ Q) → R := by
  contrapose! +distrib
  exact H

Tags:
Defined in module:: Mathlib.Tactic.Contrapose

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.

Like intro, the choose tactic supports type annotations to specify the expected type of the introduced variables. This is useful for documentation and for catching mistakes early:

example (h : ∃ n : ℕ, n > 0) : True := by
  choose (n : ℕ) (hn : n > 0) using h
  trivial

If the provided type does not match the actual type, an error is raised.

Examples:

example (h : ∀ n m : ℕ, ∃ i j, m = n + i ∨ m + j = n) : True := by
  choose i j h using h
  guard_hyp i : ℕ → ℕ → ℕ
  guard_hyp j : ℕ → ℕ → ℕ
  guard_hyp h : ∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n
  trivial

example (h : ∀ i : ℕ, i < 7 → ∃ j, i < j ∧ j < i+i) : True := by
  choose! f h h' using h
  guard_hyp f : ℕ → ℕ
  guard_hyp h : ∀ (i : ℕ), i < 7 → i < f i
  guard_hyp h' : ∀ (i : ℕ), i < 7 → f i < i + i
  trivial

Tags:
Defined in module:: Mathlib.Tactic.Choose

success_if_fail_with_msg

success_if_fail_with_msg msg tacs runs tacs and succeeds only if they fail with the message msg.

msg can be any term that evaluates to an explicit String.

Tags:
Defined in module:: Mathlib.Tactic.SuccessIfFailWithMsg

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

Tags:
Defined in module:: Mathlib.Order.Bounds.Basic

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.

Tags:
Defined in module:: Mathlib.Data.Nat.Bitwise

move_oper

move_oper op [a] repeatedly moves a to the far right hand side in applications of op. Here the constant op refers to a binary associative commutative operation, and a is any term (potentially with underscores).

If a contains underscores, they are filled in by unification with the first matching occurrence. Subterms with different values for the underscores are not matched, unless you repeat a.

Currently, move_oper supports the operators HAdd.hAdd (· + ·), HMul.hMul (· * ·), And (· ∧ ·), Or (· ∨ ·), Max.max and Min.min. To support more operations, add them to Mathlib.MoveAdd.moveOperSimpCtx.

move_add [...] uses addition as the operation: it abbreviates move_oper HAdd.add [...].
move_mul [...] uses multiplication as the operation: it abbreviates move_oper HMul.mul [...].
move_oper op [← a] moves the atoms matching a to the far left hand side instead of the right.
move_oper op [a, b, ← c, ← d, ...] moves multiple atoms simultaneously, in the order indicated by the arguments: c will appear to the left of d and a will appear to the left of b.

Tags:
Defined in module:: Mathlib.Tactic.MoveAdd

linear_combination'

linear_combination' attempts to simplify the target by creating a linear combination of a list of equalities and subtracting it from the target. The tactic will create a linear combination by adding the equalities together from left to right, so the order of the input hypotheses does matter. If the norm field of the tactic is set to skip, then the tactic will simply set the user up to prove their target using the linear combination instead of normalizing the subtraction.

Note: There is also a similar tactic linear_combination (no prime); this version is provided for backward compatibility. Compared to this tactic, linear_combination:

drops the ← syntax for reversing an equation, instead offering this operation using the - syntax
does not support multiplication of two hypotheses (h1 * h2), division by a hypothesis (3 / h), or inversion of a hypothesis (h⁻¹)
produces noisy output when the user adds or subtracts a constant to a hypothesis (h + 3)

Note: The left and right sides of all the equalities should have the same type, and the coefficients should also have this type. There must be instances of Mul and AddGroup for this type.

The input e in linear_combination' e is a linear combination of proofs of equalities, given as a sum/difference of coefficients multiplied by expressions. The coefficients may be arbitrary expressions. The expressions can be arbitrary proof terms proving equalities. Most commonly they are hypothesis names h1, h2, ....
linear_combination' (norm := tac) e runs the "normalization tactic" tac on the subgoal(s) after constructing the linear combination.
- The default normalization tactic is ring1, which closes the goal or fails.
- To get a subgoal in the case that it is not immediately provable, use ring_nf as the normalization tactic.
- To avoid normalization entirely, use skip as the normalization tactic.
linear_combination' (exp := n) e will take the goal to the nth power before subtracting the combination e. In other words, if the goal is t1 = t2, linear_combination' (exp := n) e will change the goal to (t1 - t2)^n = 0 before proceeding as above. This feature is not supported for linear_combination2.
linear_combination2 e is the same as linear_combination' e but it produces two subgoals instead of one: rather than proving that (a - b) - (a' - b') = 0 where a' = b' is the linear combination from e and a = b is the goal, it instead attempts to prove a = a' and b = b'. Because it does not use subtraction, this form is applicable also to semirings.
- Note that a goal which is provable by linear_combination' e may not be provable by linear_combination2 e; in general you may need to add a coefficient to e to make both sides match, as in linear_combination2 e + c.
- You can also reverse equalities using ← h, so for example if h₁ : a = b then 2 * (← h) is a proof of 2 * b = 2 * a.

Example Usage:

example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) : x*y = -2*y + 1 := by
  linear_combination' 1*h1 - 2*h2

example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) : x*y = -2*y + 1 := by
  linear_combination' h1 - 2*h2

example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) : x*y = -2*y + 1 := by
  linear_combination' (norm := ring_nf) -2*h2
  /- Goal: x * y + x * 2 - 1 = 0 -/

example (x y z : ℝ) (ha : x + 2*y - z = 4) (hb : 2*x + y + z = -2)
    (hc : x + 2*y + z = 2) :
    -3*x - 3*y - 4*z = 2 := by
  linear_combination' ha - hb - 2*hc

example (x y : ℚ) (h1 : x + y = 3) (h2 : 3*x = 7) :
    x*x*y + y*x*y + 6*x = 3*x*y + 14 := by
  linear_combination' x*y*h1 + 2*h2

example (x y : ℤ) (h1 : x = -3) (h2 : y = 10) : 2*x = -6 := by
  linear_combination' (norm := skip) 2*h1
  simp

axiom qc : ℚ
axiom hqc : qc = 2*qc

example (a b : ℚ) (h : ∀ p q : ℚ, p = q) : 3*a + qc = 3*b + 2*qc := by
  linear_combination' 3 * h a b + hqc

Tags:
Defined in module:: Mathlib.Tactic.LinearCombination'

calc?

Create a calc proof.

Tags:
Defined in module:: Mathlib.Tactic.Widget.Calc

mod_cases

mod_cases h : e % n, where n is a positive numeral and e is an expression of type ℕ or ℤ, performs a case disjunction on the value of e modulo n. If e : ℤ, the goal is split into n subgoals containing the new hypotheses h : e ≡ 0 [ZMOD n], ..., h : e ≡ n-1 [ZMOD n] respectively. If e : ℕ instead, then the hypotheses contain [MOD n] instead of [ZMOD n].

mod_cases e % n, with h omitted, gives the default name H to the new hypotheses.

Tags:
Defined in module:: Mathlib.Tactic.ModCases

positivity

positivity solves goals of the form 0 ≤ x, 0 < x and x ≠ 0. The tactic works recursively according to the syntax of the expression x, by attempting to prove subexpressions are positive/nonnegative/nonzero and combining this into a final proof. This tactic either closes the goal or fails.

For each subexpression e, positivity will try to:

try @[positivity]-tagged extensions to recursively prove e is positive/nonnegative/nonzero based on its subexpressions (see the positivity attribute for more details), or
try the norm_num tactic to prove e is positive/nonnegative/nonzero, or
try showing e : t is nonnegative because there is a CanonicallyOrderedAdd t instance, or
use a local hypothesis of the form 0 ≤ e, 0 < e or e ≠ 0.

This tactic is extensible. See the positivity attribute documentation for more details.

positivity [t₁, …, tₙ] first executes have := t₁; …; have := tₙ in the current goal, then runs positivity. This is useful when positivity needs derived premises such as 0 < y for division/reciprocal, or 0 ≤ x for real powers.

Examples:

example {a : ℤ} (ha : 3 < a) : 0 ≤ a ^ 3 + a := by positivity

example {a : ℤ} (ha : 1 < a) : 0 < |(3:ℤ) + a| := by positivity

example {b : ℤ} : 0 ≤ max (-3) (b ^ 2) := by positivity

example {a b c d : ℝ} (hab : 0 < a * b) (hb : 0 ≤ b) (hcd : c < d) :
    0 < a ^ c + 1 / (d - c) := by
  positivity [sub_pos_of_lt hcd, pos_of_mul_pos_left hab hb]

Tags:
Defined in module:: Mathlib.Tactic.Positivity.Core

congrm

congrm e is a tactic for proving goals of the form lhs = rhs, lhs ↔ rhs, lhs ≍ rhs, or R lhs rhs when R is a reflexive relation. The expression e is a pattern containing placeholders ?_, and this pattern is matched against lhs and rhs simultaneously. These placeholders generate new goals that state that corresponding subexpressions in lhs and rhs are equal. If the placeholders have names, such as ?m, then the new goals are given tags with those names.

Examples:

example {a b c d : ℕ} :
    Nat.pred a.succ * (d + (c + a.pred)) = Nat.pred b.succ * (b + (c + d.pred)) := by
  congrm Nat.pred (Nat.succ ?h1) * (?h2 + ?h3)
  /-  Goals left:
  case h1 ⊢ a = b
  case h2 ⊢ d = b
  case h3 ⊢ c + a.pred = c + d.pred
  -/
  sorry
  sorry
  sorry

example {a b : ℕ} (h : a = b) : (fun y : ℕ => ∀ z, a + a = z) = (fun x => ∀ z, b + a = z) := by
  congrm fun x => ∀ w, ?_ + a = w
  -- ⊢ a = b
  exact h

The congrm command is a convenient frontend to congr(...) congruence quotations. If the goal is an equality, congrm e is equivalent to refine congr(e') where e' is built from e by replacing each placeholder ?m by $(?m). The pattern e is allowed to contain $(...) expressions to immediately substitute equality proofs into the congruence, just like for congruence quotations.

Tags:
Defined in module:: Mathlib.Tactic.CongrM

unfold?

Replace the selected expression with a definitional unfolding.

After each unfolding, we apply whnfCore to simplify the expression.
Explicit natural number expressions are evaluated.
Unfolds of class projections of instances marked with @[default_instance] are not shown. This is relevant for notational type classes like +: we don't want to suggest Add.add a b as an unfolding of a + b. Similarly for OfNat n : Nat which unfolds into n : Nat.

To use unfold?, shift-click an expression in the tactic state. This gives a list of rewrite suggestions for the selected expression. Click on a suggestion to replace unfold? by a tactic that performs this rewrite.

Tags:
Defined in module:: Mathlib.Tactic.Widget.InteractiveUnfold

subst_hom_lift

subst_hom_lift p f φ tries to substitute f with p(φ) by using p.IsHomLift f φ

Tags:
Defined in module:: Mathlib.CategoryTheory.FiberedCategory.HomLift

inhabit

inhabit α tries to derive a Nonempty α instance and then uses it to make an Inhabited α instance. If the target is a Prop, this is done constructively. Otherwise, it uses Classical.choice.

Tags:
Defined in module:: Mathlib.Tactic.Inhabit

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

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence

constructorm

constructorm p_1, ..., p_n, where the main goal has type type, applies the first matching constructor for type, if type matches one of the given patterns. If type does not match any of the patterns, constructorm fails.

constructorm* p_1, ..., p_n repeatedly applies a constructor until the goal no longer matches p_1, ..., p_n. This is a more efficient and compact version of · repeat constructorm p_1, ..., p_n. It is more efficient because the pattern is compiled once.

Examples:

example : True ∧ (True ∨ True) := by
  constructorm* _ ∨ _, _ ∧ _, True

Tags:
Defined in module:: Mathlib.Tactic.CasesM

casesm

casesm p searches for the first hypothesis h : type where type matches the term p, and splits the main goal by cases on h. Use holes in p to indicate arbitrary subexpressions, for example casesm _ ∧ _ will match any conjunction. casesm p fails if no hypothesis type matches p.

casesm p_1, ..., p_n searches for a hypothesis h : type where type matches one or more of the given patterns p_1, ... p_n, and splits the main goal by cases on h.
casesm* p repeatedly performs case splits until no more hypothesis type matches p. This is a more efficient and compact version of · repeat casesm p. It is more efficient because the pattern is compiled once.
casesm! p and casesm!* p skip a hypothesis if the main goal would be replaced with two or more subgoals.

Example:

example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
  -- The following tactic destructs all conjunctions and disjunctions in the current context.
  casesm* _∨_, _∧_
  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
  · clear ‹c› ‹d› ‹e› ‹f›; trivial

Tags:
Defined in module:: Mathlib.Tactic.CasesM

cases_type

cases_type I searches for a hypothesis h : type where I has the form (I ...), and splits the main goal by cases on h. cases_type p fails if no hypothesis type has the identifier I as its head symbol.

cases_type I_1 ... I_n searches for a hypothesis h : type where type has one or more of I_1, ..., I_n as its head symbol, and splits the main goal by cases on h.
cases_type* I repeatedly performs case splits until no more hypothesis type has I as its head symbol. This shorthand for · repeat cases_type I.
cases_type! p and cases_type!* p skip a hypothesis if the main goal would be replaced with two or more subgoals.

Example:

example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
  -- The following tactic destructs all conjunctions and disjunctions in the current context.
  cases_type* Or And
  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
  · clear ‹c› ‹d› ‹e› ‹f›; trivial

Tags:
Defined in module:: Mathlib.Tactic.CasesM

polyrith

The polyrith tactic is no longer supported in Mathlib, because it relied on a defunct external service.

Attempts to prove polynomial equality goals through polynomial arithmetic on the hypotheses (and additional proof terms if the user specifies them). It proves the goal by generating an appropriate call to the tactic linear_combination. If this call succeeds, the call to linear_combination is suggested to the user.

polyrith will use all relevant hypotheses in the local context.
polyrith [t1, t2, t3] will add proof terms t1, t2, t3 to the local context.
polyrith only [h1, h2, h3, t1, t2, t3] will use only local hypotheses h1, h2, h3, and proofs t1, t2, t3. It will ignore the rest of the local context.

Notes:

This tactic only works with a working internet connection, since it calls Sage using the SageCell web API at https://sagecell.sagemath.org/. Many thanks to the Sage team and organization for allowing this use.
This tactic assumes that the user has curl available on path.

Tags:
Defined in module:: Mathlib.Tactic.Polyrith

field_simp_discharge

Default discharge strategy for field and field_simp: try to solve the (in)equality prop, of the form t = 0 or t > 0, by one of the following strategies:

Use an assumption from the context.
Use the norm_num tactic.
Use the positivity tactic.
Use the simp tactic with discharge as discharger and lemmas stating:
- 2 ≠ 0, 3 ≠ 0, 4 ≠ 0
- x ≠ 0 → y ≠ 0 → x * y ≠ 0
- a ≠ 0 → a ^ n ≠ 0 (for n : ℕ and n : ℤ)
- ↑n + 1 ≠ 0, if n : ℕ and the field has characteristic 0.

If none of the strategies finds a proof for prop, the result is none.

Tags:
Defined in module:: Mathlib.Tactic.FieldSimp.Discharger

itauto

itauto solves the main goal when it is a tautology of intuitionistic propositional logic. Unlike grind and tauto! this tactic never uses the law of excluded middle (without the ! option), and the proof search is tailored for this use case. itauto is complete for intuitionistic propositional logic: it will solve any goal that is provable in this logic.

itauto [a, b] will additionally attempt case analysis on a and b assuming that it can derive Decidable a and Decidable b.
itauto * will case on all decidable propositions that it can find among the atomic propositions.
itauto! will work as a classical SAT solver, but the algorithm is not very good in this situation.
itauto! * will case on all propositional atoms. Warning: This can blow up the proof search, so it should be used sparingly.

Example:

example (p : Prop) : ¬ (p ↔ ¬ p) := by itauto

Tags:
Defined in module:: Mathlib.Tactic.ITauto

repeat1

repeat1 tac applies tac to main goal at least once. If the application succeeds, the tactic is applied recursively to the generated subgoals until it eventually fails.

Tags:
Defined in module:: Mathlib.Tactic.Core

compute_degree

compute_degree is a tactic to solve goals of the form

natDegree f = d,
degree f = d,
natDegree f ≤ d (or <),
degree f ≤ d (or <),
coeff f d = r, if d is the degree of f.

The tactic may leave goals of the form d' = d, 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.

Tags:
Defined in module:: Mathlib.Tactic.ComputeDegree

monicity

monicity tries to solve a goal of the form Monic f. It converts the goal into a goal of the form natDegree f ≤ n and one of the form f.coeff n = 1 and calls compute_degree on those two goals.

The variant monicity! starts like monicity, but calls compute_degree! on the two side-goals.

Tags:
Defined in module:: Mathlib.Tactic.ComputeDegree

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:

seeing if rfl works
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
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)

Tags:
Defined in module:: Mathlib.Order.Defs.LinearOrder

linear_combination

The linear_combination tactic attempts to prove an (in)equality goal by exhibiting it as a specified linear combination of (in)equality hypotheses, or other (in)equality proof terms, modulo (A) moving terms between the LHS and RHS of the (in)equalities, and (B) a normalization tactic which by default is ring-normalization.

Example usage:

example {a b : ℚ} (h1 : a = 1) (h2 : b = 3) : (a + b) / 2 = 2 := by
  linear_combination (h1 + h2) / 2

example {a b : ℚ} (h1 : a ≤ 1) (h2 : b ≤ 3) : (a + b) / 2 ≤ 2 := by
  linear_combination (h1 + h2) / 2

example {a b : ℚ} : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
  linear_combination sq_nonneg (a - b)

example {x y z w : ℤ} (h₁ : x * z = y ^ 2) (h₂ : y * w = z ^ 2) :
    z * (x * w - y * z) = 0 := by
  linear_combination w * h₁ + y * h₂

example {x : ℚ} (h : x ≥ 5) : x ^ 2 > 2 * x + 11 := by
  linear_combination (x + 3) * h

example {R : Type*} [CommRing R] {a b : R} (h : a = b) : a ^ 2 = b ^ 2 := by
  linear_combination (a + b) * h

example {A : Type*} [AddCommGroup A]
    {x y z : A} (h1 : x + y = 10 • z) (h2 : x - y = 6 • z) :
    2 • x = 2 • (8 • z) := by
  linear_combination (norm := abel) h1 + h2

example (x y : ℤ) (h1 : x * y + 2 * x = 1) (h2 : x = y) :
    x * y = -2 * y + 1 := by
  linear_combination (norm := ring_nf) -2 * h2
  -- leaves goal `⊢ x * y + x * 2 - 1 = 0`

The input e in linear_combination e is a linear combination of proofs of (in)equalities, given as a sum/difference of coefficients multiplied by expressions. The coefficients may be arbitrary expressions (with nonnegativity constraints in the case of inequalities). The expressions can be arbitrary proof terms proving (in)equalities; most commonly they are hypothesis names h1, h2, ....

The left and right sides of all the (in)equalities should have the same type α, and the coefficients should also have type α. For full functionality α should be a commutative ring -- strictly speaking, a commutative semiring with "cancellative" addition (in the semiring case, negation and subtraction will be handled "formally" as if operating in the enveloping ring). If a nonstandard normalization is used (for example abel or skip), the tactic will work over types α with less algebraic structure: for equalities, the minimum is instances of [Add α] [IsRightCancelAdd α] together with instances of whatever operations are used in the tactic call.

The variant linear_combination (norm := tac) e specifies explicitly the "normalization tactic" tac to be run on the subgoal(s) after constructing the linear combination.

The default normalization tactic is ring1 (for equalities) or Mathlib.Tactic.Ring.prove{LE,LT} (for inequalities). These are finishing tactics: they close the goal or fail.
When working in algebraic categories other than commutative rings -- for example fields, abelian groups, modules -- it is sometimes useful to use normalization tactics adapted to those categories (field_simp, abel, module).
To skip normalization entirely, use skip as the normalization tactic.
The linear_combination tactic creates a linear combination by adding the provided (in)equalities together from left to right, so if tac is not invariant under commutation of additive expressions, then the order of the input hypotheses can matter.

The variant linear_combination (exp := n) e will take the goal to the nth power before subtracting the combination e. In other words, if the goal is t1 = t2, linear_combination (exp := n) e will change the goal to (t1 - t2)^n = 0 before proceeding as above. This variant is implemented only for linear combinations of equalities (i.e., not for inequalities).

Tags:
Defined in module:: Mathlib.Tactic.LinearCombination

says

If you write X says, where X is a tactic that produces a "Try this: Y" message, then you will get a message "Try this: X says Y". Once you've clicked to replace X says with X says Y, afterwards X says Y will only run Y.

The typical usage case is:

simp? [X] says simp only [X, Y, Z]

If you use set_option says.verify true (set automatically during CI) then X says Y runs X and verifies that it still prints "Try this: Y".

Tags:
Defined in module:: Mathlib.Tactic.Says

slice_lhs

slice_lhs a b => tac zooms to the left-hand side, uses associativity for categorical composition as needed, zooms in on the a-th through b-th morphisms, and invokes tac.

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.Slice

slice_rhs

slice_rhs a b => tac zooms to the right-hand side, uses associativity for categorical composition as needed, zooms in on the a-th through b-th morphisms, and invokes tac.

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.Slice

zify

The zify tactic is used to shift propositions from Nat to Int. This is often useful since Int has well-behaved subtraction.

example (a b c x y z : Nat) (h : ¬ x*y*z < 0) : c < a + 3*b := by
  zify
  zify at h
  /-
  h : ¬↑x * ↑y * ↑z < 0
  ⊢ ↑c < ↑a + 3 * ↑b
  -/

zify can be given extra lemmas to use in simplification. This is especially useful in the presence of nat subtraction: passing ≤ arguments will allow push_cast to do more work.

example (a b c : Nat) (h : a - b < c) (hab : b ≤ a) : false := by
  zify [hab] at h
  /- h : ↑a - ↑b < ↑c -/

zify makes use of the @[zify_simps] attribute to move propositions, and the push_cast tactic to simplify the Int-valued expressions. zify is in some sense dual to the lift tactic. lift (z : Int) to Nat will change the type of an integer z (in the supertype) to Nat (the subtype), given a proof that z ≥ 0; propositions concerning z will still be over Int. zify changes propositions about Nat (the subtype) to propositions about Int (the supertype), without changing the type of any variable.

Tags:
Defined in module:: Mathlib.Tactic.Zify

ghost_fun_tac

An auxiliary tactic for proving that ghostFun respects the ring operations.

Tags:
Defined in module:: Mathlib.RingTheory.WittVector.Basic

map_fun_tac

Auxiliary tactic for showing that mapFun respects the ring operations.

Tags:
Defined in module:: Mathlib.RingTheory.WittVector.Basic

tfae_have

tfae_have i → j := t, where the goal is TFAE [P₁, P₂, ...] introduces a hypothesis tfae_i_to_j : Pᵢ → Pⱼ and proof t to the local context. Note that i and j are natural number literals (beginning at 1) used as indices to specify the propositions P₁, P₂, ... that appear in the goal.

Once sufficient hypotheses have been introduced by tfae_have, tfae_finish can be used to close the goal.

All features of have are supported by tfae_have, including naming, matching, destructuring, and goal creation.

tfae_have i ← j := t adds a hypothesis in the reverse direction, of type Pⱼ → Pᵢ.
tfae_have i ↔ j := t adds a hypothesis in the both directions, of type Pᵢ ↔ Pⱼ.
tfae_have hij : i → j := t names the introduced hypothesis hij instead of tfae_i_to_j.
tfae_have i j | p₁ => t₁ | ... matches on the assumption p : Pᵢ.
tfae_have ⟨hij, hji⟩ : i ↔ j := t destructures the bi-implication into hij : Pᵢ → Pⱼ and hji : Pⱼ → Pⱼ.
tfae_have i → j := t ?a creates a new goal for ?a.

Examples:

example (h : P → R) : TFAE [P, Q, R] := by
  tfae_have 1 → 3 := h
  -- The resulting context now includes `tfae_1_to_3 : P → R`.
  sorry

-- An example of `tfae_have` and `tfae_finish`:
example : TFAE [P, Q, R] := by
  tfae_have 1 → 2 := sorry /- proof of P → Q -/
  tfae_have 2 → 1 := sorry /- proof of Q → P -/
  tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/
  tfae_finish

-- All features of `have` are supported by `tfae_have`:
example : TFAE [P, Q] := by
  -- assert `tfae_1_to_2 : P → Q`:
  tfae_have 1 → 2 := sorry

  -- assert `hpq : P → Q`:
  tfae_have hpq : 1 → 2 := sorry

  -- match on `p : P` and prove `Q` via `f p`:
  tfae_have 1 → 2
  | p => f p

  -- assert `pq : P → Q`, `qp : Q → P`:
  tfae_have ⟨pq, qp⟩ : 1 ↔ 2 := sorry

  -- assert `h : P → Q`; `?a` is a new goal:
  tfae_have h : 1 → 2 := f ?a

  sorry

Tags:
Defined in module:: Mathlib.Tactic.TFAE

tfae_finish

tfae_finish closes goals of the form TFAE [P₁, P₂, ...] once a sufficient collection of hypotheses of the form Pᵢ → Pⱼ or Pᵢ ↔ Pⱼ have been introduced to the local context.

tfae_have can be used to conveniently introduce these hypotheses; see tfae_have.

Example:

example : TFAE [P, Q, R] := by
  tfae_have 1 → 2 := sorry /- proof of P → Q -/
  tfae_have 2 → 1 := sorry /- proof of Q → P -/
  tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/
  tfae_finish

Tags:
Defined in module:: Mathlib.Tactic.TFAE

split_ifs

Splits all if-then-else-expressions into multiple goals. Given a goal of the form g (if p then x else y), split_ifs will produce two goals: p ⊢ g x and ¬p ⊢ g y. If there are multiple ite-expressions, then split_ifs will split them all, starting with a top-most one whose condition does not contain another ite-expression. split_ifs at * splits all ite-expressions in all hypotheses as well as the goal. split_ifs with h₁ h₂ h₃ overrides the default names for the hypotheses.

Tags:
Defined in module:: Mathlib.Tactic.SplitIfs

trace

Evaluates a term to a string (when possible), and prints it as a trace message.

Tags:
Defined in module:: Mathlib.Tactic.Trace

hint

The hint tactic tries every tactic registered using register_hint <prio> tac, and reports any that succeed.

Tags:
Defined in module:: Mathlib.Tactic.Hint

cfc_tac

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

Tags:
Defined in module:: Mathlib.Tactic.ContinuousFunctionalCalculus

cfc_cont_tac

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

Tags:
Defined in module:: Mathlib.Tactic.ContinuousFunctionalCalculus

cfc_zero_tac

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

Tags:
Defined in module:: Mathlib.Tactic.ContinuousFunctionalCalculus

rw_search

rw_search has been removed from Mathlib.

Tags:
Defined in module:: Mathlib.Tactic.RewriteSearch

continuity

continuity solves goals of the form Continuous f by applying lemmas tagged with the attribute @[continuity]. If the goal is not solved after attempting all rules, continuity fails.

fun_prop is a (usually more powerful) alternative to continuity.

This tactic is extensible. Tagging lemmas with the @[continuity] attribute can allow continuity to solve more goals.

continuity? reports the proof script found by continuity.

Tags:
Defined in module:: Mathlib.Tactic.Continuity

fin_cases

fin_cases h performs case analysis on a hypothesis of the form h : A, where [Fintype A] is available, or h : a ∈ A, where A : Finset X, A : Multiset X or A : List X.

As an example, in

example (f : ℕ → Prop) (p : Fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val := by
  fin_cases p; simp
  all_goals assumption

after fin_cases p; simp, there are three goals, f 0, f 1, and f 2.

Tags:
Defined in module:: Mathlib.Tactic.FinCases

guard_hyp_nums

guard_hyp_nums n succeeds if there are exactly n hypotheses and fails otherwise.

Note that, depending on what options are set, some hypotheses in the local context might not be printed in the goal view. This tactic computes the total number of hypotheses, not the number of visible hypotheses.

Tags:
Defined in module:: Mathlib.Tactic.GuardHypNums

generalize'

Backwards compatibility shim for generalize.

Tags:
Defined in module:: Mathlib.Tactic.Generalize

order

A finishing tactic for solving goals in arbitrary Preorder, PartialOrder, or LinearOrder. Supports ⊤, ⊥, and lattice operations.

Tags:
Defined in module:: Mathlib.Tactic.Order

order_core

order_core is the part of the order tactic that tries to find a contradiction.

Tags:
Defined in module:: Mathlib.Tactic.Order

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`

Tags:
Defined in module:: Mathlib.Tactic.Change

clear

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

  clear * - h₁ h₂

Tags:
Defined in module:: Mathlib.Tactic.ClearExcept

rename'

rename' h => hnew renames the hypothesis named h to hnew. To rename several hypothesis, use rename' h₁ => h₁new, h₂ => h₂new. You can use rename' a => b, b => a to swap two variables.

Tags:
Defined in module:: Mathlib.Tactic.Rename

restrict_tac?

restrict_tac? passes along Try this from aesop

Tags:
Defined in module:: Mathlib.Topology.Sheaves.Presheaf

restrict_tac

restrict_tac solves relations among subsets (copied from aesop cat)

Tags:
Defined in module:: Mathlib.Topology.Sheaves.Presheaf

by_cases!

by_cases! h : p runs the by_cases h : p tactic, followed by push Not at h in the second subgoal. For example,

by_cases! h : a < b creates one goal with hypothesis h : a < b and another with h : b ≤ a.
by_cases! h : a ≠ b creates one goal with hypothesis h : a ≠ b and another with h : a = b.

Tags:
Defined in module:: Mathlib.Tactic.ByCases

#count_heartbeats

#count_heartbeats tac counts the heartbeats used by the tactic sequence tac and prints an info line with the number of heartbeats.

#count_heartbeats! n in tac, where n is an optional natural number literal, runs tac n times on the same goal while counting the heartbeats, and prints an info line with range and standard deviation. n can be left out, and defaults to 10.

Example:

example : 1 + 1 = 2 := by
  -- The next line will print an info message of this format; the exact number may vary.
  -- info: 4646
  #count_heartbeats simp

example : 1 + 1 = 2 := by
  -- The next line will print an info message of this format; the exact numbers may vary.
  -- info: Min: 4 Max: 4 StdDev: 2%
  #count_heartbeats! 37 in simp

Tags:
Defined in module:: Mathlib.Util.CountHeartbeats

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.

Tags:
Defined in module:: Mathlib.Tactic.Algebraize

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.

Tags:
Defined in module:: Mathlib.Tactic.Algebraize

uniqueDiffWithinAt_Ici_Iic_univ

An auxiliary tactic closing goals UniqueDiffWithinAt ℝ s a where s ∈ {Iic a, Ici a, univ}.

Tags:
Defined in module:: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

norm_num

norm_num normalizes numerical expressions in the goal. By default, it supports the operations + - * / ⁻¹ ^ and % over types with (at least) an AddMonoidWithOne instance, such as ℕ, ℤ, ℚ, ℝ, ℂ. In addition to evaluating numerical expressions, norm_num will use simp to simplify the goal. If the goal has the form A = B, A ≠ B, A < B or A ≤ B, where A and B are numerical expressions, norm_num will try to close it. It also has a relatively simple primality prover.

This tactic is extensible. Extensions can allow norm_num to evaluate more kinds of expressions, or to prove more kinds of propositions. See the @[norm_num] attribute for further information on extending norm_num.

norm_num at l normalizes at location(s) l.
norm_num [h1, ...] adds the arguments h1, ... to the simp set in addition to the default simp set. All options for simp arguments are supported, in particular ←, ↑ and ↓.
norm_num only does not use the default simp set for simplification. norm_num only [h1, ...] uses only the arguments h1, ... in addition to the routines tagged @[norm_num]. norm_num only still performs post-processing steps, like simp only, use norm_num1 if you exclusively want to normalize numerical expressions.
norm_num (config := cfg) uses cfg as configuration for simp calls (see the simp tactic for further details).

Examples:

example : 43 ≤ 74 + (33 : ℤ) := by norm_num
example : ¬ (7-2)/(2*3) ≥ (1:ℝ) + 2/(3^2) := by norm_num

Tags:
Defined in module:: Mathlib.Tactic.NormNum.Core

norm_num1

norm_num1 normalizes numerical expressions in the goal. It is a basic version of norm_num that does not call simp.

By default, it supports the operations + - * / ⁻¹ ^ and % over types with (at least) an AddMonoidWithOne instance, such as ℕ, ℤ, ℚ, ℝ, ℂ. If the goal has the form A = B, A ≠ B, A < B or A ≤ B, where A and B are numerical expressions, norm_num1 will try to close it. It also has a relatively simple primality prover. :e This tactic is extensible. Extensions can allow norm_num1 to evaluate more kinds of expressions, or to prove more kinds of propositions. See the @[norm_num] attribute for further information on extending norm_num1.

norm_num1 at l normalizes at location(s) l.

Examples:

example : 43 ≤ 74 + (33 : ℤ) := by norm_num1
example : ¬ (7-2)/(2*3) ≥ (1:ℝ) + 2/(3^2) := by norm_num1

Tags:
Defined in module:: Mathlib.Tactic.NormNum.Core

pure_coherence

pure_coherence uses the coherence theorem for monoidal categories to prove the goal. It can prove any equality made up only of associators, unitors, and identities.

example {C : Type} [Category* C] [MonoidalCategory C] :
  (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom := by
  pure_coherence

Users will typically just use the coherence tactic, which can also cope with identities 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

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.Coherence

liftable_prefixes

Internal tactic used in coherence.

Rewrites an equation f = g as f₀ ≫ f₁ = g₀ ≫ g₁, where f₀ and g₀ are maximal prefixes of f and g (possibly after reassociating) which are "liftable" (i.e. expressible as compositions of unitors and associators).

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.Coherence

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

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.Coherence

monoidal_simps

Simp lemmas for rewriting a hom in monoidal categories into a normal form.

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.Coherence

pure_coherence_internal

The same as pure_coherence, but used internally in coherence without the warning.

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.Coherence

congr!

congr! tries to prove the main goal by repeatedly applying congruence rules. For example, on a goal of the form ⊢ f a1 a2 ... = f b1 b2 ..., congr! will make new goals ⊢ a1 = b1, ⊢ a2 = b2, ...

congr! is a more powerful version of the congr tactic that uses congruence lemmas (tagged with @[congr]), reflexivity rules (tagged with @[refl]) and proof discharging strategies. The full list of congruence proof strategies is documented in the module Mathlib.Tactic.CongrExclamation. The congr! tactic is used by the convert and convert_to tactics.

congr! n, where n is a positive numeral, controls the depth with which congruence is applied. For example, if the main goal is n + n + 1 = 2 * n + 1, then congr! 1 results in one goal, ⊢ n + n = 2 * n, and congr! 2 (or more) results in two (impossible) goals ⊢ HAdd.hAdd = HMul.hMul and ⊢ n = 2. By default, the depth is unlimited.
congr! with x ⟨y₁, y₂⟩ (z₁ | z₂) names or pattern-matches the variables introduced by congruence rules, like rintro x ⟨y₁, y₂⟩ (z₁ | z₂) would.
congr! (config := cfg) uses the configuration options in cfg to control the congruence rules (see Congr!.Config).

Tags:
Defined in module:: Mathlib.Tactic.CongrExclamation

aesop_graph?

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

Tags:
Defined in module:: Mathlib.Combinatorics.SimpleGraph.Basic

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.

Tags:
Defined in module:: Mathlib.Combinatorics.SimpleGraph.Basic

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.

Tags:
Defined in module:: Mathlib.Combinatorics.SimpleGraph.Basic

#check'

The #check' t tactic elaborates the term t and then pretty prints it with its type as e : ty. In contrast to #check t, we only pretty-print explicit arguments, and omit implicit or type class arguments. Currently this only works when t is the name of a declaration.

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 other #check commands, the #check' tactic allows stuck typeclass instance problems. These become metavariables in the output.

Tags:
Defined in module:: Mathlib.Tactic.Check

#check

#check t 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.

To display only explicit arguments in the type signature, see #check'.

Tags:
Defined in module:: Mathlib.Tactic.Check

congrm?

Display a widget panel allowing to generate a congrm call with holes specified by selecting subexpressions in the goal.

Tags:
Defined in module:: Mathlib.Tactic.Widget.CongrM

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.

Tags:
Defined in module:: Mathlib.Tactic.DefEqTransformations

eta_struct

eta_struct at loc transforms structure constructor applications such as S.mk x.1 ... x.n (pretty printed as, for example, {a := x.a, b := x.b, ...}) into x. This also exists as a conv-mode tactic.

The transformation is known as eta reduction for structures, and it yields definitionally equal expressions.

For example, given x : α × β, then (x.1, x.2) becomes x after this transformation.

Tags:
Defined in module:: Mathlib.Tactic.DefEqTransformations

eta_expand

eta_expand at loc eta expands all sub-expressions at the given location. It also beta reduces any applications of eta expanded terms, so it puts it into an eta-expanded "normal form." This also exists as a conv-mode tactic.

For example, if f takes two arguments, then f becomes fun x y => f x y and f x becomes fun y => f x y.

This can be useful to turn, for example, a raw HAdd.hAdd into fun x y => x + y.

Tags:
Defined in module:: Mathlib.Tactic.DefEqTransformations

reduce

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

This does the same transformation as the #reduce command.

Tags:
Defined in module:: Mathlib.Tactic.DefEqTransformations

whnf

whnf at loc puts the given location into weak-head normal form. This also exists as a conv-mode tactic.

Weak-head normal form is when the outer-most expression has been fully reduced, the expression may contain subexpressions which have not been reduced.

Tags:
Defined in module:: Mathlib.Tactic.DefEqTransformations

eta_reduce

eta_reduce at loc eta reduces all sub-expressions at the given location. This also exists as a conv-mode tactic.

For example, fun x y => f x y becomes f after eta reduction.

Tags:
Defined in module:: Mathlib.Tactic.DefEqTransformations

unfold_projs

unfold_projs at loc unfolds projections of class instances at the given location. This also exists as a conv-mode tactic.

Tags:
Defined in module:: Mathlib.Tactic.DefEqTransformations

refold_let

refold_let x y z at loc looks for the bodies of local definitions x, y, and z at the given location and replaces them with x, y, or z. This is the inverse of "zeta reduction." This also exists as a conv-mode tactic.

Tags:
Defined in module:: Mathlib.Tactic.DefEqTransformations

monoidal_coherence

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

example {C : Type} [Category* C] [MonoidalCategory C] :
  (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom := by
  monoidal_coherence

Tags:
Defined in module:: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

push_neg

push_neg rewrites the goal by pushing negations deeper into an expression. For instance, the goal ¬ ∀ x, ∃ y, x ≤ y will be transformed by push_neg into ∃ x, ∀ y, y < x. Binder names are preserved (contrary to what would happen with simp using the relevant lemmas). push_neg works as both a tactic and a conv tactic.

push_neg is a special case of the more general push tactic, namely push Not. The push tactic can be extended using the @[push] attribute. push has special-casing built in for push Not.

Tactics that introduce a negation usually have a version that automatically calls push_neg on that negation. These include by_cases!, contrapose! and by_contra!.

push_neg at l1 l2 ... rewrites at the given locations.
push_neg at * rewrites at each hypothesis and the goal.
push_neg +distrib rewrites ¬ (p ∧ q) into ¬ p ∨ ¬ q (by default, the tactic rewrites it into p → ¬ q instead).

Example:

example (h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε) :
    ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀| := by
  push_neg at h
  -- Now we have the hypothesis `h : ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|`
  exact h

Tags:
Defined in module:: Mathlib.Tactic.Push

pull

pull c rewrites the goal by pulling the constant c closer to the head of the expression. For instance, pull _ ∈ _ rewrites x ∈ y ∨ ¬ x ∈ z into x ∈ y ∪ zᶜ. More precisely, the pull tactic repeatedly rewrites an expression by applying lemmas of the form ... (c ...) = c ... (where c can appear 1 or more times on the left hand side). pull is the inverse tactic to push. To extend the pull tactic, you can tag a lemma with the @[push] attribute. pull works as both a tactic and a conv tactic.

A lemma is considered a pull lemma if its reverse direction is a push lemma that actually moves the given constant away from the head. For example

not_or : ¬ (p ∨ q) ↔ ¬ p ∧ ¬ q is a pull lemma, but not_not : ¬ ¬ p ↔ p is not.
log_mul : log (x * y) = log x + log y is a pull lemma, but log_abs : log |x| = log x is not.
Pi.mul_def : f * g = fun (i : ι) => f i * g i and Pi.one_def : 1 = fun (x : ι) => 1 are both pull lemmas for fun, because every push fun _ ↦ _ lemma is also considered a pull lemma.

TODO: define a @[pull] attribute for tagging pull lemmas that are not push lemmas.

pull _ ~ _ pulls the operator or relation ~.
pull c at l1 l2 ... rewrites at the given locations.
pull c at * rewrites at all hypotheses and the goal.
pull (disch := tac) c uses the tactic tac to discharge any hypotheses for @[push] lemmas.

Examples:

pull _ ∈ _ rewrites x ∈ y ∨ ¬ x ∈ z into x ∈ y ∪ zᶜ.
pull (disch := positivity) Real.log rewrites log a + 2 * log b into log (a * b ^ 2).
pull fun _ ↦ _ rewrites f ^ 2 + 5 into fun x => f x ^ 2 + 5 where f is a function.

Tags:
Defined in module:: Mathlib.Tactic.Push

push

push c rewrites the goal by pushing the constant c deeper into an expression. For instance, push _ ∈ _ rewrites x ∈ {y} ∪ zᶜ into x = y ∨ ¬ x ∈ z. More precisely, the push tactic repeatedly rewrites an expression by applying lemmas of the form c ... = ... (c ...) (where c can appear 0 or more times on the right hand side). To extend the push tactic, you can tag a lemma of this form with the @[push] attribute.

To instead move a constant closer to the head of the expression, use the pull tactic.

push works as both a tactic and a conv tactic.

push _ ~ _ pushes the (binary) operator ~, push ~ _ pushes the (unary) operator ~.
push c at l1 l2 ... rewrites at the given locations.
push c at * rewrites at all hypotheses and the goal.
push +distrib Not rewrites ¬ (p ∧ q) into ¬ p ∨ ¬ q (without +distrib, it rewrites it into p → ¬ q instead).
push (disch := tac) c uses the tactic tac to discharge any hypotheses for @[push] lemmas.

Examples:

push Not is the same as push ¬ _, and it rewrites ¬ ∀ ε > 0, ∃ δ > 0, δ < ε into ∃ ε > 0, ∀ δ > 0, ε ≤ δ. Notably, this preserves the binder names.
push _ ∈ _ rewrites x ∈ {y} ∪ zᶜ into x = y ∨ ¬ x ∈ z.
push (disch := positivity) Real.log rewrites log (a * b ^ 2) into log a + 2 * log b.
push fun _ ↦ _ rewrites fun x => f x ^ 2 + 5 into f ^ 2 + 5
push ∀ _, _ rewrites ∀ a, p a ∧ q a into (∀ a, p a) ∧ (∀ a, q a).

Tags:
Defined in module:: Mathlib.Tactic.Push

lift

lift e to t with x lifts the expression e to the type t by introducing a new variable x : t such that ↑x = e, and then replacing occurrences of e with ↑x. lift requires an instance of the class CanLift t' t coe cond, where t' is the type of e, and creates a side goal for the lifting condition, of the form ⊢ cond x, placing this on top of the goal stack.

Given an instance CanLift β γ, lift can also lift α → β to α → γ; more generally, given β : Π a : α, Type*, γ : Π a : α, Type*, and [Π a : α, CanLift (β a) (γ a)], it automatically generates an instance CanLift (Π a, β a) (Π a, γ a).

lift is in some sense dual to the zify tactic. lift (z : ℤ) to ℕ will change the type of an integer z (in the supertype) to ℕ (the subtype), given a proof that z ≥ 0; propositions concerning z will still be over ℤ. zify changes propositions about ℕ (the subtype) to propositions about ℤ (the supertype), without changing the type of any variable.

The norm_cast tactic can be used after lift to normalize introduced casts.

lift e to t using h with x uses the expression h to prove the lifting condition cond e. If h is a variable, lift will try to clear it from the context. If you want to keep h in the context, write lift e to t using h with x rfl h (see below).
If e is a variable, lift e to t is equivalent to lift e to t with e. The original variable e will be cleared from the context.
lift e to t with x hx adds hx : ↑x = e to the context (and if e is a variable, does not clear it).
lift e to t with x hx h adds hx : ↑x = e and h : cond e to the context (and if e is a variable, does not clear it). In particular, lift e to t using h with x hx h, where h is a variable, keeps h in the context.
lift e to t with x rfl h adds h : cond e to the context (and if e is a variable, does not clear it). In particular, lift e to t using h with x rfl h, where h is a variable, keeps h in the context.

Examples:

def P (n : ℤ) : Prop := n = 3

example (n : ℤ) (h : P n) : n = 3 := by
  lift n to ℕ
  /-
  Two goals:
  n : ℤ, h : P n ⊢ n ≥ 0
  n : ℕ, h : P ↑n ⊢ ↑n = 3
  -/
  · unfold P at h; linarith
  · exact h

example (n : ℤ) (hn : n ≥ 0) (h : P n) : n = 3 := by
  lift n to ℕ using hn
  /-
  One goal:
  n : ℕ
  h : P ↑n
  ⊢ ↑n = 3
  -/
  exact h

example (n : ℤ) (hn : n + 3 ≥ 0) (h : P (n + 3)) :
    n + 3 = n * 2 + 3 := by
  lift n + 3 to ℕ using hn with k hk
  /-
  One goal:
  n : ℤ
  k : ℕ
  hk : ↑k = n + 3
  h : P ↑k
  ⊢ ↑k = 2 * n + 3
  -/
  unfold P at h; linarith

Tags:
Defined in module:: Mathlib.Tactic.Lift

mono

mono applies monotonicity rules and local hypotheses repetitively. For example,

example (x y z k : ℤ)
    (h : 3 ≤ (4 : ℤ))
    (h' : z ≤ y) :
    (k + 3 + x) - y ≤ (k + 4 + x) - z := by
  mono

Tags:
Defined in module:: Mathlib.Tactic.Monotonicity.Basic

guard_goal_nums

guard_goal_nums n succeeds if there are exactly n goals and fails otherwise.

Tags:
Defined in module:: Mathlib.Tactic.GuardGoalNums

apply_gmonoid_gnpowRec_succ_tac

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

Tags:
Defined in module:: Mathlib.Algebra.GradedMonoid

apply_gmonoid_gnpowRec_zero_tac

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

Tags:
Defined in module:: Mathlib.Algebra.GradedMonoid

induction'

induction' x applies induction on the variable x of the inductive type t to the main goal, producing one goal for each constructor of t, in which x is replaced by that constructor applied to newly introduced variables. induction' adds an inductive hypothesis for each recursive argument to the constructor. This is a backwards-compatible variant of the induction tactic in Lean 4 core.

Prefer induction when possible, because it promotes structured proofs.

induction' x with n1 n2 ... names the introduced hypotheses: arguments to constructors and inductive hypotheses. This is the main difference with induction in core Lean.
induction' e, where e is an expression instead of a variable, generalizes e in the goal, and then performs induction on the resulting variable.
induction' h : e, where e is an expression instead of a variable, generalizes e in the goal, and then performs induction on the resulting variable, adding to each goal the hypothesis h : e = _ where _ is the constructor instance.
induction' x using r uses r as the principle of induction. Here r should be a term whose result type is of the form C t1 t2 ..., where C is a bound variable and t1, t2, ... (if present) are bound variables.
induction' x generalizing z1 z2 ... generalizes over the local variables z1, z2, ... in the inductive hypothesis.

Example:

open Nat

example (n : ℕ) : 0 < factorial n := by
  induction' n with n ih
  · rw [factorial_zero]
    simp
  · rw [factorial_succ]
    apply mul_pos (succ_pos n) ih

-- Though the following equivalent spellings should be preferred
example (n : ℕ) : 0 < factorial n := by
  induction n
  case zero =>
    rw [factorial_zero]
    simp
  case succ n ih =>
    rw [factorial_succ]
    apply mul_pos (succ_pos n) ih

Tags:
Defined in module:: Mathlib.Tactic.Cases

cases'

cases' x, where the variable x has inductive type t, splits the main goal, producing one goal for each constructor of t, in which x is replaced by that constructor applied to newly introduced variables. This is a backwards-compatible variant of the cases tactic in Lean 4 core.

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

cases' x with n1 n2 ... names the arguments to the constructors. This is the main difference with cases in core Lean.
cases' e, where e is an expression instead of a variable, generalizes e in the goal, and then performs induction on the resulting variable.
cases' h : e, where e is an expression instead of a variable, generalizes e in the goal, and then splits by cases on the resulting variable, adding to each goal the hypothesis h : e = _ where _ is the constructor instance.
cases' x using r uses r as the case matching rule. Here r should be a term whose result type is of the form C t1 t2 ..., where C is a bound variable and t1, t2, ... (if present) are bound variables.

Example:

example (h : p ∨ q) : q ∨ p := by
  cases' h with hp hq
  · exact Or.inr hp
  · exact Or.inl hq

-- Though the following equivalent spellings should be preferred
example (h : p ∨ q) : q ∨ p := by
  cases h with
  | inl hp => exact Or.inr hp
  | inr hq => exact Or.inl hq

example (h : p ∨ q) : q ∨ p := by
  rcases h with hp | hq
  · exact Or.inr hp
  · exact Or.inl hq

Tags:
Defined in module:: Mathlib.Tactic.Cases

simp_rw

simp_rw functions as a mix of simp and rw. Like rw, it applies each rewrite rule in the given order, but like simp it repeatedly applies these rules and also under binders like ∀ x, ..., ∃ x, ... and fun x ↦.... Usage:

simp_rw [lemma_1, ..., lemma_n] will rewrite the goal by applying the lemmas in that order. A lemma preceded by ← is applied in the reverse direction.
simp_rw [lemma_1, ..., lemma_n] at h₁ ... hₙ will rewrite the given hypotheses.
simp_rw [...] at * rewrites in the whole context: all hypotheses and the goal.

Lemmas passed to simp_rw must be expressions that are valid arguments to simp. For example, neither simp nor rw can solve the following, but simp_rw can:

example {a : ℕ}
    (h1 : ∀ a b : ℕ, a - 1 ≤ b ↔ a ≤ b + 1)
    (h2 : ∀ a b : ℕ, a ≤ b ↔ ∀ c, c < a → c < b) :
    (∀ b, a - 1 ≤ b) = ∀ b c : ℕ, c < a → c < b + 1 := by
  simp_rw [h1, h2]

Tags:
Defined in module:: Mathlib.Tactic.SimpRw