A small pattern I noticed in Lean proofs that can be simplified using the suffices tactic.

The suffices tactic in Lean is an interesting one. It allows us to state a goal and then prove it later, which can make proofs cleaner and easier to read–mimicking the way we might write a proof in natural language.

The documentation for suffices says:

Given a main goal ctx ⊢ t, suffices h : t' from e replaces the main goal with ctx ⊢ t'…

What wasn’t clear to me at first was why we would want to do this (besides for style).

I noticed an interesting pattern: oftentimes, we know that we can close the goal by applying an existing result, but we can’t apply it directly because the goal is not in the right form.
In these cases, we usually create a new hypothesis: an equality between (a part of) the goal and what we need to perform the application.
And building this new hypothesis might be the most important part of the proof.
When we build this new hypothesis, we are creating a new goal, but for the reader, our motivation is not clear. It only becomes clear later when we use rw [hypothesis], which allows us to close the goal.

It’s in these cases that suffices becomes very useful.

Consider this artificial (but not that artificial) example. The idea is as follows: we have a finite set B of type Finset (Fin 3)—i.e., the type of finite sets containing the elements 0, 1, and 2—and we know that it contains the elements 0, 1, and 2. We want to prove that the cardinality of B is 3. (It cannot be otherwise, since it contains all the elements of Fin 3.)

One proof generated by an LLM creates a new object for which the property is easier to prove, shows that the new object is equal to B, replaces B with the new object in the goal, and then closes the goal:

example {B : Finset (Fin 3)}
    (h₀ : 0 ∈ B) (h₁ : 1 ∈ B) (h₂ : 2 ∈ B) : B.card = 3 := by
  have : B = {0, 1, 2} := by
    ext x
    fin_cases x <;> simp [h₀, h₁, h₂]
  rw [this]; exact rfl

Alternatively, to make it clearer to the reader, we can use suffices to immediately show why it is useful to create the new object: if we show that B = {0, 1, 2}, then we can close the goal directly, since the cardinality of {0, 1, 2} is known to be 3. Hence, we can focus on proving that B is equal to {0, 1, 2}:

example {B : Finset (Fin 3)}
    (h₀ : 0 ∈ B) (h₁ : 1 ∈ B) (h₂ : 2 ∈ B) : B.card = 3 := by
  suffices B = {0, 1, 2} by rw [this]; exact rfl
  show B = {0, 1, 2}
  ext x
  fin_cases x <;> simp [h₀, h₁, h₂]

As a form of code smell, I’m starting to think that operating on hypotheses is a good indication that the proof can be simplified–either by using suffices or something else. Additionally, I think that suffices helps because it allows us to avoid momentarily pushing/popping the goal stack, which can be confusing when trying to follow the proof (in contrast to have).

While writing this, I learned about fin_cases, a tactic that creates a new goal for each case of the finite type of x. In the example above, it will create three goals, one for each case of x (0, 1, and 2). Time will tell if I use it often, but it seems like a useful tactic for my Finite Geometry project.