Tactics Reference

Robin Milner’s LCF system introduced a radical idea in the 1970s: let users extend the theorem prover with custom proof procedures, but channel all proof construction through a small trusted kernel. You could write arbitrarily clever automation, and if it produced a proof, that proof was guaranteed valid. Tactics are this idea fully realized. They are programs that build proofs, metaprograms that manipulate the proof state, search procedures that explore the space of possible arguments. When you write simp and Lean simplifies your goal through dozens of rewrite steps, you are invoking a sophisticated algorithm. When you write omega and Lean discharges a linear arithmetic obligation, you are running a decision procedure. The proof terms these tactics construct may be enormous, but they are checked by the kernel, and the kernel is small enough to trust. Think of tactics as the code you write, and the kernel as the one colleague who actually reads your pull requests.

The following covers all the major tactics in Lean 4 and Mathlib. Click on any tactic name to jump to its documentation and examples.

abel - Prove equalities in abelian groups
aesop - General automation tactic
all_goals - Apply tactic to all current goals
any_goals - Apply tactic to any applicable goal
apply - Apply hypotheses or lemmas to solve goals
apply_fun - Apply function to both sides of equality
assumption - Use hypothesis matching goal
bound - Prove inequalities from structure
by_cases - Perform case splitting
by_contra - Proof by contradiction
calc - Chain equations and inequalities
cases - Case analysis on inductive types
choose - Extract choice function from forall-exists
congr - Prove equality using congruence rules
constructor - Break down conjunctions, existentials, and iff
contradiction - Find contradictions in hypotheses
conv - Targeted rewriting in specific parts
convert - Prove by showing goal equals type of expression
decide - Run decision procedures
exact - Provide an exact proof term
exfalso - Prove anything from False
ext - Prove equality of functions extensionally
field_simp - Simplify field expressions
fin_cases - Split finite type into cases
first - Try tactics until one succeeds
focus - Limit tactics to first goal
gcongr - Prove inequalities using congruence
generalize - Replace expressions with variables
grind - Proof search using congruence closure
group - Prove equalities in groups
have - Introduce new hypotheses
hint - Get tactic suggestions
induction - Perform inductive proofs
interval_cases - Split bounded values into cases
intro - Introduce assumptions from implications and quantifiers
left - Choose left side of disjunction
lift - Lift variable to higher type
linarith - Prove linear inequalities
linear_combination - Prove from linear combinations
module - Prove equalities in modules
nlinarith - Handle nonlinear inequalities
noncomm_ring - Prove in non-commutative rings
norm_cast - Simplify by moving casts outward
norm_num - Simplify numerical expressions
nth_rw - Rewrite only the nth occurrence
obtain - Destructure existentials and structures
omega - Solve linear arithmetic over Nat and Int
pick_goal - Move specific goal to front
positivity - Prove positivity goals
push_cast - Push casts inward
push_neg - Push negations inward
qify - Shift to rationals
refine - Apply with holes to fill later
rename - Rename hypotheses for clarity
repeat - Apply tactic repeatedly until fails
revert - Move hypotheses back to the goal
rfl - Prove by reflexivity
right - Choose right side of disjunction
ring - Prove equalities in commutative rings
rw - Rewrite using equalities
simp - Apply simplification lemmas
simp_all - Simplify everything including hypotheses
simp_rw - Rewrite with simplification at each step
sorry - Admit goal without proof
specialize - Instantiate hypothesis with specific arguments
split - Handle if-then-else and pattern matching
split_ifs - Case on if-then-else expressions
subst - Substitute variable with its value
swap - Swap first two goals
symm - Swap symmetric relations
tauto - Prove logical tautologies
trans - Split transitive relations
trivial - Prove simple goals automatically
try - Attempt tactic, continue if fails
use - Provide witnesses for existential goals
zify - Shift natural numbers to integers

Logical Connectives

intro

The intro tactic moves hypotheses from the goal into the local context. When your goal is ∀ x, P x or P → Q, using intro names the bound variable or assumption and makes it available for use in the proof.

theorem intro_apply : ∀ x : Nat, x = x → x + 0 = x := by
  intro x h  -- Introduce x and hypothesis h : x = x
  simp       -- Simplify x + 0 = x

constructor

