Chap3.qmd

# 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`:

::: {.lftrt}
::: {.bef}
```state
>> ⋮
⊢ P → Q
```
:::

::: {.aft}
```state
>> ⋮
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:

::: {.lftrt}
::: {.bef}
```state
>> ⋮
⊢ P → Q
```
:::

::: {.aft}
```state
>> ⋮
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:

::: {.lftrt}
::: {.bef}
```state
>> ⋮
⊢ ¬P
```
:::

::: {.aft}
```state
>> ⋮
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:

::: {style="margin: 0% 20%"}
| `Q` | `¬Q` | `(Q` | `→` | `False)`|
|:----------:|:----------:|-:|:-:|:-|
| F | T | F | T |   [ ]{.excl} F |
| T | F | T | F |   [ ]{.excl} 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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`:

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`:

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`:

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```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::
```
:::

::: {.outpt}
```state
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`:

::: {.inout}
::: {.inpt}
```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
  apply h3 _
  **done::
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```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
  apply h3 _
  define at h2
  demorgan at h2; conditional at h2
  **done::
```
:::

::: {.outpt}
```state
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`:

::: {.inout}
::: {.inpt}
```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
  apply h3 _
  define at h2
  demorgan at h2; conditional at h2
  show a ∈ B from h2 h1
  done
```
:::

::: {.outpt}
```state
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*.

::: {.numex arguments="1"}
```lean
theorem Exercise_3_2_1a (P Q R : Prop)
    (h1 : P → Q) (h2 : Q → R) : P → R := by
  
  **done::
```
:::

::: {.numex arguments="2"}
```lean
theorem Exercise_3_2_1b (P Q R : Prop)
    (h1 : ¬R → (P → ¬Q)) : P → (Q → R) := by
  
  **done::
```
:::

::: {.numex arguments="3"}
```lean
theorem Exercise_3_2_2a (P Q R : Prop)
    (h1 : P → Q) (h2 : R → ¬Q) : P → ¬R := by
  
  **done::
```
:::

::: {.numex arguments="4"}
```lean
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`:

::: {.ind}
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:

::: {.lftrt}
::: {.bef}
```state
>> ⋮
⊢ ∀ (x : U), P x
```
:::

::: {.aft}
```state
>> ⋮
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`:

::: {.ind}
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 example, you can enter the symbol `∀` by typing `\forall` or `\all`, and you can enter `∃` by typing `\exists` or `\ex`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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:

::: {style="margin: 0% 10%"}
| | `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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {style="margin: 0% 10%"}
| Symbol | How To Type It |
|:----:|:-------:|
| `∈` | `\in` |
| `∉` | `\notin` or `\inn` |
| `⊆` | `\sub` |
| `⊈` | `\subn` |
| `=` | `=` |
| `≠` | `\ne` |
| `∪` | `\union` or `\cup` |
| `∩` | `\inter` or `\cap` |
| `\` | `\\` |
| `∆` | `\symmdiff` |
| `∅` | `\emptyset` |
| `𝒫` | `\powerset` |
:::

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

::: {.inout}
::: {.inpt}
```lean
example (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ∀ (x : U), x ∈ A → x ∉ B) : A ⊆ C := by
  
  **done::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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`:

::: {.ind}
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:

::: {.lftrt}
::: {.bef}
```state
>> ⋮
a : U
⊢ ∃ (x : U), P x
```
:::

::: {.aft}
```state
>> ⋮
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`:

::: {.ind}
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.)

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
theorem Example_3_3_5 (U : Type) (B : Set U)
    (F : Set (Set U)) : ⋃₀ F ⊆ B → F ⊆ 𝒫 B := by
  
  **done::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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 _`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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):

::: {.thm}
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. [ □]{.excl}\qedhere
:::

### Exercises

::: {.numex arguments="1"}
```lean
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::
```
:::

::: {.numex arguments="2"}
```lean
theorem Exercise_3_3_8 (U : Type) (F : Set (Set U)) (A : Set U)
    (h1 : A ∈ F) : A ⊆ ⋃₀ F := by
  
  **done::
```
:::

::: {.numex arguments="3"}
```lean
theorem Exercise_3_3_9 (U : Type) (F : Set (Set U)) (A : Set U)
    (h1 : A ∈ F) : ⋂₀ F ⊆ A := by
  
  **done::
```
:::

::: {.numex arguments="4"}
```lean
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::
```
:::

::: {.numex arguments="5"}
```lean
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`:

::: {.ind}
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`:

::: {.ind}
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*

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.  

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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).

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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`:

::: {.ind}
Prove `P → Q` and `Q → P` separately.
:::

