Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover-community/mathlib4/llms.txt

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

Structural tactics shape the architecture of a proof: they introduce hypotheses, break compound goals into pieces, provide witnesses for existentials, apply lemmas, and handle classical reasoning. While arithmetic and simplification tactics close goals automatically, structural tactics put you in control of the proof’s logical flow. Every Lean 4 proof writer needs a solid command of apply, exact, refine, obtain, rcases, induction, and ext, as well as the more specialized tools like wlog and tfae_have.

​
apply and exact

apply closes a goal by applying a term whose conclusion matches the goal, generating subgoals for any premises. exact closes a goal completely with a proof term that matches it precisely — it admits no remaining subgoals. 
-- exact: provide the complete proof term
example : 1 + 1 = 2 := by exact rfl

-- apply: use a lemma, generating subgoals for its hypotheses
example (n : ℕ) (h : n > 0) : n ≥ 1 := by
  apply Nat.one_le_iff_ne_zero.mpr
  omega

-- Chaining apply calls
example (a b c : ℕ) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c :=
  Nat.le_trans h1 h2

​
refine

refine is a more flexible version of exact that allows placeholders (_ or ?name) for parts of the term you want to fill in later. It is useful for building up a proof term incrementally. 
-- Use _ as a placeholder for subgoals
example (n : ℕ) : ∃ m, m > n := by
  refine ⟨n + 1, ?_⟩
  omega

-- Named placeholders produce named goals
example (a b : Prop) (ha : a) (hb : b) : a ∧ b := by
  refine ⟨?left, ?right⟩
  · exact ha
  · exact hb

​
constructor

constructor splits a goal that is a conjunction (∧), an iff (↔), an existential (∃), or any inductive type with exactly one constructor, into its component goals. 
example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  · exact hp
  · exact hq

example (n : ℕ) : n = n ↔ True := by
  constructor
  · intro; trivial
  · intro; rfl

​
ext

ext applies extensionality lemmas tagged with @[ext] to reduce equality of structured objects to equality of their components. It is used for functions (via funext), sets (via Set.ext), finsets, bundled morphisms, and many other types. 
-- Extensionality for functions
example (f g : ℕ → ℕ) (h : ∀ n, f n = g n) : f = g := by
  ext n
  exact h n

-- Extensionality for sets
example (s t : Set ℕ) (h : ∀ n, n ∈ s ↔ n ∈ t) : s = t := by
  ext n
  exact h n

-- ext with a specific lemma
example (f g : α →+ β) (h : ∀ x, f x = g x) : f = g := by
  ext x
  exact h x
You can specify how many variables to introduce with ext n (one variable named n) or ext x y (two variables). Without arguments, ext introduces as many as needed.

​
use

use provides witnesses for existential goals (∃ x, P x) and the first component of conjunctive goals. After use t, the goal ∃ x, P x becomes P t. 
example : ∃ n : ℕ, n > 5 := by
  use 6
  norm_num

-- Provide multiple witnesses at once
example : ∃ m n : ℕ, m + n = 10 ∧ m > n := by
  use 7, 3
  constructor <;> norm_num

-- use with a computed expression
example (n : ℕ) : ∃ m : ℕ, m > n := by
  use n + 1
  omega

​
obtain and rcases

obtain and rcases destructure hypotheses by pattern matching. They are the tactic-mode equivalents of match and fun ⟨a, b⟩ => in term mode. Use them to extract components from conjunctions, existentials, disjunctions, and inductive types. 
-- Destructure an existential
example (h : ∃ n : ℕ, n > 5 ∧ n < 10) : True := by
  obtain ⟨n, hn1, hn2⟩ := h
  trivial

-- Destructure a conjunction directly
example (h : P ∧ Q ∧ R) : R := by
  obtain ⟨_, _, hr⟩ := h
  exact hr

-- Nested patterns
example (h : ∃ p : ℕ × ℕ, p.1 + p.2 = 5) : True := by
  obtain ⟨⟨a, b⟩, hab⟩ := h
  trivial

​
cases and induction

cases performs case analysis on an inductive type, natural number, boolean, or hypothesis. induction performs structural induction and additionally provides an inductive hypothesis. 
-- cases on a natural number
example (n : ℕ) : n = 0 ∨ ∃ m, n = m + 1 := by
  cases n with
  | zero => left; rfl
  | succ m => right; exact ⟨m, rfl⟩

-- induction on ℕ
example (n : ℕ) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih => simp [Nat.add_succ, ih]

-- induction with a more complex type
example (l : List ℕ) : l.length ≥ 0 := by
  induction l with
  | nil => simp
  | cons h t ih => simp [List.length_cons]; omega
