I've been learning Lean recently. I'm fascinated by the idea of using an automated proof checker in my own mathematical study. I have, for a long time, preferred the type of mathematics that I feel I can check my work on without a solutions manual. For something like calculating an integral, I can numerically estimate some answers to see if I made some sort of egregious mistake. As such, I have avoided proofs, to my own detriment. I've been self-studying real analysis for the last year or two, so I've written a lot more proofs. But! There's always some doubt in my mind about whether I've made a subtle mistake.

Enter: Lean. Lean is a proof assistant and functional programming language that is becoming more popular in math circles. I'm learning Lean by going through How to Prove It with Lean, which accompanies How to Prove It. HTPI Lean introduces some special Lean keywords to better match the book's language, but there's an appendix for translating to standard mathlib Lean.

Here is one of the exercises I did this week out of HTPI Lean (Section 3.4 Exercise 8, which corresponds to Exercise 3.4.18(a) in HTPI). I'll first write out the proof in English, and then I'll show the Lean proof.

Theorem: Let \( \mathcal{F} \) and \( \mathcal{G} \) be families of sets. \( \bigcup \left( \mathcal{F} \cap \mathcal{G} \right) \subseteq \bigcup \mathcal{F} \cap \bigcup \mathcal{G} \).

Proof. We can prove this by showing that if \( x \) is an element of \( \bigcup \left( \mathcal{F} \cap \mathcal{G} \right) \) then it must be an element of \( \bigcup \mathcal{F} \cap \bigcup \mathcal{G} \) as well.

Let \( x \) be arbitrary and assume that \( x \in \bigcup \left( \mathcal{F} \cap \mathcal{G} \right) \). In other words, there is some set \( A \) such that \( x \in A \) and \( A \in \mathcal{F} \cap \mathcal{G} \). In order to prove that \( x \in \bigcup \mathcal{F} \cap \bigcup \mathcal{G} \), we have to separately prove that \( x \in \bigcup \mathcal{F} \) and \( x \in \bigcup \mathcal{G} \). In order for \( x \) to be in \( \bigcup \mathcal{F} \), there must be some set in \( \mathcal{F} \) that contains \( x \). Similarly for \( \bigcup \mathcal{G} \). \( A \) is such a set. \( x \in A \), and \( A \) is in both \( \mathcal{F} \) and \( \mathcal{G} \) (by the definition of the intersection). Thus, \( x \in \bigcup \mathcal{F} \cap \bigcup \mathcal{G} \).

Before we start, it's important to understand that when using Lean, there is a set of hypotheses (statements we assume are true in order to complete the proof) and a goal (the statement we would like to prove is true). The usual way to use Lean is with an interactive editor that displays the current goal state as well as all available hypotheses. The proof procedes by rewriting the goal until we can combine hypotheses to prove the goal. Simply put, if the goal at any time is p, and we have a hypothesis that proves p, the proof is complete.

Now, the Lean proof. I'll interleave my commentary and what I see in my editor with the proof.

theorem Ex_3_4_18_a (U : Type)
    (F G : (Set (Set U)))
    : ⋃₀(F ∩ G) ⊆ (⋃₀ F) ∩ (⋃₀ G)
    := by

First, we introduce the theorem we aim to prove and give it a name. We also introduce the objects we'll need for the proof. U is an unspecified type, F and G are families of sets (of type U, because we're not going to rely on the properties of the items in the set for our proof). Finally, we state our goal, and begin the proof.

  define

This is a Lean "tactic": a defined sequence of actions that transform either a hypothesis or the goal of the proof. define is actually a special tactic provided by HTPI, but there is an analogue in mathlib). define essentially rewrites the goal in a simpler form. In this case, before the define, the goal is

⊢ ⋃₀ (F ∩ G) ⊆ ⋃₀ F ∩ ⋃₀ G

(⊢ is how Lean displays what the current goal is). After the define, the goal becomes

⊢ ∀ ⦃a : U⦄, a ∈ ⋃₀ (F ∩ G) → a ∈ ⋃₀ F ∩ ⋃₀ G

This may not look simpler, but it will become clear in a moment why it is.

  fix x : U
  assume h1

This corresponds to letting x be arbitrary (which removes the "for all" quantifier above) and then assuming \( x \in \bigcup \left( \mathcal{F} \cap \mathcal{G} \right) \). In order to prove a goal of the form \( P \rightarrow Q \), we assume \( P \) is true and try to prove \( Q \). The way this affects the goal state in Lean is \( P \) becomes one of our hypotheses and \( Q \) is the new goal. Hence, here's what we see in the editor at this stage:

