Tactic cheatsheet

Reference, not a lesson: each tactic below was introduced somewhere in Part I, with a worked example in context. This page exists so you don’t have to go find that chapter again.

Every example on this page compiles: paste one into the playground with import Mathlib on top and it goes through as written, with the one exception of the #check/#print axioms block at the end, which quotes a theorem from this tutorial’s own library and therefore needs the library’s preamble — any <Snippet> elsewhere on the site will hand it to you. The fences are plain code blocks rather than runnable ones because a cheatsheet is for reading, but they were compiled to make sure the reading is not a lie.

Closing a goal outright

These end the proof. Nothing is left afterward.

Tactic	What it does	Reach for it when
exact	Supplies a term that has exactly the goal’s type.	You already have (or can write down) a proof term or a fully-applied lemma.
rfl	Closes a goal a = a (or a ↔ a) up to unfolding definitions and computation.	The two sides are definitionally the same thing, just spelled differently.
decide	Evaluates a decidable proposition to true/false and checks the result.	The statement is concrete and small — a fact about Fin 3, not about an arbitrary n.
norm_num	Evaluates and normalizes numeral expressions.	The goal is arithmetic on literal numbers, in ℕ, ℤ, ℚ, or ℝ.
simp	Rewrites with the whole @[simp] lemma database until nothing changes.	You want something obviously-true-looking to just close, and don’t need to name what fired.
ring	Proves any identity that holds in every commutative ring.	The goal is an equation of +, -, *, ^ (division allowed, treated as multiplication by an inverse) with no hypotheses needed.
linarith	Closes goals that follow from the hypotheses by linear arithmetic.	You need to add / scale-by-a-positive-constant some inequalities and hypotheses you already have.
nlinarith	linarith, plus it will try products of hypotheses you hand it.	The goal is genuinely nonlinear — a variance-style bound, a square term.
positivity	Proves 0 < e, 0 ≤ e, or e ≠ 0 by walking the syntax of e.	e is visibly a sum of squares, a sample size, a probability — built from positive pieces.
omega	A decision procedure for linear arithmetic over ℕ and ℤ, truncated subtraction included.	The goal is about sample sizes / counts in ℕ, especially anything involving n - k.
field_simp	Clears denominators, given they are provably nonzero.	The goal is an equation about means or ratio estimators and you want to get rid of the /.

Examples, in the same order:

exact

theorem effect_nonneg (y1 y0 : Fin 3 → ℝ) (h : ∀ i, y0 i ≤ y1 i) :
    y0 0 ≤ y1 0 := by
  exact h 0

rfl

example : (2 : ℕ) + 2 = 4 := rfl

decide

example : ∀ i : Fin 3, i.val < 3 := by decide

norm_num

example : ((2 : ℝ) + 4 + 6) / 3 = 4 := by norm_num

simp

example (n : ℕ) : (Finset.range n).card = n := by simp

ring

example (x m : ℝ) : (x - m) ^ 2 = x ^ 2 - 2 * m * x + m ^ 2 := by ring

linarith

example (a b : ℝ) (hab : a ≤ b) : a ≤ (a + b) / 2 := by linarith

nlinarith

example (a b : ℝ) : 2 * (a * b) ≤ a ^ 2 + b ^ 2 := by
  nlinarith [sq_nonneg (a - b)]

positivity

example (n : ℕ) (hn : 0 < n) : 0 < (n : ℝ) ^ 2 + 1 := by positivity

omega

example (n n1 : ℕ) (h : n1 ≤ n) : n1 + (n - n1) = n := by omega

field_simp

example (a b m : ℝ) (h : (a + b) / 2 = m) : a + b = 2 * m := by
  field_simp at h
  linarith

Transforming a goal

These make progress without closing the goal — they leave you with something smaller, or several somethings.

