$$ \newcommand{\setmin}{\mathbin{\backslash}} \newcommand{\symmdiff}{\bigtriangleup} $$

3  Proofs

3.1 & 3.2. Proofs Involving Negations and Conditionals

Sections 3.1 and 3.2 of How To Prove It present strategies for dealing with givens and goals involving negations and conditionals. We restate those strategies here, and explain how to use them with Lean.

Section 3.1 gives two strategies for proving a goal of the form P → Q (HTPI pp. 95, 96):

To prove a goal of the form P → Q:

1. Assume P is true and prove Q.
2. Assume Q is false and prove that P is false.

We’ve already seen how to carry out both of these strategies in Lean. For the first strategy, use the assume tactic to introduce the assumption P and assign an identifier to it; Lean will automatically set Q as the goal. We can summarize the effect of using this strategy by showing how the tactic state changes if you use the tactic assume h : P:

>> ⋮
⊢ P → Q

>> ⋮
h : P
⊢ Q

The second strategy is justified by the contrapositive law. In Lean, you can use the contrapos tactic to rewrite the goal as ¬Q → ¬P and then use the tactic assume h : ¬Q. The net effect of these two tactics is:

>> ⋮
⊢ P → Q

>> ⋮
h : ¬Q
⊢ ¬P

Section 3.2 gives two strategies for using givens of the form P → Q, with the second once again being a variation on the first based on the contrapositive law (HTPI p. 108):

To use a given of the form P → Q:

1. If you are also given P, or you can prove that P is true, then you can use this given to conclude that Q is true.
2. If you are also given ¬Q, or you can prove that Q is false, then you can use this given to conclude that P is false.

The first strategy is the modus ponens rule of inference, and we saw in the last chapter that if you have h1 : P → Q and h2 : P, then h1 h2 is a (term-mode) proof of Q; often we use this rule with the have or show tactic. For the second strategy, if you have h1 : P → Q and h2 : ¬Q, then the contrapos at h1 tactic will change h1 to h1 : ¬Q → ¬P, and then h1 h2 will be a proof of ¬P.

All of the strategies listed above for working with conditional statements as givens or goals were illustrated in examples in the last chapter.

Section 3.2 of HTPI offers two strategies for proving negative goals (HTPI pp. 101, 102):

To prove a goal of the form ¬P:

1. Reexpress the goal in some other form.
2. Use proof by contradiction: assume P is true and try to deduce a contradiction.

For the first strategy, the tactics demorgan, conditional, double_neg, and bicond_neg may be useful, and we saw how those tactics work in the last chapter. But how do you write a proof by contradiction in Lean? The answer is to use a tactic called by_contra. If the goal is ¬P, then the tactic by_contra h will introduce the assumption h : P and set the goal to be False, like this:

>> ⋮
⊢ ¬P

>> ⋮
h : P
⊢ False

In Lean, False represents a statement that is always false—that is, a contradiction, as that term is defined in Section 1.2 of HTPI. The by_contra tactic can actually be used even if the goal is not a negative statement. If the goal is a statement P that is not a negative statement, then by_contra h will initiate a proof by contradiction by introducing the assumption h : ¬P and setting the goal to be False.

You will usually complete a proof by contradiction by deducing two contradictory statements—say, h1 : Q and h2 : ¬Q. But how do you convince Lean that the proof is over? You must be able to prove the goal False from the two givens h1 and h2. There are two ways to do this. The first is based on the fact that Lean treats a statement of the form ¬Q as meaning the same thing as Q → False. This makes sense, because these statements are logically equivalent, as shown by the following truth table:

Q	¬Q	(Q	→	False)
F	T	F	T	F
T	F	T	F	F

Thinking of h2 : ¬Q as meaning h2 : Q → False, we can combine it with h1 : Q using modus ponens to deduce False. In other words, h2 h1 is a proof of False.

But there is a second way of completing the proof that it is worthwhile to know about. From contradictory statements h1 : Q and h2 : ¬Q you can validly deduce any statement. This follows from the definition of a valid argument in Section 1.1 of HTPI. According to that definition, you can validly infer a conclusion R from premises h1 : Q and h2 : ¬Q if the premises cannot both be true without the conclusion also being true. In this case, that standard is met, for the simple reason that the premises cannot both be true! (This gives part of the answer to exercise 18 in Section 1.2 of HTPI.) Thus, Lean has a rule that allows you to prove any statement from contradictory premises. If you have h1 : Q and h2 : ¬Q, then Lean will recognize absurd h1 h2 as a (term-mode) proof of any statement.

To summarize, if you have h1 : Q and h2 : ¬Q, then there are two ways to prove False. Lean will recognize h2 h1 as a proof of False, and it will recognize absurd h1 h2 as a proof of any statement, including False. Notice the difference in the order in which h1 and h2 are listed in these two proofs: In the first one, the negative statement h2 must come first, just as the conditional statement must come first in an application of modus ponens. But in a proof using absurd, the negative statement must come second.

To illustrate proof by contradiction in Lean, let’s redo our first example from the last Chapter in a different way. That example was based on Example 3.2.4 in HTPI. We’ll begin with the same first two steps, introducing two assumptions.

theorem Example_3_2_4_v2 (P Q R : Prop)
    (h : P → (Q → R)) : ¬R → (P → ¬Q) := by
  assume h2 : ¬R
  assume h3 : P
  **done::

P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
⊢ ¬Q

Now the goal is a negative statement, so we use the tactic by_contra h4 to introduce the assumption h4 : Q and set the goal to be False:

theorem Example_3_2_4_v2 (P Q R : Prop)
    (h : P → (Q → R)) : ¬R → (P → ¬Q) := by
  assume h2 : ¬R
  assume h3 : P
  by_contra h4
  **done::

P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
⊢ False

Using the givens h, h3, and h4 we can deduce first Q → R and then R by two applications of modus ponens:

theorem Example_3_2_4_v2 (P Q R : Prop)
    (h : P → (Q → R)) : ¬R → (P → ¬Q) := by
  assume h2 : ¬R
  assume h3 : P
  by_contra h4
  have h5 : Q → R := h h3
  have h6 : R := h5 h4
  **done::

P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
h5 : Q → R
h6 : R
⊢ False

Now we have a contradiction: h2 : ¬R and h6 : R. To complete the proof, we deduce False from these two givens. Either h2 h6 or absurd h6 h2 would be accepted by Lean as a proof of False:

theorem Example_3_2_4_v2 (P Q R : Prop)
    (h : P → (Q → R)) : ¬R → (P → ¬Q) := by
  assume h2 : ¬R
  assume h3 : P
  by_contra h4
  have h5 : Q → R := h h3
  have h6 : R := h5 h4
  show False from h2 h6
  done

No goals

Finally, we have two strategies for using a given that is a negative statement (HTPI pp. 105, 108):

To use a given of the form ¬P:

1. Reexpress the given in some other form.
2. If you are doing a proof by contradiction, you can achieve a contradiction by proving P, since that would contradict the given ¬P.

Of course, strategy 1 suggests the use of the demorgan, conditional, double_neg, and bicond_neg tactics, if they apply. For strategy 2, if you are doing a proof by contradiction and you have a given h : ¬P, then the tactic contradict h will set the goal to be P, which will complete the proof by contradicting h. In fact, this tactic can be used with any given; if you have a given h : P, where P is not a negative statement, then contradict h will set the goal to be ¬P. You can also follow the word contradict with a proof that is more complicated than a single identifier. For example, if you have givens h1 : P → ¬Q and h2 : P, then h1 h2 is a proof of ¬Q, so the tactic contradict h1 h2 will set the goal to be Q.

If you’re not doing a proof by contradiction, then the tactic contradict h with h' will first initiate a proof by contradiction by assuming the negation of the goal, giving that assumption the identifier h', and then it will set the goal to be the negation of the statement proven by h. In other words, contradict h with h' is shorthand for by_contra h'; contradict h.

We can illustrate this with yet another way to write the proof from Example 3.2.4. Our first three steps will be the same as last time:

theorem Example_3_2_4_v3 (P Q R : Prop)
    (h : P → (Q → R)) : ¬R → (P → ¬Q) := by
  assume h2 : ¬R
  assume h3 : P
  by_contra h4
  **done::

P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
⊢ False

Since we are now doing a proof by contradiction and the given h2 : ¬R is a negative statement, a likely way to proceed is to try to prove R, which would contradict h2. So we use the tactic contradict h2:

theorem Example_3_2_4_v3 (P Q R : Prop)
    (h : P → (Q → R)) : ¬R → (P → ¬Q) := by
  assume h2 : ¬R
  assume h3 : P
  by_contra h4
  contradict h2
  **done::

P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
⊢ R

As before, we can now prove R by combining h, h3, and h4. In fact, we could do it in one step: by modus ponens, h h3 is a proof of Q → R, and therefore, by another application of modus ponens, (h h3) h4 is a proof of R. The parentheses here are not necessary; Lean will interpret h h3 h4 as (h h3) h4, so we can complete the proof like this:

theorem Example_3_2_4_v3 (P Q R : Prop)
    (h : P → (Q → R)) : ¬R → (P → ¬Q) := by
  assume h2 : ¬R
  assume h3 : P
  by_contra h4
  contradict h2
  show R from h h3 h4
  done

No goals

You could shorten this proof slightly by replacing the lines by_contra h4 and contradict h2 with the single line contradict h2 with h4.

There is one more idea that is introduced in Section 3.2 of HTPI. The last example in that section illustrates how you can sometimes use rules of inference to work backwards. Here’s a similar example in Lean:

theorem Like_Example_3_2_5
    (U : Type) (A B C : Set U) (a : U)
    (h1 : a ∈ A) (h2 : a ∉ A \ B)
    (h3 : a ∈ B → a ∈ C) : a ∈ C := by

  **done::

U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∉ A \ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ C

The goal is a ∈ C, and the only given that even mentions C is h3 : a ∈ B → a ∈ C. If only we could prove a ∈ B, then we could apply h3, using modus ponens, to reach our goal. So it would make sense to work toward the goal of proving a ∈ B.

To get Lean to use this proof strategy, we use the tactic apply h3 _. The underscore here represents a blank to be filled in by Lean. You might think of this tactic as asking Lean the question: If we want h3 _ to be a proof of the goal a ∈ C, what do we have to put in the blank? Lean is able to figure out that the answer is: a proof of a ∈ B. So it sets the goal to be a ∈ B, since a proof of that goal, when inserted into the blank in h3 _, would prove the original goal a ∈ C:

theorem Like_Example_3_2_5
    (U : Type) (A B C : Set U) (a : U)
    (h1 : a ∈ A) (h2 : a ∉ A \ B)
    (h3 : a ∈ B → a ∈ C) : a ∈ C := by
  apply h3 _
  **done::

U : Type
A B C: Set U
a : U
h1 : a ∈ A
h2 : a ∉ A \ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B

Our situation now is very much like the one in the theorem Example_3_2_5_Simple in the previous chapter, and the rest of our proof will be similar to the proof there. The given h2 is a negative statement (a ∉ A \ B is shorthand for ¬a ∈ A \ B), so, as suggested by our first strategy for using negative givens, we reexpress it as an equivalent positive statement. Writing out the definition of set difference, h2 means ¬(a ∈ A ∧ a ∉ B), and then one of De Morgan’s laws and a conditional law allow us to rewrite it first as a ∉ A ∨ a ∈ B and then as a ∈ A → a ∈ B. Of course, we have tactics to accomplish all of these reexpressions:

theorem Like_Example_3_2_5
    (U : Type) (A B C : Set U) (a : U)
    (h1 : a ∈ A) (h2 : a ∉ A \ B)
    (h3 : a ∈ B → a ∈ C) : a ∈ C := by
  apply h3 _
  define at h2
  demorgan at h2; conditional at h2
  **done::

U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∈ A → a ∈ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B

And now it is easy to complete the proof by applying modus ponens, using h2 and h1:

theorem Like_Example_3_2_5
    (U : Type) (A B C : Set U) (a : U)
    (h1 : a ∈ A) (h2 : a ∉ A \ B)
    (h3 : a ∈ B → a ∈ C) : a ∈ C := by
  apply h3 _
  define at h2
  demorgan at h2; conditional at h2
  show a ∈ B from h2 h1
  done

No goals

We will see many more uses of the apply tactic later in this book.

Sections 3.1 and 3.2 of HTPI contain several proofs that involve algebraic reasoning. Although one can do such proofs in Lean, it requires ideas that we are not ready to introduce yet. So for the moment we will stick to proofs involving only logic and set theory.

Exercises

Fill in proofs of the following theorems. All of them are based on exercises in HTPI.

theorem Exercise_3_2_1a (P Q R : Prop)
    (h1 : P → Q) (h2 : Q → R) : P → R := by
  
  **done::

theorem Exercise_3_2_1b (P Q R : Prop)
    (h1 : ¬R → (P → ¬Q)) : P → (Q → R) := by
  
  **done::

theorem Exercise_3_2_2a (P Q R : Prop)
    (h1 : P → Q) (h2 : R → ¬Q) : P → ¬R := by
  
  **done::

theorem Exercise_3_2_2b (P Q : Prop)
    (h1 : P) : Q → ¬(Q → ¬P) := by
  
  **done::

3.3. Proofs Involving Quantifiers

In the notation used in HTPI, if \(P(x)\) is a statement about \(x\), then \(\forall x\, P(x)\) means “for all \(x\), \(P(x)\),” and \(\exists x\, P(x)\) means “there exists at least one \(x\) such that \(P(x)\).” The letter \(P\) here does not stand for a proposition; it is only when it is applied to some object \(x\) that we get a proposition. We will say that \(P\) is a predicate, and when we apply \(P\) to an object \(x\) we get the proposition \(P(x)\). You might want to think of the predicate \(P\) as representing some property that an object might have, and the proposition \(P(x)\) asserts that \(x\) has that property.

To use a predicate in Lean, you must tell Lean the type of objects to which it applies. If U is a type, then Pred U is the type of predicates that apply to objects of type U. If P has type Pred U (that is, P is a predicate applying to objects of type U) and x has type U, then to apply P to x we just write P x (with a space but no parentheses). Thus, if we have P : Pred U and x : U, then P x is an expression of type Prop. That is, P x is a proposition, and its meaning is that x has the property represented by the predicate P.

There are a few differences between the way quantified statements are written in HTPI and the way they are written in Lean. First of all, when we apply a quantifier to a variable in Lean we will specify the type of the variable explicitly. Also, Lean requires that after specifying the variable and its type, you must put a comma before the proposition to which the quantifier is applied. Thus, if P has type Pred U, then to say that P holds for all objects of type U we would write ∀ (x : U), P x. Similarly, ∃ (x : U), P x is the proposition asserting that there exists at least one x of type U such that P x.

And there is one more important difference between the way quantified statements are written in HTPI and Lean. In HTPI, a quantifier is interpreted as applying to as little as possible. Thus, \(\forall x\, P(x) \wedge Q(x)\) is interpreted as \((\forall x\, P(x)) \wedge Q(x)\); if you want the quantifier \(\forall x\) to apply to the entire statement \(P(x) \wedge Q(x)\) you must use parentheses and write \(\forall x(P(x) \wedge Q(x))\). The convention in Lean is exactly the opposite: a quantifier applies to as much as possible. Thus, Lean will interpret ∀ (x : U), P x ∧ Q x as meaning ∀ (x : U), (P x ∧ Q x). If you want the quantifier to apply to only P x, then you must use parentheses and write (∀ (x : U), P x) ∧ Q x.

With this preparation, we are ready to consider how to write proofs involving quantifiers in Lean. The most common way to prove a goal of the form ∀ (x : U), P x is to use the following strategy (HTPI p. 114):

To prove a goal of the form ∀ (x : U), P x:

Let x stand for an arbitrary object of type U and prove P x. If the letter x is already being used in the proof to stand for something, then you must choose an unused variable, say y, to stand for the arbitrary object, and prove P y.

To do this in Lean, you should use the tactic fix x : U, which tells Lean to treat x as standing for some fixed but arbitrary object of type U. This has the following effect on the tactic state:

>> ⋮
⊢ ∀ (x : U), P x

>> ⋮
x : U
⊢ P x

To use a given of the form ∀ (x : U), P x, we usually apply a rule of inference called universal instantiation, which is described by the following proof strategy (HTPI p. 121):

To use a given of the form ∀ (x : U), P x:

You may plug in any value of type U, say a, for x and use this given to conclude that P a is true.

This strategy says that if you have h : ∀ (x : U), P x and a : U, then you can infer P a. Indeed, in this situation Lean will recognize h a as a proof of P a. For example, you can write have h' : P a := h a in a Lean tactic-mode proof, and Lean will add h' : P a to the tactic state. Note that a here need not be simply a variable; it can be any expression denoting an object of type U.

Let’s try these strategies out in a Lean proof. In Lean, if you don’t want to give a theorem a name, you can simply call it an example rather than a theorem, and then there is no need to give it a name. In the following theorem, you can enter the symbol ∀ by typing \forall or \all, and you can enter ∃ by typing \exists or \ex.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x → ¬Q x)
    (h2 : ∀ (x : U), Q x) :
    ¬∃ (x : U), P x := by
  
  **done::

U : Type
P Q : Pred U
h1 : ∀ (x : U), P x → ¬Q x
h2 : ∀ (x : U), Q x
⊢ ¬∃ (x : U), P x

To use the givens h1 and h2, we will probably want to use universal instantiation. But to do that we would need an object of type U to plug in for x in h1 and h2, and there is no object of type U in the tactic state. So at this point, we can’t apply universal instantiation to h1 and h2. We should watch for an object of type U to come up in the course of the proof, and consider applying universal instantiation if one does. Until then, we turn our attention to the goal.

The goal is a negative statement, so we begin by reexpressing it as an equivalent positive statement, using a quantifier negation law. The tactic quant_neg applies a quantifier negation law to rewrite the goal. As with the other tactics for applying logical equivalences, you can write quant_neg at h if you want to apply a quantifier negation law to a given h. The effect of the tactic can be summarized as follows:

	quant_neg Tactic
¬∀ (x : U), P x	is changed to	∃ (x : U), ¬P x
¬∃ (x : U), P x	is changed to	∀ (x : U), ¬P x
∀ (x : U), P x	is changed to	¬∃ (x : U), ¬P x
∃ (x : U), P x	is changed to	¬∀ (x : U), ¬P x

Using the quant_neg tactic leads to the following result.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x → ¬Q x)
    (h2 : ∀ (x : U), Q x) :
    ¬∃ (x : U), P x := by
  quant_neg     --Goal is now ∀ (x : U), ¬P x
  **done::

U : Type
P Q : Pred U
h1 : ∀ (x : U), P x → ¬Q x
h2 : ∀ (x : U), Q x
⊢ ∀ (x : U), ¬P x

Now the goal starts with ∀, so we use the strategy above and introduce an arbitrary object of type U. Since the variable x occurs as a bound variable in several statements in this theorem, it might be best to use a different letter for the arbitrary object; this isn’t absolutely necessary, but it may help to avoid confusion. So our next tactic is fix y : U.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x → ¬Q x)
    (h2 : ∀ (x : U), Q x) :
    ¬∃ (x : U), P x := by
  quant_neg     --Goal is now ∀ (x : U), ¬P x
  fix y : U
  **done::

