diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex
index cbe9530..dc9a457 100644
--- a/Bookshelf/Enderton/Set.tex
+++ b/Bookshelf/Enderton/Set.tex
@@ -1,5 +1,8 @@
 \documentclass{report}
 
+\usepackage{graphicx}
+\graphicspath{{./Set/images/}}
+
 \input{../../preamble}
 \makeleancommands{../..}
 
@@ -1720,7 +1723,7 @@ Show that $A + (B + C) = (A + B) + C$.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 4.16}}%
+\subsection{\verified{Exercise 4.16}}%
 \label{sub:exercise-4.16}
 
 Simplify:
@@ -1728,11 +1731,26 @@ Simplify:
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.exercise\_4\_16}
+
+  Let $A$, $B$, and $C$ be arbitrary sets.
+  Then
+    \begin{align*}
+      [(A \cup B \cup C) \cap (A \cup B)] & - [(A \cup (B - C)) \cap A] \\
+        & = [A \cup B] - [A] \\
+        & = \{ x \mid x \in (A \cup B) \land x \not\in A \} \\
+        & = \{ x \mid x \in \{ y \mid y \in A \lor y \in B \} \land x \not\in A \} \\
+        & = \{ x \mid (x \in A \lor x \in B) \land x \not\in A \} \\\
+        & = \{ x \mid (x \in A \land x \not\in A) \lor (x \in B \land x \not\in A) \} \\
+        & = \{ x \mid F \lor (X \in B \land x \not\in A) \} \\
+        & = \{ x \mid x \in B \land x \not\in A \} \\
+        & = B - A.
+    \end{align*}
 
 \end{proof}
 
-\subsection{\unverified{Exercise 4.17}}%
+\subsection{\verified{Exercise 4.17}}%
 \label{sub:exercise-4.17}
 
 Show that the following four conditions are equivalent.
@@ -1746,11 +1764,58 @@ Show that the following four conditions are equivalent.
 
 \begin{proof}
 
-  TODO
+  \statementpadding
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.exercise\_4\_17\_i}
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.exercise\_4\_17\_ii}
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.exercise\_4\_17\_iii}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.exercise\_4\_17\_iv}
+
+  Let $A$ and $B$ be arbitrary sets.
+  We show that (i) $(a) \Rightarrow (b)$, (ii) $(b) \Rightarrow (c)$, (iii)
+    $(c) \Rightarrow (d)$, and (iv) $(d) \Rightarrow (a)$.
+
+  \paragraph{(i)}%
+
+    Suppose $A \subseteq B$.
+    That is, $\forall t, t \in A \Rightarrow t \in B$.
+    Then there is no element such that $t \in A$ and $t \not\in B$.
+    By definition of the relative complement, this immediately implies
+      $A - B = \emptyset$.
+
+  \paragraph{(ii)}%
+
+    Suppose $A - B = \emptyset$.
+    By definition of the relative complement,
+      $$A - B = \emptyset = \{ x \mid x \in A \land x \not\in B \}.$$
+    Then, for all $t$,
+      $\neg(t \in A \land t \not\in B) = t \not\in A \lor t \in B$.
+    This implies, by definition of the subset, that $A \subseteq B$.
+    It then immediately follows that $A \cup B = B$.
+
+  \paragraph{(iii)}%
+
+    Suppose $A \cup B = B$.
+    Then there is no member of $A$ that is not a member of $B$.
+    In other words, $A \subseteq B$.
+    This immediately implies $A \cap B = A$.
+
+  \paragraph{(iv)}%
+
+    Suppose $A \cap B = A$.
+    Then every member of $A$ is a member of $B$.
+    This immediately implies $A \subseteq B$.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 4.18}}%
+\subsection{\partial{Exercise 4.18}}%
 \label{sub:exercise-4.18}
 
 Assume that $A$ and $B$ are subsets of $S$.
@@ -1759,11 +1824,30 @@ List all of the different sets that can be made from these three by use of the
 
 \begin{proof}
 
-  TODO
+  We can reason about this diagrammatically:
+
+  \begin{figure}[ht]
+    \includegraphics[width=0.6\textwidth]{venn-diagram}
+    \centering
+  \end{figure}
+
+  In the above diagram, we assume the left circle corresponds to set $A$ and the
+    right circle corresponds to $B$.
+  The the possible sets we can make via the specified operators are:
+
+  \begin{itemize}
+    \item $A - B$, the left circle excluding the overlapping region.
+    \item $A \cap B$, the overlapping region.
+    \item $B - A$, the right circle excluding the overlapping region.
+    \item $(A \cup B) \cap A$, the left circle.
+    \item $(A \cup B) \cap B$, the right circle.
+    \item $(A - B) \cup (B - A)$, the symmetric difference.
+    \item $A \cup B$, the entire diagram.
+  \end{itemize}
 
 \end{proof}
 
-\subsection{\unverified{Exercise 4.19}}%
+\subsection{\verified{Exercise 4.19}}%
 \label{sub:exercise-4.19}
 
 Is $\powerset{(A - B)}$ always equal to $\powerset{A} - \powerset{B}$?