Tactic	What it does	Reach for it when
intro	Moves the antecedent of a → or ∀ from the goal into the context.	The goal is ∀ x, … or h → … and you want x / h as a hypothesis.
apply	Works backwards: unifies the goal with a lemma’s conclusion, leaves its remaining hypotheses as new goals.	You know which lemma proves this, and want Lean to figure out what’s left.
refine	exact with holes (?_) left where you want new goals.	You know the shape of the term (an anonymous constructor, a lemma with some obvious and some non-obvious arguments) but not every piece yet.
rw	Replaces occurrences of an equation’s left-hand side by its right-hand side in the goal (rw [← h] goes right-to-left).	You have an equation and want to substitute it into the goal, not prove the goal outright.
simp only	Like simp, but only with the exact lemma list you name.	You want simp’s rewriting without the opacity — the standard style for anything meant to be read.
unfold	Replaces a def by its right-hand side in the goal.	The goal mentions a name whose definition you need to see to make progress.
show	Restates the goal in a definitionally equal form.	You want to tell Lean (and the reader) what you think the goal actually is, before proceeding.
change	Like show, but can also target the type of a hypothesis mid-proof.	A previous tactic left a goal that is correct but ugly, and you want to fold it back to a named form.
calc	Writes a chain of equalities/inequalities with a justification per step, exactly as on paper.	The proof is a sequence of algebraic steps and you want it readable, not a black box.
have	Proves an intermediate fact and adds it to the context — “note that …”.	You want to name and reuse a fact partway through, or make an implicit step explicit.
obtain / rcases	Takes apart an ∃, ∧, or ∨ (same tactic, two spellings).	A hypothesis packages a witness or a case split you need to unpack before proceeding.
cases	The low-level version of obtain/rcases: one named goal per constructor.	You want to write out each resulting case explicitly, e.g. by pattern name.
constructor	Applies the constructor of an inductive goal — for ∧, splits into the two conjuncts.	The goal is a conjunction, an ↔ (via Iff.intro), or another one-constructor inductive type.
use	Supplies a witness for an ∃ goal, leaving the property to prove.	The goal is ∃ x, p x and you already know which x works.
ext / funext	Turns a goal about equal functions/sets into a goal about equal values/membership.	Two functions or Finsets are equal because they agree pointwise, and that pointwise fact is easier.
by_cases	Splits the proof on whether a decidable proposition holds.	An indicator, an if-then-else, or any statement that is genuinely two cases.
by_contra	Assumes the negation of the goal and aims for False.	A direct proof is awkward, but assuming the goal is false gives you an immediate contradiction.
exfalso	Replaces any goal by False.	You intend to derive a contradiction from hypotheses that are already jointly impossible.
push_cast / norm_cast	Push a (· : ℝ) coercion toward the leaves of an expression, or remove it altogether.	The goal mixes ℕ and ℝ (or another coercion) and you need it uniformly in one type.
congr	Reduces f a = f b to a = b (and similar), by peeling off the shared structure.	The two sides of an equation differ in only one argument of an otherwise-identical expression.
gcongr	congr aware of monotonicity: reduces an inequality between similar-shaped expressions to inequalities between their pieces.	The goal is f a ≤ f b for a known-monotone f (sums, products of nonnegatives, …).

Examples, in the same order:

intro

example (y1 y0 : Fin 3 → ℝ) : (∀ i, y0 i ≤ y1 i) → y0 0 ≤ y1 0 := by
  intro h
  exact h 0

apply