The constructor tactic applies the first constructor of an inductive type to the goal. For And (conjunction), it splits the goal into two subgoals. For Exists, it expects you to provide a witness. For Iff, it creates subgoals for both directions.

theorem constructor_example : True ∧ True := by
  constructor
  · trivial  -- Prove first True
  · trivial  -- Prove second True

left and right

The left and right tactics select which side of a disjunction to prove. When your goal is P ∨ Q, use left to commit to proving P or right to prove Q.

theorem or_example : 5 < 10 ∨ 10 < 5 := by
  left
  simp

use

The use tactic provides a concrete witness for an existential goal. When your goal is ∃ x, P x, using use t substitutes t for x and leaves you to prove P t.

theorem use_example : ∃ x : Nat, x * 2 = 10 := by
  exact ⟨5, rfl⟩

obtain

The obtain tactic extracts components from existential statements and structures in hypotheses. It combines have and pattern matching, letting you name both the witness and the proof simultaneously.

theorem have_example (x : Nat) : x + 0 = x := by
  have h : x + 0 = x := by simp
  exact h

theorem obtain_example (h : ∃ x : Nat, x > 5 ∧ x < 10) : ∃ y, y = 7 := by
  obtain ⟨_x, _hgt, _hlt⟩ := h  -- Destructure the existential
  exact ⟨7, rfl⟩

Applying Lemmas

exact

The exact tactic closes a goal by providing a term whose type matches the goal exactly. It performs no additional unification or elaboration beyond what is necessary.

theorem exact_example (h : 2 + 2 = 4) : 4 = 2 + 2 := by
  exact h.symm

/-- `refine` allows holes with ?_ -/
theorem refine_example : ∃ x : Nat, x > 5 := by
  refine ⟨10, ?_⟩  -- Use 10, but leave proof as a hole
  simp              -- Fill the hole: prove 10 > 5

apply

The apply tactic works backwards from the goal. Given a lemma h : A → B and a goal B, using apply h reduces the goal to proving A. It unifies the conclusion of the lemma with the current goal.

refine

The refine tactic is like exact but allows placeholders written as ?_ that become new goals. This lets you partially specify a proof term while deferring some parts.

theorem exact_example (h : 2 + 2 = 4) : 4 = 2 + 2 := by
  exact h.symm

/-- `refine` allows holes with ?_ -/
theorem refine_example : ∃ x : Nat, x > 5 := by
  refine ⟨10, ?_⟩  -- Use 10, but leave proof as a hole
  simp              -- Fill the hole: prove 10 > 5

convert

The convert tactic applies a term to the goal even when the types do not match exactly, generating side goals for the mismatches. It is useful when you have a lemma that is almost but not quite what you need.

theorem convert_example (x y : Nat) (h : x = y) : Nat.succ x = Nat.succ y := by
  convert rfl using 1
  rw [h]

specialize

The specialize tactic instantiates a universally quantified hypothesis with concrete values, replacing the general statement with a specific instance in your context.

theorem specialize_example (h : ∀ x : Nat, x > 0 → x ≥ 1) : 5 ≥ 1 := by
  specialize h 5 (by simp)
  exact h

Context Manipulation

have

The have tactic introduces a new hypothesis into the context. You state what you want to prove as an intermediate step, prove it, and then it becomes available for the rest of the proof.

theorem have_example (x : Nat) : x + 0 = x := by
  have h : x + 0 = x := by simp
  exact h

theorem obtain_example (h : ∃ x : Nat, x > 5 ∧ x < 10) : ∃ y, y = 7 := by
  obtain ⟨_x, _hgt, _hlt⟩ := h  -- Destructure the existential
  exact ⟨7, rfl⟩

rename

The rename tactic changes the name of a hypothesis in the local context, making proofs more readable when auto-generated names are unclear.

theorem rename_example (h : 1 = 1) : 1 = 1 := by
  exact h

revert

The revert tactic is the inverse of intro. It moves a hypothesis from the context back into the goal as an implication or universal quantifier, which is useful before applying induction or certain lemmas.

theorem revert_example (x : Nat) (h : x = 5) : x = 5 := by
  revert h x
  intro x h
  exact h

generalize

The generalize tactic replaces a specific expression in the goal with a fresh variable, abstracting over that value. This is useful when you need to perform induction on a compound expression.

theorem generalize_example : (2 + 3) * 4 = 20 := by
  simp

Rewriting and Simplifying