@@ -1771,11 +1855,35 @@ Is it ever equal to $\powerset{A} - \powerset{B}$?
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.exercise\_4\_19}
+
+  Let $A$ and $B$ be arbitrary sets.
+  We show (i) that $\emptyset \in \powerset{(A - B})$ and (ii)
+    $\emptyset \not\in \powerset{A} - \powerset{B}$.
+
+  \paragraph{(i)}%
+  \label{par:exercise-4.19-i}
+
+    By definition of the \nameref{ref:power-set},
+      $$\powerset{(A - B)} = \{ x \mid x \subseteq A - B \}.$$
+    But $\emptyset$ is a subset of \textit{every} set.
+    Thus $\emptyset \in \powerset{(A - B)}$.
+
+  \paragraph{(ii)}%
+
+    By the same reasoning found in \nameref{par:exercise-4.19-i},
+      $\emptyset \in \powerset{A}$ and $\emptyset \in \powerset{B}$.
+    But then, by definition of the relative complement,
+      $\emptyset \not\in \powerset{A} - \powerset{B}$.
+
+  \paragraph{Conclusion}%
+
+    By the \nameref{ref:extensionality-axiom}, the two sets are never equal.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 4.20}}%
+\subsection{\verified{Exercise 4.20}}%
 \label{sub:exercise-4.20}
 
 Let $A$, $B$, and $C$ be sets such that $A \cup B = A \cup C$ and
@@ -1784,22 +1892,95 @@ Show that $B = C$.
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.exercise\_4\_20}
+
+  Let $A$, $B$, and $C$ be arbitrary sets.
+  By the \nameref{ref:extensionality-axiom}, $B = C$ if and only if for all sets
+    $x$, $x \in B \iff x \in C$.
+  We prove both directions of this biconditional.
+
+  \paragraph{($\Rightarrow$)}%
+
+    Suppose $x \in B$.
+    Then there are two cases to consider:
+
+    \subparagraph{Case 1}%
+
+      Assume $x \in A$.
+      Then $x \in A \cap B$.
+      By hypothesis, $A \cap B = A \cap C$.
+      Thus $x \in A \cap C$ immediately implying $x \in C$.
+
+    \subparagraph{Case 2}%
+
+      Assume $x \not\in A$.
+      Then $x \in A \cup B$.
+      By hypothesis, $A \cup B = A \cup C$.
+      Thus $x \in A \cup C$.
+      Since $x \not\in A$, it follows $x \in C$.
+
+  \paragraph{($\Leftarrow$)}%
+
+    Suppose $x \in C$.
+    Then there are two cases to consider:
+
+    \subparagraph{Case 1}%
+
+      Assume $x \in A$.
+      Then $x \in A \cap C$.
+      By hypothesis, $A \cap B = A \cap C$.
+      Thus $x \in A \cap B$, immediately implying $x \in B$.
+
+    \subparagraph{Case 2}%
+
+      Assume $x \not\in A$.
+      Then $x \in A \cup C$.
+      By hypothesis, $A \cup B = A \cup C$.
+      Thus $x \in A \cup B$.
+      Since $x \not\in A$, it follows $x \in B$.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 4.21}}%
+\subsection{\verified{Exercise 4.21}}%
 \label{sub:exercise-4.21}
 
 Show that $\bigcup (A \cup B) = \bigcup A \cup \bigcup B$.
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.exercise\_4\_21}
+
+  Let $A$ and $B$ be arbitrary sets.
+  By the \nameref{ref:extensionality-axiom}, the specified equality holds if and
+    only if for all sets $x$,
+    $$x \in \bigcup (A \cup B) \iff x \in \bigcup A \cup \bigcup B.$$
+  We prove both directions of this biconditional.
+
+  \paragraph{($\Rightarrow$)}%
+
+    Suppose $x \in \bigcup (A \cup B)$.
+    By definition of the union of sets, there exists some $b \in A \cup B$ such
+      that $x \in b$.
+    If $b \in A$, then $x \in \bigcup A$ and $x \in \bigcup A \cup \bigcup B$.
+    Alternatively, if $b \in B$, then $x \in \bigcup B$ and
+      $x \in \bigcup A \cup \bigcup B$.
+    Regardless, $x$ is in the target set.
+
+  \paragraph{($\Leftarrow$)}%
+
+    Suppose $x \in \bigcup A \cup \bigcup B$.
+    Then $x \in \bigcup A$ or $x \in \bigcup B$.
+    WLOG, suppose $x \in \bigcup A$.
+    By definition of the union of sets, there exists some $b \in A$ such that
+      $x \in b$.
+    But then $b \in A \cup B$ meaning $x$ is also a member of
+      $\bigcup (A \cup B)$.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 4.22}}%
+\subsection{\verified{Exercise 4.22}}%
 \label{sub:exercise-4.22}
 
 Show that if $A$ and $B$ are nonempty sets, then
@@ -1807,11 +1988,39 @@ Show that if $A$ and $B$ are nonempty sets, then
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.exercise\_4\_22}
+
+  Let $A$ and $B$ be arbitrary, nonempty sets.
+  By the \nameref{ref:extensionality-axiom}, the specified equality holds if and
+    only if for all sets $x$,
+    \begin{equation}
+      \label{sub:exercise-4.22-eq1}
+      x \in \bigcap (A \cup B) \iff x \in \bigcap A \cap \bigcap B.
+    \end{equation}
+  We prove both directions of this biconditional.
+
+  \paragraph{($\Rightarrow$)}%
+
+    Suppose $x \in \bigcap (A \cup B)$.
+    Then for all $b \in A \cup B$, $x \in B$.
+    In other words, for every member $b_1$ of $A$ and every member $b_2$ of $B$,
+      $x$ is a member of both $b_1$ and $b_2$.
+    But that implies $x \in \bigcap A$ and $x \in \bigcap B$.
+
+  \paragraph{($\Leftarrow$)}%
+
+    Suppose $x \in \bigcap A \cap \bigcap B$.
+    That is, $x \in \bigcap A$ and $x \in \bigcap B$.
+    By definition of the intersection of sets, forall sets $b$, if $b \in A$,
+      then $x \in b$.
+    Likewise, if $b \in B$, then $x \in b$.
+    In other words, if $b$ is a member of either $A$ or $B$, $x \in b$.
+    That immediately implies $x \in \bigcap (A \cup B$.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 4.23}}%
+\subsection{\partial{Exercise 4.23}}%
 \label{sub:exercise-4.23}
 
 Show that if $\mathscr{B}$ is nonempty, then
