Tactic Reference

Tactics are commands used inside by blocks to construct proofs step by step. Grouped by purpose; see the Lean Tactic Reference for full documentation.

Closing Tactics

Directly close the current goal.

Tactic	Effect	Introduced	Mathlib
rfl	Close a goal a = a (definitional equality).	P02 S01	~14k
exact	Close the goal with the given term.	P02 S01	~45k
exact?	Search the library for a closing term and suggest it.	P02 S01	—
assumption	Close the goal with a matching hypothesis from the context.	P02 S01	~200
decide	Prove decidable propositions by computation.		~100
trivial	Try rfl, assumption, contradiction, and similar.	P02 S04	~100
contradiction	Close the goal from conflicting hypotheses.	P02 S04	~200

Rewriting

Transform the goal or hypotheses using equalities and rules.

Tactic	Effect	Introduced	Mathlib
rw	Rewrite using an equality or iff; rw [← h] for reverse; rw [...] at k targets a hypothesis.	P02 S01	~70k
nth_rw	Rewrite only the n-th occurrence.	P02 S01	~450
simp	Repeatedly apply rewrite rules from a configurable set; simp only [...] for explicit control.	P02 S01	~45k
push_neg	Push negation inward through connectives and quantifiers.	P02 S04	~150
norm_num	Evaluate closed numerical expressions.		~200
ring	Prove polynomial equalities in commutative (semi)rings.	P05 S04	~800

Goal Structuring

Reshape the goal or introduce intermediate steps.

Tactic	Effect	Introduced	Mathlib
intro	Assume the antecedent of → or ∀, adding it as a hypothesis.	P02 S01	~14k
revert	Move a hypothesis back into the goal (inverse of intro).	P02 S01	~250
apply	Backward reasoning: reduce the goal using a lemma or hypothesis.	P02 S02	~17k
have	Introduce a new fact derived from existing ones.	P02 S02	~36k
suffices	Like have, but prove the main goal first.	P02 S02	~3.1k
refine	Like exact but allows ?_ placeholders that become new goals.	P02 S02	~24k
calc	Chain equalities or inequalities through intermediate steps.	P05 S03	~2.8k
symm	Swap sides of an equality or iff.	P02 S01	~450
trans	Chain two relations through an intermediate value.	P02 S03	~450

Case Analysis and Induction

Split goals or hypotheses by structure.

Tactic	Effect	Introduced	Mathlib
constructor	Split P ∧ Q or P ↔ Q into subgoals.	P02 S03	~3.3k
left / right	Choose which side of P ∨ Q to prove.	P02 S03	~850
obtain	Destructure a hypothesis: obtain ⟨a, b⟩ := h.	P02 S03	~16k
cases	Case analysis on a hypothesis.	P02 S03	~3.2k
rcases	Recursive pattern matching on hypotheses.	P02 S03	~8k
rintro	Combine intro and rcases.	P02 S03	~7k
induction	Structural induction on an inductive type.	P05 S07	~4.2k
by_contra	Assume ¬ goal and derive False (classical).	P02 S04	~1k
by_cases	Split into P and ¬P branches (classical).	P02 S04	~4.6k
exfalso	Change the goal to False.	P02 S04	~150

Existentials and Extensionality

Supply witnesses or prove equality by components.

Tactic	Effect	Introduced	Mathlib
use	Supply a witness for an existential goal.	P02 S05	~2.5k
choose	Extract a witness function from ∀ x, ∃ y, P x y.	P02 S05	~800
ext	Prove f = g by showing f x = g x for arbitrary x.	P02 S05	~11k

Automation

Higher-level tactics that search for or compute proofs.

Tactic	Effect	Introduced	Mathlib
tauto	Close propositional tautologies.	P02 S04	~250
omega	Decision procedure for linear integer/natural arithmetic.		~31
linarith	Prove goals from linear arithmetic over ordered fields.		~350
grind	SMT-style solver handling quantifiers, congruence, and arithmetic.		~1.4k
apply?	Search for a lemma that makes progress and suggest it.	P02 S02	—

Combinators

Modify how other tactics are applied.

Tactic	Effect	Introduced	Mathlib
all_goals	Run a tactic on every open goal.	P02 S03	~600
repeat	Apply a tactic until it fails.	P02 S03	~150
try	Attempt a tactic; succeed silently if it fails.	P02 S03	~150
first	Try tactics in order: first | t₁ | t₂.		—
<;>	Apply a tactic to all goals produced by the previous tactic.	P02 S03	—