Tactic Cheat Sheet
Quick reference for every Lean 4 tactic. Search, filter by category, and click to learn more.
Showing 35 of 35 tactics
| Tactic | Description |
|---|---|
| rfl | Prove equalities by computation (reflexivity) |
| rw | Rewrite the goal or hypothesis using an equality |
| simp | Simplify using a database of @[simp] lemmas |
| exact | Close a goal with an exact proof term |
| apply | Apply a function or lemma to reduce a goal |
| intro | Introduce hypotheses from implications or ∀ |
| have | State and prove an intermediate lemma |
| let | Introduce a local definition in the proof |
| cases | Split into cases for inductive types |
| induction | Prove by induction on a variable |
| omega | Solve linear arithmetic over ℕ and ℤ |
| decide | Evaluate decidable propositions |
| native_decide | Like decide but uses compiled native code |
| aesop | Automated proof search combining multiple strategies |
| simp only | Simplify using only specified lemmas |
| simp_all | Simplify goal and all hypotheses |
| termination_by | Specify termination measure for recursive defs |
| calc | Step-by-step equational/relational reasoning |
| conv | Navigate into subexpressions for targeted rewrites |
| by_contra | Prove by contradiction |
| by_cases | Split on a decidable proposition |
| <;> | Apply a tactic to all remaining goals |
| first | Try tactics in order, use the first that works |
| repeat | Repeat a tactic until it fails |
| ring | Prove polynomial identities over rings |
| field_simp | Clear denominators in field expressions |
| linarith | Prove linear arithmetic inequalities |
| nlinarith | Prove nonlinear arithmetic goals |
| polyrith | Find polynomial proofs via Gröbner bases |
| rcases | Recursive case split / pattern match on hypotheses |
| obtain | Destructure and introduce existential witnesses |
| push_neg | Push negations inward using De Morgan rules |
| contrapose | Transform goal to its contrapositive |
| ext | Prove equality by extensionality |
| congr | Break equality into congruence subgoals |