U : Type
P Q : Pred U
h1 : ∀ (x : U), P x → ¬Q x
h2 : ∀ (x : U), Q x
y : U
⊢ ¬P y

Now we have an object of type U in the tactic state, namely, y. So let’s try applying universal instantiation to h1 and h2 and see if it helps.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x → ¬Q x)
    (h2 : ∀ (x : U), Q x) :
    ¬∃ (x : U), P x := by
  quant_neg     --Goal is now ∀ (x : U), ¬P x
  fix y : U
  have h3 : P y → ¬Q y := h1 y
  have h4 : Q y := h2 y
  **done::

U : Type
P Q : Pred U
h1 : ∀ (x : U), P x → ¬Q x
h2 : ∀ (x : U), Q x
y : U
h3 : P y → ¬Q y
h4 : Q y
⊢ ¬P y

We’re almost done, because the goal now follows easily from h3 and h4. If we use the contrapositive law to rewrite h3 as Q y → ¬P y, then we can apply modus ponens to the rewritten h3 and h4 to reach the goal:

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x → ¬Q x)
    (h2 : ∀ (x : U), Q x) :
    ¬∃ (x : U), P x := by
  quant_neg     --Goal is now ∀ (x : U), ¬P x
  fix y : U
  have h3 : P y → ¬Q y := h1 y
  have h4 : Q y := h2 y
  contrapos at h3  --Now h3 : Q y → ¬P y
  show ¬P y from h3 h4
  done

No goals

Our next example is a theorem of set theory. You already know how to type a few set theory symbols in Lean, but you’ll need a few more for our next example. Here’s a summary of the most important set theory symbols and how to type them in Lean.

Symbol	How To Type It
∈	\in
∉	\notin or \inn
⊆	\sub
⊈	\subn
=	=
≠	\ne
∪	\union or \cup
∩	\inter or \cap
\	\\
△	\bigtriangleup
∅	\emptyset
𝒫	\powerset

With this preparation, we can turn to our next example.

example (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ∀ (x : U), x ∈ A → x ∉ B) : A ⊆ C := by
  
  **done::

U : Type
A B C : Set U
h1 : A ⊆ B ∪ C
h2 : ∀ x ∈ A, x ∉ B
⊢ A ⊆ C

Notice that in the Infoview, Lean has written h2 as ∀ x ∈ A, x ∉ B, using a bounded quantifier. As explained in Section 2.2 of HTPI (see p. 72), this is a shorter way of writing the statement ∀ (x : U), x ∈ A → x ∉ B. We begin by using the define tactic to write out the definition of the goal.

example (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ∀ (x : U), x ∈ A → x ∉ B) : A ⊆ C := by
  define  --Goal : ∀ ⦃a : U⦄, a ∈ A → a ∈ C
  **done::

U : Type
A B C: Set U
h1 : A ⊆ B ∪ C
h2 : ∀ x ∈ A, x ∉ B
⊢ ∀ ⦃a : U⦄,
>>  a ∈ A → a ∈ C

Notice that Lean’s definition of the goal starts with ∀ ⦃a : U⦄, not ∀ (a : U). Why did Lean use those funny double braces rather than parentheses? We’ll return to that question shortly. The difference doesn’t affect our next steps, which are to introduce an arbitrary object y of type U and assume y ∈ A.

example (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ∀ (x : U), x ∈ A → x ∉ B) : A ⊆ C := by
  define  --Goal : ∀ ⦃a : U⦄, a ∈ A → a ∈ C
  fix y : U
  assume h3 : y ∈ A
  **done::

U : Type
A B C : Set U
h1 : A ⊆ B ∪ C
h2 : ∀ x ∈ A, x ∉ B
y : U
h3 : y ∈ A
⊢ y ∈ C

Now we can combine h2 and h3 to conclude that y ∉ B. Since we have y : U, by universal instantiation, h2 y is a proof of y ∈ A → y ∉ B, and therefore by modus ponens, h2 y h3 is a proof of y ∉ B.

example (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ∀ (x : U), x ∈ A → x ∉ B) : A ⊆ C := by
  define  --Goal : ∀ ⦃a : U⦄, a ∈ A → a ∈ C
  fix y : U
  assume h3 : y ∈ A
  have h4 : y ∉ B := h2 y h3
  **done::

U : Type
A B C : Set U
h1 : A ⊆ B ∪ C
h2 : ∀ x ∈ A, x ∉ B
y : U
h3 : y ∈ A
h4 : y ∉ B
⊢ y ∈ C

We should be able to use similar reasoning to combine h1 and h3, if we first write out the definition of h1.

example (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ∀ (x : U), x ∈ A → x ∉ B) : A ⊆ C := by
  define  --Goal : ∀ ⦃a : U⦄, a ∈ A → a ∈ C
  fix y : U
  assume h3 : y ∈ A
  have h4 : y ∉ B := h2 y h3
  define at h1  --h1 : ∀ ⦃a : U⦄, a ∈ A → a ∈ B ∪ C
  **done::

U : Type
A B C : Set U
h1 : ∀ ⦃a : U⦄,
>>  a ∈ A → a ∈ B ∪ C
h2 : ∀ x ∈ A, x ∉ B
y : U
h3 : y ∈ A
h4 : y ∉ B
⊢ y ∈ C

Once again, Lean has used double braces to define h1, and now we are ready to explain what they mean. If the definition had been h1 : ∀ (a : U), a ∈ A → a ∈ B ∪ C, then exactly as in the previous step, h1 y h3 would be a proof of y ∈ B ∪ C. The use of double braces in the definition h1 : ∀ ⦃a : U⦄, a ∈ A → a ∈ B ∪ C means that you don’t need to tell Lean that y is being plugged in for a in the universal instantiation step; Lean will figure that out on its own. Thus, you can just write h1 h3 as a proof of y ∈ B ∪ C. Indeed, if you write h1 y h3 then you will get an error message, because Lean expects not to be told what to plug in for a. You might think of the definition of h1 as meaning h1 : _ ∈ A → _ ∈ B ∪ C, where the blanks can be filled in with anything of type U (with the same thing being put in both blanks). When you ask Lean to apply modus ponens by combining this statement with h3 : y ∈ A, Lean figures out that in order for modus ponens to apply, the blanks must be filled in with y.

In this situation, the a in h1 is called an implicit argument. What this means is that, when h1 is applied to make an inference in a proof, the value to be assigned to a is not specified explicitly; rather, the value is inferred by Lean. We will see many more examples of implicit arguments later in this book. In fact, there are two slightly different kinds of implicit arguments in Lean. One kind is indicated using the double braces ⦃ ⦄ used in this example, and the other is indicated using curly braces, { }. The difference between these two kinds of implicit arguments won’t be important in this book; all that will matter to us is that if you see either ∀ ⦃a : U⦄ or ∀ {a : U} rather than ∀ (a : U), then you must remember that a is an implicit argument.

example (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ∀ (x : U), x ∈ A → x ∉ B) : A ⊆ C := by
  define  --Goal : ∀ ⦃a : U⦄, a ∈ A → a ∈ C
  fix y : U
  assume h3 : y ∈ A
  have h4 : y ∉ B := h2 y h3
  define at h1  --h1 : ∀ ⦃a : U⦄, a ∈ A → a ∈ B ∪ C
  have h5 : y ∈ B ∪ C := h1 h3
  **done::

U : Type
A B C : Set U
h1 : ∀ ⦃a : U⦄,
>>  a ∈ A → a ∈ B ∪ C
h2 : ∀ x ∈ A, x ∉ B
y : U
h3 : y ∈ A
h4 : y ∉ B
h5 : y ∈ B ∪ C
⊢ y ∈ C

If Lean was able to figure out that y should be plugged in for a in h1 in this step, couldn’t it have figured out that y should be plugged in for x in h2 in the previous have step? The answer is yes. Of course, in h2, x was not an implicit argument, so Lean wouldn’t automatically figure out what to plug in for x. But we could have asked it to figure it out by writing the proof in the previous step as h2 _ h3 rather than h2 y h3. In a term-mode proof, an underscore represents a blank to be filled in by Lean. Try changing the earlier step of the proof to have h4 : y ∉ B := h2 _ h3 and you will see that Lean will accept it. Of course, in this case this doesn’t save us any typing, but in some situations it is useful to let Lean figure out some part of a proof.

Lean’s ability to fill in blanks in term-mode proofs is limited. For example, if you try changing the previous step to have h4 : y ∉ B := h2 y _, you’ll get a red squiggle under the blank, and the error message in the Infoview pane will say don't know how to synthesize placeholder. In other words, Lean was unable to figure out how to fill in the blank in this case. In future proofs you might try replacing some expressions with blanks to get a feel for what Lean can and cannot figure out for itself.

Continuing with the proof, we see that we’re almost done, because we can combine h4 and h5 to reach our goal. To see how, we first write out the definition of h5.

example (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ∀ (x : U), x ∈ A → x ∉ B) : A ⊆ C := by
  define  --Goal : ∀ ⦃a : U⦄, a ∈ A → a ∈ C
  fix y : U
  assume h3 : y ∈ A
  have h4 : y ∉ B := h2 y h3
  define at h1  --h1 : ∀ ⦃a : U⦄, a ∈ A → a ∈ B ∪ C
  have h5 : y ∈ B ∪ C := h1 h3
  define at h5  --h5 : y ∈ B ∨ y ∈ C
  **done::

U : Type
A B C : Set U
h1 : ∀ ⦃a : U⦄,
>>  a ∈ A → a ∈ B ∪ C
h2 : ∀ x ∈ A, x ∉ B
y : U
h3 : y ∈ A
h4 : y ∉ B
h5 : y ∈ B ∨ y ∈ C
⊢ y ∈ C

A conditional law will convert h5 to y ∉ B → y ∈ C, and then modus ponens with h4 will complete the proof.

example (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ∀ (x : U), x ∈ A → x ∉ B) : A ⊆ C := by
  define  --Goal : ∀ ⦃a : U⦄, a ∈ A → a ∈ C
  fix y : U
  assume h3 : y ∈ A
  have h4 : y ∉ B := h2 y h3
  define at h1  --h1 : ∀ ⦃a : U⦄, a ∈ A → a ∈ B ∪ C
  have h5 : y ∈ B ∪ C := h1 h3
  define at h5  --h5 : y ∈ B ∨ y ∈ C
  conditional at h5  --h5 : y ∉ B → y ∈ C
  show y ∈ C from h5 h4
  done

No goals

Next we turn to strategies for working with existential quantifiers (HTPI p. 118).

To prove a goal of the form ∃ (x : U), P x:

Find a value of x, say a, for which you think P a is true, and prove P a.

This strategy is based on the fact that if you have a : U and h : P a, then you can infer ∃ (x : U), P x. Indeed, in this situation the expression Exists.intro a h is a Lean term-mode proof of ∃ (x : U), P x. The name Exists.intro indicates that this is a rule for introducing an existential quantifier.

Note that, as with the universal instantiation rule, a here can be any expression denoting an object of type U; it need not be simply a variable. For example, if A and B have type Set U, F has type Set (Set U), and you have a given h : A ∪ B ∈ F, then Exists.intro (A ∪ B) h is a proof of ∃ (x : Set U), x ∈ F.

As suggested by the strategy above, we will often want to use the Exists.intro rule in situations in which our goal is ∃ (x : U), P x and we have an object a of type U that we think makes P a true, but we don’t yet have a proof of P a. In that situation we can use the tactic apply Exists.intro a _. Recall that the apply tactic asks Lean to figure out what to put in the blank to turn Exists.intro a _ into a proof of the goal. Lean will figure out that what needs to go in the blank is a proof of P a, so it sets P a to be the goal. In other words, the tactic apply Exists.intro a _ has the following effect on the tactic state:

>> ⋮
a : U
⊢ ∃ (x : U), P x

>> ⋮
a : U
⊢ P a

Our strategy for using an existential given is a rule that is called existential instantiation in HTPI (HTPI p. 120):

To use a given of the form ∃ (x : U), P x:

Introduce a new variable, say u, into the proof to stand for an object of type U for which P u is true.

Suppose that, in a Lean proof, you have h : ∃ (x : U), P x. To apply the existential instantiation rule, you would use the tactic obtain (u : U) (h' : P u) from h. This tactic introduces into the tactic state both a new variable u of type U and also the identifier h' for the new given P u. Note that h can be any proof of a statement of the form ∃ (x : U), P x; it need not be just a single identifier.

Often, if your goal is an existential statement ∃ (x : U), P x, you won’t be able to use the strategy above for existential goals right away, because you won’t know what object a to use in the tactic apply Exists.intro a _. You may have to wait until a likely candidate for a pops up in the course of the proof. On the other hand, it is usually best to use the obtain tactic right away if you have an existential given. This is illustrated in our next example.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), ∃ (y : U), P x → ¬ Q y)
    (h2 : ∃ (x : U), ∀ (y : U), P x → Q y) :
    ∃ (x : U), ¬P x := by
  
  **done::

U : Type
P Q : Pred U
h1 : ∀ (x : U), ∃ (y : U),
>>  P x → ¬Q y
h2 : ∃ (x : U), ∀ (y : U),
>>  P x → Q y
⊢ ∃ (x : U), ¬P x

The goal is the existential statement ∃ (x : U), ¬P x, and our strategy for existential goals says that we should try to find an object a of type U that we think would make the statement ¬P a true. But we don’t have any objects of type U in the tactic state, so it looks like we can’t use that strategy yet. Similarly, we can’t use the given h1 yet, since we have nothing to plug in for x in h1. However, h2 is an existential given, and we can use it right away.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), ∃ (y : U), P x → ¬ Q y)
    (h2 : ∃ (x : U), ∀ (y : U), P x → Q y) :
    ∃ (x : U), ¬P x := by
  obtain (a : U)
    (h3 : ∀ (y : U), P a → Q y) from h2
  **done::

U : Type
P Q : Pred U
h1 : ∀ (x : U), ∃ (y : U),
>>  P x → ¬Q y
h2 : ∃ (x : U), ∀ (y : U),
>>  P x → Q y
a : U
h3 : ∀ (y : U), P a → Q y
⊢ ∃ (x : U), ¬P x

Now that we have a : U, we can apply universal instantiation to h1, plugging in a for x.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), ∃ (y : U), P x → ¬ Q y)
    (h2 : ∃ (x : U), ∀ (y : U), P x → Q y) :
    ∃ (x : U), ¬P x := by
  obtain (a : U)
    (h3 : ∀ (y : U), P a → Q y) from h2
  have h4 : ∃ (y : U), P a → ¬ Q y := h1 a
  **done::

U : Type
P Q : Pred U
h1 : ∀ (x : U), ∃ (y : U),
>>  P x → ¬Q y
h2 : ∃ (x : U), ∀ (y : U),
>>  P x → Q y
a : U
h3 : ∀ (y : U), P a → Q y
h4 : ∃ (y : U), P a → ¬Q y
⊢ ∃ (x : U), ¬P x

By the way, this is another case in which Lean could have figured out a part of the proof on its own. Try changing h1 a in the last step to h1 _, and you’ll see that Lean will be able to figure out how to fill in the blank.

Our new given h4 is another existential statement, so again we use it right away to introduce another object of type U. Since this object might not be the same as a, we must give it a different name. (Indeed, if you try to use the name a again, Lean will give you an error message.)

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), ∃ (y : U), P x → ¬ Q y)
    (h2 : ∃ (x : U), ∀ (y : U), P x → Q y) :
    ∃ (x : U), ¬P x := by
  obtain (a : U)
    (h3 : ∀ (y : U), P a → Q y) from h2
  have h4 : ∃ (y : U), P a → ¬ Q y := h1 a
  obtain (b : U) (h5 : P a → ¬ Q b) from h4
  **done::

U : Type
P Q : Pred U
h1 : ∀ (x : U), ∃ (y : U),
>>  P x → ¬Q y
h2 : ∃ (x : U), ∀ (y : U),
>>  P x → Q y
a : U
h3 : ∀ (y : U), P a → Q y
h4 : ∃ (y : U), P a → ¬Q y
b : U
h5 : P a → ¬Q b
⊢ ∃ (x : U), ¬P x

We have not yet used h3. We could plug in either a or b for y in h3, but a little thought should show you that plugging in b is more useful.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), ∃ (y : U), P x → ¬ Q y)
    (h2 : ∃ (x : U), ∀ (y : U), P x → Q y) :
    ∃ (x : U), ¬P x := by
  obtain (a : U)
    (h3 : ∀ (y : U), P a → Q y) from h2
  have h4 : ∃ (y : U), P a → ¬ Q y := h1 a
  obtain (b : U) (h5 : P a → ¬ Q b) from h4
  have h6 : P a → Q b := h3 b
  **done::

U : Type
P Q : Pred U
h1 : ∀ (x : U), ∃ (y : U),
>>  P x → ¬Q y
h2 : ∃ (x : U), ∀ (y : U),
>>  P x → Q y
a : U
h3 : ∀ (y : U), P a → Q y
h4 : ∃ (y : U), P a → ¬Q y
b : U
h5 : P a → ¬Q b
h6 : P a → Q b
⊢ ∃ (x : U), ¬P x

Now look at h5 and h6. They show that P a leads to contradictory conclusions, ¬Q b and Q b. This means that P a must be false. We finally know what value of x to use to prove the goal.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), ∃ (y : U), P x → ¬ Q y)
    (h2 : ∃ (x : U), ∀ (y : U), P x → Q y) :
    ∃ (x : U), ¬P x := by
  obtain (a : U)
    (h3 : ∀ (y : U), P a → Q y) from h2
  have h4 : ∃ (y : U), P a → ¬ Q y := h1 a
  obtain (b : U) (h5 : P a → ¬ Q b) from h4
  have h6 : P a → Q b := h3 b
  apply Exists.intro a _
  **done::

U : Type
P Q : Pred U
h1 : ∀ (x : U), ∃ (y : U),
>>  P x → ¬Q y
h2 : ∃ (x : U), ∀ (y : U),
>>  P x → Q y
a : U
h3 : ∀ (y : U), P a → Q y
h4 : ∃ (y : U), P a → ¬Q y
b : U
h5 : P a → ¬Q b
h6 : P a → Q b
⊢ ¬P a

Since the goal is now a negative statement that cannot be reexpressed as a positive statement, we use proof by contradiction.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), ∃ (y : U), P x → ¬ Q y)
    (h2 : ∃ (x : U), ∀ (y : U), P x → Q y) :
    ∃ (x : U), ¬P x := by
  obtain (a : U)
    (h3 : ∀ (y : U), P a → Q y) from h2
  have h4 : ∃ (y : U), P a → ¬ Q y := h1 a
  obtain (b : U) (h5 : P a → ¬ Q b) from h4
  have h6 : P a → Q b := h3 b
  apply Exists.intro a _
  by_contra h7
  **done::

U : Type
P Q : Pred U
h1 : ∀ (x : U), ∃ (y : U),
>>  P x → ¬Q y
h2 : ∃ (x : U), ∀ (y : U),
>>  P x → Q y
a : U
h3 : ∀ (y : U), P a → Q y
h4 : ∃ (y : U), P a → ¬Q y
b : U
h5 : P a → ¬Q b
h6 : P a → Q b
h7 : P a
⊢ False

