Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover/lean4/llms.txt

Use this file to discover all available pages before exploring further.

Lean 4 supports two styles of proof: tactic mode (interactive, goal-directed) and term mode (direct construction of a proof term). In term mode you write a Lean expression whose type is the proposition you want to prove — no tactics, no goal state. Understanding term-mode proofs gives you a deep insight into how Lean’s kernel works, and it is often the right choice for short, transparent proofs.

​
When to Use Term Mode vs Tactic Mode

SituationPrefer
Short, structural proof (one or two steps)Term mode
Simple equational reasoning (rfl, Eq.trans)Term mode
Complex multi-step proof with many goalsTactic mode
Automation needed (omega, simp, grind)Tactic mode
Proof readability for future readersEither; calc bridges both
Performance-sensitive proof (large terms)Tactic mode with have
You can freely nest by inside a term-mode proof to hand off any subgoal to tactic mode, and you can use term expressions inside tactic mode with exact. The two styles complement each other.

​
Lambda Proofs of ∀

Because ∀ x : α, P x is literally a dependent function type (x : α) → P x, a proof of a universally-quantified proposition is just a function: 
-- Proof of ∀ n : Nat, n + 0 = n
theorem add_zero_term : ∀ n : Nat, n + 0 = n :=
  fun n => rfl

-- Proof of an implication (→ is a special case of ∀)
theorem imp_id : ∀ p : Prop, p → p :=
  fun _p hp => hp

​
Anonymous Constructor Syntax ⟨a, b⟩

For any structure or inductive type with a single constructor, you can use angle brackets ⟨...⟩ as a shorthand. This is used constantly for And, Exists, Subtype, and custom structures. 
-- Proof of p ∧ q
theorem and_intro_term (hp : p) (hq : q) : p ∧ q := ⟨hp, hq⟩

-- Proof of ∃ n, n > 0
theorem exists_pos : ∃ n : Nat, n > 0 := ⟨1, Nat.one_pos⟩

-- Nested anonymous constructors
theorem and_assoc_term (h : p ∧ (q ∧ r)) : (p ∧ q) ∧ r :=
  ⟨⟨h.1, h.2.1⟩, h.2.2⟩

​
Eq.subst and Eq.mpr

When you have a proof h : a = b and a proof ha : P a, you can obtain P b using Eq.subst: 
-- Eq.subst : a = b → P a → P b
example (α : Type) (a b : α) (P : α → Prop) (h : a = b) (ha : P a) : P b :=
  h ▸ ha   -- the ▸ notation is sugar for Eq.subst
Eq.mpr is the primitive used internally. Given h : P = Q (a proof that types are equal), Eq.mpr h : Q → P. This appears in desugared rewrites: 
-- Eq.mpr used explicitly (rarely needed directly)
example (n : Nat) : n + 0 = n :=
  Eq.mpr (congrArg (n + 0 = ·) (Nat.add_zero n)) rfl

​
congrArg

congrArg f h lifts h : a = b through a function f, yielding f a = f b: 
theorem succ_congr (m n : Nat) (h : m = n) : m + 1 = n + 1 :=
  congrArg (· + 1) h

​
show — Type Annotation in Proofs

show t in a term-mode context is @id t, which forces Lean to unify the expected type with t. It is helpful for readability when the inferred type is not obvious: 
theorem show_term (p q : Prop) (h : p ↔ q) (hp : p) : q :=
  show q from h.mp hp

-- Also works inside by blocks:
theorem show_tactic (n : Nat) : n + 0 = n := by
  show n + 0 = n
  rfl

​
have and let in Term Mode

have binds a local proof term; let binds a local definition that may appear in subsequent types. 
theorem have_term (p q r : Prop) (hpq : p → q) (hqr : q → r) (hp : p) : r :=
  have hq : q := hpq hp
  have hr : r := hqr hq
  hr