rw (rewrite)

The rw tactic replaces occurrences of the left-hand side of an equality with the right-hand side. Use rw [←h] to rewrite in the reverse direction. Multiple rewrites can be chained in a single rw [h1, h2, h3].

theorem rw_example (a b : Nat) (h : a = b) : a + 2 = b + 2 := by
  rw [h]  -- Rewrite a to b using h

theorem simp_example (x : Nat) : x + 0 = x ∧ 0 + x = x := by
  simp  -- Simplifies both sides

Tip

rw rewrites the first occurrence it finds. Use rw [h] at hyp to rewrite in a hypothesis instead of the goal. If rewriting fails due to dependent types or metavariables, try simp_rw which handles these cases more gracefully. Use nth_rw n [h] to target a specific occurrence.

simp

The simp tactic repeatedly applies lemmas marked with @[simp] to simplify the goal. It handles common algebraic identities, list operations, and logical simplifications automatically.

theorem rw_example (a b : Nat) (h : a = b) : a + 2 = b + 2 := by
  rw [h]  -- Rewrite a to b using h

theorem simp_example (x : Nat) : x + 0 = x ∧ 0 + x = x := by
  simp  -- Simplifies both sides

Tip

Use simp only [lemma1, lemma2] for reproducible proofs. Bare simp can break when new simp lemmas are added to the library. Use simp? to see which lemmas were applied, then replace with simp only [...] for stability. In Mathlib code reviews, bare simp at non-terminal positions is discouraged.

simp_all

The simp_all tactic simplifies both the goal and all hypotheses simultaneously, using each simplified hypothesis to help simplify the others.

theorem simp_all_example (x : Nat) (h : x = 0) : x + x = 0 := by
  simp_all

simp_rw

The simp_rw tactic rewrites using the given lemmas but applies simplification at each step, which helps when rewrites would otherwise fail due to associativity or other issues.

theorem simp_rw_example (x y : Nat) : (x + y) + (y + x) = 2 * (x + y) := by
  simp_rw [Nat.add_comm y x]
  ring

nth_rw

The nth_rw tactic rewrites only a specific occurrence of a pattern, counting from 1. This gives precise control when an expression appears multiple times and you only want to change one instance.

theorem nth_rewrite_example (x : Nat) : x + x + x = 3 * x := by
  nth_rw 2 [← Nat.add_zero x]  -- Rewrite only the second occurrence of x
  simp
  ring

norm_num

The norm_num tactic evaluates and simplifies numeric expressions, proving goals like 2 + 2 = 4 or 7 < 10 by computation. It handles arithmetic in various number types.

theorem norm_num_example : 2 ^ 3 + 5 * 7 = 43 := by
  norm_num

norm_cast

The norm_cast tactic normalizes expressions involving type coercions by pushing casts outward and combining them, making goals about mixed numeric types easier to prove.

theorem norm_cast_example (n : Nat) : (n : Int) + 1 = ((n + 1) : Int) := by
  norm_cast

push_cast

The push_cast tactic pushes type coercions inward through operations, distributing a cast over addition, multiplication, and other operations.

set_option linter.unusedTactic false in
theorem push_cast_example (n m : Nat) : ((n + m) : Int) = (n : Int) + (m : Int) := by
  push_cast
  rfl

conv

The conv tactic enters a conversion mode that lets you navigate to specific subexpressions and rewrite only there. It is invaluable when rw affects the wrong occurrence or when you need surgical precision.

theorem conv_example (x y : Nat) : x + y = y + x := by
  conv =>
    lhs  -- Focus on left-hand side
    rw [Nat.add_comm]

Tip

Navigation commands in conv mode: lhs/rhs select sides of an equation, arg n selects the nth argument, ext introduces binders, and enter [1, 2] navigates by path. Use conv_lhs or conv_rhs as shortcuts when you only need to work on one side of an equation.

Reasoning with Relations

rfl (reflexivity)

The rfl tactic proves goals of the form a = a where both sides are definitionally equal. It works even when the equality is not syntactically obvious but follows from definitions.

theorem rfl_example (x : Nat) : x = x := by
  rfl

symm

The symm tactic reverses a symmetric relation like equality. If your goal is a = b and you have h : b = a, using symm on h or the goal makes them match.

theorem symm_example (x y : Nat) (h : x = y) : y = x := by
  symm
  exact h