Now h5 h7 is a proof of ¬Q b and h6 h7 is a proof of Q b, so h5 h7 (h6 h7) is a proof of False.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), ∃ (y : U), P x → ¬ Q y)
    (h2 : ∃ (x : U), ∀ (y : U), P x → Q y) :
    ∃ (x : U), ¬P x := by
  obtain (a : U)
    (h3 : ∀ (y : U), P a → Q y) from h2
  have h4 : ∃ (y : U), P a → ¬ Q y := h1 a
  obtain (b : U) (h5 : P a → ¬ Q b) from h4
  have h6 : P a → Q b := h3 b
  apply Exists.intro a _
  by_contra h7
  show False from h5 h7 (h6 h7)
  done

No goals

We conclude this section with the theorem from Example 3.3.5 in HTPI. That theorem concerns a union of a family of sets. In HTPI, such a union is written using a large union symbol, \(\bigcup\). Lean uses the symbol ⋃₀, which is entered by typing \U0 (that is, backslash–capital U–zero). For an intersection of a family of sets, Lean uses ⋂₀, typed as \I0.

theorem Example_3_3_5 (U : Type) (B : Set U)
    (F : Set (Set U)) : ⋃₀ F ⊆ B → F ⊆ 𝒫 B := by
  
  **done::

U : Type
B : Set U
F : Set (Set U)
⊢ ⋃₀ F ⊆ B → F ⊆ 𝒫 B

Note that F has type Set (Set U), which means that it is a set whose elements are sets of objects of type U. Since the goal is a conditional statement, we assume the antecedent and set the consequent as our goal. We’ll also write out the definition of the new goal.

theorem Example_3_3_5 (U : Type) (B : Set U)
    (F : Set (Set U)) : ⋃₀ F ⊆ B → F ⊆ 𝒫 B := by
  assume h1 : ⋃₀ F ⊆ B
  define
  **done::

U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
⊢ ∀ ⦃a : Set U⦄,
>>  a ∈ F → a ∈ 𝒫 B

Based on the form of the goal, we introduce an arbitrary object x of type Set U and assume x ∈ F. The new goal will be x ∈ 𝒫 B. The define tactic works out that this means x ⊆ B, which can be further expanded to ∀ ⦃a : U⦄, a ∈ x → a ∈ B.

theorem Example_3_3_5 (U : Type) (B : Set U)
    (F : Set (Set U)) : ⋃₀ F ⊆ B → F ⊆ 𝒫 B := by
  assume h1 : ⋃₀ F ⊆ B
  define
  fix x : Set U
  assume h2 : x ∈ F
  define
  **done::

U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
⊢ ∀ ⦃a : U⦄,
>>  a ∈ x → a ∈ B

Once again the form of the goal dictates our next steps: introduce an arbitrary y of type U and assume y ∈ x.

theorem Example_3_3_5 (U : Type) (B : Set U)
    (F : Set (Set U)) : ⋃₀ F ⊆ B → F ⊆ 𝒫 B := by
  assume h1 : ⋃₀ F ⊆ B
  define
  fix x : Set U
  assume h2 : x ∈ F
  define
  fix y : U
  assume h3 : y ∈ x
  **done::

U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ B

The goal can be analyzed no further, so we turn to the givens. We haven’t used h1 yet. To see how to use it, we write out its definition.

theorem Example_3_3_5 (U : Type) (B : Set U)
    (F : Set (Set U)) : ⋃₀ F ⊆ B → F ⊆ 𝒫 B := by
  assume h1 : ⋃₀ F ⊆ B
  define
  fix x : Set U
  assume h2 : x ∈ F
  define
  fix y : U
  assume h3 : y ∈ x
  define at h1
  **done::

U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄,
>>  a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ B

Now we see that we can try to use h1 to reach our goal. Indeed, h1 _ would be a proof of the goal if we could fill in the blank with a proof of y ∈ ∪₀F. So we use the apply h1 _ tactic.

theorem Example_3_3_5 (U : Type) (B : Set U)
    (F : Set (Set U)) : ⋃₀ F ⊆ B → F ⊆ 𝒫 B := by
  assume h1 : ⋃₀ F ⊆ B
  define
  fix x : Set U
  assume h2 : x ∈ F
  define
  fix y : U
  assume h3 : y ∈ x
  define at h1
  apply h1 _
  **done::

U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄,
>>  a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ ⋃₀ F

Once again we have a goal that can be analyzed by using the define tactic.

theorem Example_3_3_5 (U : Type) (B : Set U)
    (F : Set (Set U)) : ⋃₀ F ⊆ B → F ⊆ 𝒫 B := by
  assume h1 : ⋃₀ F ⊆ B
  define
  fix x : Set U
  assume h2 : x ∈ F
  define
  fix y : U
  assume h3 : y ∈ x
  define at h1
  apply h1 _
  define
  **done::

U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄,
>>  a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ ∃ t ∈ F, y ∈ t

Our goal now is ∃ (t : Set U), t ∈ F ∧ y ∈ t, although once again Lean has used a bounded quantifier to write this in a shorter form. So we look for a value of t that will make the statement t ∈ F ∧ y ∈ t true. The givens h2 and h3 tell us that x is such a value, so as described earlier our next tactic should be apply Exists.intro x _.

theorem Example_3_3_5 (U : Type) (B : Set U)
    (F : Set (Set U)) : ⋃₀ F ⊆ B → F ⊆ 𝒫 B := by
  assume h1 : ⋃₀ F ⊆ B
  define
  fix x : Set U
  assume h2 : x ∈ F
  define
  fix y : U
  assume h3 : y ∈ x
  define at h1
  apply h1 _
  define
  apply Exists.intro x _
  **done::

U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄,
>>  a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ x ∈ F ∧ y ∈ x

Clearly the goal now follows from h2 and h3, but how do we write the proof in Lean? Since we need to introduce the “and” symbol ∧, you shouldn’t be surprised to learn that the rule we need is called And.intro. Proof strategies for statements involving “and” will be the subject of the next section.

theorem Example_3_3_5 (U : Type) (B : Set U)
    (F : Set (Set U)) : ⋃₀ F ⊆ B → F ⊆ 𝒫 B := by
  assume h1 : ⋃₀ F ⊆ B
  define
  fix x : Set U
  assume h2 : x ∈ F
  define
  fix y : U
  assume h3 : y ∈ x
  define at h1
  apply h1 _
  define
  apply Exists.intro x _
  show x ∈ F ∧ y ∈ x from And.intro h2 h3
  done

No goals

You might want to compare the Lean proof above to the way the proof was written in HTPI. Here are the theorem and proof from HTPI (HTPI p. 125):

Suppose \(B\) is a set and \(\mathcal{F}\) is a family of sets. If \(\bigcup\mathcal{F} \subseteq B\) then \(\mathcal{F} \subseteq \mathscr{P}(B)\).

Proof. Suppose \(\bigcup \mathcal{F} \subseteq B\). Let \(x\) be an arbitrary element of \(\mathcal{F}\). Let \(y\) be an arbitrary element of \(x\). Since \(y \in x\) and \(x \in \mathcal{F}\), by the definition of \(\bigcup \mathcal{F}\), \(y \in \bigcup \mathcal{F}\). But then since \(\bigcup \mathcal{F} \subseteq B\), \(y \in B\). Since \(y\) was an arbitrary element of \(x\), we can conclude that \(x \subseteq B\), so \(x \in \mathscr{P}(B)\). But \(x\) was an arbitrary element of \(\mathcal{F}\), so this shows that \(\mathcal{F} \subseteq \mathscr{P}(B)\), as required.  □

Exercises

theorem Exercise_3_3_1
    (U : Type) (P Q : Pred U) (h1 : ∃ (x : U), P x → Q x) :
    (∀ (x : U), P x) → ∃ (x : U), Q x := by
  
  **done::

theorem Exercise_3_3_8 (U : Type) (F : Set (Set U)) (A : Set U)
    (h1 : A ∈ F) : A ⊆ ⋃₀ F := by
  
  **done::

theorem Exercise_3_3_9 (U : Type) (F : Set (Set U)) (A : Set U)
    (h1 : A ∈ F) : ⋂₀ F ⊆ A := by
  
  **done::

theorem Exercise_3_3_10 (U : Type) (B : Set U) (F : Set (Set U))
    (h1 : ∀ (A : Set U), A ∈ F → B ⊆ A) : B ⊆ ⋂₀ F := by
  
  **done::

theorem Exercise_3_3_13 (U : Type)
    (F G : Set (Set U)) : F ⊆ G → ⋂₀ G ⊆ ⋂₀ F := by
  
  **done::

3.4. Proofs Involving Conjunctions and Biconditionals

The strategies in HTPI for working with conjunctions are very simple (HTPI p. 130).

To prove a goal of the form P ∧ Q:

Prove P and Q separately.

We already saw an example, at the end of the last section, of the use of the rule And.intro to prove a conjunction. In general, if you have h1 : P and h2 : Q, then And.intro h1 h2 is a proof of P ∧ Q. It follows that if your goal is P ∧ Q but you don’t yet have proofs of P and Q, then you can use the tactic apply And.intro _ _. Lean will figure out that the blanks need to be filled in with proofs of P and Q, so it will ask you to prove P and Q separately, as suggested by the strategy above.

If you already have a proof of either P or Q, then you can fill in one of the blanks in the apply tactic. For example, if you have h : P, then you can write apply And.intro h _, and Lean will tell you that you just have to prove Q to complete the proof. Similarly, if you have h : Q, then apply And.intro _ h will lead to just the single goal P. There is also a shortcut you can use with the apply tactic: any blanks that come at the end of the tactic can be left out. So instead of apply And.intro _ _, you can just write apply And.intro, and instead of apply And.intro h _, you can write apply And.intro h. On the other hand, apply And.intro _ h can’t be shortened; it is only blanks at the end that can be left out.

The strategy for a given that is a conjunction is similar (HTPI p. 131).

To use a given of the form P ∧ Q:

Treat this as two separate givens: P, and Q.

If you have a given h : P ∧ Q, then Lean will recognize h.left as a proof of P, and h.right as a proof of Q.

Here’s an example that illustrates these strategies. It is similar to Example 3.4.1 in HTPI

theorem Like_Example_3_4_1 (U : Type)
    (A B C D : Set U) (h1 : A ⊆ B)
    (h2 : ¬∃ (c : U), c ∈ C ∩ D) :
    A ∩ C ⊆ B \ D := by
  
  **done::

U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ (c : U), c ∈ C ∩ D
⊢ A ∩ C ⊆ B \ D

The define tactic will rewrite the goal as ∀ ⦃a : U⦄, a ∈ A ∩ C → a ∈ B \ D, and then we can introduce an arbitrary x : U and assume x ∈ A ∩ C.

theorem Like_Example_3_4_1 (U : Type)
    (A B C D : Set U) (h1 : A ⊆ B)
    (h2 : ¬∃ (c : U), c ∈ C ∩ D) :
    A ∩ C ⊆ B \ D := by
  define
  fix x : U
  assume h3 : x ∈ A ∩ C
  **done::

U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ (c : U), c ∈ C ∩ D
x : U
h3 : x ∈ A ∩ C
⊢ x ∈ B \ D

Now let’s take a look at the definitions of h3 and the goal:

theorem Like_Example_3_4_1 (U : Type)
    (A B C D : Set U) (h1 : A ⊆ B)
    (h2 : ¬∃ (c : U), c ∈ C ∩ D) :
    A ∩ C ⊆ B \ D := by
  define
  fix x : U
  assume h3 : x ∈ A ∩ C
  define at h3; define
  **done::

U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ (c : U), c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B ∧ x ∉ D

Since the goal is now a conjunction, we apply the strategy above by using the tactic apply And.intro.

theorem Like_Example_3_4_1 (U : Type)
    (A B C D : Set U) (h1 : A ⊆ B)
    (h2 : ¬∃ (c : U), c ∈ C ∩ D) :
    A ∩ C ⊆ B \ D := by
  define
  fix x : U
  assume h3 : x ∈ A ∩ C
  define at h3; define
  apply And.intro
  **done::

case left
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ (c : U), c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B
case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ (c : U), c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∉ D

Look carefully at the tactic state. Lean has listed two goals, one after the other, and it has helpfully labeled them “case left” and “case right,” indicating that the first goal is to prove the left side of the conjunction and the second is to prove the right. The given information in both cases is the same, but in the first case the goal is x ∈ B, and in the second it is x ∉ D. At this point, if we simply continue with the proof, Lean will interpret our tactics as applying to the first goal, until we achieve that goal. Once we achieve it, Lean will move on to the second goal.

However, we can make our proof more readable by separating and labeling the proofs of the two goals. To do this, we type a bullet (which looks like this: ·) and then a comment describing the first goal. (To type a bullet, type \.—that is, backslash–period.) The proof of the first goal will appear below this line, indented further and ending with done. To prepare for this, we leave a blank line, type tab to increase the indenting, and then type done. Then we do the same for the second goal: on the next line, we return to the previous level of indenting and type a bullet and a comment describing the second goal. We follow this with a blank line and then an indented done to indicate the end of the proof of the second goal. We’re going to work on the first goal first, so we click on the first blank line to position the cursor there. The screen now looks like this:

theorem Like_Example_3_4_1 (U : Type)
    (A B C D : Set U) (h1 : A ⊆ B)
    (h2 : ¬∃ (c : U), c ∈ C ∩ D) :
    A ∩ C ⊆ B \ D := by
  define
  fix x : U
  assume h3 : x ∈ A ∩ C
  define at h3; define
  apply And.intro
  · -- Proof that x ∈ B

    **done::
  · -- Proof that x ∉ D

    **done::
  done

case left
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ (c : U), c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B

Of course, there are red squiggles under both new occurrences of done, since neither goal has yet been achieved. We can work on the goals in either order by positioning the cursor on either blank line, and the Infoview pane will show the tactic state for the goal at the position of the cursor. In the display above, we have positioned the cursor on the first blank line, so the Infoview shows the tactic state for the first goal.

This first goal is easy: We have h1 : A ⊆ B and, as explained above, h3.left : x ∈ A. As we have seen in several previous examples, the tactic define at h1 will rewrite h1 as ∀ ⦃a : U⦄, a ∈ A → a ∈ B, and then h1 h3.left will be a proof of x ∈ B. And now we’ll let you in on a little secret: usually the define tactic isn’t really necessary. You may find the define tactic to be useful in many situations, because it helps you see what a statement means. But Lean doesn’t need to be told to work out what the statement means; it will do that automatically. So we can skip the define tactic and just give h1 h3.left as a proof of x ∈ B. In general, if you have h1 : A ⊆ B and h2 : x ∈ A, then Lean will recognize h1 h2 as a proof of x ∈ B. Thus, the tactic show x ∈ B from h1 h3.left will complete the first goal. Once we type this (indented to the same position as the done for the first goal), the red squiggle disappears from the first done, and the tactic state shows the No goals message. If we then click on the blank line for the second goal, the Infoview pane shows the tactic state for that goal:

theorem Like_Example_3_4_1 (U : Type)
    (A B C D : Set U) (h1 : A ⊆ B)
    (h2 : ¬∃ (c : U), c ∈ C ∩ D) :
    A ∩ C ⊆ B \ D := by
  define
  fix x : U
  assume h3 : x ∈ A ∩ C
  define at h3; define
  apply And.intro
  · -- Proof that x ∈ B:
    show x ∈ B from h1 h3.left
    done
  · -- Proof that x ∉ D

    **done::
  done

case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ (c : U), c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∉ D

The second goal is a negative statement, and the given h2 is also a negative statement. This suggests using proof by contradiction, and achieving the contradiction by contradicting h2.

theorem Like_Example_3_4_1 (U : Type)
    (A B C D : Set U) (h1 : A ⊆ B)
    (h2 : ¬∃ (c : U), c ∈ C ∩ D) :
    A ∩ C ⊆ B \ D := by
  define
  fix x : U
  assume h3 : x ∈ A ∩ C
  define at h3; define
  apply And.intro
  · -- Proof that x ∈ B.
    show x ∈ B from h1 h3.left
    done
  · -- Proof that x ∉ D.
    contradict h2 with h4
    **done::
  done

case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ (c : U), c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
h4 : x ∈ D
⊢ ∃ (c : U), c ∈ C ∩ D

The goal is now an existential statement, and looking at h3 and h4 it is clear that the right value to plug in for c in the goal is x. The tactic apply Exists.intro x will change the goal to x ∈ C ∩ D (we have again left off the unnecessary blank at the end of the apply tactic).

theorem Like_Example_3_4_1 (U : Type)
    (A B C D : Set U) (h1 : A ⊆ B)
    (h2 : ¬∃ (c : U), c ∈ C ∩ D) :
    A ∩ C ⊆ B \ D := by
  define
  fix x : U
  assume h3 : x ∈ A ∩ C
  define at h3; define
  apply And.intro
  · -- Proof that x ∈ B.
    show x ∈ B from h1 h3.left
    done
  · -- Proof that x ∉ D.
    contradict h2 with h4
    apply Exists.intro x
    **done::
  done

case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ (c : U), c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
h4 : x ∈ D
⊢ x ∈ C ∩ D

The define tactic would now rewrite the goal as x ∈ C ∧ x ∈ D, and we could prove this goal by combining h3.right and h4, using the And.intro rule. But since we know what the result of the define tactic will be, there is really no need to use it. We can just use And.intro right away to complete the proof.

theorem Like_Example_3_4_1 (U : Type)
    (A B C D : Set U) (h1 : A ⊆ B)
    (h2 : ¬∃ (c : U), c ∈ C ∩ D) :
    A ∩ C ⊆ B \ D := by
  define
  fix x : U
  assume h3 : x ∈ A ∩ C
  define at h3; define
  apply And.intro
  · -- Proof that x ∈ B.
    show x ∈ B from h1 h3.left
    done
  · -- Proof that x ∉ D.
    contradict h2 with h4
    apply Exists.intro x
    show x ∈ C ∩ D from And.intro h3.right h4
    done
  done

No goals

Since P ↔︎ Q is shorthand for (P → Q) ∧ (Q → P), the strategies given above for conjunctions lead immediately to the following strategies for biconditionals (HTPI p. 132):

To prove a goal of the form P ↔︎ Q:

Prove P → Q and Q → P separately.

To use a given of the form P ↔︎ Q:

Treat this as two separate givens: P → Q, and Q → P.

The methods for using these strategies in Lean are similar to those we used above for conjunctions. If we have h1 : P → Q and h2 : Q → P, then Iff.intro h1 h2 is a proof of P ↔︎ Q. Thus, if the goal is P ↔︎ Q, then the tactic apply Iff.intro _ _ will convert this into two separate goals, P → Q and Q → P. Once again, you can fill in one of these blanks if you already have a proof of either P → Q or Q → P, and you can leave out any blanks at the end of the tactic. If you have a given h : P ↔︎ Q, then h.ltr is a proof of the left-to-right direction of the biconditional, P → Q, and h.rtl is a proof of the right-to-left direction, Q → P.

Let’s try these strategies out in an example.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x ↔ Q x) :
    (∃ (x : U), P x) ↔ ∃ (x : U), Q x := by
  
  **done::

U : Type
P Q : Pred U
h1 : ∀ (x : U), P x ↔ Q x
⊢ (∃ (x : U), P x) ↔
>>  ∃ (x : U), Q x