@@ -1819,46 +2028,186 @@ Show that if $\mathscr{B}$ is nonempty, then
 
 \begin{proof}
 
-  TODO
+  Refer to \nameref{sub:general-distributive-laws}.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 4.24a}}%
+\subsection{\verified{Exercise 4.24a}}%
 \label{sub:exercise-4.24a}
 
 Show that if $\mathscr{A}$ is nonempty, then
-  $\powerset{\bigcap A} = \bigcap\; \{\powerset{X} \mid X \in \mathscr{A} \}$.
+  $\powerset{\bigcap\mathscr{A}} =
+    \bigcap\; \{\powerset{X} \mid X \in \mathscr{A} \}$.
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.exercise\_4\_24a}
+
+  Suppose $\mathscr{A}$ is a nonempty set.
+  Then $\bigcap \mathscr{A}$ is well-defined.
+  Therefore
+    \begin{align*}
+      \powerset{\bigcap\mathscr{A}}
+        & = \{ x \mid x \subseteq \bigcap \mathscr{A} \}
+          & \textref{ref:power-set} \\
+        & = \{ x \mid x \subseteq
+          \{ y \mid \forall X \in \mathscr{A}, y \in X \} \}
+          & \text{def'n intersection} \\
+        & = \{ x \mid \forall t \in x,
+          t \in \{ y \mid \forall X \in \mathscr{A}, y \in X \} \}
+          & \text{def'n subset} \\
+        & = \{ x \mid \forall t \in x,
+          (\forall X \in \mathscr{A}, t \in X) \} \\
+        & = \{ x \mid \forall X \in \mathscr{A},
+          (\forall t \in x, t \in X) \} \\
+        & = \{ x \mid \forall X \in \mathscr{A}, x \subseteq X \} \\
+        & = \{ x \mid \forall X \in \mathscr{A}, x \in \powerset{X} \}
+          & \textref{ref:power-set-axiom} \\
+        & = \{ x \mid
+          \forall t \in \{ \powerset{X} \mid X \in \mathscr{A} \}, x \in t \} \\
+        & = \bigcap\; \{\powerset{X} \mid X \in \mathscr{A}\}.
+    \end{align*}
 
 \end{proof}
 
-\subsection{\unverified{Exercise 4.24b}}%
+\subsection{\verified{Exercise 4.24b}}%
 \label{sub:exercise-4.24b}
 
 Show that
-  $$\bigcup\; \{ \powerset{X} \mid X \in \mathscr{A} \} \subseteq
-    \powerset{\bigcup A}.$$
+  \begin{equation}
+    \label{sub:exercise-4.24b-eq1}
+    \bigcup\; \{ \powerset{X} \mid X \in \mathscr{A} \} \subseteq
+      \powerset{\bigcup\mathscr{A}}.
+  \end{equation}
 Under what conditions does equality hold?
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.exercise\_4\_24b}
+
+  We first prove \eqref{sub:exercise-4.24b-eq1}.
+  Let $x \in \bigcup\; \{ \powerset{X} \mid X \in \mathscr{A} \}$.
+  By definition of the union of sets,
+    $(\exists X \in \mathscr{A}), x \in \powerset{X}$.
+  By definition of the \nameref{ref:power-set}, $x \subseteq X$.
+  By \nameref{sub:exercise-3.3}, $X \subseteq \bigcup \mathscr{A}$.
+  Therefore $x \subseteq \bigcup \mathscr{A}$, proving
+    $x \in \powerset{\mathscr{A}}$ as expected.
+
+  \suitdivider
+
+  \noindent
+  We show $\powerset{\bigcup A} \subseteq 
+    \bigcup\;\{ \powerset{X} \mid X \in \mathscr{A} \}$ if and only if
+    $\bigcup\mathscr{A} \in \mathscr{A}$.
+
+  \paragraph{($\Rightarrow$)}%
+
+    Suppose $\powerset{\bigcup\mathscr{A}} \subseteq
+      \bigcup\;\{ \powerset{X} \mid X \in \mathscr{A} \}$.
+    By definition of the \nameref{ref:power-set},
+      $\bigcup\mathscr{A} \in \powerset{\bigcup\mathscr{A}}$.
+    By hypothesis, $\bigcup\mathscr{A} \in 
+      \bigcup\;\{ \powerset{X} \mid X \in \mathscr{A} \}$.
+    By definition of the union of sets, there exists some $X \in \mathscr{A}$
+      such that $\bigcup\mathscr{A} \in \powerset{X}$.
+    That is, $\bigcup\mathscr{A} \subseteq X$.
+    But $\bigcup\mathscr{A}$ cannot be a proper subset of $X$ since
+      $X \in \mathscr{A}$.
+    Thus $\bigcup\mathscr{A} = X$.
+    This proves $\bigcup\mathscr{A} \in
+      \bigcup\;\{ \powerset{X} \mid X \in \mathscr{A} \}$.
+
+  \paragraph{($\Leftarrow$)}%
+
+    Suppose $\bigcup\mathscr{A} \in A$.
+    Let $x \in \powerset{\bigcup\mathscr{A}}$.
+    Since $\bigcup\mathscr{A} \in \mathscr{A}$, it immediately follows that
+      $x \in \{\powerset{X} \mid X \in \mathscr{A}\}$.
+
+  \paragraph{Conclusion}%
+
+    Equality follows immediately from this fact in conjunction with the proof
+      of \eqref{sub:exercise-4.24b-eq1}.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 4.25}}%
+\subsection{\verified{Exercise 4.25}}%
 \label{sub:exercise-4.25}
 
 Is $A \cup \bigcup \mathscr{B}$ always the same as