example (a b c : ℝ) (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c := by
  apply le_trans
  · exact hab
  · exact hbc

refine

example (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a ∧ 0 ≤ a + b := by
  refine ⟨ha, ?_⟩
  exact add_nonneg ha hb

rw

example (y1 yobs : ℝ) (h : yobs = y1) (hy : y1 = 3) : yobs = 3 := by
  rw [h]
  exact hy

simp only

example (y : Fin 3 → ℝ) : y 0 + 0 + y 1 * 1 = y 0 + y 1 := by
  simp only [add_zero, mul_one]

unfold

def sqr (x : ℝ) : ℝ := x * x

example (x : ℝ) : sqr x = x ^ 2 := by
  unfold sqr
  ring

show

example (π : ℝ) (hπ : 0 < π) : π * π⁻¹ = 1 := by
  show π / π = 1        -- `a * a⁻¹` and `a / a` are definitionally the same
  exact div_self hπ.ne'

change

def Z (z : Finset (Fin 3)) (i : Fin 3) : ℝ := if i ∈ z then 1 else 0

example (z : Finset (Fin 3)) (i : Fin 3) (h : i ∈ z) : Z z i = 1 := by
  change (if i ∈ z then (1 : ℝ) else 0) = 1   -- unfold `Z` by hand
  simp [h]

calc

example (z y1 y0 : ℝ) : z * y1 + (1 - z) * y0 = y0 + z * (y1 - y0) := by
  calc z * y1 + (1 - z) * y0
      = z * y1 + y0 - z * y0 := by ring
    _ = y0 + z * (y1 - y0) := by ring

have

example (a b c : ℝ) (h : a ≤ b) (h' : b ≤ c) : a ≤ c := by
  have step : a ≤ b := h
  exact le_trans step h'

obtain / rcases

example (y1 y0 : Fin 3 → ℝ) (h : ∃ i, y1 i - y0 i = 2) :
    ∃ i, 0 < y1 i - y0 i := by
  obtain ⟨i, hi⟩ := h        -- `rcases h with ⟨i, hi⟩` is identical
  exact ⟨i, by rw [hi]; norm_num⟩

cases

example (h : True ∨ True) : True := by
  cases h with
  | inl h => exact h
  | inr h => exact h

constructor

example (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a ∧ 0 ≤ b := by
  constructor
  · exact ha
  · exact hb

use

example (y1 y0 : Fin 3 → ℝ) (h : y0 2 < y1 2) : ∃ i, y0 i < y1 i := by
  use 2

ext / funext

example (y1 y0 : Fin 3 → ℝ) (h : ∀ i, y1 i = y0 i) : y1 = y0 := by
  funext i
  exact h i

example (s t : Finset (Fin 3)) (h : ∀ i, i ∈ s ↔ i ∈ t) : s = t := by
  ext i
  exact h i

by_cases

example (i : Fin 3) (z : Finset (Fin 3)) :
    (if i ∈ z then (1 : ℝ) else 0) * (if i ∈ z then (1 : ℝ) else 0)
      = if i ∈ z then (1 : ℝ) else 0 := by
  by_cases h : i ∈ z
  · rw [ite_eq_left h, mul_one]
  · rw [ite_eq_right h, mul_zero]

by_contra

example (x : ℝ) (h : ¬ (x < 0)) : 0 ≤ x := by
  by_contra hc
  exact h (lt_of_not_ge hc)

exfalso

example (n : ℕ) (h1 : 0 < n) (h2 : n = 0) : (1 : ℝ) = 2 := by
  exfalso
  rw [h2] at h1
  exact absurd h1 (lt_irrefl 0)

push_cast / norm_cast

example (n1 n0 : ℕ) : ((n1 + n0 : ℕ) : ℝ) = (n1 : ℝ) + (n0 : ℝ) := by
  push_cast
  ring

congr

example (f : ℝ → ℝ) (a b : ℝ) (h : b = a) : f a = f b := by
  congr 1        -- goal is now `a = b`
  exact h.symm

gcongr

example (a b c d : ℝ) (hb : 0 ≤ b) (hc : 0 ≤ c) (h1 : a ≤ b) (h2 : c ≤ d) :
    a * c ≤ b * d := by
  gcongr

Searching for a lemma

None of these belong in a finished proof — run them, read what they print, paste the answer in, delete the search tactic.

Tactic	What it does	Reach for it when
exact?	Looks for a single lemma that closes the goal outright.	You suspect the exact fact you need is already in Mathlib, verbatim.
apply?	Looks for lemmas whose conclusion matches the goal, even if they leave hypotheses.	exact? came up empty but the goal still looks like a known shape.
simp?	Runs simp, then prints the simp only [...] it actually used.	You want a simp call to survive into readable, reviewable code.
rw?	Lists rewrites that apply to the current goal.	You know the goal needs some rewrite but not which lemma provides it.
hint	Tries a battery of closing tactics (assumption, norm_num, decide, exact?, …) and reports which ones work.	You have no idea which single tactic will close the goal and want a menu.

example (x : ℝ) : 0 ≤ x ^ 2 := by
  -- `exact?` reports: Try this: exact sq_nonneg x
  exact sq_nonneg x

example (a b c : ℝ) : (a + b) / c = a / c + b / c := by
  -- `rw?` reports: Try this: rw [add_div]
  rw [add_div]

example (a b : ℝ) (h : a ≤ b) : a ≤ b + 1 := by
  -- `hint` reports several working tactics, e.g.: Try this: exact le_trans h (le_add_of_nonneg_right zero_le_one)
  linarith

Inspecting things

Not tactics — commands you run in the editor to ask Lean a question, rather than to change the goal.

Command	What it does	Reach for it when
#check e	Prints the type of an expression, without evaluating it.	You want to know the exact type Lean assigns to a term or a lemma name, including implicit arguments.
#print n	Prints a declaration’s full definition (or a structure’s fields, or a theorem’s statement).	You want to see what a name actually unfolds to.
#print axioms n	Walks the proof term of n and lists every axiom it transitively depends on.	You want to know whether a theorem — yours or someone else’s — secretly rests on sorry or something unusual.
#eval e	Evaluates e and prints the result, for anything Lean can actually compute.	You want a quick numeric sanity check; does not work on noncomputable (most ℝ-valued) definitions.
#guard_msgs	Asserts that the next command’s output matches an expected message, and fails the file otherwise.	You are writing a doc-test and want the compiler itself to check that an example’s printed output stays correct.

#check @HT_unbiased
-- @HT_unbiased : ∀ {n : ℕ} (D : Design n) (P : Population n),
--   (∀ (i : Fin n), 0 < D.propensity i) → (∀ (i : Fin n), D.propensity i < 1) →
--     D.expect (HT D P) = P.tau

#print axioms HT_unbiased
-- 'MrCLean.HT_unbiased' depends on axioms: [propext, Classical.choice, Quot.sound]

#eval Nat.choose 5 2
-- 10

/-- info: 4 -/
#guard_msgs in
#eval 2 + 2

Common error messages and what they usually mean

Message (abbreviated)	It usually means
Tactic 'rewrite' failed: Did not find an occurrence of the pattern	The equation’s left-hand side doesn’t literally appear in the goal — often the two sides are swapped (rw [← h] instead of rw [h]), or the term is written in an unnormalized form the rewrite can’t see through.
unsolved goals	A tactic block ended without closing every goal — often a tactic that was expected to finish only made partial progress. Read the printed goal state; that’s exactly what’s left.
type mismatch … has type … but is expected to have type …	The term you supplied has the wrong type — classically a ℕ where a ℝ was wanted, or a Prop shaped differently than the goal (wrong quantifier order, ∧ vs ∨).
unknown identifier 'foo'	Misspelling, wrong Mathlib name, or a needed open / namespace prefix is missing. Try exact? or search the docs rather than guessing the exact camel-case.
failed to synthesize instance	A required typeclass (often Decidable, Fintype, or a numeric coercion) isn’t available for the types involved — frequently a sign a ℕ/ℝ mismatch is hiding upstream.
linarith failed to find a contradiction	The goal isn’t a linear consequence of the hypotheses in context — either a needed fact (an inequality, a have) isn’t in scope yet, or the goal actually needs nlinarith or a nonlinear step first.
ring failed, or the goal is silently unchanged after ring	The goal isn’t a ring identity as stated — check for a stray inequality, an unresolved division that needs field_simp first, or a natural-number subtraction that doesn’t commute the way you expect.
declaration uses 'sorry'	Not an error — a warning. Something in this declaration (possibly indirectly, through a lemma it calls) is unproven. Run #print axioms on it to see whether sorryAx shows up.