The goal is a biconditional statement, so we begin with the tactic apply Iff.intro.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x ↔ Q x) :
    (∃ (x : U), P x) ↔ ∃ (x : U), Q x := by
  apply Iff.intro
  **done::

case mp
U : Type
P Q : Pred U
h1 : ∀ (x : U), P x ↔ Q x
⊢ (∃ (x : U), P x) →
>>  ∃ (x : U), Q x
case mpr
U : Type
P Q : Pred U
h1 : ∀ (x : U), P x ↔ Q x
⊢ (∃ (x : U), Q x) →
>>  ∃ (x : U), P x

Once again, we have two goals. (The case labels this time aren’t very intuitive; “mp” stands for “modus ponens” and “mpr” stands for “modus ponens reverse”.) Whenever we have multiple goals, we’ll use the bulleted-and-indented style introduced in the last example. As in HTPI, we’ll label the proofs of the two goals with (→) and (←), representing the two directions of the biconditional symbol ↔︎. (You can type ← in VS Code by typing \l, short for “left”.) The first goal is a conditional statement, so we assume the antecedent.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x ↔ Q x) :
    (∃ (x : U), P x) ↔ ∃ (x : U), Q x := by
  apply Iff.intro
  · -- (→)
    assume h2 : ∃ (x : U), P x
    **done::
  · -- (←)

    **done::
  done

case mp
U : Type
P Q : Pred U
h1 : ∀ (x : U), P x ↔ Q x
h2 : ∃ (x : U), P x
⊢ ∃ (x : U), Q x

As usual, when we have an existential given, we use it right away.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x ↔ Q x) :
    (∃ (x : U), P x) ↔ ∃ (x : U), Q x := by
  apply Iff.intro
  · -- (→)
    assume h2 : ∃ (x : U), P x
    obtain (u : U) (h3 : P u) from h2
    **done::
  · -- (←)

    **done::
  done

case mp
U : Type
P Q : Pred U
h1 : ∀ (x : U), P x ↔ Q x
h2 : ∃ (x : U), P x
u : U
h3 : P u
⊢ ∃ (x : U), Q x

Now that we have an object of type U in the tactic state, we can use h1 by applying universal instantiation.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x ↔ Q x) :
    (∃ (x : U), P x) ↔ ∃ (x : U), Q x := by
  apply Iff.intro
  · -- (→)
    assume h2 : ∃ (x : U), P x
    obtain (u : U) (h3 : P u) from h2
    have h4 : P u ↔ Q u := h1 u
    **done::
  · -- (←)

    **done::
  done

case mp
U : Type
P Q : Pred U
h1 : ∀ (x : U), P x ↔ Q x
h2 : ∃ (x : U), P x
u : U
h3 : P u
h4 : P u ↔ Q u
⊢ ∃ (x : U), Q x

Looking at h3 and h4, we can now see that we will be able to complete the proof if we assign the value u to x in the goal. So our next step is the tactic apply Exists.intro u.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x ↔ Q x) :
    (∃ (x : U), P x) ↔ ∃ (x : U), Q x := by
  apply Iff.intro
  · -- (→)
    assume h2 : ∃ (x : U), P x
    obtain (u : U) (h3 : P u) from h2
    have h4 : P u ↔ Q u := h1 u
    apply Exists.intro u
    **done::
  · -- (←)

    **done::
  done

case mp
U : Type
P Q : Pred U
h1 : ∀ (x : U), P x ↔ Q x
h2 : ∃ (x : U), P x
u : U
h3 : P u
h4 : P u ↔ Q u
⊢ Q u

To complete the proof, we use the left-to-right direction of h4. We have h4.ltr : P u → Q u and h3 : P u, so by modus ponens, h4.ltr h3 proves the goal Q u. Once we enter this step, Lean indicates that the left-to-right proof is complete, and we can position the cursor below the right-to-left bullet to see the tactic state for the second half of the proof.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x ↔ Q x) :
    (∃ (x : U), P x) ↔ ∃ (x : U), Q x := by
  apply Iff.intro
  · -- (→)
    assume h2 : ∃ (x : U), P x
    obtain (u : U) (h3 : P u) from h2
    have h4 : P u ↔ Q u := h1 u
    apply Exists.intro u
    show Q u from h4.ltr h3
    done
  · -- (←)

    **done::
  done

case mpr
U : Type
P Q : Pred U
h1 : ∀ (x : U), P x ↔ Q x
⊢ (∃ (x : U), Q x) →
>>  ∃ (x : U), P x

The second half of the proof is similar to the first. We begin by assuming h2 : ∃ (x : U), Q x, and then we use that assumption to obtain u : U and h3 : Q u.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x ↔ Q x) :
    (∃ (x : U), P x) ↔ ∃ (x : U), Q x := by
  apply Iff.intro
  · -- (→)
    assume h2 : ∃ (x : U), P x
    obtain (u : U) (h3 : P u) from h2
    have h4 : P u ↔ Q u := h1 u
    apply Exists.intro u
    show Q u from h4.ltr h3
    done
  · -- (←)
    assume h2 : ∃ (x : U), Q x
    obtain (u : U) (h3 : Q u) from h2
    **done::
  done

case mpr
U : Type
P Q : Pred U
h1 : ∀ (x : U), P x ↔ Q x
h2 : ∃ (x : U), Q x
u : U
h3 : Q u
⊢ ∃ (x : U), P x

We can actually shorten the proof by packing a lot into a single step. See if you can figure out the last line of the completed proof below; we’ll give an explanation after the proof.

example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x ↔ Q x) :
    (∃ (x : U), P x) ↔ ∃ (x : U), Q x := by
  apply Iff.intro
  · -- (→)
    assume h2 : ∃ (x : U), P x
    obtain (u : U) (h3 : P u) from h2
    have h4 : P u ↔ Q u := h1 u
    apply Exists.intro u
    show Q u from h4.ltr h3
    done
  · -- (←)
    assume h2 : ∃ (x : U), Q x
    obtain (u : U) (h3 : Q u) from h2
    show ∃ (x : U), P x from Exists.intro u ((h1 u).rtl h3)
    done
  done

To understand the last step, start with the fact that h1 u is a proof of P u ↔︎ Q u. Therefore (h1 u).rtl is a proof of Q u → P u, so by modus ponens, (h1 u).rtl h3 is a proof of P u. It follows that Exists.intro u ((h1 u).rtl h3) is a proof of ∃ (x : U), P x, which was the goal.

There is one more style of reasoning that is sometimes used in proofs of biconditional statements. It is illustrated in Example 3.4.5 of HTPI. Here is that theorem, as it is presented in HTPI (HTPI p. 137).

Suppose \(A\), \(B\), and \(C\) are sets. Then \(A \cap (B \setmin C) = (A \cap B) \setmin C\).

Proof. Let \(x\) be arbitrary. Then \[\begin{align*} x \in A \cap (B \setmin C) &\text{ iff } x \in A \wedge x \in B \setmin C\\ &\text{ iff } x \in A \wedge x \in B \wedge x \notin C\\ &\text{ iff } x \in (A \cap B) \wedge x \notin C\\ &\text{ iff } x \in (A \cap B) \setmin C. \end{align*}\] Thus, \(\forall x(x \in A \cap (B \setmin C) \leftrightarrow x \in (A \cap B) \setmin C)\), so \(A \cap (B \setmin C) = (A \cap B) \setmin C\).  □

This proof is based on a fundamental principle of set theory that says that if two sets have exactly the same elements, then they are equal. This principle is called the axiom of extensionality, and it is what justifies the inference, in the last sentence, from \(\forall x(x \in A \cap (B \setmin C) \leftrightarrow x \in (A \cap B) \setmin C)\) to \(A \cap (B \setmin C) = (A \cap B) \setmin C\).

The heart of the proof is a string of equivalences that, taken together, establish the biconditional statement \(x \in A \cap (B \setmin C) \leftrightarrow x \in (A \cap B) \setmin C\). One can also use this technique to prove a biconditional statement in Lean. This time we’ll simply present the complete proof first, and then explain it afterwards.

theorem Example_3_4_5 (U : Type)
    (A B C : Set U) : A ∩ (B \ C) = (A ∩ B) \ C := by
  apply Set.ext
  fix x : U
  show x ∈ A ∩ (B \ C) ↔ x ∈ (A ∩ B) \ C from
    calc x ∈ A ∩ (B \ C)
      _ ↔ x ∈ A ∧ (x ∈ B ∧ x ∉ C) := Iff.refl _
      _ ↔ (x ∈ A ∧ x ∈ B) ∧ x ∉ C := and_assoc.symm
      _ ↔ x ∈ (A ∩ B) \ C := Iff.refl _
  done

The name of the axiom of extensionality in Lean is Set.ext, and it is applied in the first step of the Lean proof. As usual, the apply tactic works backwards from the goal. In other words, after the first line of the proof, the goal is ∀ (x : U), x ∈ A ∩ (B \ C) ↔︎ x ∈ (A ∩ B) \ C, because by Set.ext, the conclusion of the theorem would follow from this statement. The rest of the proof then proves this goal by introducing an arbitrary x of type U and then proving the biconditional by stringing together several equivalences, exactly as in the HTPI proof.

The proof of the biconditional is called a calculational proof, and it is introduced by the keyword calc. The calculational proof consists of a string of biconditional statements, each of which is provided with a proof. You can think of the underscore on the left side of each biconditional as standing for the right side of the previous biconditional (or, in the case of the first biconditional, the statement after calc).

The proofs of the individual biconditionals in the calculational proof require some explanation. Lean has a large library of theorems that it knows, and you can use those theorems in your proofs. In particular, Iff.refl and and_assoc are names of theorems in Lean’s library. You can find out what any theorem says by using the Lean command #check. (Commands that ask Lean for a response generally start with the character #.) If you type #check Iff.refl in a Lean file, you will see Lean’s response in the Infoview pane: Iff.refl (a : Prop) : a ↔︎ a. What this tells us is that Lean already knows the theorem

theorem Iff.refl (a : Prop) : a ↔ a

(This theorem says that “iff” has a property called reflexivity; we’ll discuss reflexivity in Chapter 4.) When variables are declared in the statement of a theorem, it is understood that they can stand for anything of the appropriate type (see Section 3.1 of HTPI). Thus, the theorem Iff.refl can be thought of as establishing the truth of the statement ∀ (a : Prop), a ↔︎ a. In fact, you can get Lean to report the meaning of the theorem in this form with the command #check @Iff.refl. What this means is that, in any proof, Lean lets you treat Iff.refl as a proof of the statement ∀ (a : Prop), a ↔︎ a. Thus, by universal instantiation, for any proposition a, Lean will recognize Iff.refl a as a proof of a ↔︎ a. This is used to justify the first biconditional in the calculational proof.

But wait! The first biconditional in the calculational proof is x ∈ A ∩ (B \ C) ↔︎ x ∈ A ∧ (x ∈ B ∧ x ∉ C), which does not have the form a ↔︎ a. How can it be justified by the theorem Iff.refl? Recall that Lean doesn’t need to be told to write out definitions of mathematical notation; it does that automatically. When the definitions of the set theory notation are written out, the first biconditional in the calculational proof becomes x ∈ A ∧ (x ∈ B ∧ x ∉ C) ↔︎ x ∈ A ∧ (x ∈ B ∧ x ∉ C), which does have the form a ↔︎ a, so it can be proven with the term-mode proof Iff.refl _. Note that we are using an underscore here to ask Lean to figure out what to plug in for a. This saves us the trouble of writing out the full term-mode proof, which would be Iff.refl (x ∈ A ∧ (x ∈ B ∧ x ∉ C)). The lesson of this example is that the theorem Iff.refl is more powerful than it looks. Not only can we use Iff.refl _ to prove statements of the form a ↔︎ a, we can also use it to prove statements of the form a ↔︎ a', if a and a' reduce to the same thing when definitions are filled in. We say in this case that a and a' are definitionally equal. This explains the third line of the calculational proof, which is also justified by the proof Iff.refl _.

The second line uses the theorem and_assoc. If you type #check and_assoc, you will get this response from Lean:

and_assoc {a b c : Prop} : (a ∧ b) ∧ c ↔ a ∧ b ∧ c

Once again, it is understood that the variables a, b, and c can stand for any propositions, as you can see by giving the command #check @and_assoc. This generates the response

@and_assoc : ∀ {a b c : Prop}, (a ∧ b) ∧ c ↔ a ∧ b ∧ c

which is shorthand for

@and_assoc : ∀ {a : Prop}, ∀ {b : Prop}, ∀ {c : Prop},
              (a ∧ b) ∧ c ↔ a ∧ (b ∧ c)

Recall that the curly braces indicate that a, b, and c are implicit arguments, and that Lean groups the logical connectives to the right, which means that it interprets a ∧ b ∧ c as a ∧ (b ∧ c). This is the associative law for “and” (see Section 1.2 of HTPI). Since a, b, and c are implicit, Lean will recognize and_assoc as a proof of any statement of the form (a ∧ b) ∧ c ↔︎ a ∧ (b ∧ c), where a, b, and c can be replaced with any propositions. Lean doesn’t need to be told what propositions are being used as a, b, and c; it will figure that out for itself. Unfortunately, the second biconditional in the calculational proof is x ∈ A ∧ (x ∈ B ∧ x ∉ C) ↔︎ (x ∈ A ∧ x ∈ B) ∧ x ∉ C, which has the form a ∧ (b ∧ c) ↔︎ (a ∧ b) ∧ c, not (a ∧ b) ∧ c ↔︎ a ∧ (b ∧ c). (Notice that the first of these biconditionals is the same as the second except that the left and right sides have been swapped.) To account for this discrepancy, we use the fact that if h is a proof of any biconditional P ↔︎ Q, then h.symm is a proof of Q ↔︎ P. Thus and_assoc.symm proves the second biconditional in the calculational proof. (By the way, the HTPI proof avoids any mention of the associativity of “and” by simply leaving out parentheses in the conjunction \(x \in A \wedge x \in B \wedge x \notin C\). As explained in Section 1.2 of HTPI, this represents an implicit use of the associativity of “and.”)

You can get a better understanding of the first step of our last proof by typing #check @Set.ext. The result is

@Set.ext : ∀ {α : Type u_1} {a b : Set α},
            (∀ (x : α), x ∈ a ↔ x ∈ b) → a = b

which is shorthand for

@Set.ext : ∀ {α : Type u_1}, ∀ {a : Set α}, ∀ {b : Set α},
            (∀ (x : α), x ∈ a ↔ x ∈ b) → a = b

Ignoring the u_1, whose significance won’t be important to us, this means that Set.ext can be used to prove any statement of the form (∀ (x : α), x ∈ a ↔︎ x ∈ b) → a = b, where α can be replaced by any type and a and b can be replaced by any sets of objects of type α. Make sure you understand how this explains the effect of the tactic apply Set.ext in the first step of our last proof. Almost all of our proofs that two sets are equal will start with apply Set.ext.

Notice that in Lean’s responses to both #check @and_assoc and #check @Set.ext, multiple universal quantifiers in a row were grouped together and written as a single universal quantifier followed by a list of variables (with types). Lean allows this notational shorthand for any sequence of consecutive quantifiers, as long as they are all of the same kind (all existential or all universal), and we will use this notation from now on.

Exercises

theorem Exercise_3_4_2 (U : Type) (A B C : Set U)
    (h1 : A ⊆ B) (h2 : A ⊆ C) : A ⊆ B ∩ C := by
  
  **done::

theorem Exercise_3_4_4 (U : Type) (A B C : Set U)
    (h1 : A ⊆ B) (h2 : A ⊈ C) : B ⊈ C := by
  
  **done::

theorem Exercise_3_3_16 (U : Type) (B : Set U)
    (F : Set (Set U)) : F ⊆ 𝒫 B → ⋃₀ F ⊆ B := by
  
  **done::

theorem Exercise_3_3_17 (U : Type) (F G : Set (Set U))
    (h1 : ∀ (A : Set U), A ∈ F → ∀ (B : Set U), B ∈ G → A ⊆ B) :
    ⋃₀ F ⊆ ⋂₀ G := by
  
  **done::

theorem Exercise_3_4_7 (U : Type) (A B : Set U) :
    𝒫 (A ∩ B) = 𝒫 A ∩ 𝒫 B := by

  **done::

theorem Exercise_3_4_17 (U : Type) (A : Set U) : A = ⋃₀ (𝒫 A) := by

  **done::

theorem Exercise_3_4_18a (U : Type) (F G : Set (Set U)) :
    ⋃₀ (F ∩ G) ⊆ (⋃₀ F) ∩ (⋃₀ G) := by
  
  **done::

theorem Exercise_3_4_19 (U : Type) (F G : Set (Set U)) :
    (⋃₀ F) ∩ (⋃₀ G) ⊆ ⋃₀ (F ∩ G) ↔
      ∀ (A B : Set U), A ∈ F → B ∈ G → A ∩ B ⊆ ⋃₀ (F ∩ G) := by
  
  **done::

3.5. Proofs Involving Disjunctions

A common proof method for dealing with givens or goals that are disjunctions is proof by cases. Here’s how it works (HTPI p. 143).

To use a given of the form P ∨ Q:

Break your proof into cases. For case 1, assume that P is true and use this assumption to prove the goal. For case 2, assume that Q is true and prove the goal.

In Lean, you can break a proof into cases by using the by_cases tactic. If you have a given h : P ∨ Q, then the tactic by_cases on h will break your proof into two cases. For the first case, the given h will be changed to h : P, and for the second, it will be changed to h : Q; the goal for both cases will be the same as the original goal. Thus, the effect of the by_cases on h tactic is as follows:

>> ⋮
h : P ∨ Q
⊢ goal

case Case_1
>> ⋮
h : P
⊢ goal
case Case_2
>> ⋮
h : Q
⊢ goal

Notice that the original given h : P ∨ Q gets replaced by h : P in case 1 and h : Q in case 2. This is usually what is most convenient, but if you write by_cases on h with h1, then the original given h will be preserved, and new givens h1 : P and h1 : Q will be added to cases 1 and 2, respectively. If you want different names for the new givens in the two cases, then use by_cases on h with h1, h2 to add the new given h1 : P in case 1 and h2 : Q in case 2.

You can follow by_cases on with any proof of a disjunction, even if that proof is not just a single identifier. In that cases you will want to add with to specify the identifier or identifiers to be used for the new assumptions in the two cases. Another variant is that you can use the tactic by_cases h : P to break your proof into two cases, with the new assumptions being h : P in case 1 and h : ¬P in case 2. In other words, the effect of by_cases h : P is the same as adding the new given h : P ∨ ¬P (which, of course, is a tautology) and then using the tactic by_cases on h.

There are several introduction rules that you can use in Lean to prove a goal of the form P ∨ Q. If you have h : P, then Lean will accept Or.intro_left Q h as a proof of P ∨ Q. In most situations Lean can infer the proposition Q from context, and in that case you can use the shorter form Or.inl h as a proof of P ∨ Q. You can see the difference between Or.intro_left and Or.inl by using the #check command:

@Or.intro_left : ∀ {a : Prop} (b : Prop), a → a ∨ b

@Or.inl : ∀ {a b : Prop}, a → a ∨ b

Notice that b is an implicit argument in Or.inl, but not in Or.intro_left.

Similarly, if you have h : Q, then Or.intro_right P h is a proof of P ∨ Q. In most situations Lean can infer P from context, and you can use the shorter form Or.inr h.