For simple induction on ℕ where the goal is arithmetic, omega or linarith can often finish the step without explicitly writing out the induction. For complex recursive structures, induction with explicit case names is clearer.

​
by_contra and by_cases

by_contra h introduces the negation of the current goal as hypothesis h and switches the goal to False, enabling proof by contradiction. by_cases h : P performs classical case analysis on any proposition P, splitting into cases P and ¬P. 
-- by_contra: proof by contradiction
example (n : ℕ) (h : n ≠ 0) : n > 0 := by
  by_contra h'
  push_neg at h'
  omega

-- by_cases: classical case split on any proposition
example (n : ℕ) : n = 0 ∨ n > 0 := by
  by_cases h : n = 0
  · left; exact h
  · right; omega

​
contrapose

contrapose replaces a goal P → Q (or P given ¬Q in context) with its contrapositive ¬Q → ¬P. Combined with push_neg, this is a standard pattern for proving implications. 
-- Switch to the contrapositive
example (n : ℕ) : n ≠ 0 → n > 0 := by
  contrapose
  push_neg
  omega

-- contrapose! = contrapose + push_neg
example (n : ℕ) : n ≠ 0 → n > 0 := by
  contrapose!
  omega

​
push_neg

push_neg pushes negations inward through quantifiers and logical connectives. It is fully covered in the Simplification Tactics page and is often used together with by_contra or contrapose. 
example (h : ¬ ∀ x : ℝ, x ^ 2 ≥ 0) : ∃ x : ℝ, x ^ 2 < 0 := by
  push_neg at h
  exact h

​
wlog

wlog reduces the goal to a canonical case. wlog h : P splits into two goals: a side goal (placed first) where you reduce the h : ¬ P case to the P case using symmetry, and a main goal where h : P is in context and you prove the goal directly. The side goal also receives this, the statement that the main goal holds whenever P holds. 
-- Prove a symmetric statement by WLOG
example (a b : ℝ) : a * b ≤ (a ^ 2 + b ^ 2) / 2 := by
  wlog h : a ≤ b
  · push_neg at h
    linarith [this b a (le_of_lt h)]
  nlinarith [sq_nonneg (a - b)]
The general form is:
wlog h : P
wlog h : P generalizing x y   -- reverts x and y before creating the side goal
wlog h : P with H              -- names the "sufficiency" hypothesis H instead of this
After wlog h : P, two goals are produced:
  1. Side goal (first): the context gains h : ¬ P and this (or H), the statement that the original goal follows from P. You must reduce the general case to the case where P holds, typically by a symmetry argument applying this with swapped arguments.
  2. Main goal: the context gains h : P and you prove the original goal under this assumption.
The generalizing x y modifier reverts x and y before constructing the side goal, so the wlog-claim this can be applied to x and y in a different order (the typical symmetry use case).This is most useful for symmetric goals (like swapping two variables) or for goals where one case implies the other by a simple transformation.

​
tfae_have and tfae_finish

tfae_have and tfae_finish prove goals of the form TFAE [P₁, P₂, ..., Pₙ] (“The Following Are Equivalent”). You establish individual implications using tfae_have i → j and then call tfae_finish to assemble them into the full equivalence. 
-- Prove a TFAE chain
example (n : ℕ) : TFAE [n = 0, n ≤ 0, ¬ n > 0] := by
  tfae_have 1 → 2 := by omega
  tfae_have 2 → 3 := by omega
  tfae_have 3 → 1 := by omega
  tfae_finish

-- With sorry placeholders while building the proof
example (p q r : Prop) : TFAE [p, q, r] := by
  tfae_have 1 → 2 := fun hp => sorry
  tfae_have 2 → 3 := fun hq => sorry
  tfae_have 3 → 1 := fun hr => sorry
  tfae_finish
TFAE requires a Hamiltonian path through the implication graph — you need enough tfae_have statements for tfae_finish to find a cycle visiting all propositions. For n propositions, n directed implications suffice if they form a cycle (1→2→3→…→n→1).

​
Quick Comparison

Goal Decomposition

constructor — split conjunctions/iffs into partscases — case-split on an inductive typercases / obtain — pattern-match a hypothesisext — reduce equality of structures to components

Witness Provision

use — provide a witness for an existentialrefine — partially fill a proof term with _apply — apply a lemma, generate subgoalsexact — close goal with a complete proof term

Classical Reasoning

by_contra — proof by contradictionby_cases — classical case split on any Propcontrapose — switch to contrapositivepush_neg — push negations inward

Advanced Structure

induction — structural inductionwlog — reduce to canonical casetfae_have / tfae_finish — equivalence chainsobtain — simultaneous destructuring

Build docs developers (and LLMs) love

Get started for freeTalk to us