ホーム / Technical /

The differences between `exact`, `apply`, and `rw` in Lean

Friday, 26 June 2026

Lean Mathematics Technical

t f B! P L

Since starting to learn Lean 4, I often found myself confused about when to use exact, apply, and rw (rewrite). I decided to write this post to clear up the differences.

1. exact — Provide a proof that perfectly matches the goal

The exact tactic closes the current goal immediately by directly providing a hypothesis or a theorem whose type perfectly matches the goal.

Think of it as snapping the final piece of a puzzle perfectly into place.
  • If the type of the given expression perfectly matches the goal, the goal disappears.
  • If the type is even slightly different, it throws an error. Perfect alignment is an absolute prerequisite.
-- When you have a hypothesis h : P, and the goal is P
exact h

2. apply — Trace an implication (→) backward to move the goal one step back

The apply tactic uses a theorem or hypothesis of the form A → B (A implies B) to rewrite the goal from B to A using backward reasoning.

Think of it as replacing your goal like this: "I want to prove B. Since there is a theorem A → B, I will prove A next."
  • When the current goal matches the conclusion (B) of the theorem, it replaces the goal with the theorem's premise (A).
  • If you apply a theorem that requires multiple premises, the goal may split into multiple subgoals.
-- When you have a theorem h : P → Q, and the current goal is Q
apply h
-- The goal changes to P

3. rw / rewrite — Rewrite expressions in the goal using equalities or equivalences

The rw tactic uses a relation like A = B or A ↔ B to replace occurrences of A with B inside the goal (or inside a specific hypothesis).

Think of it as "substitution" in algebra, transforming the structure of an expression into an equivalent form.
  • By default, it rewrites from left to right (A → B).
  • To rewrite in the reverse direction (B → A), use the syntax rw [← h].
  • Unlike apply or exact, it allows you to target and rewrite **specific subexpressions** rather than the entire goal.
  • If the goal can be resolved by rfl (meaning both sides become identical) as a result of the rewrite, the goal closes automatically.
-- When you have a hypothesis h : x = y, and the current goal is x + 1 = z
rw [h]
-- x in the goal is replaced by y, changing the goal to y + 1 = z

Comparing the Three Tactics at a Glance

Tactic Shape of the Target Object Effect on the Goal Key Characteristic
exact P (the goal itself) Closes the goal on the spot Requires an exact match; throws an error if there is any mismatch.
apply A → B (Implication) Moves back the goal from B to A Reasons backward from the conclusion, turning the premise into a new target.
rw A = B / A ↔ B Rewrites A to B within the goal Can transform individual subexpressions. Use ← for reverse direction.

How to Choose When You're Stuck

  1. You have a hypothesis that looks exactly like your current goal ⇒ exact
  2. You want to use a theorem that says "if ... then it leads to my current goal" ⇒ apply
  3. You want to transform an expression using a rule that says "this equals that" ⇒ rw

By combining these three tactics effectively, you can make progress on a major portion of proofs in Lean 4. In the next post, we plan to look at concrete examples of how to orchestrate these tactics together within real theorem proving contexts.

📖 The code covered in this post is available in the following GitHub repository:

https://github.com/ringring-creator/LearnLean

Since I am currently learning, the content will be updated from time to time.

QooQ