h1 : x ∈ ⋃₀ (F ∩ G)
⊢ x ∈ ⋃₀ F ∩ ⋃₀ G
  define; define at h1

More simplifying. define at h1 means to apply the define tactic to the h1 hypothesis instead of the goal. This could have been written on two lines, but it felt to me like they belonged together, so I combined them on the same line with a semi-colon. The new goal state is:

h1 : ∃ t ∈ F ∩ G, x ∈ t
⊢ x ∈ ⋃₀ F ∧ x ∈ ⋃₀ G
  obtain (A : _) (h2 : _) from h1

One of our hypotheses (h1) is an existential statement (it claims that some object exists). The obtain tactic fetches such an object from the aether and assigns the name A to it. A has some properties, and the existence of those properties is assigned to the hypothesis h2. The underscores are an indication that we don't have to fill out the type of A or the full statement of h2, Lean can infer it from context. Here's the new state:

h1 : ∃ t ∈ F ∩ G, x ∈ t
A : Set U
h2 : A ∈ F ∩ G ∧ x ∈ A
⊢ x ∈ ⋃₀ F ∧ x ∈ ⋃₀ G
  have h3 : _ := h2.left; define at h3

have is a tactic that produces a new hypothesis from a combination/distillation of our existing ones (essentially, it's a mini-lemma). h2.left refers to the left branch of the h2 hypothesis (which is an "and", so both of its sub-statements must be true). Here's the new state:

h1 : ∃ t ∈ F ∩ G, x ∈ t
A : Set U
h2 : A ∈ F ∩ G ∧ x ∈ A
h3 : A ∈ F ∧ A ∈ G
⊢ x ∈ ⋃₀ F ∧ x ∈ ⋃₀ G

We are almost done. Here is the next line of the proof:

  apply And.intro

Our goal statement is an "and" statement, which we can prove is true by separately proving both branches are true. This re-writes the goal in the following way:

▼ 2 goals
case left
U : Type
F G : Set (Set U)
x : U
h1 : ∃ t ∈ F ∩ G, x ∈ t
A : Set U
h2 : A ∈ F ∩ G ∧ x ∈ A
h3 : A ∈ F ∧ A ∈ G
⊢ x ∈ ⋃₀ F

case right
U : Type
F G : Set (Set U)
x : U
h1 : ∃ t ∈ F ∩ G, x ∈ t
A : Set U
h2 : A ∈ F ∩ G ∧ x ∈ A
h3 : A ∈ F ∧ A ∈ G
⊢ x ∈ ⋃₀ G

What Lean has done for us is it has split our goal into two subgoals. We will separately prove the left and right branches, and so complete the proof.

Here is the proof of the left branch:

  ·
    show _ from Exists.intro A (And.intro h3.left h2.right)
    done

The dot indicates that we are proving a subgoal. show is a tactic that proves the goal using a combination of hypothesis. The Exists.intro tactic proves an existential goal (\( x \in \bigcup \mathcal{G} \) can be re-written as \( \exists t \in \mathcal{G}, x \in t \)) by providing an object with the required properties (in this case, A). And.intro proves an "and" goal by providing proofs of both branches. In this case, h3.left is a proof that A ∈ F and h2.right is a proof that x ∈ A.

The proof of the other branch proceed in the same way, so our proof is complete. At this point, we get a 🎉 emoji in our editor indicating we've successfully proved the goal.

Here's the complete proof:

theorem Ex_3_4_18_a (U : Type)
    (F G : (Set (Set U)))
    : ⋃₀(F ∩ G) ⊆ (⋃₀ F) ∩ (⋃₀ G)
    := by

  define
  fix x : U
  assume h1
  define; define at h1
  obtain (A : _) (h2 : _) from h1
  have h3 : _ := h2.left; define at h3
  apply And.intro
  ·
    show _ from Exists.intro A (And.intro h3.left h2.right)
    done
  ·
    show _ from Exists.intro A (And.intro h3.right h2.right)
    done

  done

I really like writing Lean proofs! If you want to get into writing Lean proofs, I started by playing the Natural Number Game. It's in the browser so you don't have to install anything, and it gives you a really good mental model for how to write Lean proofs.