Often, when your goal has the form P ∨ Q, you will be unable to prove P, and also unable to prove Q. Proof by cases can help in that situation as well (HTPI p. 145).

To prove a goal of the form P ∨ Q:

Break your proof into cases. In each case, either prove P or prove Q.

Example 3.5.2 from HTPI illustrates these strategies:

theorem Example_3_5_2
    (U : Type) (A B C : Set U) :
    A \ (B \ C) ⊆ (A \ B) ∪ C := by

  **done::

U : Type
A B C : Set U
⊢ A \ (B \ C) ⊆ A \ B ∪ C

The define tactic would rewrite the goal as ∀ ⦃a : U⦄, a ∈ A \ (B \ C) → a ∈ A \ B ∪ C, which suggests that our next two tactics should be fix x : U and assume h1 : x ∈ A \ (B \ C). But as we have seen before, if you know what the result of the define tactic is going to be, then there is usually no need to use it. After introducing x as an arbitrary element of A \ (B \ C), we write out the definitions of our new given and goal to help guide our next strategy choice:

theorem Example_3_5_2
    (U : Type) (A B C : Set U) :
    A \ (B \ C) ⊆ (A \ B) ∪ C := by
  fix x : U
  assume h1 : x ∈ A \ (B \ C)
  define; define at h1
  **done::

U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
⊢ x ∈ A \ B ∨ x ∈ C

The goal is now a disjunction, which suggests that proof by cases might be helpful. But what cases should we use? The key is to look at the meaning of the right half of the given h1. The meaning of x ∉ B \ C is ¬(x ∈ B ∧ x ∉ C), which, by one of the De Morgan laws, is equivalent to x ∉ B ∨ x ∈ C.

theorem Example_3_5_2
    (U : Type) (A B C : Set U) :
    A \ (B \ C) ⊆ (A \ B) ∪ C := by
  fix x : U
  assume h1 : x ∈ A \ (B \ C)
  define; define at h1
  have h2 : x ∉ B \ C := h1.right
  define at h2; demorgan at h2
            --h2 : x ∉ B ∨ x ∈ C
  **done::

U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B ∨ x ∈ C
⊢ x ∈ A \ B ∨ x ∈ C

The new given h2 is now a disjunction, which suggests what cases we should use:

theorem Example_3_5_2
    (U : Type) (A B C : Set U) :
    A \ (B \ C) ⊆ (A \ B) ∪ C := by
  fix x : U
  assume h1 : x ∈ A \ (B \ C)
  define; define at h1
  have h2 : x ∉ B \ C := h1.right
  define at h2; demorgan at h2
            --h2 : x ∉ B ∨ x ∈ C
  by_cases on h2
  **done::

case Case_1
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B
⊢ x ∈ A \ B ∨ x ∈ C
case Case_2
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∈ C
⊢ x ∈ A \ B ∨ x ∈ C

Of course, now that we have two goals, we will introduce bullets labeling the two parts of the proof as case 1 and case 2. Looking at the givens h1 and h2 in both cases, it is not hard to see that we should be able to prove x ∈ A \ B in case 1 and x ∈ C in case 2. Thus, in case 1 we will be able to give a proof of the goal that has the form Or.inl _, where the blank will be filled in with a proof of x ∈ A \ B, and in case 2 we can use Or.inr _, filling in the blank with a proof of x ∈ C. This suggests that we should use the tactics apply Or.inl in case 1 and apply Or.inr in case 2. Focusing first on case 1, we get:

theorem Example_3_5_2
    (U : Type) (A B C : Set U) :
    A \ (B \ C) ⊆ (A \ B) ∪ C := by
  fix x : U
  assume h1 : x ∈ A \ (B \ C)
  define; define at h1
  have h2 : x ∉ B \ C := h1.right
  define at h2; demorgan at h2
            --h2 : x ∉ B ∨ x ∈ C
  by_cases on h2
  · -- Case 1. h2 : x ∉ B
    apply Or.inl
    **done::
  · -- Case 2. h2 : x ∈ C

    **done::
  done

case Case_1.h
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B
⊢ x ∈ A \ B

Notice that the tactic apply Or.inl has changed the goal for case 1 to the left half of the original goal, x ∈ A \ B. Since this means x ∈ A ∧ x ∉ B, we can complete case 1 by combining h1.left with h2, and then we can move on to case 2.

theorem Example_3_5_2
    (U : Type) (A B C : Set U) :
    A \ (B \ C) ⊆ (A \ B) ∪ C := by
  fix x : U
  assume h1 : x ∈ A \ (B \ C)
  define; define at h1
  have h2 : x ∉ B \ C := h1.right
  define at h2; demorgan at h2
            --h2 : x ∉ B ∨ x ∈ C
  by_cases on h2
  · -- Case 1. h2 : x ∉ B
    apply Or.inl
    show x ∈ A \ B from And.intro h1.left h2
    done
  · -- Case 2. h2 : x ∈ C

    **done::
  done

case Case_2
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∈ C
⊢ x ∈ A \ B ∨ x ∈ C

Case 2 is similar, using Or.inr and h2

theorem Example_3_5_2
    (U : Type) (A B C : Set U) :
    A \ (B \ C) ⊆ (A \ B) ∪ C := by
  fix x : U
  assume h1 : x ∈ A \ (B \ C)
  define; define at h1
  have h2 : x ∉ B \ C := h1.right
  define at h2; demorgan at h2
            --h2 : x ∉ B ∨ x ∈ C
  by_cases on h2
  · -- Case 1. h2 : x ∉ B
    apply Or.inl
    show x ∈ A \ B from And.intro h1.left h2
    done
  · -- Case 2. h2 : x ∈ C
    apply Or.inr
    show x ∈ C from h2
    done
  done

No goals

There is a second strategy that is often useful to prove a goal of the form P ∨ Q. It is motivated by the fact that P ∨ Q is equivalent to both ¬P → Q and ¬Q → P (HTPI p. 147).

To prove a goal of the form P ∨ Q:

Assume that P is false and prove Q, or assume that Q is false and prove P.

If your goal is P ∨ Q, then the Lean tactic or_left with h will add the new given h : ¬Q to the tactic state and set the goal to be P, and or_right with h will add h : ¬P to the tactic state and set the goal to be Q. For example, here is the effect of the tactic or_left with h:

>> ⋮
⊢ P ∨ Q

>> ⋮
h : ¬Q
⊢ P

Notice that or_left and or_right have the same effect as apply Or.inl and apply Or.inr, except that each adds a new given to the tactic state. Sometimes you can tell in advance that you won’t need the extra given, and in that case the tactics apply Or.inl and apply Or.inr can be useful. For example, that was the case in the example above. But if you think the extra given might be useful, you are better off using or_left or or_right. Here’s an example illustrating this.

example (U : Type) (A B C : Set U)
    (h1 : A \ B ⊆ C) : A ⊆ B ∪ C := by
  
  **done::

U : Type
A B C : Set U
h1 : A \ B ⊆ C
⊢ A ⊆ B ∪ C

Of course, we begin by letting x be an arbitrary element of A. Writing out the meaning of the new goal shows that it is a disjunction.

example (U : Type) (A B C : Set U)
    (h1 : A \ B ⊆ C) : A ⊆ B ∪ C := by
  fix x : U
  assume h2 : x ∈ A
  define
  **done::

U : Type
A B C : Set U
h1 : A \ B ⊆ C
x : U
h2 : x ∈ A
⊢ x ∈ B ∨ x ∈ C

Looking at the givens h1 and h2, we see that if we assume x ∉ B, then we should be able to prove x ∈ C. This suggests that we should use the or_right tactic.

example (U : Type) (A B C : Set U)
    (h1 : A \ B ⊆ C) : A ⊆ B ∪ C := by
  fix x : U
  assume h2 : x ∈ A
  define
  or_right with h3
  **done::

U : Type
A B C : Set U
h1 : A \ B ⊆ C
x : U
h2 : x ∈ A
h3 : x ∉ B
⊢ x ∈ C

We can now complete the proof. Notice that h1 _ will be a proof of the goal x ∈ C, if we can fill in the blank with a proof of x ∈ A \ B. Since x ∈ A \ B means x ∈ A ∧ x ∉ B, we can prove it with the expression And.intro h2 h3.

example (U : Type) (A B C : Set U)
    (h1 : A \ B ⊆ C) : A ⊆ B ∪ C := by
  fix x : U
  assume h2 : x ∈ A
  define
  or_right with h3
  show x ∈ C from h1 (And.intro h2 h3)
  done

No goals

The fact that P ∨ Q is equivalent to both ¬P → Q and ¬Q → P also suggests another strategy for using a given that is a disjunction (HTPI p. 149).

To use a given of the form P ∨ Q:

If you are also given ¬P, or you can prove that P is false, then you can use this given to conclude that Q is true. Similarly, if you are given ¬Q or can prove that Q is false, then you can conclude that P is true.

This strategy is a rule of inference called disjunctive syllogism, and the tactic for using this strategy in Lean is called disj_syll. If you have h1 : P ∨ Q and h2 : ¬P, then the tactic disj_syll h1 h2 will change h1 to h1 : Q; if instead you have h2 : ¬Q, then disj_syll h1 h2 will change h1 to h1 : P. Notice that, as with the by_cases tactic, the given h1 gets replaced with the conclusion of the rule. The tactic disj_syll h1 h2 with h3 will preserve the original h1 and introduce the conclusion as a new given with the identifier h3. Also, as with the by_cases tactic, either h1 or h2 can be a complex proof rather than simply an identifier (although in that case it must be enclosed in parentheses, so that Lean can tell where h1 ends and h2 begins). The only requirement is that h1 must be a proof of a disjunction, and h2 must be a proof of the negation of one side of the disjunction. If h1 is not simply an identifier, then you will want to use with to specify the identifier to be used for the conclusion of the rule.

Here’s an example illustrating the use of the disjunctive syllogism rule.

example
    (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ¬∃ (x : U), x ∈ A ∩ B) : A ⊆ C := by

  **done::

U : Type
A B C : Set U
h1 : A ⊆ B ∪ C
h2 : ¬∃ (x : U),
>>  x ∈ A ∩ B
⊢ A ⊆ C

Of course, we begin by introducing an arbitrary element of A. We also rewrite h2 as an equivalent positive statement.

example
    (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ¬∃ (x : U), x ∈ A ∩ B) : A ⊆ C := by
  fix a : U
  assume h3 : a ∈ A
  quant_neg at h2
  **done::

U : Type
A B C : Set U
h1 : A ⊆ B ∪ C
h2 : ∀ (x : U),
>>  x ∉ A ∩ B
a : U
h3 : a ∈ A
⊢ a ∈ C

We can now make two inferences by combining h1 with h3 and by applying h2 to a. To see how to use the inferred statements, we write out their definitions, and since one of them is a negative statement, we reexpress it as an equivalent positive statement.

example
    (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ¬∃ (x : U), x ∈ A ∩ B) : A ⊆ C := by
  fix a : U
  assume h3 : a ∈ A
  quant_neg at h2
  have h4 : a ∈ B ∪ C := h1 h3
  have h5 : a ∉ A ∩ B := h2 a
  define at h4
  define at h5; demorgan at h5
  **done::

U : Type
A B C : Set U
h1 : A ⊆ B ∪ C
h2 : ∀ (x : U),
>>  x ∉ A ∩ B
a : U
h3 : a ∈ A
h4 : a ∈ B ∨ a ∈ C
h5 : a ∉ A ∨ a ∉ B
⊢ a ∈ C

Both h4 and h5 are disjunctions, and looking at h3 we see that the disjunctive syllogism rule can be applied. From h3 and h5 we can draw the conclusion a ∉ B, and then combining that conclusion with h4 we can infer a ∈ C. Since that is the goal, we are done.

example
    (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ¬∃ (x : U), x ∈ A ∩ B) : A ⊆ C := by
  fix a : U
  assume h3 : a ∈ A
  quant_neg at h2
  have h4 : a ∈ B ∪ C := h1 h3
  have h5 : a ∉ A ∩ B := h2 a
  define at h4
  define at h5; demorgan at h5
  disj_syll h5 h3  --h5 : a ∉ B
  disj_syll h4 h5  --h4 : a ∈ C
  show a ∈ C from h4
  done

No goals

We’re going to redo the last example, to illustrate another useful technique in Lean. We start with some of the same steps as before.

example
    (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ¬∃ (x : U), x ∈ A ∩ B) : A ⊆ C := by
  fix a : U
  assume h3 : a ∈ A
  have h4 : a ∈ B ∪ C := h1 h3
  define at h4
  **done::

U : Type
A B C : Set U
h1 : A ⊆ B ∪ C
h2 : ¬∃ (x : U),
>>  x ∈ A ∩ B
a : U
h3 : a ∈ A
h4 : a ∈ B ∨ a ∈ C
⊢ a ∈ C

At this point, you might see a possible route to the goal: from h2 and h3 we should be able to prove that a ∉ B, and then, combining that with h4 by the disjunctive syllogism rule, we should be able to deduce the goal a ∈ C. Let’s try writing the proof that way.

??example::
    (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ¬∃ (x : U), x ∈ A ∩ B) : A ⊆ C := by
  fix a : U
  assume h3 : a ∈ A
  have h4 : a ∈ B ∪ C := h1 h3
  define at h4
  have h5 : a ∉ B := sorry
  disj_syll h4 h5  --h4 : a ∈ C
  show a ∈ C from h4
  done

No goals

We have introduced a new idea in this proof. The justification we have given for introducing h5 : a ∉ B is sorry. You might think of this as meaning “Sorry, I’m not going to give a justification for this statement, but please accept it anyway.” Of course, this is cheating; in a complete proof, every step must be justified. Lean accepts sorry as a proof of any statement, but it displays it in red to warn you that you’re cheating. It also puts a brown squiggle under the keyword example and it puts the message declaration uses 'sorry' in the Infoview, to warn you that, although the proof has reached the goal, it is not fully justified.

Although writing the proof this way is cheating, it is a convenient way to see that our plan of attack for this proof is reasonable. Lean has accepted the proof, except for the warning that we have used sorry. So now we know that if we go back and replace sorry with a proof of a ∉ B, then we will have a complete proof.

The proof of a ∉ B is hard enough that it is easier to do it in tactic mode rather than term mode. So we will begin the proof as we always do for tactic-mode proofs: we replace sorry with by, leave a blank line, and then put done, indented further than the surrounding text. When we put the cursor on the blank line before done, we see the tactic state for our “proof within a proof.”

example
    (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ¬∃ (x : U), x ∈ A ∩ B) : A ⊆ C := by
  fix a : U
  assume h3 : a ∈ A
  have h4 : a ∈ B ∪ C := h1 h3
  define at h4
  have h5 : a ∉ B := by

    **done::
  disj_syll h4 h5  --h4 : a ∈ C
  show a ∈ C from h4
  done

U : Type
A B C : Set U
h1 : A ⊆ B ∪ C
h2 : ¬∃ (x : U),
>>  x ∈ A ∩ B
a : U
h3 : a ∈ A
h4 : a ∈ B ∨ a ∈ C
⊢ a ∉ B

Note that h5 : a ∉ B is not a given in the tactic state, because we have not yet justified it; in fact, a ∉ B is the goal. This goal is a negative statement, and h2 is also negative. This suggests that we could try using proof by contradiction, achieving the contradiction by contradicting h2. So we use the tactic contradict h2 with h6.

example
    (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ¬∃ (x : U), x ∈ A ∩ B) : A ⊆ C := by
  fix a : U
  assume h3 : a ∈ A
  have h4 : a ∈ B ∪ C := h1 h3
  define at h4
  have h5 : a ∉ B := by
    contradict h2 with h6
    **done::
  disj_syll h4 h5  --h4 : a ∈ C
  show a ∈ C from h4
  done

U : Type
A B C : Set U
h1 : A ⊆ B ∪ C
h2 : ¬∃ (x : U),
>>  x ∈ A ∩ B
a : U
h3 : a ∈ A
h4 : a ∈ B ∨ a ∈ C
h6 : a ∈ B
⊢ ∃ (x : U), x ∈ A ∩ B

Looking at h3 and h6, we see that the right value to plug in for x in the goal is a. In fact, Exists.intro a _ will prove the goal, if we can fill in the blank with a proof of a ∈ A ∩ B. Since this means a ∈ A ∧ a ∈ B, we can prove it with And.intro h3 h6. Thus, we can complete the proof in one more step:

example
    (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ¬∃ (x : U), x ∈ A ∩ B) : A ⊆ C := by
  fix a : U
  assume h3 : a ∈ A
  have h4 : a ∈ B ∪ C := h1 h3
  define at h4
  have h5 : a ∉ B := by
    contradict h2 with h6
    show ∃ (x : U), x ∈ A ∩ B from
      Exists.intro a (And.intro h3 h6)
    done
  disj_syll h4 h5  --h4 : a ∈ C
  show a ∈ C from h4
  done

No goals

The red squiggle has disappeared from the word done, indicating that the proof is complete.

It was not really necessary for us to use sorry when writing this proof. We could have simply written the steps in order, exactly as they appear above. Any time you use the have tactic with a conclusion that is difficult to justify, you have a choice. You can establish the have with sorry, complete the proof, and then return and fill in a justification for the have, as we did in the example above. Or, you can justify the have right away by typing by after := and then plunging into the “proof within in a proof.” Once you complete the inner proof, you can continue with the original proof.

And in case you were wondering: yes, if the inner proof uses the have tactic with a statement that is hard to justify, then you can write a “proof within a proof within a proof”!

Exercises

In each case, replace sorry with a proof.

theorem Exercise_3_5_2 (U : Type) (A B C : Set U) :
    (A ∪ B) \ C ⊆ A ∪ (B \ C) := sorry

theorem Exercise_3_5_5 (U : Type) (A B C : Set U)
    (h1 : A ∩ C ⊆ B ∩ C) (h2 : A ∪ C ⊆ B ∪ C) : A ⊆ B := sorry

theorem Exercise_3_5_7 (U : Type) (A B C : Set U) :
    A ∪ C ⊆ B ∪ C ↔ A \ C ⊆ B \ C := sorry

theorem Exercise_3_5_8 (U : Type) (A B : Set U) :
    𝒫 A ∪ 𝒫 B ⊆ 𝒫 (A ∪ B) := sorry

theorem Exercise_3_5_17b (U : Type) (F : Set (Set U)) (B : Set U) :
    B ∪ (⋂₀ F) = {x : U | ∀ (A : Set U), A ∈ F → x ∈ B ∪ A} := sorry

theorem Exercise_3_5_18 (U : Type) (F G H : Set (Set U))
    (h1 : ∀ (A : Set U), A ∈ F → ∀ (B : Set U), B ∈ G → A ∪ B ∈ H) :
    ⋂₀ H ⊆ (⋂₀ F) ∪ (⋂₀ G) := sorry

theorem Exercise_3_5_24a (U : Type) (A B C : Set U) :
    (A ∪ B) △ C ⊆ (A △ C) ∪ (B △ C) := sorry

3.6. Existence and Uniqueness Proofs

Recall that ∃! (x : U), P x means that there is exactly one x of type U such that P x is true. One way to deal with a given or goal of this form is to use the define tactic to rewrite it as the equivalent statement ∃ (x : U), P x ∧ ∀ (x_1 : U), P x_1 → x_1 = x. You can then apply techniques discussed previously in this chapter. However, there are also proof techniques, and corresponding Lean tactics, for working directly with givens and goals of this form.