#### To use a given of the form `P ↔ Q`:

::: {.ind}
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.

::: {.inout}
::: {.inpt}
```lean
example (U : Type) (P Q : Pred U)
    (h1 : ∀ (x : U), P x ↔ Q x) :
    (∃ (x : U), P x) ↔ ∃ (x : U), Q x := by
  
  **done::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

```lean
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).

::: {.thm}
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$. [ □]{.excl}\qedhere
:::

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.

```lean
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

```lean
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:

::: {.ind}
```
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

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

which is shorthand for

::: {.ind}
```
@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

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

which is shorthand for

::: {.ind}
```
@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

::: {.numex arguments="1"}
```lean
theorem Exercise_3_4_2 (U : Type) (A B C : Set U)
    (h1 : A ⊆ B) (h2 : A ⊆ C) : A ⊆ B ∩ C := by
  
  **done::
```
:::

::: {.numex arguments="2"}
```lean
theorem Exercise_3_4_4 (U : Type) (A B C : Set U)
    (h1 : A ⊆ B) (h2 : A ⊈ C) : B ⊈ C := by
  
  **done::
```
:::

::: {.numex arguments="3"}
```lean
theorem Exercise_3_3_16 (U : Type) (B : Set U)
    (F : Set (Set U)) : F ⊆ 𝒫 B → ⋃₀ F ⊆ B := by
  
  **done::
```
:::

::: {.numex arguments="4"}
```lean
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::
```
:::

::: {.numex arguments="5"}
```lean
theorem Exercise_3_4_7 (U : Type) (A B : Set U) :
    𝒫 (A ∩ B) = 𝒫 A ∩ 𝒫 B := by

  **done::
```
:::

::: {.numex arguments="6"}
```lean
theorem Exercise_3_4_17 (U : Type) (A : Set U) : A = ⋃₀ (𝒫 A) := by

  **done::
```
:::

::: {.numex arguments="7"}
```lean
theorem Exercise_3_4_18a (U : Type) (F G : Set (Set U)) :
    ⋃₀ (F ∩ G) ⊆ (⋃₀ F) ∩ (⋃₀ G) := by
  
  **done::
```
:::

::: {.numex arguments="8"}
```lean
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`:

::: {.ind}
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:

::: {.lftrt}
::: {.bef}
```state
>> ⋮
h : P ∨ Q
⊢ goal
```
:::

::: {.aft}
```state
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:

::: {.ind}
```
@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`:

::: {.ind}
Break your proof into cases.  In each case, either prove `P` or prove `Q`.
:::

Example 3.5.2 from *HTPI* illustrates these strategies:

::: {.inout}
::: {.inpt}
```lean
theorem Example_3_5_2
    (U : Type) (A B C : Set U) :
    A \ (B \ C) ⊆ (A \ B) ∪ C := by

  **done::
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```lean
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

```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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

```
:::

::: {.outpt}
```state
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`

::: {.inout}
::: {.inpt}
```lean
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

```
:::

::: {.outpt}
```state
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`:

::: {.ind}
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`:

::: {.lftrt}
::: {.bef}
```state
>> ⋮
⊢ P ∨ Q
```
:::

::: {.aft}
```state
>> ⋮
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.

::: {.inout}
::: {.inpt}
```lean
example (U : Type) (A B C : Set U)
    (h1 : A \ B ⊆ C) : A ⊆ B ∪ C := by
  
  **done::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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`:

::: {.ind}
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.

::: {.inout}
::: {.inpt}
```lean
example
    (U : Type) (A B C : Set U) (h1 : A ⊆ B ∪ C)
    (h2 : ¬∃ (x : U), x ∈ A ∩ B) : A ⊆ C := by

  **done::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
??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
```
:::

::: {.outpt}
```state
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."

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.numex arguments="1"}
```lean
theorem Exercise_3_5_2 (U : Type) (A B C : Set U) :
    (A ∪ B) \ C ⊆ A ∪ (B \ C) := sorry
```
:::

::: {.numex arguments="2"}
```lean
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
```
:::

::: {.numex arguments="3"}
```lean
theorem Exercise_3_5_7 (U : Type) (A B C : Set U) :
    A ∪ C ⊆ B ∪ C ↔ A \ C ⊆ B \ C := sorry
```
:::

::: {.numex arguments="4"}
```lean
theorem Exercise_3_5_8 (U : Type) (A B : Set U) :
    𝒫 A ∪ 𝒫 B ⊆ 𝒫 (A ∪ B) := sorry
```
:::

::: {.numex arguments="5"}
```lean
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
```
:::

::: {.numex arguments="6"}
```lean
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
```
:::

::: {.numex arguments="7"}
```lean
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`:

::: {.ind}
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):

::: {.thm}
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$. [ □]{.excl}\qedhere
:::

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`.

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

