diff --git a/Chap3.qmd b/Chap3.qmd
index 9570b06..b5c64c9 100644
--- a/Chap3.qmd
+++ b/Chap3.qmd
@@ -4021,7 +4021,7 @@ Usually your proof will be more readable if you use the `show` tactic to state e
The `apply?` tactic has not only come up with a suggested tactic, it has applied that tactic, and the proof is now complete. You can confirm that the tactic completes the proof by replacing the line `apply?` in the proof with `apply?`'s suggested `exact` tactic.
-The `apply?` tactic is somewhat unpredictable; sometimes it is able to find the right theorem in the library, and sometimes it isn't. But it is always worth a try. Another way to try to find theorems is to visit the documentation page for Lean's mathematics library, which can be found at [https://leanprover-community.github.io/mathlib4_docs/](https://leanprover-community.github.io/mathlib4_docs/).
+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
diff --git a/docs/Chap3.html b/docs/Chap3.html
index f2797dd..5a74872 100644
--- a/docs/Chap3.html
+++ b/docs/Chap3.html
@@ -3399,7 +3399,7 @@ To us
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. 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/.
+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, Moogle, and Loogle. Another way to try to find theorems is to visit the documentation page for Lean’s mathematics library, which can be found at https://leanprover-community.github.io/mathlib4_docs/.
Exercises
diff --git a/docs/How-To-Prove-It-With-Lean.pdf b/docs/How-To-Prove-It-With-Lean.pdf
index 2d09bc6..a99c362 100644
Binary files a/docs/How-To-Prove-It-With-Lean.pdf and b/docs/How-To-Prove-It-With-Lean.pdf differ
diff --git a/docs/search.json b/docs/search.json
index d791c82..b3b0493 100644
--- a/docs/search.json
+++ b/docs/search.json
@@ -144,7 +144,7 @@
"href": "Chap3.html#existence-and-uniqueness-proofs",
"title": "3 Proofs",
"section": "3.6. Existence and Uniqueness Proofs",
- "text": "3.6. Existence and Uniqueness Proofs\nRecall 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.\nOften 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.\nWith that preparation, here is our strategy for proving statements of the form ∃! (x : U), P x (HTPI pp. 156–157).\n\nTo prove a goal of the form ∃! (x : U), P x:\n\nProve ∃ (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.\n\nTo 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):\n\nThere is a unique set \\(A\\) such that for every set \\(B\\), \\(A \\cup B = B\\).\n\n\nProof. Existence: Clearly \\(\\forall B(\\varnothing \\cup B = B)\\), so \\(\\varnothing\\) has the required property.\nUniqueness: 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\\). □\n\nYou 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.\nThe 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.\nWith 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n **done::\n\n\ncase h\nU : Type\nB : Set U\n⊢ ∀ (x : U),\n>> x ∈ ∅ ∪ B ↔ x ∈ B\n\n\nBased 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n\n **done::\n · -- (←)\n\n **done::\n done\n\n\ncase h.mp\nU : Type\nB : Set U\nx : U\n⊢ x ∈ ∅ ∪ B → x ∈ B\n\n\nOf 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n assume h1 : x ∈ ∅ ∪ B\n define at h1\n **done::\n · -- (←)\n\n **done::\n done\n\n\ncase h.mp\nU : Type\nB : Set U\nx : U\nh1 : x ∈ ∅ ∨ x ∈ B\n⊢ x ∈ B\n\n\nNow 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n assume h1 : x ∈ ∅ ∪ B\n define at h1\n have h2 : x ∉ ∅ := by\n\n **done::\n **done::\n · -- (←)\n\n **done::\n done\n\n\nU : Type\nB : Set U\nx : U\nh1 : x ∈ ∅ ∨ x ∈ B\n⊢ x ∉ ∅\n\n\nThe goal for our “proof within a proof” is a negative statement, so proof by contradiction seems like a good start.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n assume h1 : x ∈ ∅ ∪ B\n define at h1\n have h2 : x ∉ ∅ := by\n by_contra h3\n **done::\n **done::\n · -- (←)\n\n **done::\n done\n\n\nU : Type\nB : Set U\nx : U\nh1 : x ∈ ∅ ∨ x ∈ B\nh3 : x ∈ ∅\n⊢ False\n\n\nTo 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n assume h1 : x ∈ ∅ ∪ B\n define at h1\n have h2 : x ∉ ∅ := by\n by_contra h3\n define at h3 --h3 : False\n show False from h3\n done\n **done::\n · -- (←)\n\n **done::\n done\n\n\ncase h.mp\nU : Type\nB : Set U\nx : U\nh1 : x ∈ ∅ ∨ x ∈ B\nh2 : x ∉ ∅\n⊢ x ∈ B\n\n\nNow 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n assume h1 : x ∈ ∅ ∪ B\n define at h1\n have h2 : x ∉ ∅ := by\n by_contra h3\n define at h3 --h3 : False\n show False from h3\n done\n disj_syll h1 h2 --h1 : x ∈ B\n show x ∈ B from h1\n done\n · -- (←)\n\n **done::\n done\n\n\ncase h.mpr\nU : Type\nB : Set U\nx : U\n⊢ x ∈ B → x ∈ ∅ ∪ B\n\n\nThis 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n assume h1 : x ∈ ∅ ∪ B\n define at h1\n have h2 : x ∉ ∅ := by\n by_contra h3\n define at h3 --h3 : False\n show False from h3\n done\n disj_syll h1 h2 --h1 : x ∈ B\n show x ∈ B from h1\n done\n · -- (←)\n assume h1 : x ∈ B\n show x ∈ ∅ ∪ B from Or.inr h1\n done\n done\n\n\nNo goals\n\n\nThe 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.\n\n\ntheorem union_comm {U : Type} (X Y : Set U) :\n X ∪ Y = Y ∪ X := by\n \n **done::\n\n\nU : Type\nX Y : Set U\n⊢ X ∪ Y = Y ∪ X\n\n\nOnce 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.\n\n\ntheorem union_comm {U : Type} (X Y : Set U) :\n X ∪ Y = Y ∪ X := by\n apply Set.ext\n fix x : U\n **done::\n\n\ncase h\nU : Type\nX Y : Set U\nx : U\n⊢ x ∈ X ∪ Y ↔ x ∈ Y ∪ X\n\n\nTo 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.)\n\n\ntheorem union_comm {U : Type} (X Y : Set U) :\n X ∪ Y = Y ∪ X := by\n apply Set.ext\n fix x : U\n define : x ∈ X ∪ Y\n define : x ∈ Y ∪ X\n **done::\n\n\ncase h\nU : Type\nX Y : Set U\nx : U\n⊢ x ∈ X ∨ x ∈ Y ↔\n>> x ∈ Y ∨ x ∈ X\n\n\nBy 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.\nReturning 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”?\nTry 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.\n\n\ntheorem union_comm {U : Type} (X Y : Set U) :\n X ∪ Y = Y ∪ X := by\n apply Set.ext\n fix x : U\n define : x ∈ X ∪ Y\n define : x ∈ Y ∪ X\n show x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X from or_comm\n done\n\n\nNo goals\n\n\nWe 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:\n\n@empty_union : ∀ {U : Type} (B : Set U), ∅ ∪ B = B\n\n@union_comm : ∀ {U : Type} (X Y : Set U), X ∪ Y = Y ∪ X\n\nNotice 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.)\nWe are finally ready to prove the theorem from Example 3.6.2. Here is the theorem:\n\n\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n\n **done::\n\n\nU : Type\n⊢ ∃! (A : Set U),\n>> ∀ (B : Set U),\n>> A ∪ B = B\n\n\nThe goal starts with ∃!, so we use our new tactic, exists_unique.\n\n\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n exists_unique\n **done::\n\n\ncase Existence\nU : Type\n⊢ ∃ (A : Set U),\n>> ∀ (B : Set U),\n>> A ∪ B = B\ncase Uniqueness\nU : Type\n⊢ ∀ (A_1 A_2 : Set U),\n>> (∀ (B : Set U),\n>> A_1 ∪ B = B) →\n>> (∀ (B : Set U),\n>> A_2 ∪ B = B) →\n>> A_1 = A_2\n\n\nWe have two goals, labeled Existence and Uniqueness. Imitating the proof from HTPI, we prove existence by using the value ∅ for A.\n\n\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n exists_unique\n · -- Existence\n apply Exists.intro ∅\n **done::\n · -- Uniqueness\n\n **done::\n done\n\n\ncase Existence\nU : Type\n⊢ ∀ (B : Set U),\n>> ∅ ∪ B = B\n\n\nThe goal is now precisely the statement of the theorem empty_union, so we can prove it by simply citing that theorem.\n\n\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n exists_unique\n · -- Existence\n apply Exists.intro ∅\n show ∀ (B : Set U), ∅ ∪ B = B from empty_union\n done\n · -- Uniqueness\n\n **done::\n done\n\n\ncase Uniqueness\nU : Type\n⊢ ∀ (A_1 A_2 : Set U),\n>> (∀ (B : Set U),\n>> A_1 ∪ B = B) →\n>> (∀ (B : Set U),\n>> A_2 ∪ B = B) →\n>> A_1 = A_2\n\n\nFor 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.\n\n\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n exists_unique\n · -- Existence\n apply Exists.intro ∅\n show ∀ (B : Set U), ∅ ∪ B = B from empty_union\n done\n · -- Uniqueness\n fix C : Set U; fix D : Set U\n assume h1 : ∀ (B : Set U), C ∪ B = B\n assume h2 : ∀ (B : Set U), D ∪ B = B\n **done::\n done\n\n\ncase Uniqueness\nU : Type\nC D : Set U\nh1 : ∀ (B : Set U),\n>> C ∪ B = B\nh2 : ∀ (B : Set U),\n>> D ∪ B = B\n⊢ C = D\n\n\nThe next step in HTPI was to apply h1 to D, and h2 to C. We do the same thing in Lean.\n\n\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n exists_unique\n · -- Existence\n apply Exists.intro ∅\n show ∀ (B : Set U), ∅ ∪ B = B from empty_union\n done\n · -- Uniqueness\n fix C : Set U; fix D : Set U\n assume h1 : ∀ (B : Set U), C ∪ B = B\n assume h2 : ∀ (B : Set U), D ∪ B = B\n have h3 : C ∪ D = D := h1 D\n have h4 : D ∪ C = C := h2 C \n **done::\n done\n\n\ncase Uniqueness\nU : Type\nC D : Set U\nh1 : ∀ (B : Set U),\n>> C ∪ B = B\nh2 : ∀ (B : Set U),\n>> D ∪ B = B\nh3 : C ∪ D = D\nh4 : D ∪ C = C\n⊢ C = D\n\n\nThe 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:\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n exists_unique\n · -- Existence\n apply Exists.intro ∅\n show ∀ (B : Set U), ∅ ∪ B = B from empty_union\n done\n · -- Uniqueness\n fix C : Set U; fix D : Set U\n assume h1 : ∀ (B : Set U), C ∪ B = B\n assume h2 : ∀ (B : Set U), D ∪ B = B\n have h3 : C ∪ D = D := h1 D\n have h4 : D ∪ C = C := h2 C \n show C = D from\n calc C\n _ = D ∪ C := h4.symm\n _ = C ∪ D := union_comm D C\n _ = D := h3\n done\n done\nSince 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):\n\n\nTo use a given of the form ∃! (x : U), P x:\n\nIntroduce 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.\n\nIf you have a given h : ∃! (x : U), P x, then the tactic obtain (a : U) (h1 : P a) (h2 : ∀ (x_1 x_2 : U), P x_1 → P x_2 → x_1 = x_2) from h will introduce into the tactic state a new variable a of type U and new givens (h1 : P a) and (h2 : ∀ (x_1 x_2 : U), P x_1 → P x_2 → x_1 = x_2). To illustrate the use of this tactic, let’s prove the theorem in Example 3.6.4 of HTPI.\n\n\ntheorem Example_3_6_4 (U : Type) (A B C : Set U)\n (h1 : ∃ (x : U), x ∈ A ∩ B)\n (h2 : ∃ (x : U), x ∈ A ∩ C)\n (h3 : ∃! (x : U), x ∈ A) :\n ∃ (x : U), x ∈ B ∩ C := by\n\n **done::\n\n\nU : Type\nA B C : Set U\nh1 : ∃ (x : U),\n>> x ∈ A ∩ B\nh2 : ∃ (x : U),\n>> x ∈ A ∩ C\nh3 : ∃! (x : U), x ∈ A\n⊢ ∃ (x : U), x ∈ B ∩ C\n\n\nWe 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.\n\n\ntheorem Example_3_6_4 (U : Type) (A B C : Set U)\n (h1 : ∃ (x : U), x ∈ A ∩ B)\n (h2 : ∃ (x : U), x ∈ A ∩ C)\n (h3 : ∃! (x : U), x ∈ A) :\n ∃ (x : U), x ∈ B ∩ C := by\n obtain (b : U) (h4 : b ∈ A ∩ B) from h1\n obtain (c : U) (h5 : c ∈ A ∩ C) from h2\n obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),\n y ∈ A → z ∈ A → y = z) from h3\n define at h4; define at h5\n **done::\n\n\nU : Type\nA B C : Set U\nh1 : ∃ (x : U),\n>> x ∈ A ∩ B\nh2 : ∃ (x : U),\n>> x ∈ A ∩ C\nh3 : ∃! (x : U), x ∈ A\nb : U\nh4 : b ∈ A ∧ b ∈ B\nc : U\nh5 : c ∈ A ∧ c ∈ C\na : U\nh6 : a ∈ A\nh7 : ∀ (y z : U),\n>> y ∈ A → z ∈ A → y = z\n⊢ ∃ (x : U), x ∈ B ∩ C\n\n\nThe 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.\n\n\ntheorem Example_3_6_4 (U : Type) (A B C : Set U)\n (h1 : ∃ (x : U), x ∈ A ∩ B)\n (h2 : ∃ (x : U), x ∈ A ∩ C)\n (h3 : ∃! (x : U), x ∈ A) :\n ∃ (x : U), x ∈ B ∩ C := by\n obtain (b : U) (h4 : b ∈ A ∩ B) from h1\n obtain (c : U) (h5 : c ∈ A ∩ C) from h2\n obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),\n y ∈ A → z ∈ A → y = z) from h3\n define at h4; define at h5\n have h8 : b = c := h7 b c h4.left h5.left\n **done::\n\n\nU : Type\nA B C : Set U\nh1 : ∃ (x : U),\n>> x ∈ A ∩ B\nh2 : ∃ (x : U),\n>> x ∈ A ∩ C\nh3 : ∃! (x : U), x ∈ A\nb : U\nh4 : b ∈ A ∧ b ∈ B\nc : U\nh5 : c ∈ A ∧ c ∈ C\na : U\nh6 : a ∈ A\nh7 : ∀ (y z : U),\n>> y ∈ A → z ∈ A → y = z\nh8 : b = c\n⊢ ∃ (x : U), x ∈ B ∩ C\n\n\nFor 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).\nAs 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.\n\n\ntheorem Example_3_6_4 (U : Type) (A B C : Set U)\n (h1 : ∃ (x : U), x ∈ A ∩ B)\n (h2 : ∃ (x : U), x ∈ A ∩ C)\n (h3 : ∃! (x : U), x ∈ A) :\n ∃ (x : U), x ∈ B ∩ C := by\n obtain (b : U) (h4 : b ∈ A ∩ B) from h1\n obtain (c : U) (h5 : c ∈ A ∩ C) from h2\n obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),\n y ∈ A → z ∈ A → y = z) from h3\n define at h4; define at h5\n have h8 : b = c := h7 b c h4.left h5.left\n rewrite [h8] at h4\n **done::\n\n\nU : Type\nA B C : Set U\nh1 : ∃ (x : U),\n>> x ∈ A ∩ B\nh2 : ∃ (x : U),\n>> x ∈ A ∩ C\nh3 : ∃! (x : U), x ∈ A\nb c : U\nh4 : c ∈ A ∧ c ∈ B\nh5 : c ∈ A ∧ c ∈ C\na : U\nh6 : a ∈ A\nh7 : ∀ (y z : U),\n>> y ∈ A → z ∈ A → y = z\nh8 : b = c\n⊢ ∃ (x : U), x ∈ B ∩ C\n\n\nNow 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:\ntheorem Example_3_6_4 (U : Type) (A B C : Set U)\n (h1 : ∃ (x : U), x ∈ A ∩ B)\n (h2 : ∃ (x : U), x ∈ A ∩ C)\n (h3 : ∃! (x : U), x ∈ A) :\n ∃ (x : U), x ∈ B ∩ C := by\n obtain (b : U) (h4 : b ∈ A ∩ B) from h1\n obtain (c : U) (h5 : c ∈ A ∩ C) from h2\n obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),\n y ∈ A → z ∈ A → y = z) from h3\n define at h4; define at h5\n have h8 : b = c := h7 b c h4.left h5.left\n rewrite [h8] at h4\n show ∃ (x : U), x ∈ B ∩ C from\n Exists.intro c (And.intro h4.right h5.right)\n done\nYou might want to compare the Lean proof above to the proof of this theorem as it appears in HTPI (HTPI p. 160):\n\nSuppose \\(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\n\n\nProof. 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. □\n\nBefore 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:\n\n\ntheorem union_comm {U : Type} (X Y : Set U) :\n X ∪ Y = Y ∪ X := by\n apply Set.ext\n fix x : U\n define : x ∈ X ∪ Y\n define : x ∈ Y ∪ X\n **done::\n\n\ncase h\nU : Type\nX Y : Set U\nx : U\n⊢ x ∈ X ∨ x ∈ Y ↔\n>> x ∈ Y ∨ x ∈ X\n\n\nNow let’s give the apply? tactic a try.\ntheorem union_comm {U : Type} (X Y : Set U) :\n X ∪ Y = Y ∪ X := by\n apply Set.ext\n fix x : U\n define : x ∈ X ∪ Y\n define : x ∈ Y ∪ X\n ++apply?::\n done\nIt 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\n\nshow x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X from Or.comm\n\nThe 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.\nUsually 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.”\nThe 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.\nThe apply? tactic is somewhat unpredictable; sometimes it is able to find the right theorem in the library, and sometimes it isn’t. But it is always worth a try. Another way to try to find theorems is to visit the documentation page for Lean’s mathematics library, which can be found at https://leanprover-community.github.io/mathlib4_docs/.\n\n\nExercises\n\ntheorem Exercise_3_4_15 (U : Type) (B : Set U) (F : Set (Set U)) :\n ⋃₀ {X : Set U | ∃ (A : Set U), A ∈ F ∧ X = A \\ B}\n ⊆ ⋃₀ (F \\ 𝒫 B) := sorry\n\n\ntheorem Exercise_3_5_9 (U : Type) (A B : Set U)\n (h1 : 𝒫 (A ∪ B) = 𝒫 A ∪ 𝒫 B) : A ⊆ B ∨ B ⊆ A := by\n --Hint: Start like this:\n have h2 : A ∪ B ∈ 𝒫 (A ∪ B) := sorry\n \n **done::\n\n\ntheorem Exercise_3_6_6b (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U), A ∪ B = A := sorry\n\n\ntheorem Exercise_3_6_7b (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U), A ∩ B = A := sorry\n\n\ntheorem Exercise_3_6_8a (U : Type) : ∀ (A : Set U),\n ∃! (B : Set U), ∀ (C : Set U), C \\ A = C ∩ B := sorry\n\n\ntheorem Exercise_3_6_10 (U : Type) (A : Set U)\n (h1 : ∀ (F : Set (Set U)), ⋃₀ F = A → A ∈ F) :\n ∃! (x : U), x ∈ A := by\n --Hint: Start like this:\n set F0 : Set (Set U) := {X : Set U | X ⊆ A ∧ ∃! (x : U), x ∈ X}\n --Now F0 is in the tactic state, with the definition above\n have h2 : ⋃₀ F0 = A := sorry\n \n **done::"
+ "text": "3.6. Existence and Uniqueness Proofs\nRecall 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.\nOften 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.\nWith that preparation, here is our strategy for proving statements of the form ∃! (x : U), P x (HTPI pp. 156–157).\n\nTo prove a goal of the form ∃! (x : U), P x:\n\nProve ∃ (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.\n\nTo 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):\n\nThere is a unique set \\(A\\) such that for every set \\(B\\), \\(A \\cup B = B\\).\n\n\nProof. Existence: Clearly \\(\\forall B(\\varnothing \\cup B = B)\\), so \\(\\varnothing\\) has the required property.\nUniqueness: 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\\). □\n\nYou 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.\nThe 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.\nWith 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n **done::\n\n\ncase h\nU : Type\nB : Set U\n⊢ ∀ (x : U),\n>> x ∈ ∅ ∪ B ↔ x ∈ B\n\n\nBased 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n\n **done::\n · -- (←)\n\n **done::\n done\n\n\ncase h.mp\nU : Type\nB : Set U\nx : U\n⊢ x ∈ ∅ ∪ B → x ∈ B\n\n\nOf 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n assume h1 : x ∈ ∅ ∪ B\n define at h1\n **done::\n · -- (←)\n\n **done::\n done\n\n\ncase h.mp\nU : Type\nB : Set U\nx : U\nh1 : x ∈ ∅ ∨ x ∈ B\n⊢ x ∈ B\n\n\nNow 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n assume h1 : x ∈ ∅ ∪ B\n define at h1\n have h2 : x ∉ ∅ := by\n\n **done::\n **done::\n · -- (←)\n\n **done::\n done\n\n\nU : Type\nB : Set U\nx : U\nh1 : x ∈ ∅ ∨ x ∈ B\n⊢ x ∉ ∅\n\n\nThe goal for our “proof within a proof” is a negative statement, so proof by contradiction seems like a good start.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n assume h1 : x ∈ ∅ ∪ B\n define at h1\n have h2 : x ∉ ∅ := by\n by_contra h3\n **done::\n **done::\n · -- (←)\n\n **done::\n done\n\n\nU : Type\nB : Set U\nx : U\nh1 : x ∈ ∅ ∨ x ∈ B\nh3 : x ∈ ∅\n⊢ False\n\n\nTo 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n assume h1 : x ∈ ∅ ∪ B\n define at h1\n have h2 : x ∉ ∅ := by\n by_contra h3\n define at h3 --h3 : False\n show False from h3\n done\n **done::\n · -- (←)\n\n **done::\n done\n\n\ncase h.mp\nU : Type\nB : Set U\nx : U\nh1 : x ∈ ∅ ∨ x ∈ B\nh2 : x ∉ ∅\n⊢ x ∈ B\n\n\nNow 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n assume h1 : x ∈ ∅ ∪ B\n define at h1\n have h2 : x ∉ ∅ := by\n by_contra h3\n define at h3 --h3 : False\n show False from h3\n done\n disj_syll h1 h2 --h1 : x ∈ B\n show x ∈ B from h1\n done\n · -- (←)\n\n **done::\n done\n\n\ncase h.mpr\nU : Type\nB : Set U\nx : U\n⊢ x ∈ B → x ∈ ∅ ∪ B\n\n\nThis 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.\n\n\ntheorem empty_union {U : Type} (B : Set U) :\n ∅ ∪ B = B := by\n apply Set.ext\n fix x : U\n apply Iff.intro\n · -- (→)\n assume h1 : x ∈ ∅ ∪ B\n define at h1\n have h2 : x ∉ ∅ := by\n by_contra h3\n define at h3 --h3 : False\n show False from h3\n done\n disj_syll h1 h2 --h1 : x ∈ B\n show x ∈ B from h1\n done\n · -- (←)\n assume h1 : x ∈ B\n show x ∈ ∅ ∪ B from Or.inr h1\n done\n done\n\n\nNo goals\n\n\nThe 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.\n\n\ntheorem union_comm {U : Type} (X Y : Set U) :\n X ∪ Y = Y ∪ X := by\n \n **done::\n\n\nU : Type\nX Y : Set U\n⊢ X ∪ Y = Y ∪ X\n\n\nOnce 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.\n\n\ntheorem union_comm {U : Type} (X Y : Set U) :\n X ∪ Y = Y ∪ X := by\n apply Set.ext\n fix x : U\n **done::\n\n\ncase h\nU : Type\nX Y : Set U\nx : U\n⊢ x ∈ X ∪ Y ↔ x ∈ Y ∪ X\n\n\nTo 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.)\n\n\ntheorem union_comm {U : Type} (X Y : Set U) :\n X ∪ Y = Y ∪ X := by\n apply Set.ext\n fix x : U\n define : x ∈ X ∪ Y\n define : x ∈ Y ∪ X\n **done::\n\n\ncase h\nU : Type\nX Y : Set U\nx : U\n⊢ x ∈ X ∨ x ∈ Y ↔\n>> x ∈ Y ∨ x ∈ X\n\n\nBy 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.\nReturning 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”?\nTry 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.\n\n\ntheorem union_comm {U : Type} (X Y : Set U) :\n X ∪ Y = Y ∪ X := by\n apply Set.ext\n fix x : U\n define : x ∈ X ∪ Y\n define : x ∈ Y ∪ X\n show x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X from or_comm\n done\n\n\nNo goals\n\n\nWe 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:\n\n@empty_union : ∀ {U : Type} (B : Set U), ∅ ∪ B = B\n\n@union_comm : ∀ {U : Type} (X Y : Set U), X ∪ Y = Y ∪ X\n\nNotice 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.)\nWe are finally ready to prove the theorem from Example 3.6.2. Here is the theorem:\n\n\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n\n **done::\n\n\nU : Type\n⊢ ∃! (A : Set U),\n>> ∀ (B : Set U),\n>> A ∪ B = B\n\n\nThe goal starts with ∃!, so we use our new tactic, exists_unique.\n\n\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n exists_unique\n **done::\n\n\ncase Existence\nU : Type\n⊢ ∃ (A : Set U),\n>> ∀ (B : Set U),\n>> A ∪ B = B\ncase Uniqueness\nU : Type\n⊢ ∀ (A_1 A_2 : Set U),\n>> (∀ (B : Set U),\n>> A_1 ∪ B = B) →\n>> (∀ (B : Set U),\n>> A_2 ∪ B = B) →\n>> A_1 = A_2\n\n\nWe have two goals, labeled Existence and Uniqueness. Imitating the proof from HTPI, we prove existence by using the value ∅ for A.\n\n\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n exists_unique\n · -- Existence\n apply Exists.intro ∅\n **done::\n · -- Uniqueness\n\n **done::\n done\n\n\ncase Existence\nU : Type\n⊢ ∀ (B : Set U),\n>> ∅ ∪ B = B\n\n\nThe goal is now precisely the statement of the theorem empty_union, so we can prove it by simply citing that theorem.\n\n\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n exists_unique\n · -- Existence\n apply Exists.intro ∅\n show ∀ (B : Set U), ∅ ∪ B = B from empty_union\n done\n · -- Uniqueness\n\n **done::\n done\n\n\ncase Uniqueness\nU : Type\n⊢ ∀ (A_1 A_2 : Set U),\n>> (∀ (B : Set U),\n>> A_1 ∪ B = B) →\n>> (∀ (B : Set U),\n>> A_2 ∪ B = B) →\n>> A_1 = A_2\n\n\nFor 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.\n\n\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n exists_unique\n · -- Existence\n apply Exists.intro ∅\n show ∀ (B : Set U), ∅ ∪ B = B from empty_union\n done\n · -- Uniqueness\n fix C : Set U; fix D : Set U\n assume h1 : ∀ (B : Set U), C ∪ B = B\n assume h2 : ∀ (B : Set U), D ∪ B = B\n **done::\n done\n\n\ncase Uniqueness\nU : Type\nC D : Set U\nh1 : ∀ (B : Set U),\n>> C ∪ B = B\nh2 : ∀ (B : Set U),\n>> D ∪ B = B\n⊢ C = D\n\n\nThe next step in HTPI was to apply h1 to D, and h2 to C. We do the same thing in Lean.\n\n\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n exists_unique\n · -- Existence\n apply Exists.intro ∅\n show ∀ (B : Set U), ∅ ∪ B = B from empty_union\n done\n · -- Uniqueness\n fix C : Set U; fix D : Set U\n assume h1 : ∀ (B : Set U), C ∪ B = B\n assume h2 : ∀ (B : Set U), D ∪ B = B\n have h3 : C ∪ D = D := h1 D\n have h4 : D ∪ C = C := h2 C \n **done::\n done\n\n\ncase Uniqueness\nU : Type\nC D : Set U\nh1 : ∀ (B : Set U),\n>> C ∪ B = B\nh2 : ∀ (B : Set U),\n>> D ∪ B = B\nh3 : C ∪ D = D\nh4 : D ∪ C = C\n⊢ C = D\n\n\nThe 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:\ntheorem Example_3_6_2 (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U),\n A ∪ B = B := by\n exists_unique\n · -- Existence\n apply Exists.intro ∅\n show ∀ (B : Set U), ∅ ∪ B = B from empty_union\n done\n · -- Uniqueness\n fix C : Set U; fix D : Set U\n assume h1 : ∀ (B : Set U), C ∪ B = B\n assume h2 : ∀ (B : Set U), D ∪ B = B\n have h3 : C ∪ D = D := h1 D\n have h4 : D ∪ C = C := h2 C \n show C = D from\n calc C\n _ = D ∪ C := h4.symm\n _ = C ∪ D := union_comm D C\n _ = D := h3\n done\n done\nSince 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):\n\n\nTo use a given of the form ∃! (x : U), P x:\n\nIntroduce 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.\n\nIf you have a given h : ∃! (x : U), P x, then the tactic obtain (a : U) (h1 : P a) (h2 : ∀ (x_1 x_2 : U), P x_1 → P x_2 → x_1 = x_2) from h will introduce into the tactic state a new variable a of type U and new givens (h1 : P a) and (h2 : ∀ (x_1 x_2 : U), P x_1 → P x_2 → x_1 = x_2). To illustrate the use of this tactic, let’s prove the theorem in Example 3.6.4 of HTPI.\n\n\ntheorem Example_3_6_4 (U : Type) (A B C : Set U)\n (h1 : ∃ (x : U), x ∈ A ∩ B)\n (h2 : ∃ (x : U), x ∈ A ∩ C)\n (h3 : ∃! (x : U), x ∈ A) :\n ∃ (x : U), x ∈ B ∩ C := by\n\n **done::\n\n\nU : Type\nA B C : Set U\nh1 : ∃ (x : U),\n>> x ∈ A ∩ B\nh2 : ∃ (x : U),\n>> x ∈ A ∩ C\nh3 : ∃! (x : U), x ∈ A\n⊢ ∃ (x : U), x ∈ B ∩ C\n\n\nWe 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.\n\n\ntheorem Example_3_6_4 (U : Type) (A B C : Set U)\n (h1 : ∃ (x : U), x ∈ A ∩ B)\n (h2 : ∃ (x : U), x ∈ A ∩ C)\n (h3 : ∃! (x : U), x ∈ A) :\n ∃ (x : U), x ∈ B ∩ C := by\n obtain (b : U) (h4 : b ∈ A ∩ B) from h1\n obtain (c : U) (h5 : c ∈ A ∩ C) from h2\n obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),\n y ∈ A → z ∈ A → y = z) from h3\n define at h4; define at h5\n **done::\n\n\nU : Type\nA B C : Set U\nh1 : ∃ (x : U),\n>> x ∈ A ∩ B\nh2 : ∃ (x : U),\n>> x ∈ A ∩ C\nh3 : ∃! (x : U), x ∈ A\nb : U\nh4 : b ∈ A ∧ b ∈ B\nc : U\nh5 : c ∈ A ∧ c ∈ C\na : U\nh6 : a ∈ A\nh7 : ∀ (y z : U),\n>> y ∈ A → z ∈ A → y = z\n⊢ ∃ (x : U), x ∈ B ∩ C\n\n\nThe 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.\n\n\ntheorem Example_3_6_4 (U : Type) (A B C : Set U)\n (h1 : ∃ (x : U), x ∈ A ∩ B)\n (h2 : ∃ (x : U), x ∈ A ∩ C)\n (h3 : ∃! (x : U), x ∈ A) :\n ∃ (x : U), x ∈ B ∩ C := by\n obtain (b : U) (h4 : b ∈ A ∩ B) from h1\n obtain (c : U) (h5 : c ∈ A ∩ C) from h2\n obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),\n y ∈ A → z ∈ A → y = z) from h3\n define at h4; define at h5\n have h8 : b = c := h7 b c h4.left h5.left\n **done::\n\n\nU : Type\nA B C : Set U\nh1 : ∃ (x : U),\n>> x ∈ A ∩ B\nh2 : ∃ (x : U),\n>> x ∈ A ∩ C\nh3 : ∃! (x : U), x ∈ A\nb : U\nh4 : b ∈ A ∧ b ∈ B\nc : U\nh5 : c ∈ A ∧ c ∈ C\na : U\nh6 : a ∈ A\nh7 : ∀ (y z : U),\n>> y ∈ A → z ∈ A → y = z\nh8 : b = c\n⊢ ∃ (x : U), x ∈ B ∩ C\n\n\nFor 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).\nAs 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.\n\n\ntheorem Example_3_6_4 (U : Type) (A B C : Set U)\n (h1 : ∃ (x : U), x ∈ A ∩ B)\n (h2 : ∃ (x : U), x ∈ A ∩ C)\n (h3 : ∃! (x : U), x ∈ A) :\n ∃ (x : U), x ∈ B ∩ C := by\n obtain (b : U) (h4 : b ∈ A ∩ B) from h1\n obtain (c : U) (h5 : c ∈ A ∩ C) from h2\n obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),\n y ∈ A → z ∈ A → y = z) from h3\n define at h4; define at h5\n have h8 : b = c := h7 b c h4.left h5.left\n rewrite [h8] at h4\n **done::\n\n\nU : Type\nA B C : Set U\nh1 : ∃ (x : U),\n>> x ∈ A ∩ B\nh2 : ∃ (x : U),\n>> x ∈ A ∩ C\nh3 : ∃! (x : U), x ∈ A\nb c : U\nh4 : c ∈ A ∧ c ∈ B\nh5 : c ∈ A ∧ c ∈ C\na : U\nh6 : a ∈ A\nh7 : ∀ (y z : U),\n>> y ∈ A → z ∈ A → y = z\nh8 : b = c\n⊢ ∃ (x : U), x ∈ B ∩ C\n\n\nNow 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:\ntheorem Example_3_6_4 (U : Type) (A B C : Set U)\n (h1 : ∃ (x : U), x ∈ A ∩ B)\n (h2 : ∃ (x : U), x ∈ A ∩ C)\n (h3 : ∃! (x : U), x ∈ A) :\n ∃ (x : U), x ∈ B ∩ C := by\n obtain (b : U) (h4 : b ∈ A ∩ B) from h1\n obtain (c : U) (h5 : c ∈ A ∩ C) from h2\n obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),\n y ∈ A → z ∈ A → y = z) from h3\n define at h4; define at h5\n have h8 : b = c := h7 b c h4.left h5.left\n rewrite [h8] at h4\n show ∃ (x : U), x ∈ B ∩ C from\n Exists.intro c (And.intro h4.right h5.right)\n done\nYou might want to compare the Lean proof above to the proof of this theorem as it appears in HTPI (HTPI p. 160):\n\nSuppose \\(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\n\n\nProof. 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. □\n\nBefore 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:\n\n\ntheorem union_comm {U : Type} (X Y : Set U) :\n X ∪ Y = Y ∪ X := by\n apply Set.ext\n fix x : U\n define : x ∈ X ∪ Y\n define : x ∈ Y ∪ X\n **done::\n\n\ncase h\nU : Type\nX Y : Set U\nx : U\n⊢ x ∈ X ∨ x ∈ Y ↔\n>> x ∈ Y ∨ x ∈ X\n\n\nNow let’s give the apply? tactic a try.\ntheorem union_comm {U : Type} (X Y : Set U) :\n X ∪ Y = Y ∪ X := by\n apply Set.ext\n fix x : U\n define : x ∈ X ∪ Y\n define : x ∈ Y ∪ X\n ++apply?::\n done\nIt 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\n\nshow x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X from Or.comm\n\nThe 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.\nUsually 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.”\nThe 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.\nThe 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, Moogle, and Loogle. 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/.\n\n\nExercises\n\ntheorem Exercise_3_4_15 (U : Type) (B : Set U) (F : Set (Set U)) :\n ⋃₀ {X : Set U | ∃ (A : Set U), A ∈ F ∧ X = A \\ B}\n ⊆ ⋃₀ (F \\ 𝒫 B) := sorry\n\n\ntheorem Exercise_3_5_9 (U : Type) (A B : Set U)\n (h1 : 𝒫 (A ∪ B) = 𝒫 A ∪ 𝒫 B) : A ⊆ B ∨ B ⊆ A := by\n --Hint: Start like this:\n have h2 : A ∪ B ∈ 𝒫 (A ∪ B) := sorry\n \n **done::\n\n\ntheorem Exercise_3_6_6b (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U), A ∪ B = A := sorry\n\n\ntheorem Exercise_3_6_7b (U : Type) :\n ∃! (A : Set U), ∀ (B : Set U), A ∩ B = A := sorry\n\n\ntheorem Exercise_3_6_8a (U : Type) : ∀ (A : Set U),\n ∃! (B : Set U), ∀ (C : Set U), C \\ A = C ∩ B := sorry\n\n\ntheorem Exercise_3_6_10 (U : Type) (A : Set U)\n (h1 : ∀ (F : Set (Set U)), ⋃₀ F = A → A ∈ F) :\n ∃! (x : U), x ∈ A := by\n --Hint: Start like this:\n set F0 : Set (Set U) := {X : Set U | X ⊆ A ∧ ∃! (x : U), x ∈ X}\n --Now F0 is in the tactic state, with the definition above\n have h2 : ⋃₀ F0 = A := sorry\n \n **done::"
},
{
"objectID": "Chap3.html#more-examples-of-proofs",