-  $\bigcup\; \{ A \cup X \mid X \in \mathscr{B} \}$?
+  $\bigcup\;\{ A \cup X \mid X \in \mathscr{B} \}$?
 If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.exercise\_4\_25}
+
+  We prove that
+    \begin{equation}
+      \label{sub:exercise-4.25-eq1}
+      A \cup \bigcup \mathscr{B} =
+        \bigcup\;\{ A \cup X \mid X \in \mathscr{B} \}
+    \end{equation}
+    if and only if $A = \emptyset$ or $\mathscr{B} \neq \emptyset$.
+  We prove both directions of this biconditional.
+
+  \paragraph{($\Rightarrow$)}%
+
+    Suppose \eqref{sub:exercise-4.25-eq1} holds true.
+    There are two cases to consider:
+
+    \subparagraph{Case 1}%
+
+      Suppose $B \neq \emptyset$.
+      Then $A = \emptyset \lor \mathscr{B} \neq \emptyset$ holds trivially.
+
+    \subparagraph{Case 2}%
+
+      Suppose $B = \emptyset$.
+      Then $$A \cup \bigcup \mathscr{B} = A \cup \bigcup \emptyset = A$$ and
+        $$
+          \bigcup\;\{ A \cup X \mid X \in \mathscr{B} \}
+            = \bigcup \emptyset \\
+            = \emptyset.
+        $$
+      Then by hypothesis \eqref{sub:exercise-4.25-eq1}, $A = \emptyset$.
+      Then $A = \emptyset \lor \mathscr{B} \neq \emptyset$ holds trivially.
+
+  \paragraph{($\Leftarrow$)}%
+
+    Suppose $A = \emptyset$ or $\mathscr{B} \neq \emptyset$.
+    There are two cases to consider:
+
+    \paragraph{Case 1}%
+
+      Suppose $A = \emptyset$.
+      Then $A \cup \bigcup \mathscr{B} = \bigcup{\mathscr{B}}$.
+      Likewise,
+        $$
+          \bigcup \{ A \cup X \mid X \in \mathscr{B} \}
+            = \bigcup \{ X \mid X \in \mathscr{B} \} \\
+            = \bigcup \mathscr{B}.
+        $$
+      Therefore \eqref{sub:exercise-4.25-eq1} holds.
+
+    \paragraph{Case 2}%
+
+      Suppose $B \neq \emptyset$.
+      Then
+        \begin{align*}
+          A \cup \bigcup\mathscr{B}
+            & = \{ x \mid x \in A \lor x \in \bigcup\mathscr{B} \} \\
+            & = \{ x \mid x \in A \lor (\exists b \in \mathscr{B}) x \in b \} \\
+            & = \{ x \mid (\exists b \in \mathscr{B}) x \in A \lor x \in b \} \\
+            & = \{ x \mid (\exists b \in \mathscr{B}) x \in A \cup b \} \\
+            & = \{ x \mid x \in \bigcup \{ A \cup X \mid X \in \mathscr{B} \} \\
+            & = \bigcup \{ A \cup X \mid X \in \mathscr{B} \}.
+        \end{align*}
+      Therefore \eqref{sub:exercise-4.25-eq1} holds.
 
 \end{proof}
 
diff --git a/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean
index 2290fd4..79edd4a 100644
--- a/Bookshelf/Enderton/Set/Chapter_2.lean
+++ b/Bookshelf/Enderton/Set/Chapter_2.lean
@@ -105,8 +105,6 @@ theorem exercise_3_4 (h : A ⊆ B) : ⋃₀ A ⊆ ⋃₀ B := by
 Assume that every member of `𝓐` is a subset of `B`. Show that `⋃ 𝓐 ⊆ B`.
 -/
 theorem exercise_3_5 (h : ∀ x ∈ 𝓐, x ⊆ B) : ⋃₀ 𝓐 ⊆ B := by
-  unfold Set.sUnion sSup Set.instSupSetSet
-  simp only
   show ∀ y ∈ { a | ∃ t, t ∈ 𝓐 ∧ a ∈ t }, y ∈ B
   intro y hy
   rw [Set.mem_setOf_eq] at hy
@@ -117,9 +115,8 @@ theorem exercise_3_5 (h : ∀ x ∈ 𝓐, x ⊆ B) : ⋃₀ 𝓐 ⊆ B := by
 
 Show that for any set `A`, `⋃ 𝓟 A = A`.
 -/
-theorem exercise_3_6a : ⋃₀ (Set.powerset A) = A := by
-  unfold Set.sUnion sSup Set.instSupSetSet Set.powerset
-  simp only
+theorem exercise_3_6a : ⋃₀ (𝒫 A) = A := by
+  show { a | ∃ t, t ∈ { t | t ⊆ A } ∧ a ∈ t } = A
   ext x
   apply Iff.intro
   · intro hx
@@ -136,11 +133,10 @@ theorem exercise_3_6a : ⋃₀ (Set.powerset A) = A := by
 Show that `A ⊆ 𝓟 ⋃ A`. Under what conditions does equality hold?
 -/
 theorem exercise_3_6b
-  : A ⊆ Set.powerset (⋃₀ A)
-  ∧ (A = Set.powerset (⋃₀ A) ↔ ∃ B, A = Set.powerset B) := by
+  : A ⊆ 𝒫 (⋃₀ A)
+  ∧ (A = 𝒫 (⋃₀ A) ↔ ∃ B, A = 𝒫 B) := by
   apply And.intro
-  · unfold Set.powerset
-    show ∀ x ∈ A, x ∈ { t | t ⊆ ⋃₀ A }
+  · show ∀ x ∈ A, x ∈ { t | t ⊆ ⋃₀ A }
     intro x hx
     rw [Set.mem_setOf]
     exact exercise_3_3 x hx
@@ -156,10 +152,8 @@ theorem exercise_3_6b
 Show that for any sets `A` and `B`, `𝓟 A ∩ 𝓟 B = 𝓟 (A ∩ B)`.
 -/
 theorem exercise_3_7A
-  : Set.powerset A ∩ Set.powerset B = Set.powerset (A ∩ B) := by
-  suffices
-    Set.powerset A ∩ Set.powerset B ⊆ Set.powerset (A ∩ B) ∧
-    Set.powerset (A ∩ B) ⊆ Set.powerset A ∩ Set.powerset B from
+  : 𝒫 A ∩ 𝒫 B = 𝒫 (A ∩ B) := by
+  suffices 𝒫 A ∩ 𝒫 B ⊆ 𝒫 (A ∩ B) ∧ 𝒫 (A ∩ B) ⊆ 𝒫 A ∩ 𝒫 B from
     subset_antisymm this.left this.right
   apply And.intro
   · unfold Set.powerset
@@ -178,7 +172,7 @@ theorem exercise_3_7A
 Show that `𝓟 A ∪ 𝓟 B ⊆ 𝓟 (A ∪ B)`.
 -/
 theorem exercise_3_7b_i
-  : Set.powerset A ∪ Set.powerset B ⊆ Set.powerset (A ∪ B) := by
+  : 𝒫 A ∪ 𝒫 B ⊆ 𝒫 (A ∪ B) := by
   unfold Set.powerset
   intro x hx
   simp at hx
@@ -195,7 +189,7 @@ theorem exercise_3_7b_i
 Under what conditions does `𝓟 A ∪ 𝓟 B = 𝓟 (A ∪ B)`.?
 -/
 theorem exercise_3_7b_ii
-  : Set.powerset A ∪ Set.powerset B = Set.powerset (A ∪ B) ↔ A ⊆ B ∨ B ⊆ A := by
+  : 𝒫 A ∪ 𝒫 B = 𝒫 (A ∪ B) ↔ A ⊆ B ∨ B ⊆ A := by
   unfold Set.powerset
   apply Iff.intro
   · intro h
@@ -247,15 +241,15 @@ theorem exercise_3_7b_ii
 Give an example of sets `a` and `B` for which `a ∈ B` but `𝓟 a ∉ 𝓟 B`.
 -/
 theorem exercise_3_9 (ha : a = {1}) (hB : B = {{1}})
-  : a ∈ B ∧ Set.powerset a ∉ Set.powerset B := by
+  : a ∈ B ∧ 𝒫 a ∉ 𝒫 B := by
   apply And.intro
   · rw [ha, hB]
     simp
   · intro h
-    have h₁ : Set.powerset a = {∅, {1}} := by
+    have h₁ : 𝒫 a = {∅, {1}} := by
       rw [ha]
       exact Set.powerset_singleton 1
-    have h₂ : Set.powerset B = {∅, {{1}}} := by
+    have h₂ : 𝒫 B = {∅, {{1}}} := by
       rw [hB]
       exact Set.powerset_singleton {1}
     rw [h₁, h₂] at h
@@ -275,7 +269,7 @@ theorem exercise_3_9 (ha : a = {1}) (hB : B = {{1}})
 Show that if `a ∈ B`, then `𝓟 a ∈ 𝓟 𝓟 ⋃ B`.
 -/
 theorem exercise_3_10 (ha : a ∈ B)
-  : Set.powerset a ∈ Set.powerset (Set.powerset (⋃₀ B)) := by
+  : 𝒫 a ∈ 𝒫 (𝒫 (⋃₀ B)) := by
   have h₁ := exercise_3_3 a ha
   have h₂ := Chapter_1.exercise_1_3 h₁
   generalize hb : 𝒫 (⋃₀ B) = b
@@ -289,11 +283,7 @@ Show that for any sets `A` and `B`, `A = (A ∩ B) ∪ (A - B)`.
 -/
 theorem exercise_4_11_i {A B : Set α}
   : A = (A ∩ B) ∪ (A \ B) := by
-  unfold Union.union Set.instUnionSet Set.union
-  unfold SDiff.sdiff Set.instSDiffSet Set.diff
-  unfold Inter.inter Set.instInterSet Set.inter
-  unfold Membership.mem Set.instMembershipSet Set.Mem setOf
-  simp only
+  show A = fun a => A a ∧ B a ∨ A a ∧ ¬B a
   suffices ∀ x, (A x ∧ (B x ∨ ¬B x)) = A x by
     conv => rhs; ext x; rw [← and_or_left, this]
   intro x
@@ -310,10 +300,7 @@ Show that for any sets `A` and `B`, `A ∪ (B - A) = A ∪ B`.
 -/
 theorem exercise_4_11_ii {A B : Set α}
   : A ∪ (B \ A) = A ∪ B := by
-  unfold Union.union Set.instUnionSet Set.union
-  unfold SDiff.sdiff Set.instSDiffSet Set.diff
-  unfold Membership.mem Set.instMembershipSet Set.Mem setOf
-  simp only
+  show (fun a => A a ∨ B a ∧ ¬A a) = fun a => A a ∨ B a
   suffices ∀ x, ((A x ∨ B x) ∧ (A x ∨ ¬A x)) = (A x ∨ B x) by
     conv => lhs; ext x; rw [or_and_left, this x]
   intro x
@@ -418,4 +405,249 @@ theorem exercise_4_14 : A \ (B \ C) ≠ (A \ B) \ C := by
 
 end
 
+/-- ### Exercise 4.16
+
+Simplify:
+`[(A ∪ B ∪ C) ∩ (A ∪ B)] - [(A ∪ (B - C)) ∩ A]`
+-/
+theorem exercise_4_16 {A B C : Set α}
+  : ((A ∪ B ∪ C) ∩ (A ∪ B)) \ ((A ∪ (B \ C)) ∩ A) = B \ A := by
+  calc ((A ∪ B ∪ C) ∩ (A ∪ B)) \ ((A ∪ (B \ C)) ∩ A)
+    _ = (A ∪ B) \ ((A ∪ (B \ C)) ∩ A) := by rw [Set.union_inter_cancel_left]
+    _ = (A ∪ B) \ A := by rw [Set.union_inter_cancel_left]
+    _ = B \ A := by rw [Set.union_diff_left]
+
+/-! ### Exercise 4.17
+
+Show that the following four conditions are equivalent.
+
+(a) `A ⊆ B`
+(b) `A - B = ∅`
+(c) `A ∪ B = B`
+(d) `A ∩ B = A`
+-/
+
+theorem exercise_4_17_i {A B : Set α} (h : A ⊆ B)
+  : A \ B = ∅ := by
+  ext x
+  apply Iff.intro
+  · intro hx
+    exact absurd (h hx.left) hx.right
+  · intro hx
+    exact False.elim hx
+
+theorem exercise_4_17_ii {A B : Set α} (h : A \ B = ∅)
+  : A ∪ B = B := by
+  suffices A ⊆ B from Set.left_subset_union_eq_self this
+  show ∀ t, t ∈ A → t ∈ B
+  intro t ht
+  rw [Set.ext_iff] at h
+  by_contra nt
+  exact (h t).mp ⟨ht, nt⟩
+
+theorem exercise_4_17_iii {A B : Set α} (h : A ∪ B = B)
+  : A ∩ B = A := by
+  suffices A ⊆ B from Set.inter_eq_left_iff_subset.mpr this
+  exact Set.union_eq_right_iff_subset.mp h
+
+theorem exercise_4_17_iv {A B : Set α} (h : A ∩ B = A)
+  : A ⊆ B := Set.inter_eq_left_iff_subset.mp h
+
+/-- ### Exercise 4.19
+
+Is `𝒫 (A - B)` always equal to `𝒫 A - 𝒫 B`? Is it ever equal to `𝒫 A - 𝒫 B`?
+-/
+theorem exercise_4_19 {A B : Set α}
+  : 𝒫 (A \ B) ≠ (𝒫 A) \ (𝒫 B) := by
+  intro h
+  have he : ∅ ∈ 𝒫 (A \ B) := by simp
+  have ne : ∅ ∉ (𝒫 A) \ (𝒫 B) := by simp
+  rw [Set.ext_iff] at h
+  have := h ∅
+  exact absurd (this.mp he) ne
+
+/-- ### Exercise 4.20
+
+Let `A`, `B`, and `C` be sets such that `A ∪ B = A ∪ C` and `A ∩ B = A ∩ C`.
+Show that `B = C`.
+-/
+theorem exercise_4_20 {A B C : Set α}
+  (hu : A ∪ B = A ∪ C) (hi : A ∩ B = A ∩ C) : B = C := by
+  ext x
+  apply Iff.intro
+  · intro hB
+    by_cases hA : x ∈ A
+    · have : x ∈ A ∩ B := Set.mem_inter hA hB
+      rw [hi] at this
+      exact this.right
+    · have : x ∈ A ∪ B := Set.mem_union_right A hB
+      rw [hu] at this
+      exact Or.elim this (absurd · hA) (by simp)
+  · intro hC
+    by_cases hA : x ∈ A
+    · have : x ∈ A ∩ C := Set.mem_inter hA hC
+      rw [← hi] at this
+      exact this.right
+    · have : x ∈ A ∪ C := Set.mem_union_right A hC
+      rw [← hu] at this
+      exact Or.elim this (absurd · hA) (by simp)
+
+/-- ### Exercise 4.21
+
+Show that `⋃ (A ∪ B) = (⋃ A) ∪ (⋃ B)`.
+-/
+theorem exercise_4_21 {A B : Set (Set α)}
+  : ⋃₀ (A ∪ B) = (⋃₀ A) ∪ (⋃₀ B) := by
+  ext x
+  apply Iff.intro
+  · intro hx
+    have ⟨t, ht⟩ : ∃ t, t ∈ A ∪ B ∧ x ∈ t := hx
+    apply Or.elim ht.left
+    · intro hA
+      exact Or.inl ⟨t, ⟨hA, ht.right⟩⟩
+    · intro hB
+      exact Or.inr ⟨t, ⟨hB, ht.right⟩⟩
+  · intro hx
+    apply Or.elim hx
+    · intro hA
+      have ⟨t, ht⟩ : ∃ t, t ∈ A ∧ x ∈ t := hA
+      exact ⟨t, ⟨Set.mem_union_left B ht.left, ht.right⟩⟩
+    · intro hB
+      have ⟨t, ht⟩ : ∃ t, t ∈ B ∧ x ∈ t := hB
+      exact ⟨t, ⟨Set.mem_union_right A ht.left, ht.right⟩⟩
+
+/-- ### Exercise 4.22
+
+Show that if `A` and `B` are nonempty sets, then `⋂ (A ∪ B) = ⋂ A ∩ ⋂ B`.
+-/
+theorem exercise_4_22 {A B : Set (Set α)}
+  : ⋂₀ (A ∪ B) = ⋂₀ A ∩ ⋂₀ B := by
+  ext x
+  apply Iff.intro
+  · intro hx
+    have : ∀ t : Set α, t ∈ A ∪ B → x ∈ t := hx
+    show (∀ t : Set α, t ∈ A → x ∈ t) ∧ (∀ t : Set α, t ∈ B → x ∈ t)
+    rw [← forall_and]
+    intro t
+    exact ⟨
+      fun ht => this t (Set.mem_union_left B ht),
+      fun ht => this t (Set.mem_union_right A ht)
+    ⟩
+  · intro hx
+    have : ∀ t : Set α, (t ∈ A → x ∈ t) ∧ (t ∈ B → x ∈ t) := by
+      have : (∀ t : Set α, t ∈ A → x ∈ t) ∧ (∀ t : Set α, t ∈ B → x ∈ t) := hx
+      rwa [← forall_and] at this
+    show ∀ (t : Set α), t ∈ A ∪ B → x ∈ t
+    intro t ht
+    apply Or.elim ht
+    · intro hA
+      exact (this t).left hA
+    · intro hB
+      exact (this t).right hB
+
+/-- ### Exercise 4.24a
+
+Show that is `𝓐` is nonempty, then `𝒫 (⋂ 𝓐) = ⋂ { 𝒫 X | X ∈ 𝓐 }`.
+-/
+theorem exercise_4_24a {𝓐 : Set (Set α)}
+  : 𝒫 (⋂₀ 𝓐) = ⋂₀ { 𝒫 X | X ∈ 𝓐 } := by
+  calc 𝒫 (⋂₀ 𝓐)
+    _ = { x | x ⊆ ⋂₀ 𝓐 } := rfl
+    _ = { x | x ⊆ { y | ∀ X, X ∈ 𝓐 → y ∈ X } } := rfl
+    _ = { x | ∀ t ∈ x, t ∈ { y | ∀ X, X ∈ 𝓐 → y ∈ X } } := rfl
+    _ = { x | ∀ t ∈ x, (∀ X, X ∈ 𝓐 → t ∈ X) } := rfl
+    _ = { x | ∀ X ∈ 𝓐, (∀ t, t ∈ x → t ∈ X) } := by
+      ext
+      rw [Set.mem_setOf, Set.mem_setOf, forall_mem_comm (· ∈ ·)]
+    _ = { x | ∀ X ∈ 𝓐, x ⊆ X} := rfl
+    _ = { x | ∀ X ∈ 𝓐, x ∈ 𝒫 X } := rfl
+    _ = { x | ∀ t ∈ { 𝒫 X | X ∈ 𝓐 }, x ∈ t} := by simp
+    _ = ⋂₀ { 𝒫 X | X ∈ 𝓐 } := rfl
+
+/-- ### Exercise 4.24b
+
+Show that
+```
+⋃ {𝒫 X | X ∈ 𝓐} ⊆ 𝒫 ⋃ 𝓐.
+```
+Under what conditions does equality hold?
+-/
+theorem exercise_4_24b {𝓐 : Set (Set α)}
+  : (⋃₀ { 𝒫 X | X ∈ 𝓐 } ⊆ 𝒫 ⋃₀ 𝓐)
+  ∧ ((⋃₀ { 𝒫 X | X ∈ 𝓐 } = 𝒫 ⋃₀ 𝓐) ↔ (⋃₀ 𝓐 ∈ 𝓐)) := by
+  have hS : (⋃₀ { 𝒫 X | X ∈ 𝓐 } ⊆ 𝒫 ⋃₀ 𝓐) := by
+    simp
+    exact exercise_3_3
+  refine ⟨hS, ?_⟩
+  apply Iff.intro
+  · intro rS
+    have rS : 𝒫 ⋃₀ 𝓐 ⊆ ⋃₀ { 𝒫 X | X ∈ 𝓐 } :=
+      (Set.Subset.antisymm_iff.mp rS).right
+    have hA : ⋃₀ 𝓐 ∈ ⋃₀ { 𝒫 X | X ∈ 𝓐 } :=
+      rS Set.self_mem_powerset_self
+    conv at hA =>
+      rhs
+      unfold Set.sUnion sSup Set.instSupSetSet
+      simp only
+    have ⟨X, ⟨⟨x, hx⟩, ht⟩⟩ := Set.mem_setOf.mp hA
+    have : ⋃₀ 𝓐 = x := by
+      rw [← hx.right] at ht
+      have hl : ⋃₀ 𝓐 ⊆ x := ht
+      have hr : x ⊆ ⋃₀ 𝓐 := exercise_3_3 x hx.left
+      exact Set.Subset.antisymm hl hr
+    rw [← this] at hx
+    exact hx.left
+  · intro hA
+    suffices 𝒫 ⋃₀ 𝓐 ⊆ ⋃₀ { 𝒫 X | X ∈ 𝓐 } from
+      subset_antisymm hS this
+    show ∀ x, x ∈ 𝒫 ⋃₀ 𝓐 → x ∈ ⋃₀ { x | ∃ X, X ∈ 𝓐 ∧ 𝒫 X = x }
+    intro x hx
+    unfold Set.sUnion sSup Set.instSupSetSet
+    simp only [Set.mem_setOf_eq, exists_exists_and_eq_and, Set.mem_powerset_iff]
+    exact ⟨⋃₀ 𝓐, ⟨hA, hx⟩⟩
+
+/-- ### Exercise 4.25
+
+Is `A ∪ (⋃ 𝓑)` always the same as `⋃ { A ∪ X | X ∈ 𝓑 }`? If not, then under
+what conditions does equality hold? 
+-/
+theorem exercise_4_25 {A : Set α} (𝓑 : Set (Set α))
+  : (A ∪ (⋃₀ 𝓑) = ⋃₀ { A ∪ X | X ∈ 𝓑 }) ↔ (A = ∅ ∨ Set.Nonempty 𝓑) := by
+  apply Iff.intro
+  · intro h
+    by_cases h𝓑 : Set.Nonempty 𝓑
+    · exact Or.inr h𝓑
+    · have : 𝓑 = ∅ := Set.not_nonempty_iff_eq_empty.mp h𝓑
+      rw [this] at h
+      simp at h
+      exact Or.inl h
+  · intro h
+    apply Or.elim h
+    · intro hA
+      rw [hA]
+      simp
+    · intro h𝓑
+      calc A ∪ (⋃₀ 𝓑)
+        _ = { x | x ∈ A ∨ x ∈ ⋃₀ 𝓑} := rfl
+        _ = { x | x ∈ A ∨ (∃ b ∈ 𝓑, x ∈ b) } := rfl
+        _ = { x | ∃ b ∈ 𝓑, x ∈ A ∨ x ∈ b } := by
+          ext x
+          rw [Set.mem_setOf, Set.mem_setOf]
+          apply Iff.intro
+          · intro hx
+            apply Or.elim hx
+            · intro hA
+              have ⟨b, hb⟩ := Set.nonempty_def.mp h𝓑
+              exact ⟨b, ⟨hb, Or.inl hA⟩⟩
+            · intro ⟨b, hb⟩
+              exact ⟨b, ⟨hb.left, Or.inr hb.right⟩⟩
+          · intro ⟨b, ⟨hb, hx⟩⟩
+            apply Or.elim hx
+            · exact (Or.inl ·)
+            · intro h
+              exact Or.inr ⟨b, ⟨hb, h⟩⟩
+        _ = { x | ∃ b ∈ 𝓑, x ∈ A ∪ b } := rfl
+        _ = { x | ∃ t, t ∈ { y | ∃ X, X ∈ 𝓑 ∧ A ∪ X = y } ∧ x ∈ t } := by simp
+        _ = ⋃₀ { A ∪ X | X ∈ 𝓑 } := rfl
+
 end Enderton.Set.Chapter_2
\ No newline at end of file
diff --git a/Bookshelf/Enderton/Set/images/venn-diagram.png b/Bookshelf/Enderton/Set/images/venn-diagram.png
new file mode 100644
index 0000000..8e21612
Binary files /dev/null and b/Bookshelf/Enderton/Set/images/venn-diagram.png differ
diff --git a/Common/Logic/Basic.lean b/Common/Logic/Basic.lean
index a385dd8..b8bed5a 100644
--- a/Common/Logic/Basic.lean
+++ b/Common/Logic/Basic.lean
@@ -9,10 +9,23 @@ Additional theorems and definitions related to basic logic.
 /--
 The de Morgan law that distributes negation across a conjunction.
 -/
-theorem not_and_de_morgan {a b : Prop} : (¬(a ∧ b)) ↔ (¬ a ∨ ¬ b) := by
+theorem not_and_de_morgan : (¬(p ∧ q)) ↔ (¬p ∨ ¬q) := by
   tauto
 
 /--
 Renaming of `not_or` to indicate its relationship to de Morgan's laws.
 -/
-theorem not_or_de_morgan : ¬(p ∨ q) ↔ ¬p ∧ ¬q := not_or
\ No newline at end of file
+theorem not_or_de_morgan : ¬(p ∨ q) ↔ ¬p ∧ ¬q := not_or
+
+/--
+Universal quantification across nested set memberships can be commuted in either
+order.
+-/
+theorem forall_mem_comm {X : Set α} {Y : Set β} (p : α → β → Prop)
+  : (∀ u ∈ X, (∀ v, v ∈ Y → p u v)) = (∀ v ∈ Y, (∀ u, u ∈ X → p u v)) := by
+  refine propext ?_
+  apply Iff.intro
+  · intro h v hv u hu
+    exact h u hu v hv
+  · intro h u hu v hv
+    exact h v hv u hu
\ No newline at end of file
diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean
index a8e3ffd..509a31a 100644
--- a/Common/Set/Basic.lean
+++ b/Common/Set/Basic.lean
@@ -89,6 +89,14 @@ theorem mem_mem_imp_pair_subset {x y : α}
   · intro hy'
     rwa [hy']
 
+/-! ## Powerset -/
+
+/--
+Every `Set` is a member of its own powerset.
+-/
+theorem self_mem_powerset_self {A : Set α}
+  : A ∈ 𝒫 A := subset_self A
+
 /-! ## Symmetric Difference -/
 
 /--
@@ -116,8 +124,7 @@ This is the contraposition of `mem_symm_diff_iff_exclusive_mem`.
 -/
 theorem not_mem_symm_diff_inter_or_not_union {A B : Set α}
   : x ∉ (A ∆ B) ↔ (x ∈ A ∩ B) ∨ (x ∉ A ∪ B) := by
-  unfold symmDiff
-  simp
+  show ¬(x ∈ A ∧ ¬x ∈ B ∨ x ∈ B ∧ ¬x ∈ A) ↔ x ∈ A ∧ x ∈ B ∨ ¬(x ∈ A ∨ x ∈ B)
   rw [
     not_or_de_morgan,
     not_and_de_morgan, not_and_de_morgan,
@@ -125,16 +132,12 @@ theorem not_mem_symm_diff_inter_or_not_union {A B : Set α}
     not_or_de_morgan
   ]
   apply Iff.intro
-  · intro hx
-    apply Or.elim hx.left
+  · intro nx
+    apply Or.elim nx.left
     · intro nA
-      exact Or.elim hx.right
-        (fun nB => Or.inr ⟨nA, nB⟩)
-        (fun hA => absurd hA nA)
+      exact Or.elim nx.right (Or.inr ⟨nA, ·⟩) (absurd · nA)
     · intro hB
-      apply Or.elim hx.right
-        (fun nB => absurd hB nB)
-        (fun hA => Or.inl ⟨hA, hB⟩)
+      exact Or.elim nx.right (absurd hB ·) (Or.inl ⟨·, hB⟩)
   · intro hx
     apply Or.elim hx
     · intro hy