Tips of Proof by Lean

In this post, we will look at some handy tactics that make proving in Lean 4 a lot smoother. We are continuing to use "Introduction to Lean Language from Scratch: Hands-on Formal Mathematics Library Development" as our learning material.

As proofs get more complex, being able to break down your goals step-by-step or quickly look up the names of lemmas you want to use becomes incredibly helpful. We will explore four tactics through concrete code examples: have, suffices, exact?, and show ... from by.

The have Tactic — Declaring Local Lemmas

The have tactic allows you to declare a local lemma in the middle of a proof and reference it by name in subsequent goals. In the following example, while proving ¬¬¬P → ¬P, we establish an intermediate local lemma ¬¬P.

example (P : Prop) : ¬¬¬ P → ¬ P := by
  intro hn3p -- ¬¬¬ P
  intro hp   -- P ⊢ False

  -- Prove a lemma for local use
  have hn2p : ¬¬ P := by
    intro hnp -- ¬ P → False
    contradiction -- Contradiction between hp and hnp

  exact hn3p hn2p

You declare a lemma using the syntax have name : type := by, and then provide its proof inside the by block. Since you can reference the proven lemma by name in the rest of the proof, this is highly effective for breaking complex proofs down into smaller, manageable steps.

The suffices Tactic — "It Suffices to Show..." Reasoning

The suffices tactic is used to express the reasoning: "If I can show X, it suffices to prove the original goal." When attacking the original goal directly is difficult, this allows you to advance the proof by routing through a more manageable proposition.

example (P : Prop) : ¬¬ (P ∨ ¬P) := by
  intro h -- ¬ (P ∨ ¬P) ⊢ False
  -- It suffices to show ¬ P
  suffices hyp : ¬ P from by
    -- Derive the original goal from ¬ P
    have : P ∨ ¬ P := by
      right
      exact hyp
    exact h this

  guard_target =⇛ ¬ P

  intro hq -- P
  have : P ∨ ¬ P := by
    left
    exact hq
  contradiction

Writing suffices hyp : ¬ P from by ... creates a two-stage structure. First, you show that "having ¬ P is enough to prove the original goal" inside the from by block, and after that, you proceed to prove ¬ P itself.

The exact? Tactic — Searching for Proof Terms in Libraries

The exact? tactic automatically searches imported libraries and local definitions for a proof term that matches the current goal. If a candidate is found, it displays a suggestion as a Try this: prompt.

example (P : Prop) : (P → True) ↔ True := by
  exact?
  -- Try this:
  -- [apply] exact imp_true_iff P

When working with large libraries like Mathlib, you often know a target theorem must exist but just don't know its exact name. In such situations, using exact? is incredibly convenient because it suggests candidates without requiring you to manually search through documentation.

show ... from by — Inline Disposable Lemmas

Using show P from by *** allows you to declare and prove a temporary, anonymous lemma inline. A good rule of thumb for choosing between this and have is the number of times you need to reference it. If you only use the lemma once, show ... from by keeps the code much cleaner.

In the following example, rw utilizes the rewriting (P → False) ↔ ¬ P exactly once, making it a perfect use case for show ... from by.

example (P Q : Prop) (h : ¬ P ↔ Q) : (P → False) ↔ Q := by
  rw [show (P → False) ↔ ¬ P from by rfl]
  rw [h]