::: {.outpt}
```state
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.

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

    **done::
  · -- (←)

    **done::
  done
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
theorem union_comm {U : Type} (X Y : Set U) :
    X ∪ Y = Y ∪ X := by
  
  **done::
```
:::

::: {.outpt}
```state
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`.

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

::: {.outpt}
```state
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.)

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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:

::: {.ind}
```
@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:

::: {.inout}
::: {.inpt}
```lean
theorem Example_3_6_2 (U : Type) :
    ∃! (A : Set U), ∀ (B : Set U),
    A ∪ B = B := by

  **done::

```
:::

::: {.outpt}
```state
U : Type
⊢ ∃! (A : Set U),
>>  ∀ (B : Set U),
>>    A ∪ B = B
```
:::
:::

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

::: {.inout}
::: {.inpt}
```lean
theorem Example_3_6_2 (U : Type) :
    ∃! (A : Set U), ∀ (B : Set U),
    A ∪ B = B := by
  exists_unique
  **done::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```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

    **done::
  done
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```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
    **done::
  done
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```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
```
:::

::: {.outpt}
```state
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:

```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 
    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`:

::: {.ind}
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)` <br>`(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*.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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:

```lean
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):

::: {.thm}
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. [&nbsp;□]{.excl}\qedhere
:::

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:

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

```lean
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

::: {.ind}
```
show x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X from Or.comm
```
:::

The command `#check @Or.comm` will tell you that `Or.comm` is just an alternative name for the theorem `or_comm`.  So the step suggested by the `apply?` tactic is essentially the same as 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.  There are also tools available on the internet for searching Lean's library, including [LeanSearch](https://leansearch.net), [Moogle](https://www.moogle.ai), and [Loogle](https://loogle.lean-lang.org). 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/](https://leanprover-community.github.io/mathlib4_docs/).

### Exercises

::: {.numex arguments="1"}
```lean
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
```
:::

::: {.numex arguments="2"}
```lean
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::
```
:::

::: {.numex arguments="3"}
```lean
theorem Exercise_3_6_6b (U : Type) :
    ∃! (A : Set U), ∀ (B : Set U), A ∪ B = A := sorry
```
:::

::: {.numex arguments="4"}
```lean
theorem Exercise_3_6_7b (U : Type) :
    ∃! (A : Set U), ∀ (B : Set U), A ∩ B = A := sorry
```
:::

::: {.numex arguments="5"}
```lean
theorem Exercise_3_6_8a (U : Type) : ∀ (A : Set U),
    ∃! (B : Set U), ∀ (C : Set U), C \ A = C ∩ B := sorry
```
:::

::: {.numex arguments="6"}
```lean
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`.

::: {.inout}
::: {.inpt}
```lean
theorem Theorem_3_3_7 :
    ∀ (a b c : Int), a ∣ b → b ∣ c → a ∣ c := by
  
  **done::
```
:::

::: {.outpt}
```state
⊢ ∀ (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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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:

::: {.ind}
```
@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)`.

::: {.inout}
::: {.inpt}
```lean
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::
```
:::

::: {.outpt}
```state
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.

```lean
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).

::: {.nthm arguments="Theorem 3.4.7"}
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$. [&nbsp;□]{.excl}\qedhere
:::

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.

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

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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]`.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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:

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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

::: {.ind}
```
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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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)`:

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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

::: {.ind}
```
@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.

::: {.inout}
::: {.inpt}
```lean
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
```
:::
::: {.outpt}
```state
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`.

::: {.inout}
::: {.inpt}
```lean
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
```
:::

::: {.outpt}
```state
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

:::{.ind}
```
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:

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

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

::: {.ind}
```
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 `rewrite`s in one step.  When a tactic proof is short enough that it can be written on one line, we generally leave off `done`.

```lean
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.

```lean
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:

:::{.ind}
```
@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.

```lean
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

::: {.numex arguments="1"}
```lean
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.)

```lean
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
```

::: {.mdsk}
:::

For the next exercise you will need the following definitions:

```lean
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`.

::: {.numex arguments="3"}
```lean
theorem Exercise_3_4_10 (x y : Int)
    (h1 : odd x) (h2 : odd y) : even (x - y) := sorry
```
:::

::: {.numex arguments="4"}
```lean
theorem Exercise_3_4_27a :
    ∀ (n : Int), 15 ∣ n ↔ 3 ∣ n ∧ 5 ∣ n := sorry
```
:::

::: {.numex arguments="5"}
```lean
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
```
:::