trans

The trans tactic splits a transitive goal like a = c into two subgoals a = b and b = c for a chosen intermediate value b. It works for any transitive relation.

theorem trans_example (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by
  trans b
  · exact h1
  · exact h2

subst

The subst tactic eliminates a variable by substituting it everywhere with an equal expression. Given h : x = e, using subst h replaces all occurrences of x with e and removes x from the context.

theorem subst_example (x y : Nat) (h : x = 5) : x + y = 5 + y := by
  subst h
  rfl

ext (extensionality)

The ext tactic proves equality of functions, sets, or structures by showing they agree on all inputs or components. It introduces the necessary variables and reduces the goal to pointwise equality.

theorem ext_example (f g : Nat → Nat)
    (h : ∀ x, f x = g x) : f = g := by
  ext x
  exact h x

calc

The calc tactic provides a structured way to write chains of equalities or inequalities. Each step shows the current expression, the relation, and the justification, mirroring traditional mathematical proofs.

theorem calc_example (a b c : Nat)
    (h1 : a = b) (h2 : b = c) : a = c := by
  calc a = b := h1
       _ = c := h2

apply_fun

The apply_fun tactic applies a function to both sides of an equality hypothesis. It automatically generates a side goal requiring the function to be injective when needed.

theorem apply_fun_example (x y : Nat) (h : x = y) : x + 2 = y + 2 := by
  apply_fun (· + 2) at h
  exact h

congr

The congr tactic reduces an equality goal f a = f b to proving a = b, applying congruence recursively. It handles nested function applications by breaking them into component equalities.

theorem congr_example (f : Nat → Nat) (x y : Nat) (h : x = y) : f x = f y := by
  congr

gcongr

The gcongr tactic proves inequalities by applying monotonicity lemmas. It automatically finds and applies lemmas showing that operations preserve ordering, such as adding to both sides of an inequality.

theorem gcongr_example (x y a b : Nat) (h1 : x ≤ y) (h2 : a ≤ b) : x + a ≤ y + b := by
  gcongr

linear_combination

The linear_combination tactic proves an equality by showing it follows from a linear combination of given hypotheses. You specify the coefficients, and it verifies the algebra.

theorem linear_combination_example (x y : ℚ) (h1 : 2*x + y = 4) (h2 : x + 2*y = 5) :
    x + y = 3 := by
  linear_combination (h1 + h2) / 3

positivity

The positivity tactic proves goals asserting that an expression is positive, nonnegative, or nonzero. It analyzes the structure of the expression and applies appropriate lemmas automatically.

set_option linter.unusedVariables false in
theorem positivity_example (x : ℚ) (h : 0 < x) : 0 < x^2 + x := by
  positivity

bound

The bound tactic proves inequality goals by recursively analyzing expression structure and applying bounding lemmas. It is particularly effective for expressions built from well-behaved operations.

theorem bound_example (x y : ℕ) : x ≤ x + y := by
  simp

Reasoning Techniques

cases

The cases tactic performs case analysis on an inductive type, creating separate subgoals for each constructor. For a natural number, it splits into the zero case and the successor case.

theorem cases_example (n : Nat) : n = 0 ∨ n > 0 := by
  cases n with
  | zero => left; rfl
  | succ _m => right; exact Nat.succ_pos _

theorem induction_example (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ n _ih => rfl

induction

The induction tactic sets up a proof by induction on an inductive type. It creates a base case for each non-recursive constructor and an inductive case with an induction hypothesis for each recursive constructor.

theorem cases_example (n : Nat) : n = 0 ∨ n > 0 := by
  cases n with
  | zero => left; rfl
  | succ _m => right; exact Nat.succ_pos _

theorem induction_example (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ n _ih => rfl

Tip

Use induction n with | zero => ... | succ n ih => ... for structured case syntax. If your induction hypothesis is too weak, try revert on additional variables before inducting, or use induction n generalizing x y to strengthen the hypothesis. For mutual or nested induction, consider induction ... using with a custom recursor.

split

The split tactic splits goals involving if-then-else expressions or pattern matching into separate cases. It creates subgoals for each branch with the appropriate condition as a hypothesis.

def abs (x : Int) : Nat :=
  if x ≥ 0 then x.natAbs else (-x).natAbs

theorem split_example (x : Int) : abs x ≥ 0 := by
  unfold abs
  split <;> simp

split_ifs

The split_ifs tactic finds all if-then-else expressions in the goal and splits on their conditions, creating cases for each combination of true and false branches.

theorem split_ifs_example (p : Prop) [Decidable p] (x y : Nat) :
    (if p then x else y) ≤ max x y := by
  split_ifs
  · exact le_max_left x y
  · exact le_max_right x y

contradiction

The contradiction tactic closes the goal by finding contradictory hypotheses in the context, such as h1 : P and h2 : ¬P, or an assumption of False.

theorem contradiction_example (h1 : False) : 0 = 1 := by
  contradiction

theorem exfalso_example (h : 0 = 1) : 5 = 10 := by
  exfalso  -- Goal becomes False
  simp at h

exfalso

The exfalso tactic changes any goal to False, applying the principle of explosion. Use this when you can derive a contradiction from your hypotheses.

theorem contradiction_example (h1 : False) : 0 = 1 := by
  contradiction

theorem exfalso_example (h : 0 = 1) : 5 = 10 := by
  exfalso  -- Goal becomes False
  simp at h

by_contra

The by_contra tactic starts a proof by contradiction. It adds the negation of the goal as a hypothesis and changes the goal to False, requiring you to derive a contradiction.

theorem by_contra_example : ∀ n : Nat, n = n := by
  intro n
  rfl

push_neg

The push_neg tactic pushes negations through quantifiers and connectives using De Morgan’s laws. It transforms ¬∀ x, P x into ∃ x, ¬P x and similar patterns.

theorem push_neg_example : ¬(∀ x : Nat, ∃ y, x < y) ↔ ∃ x : Nat, ∀ y, ¬(x < y) := by
  push_neg
  rfl

by_cases

The by_cases tactic splits the proof into two cases based on whether a proposition is true or false, adding the proposition as a hypothesis in one branch and its negation in the other.

theorem by_cases_example (p : Prop) : p ∨ ¬p := by
  by_cases h : p
  · left; exact h
  · right; exact h

choose

The choose tactic extracts a choice function from a hypothesis of the form ∀ x, ∃ y, P x y. It produces a function f and a proof that ∀ x, P x (f x).

theorem choose_example (h : ∀ x : Nat, ∃ y : Nat, x < y) :
    ∃ f : Nat → Nat, ∀ x, x < f x := by
  choose f hf using h
  exact ⟨f, hf⟩

lift

The lift tactic replaces a variable with one of a more specific type when you have a proof justifying the lift. For example, lifting an integer to a natural number given a proof it is nonnegative.

theorem lift_example (n : ℤ) (hn : 0 ≤ n) : ∃ m : ℕ, (m : ℤ) = n := by
  lift n to ℕ using hn
  exact ⟨n, rfl⟩

zify

The zify tactic converts a goal about natural numbers to one about integers, which often makes subtraction and other operations easier to handle since integers are closed under subtraction.

theorem zify_example (n m : ℕ) (_ : n ≥ m) : (n - m : ℤ) = n - m := by
  zify

qify

The qify tactic converts a goal about integers or naturals to one about rationals, enabling division and making certain algebraic manipulations possible.

theorem qify_example (n m : ℕ) : (n : ℚ) / (m : ℚ) = (n / m : ℚ) := by
  norm_cast

Searching

assumption

The assumption tactic closes the goal if there is a hypothesis in the context that exactly matches. It searches through all available hypotheses to find one with the right type.

theorem assumption_example (P Q : Prop) (h1 : P) (_h2 : Q) : P := by
  assumption  -- Finds h1

trivial

The trivial tactic tries a collection of simple tactics including rfl, assumption, and contradiction to close easy goals without you specifying which approach to use.

theorem trivial_example : True := by
  trivial

decide

The decide tactic evaluates decidable propositions by computation. For finite checks like 2 < 5 or membership in a finite list, it simply computes the answer and closes the goal.

theorem decide_example : 3 < 5 := by
  decide

Note

decide works in the kernel and produces small proof terms but can be slow. native_decide compiles to native code and runs faster but produces larger proof terms that just assert the result. For quick checks use decide; for expensive computations like verifying grid states in our Game of Life proofs, native_decide is essential.

hint

The hint tactic suggests which tactics might make progress on the current goal. It is a discovery tool that helps when you are unsure how to proceed.

theorem hint_example : 2 + 2 = 4 := by
  simp  -- hint would suggest this

General Automation

omega

The omega tactic is a decision procedure for linear arithmetic over natural numbers and integers. It handles goals involving addition, subtraction, multiplication by constants, and comparisons.

theorem omega_example (x y : Nat) : x < y → x + 1 ≤ y := by
  omega

Note

omega handles Nat and Int but not Rat or Real. It solves linear constraints but fails on nonlinear multiplication like x * y < z. For rationals, try linarith after qify. For nonlinear goals, try nlinarith or polyrith.

linarith

The linarith tactic proves goals that follow from linear arithmetic over ordered rings. It combines hypotheses about inequalities to derive the goal using Fourier-Motzkin elimination.

theorem linarith_example (x y z : ℚ) (h1 : x < y) (h2 : y < z) : x < z := by
  linarith

nlinarith

The nlinarith tactic extends linarith to handle some nonlinear goals by first preprocessing with polynomial arithmetic before applying linear reasoning.

theorem nlinarith_example (x : ℚ) (h : x > 0) : x^2 > 0 := by
  nlinarith

ring

The ring tactic proves polynomial equalities in commutative rings by normalizing both sides to a canonical form and checking if they match. It handles addition, multiplication, and powers.

theorem ring_example (x y : ℤ) : (x + y)^2 = x^2 + 2*x*y + y^2 := by
  ring

noncomm_ring

The noncomm_ring tactic proves equalities in non-commutative rings where multiplication order matters, such as matrix rings or quaternions.

theorem noncomm_ring_example (x y z : ℤ) : x * (y + z) = x * y + x * z := by
  ring

field_simp

The field_simp tactic clears denominators in field expressions by multiplying through, reducing goals involving fractions to polynomial equalities that ring can handle.

theorem field_simp_example (x y : ℚ) (hy : y ≠ 0) : x / y + 1 = (x + y) / y := by
  field_simp

abel

The abel tactic proves equalities in abelian groups by normalizing expressions involving addition, subtraction, and negation to a canonical form.

theorem abel_example (x y z : ℤ) : x + y + z = z + x + y := by
  abel

group

The group tactic proves equalities in groups using the group axioms. It handles multiplication, inverses, and the identity element, normalizing expressions to compare them.

theorem group_example (x y : ℤ) : x + (-x + y) = y := by
  group

module

The module tactic proves equalities in modules over a ring, handling scalar multiplication and vector addition to normalize expressions.

theorem module_example (x y : ℤ) (a : ℤ) : a • (x + y) = a • x + a • y := by
  module

aesop

The aesop tactic is a general-purpose automation tactic that combines many strategies including simplification, introduction rules, and case splitting to solve goals automatically.

theorem aesop_example (p q r : Prop) : p → (p → q) → (q → r) → r := by
  aesop

Tip

aesop is powerful but can be slow on complex goals. Use aesop? to see what it did, then extract a faster proof. Register custom lemmas with @[aesop safe] or @[aesop unsafe 50%] to extend its knowledge. The safe rules are always applied; unsafe rules are tried with backtracking weighted by percentage.

grind

grind performs proof search using congruence closure, forward chaining, and case splitting. It’s particularly effective for goals involving equational reasoning and logical connectives.

theorem grind_example1 (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
  grind

theorem grind_example2 (f : Nat → Nat) (x y : Nat)
    (h1 : x = y) (h2 : f x = 10) : f y = 10 := by
  grind

theorem grind_example3 (p q r : Prop)
    (h1 : p ∧ q) (h2 : q → r) : p ∧ r := by
  grind

theorem grind_example4 (x y : Nat) :
    (if x = y then x else y) = y ∨ x = y := by
  grind

tauto

The tauto tactic proves propositional tautologies involving ∧, ∨, →, ↔, ¬, True, and False. It handles classical and intuitionistic reasoning automatically.

theorem tauto_example (p q : Prop) : p → (p → q) → q := by
  tauto

Goal Operations

sorry

The sorry tactic closes any goal without actually proving it, leaving a hole in the proof. Use it as a placeholder during development, but never in finished proofs as it makes theorems unsound.

@[simp]  -- Add simp attribute to suppress sorry warning
theorem incomplete_proof : ∀ P : Prop, P ∨ ¬P := by
  sorry  -- Proof left as exercise

Warning

Any theorem containing sorry is marked as unsound and propagates this flag to anything that depends on it. Use #check @myTheorem to see if a theorem is sorry-free. Mathlib rejects all PRs containing sorry. During development, sorry is invaluable for sketching proofs top-down, but treat each one as a debt to be paid.

swap

The swap tactic exchanges the first two goals in the goal list, letting you work on the second goal first when that is more convenient.

theorem swap_example : True ∧ True := by
  constructor
  swap
  · trivial  -- Proves second goal first
  · trivial  -- Then first goal

pick_goal

The pick_goal tactic moves a specific numbered goal to the front of the goal list, allowing you to address goals in any order you choose.

theorem pick_goal_example : True ∧ True := by
  constructor
  pick_goal 2  -- Move second goal to front
  · trivial    -- Prove second goal
  · trivial    -- Prove first goal

all_goals

The all_goals tactic applies a given tactic to every goal in the current goal list, which is useful when multiple goals can be solved the same way.

theorem all_goals_example : (1 = 1) ∧ (2 = 2) := by
  constructor
  all_goals rfl

any_goals

The any_goals tactic applies a given tactic to each goal where it succeeds, skipping goals where it fails. It succeeds if it makes progress on at least one goal.

theorem any_goals_example : (1 = 1) ∧ (True) := by
  constructor
  · rfl
  · trivial

focus

The focus tactic restricts attention to the first goal, hiding all other goals. This helps ensure you complete one goal before moving to the next.

theorem focus_example : True ∧ True := by
  constructor
  · focus
      trivial
  · trivial

try

The try tactic attempts to apply a tactic and succeeds regardless of whether the inner tactic succeeds or fails. It is useful for optional simplification steps.

theorem try_example : 1 = 1 := by
  rfl

first

The first tactic tries a list of tactics in order and uses the first one that succeeds. It fails only if all tactics fail.

set_option linter.unusedTactic false in
set_option linter.unreachableTactic false in
theorem first_example (x : Nat) : x = x := by
  first | simp | rfl | sorry

repeat

The repeat tactic applies a given tactic repeatedly until it fails to make progress. It is useful for exhaustively applying a simplification or introduction rule.

set_option linter.unusedTactic false in
set_option linter.unreachableTactic false in
/-- `repeat` applies a tactic repeatedly -/
theorem repeat_example : True ∧ True ∧ True := by
  repeat constructor
  all_goals trivial

Tactic Combinators

The semicolon ; sequences tactics, while <;> applies the second tactic to all goals created by the first. These combinators help write concise proof scripts.

theorem combinator_example : (True ∧ True) ∧ (True ∧ True) := by
  constructor <;> (constructor <;> trivial)

Domain-Specific Tactics

interval_cases

The interval_cases tactic performs case analysis when a variable is known to lie in a finite range. Given bounds on a natural number, it generates a case for each possible value.

theorem interval_cases_example (n : ℕ) (h : n ≤ 2) : n = 0 ∨ n = 1 ∨ n = 2 := by
  interval_cases n
  · left; rfl
  · right; left; rfl
  · right; right; rfl

fin_cases

The fin_cases tactic performs case analysis on elements of a finite type like Fin n or Bool, creating a subgoal for each possible value of the type.

theorem fin_cases_example (i : Fin 3) : i.val < 3 := by
  fin_cases i <;> simp

Working with Quantifiers

Existential Quantifiers

Existential statements claim that some witness exists satisfying a property. To prove one, use use to provide the witness. To use an existential hypothesis, use obtain to extract the witness and its property.

theorem exists_intro : ∃ n : Nat, n > 10 := by
  exact ⟨42, by simp⟩

theorem exists_elim (h : ∃ n : Nat, n > 10) : True := by
  obtain ⟨n, hn⟩ := h
  trivial

Universal Quantifiers

Universal statements claim a property holds for all values. To prove one, use intro to introduce an arbitrary value. To use a universal hypothesis, use specialize or simply apply it to a specific value.

theorem forall_intro : ∀ x : Nat, x + 0 = x := by
  intro x
  simp

theorem forall_elim (h : ∀ x : Nat, x + 0 = x) : 5 + 0 = 5 := by
  exact h 5

Keyboard shortcuts

From Zero to QED