Often a goal of the form ∃! (x : U), P x is proven by using the following strategy. This is a slight rephrasing of the strategy presented in HTPI. The rephrasing is based on the fact that for any propositions A, B, and C, A ∧ B → C is equivalent to A → B → C (you can check this equivalence by making a truth table). The second of these statements is usually easier to work with in Lean than the first one, so we will often rephrase statements that have the form A ∧ B → C as A → B → C. To see why the second statement is easier to use, suppose that you have givens hA : A and hB : B. If you also have h : A → B → C, then h hA is a proof of B → C, and therefore h hA hB is a proof of C. If instead you had h' : (A ∧ B) → C, then to prove C you would have to write h' (And.intro hA hB), which is a bit less convenient.

With that preparation, here is our strategy for proving statements of the form ∃! (x : U), P x (HTPI pp. 156–157).

To prove a goal of the form ∃! (x : U), P x:

Prove ∃ (x : U), P x and ∀ (x_1 x_2 : U), P x_1 → P x_2 → x_1 = x_2. The first of these goals says that there exists an x such that P x is true, and the second says that it is unique. The two parts of the proof are therefore sometimes labeled existence and uniqueness.

To apply this strategy in a Lean proof, we use the tactic exists_unique. We’ll illustrate this with the theorem from Example 3.6.2 in HTPI. Here’s how that theorem and its proof are presented in HTPI (HTPI pp. 157–158):

There is a unique set \(A\) such that for every set \(B\), \(A \cup B = B\).

Proof. Existence: Clearly \(\forall B(\varnothing \cup B = B)\), so \(\varnothing\) has the required property.

Uniqueness: Suppose \(\forall B(C \cup B = B)\) and \(\forall B(D \cup B = B)\). Applying the first of these assumptions to \(D\) we see that \(C \cup D = D\), and applying the second to \(C\) we get \(D \cup C = C\). But clearly \(C \cup D = D \cup C\), so \(C = D\).  □

You will notice that there are two statements in this proof that are described as “clearly” true. This brings up one of the difficulties with proving theorems in Lean: things that are clear to us are not necessarily clear to Lean! There are two ways to deal with such “clear” statements. The first is to see if the statement is in the library of theorems that Lean knows. The second is to prove the statement as a preliminary theorem that can then be used in the proof of our main theorem. We’ll take the second approach here, since proving these “clear” facts will give us more practice with Lean proofs, but later we’ll have more to say about searching for statements in Lean’s theorem library.

The first theorem we need says that for every set B, ∅ ∪ B = B, and it brings up a subtle issue: in Lean, the symbol ∅ is ambiguous! The reason for this is Lean’s strict typing rules. For each type U, there is an empty set of type Set U. There is, for example, the set of type Set Nat that contains no natural numbers, and also the set of type Set Real that contains no real numbers. To Lean, these are different sets, because they have different types. Which one does the symbol ∅ denote? The answer will be different in different contexts. Lean can often figure out from context which empty set you have in mind, but if it can’t, then you have to tell it explicitly by writing (∅ : Set U) rather than ∅. Fortunately, in our theorems Lean is able to figure out which empty set we have in mind.

With that preparation, we are ready to prove our first preliminary theorem. Since the goal is an equation between sets, our first step is to use the tactic apply Set.ext.

theorem empty_union {U : Type} (B : Set U) :
    ∅ ∪ B = B := by
  apply Set.ext
  **done::

case h
U : Type
B : Set U
⊢ ∀ (x : U),
>>  x ∈ ∅ ∪ B ↔ x ∈ B

Based on the form of the goal, our next two tactics should be fix x : U and apply Iff.intro. This leaves us with two goals, corresponding to the two directions of the biconditional, but we’ll focus first on just the left-to-right direction.

theorem empty_union {U : Type} (B : Set U) :
    ∅ ∪ B = B := by
  apply Set.ext
  fix x : U
  apply Iff.intro
  · -- (→)

    **done::
  · -- (←)

    **done::
  done

case h.mp
U : Type
B : Set U
x : U
⊢ x ∈ ∅ ∪ B → x ∈ B

Of course, our next step is to assume x ∈ ∅ ∪ B. To help us see how to move forward, we also write out the definition of this assumption.

theorem empty_union {U : Type} (B : Set U) :
    ∅ ∪ B = B := by
  apply Set.ext
  fix x : U
  apply Iff.intro
  · -- (→)
    assume h1 : x ∈ ∅ ∪ B
    define at h1
    **done::
  · -- (←)

    **done::
  done

case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
⊢ x ∈ B

Now you should see a way to complete the proof: the statement x ∈ ∅ is false, so we should be able to apply the disjunctive syllogism rule to h1 to infer the goal x ∈ B. To carry out this plan, we’ll first have to prove x ∉ ∅. We’ll use the have tactic, and since there’s no obvious term-mode proof to justify it, we’ll try a tactic-mode proof.

theorem empty_union {U : Type} (B : Set U) :
    ∅ ∪ B = B := by
  apply Set.ext
  fix x : U
  apply Iff.intro
  · -- (→)
    assume h1 : x ∈ ∅ ∪ B
    define at h1
    have h2 : x ∉ ∅ := by

      **done::
    **done::
  · -- (←)

    **done::
  done

U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
⊢ x ∉ ∅

The goal for our “proof within a proof” is a negative statement, so proof by contradiction seems like a good start.

theorem empty_union {U : Type} (B : Set U) :
    ∅ ∪ B = B := by
  apply Set.ext
  fix x : U
  apply Iff.intro
  · -- (→)
    assume h1 : x ∈ ∅ ∪ B
    define at h1
    have h2 : x ∉ ∅ := by
      by_contra h3
      **done::
    **done::
  · -- (←)

    **done::
  done

U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h3 : x ∈ ∅
⊢ False

To see how to use the new assumption h3, we use the tactic define at h3. The definition Lean gives for the statement x ∈ ∅ is False. In other words, Lean knows that, by the definition of ∅, the statement x ∈ ∅ is false. Since False is our goal, this completes the inner proof, and we can return to the main proof.

theorem empty_union {U : Type} (B : Set U) :
    ∅ ∪ B = B := by
  apply Set.ext
  fix x : U
  apply Iff.intro
  · -- (→)
    assume h1 : x ∈ ∅ ∪ B
    define at h1
    have h2 : x ∉ ∅ := by
      by_contra h3
      define at h3  --h3 : False
      show False from h3
      done
    **done::
  · -- (←)

    **done::
  done

case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h2 : x ∉ ∅
⊢ x ∈ B

Now that we have established the claim h2 : x ∉ ∅, we can apply the disjunctive syllogism rule to h1 and h2 to reach the goal. This completes the left-to-right direction of the biconditional proof, so we move on to the right-to-left direction.

theorem empty_union {U : Type} (B : Set U) :
    ∅ ∪ B = B := by
  apply Set.ext
  fix x : U
  apply Iff.intro
  · -- (→)
    assume h1 : x ∈ ∅ ∪ B
    define at h1
    have h2 : x ∉ ∅ := by
      by_contra h3
      define at h3  --h3 : False
      show False from h3
      done
    disj_syll h1 h2  --h1 : x ∈ B
    show x ∈ B from h1
    done
  · -- (←)

    **done::
  done

case h.mpr
U : Type
B : Set U
x : U
⊢ x ∈ B → x ∈ ∅ ∪ B

This direction of the biconditional proof is easier: once we introduce the assumption h1 : x ∈ B, our goal will be x ∈ ∅ ∪ B, which means x ∈ ∅ ∨ x ∈ B, and we can prove it with the proof Or.inr h1.

theorem empty_union {U : Type} (B : Set U) :
    ∅ ∪ B = B := by
  apply Set.ext
  fix x : U
  apply Iff.intro
  · -- (→)
    assume h1 : x ∈ ∅ ∪ B
    define at h1
    have h2 : x ∉ ∅ := by
      by_contra h3
      define at h3  --h3 : False
      show False from h3
      done
    disj_syll h1 h2  --h1 : x ∈ B
    show x ∈ B from h1
    done
  · -- (←)
    assume h1 : x ∈ B
    show x ∈ ∅ ∪ B from Or.inr h1
    done
  done

No goals

The second fact that was called “clear” in the proof from Example 3.6.2 was the equation C ∪ D = D ∪ C. This looks like an instance of the commutativity of the union operator. Let’s prove that union is commutative.

theorem union_comm {U : Type} (X Y : Set U) :
    X ∪ Y = Y ∪ X := by
  
  **done::

U : Type
X Y : Set U
⊢ X ∪ Y = Y ∪ X

Once again, we begin with apply Set.ext, which converts the goal to ∀ (x : U), x ∈ X ∪ Y ↔︎ x ∈ Y ∪ X, and then fix x : U.

theorem union_comm {U : Type} (X Y : Set U) :
    X ∪ Y = Y ∪ X := by
  apply Set.ext
  fix x : U
  **done::

case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∪ Y ↔ x ∈ Y ∪ X

To understand the goal better, we’ll write out the definitions of the two sides of the biconditional. We use an extension of the define tactic that allows us to write out the definition of just a part of a given or the goal. The tactic define : x ∈ X ∪ Y will replace x ∈ X ∪ Y with its definition wherever it appears in the goal, and then define : x ∈ Y ∪ X will replace x ∈ Y ∪ X with its definition. (Note that define : X ∪ Y produces a result that is not as useful. It is usually best to define a complete statement rather than just a part of a statement. As usual, you can add at to do the replacements in a given rather than the goal.)

theorem union_comm {U : Type} (X Y : Set U) :
    X ∪ Y = Y ∪ X := by
  apply Set.ext
  fix x : U
  define : x ∈ X ∪ Y
  define : x ∈ Y ∪ X
  **done::

case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∨ x ∈ Y ↔
>>  x ∈ Y ∨ x ∈ X

By the way, there are similar extensions of all of the tactics contrapos, demorgan, conditional, double_neg, bicond_neg, and quant_neg that allow you to use a logical equivalence to rewrite just a part of a formula. For example, if your goal is P ∧ (¬Q → R), then the tactic contrapos : ¬Q → R will change the goal to P ∧ (¬R → Q). If you have a given h : P → ¬∀ (x : U), Q x, then the tactic quant_neg : ¬∀ (x : U), Q x at h will change h to h : P → ∃ (x : U), ¬Q x.

Returning to our proof of union_comm: the goal is now x ∈ X ∨ x ∈ Y ↔︎ x ∈ Y ∨ x ∈ X. You could prove this by a somewhat tedious application of the rules for biconditionals and disjunctions that were discussed in the last two sections, and we invite you to try it. But there is another possibility. The goal now has the form P ∨ Q ↔︎ Q ∨ P, which is the commutative law for “or” (see Section 1.2 of HTPI). We saw in a previous example that Lean has, in its library, the associative law for “and”; it is called and_assoc. Does Lean also know the commutative law for “or”?

Try typing #check @or_ in VS Code. After a few seconds, a pop-up window appears with possible completions of this command. You will see or_assoc on the list, as well as or_comm. Select or_comm, and you’ll get this response: @or_comm : ∀ {a b : Prop}, a ∨ b ↔︎ b ∨ a. Since a and b are implicit arguments in this theorem, you can use or_comm to prove any statement of the form a ∨ b ↔︎ b ∨ a, where Lean will figure out for itself what a and b stand for. In particular, or_comm will prove our current goal.

theorem union_comm {U : Type} (X Y : Set U) :
    X ∪ Y = Y ∪ X := by
  apply Set.ext
  fix x : U
  define : x ∈ X ∪ Y
  define : x ∈ Y ∪ X
  show x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X from or_comm
  done

No goals

We have now proven the two statements that were said to be “clearly” true in the proof in Example 3.6.2 of HTPI, and we have given them names. And that means that we can now use these theorems, in the file containing these proofs, to prove other theorems. As with any theorem in Lean’s library, you can use the #check command to confirm what these theorems say. If you type #check @empty_union and #check @union_comm, you will get these results:

@empty_union : ∀ {U : Type} (B : Set U), ∅ ∪ B = B

@union_comm : ∀ {U : Type} (X Y : Set U), X ∪ Y = Y ∪ X

Notice that in both theorems we used curly braces when we introduced the type U, so it is an implicit argument and will not need to be specified when we apply the theorems. (Why did we decide to make U an implicit argument? Well, when we apply the theorem empty_union we will be specifying the set B, and when we apply union_comm we will be specifying the sets X and Y. Lean can figure out what U is by examining the types of these sets, so there is no need to specify it separately.)

We are finally ready to prove the theorem from Example 3.6.2. Here is the theorem:

theorem Example_3_6_2 (U : Type) :
    ∃! (A : Set U), ∀ (B : Set U),
    A ∪ B = B := by

  **done::

U : Type
⊢ ∃! (A : Set U),
>>  ∀ (B : Set U),
>>    A ∪ B = B

The goal starts with ∃!, so we use our new tactic, exists_unique.

theorem Example_3_6_2 (U : Type) :
    ∃! (A : Set U), ∀ (B : Set U),
    A ∪ B = B := by
  exists_unique
  **done::

case Existence
U : Type
⊢ ∃ (A : Set U),
>>  ∀ (B : Set U),
>>    A ∪ B = B
case Uniqueness
U : Type
⊢ ∀ (A_1 A_2 : Set U),
>>  (∀ (B : Set U),
>>      A_1 ∪ B = B) →
>>  (∀ (B : Set U),
>>      A_2 ∪ B = B) →
>>  A_1 = A_2

We have two goals, labeled Existence and Uniqueness. Imitating the proof from HTPI, we prove existence by using the value ∅ for A.

theorem Example_3_6_2 (U : Type) :
    ∃! (A : Set U), ∀ (B : Set U),
    A ∪ B = B := by
  exists_unique
  · -- Existence
    apply Exists.intro ∅
    **done::
  · -- Uniqueness

    **done::
  done

case Existence
U : Type
⊢ ∀ (B : Set U),
>>  ∅ ∪ B = B

The goal is now precisely the statement of the theorem empty_union, so we can prove it by simply citing that theorem.

theorem Example_3_6_2 (U : Type) :
    ∃! (A : Set U), ∀ (B : Set U),
    A ∪ B = B := by
  exists_unique
  · -- Existence
    apply Exists.intro ∅
    show ∀ (B : Set U), ∅ ∪ B = B from empty_union
    done
  · -- Uniqueness

    **done::
  done

case Uniqueness
U : Type
⊢ ∀ (A_1 A_2 : Set U),
>>  (∀ (B : Set U),
>>      A_1 ∪ B = B) →
>>  (∀ (B : Set U),
>>      A_2 ∪ B = B) →
>>  A_1 = A_2

For the uniqueness proof, we begin by introducing arbitrary sets C and D and assuming ∀ (B : Set U), C ∪ B = B and ∀ (B : Set U), D ∪ B = B, exactly as in the HTPI proof.

theorem Example_3_6_2 (U : Type) :
    ∃! (A : Set U), ∀ (B : Set U),
    A ∪ B = B := by
  exists_unique
  · -- Existence
    apply Exists.intro ∅
    show ∀ (B : Set U), ∅ ∪ B = B from empty_union
    done
  · -- Uniqueness
    fix C : Set U; fix D : Set U
    assume h1 : ∀ (B : Set U), C ∪ B = B
    assume h2 : ∀ (B : Set U), D ∪ B = B
    **done::
  done

case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U),
>>  C ∪ B = B
h2 : ∀ (B : Set U),
>>  D ∪ B = B
⊢ C = D

The next step in HTPI was to apply h1 to D, and h2 to C. We do the same thing in Lean.

theorem Example_3_6_2 (U : Type) :
    ∃! (A : Set U), ∀ (B : Set U),
    A ∪ B = B := by
  exists_unique
  · -- Existence
    apply Exists.intro ∅
    show ∀ (B : Set U), ∅ ∪ B = B from empty_union
    done
  · -- Uniqueness
    fix C : Set U; fix D : Set U
    assume h1 : ∀ (B : Set U), C ∪ B = B
    assume h2 : ∀ (B : Set U), D ∪ B = B
    have h3 : C ∪ D = D := h1 D
    have h4 : D ∪ C = C := h2 C 
    **done::
  done

case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U),
>>  C ∪ B = B
h2 : ∀ (B : Set U),
>>  D ∪ B = B
h3 : C ∪ D = D
h4 : D ∪ C = C
⊢ C = D

The goal can now be achieved by stringing together a sequence of equations: C = D ∪ C = C ∪ D = D. The first of these equations is h4.symm—that is, h4 read backwards; the second follows from the commutative law for union; and the third is h3. We saw in Section 3.4 that you can prove a biconditional statement in Lean by stringing together a sequence of biconditionals in a calculational proof. Exactly the same method applies to equations. Here is the complete proof of the theorem:

theorem Example_3_6_2 (U : Type) :
    ∃! (A : Set U), ∀ (B : Set U),
    A ∪ B = B := by
  exists_unique
  · -- Existence
    apply Exists.intro ∅
    show ∀ (B : Set U), ∅ ∪ B = B from empty_union
    done
  · -- Uniqueness
    fix C : Set U; fix D : Set U
    assume h1 : ∀ (B : Set U), C ∪ B = B
    assume h2 : ∀ (B : Set U), D ∪ B = B
    have h3 : C ∪ D = D := h1 D
    have h4 : D ∪ C = C := h2 C 
    show C = D from
      calc C
        _ = D ∪ C := h4.symm
        _ = C ∪ D := union_comm D C
        _ = D := h3
    done
  done

Since the statement ∃! (x : U), P x asserts both the existence and the uniqueness of an object satisfying the predicate P, we have the following strategy for using a given of this form (HTPI p. 159):

To use a given of the form ∃! (x : U), P x:

Introduce a new variable, say a, into the proof to stand for an object of type U for which P a is true. You may also assert that ∀ (x_1 x_2 : U), P x_1 → P x_2 → x_1 = x2.

If you have a given h : ∃! (x : U), P x, then the tactic obtain (a : U) (h1 : P a)
(h2 : ∀ (x_1 x_2 : U), P x_1 → P x_2 → x_1 = x_2) from h will introduce into the tactic state a new variable a of type U and new givens (h1 : P a) and (h2 : ∀ (x_1 x_2 : U), P x_1 → P x_2 → x_1 = x_2). To illustrate the use of this tactic, let’s prove the theorem in Example 3.6.4 of HTPI.

theorem Example_3_6_4 (U : Type) (A B C : Set U)
    (h1 : ∃ (x : U), x ∈ A ∩ B)
    (h2 : ∃ (x : U), x ∈ A ∩ C)
    (h3 : ∃! (x : U), x ∈ A) :
    ∃ (x : U), x ∈ B ∩ C := by

  **done::

U : Type
A B C : Set U
h1 : ∃ (x : U),
>>  x ∈ A ∩ B
h2 : ∃ (x : U),
>>  x ∈ A ∩ C
h3 : ∃! (x : U), x ∈ A
⊢ ∃ (x : U), x ∈ B ∩ C

We begin by applying the obtain tactic to h1, h2, and h3. In the case of h3, we get an extra given asserting the uniqueness of the element of A. We also write out the definitions of two of the new givens we obtain.