-- let for local definitions
theorem let_term (n : Nat) : n + 2 = n + 1 + 1 :=
  let m := n + 1
  show n + 2 = m + 1 from rfl

​
suffices in Term Mode

suffices h : t from e introduces an intermediate goal t. You then provide e : original_goal which may refer to h : t, followed by a proof of t. 
theorem suffices_term (n : Nat) (h : n ≥ 2) : n ≥ 1 :=
  suffices h' : n ≥ 2 from Nat.le_trans (by omega) h'
  h

​
calc Blocks

calc is ideal for chains of equalities, inequalities, or any transitive relation. It is the clearest way to present multi-step equational proofs in either term or tactic mode. 
-- A calc block in term mode
theorem calc_example (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a = c :=
  calc a = b := h₁
       _ = c := h₂

-- calc with mixed relations (requires Trans instances)
theorem calc_mixed (n : Nat) (h : n ≥ 5) : n ≥ 3 :=
  calc n ≥ 5 := h
       _ ≥ 3 := by omega

-- calc as a tactic inside by
theorem calc_tactic (a b : Nat) : (a + b) * 2 = 2 * a + 2 * b := by
  calc (a + b) * 2
      = a * 2 + b * 2 := Nat.add_mul a b 2
    _ = 2 * a + 2 * b := by omega

​
match in Proofs

match on a proof of an inductive proposition is the primitive behind cases and obtain. It is fully available in term-mode proofs. 
-- Proof of Or.comm
theorem or_comm_term (h : p ∨ q) : q ∨ p :=
  match h with
  | Or.inl hp => Or.inr hp
  | Or.inr hq => Or.inl hq

-- Destructuring And in term mode
theorem proj_right (h : p ∧ q) : q :=
  match h with
  | And.intro _ hq => hq
  -- equivalent to: h.right
For And, use .left / .right projections. For Or, use match or Or.elim. For Exists, use h.choose and h.choose_spec (classical) or let ⟨x, hx⟩ := h.

​
Combining Term Mode and Tactic Mode

You can freely switch between the two styles. The most common pattern is a term-mode skeleton with by leaves: 
theorem combined_example (n : Nat) (h : n > 2) : ∃ m, n = m + 3 :=
  ⟨n - 3, by omega⟩

-- Using term-mode for structure and tactic for arithmetic
theorem combined_and (p : Prop) (n : Nat) (hp : p) (hn : n > 0) : p ∧ n ≠ 0 :=
  ⟨hp, by omega⟩
The other direction — a by block with exact to hand off to term mode — is equally natural: 
theorem tactic_with_term (p q r : Prop) (hpq : p → q) (hqr : q → r) : p → r := by
  exact fun hp => hqr (hpq hp)

​
A Self-Contained Term-Mode Proof

Here is a complete proof of function composition, written entirely in term mode: 
-- Function composition is associative
theorem comp_assoc
    {α β γ δ : Type}
    (f : α → β) (g : β → γ) (h : γ → δ) :
    (h ∘ g) ∘ f = h ∘ (g ∘ f) :=
  rfl   -- definitionally true; the kernel checks it directly
And a slightly more involved proof using have and calc: 
theorem add_comm_three (a b c : Nat) : a + b + c = c + b + a :=
  calc a + b + c
      = a + (b + c) := by rw [Nat.add_assoc]
    _ = a + (c + b) := by rw [Nat.add_comm b c]
    _ = c + b + a   := by omega
Every proof term in Lean 4 — whether produced by tactics or written directly — is ultimately checked by the kernel: a small, trusted elaborator that verifies type correctness. Tactics are macros that generate kernel-checkable proof terms. This means:
  • A by omega proof compiles to a proof term the kernel can verify without trusting the omega solver itself (in kernel mode).
  • native_decide is a partial exception: it trusts the native compiler rather than the kernel.
  • You can see the actual proof term with #print myTheorem or set_option pp.all true.

Build docs developers (and LLMs) love

Get started for freeTalk to us