theorem Example_3_6_4 (U : Type) (A B C : Set U)
    (h1 : ∃ (x : U), x ∈ A ∩ B)
    (h2 : ∃ (x : U), x ∈ A ∩ C)
    (h3 : ∃! (x : U), x ∈ A) :
    ∃ (x : U), x ∈ B ∩ C := by
  obtain (b : U) (h4 : b ∈ A ∩ B) from h1
  obtain (c : U) (h5 : c ∈ A ∩ C) from h2
  obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),
    y ∈ A → z ∈ A → y = z)  from h3
  define at h4; define at h5
  **done::

U : Type
A B C : Set U
h1 : ∃ (x : U),
>>  x ∈ A ∩ B
h2 : ∃ (x : U),
>>  x ∈ A ∩ C
h3 : ∃! (x : U), x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (y z : U),
>>  y ∈ A → z ∈ A → y = z
⊢ ∃ (x : U), x ∈ B ∩ C

The key to the rest of the proof is the observation that, by the uniqueness of the element of A, b must be equal to c. To justify this conclusion, note that by two applications of universal instantiation, h7 b c is a proof of b ∈ A → c ∈ A → b = c, and therefore by two applications of modus ponens, h7 b c h4.left h5.left is a proof of b = c.

theorem Example_3_6_4 (U : Type) (A B C : Set U)
    (h1 : ∃ (x : U), x ∈ A ∩ B)
    (h2 : ∃ (x : U), x ∈ A ∩ C)
    (h3 : ∃! (x : U), x ∈ A) :
    ∃ (x : U), x ∈ B ∩ C := by
  obtain (b : U) (h4 : b ∈ A ∩ B) from h1
  obtain (c : U) (h5 : c ∈ A ∩ C) from h2
  obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),
    y ∈ A → z ∈ A → y = z)  from h3
  define at h4; define at h5
  have h8 : b = c := h7 b c h4.left h5.left
  **done::

U : Type
A B C : Set U
h1 : ∃ (x : U),
>>  x ∈ A ∩ B
h2 : ∃ (x : U),
>>  x ∈ A ∩ C
h3 : ∃! (x : U), x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (y z : U),
>>  y ∈ A → z ∈ A → y = z
h8 : b = c
⊢ ∃ (x : U), x ∈ B ∩ C

For our next step, we will need a new tactic. Since we have h8 : b = c, we should be able to replace b with c anywhere it appears. The tactic that allows us to do this called rewrite. If h is a proof of any equation s = t, then rewrite [h] will replace all occurrences of s in the goal with t. Notice that it is the left side of the equation that is replaced with the right side; if you want the replacement to go in the other direction, so that t is replaced with s, you can use rewrite [←h]. (Alternatively, since h.symm is a proof of t = s, you can use rewrite [h.symm].) You can also apply the rewrite tactic to biconditional statements. If you have h : P ↔︎ Q, then rewrite [h] will cause all occurrences of P in the goal to be replaced with Q (and rewrite [←h] will replace Q with P).

As with many other tactics, you can add at h' to specify that the replacement should be done in the given h' rather than the goal. In our case, rewrite [h8] at h4 will change both occurrences of b in h4 to c.

theorem Example_3_6_4 (U : Type) (A B C : Set U)
    (h1 : ∃ (x : U), x ∈ A ∩ B)
    (h2 : ∃ (x : U), x ∈ A ∩ C)
    (h3 : ∃! (x : U), x ∈ A) :
    ∃ (x : U), x ∈ B ∩ C := by
  obtain (b : U) (h4 : b ∈ A ∩ B) from h1
  obtain (c : U) (h5 : c ∈ A ∩ C) from h2
  obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),
    y ∈ A → z ∈ A → y = z)  from h3
  define at h4; define at h5
  have h8 : b = c := h7 b c h4.left h5.left
  rewrite [h8] at h4
  **done::

U : Type
A B C : Set U
h1 : ∃ (x : U),
>>  x ∈ A ∩ B
h2 : ∃ (x : U),
>>  x ∈ A ∩ C
h3 : ∃! (x : U), x ∈ A
b c : U
h4 : c ∈ A ∧ c ∈ B
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (y z : U),
>>  y ∈ A → z ∈ A → y = z
h8 : b = c
⊢ ∃ (x : U), x ∈ B ∩ C

Now the right sides of h4 and h5 tell us that we can prove the goal by plugging in c for x. Here is the complete proof:

theorem Example_3_6_4 (U : Type) (A B C : Set U)
    (h1 : ∃ (x : U), x ∈ A ∩ B)
    (h2 : ∃ (x : U), x ∈ A ∩ C)
    (h3 : ∃! (x : U), x ∈ A) :
    ∃ (x : U), x ∈ B ∩ C := by
  obtain (b : U) (h4 : b ∈ A ∩ B) from h1
  obtain (c : U) (h5 : c ∈ A ∩ C) from h2
  obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),
    y ∈ A → z ∈ A → y = z)  from h3
  define at h4; define at h5
  have h8 : b = c := h7 b c h4.left h5.left
  rewrite [h8] at h4
  show ∃ (x : U), x ∈ B ∩ C from
    Exists.intro c (And.intro h4.right h5.right)
  done

You might want to compare the Lean proof above to the proof of this theorem as it appears in HTPI (HTPI p. 160):

Suppose \(A\), \(B\), and \(C\) are sets, \(A\) and \(B\) are not disjoint, \(A\) and \(C\) are not disjoint, and \(A\) has exactly one element. Then \(B\) and \(C\) are not disjoint

Proof. Since \(A\) and \(B\) are not disjoint, we can let \(b\) be something such that \(b \in A\) and \(b \in B\). Similarly, since \(A\) and \(C\) are not disjoint, there is some object \(c\) such that \(c \in A\) and \(c \in C\). Since \(A\) has only one element, we must have \(b = c\). Thus \(b = c \in B \cap C\) and therefore \(B\) and \(C\) are not disjoint.  □

Before ending this section, we return to the question of how you can tell if a theorem you want to use is in Lean’s library. In an earlier example, we guessed that the commutative law for “or” might be in Lean’s library, and we were then able to use the #check command to confirm it. But there is another technique that we could have used: the tactic apply?, which asks Lean to search through its library of theorems to see if there is one that could be applied to prove the goal. Let’s return to our proof of the theorem union_comm, which started like this:

theorem union_comm {U : Type} (X Y : Set U) :
    X ∪ Y = Y ∪ X := by
  apply Set.ext
  fix x : U
  define : x ∈ X ∪ Y
  define : x ∈ Y ∪ X
  **done::

case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∨ x ∈ Y ↔
>>  x ∈ Y ∨ x ∈ X

Now let’s give the apply? tactic a try.

theorem union_comm {U : Type} (X Y : Set U) :
    X ∪ Y = Y ∪ X := by
  apply Set.ext
  fix x : U
  define : x ∈ X ∪ Y
  define : x ∈ Y ∪ X
  ++apply?::
  done

It takes a few seconds for Lean to search its library of theorems, but eventually a blue squiggle appears under apply?, indicating that the tactic has produced an answer. You will find the answer in the Infoview pane: Try this: exact or_comm. The word exact is the name of a tactic that we have not discussed; it is a shorthand for show _ from, where the blank gets filled in with the goal. Thus, you can think of apply?’s answer as a shortened form of the tactic

show x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X from or_comm

Of course, this is precisely the step we used earlier to complete the proof.

Usually your proof will be more readable if you use the show tactic to state explicitly the goal that is being proven. This also gives Lean a chance to correct you if you have become confused about what goal you are proving. But sometimes—for example, if the goal is very long—it is convenient to use the exact tactic instead. You might think of exact as meaning “the following is a term-mode proof that is exactly what is needed to prove the goal.”

The apply? tactic has not only come up with a suggested tactic, it has applied that tactic, and the proof is now complete. You can confirm that the tactic completes the proof by replacing the line apply? in the proof with apply?’s suggested exact tactic.

The apply? tactic is somewhat unpredictable; sometimes it is able to find the right theorem in the library, and sometimes it isn’t. But it is always worth a try. Another way to try to find theorems is to visit the documentation page for Lean’s mathematics library, which can be found at https://leanprover-community.github.io/mathlib4_docs/.

Exercises

theorem Exercise_3_4_15 (U : Type) (B : Set U) (F : Set (Set U)) :
    ⋃₀ {X : Set U | ∃ (A : Set U), A ∈ F ∧ X = A \ B}
      ⊆ ⋃₀ (F \ 𝒫 B) := sorry

theorem Exercise_3_5_9 (U : Type) (A B : Set U)
    (h1 : 𝒫 (A ∪ B) = 𝒫 A ∪ 𝒫 B) : A ⊆ B ∨ B ⊆ A := by
  --Hint:  Start like this:
  have h2 : A ∪ B ∈ 𝒫 (A ∪ B) := sorry
  **done::

theorem Exercise_3_6_6b (U : Type) :
    ∃! (A : Set U), ∀ (B : Set U), A ∪ B = A := sorry

theorem Exercise_3_6_7b (U : Type) :
    ∃! (A : Set U), ∀ (B : Set U), A ∩ B = A := sorry

theorem Exercise_3_6_8a (U : Type) : ∀ (A : Set U),
    ∃! (B : Set U), ∀ (C : Set U), C \ A = C ∩ B := sorry

theorem Exercise_3_6_10 (U : Type) (A : Set U)
    (h1 : ∀ (F : Set (Set U)), ⋃₀ F = A → A ∈ F) :
    ∃! (x : U), x ∈ A := by
  --Hint:  Start like this:
  set F0 : Set (Set U) := {X : Set U | X ⊆ A ∧ ∃! (x : U), x ∈ X}
  --Now F0 is in the tactic state, with the definition above
  have h2 : ⋃₀ F0 = A := sorry
  
  **done::

3.7. More Examples of Proofs

It is finally time to discuss proofs involving algebraic reasoning. Lean has types for several different kinds of numbers. Nat is the type of natural numbers—that is, the numbers 0, 1, 2, …. Int is the type of integers, Rat is the type of rational numbers, Real is the type of real numbers, and Complex is the type of complex numbers. Lean also uses the notation ℕ, ℤ, ℚ, ℝ, and ℂ for these types. (If you want to use those names for the number types, you can enter them by typing \N, \Z, \Q, \R, and \C.) To write formulas involving arithmetic operations, you should use the symbols + for addition, - for subtraction, * for multiplication, / for division, and ^ for exponentiation. You can enter the symbols ≤, ≥, and ≠ by typing \le, \ge, and \ne, respectively. We will discuss some of the more subtle points of algebraic reasoning in Chapter 6. For the moment, you are best off avoiding subtraction and division when working with natural numbers and avoiding division when working with integers.

To see what’s involved in proving theorems about numbers in Lean, we’ll turn to a few examples from earlier in Chapter 3 of HTPI. We begin with Theorem 3.3.7, which concerns divisibility of integers. As in HTPI, for integers x and y, we will write x ∣ y to mean that x divides y, or y is divisible by x. The formal definition is that x ∣ y means that there is an integer k such that y = x * k. For example, 3 ∣ 12, since 12 = 3 * 4. Lean knows this notation, but there is an important warning: to type the vertical line that means “divides,” you must type \|, not simply |. (There are two slightly different vertical line symbols, and you have to look closely to see that they are different: | and ∣. It is the second one that means “divides” in Lean, and to enter it you must type \|.) Here is Theorem 3.3.7, written using our usual rephrasing of a statement of the form A ∧ B → C as A → B → C.

theorem Theorem_3_3_7 :
    ∀ (a b c : Int), a ∣ b → b ∣ c → a ∣ c := by
  
  **done::

⊢ ∀ (a b c : ℤ),
>>  a ∣ b → b ∣ c → a ∣ c

Of course, we begin the proof by introducing arbitrary integers a, b, and c, and assuming a ∣ b and b ∣ c. We also write out the definitions of our assumptions and the goal.

theorem Theorem_3_3_7 :
    ∀ (a b c : Int), a ∣ b → b ∣ c → a ∣ c := by
  fix a : Int; fix b : Int; fix c : Int
  assume h1 : a ∣ b; assume h2 : b ∣ c
  define at h1; define at h2; define
  **done::

a b c : ℤ
h1 : ∃ (c : ℤ),
>>  b = a * c
h2 : ∃ (c_1 : ℤ),
>>  c = b * c_1
⊢ ∃ (c_1 : ℤ),
>>  c = a * c_1

We always use existential givens right away, so we use h1 and h2 to introduce two new variables, m and n.

theorem Theorem_3_3_7 :
    ∀ (a b c : Int), a ∣ b → b ∣ c → a ∣ c := by
  fix a : Int; fix b : Int; fix c : Int
  assume h1 : a ∣ b; assume h2 : b ∣ c
  define at h1; define at h2; define
  obtain (m : Int) (h3 : b = a * m) from h1
  obtain (n : Int) (h4 : c = b * n) from h2
  **done::

a b c : ℤ
h1 : ∃ (c : ℤ),
>>  b = a * c
h2 : ∃ (c_1 : ℤ),
>>  c = b * c_1
m : ℤ
h3 : b = a * m
n : ℤ
h4 : c = b * n
⊢ ∃ (c_1 : ℤ),
>>  c = a * c_1

If we substitute the value for b given in h3 into h4, we will see how to reach the goal. Of course, the rewrite tactic is what we need for this.

theorem Theorem_3_3_7 :
    ∀ (a b c : Int), a ∣ b → b ∣ c → a ∣ c := by
  fix a : Int; fix b : Int; fix c : Int
  assume h1 : a ∣ b; assume h2 : b ∣ c
  define at h1; define at h2; define
  obtain (m : Int) (h3 : b = a * m) from h1
  obtain (n : Int) (h4 : c = b * n) from h2
  rewrite [h3] at h4   --h4 : c = a * m * n
  **done::

a b c : ℤ
h1 : ∃ (c : ℤ),
>>  b = a * c
h2 : ∃ (c_1 : ℤ),
>>  c = b * c_1
m : ℤ
h3 : b = a * m
n : ℤ
h4 : c = a * m * n
⊢ ∃ (c_1 : ℤ),
>>  c = a * c_1

Looking at h4, we see that the value we should use for c_1 in the goal is m * n.

theorem Theorem_3_3_7 :
    ∀ (a b c : Int), a ∣ b → b ∣ c → a ∣ c := by
  fix a : Int; fix b : Int; fix c : Int
  assume h1 : a ∣ b; assume h2 : b ∣ c
  define at h1; define at h2; define
  obtain (m : Int) (h3 : b = a * m) from h1
  obtain (n : Int) (h4 : c = b * n) from h2
  rewrite [h3] at h4   --h4 : c = a * m * n
  apply Exists.intro (m * n)
  **done::

a b c : ℤ
h1 : ∃ (c : ℤ),
>>  b = a * c
h2 : ∃ (c_1 : ℤ),
>>  c = b * c_1
m : ℤ
h3 : b = a * m
n : ℤ
h4 : c = a * m * n
⊢ c = a * (m * n)

Note that in the application of Exists.intro, the parentheses around m * n are necessary to help Lean parse the line correctly. Comparing h4 to the goal, you might think that we can finish the proof with show c = a * (m * n) from h4. But if you try it, you will get an error message. What’s the problem? The difference in the parentheses is the clue. Lean groups the arithmetic operations +, -, *, and / to the left, so h4 means h4 : c = (a * m) * n, which is not quite the same as the goal. To prove the goal, we will need to apply the associative law for multiplication.

We have already seen that and_assoc is Lean’s name for the associative law for “and”. Perhaps you can guess that the name for the associative law for multiplication is mul_assoc. If you type #check @mul_assoc, Lean’s response will be:

@mul_assoc : ∀ {G : Type u_1} [inst : Semigroup G] (a b c : G),
              a * b * c = a * (b * c)

The implicit arguments in this cases are a little complicated (the expression [inst : Semigroup G] represents yet another kind of implicit argument). But what they mean is that mul_assoc can be used to prove any statement of the form ∀ (a b c : G), a * b * c = a * (b * c), as long as G is a type that has an associative multiplication operation. In particular, mul_assoc can be used as a proof of ∀ (a b c : Int), a * b * c = a * (b * c). (There are also versions of this theorem for particular number types. You can use the #check command to verify the theorems Nat.mul_assoc : ∀ (a b c : ℕ), a * b * c = a * (b * c), Int.mul_assoc : ∀ (a b c : ℤ), a * b * c = a * (b * c), and so on.)

Returning to our proof of Theorem 3.3.7, by three applications of universal instantiation, mul_assoc a m n is a proof of a * m * n = a * (m * n), and that is exactly what we need to finish the proof. The tactic rewrite [mul_assoc a m n] at h4 will replace a * m * n in h4 with a * (m * n).

theorem Theorem_3_3_7 :
    ∀ (a b c : Int), a ∣ b → b ∣ c → a ∣ c := by
  fix a : Int; fix b : Int; fix c : Int
  assume h1 : a ∣ b; assume h2 : b ∣ c
  define at h1; define at h2; define
  obtain (m : Int) (h3 : b = a * m) from h1
  obtain (n : Int) (h4 : c = b * n) from h2
  rewrite [h3] at h4   --h4 : c = a * m * n
  apply Exists.intro (m * n)
  rewrite [mul_assoc a m n] at h4
  **done::

a b c : ℤ
h1 : ∃ (c : ℤ),
>>  b = a * c
h2 : ∃ (c_1 : ℤ),
>>  c = b * c_1
m : ℤ
h3 : b = a * m
n : ℤ
h4 : c = a * (m * n)
⊢ c = a * (m * n)

By the way, this is a case in which Lean could have figured out some details on its own. If we had used rewrite [mul_assoc _ _ _] at h4, then Lean would have figured out that the blanks had to be filled in with a, m, and n. And as with the apply tactic, blanks at the end of rewrite rules can be left out, so even rewrite [mul_assoc] at h4 would have worked.

Of course, now h4 really does match the goal exactly, so we can use it to complete the proof.

theorem Theorem_3_3_7 :
    ∀ (a b c : Int), a ∣ b → b ∣ c → a ∣ c := by
  fix a : Int; fix b : Int; fix c : Int
  assume h1 : a ∣ b; assume h2 : b ∣ c
  define at h1; define at h2; define
  obtain (m : Int) (h3 : b = a * m) from h1
  obtain (n : Int) (h4 : c = b * n) from h2
  rewrite [h3] at h4   --h4 : c = a * m * n
  apply Exists.intro (m * n)
  rewrite [mul_assoc a m n] at h4
  show c = a * (m * n) from h4
  done

As usual, you might find it instructive to compare the Lean proof above to the proof of this theorem in HTPI.

For our next example, we’ll do a somewhat more complex proof concerning divisibility. Here is the proof from HTPI (HTPI p. 139).

For every integer \(n\), \(6 \mid n\) iff \(2 \mid n\) and \(3 \mid n\).

Proof. Let \(n\) be an arbitrary integer.

(\(\to\)) Suppose \(6 \mid n\). Then we can choose an integer \(k\) such that \(6k=n\). Therefore \(n = 6k = 2(3k)\), so \(2 \mid n\), and similarly \(n = 6k = 3(2k)\), so \(3 \mid n\).

(\(\leftarrow\)) Suppose \(2 \mid n\) and \(3 \mid n\). Then we can choose integers \(j\) and \(k\) such that \(n = 2j\) and \(n = 3k\). Therefore \(6(j-k) = 6j - 6k = 3(2j) - 2(3k) = 3n - 2n = n\), so \(6 \mid n\).  □

Let’s try writing the proof in Lean. We use exactly the same strategy as in the HTPI proof: we begin by fixing an arbitrary integer n, and then we prove the two directions of the biconditional separately.

theorem Theorem_3_4_7 :
    ∀ (n : Int), 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n := by
  fix n : Int
  apply Iff.intro
  **done::

case mp
n : ℤ
⊢ 6 ∣ n → 2 ∣ n ∧ 3 ∣ n
case mpr
n : ℤ
⊢ 2 ∣ n ∧ 3 ∣ n → 6 ∣ n

For the left-to-right direction, we assume 6 ∣ n, and since the definition of this assumption is an existential statement, we immediately apply existential instantiation.

theorem Theorem_3_4_7 :
    ∀ (n : Int), 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n := by
  fix n : Int
  apply Iff.intro
  · -- (→)
    assume h1 : 6 ∣ n; define at h1
    obtain (k : Int) (h2 : n = 6 * k) from h1
    **done::
  · -- (←)

    **done::
  done

case mp
n : ℤ
h1 : ∃ (c : ℤ),
>>  n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 2 ∣ n ∧ 3 ∣ n

Our goal is now a conjunction, so we prove the two conjuncts separately. Focusing just on the first one, 2 ∣ n, we write out the definition to decide how to proceed.

theorem Theorem_3_4_7 :
    ∀ (n : Int), 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n := by
  fix n : Int
  apply Iff.intro
  · -- (→)
    assume h1 : 6 ∣ n; define at h1
    obtain (k : Int) (h2 : n = 6 * k) from h1
    apply And.intro
    · -- Proof that 2 ∣ n
      define
      **done::
    · -- Proof that 3 ∣ n

      **done::
    done
  · -- (←)

    **done::
  done

case mp.left
n : ℤ
h1 : ∃ (c : ℤ),
>>  n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ ∃ (c : ℤ), n = 2 * c

Since we have n = 6 * k = 2 * 3 * k, it looks like 3 * k is the value we should use for c.

theorem Theorem_3_4_7 :
    ∀ (n : Int), 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n := by
  fix n : Int
  apply Iff.intro
  · -- (→)
    assume h1 : 6 ∣ n; define at h1
    obtain (k : Int) (h2 : n = 6 * k) from h1
    apply And.intro
    · -- Proof that 2 ∣ n
      define
      apply Exists.intro (3 * k)
      **done::
    · -- Proof that 3 ∣ n

      **done::
    done
  · -- (←)

    **done::
  done

case mp.left
n : ℤ
h1 : ∃ (c : ℤ),
>>  n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 2 * (3 * k)

Once again, if you think carefully about it, you will see that in order to deduce the goal from h2, we will need to use the associativity of multiplication to rewrite the goal as n = 2 * 3 * k. As we have already seen, mul_assoc 2 3 k is a proof of 2 * 3 * k = 2 * (3 * k). Since we want to replace the right side of this equation with the left in the goal, we’ll use the tactic rewrite [←mul_assoc 2 3 k].

theorem Theorem_3_4_7 :
    ∀ (n : Int), 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n := by
  fix n : Int
  apply Iff.intro
  · -- (→)
    assume h1 : 6 ∣ n; define at h1
    obtain (k : Int) (h2 : n = 6 * k) from h1
    apply And.intro
    · -- Proof that 2 ∣ n
      define
      apply Exists.intro (3 * k)
      rewrite [←mul_assoc 2 3 k]
      **done::
    · -- Proof that 3 ∣ n

      **done::
    done
  · -- (←)

    **done::
  done

case mp.left
n : ℤ
h1 : ∃ (c : ℤ),
>>  n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 2 * 3 * k

Do we have to convince Lean that 2 * 3 = 6? No, remember that Lean works out definitions on its own. Lean knows the definition of multiplication, and it knows that, according to that definition, 2 * 3 is equal to 6. So it regards n = 6 * k and n = 2 * 3 * k as definitionally equal, and therefore it will recognize h2 as a proof of the goal.

theorem Theorem_3_4_7 :
    ∀ (n : Int), 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n := by
  fix n : Int
  apply Iff.intro
  · -- (→)
    assume h1 : 6 ∣ n; define at h1
    obtain (k : Int) (h2 : n = 6 * k) from h1
    apply And.intro
    · -- Proof that 2 ∣ n
      define
      apply Exists.intro (3 * k)
      rewrite [←mul_assoc 2 3 k]
      show n = 2 * 3 * k from h2
      done
    · -- Proof that 3 ∣ n

      **done::
    done
  · -- (←)

    **done::
  done

case mp.right
n : ℤ
h1 : ∃ (c : ℤ),
>>  n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 3 ∣ n

The proof of the next goal, 3 ∣ n, is similar, and it completes the left-to-right direction of the biconditional.

theorem Theorem_3_4_7 :
    ∀ (n : Int), 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n := by
  fix n : Int
  apply Iff.intro
  · -- (→)
    assume h1 : 6 ∣ n; define at h1
    obtain (k : Int) (h2 : n = 6 * k) from h1
    apply And.intro
    · -- Proof that 2 ∣ n
      define
      apply Exists.intro (3 * k)
      rewrite [←mul_assoc 2 3 k]
      show n = 2 * 3 * k from h2
      done
    · -- Proof that 3 ∣ n
      define
      apply Exists.intro (2 * k)
      rewrite [←mul_assoc 3 2 k]
      show n = 3 * 2 * k from h2
      done
    done
  · -- (←)

    **done::
  done

case mpr
n : ℤ
⊢ 2 ∣ n ∧ 3 ∣ n → 6 ∣ n

For the right-to-left direction, we begin by assuming 2 ∣ n ∧ 3 ∣ n. We write out the definitions of 2 ∣ n and 3 ∣ n, and since this gives us two existential givens, we apply existential instantiation twice. To save space, we won’t repeat the proof of the first half of the proof in the displays below.

theorem Theorem_3_4_7 :
    ∀ (n : Int), 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n := by
  fix n : Int
  apply Iff.intro
  · -- (→)
    ...
  · -- (←)
    assume h1 : 2 ∣ n ∧ 3 ∣ n
    have h2 : 2 ∣ n := h1.left
    have h3 : 3 ∣ n := h1.right
    define at h2; define at h3; define
    obtain (j : Int) (h4 : n = 2 * j) from h2
    obtain (k : Int) (h5 : n = 3 * k) from h3
    **done::
  done

case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ (c : ℤ),
>>  n = 2 * c
h3 : ∃ (c : ℤ),
>>  n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ ∃ (c : ℤ),
>>  n = 6 * c

The next step in the HTPI proof is a string of equations that proves \(6(j - k) = n\), which establishes that \(6 \mid n\). Let’s try to do the same thing in Lean, using a calculational proof:

theorem ??Theorem_3_4_7:: :
    ∀ (n : Int), 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n := by
  fix n : Int
  apply Iff.intro
  · -- (→)
    ...
  · -- (←)
    assume h1 : 2 ∣ n ∧ 3 ∣ n
    have h2 : 2 ∣ n := h1.left
    have h3 : 3 ∣ n := h1.right
    define at h2; define at h3; define
    obtain (j : Int) (h4 : n = 2 * j) from h2
    obtain (k : Int) (h5 : n = 3 * k) from h3
    have h6 : 6 * (j - k) = n :=
      calc 6 * (j - k)
        _ = 6 * j - 6 * k := sorry
        _ = 3 * (2 * j) - 2 * (3 * k) := sorry
        _ = 3 * n - 2 * n := sorry
        _ = (3 - 2) * n := sorry
        _ = n := sorry
    show ∃ (c : Int), n = 6 * c from
      Exists.intro (j - k) h6.symm
    done
  done

No goals

Sometimes the easiest way to write a calculational proof is to justify each line with sorry and then go back and fill in real justifications. Lean has accepted the proof above, so we know that we’ll have a complete proof if we can replace each sorry with a justification.

To justify the first line of the calculational proof, try replacing sorry with by apply?. Lean comes up with a justification: Int.mul_sub 6 j k. The command #check @Int.mul_sub tells us that the theorem Int.mul_sub means

Int.mul_sub : ∀ (a b c : ℤ), a * (b - c) = a * b - a * c

Thus, we can fill in Int.mul_sub 6 j k as a proof of the first equation.

It looks like we’ll have to use the associativity of multiplication again to prove the second equation, but it will take more than one step. Let’s try writing a tactic-mode proof. In the display below, we’ll just focus on the calculational proof.

have h6 : 6 * (j - k) = n :=
  calc 6 * (j - k)
    _ = 6 * j - 6 * k := Int.mul_sub 6 j k
    _ = 3 * (2 * j) - 2 * (3 * k) := by

          **done::
    _ = 3 * n - 2 * n := sorry
    _ = (3 - 2) * n := sorry
    _ = n := sorry

n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ (c : ℤ),
>>  n = 2 * c
h3 : ∃ (c : ℤ),
>>  n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ 6 * j - 6 * k =
>>  3 * (2 * j) -
>>    2 * (3 * k)

To justify the second equation, we’ll have to use associativity to rewrite both 3 * (2 * j) as 3 * 2 * j and also 2 * (3 * k) as 2 * 3 * k. So we apply the rewrite tactic to both of the proofs mul_assoc 3 2 j : 3 * 2 * j = 3 * (2 * j) and mul_assoc 2 3 k : 2 * 3 * k = 2 * (3 * k):

have h6 : 6 * (j - k) = n :=
  calc 6 * (j - k)
    _ = 6 * j - 6 * k := Int.mul_sub 6 j k
    _ = 3 * (2 * j) - 2 * (3 * k) := by
          rewrite [←mul_assoc 3 2 j]
          rewrite [←mul_assoc 2 3 k]
          **done::
    _ = 3 * n - 2 * n := sorry
    _ = (3 - 2) * n := sorry
    _ = n := sorry

n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ (c : ℤ),
>>  n = 2 * c
h3 : ∃ (c : ℤ),
>>  n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ 6 * j - 6 * k =
>>  3 * 2 * j - 
>>    2 * 3 * k

To finish off the justification of the second equation, we’ll use the theorem Eq.refl. The command #check @Eq.refl gives the result

@Eq.refl : ∀ {α : Sort u_1} (a : α), a = a

Ignoring the implicit argument α, this should remind you of the theorem Iff.refl : ∀ (a : Prop), a ↔︎ a. Recall that we were able to use Iff.refl _ to prove not only any statement of the form a ↔︎ a, but also statements of the form a ↔︎ a', where a and a' are definitionally equal. Similarly, Eq.refl _ will prove any equation of the form a = a', where a and a' are definitionally equal. Since Lean knows that, by definition, 3 * 2 = 6 and 2 * 3 = 6, the goal has this form. Thus we can complete the proof with the tactic show 6 * j - 6 * k = 3 * 2 * j - 2 * 3 * k from Eq.refl _. As we saw earlier, a shorter version of this would be exact Eq.refl _. But this situation comes up often enough that there is an even shorter version: the tactic rfl can be used as a shorthand for either exact Eq.refl _ or exact Iff.refl _. In other words, in a tactic-mode proof, if the goal has one of the forms a = a' or a ↔︎ a', where a and a' are definitionally equal, then the tactic rfl will prove the goal. So rfl will finish off the justification of the second equation, and we can move on to the third.

have h6 : 6 * (j - k) = n :=
  calc 6 * (j - k)
    _ = 6 * j - 6 * k := Int.mul_sub 6 j k
    _ = 3 * (2 * j) - 2 * (3 * k) := by
          rewrite [←mul_assoc 3 2 j]
          rewrite [←mul_assoc 2 3 k]
          rfl
          done
    _ = 3 * n - 2 * n := by

          **done::
    _ = (3 - 2) * n := sorry
    _ = n := sorry

n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ (c : ℤ),
>>  n = 2 * c
h3 : ∃ (c : ℤ),
>>  n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ 3 * (2 * j) -
>>  2 * (3 * k) =
>>    3 * n - 2 * n

To justify the third equation we have to substitute n for both 2 * j and 3 * k. We can use h4 and h5 in the rewrite tactic to do this. In fact, we can do it in one step: you can put a list of proofs of equations or biconditionals inside the brackets, and the rewrite tactic will perform all of the replacements, one after another. In our case, the tactic rewrite [←h4, ←h5] will first replace 2 * j in the goal with n, and then it will replace 3 * k with n.

have h6 : 6 * (j - k) = n :=
  calc 6 * (j - k)
    _ = 6 * j - 6 * k := Int.mul_sub 6 j k
    _ = 3 * (2 * j) - 2 * (3 * k) := by
          rewrite [←mul_assoc 3 2 j]
          rewrite [←mul_assoc 2 3 k]
          rfl
          done
    _ = 3 * n - 2 * n := by
          rewrite [←h4, ←h5]
          **done::
    _ = (3 - 2) * n := sorry
    _ = n := sorry

n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ (c : ℤ),
>>  n = 2 * c
h3 : ∃ (c : ℤ),
>>  n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ 3 * n - 2 * n =
>>  3 * n - 2 * n

Of course, the rfl tactic will now finish off the justification of the third equation.

The fourth equation is 3 * n - 2 * n = (3 - 2) * n. It looks like the algebraic law we need to justify this is a lot like the one that was used in the first equation, but with the multiplication to the right of the subtraction rather than to the left. It shouldn’t be surprising, therefore, that the name of the theorem we need is Int.sub_mul. The command #check @Int.sub_mul gives the response

Int.sub_mul : ∀ (a b c : ℤ), (a - b) * c = a * c - b * c

so Int.sub_mul 3 2 n is a proof of (3 - 2) * n = 3 * n - 2 * n. But the fourth equation has the sides of this equation reversed, so to justify it we need (Int.sub_mul 3 2 n).symm.

Finally, the fifth equation is (3 - 2) * n = n. Why is this true? Because it is definitionally equal to 1 * n = n. Is there a theorem to justify this last equation? One way to find the answer is to type in this example:

example (n : Int) : 1 * n = n := by ++apply?::

Lean responds with exact Int.one_mul n, and #check @Int.one_mul yields

Int.one_mul : ∀ (a : ℤ), 1 * a = a

So Int.one_mul n should justify the last equation. Here’s the complete calculational proof, where we have shortened the second step a bit by doing both rewrites in one step. When a tactic proof is short enough that it can be written on one line, we generally leave off done.

have h6 : 6 * (j - k) = n :=
  calc 6 * (j - k)
    _ = 6 * j - 6 * k := Int.mul_sub 6 j k
    _ = 3 * (2 * j) - 2 * (3 * k) := by
          rewrite [←mul_assoc 3 2 j, ←mul_assoc 2 3 k]; rfl
    _ = 3 * n - 2 * n := by rewrite [←h4, ←h5]; rfl
    _ = (3 - 2) * n := (Int.sub_mul 3 2 n).symm
    _ = n := Int.one_mul n

Whew! This example illustrates why algebraic reasoning in Lean can be difficult. But one reason why this proof was challenging is that we justified all of our steps from basic algebraic principles. Fortunately, there are more powerful tactics that can automate some algebraic reasoning. For example, the tactic ring can combine algebraic laws involving addition, subtraction, multiplication, and exponentiation with natural number exponents to prove many equations in one step. Also, the tactic rw is a variant of rewrite that automatically applies rfl after the rewriting if it can be used to finish the proof. Here’s a shortened version of our calculational proof that uses these tactics.

have h6 : 6 * (j - k) = n :=
  calc 6 * (j - k)
    _ = 3 * (2 * j) - 2 * (3 * k) := by ring
    _ = 3 * n - 2 * n := by rw [←h4, ←h5]
    _ = n := by ring

By the way, the theorems Int.mul_sub, Int.sub_mul, and Int.one_mul that we used earlier are the integer versions of more general theorems mul_sub, sub_mul, and one_mul. The #check command tells us what these general theorems say:

@mul_sub : ∀ {α : Type u_1} [inst : NonUnitalNonAssocRing α]
            (a b c : α), a * (b - c) = a * b - a * c

@sub_mul : ∀ {α : Type u_1} [inst : NonUnitalNonAssocRing α]
            (a b c : α), (a - b) * c = a * c - b * c

@one_mul : ∀ {M : Type u_1} [inst : MulOneClass M]
            (a : M), 1 * a = a

The implicit arguments say that these theorems apply in any number system with the appropriate algebraic properties. We’ll use the third theorem in our next example, which involves algebraic reasoning about real numbers. You can use the #check command to find the meanings of the other theorems we use in this proof.

theorem Example_3_5_4 (x : Real) (h1 : x ≤ x ^ 2) : x ≤ 0 ∨ 1 ≤ x := by
  or_right with h2     --h2 : ¬x ≤ 0;  Goal : 1 ≤ x
  have h3 : 0 < x := lt_of_not_le h2
  have h4 : 1 * x ≤ x * x :=
    calc 1 * x
      _ = x := one_mul x
      _ ≤ x ^ 2 := h1
      _ = x * x := by ring
  show 1 ≤ x from le_of_mul_le_mul_right h4 h3
  done

Exercises

theorem Exercise_3_3_18a (a b c : Int)
    (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := sorry

2. Complete the following proof by justifying the steps in the calculational proof. Remember that you can use the tactic demorgan : ... to apply one of De Morgan’s laws to just a part of the goal. You may also find the theorem and_or_left useful. (Use #check to see what the theorem says.)

theorem Exercise_3_4_6 (U : Type) (A B C : Set U) :
    A \ (B ∩ C) = (A \ B) ∪ (A \ C) := by
  apply Set.ext
  fix x : U
  show x ∈ A \ (B ∩ C) ↔ x ∈ A \ B ∪ A \ C from
    calc x ∈ A \ (B ∩ C)
      _ ↔ x ∈ A ∧ ¬(x ∈ B ∧ x ∈ C) := sorry
      _ ↔ x ∈ A ∧ (x ∉ B ∨ x ∉ C) := sorry  
      _ ↔ (x ∈ A ∧ x ∉ B) ∨ (x ∈ A ∧ x ∉ C) := sorry
      _ ↔ x ∈ (A \ B) ∪ (A \ C) := sorry
  done

For the next exercise you will need the following definitions:

def even (n : Int) : Prop := ∃ (k : Int), n = 2 * k

def odd (n : Int) : Prop := ∃ (k : Int), n = 2 * k + 1

These definitions tell Lean that if n has type Int, then even n means ∃ (k : Int), n = 2 * k and odd n means ∃ (k : Int), n = 2 * k + 1.

theorem Exercise_3_4_10 (x y : Int)
    (h1 : odd x) (h2 : odd y) : even (x - y) := sorry

theorem Exercise_3_4_27a :
    ∀ (n : Int), 15 ∣ n ↔ 3 ∣ n ∧ 5 ∣ n := sorry

theorem Like_Exercise_3_7_5 (U : Type) (F : Set (Set U))
    (h1 : 𝒫 (⋃₀ F) ⊆ ⋃₀ {𝒫 A | A ∈ F}) :
    ∃ (A : Set U), A ∈ F ∧ ∀ (B : Set U), B ∈ F → B ⊆ A := sorry