diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex
index 336862c..7c5074c 100644
--- a/Bookshelf/Enderton/Set.tex
+++ b/Bookshelf/Enderton/Set.tex
@@ -432,7 +432,7 @@ List all the members of $V_4$.
 \section{Exercises 3}%
 \label{sec:exercises-3}
 
-\subsection{\unverified{Exercise 3.1}}%
+\subsection{\verified{Exercise 3.1}}%
 \label{sub:exercise-3.1}
 
 Assume that $A$ is the set of integers divisible by $4$.
@@ -440,25 +440,31 @@ Similarly assume that $B$ and $C$ are the sets of integers divisible by $9$ and
   $10$, respectively.
 What is in $A \cap B \cap C$?
 
-\begin{proof}
+\begin{answer}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_3\_1}
 
-\end{proof}
+  The set of integers divisible by $4$, $9$, and $10$.
 
-\subsection{\unverified{Exercise 3.2}}%
+\end{answer}
+
+\subsection{\verified{Exercise 3.2}}%
 \label{sub:exercise-3.2}
 
 Give an example of sets $A$ and $B$ for which $\bigcup A = \bigcup B$ but
   $A \neq B$.
 
-\begin{proof}
+\begin{answer}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_3\_2}
 
-\end{proof}
+  Let $A = \{\{1\}, \{2\}\}$ and $B = \{\{1, 2\}\}$.
 
-\subsection{\unverified{Exercise 3.3}}%
+\end{answer}
+
+\subsection{\verified{Exercise 3.3}}%
 \label{sub:exercise-3.3}
 
 Show that every member of a set $A$ is a subset of $\bigcup A$.
@@ -466,22 +472,38 @@ Show that every member of a set $A$ is a subset of $\bigcup A$.
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_3\_3}
+
+  Let $x \in A$.
+  By definition, $$\bigcup A = \{ y \mid (\exists b \in A) y \in b\}.$$
+  Then $\{ y \mid y \in x\} \subseteq \bigcup A$.
+  But $\{ y \mid y \in x\} = x$.
+  Thus $x \subseteq \bigcup A$.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 3.4}}%
+\subsection{\verified{Exercise 3.4}}%
 \label{sub:exercise-3.4}
 
 Show that if $A \subseteq B$, then $\bigcup A \subseteq \bigcup B$.
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_3\_4}
+
+  Let $A$ and $B$ be sets such that $A \subseteq B$.
+  Let $x \in \bigcup A$.
+  By definition of the union, there exists some $b \in A$ such that $x \in b$.
+  By definition of the subset, $b \in B$.
+  This immediatley implies $x \in \bigcup B$.
+  Since this holds for all $x \in \bigcup A$, it follows
+    $\bigcup A \subseteq \bigcup B$.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 3.5}}%
+\subsection{\verified{Exercise 3.5}}%
 \label{sub:exercise-3.5}
 
 Assume that every member of $\mathscr{A}$ is a subset of $B$.
@@ -489,22 +511,61 @@ Show that $\bigcup \mathscr{A} \subseteq B$.
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_3\_5}
+
+  Let $x \in \bigcup \mathscr{A}$.
+  By definition,
+    $$\bigcup \mathscr{A} = \{ y \mid (\exists b \in A)y \in b \}.$$
+  Then there exists some $b \in A$ such that $x \in b$.
+  By hypothesis, $b \subseteq B$.
+  Thus $x$ must also be a member of $B$.
+  Since this holds for all $x \in \bigcup \mathscr{A}$, it follows
+    $\bigcup \mathscr{A} \subseteq B$.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 3.6a}}%
+\subsection{\verified{Exercise 3.6a}}%
 \label{sub:exercise-3.6a}
 
 Show that for any set $A$, $\bigcup \powerset{A} = A$.
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_3\_6a}
+
+  We prove that (i) $\bigcup \powerset{A} \subseteq A$ and (ii)
+    $A \subseteq \bigcup \powerset{A}$.
+
+  \paragraph{(i)}%
+  \label{par:exercise-3.6a-i}
+
+    By definition, the \nameref{ref:power-set} of $A$ is the set of all subsets
+      of $A$.
+    In other words, every member of $\powerset{A}$ is a subset of $A$.
+    By \nameref{sub:exercise-3.5}, $\bigcup \powerset{A} \subseteq A$.
+
+  \paragraph{(ii)}%
+  \label{par:exercise-3.6a-ii}
+
+    Let $x \in A$.
+    By definition of the power set of $A$, $\{x\} \in \powerset{A}$. 
+    By definition of the union,
+      $$\bigcup \powerset{A} =
+        \{ y \mid (\exists b \in \powerset{A}), y \in b).$$
+    Since $x \in \{x\}$ and $\{x\} \in \powerset{A}$, it follows
+      $x \in \bigcup \powerset{A}$.
+    Thus $A \subseteq \bigcup \powerset{A}$.
+
+  \paragraph{Conclusion}%
+
+    By \nameref{par:exercise-3.6a-i} and \nameref{par:exercise-3.6a-ii},
+      $\bigcup \powerset{A} = A$.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 3.6b}}%
+\subsection{\verified{Exercise 3.6b}}%
 \label{sub:exercise-3.6b}
 
 Show that $A \subseteq \powerset{\bigcup A}$.
@@ -512,35 +573,176 @@ Under what conditions does equality hold?
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_3\_6b}
+
+  Let $x \in A$.
+  By \nameref{sub:exercise-3.3}, $x$ is a subset of $\bigcup A$.
+  By the definition of the \nameref{ref:power-set},
+    $$\powerset{\bigcup A} = \{ y \mid y \subseteq \bigcup A \}.$$
+  Therefore $x \in \powerset{\bigcup A}$.
+  Since this holds for all $x \in A$, $A \subseteq \powerset{\bigcup A}$.
+
+  \suitdivider
+
+  We show equality holds if and only if there exists some set $B$ such that
+    $A = \powerset{B}$.
+
+  \paragraph{($\Rightarrow$)}%
+  \label{par:exercise-3.6b-right}
+
+    Suppose $A = \powerset{\bigcup A}$.
+    Then our statement immediately follows by settings $B = \bigcup A$.
+
+  \paragraph{($\Leftarrow$)}%
+  \label{par:exercise-3.6b-left}
+
+    Suppose there exists some set $B$ such that $A = \powerset{B}$.
+    Therefore
+      \begin{align*}
+        \powerset{\bigcup A}
+          & = \powerset{\left(\bigcup {\powerset {B}}\right)} \\
+          & = \powerset{B} & \textref{sub:exercise-3.6a} \\
+          & = A.
+      \end{align*}
+
+  \paragraph{Conclusion}%
+
+    By \nameref{par:exercise-3.6b-right} and \nameref{par:exercise-3.6b-left},
+      $A = \powerset{\bigcup A}$ if and only if there exists some set $B$ such
+      that $A = \powerset{B}$.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 3.7a}}%
+\subsection{\verified{Exercise 3.7a}}%
 \label{sub:exercise-3.7a}
 
 Show that for any sets $A$ and $B$,
-  $$\powerset{A} \cap \powerset{B} = \powerset(A \cap B).$$
+  $$\powerset{A} \cap \powerset{B} = \powerset{(A \cap B)}.$$
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_3\_7a}
+
+  Let $A$ and $B$ be arbitrary sets. We show that
+    $\powerset{A} \cap \powerset{B} \subseteq \powerset{(A \cap B)}$ and then
+    show that $\powerset{A} \cap \powerset{B} \supseteq \powerset{(A \cap B)}$.
+
+  \paragraph{($\subseteq$)}%
+
+    Let $x \in \powerset{A} \cap \powerset{B}$.
+    That is, $x \in \powerset{A}$ and $x \in \powerset{B}$.
+    By the definition of the \nameref{ref:power-set},
+      \begin{align*}
+        \powerset{A} & = \{ y \mid y \subseteq A \} \\
+        \powerset{B} & = \{ y \mid y \subseteq B \}
+      \end{align*}
+    Thus $x \subseteq A$ and $x \subseteq B$, meaning $x \subseteq A \cap B$.
+    But then $x \in \powerset{(A \cap B)}$, the set of all subsets of
+      $A \cap B$.
+    Since this holds for all $x \in \powerset{A} \cap \powerset{B}$, it follows
+      $$\powerset{A} \cap \powerset{B} \subseteq \powerset{(A \cap B)}.$$
+
+  \paragraph{($\supseteq$)}%
+
+    Let $x \in \powerset{(A \cap B)}$.
+    By the definition of the \nameref{ref:power-set},
+      $$\powerset{(A \cap B)} = \{ y \mid y \subseteq A \cap B \}.$$
+    Thus $x \subseteq A \cap B$, meaning $x \subseteq A$ and $x \subseteq B$.
+    But this implies $x \in \powerset{A}$, the set of all subsets of $A$.
+    Likewise $x \in \powerset{B}$, the set of all subsets of $B$.
+    Thus $x \in \powerset{A} \cap \powerset{B}$.
+    Since this holds for all $x \in \powerset{(A \cap B)}$, it follows
+      $$\powerset{(A \cap B)} \subseteq \powerset{A} \cap \powerset{B}.$$
+
+  \paragraph{Conclusion}%
+
+    Since each side of our identity is a subset of the other,
+      $$\powerset{(A \cap B)} = \powerset{A} \cap \powerset{B}.$$
 
 \end{proof}
 
-\subsection{\unverified{Exercise 3.7b}}%
+\subsection{\verified{Exercise 3.7b}}%
 \label{sub:exercise-3.7b}
 
-Show that $\powerset{A} \cup \powerset{B} \subseteq \powerset(A \cup B)$.
+Show that $\powerset{A} \cup \powerset{B} \subseteq \powerset{(A \cup B)}$.
 Under what conditions does equality hold?
 
 \begin{proof}
 
-  TODO
+  \  % Add space.
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_3\_7b\_i}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_3\_7b\_ii}
+
+  Let $x \in \powerset{A} \cup \powerset{B}$.
+  By definition, $x \in \powerset{A}$ or $x \in \powerset{B}$ (or both).
+  By the definition of the \nameref{ref:power-set},
+    \begin{align*}
+      \powerset{A} &= \{ y \mid y \subseteq A \} \\
+      \powerset{B} &= \{ y \mid y \subseteq B \}.
+    \end{align*}
+  Thus $x \subseteq A$ or $x \subseteq B$.
+  Therefore $x \subseteq A \cup B$.
+  But then $x \in \powerset{(A \cup B)}$, the set of all subsets of $A \cup B$.
+
+  \suitdivider
+
+  We show equality holds if and only if one of $A$ or $B$ is a subset of the
+    other.
+
+  \paragraph{($\Rightarrow$)}%
+  \label{par:exercise-3.7b-right}
+
+    Suppose
+      \begin{equation}
+        \label{sub:exercise-3.7b-eq1}
+        \powerset{A} \cup \powerset{B} = \powerset{(A \cup B)}.
+      \end{equation}
+    By the definition of the \nameref{ref:power-set},
+      $A \cup B \in \powerset{(A \cup B)}$.
+    Then \eqref{sub:exercise-3.7b-eq1} implies
+      $A \cup B \in \powerset{A} \cup \powerset{B}$.
+    That is, $A \cup B \in \powerset{A}$ or $A \cup B \in \powerset{B}$ (or
+      both).
+
+    For the sake of contradiction, suppose $A \not\subseteq B$ and
+      $B \not\subseteq A$.
+    Then there exists an element $x \in A$ such that $x \not\in B$ and there
+      exists an element $y \in B$ such that $y \not\in A$.
+    But then $A \cup B \not\in \powerset{A}$ since $y$ cannot be a member of a
+      member of $\powerset{A}$.
+    Likewise, $A \cup B \not\in \powerset{B}$ since $x$ cannot be a member of a
+      member of $\powerset{B}$.
+    Therefore our assumption is incorrect.
+    In other words, $A \subseteq B$ or $B \subseteq A$.
+
+  \paragraph{($\Leftarrow$)}%
+  \label{par:exercise-3.7b-left}
+
+    WLOG, suppose $A \subseteq B$.
+    Then, by \nameref{sub:exercise-1.3}, $\powerset{A} \subseteq \powerset{B}$.
+    Thus
+      \begin{align*}
+        \powerset{A} \cup \powerset{B}
+          & = \powerset{B} \\
+          & = \powerset{A \cup B}.
+      \end{align*}
+
+  \paragraph{Conclusion}%
+
+    By \nameref{par:exercise-3.7b-right} and \nameref{par:exercise-3.7b-left},
+      it follows
+      $\powerset{A} \cup \powerset{B} \subseteq \powerset{(A \cup B)}$ if and
+      only if $A \subseteq B$ or $B \subseteq A$.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 3.8}}%
+\subsection{\partial{Exercise 3.8}}%
 \label{sub:exercise-3.8}
 
 Show that there is no set to which every singleton (that is, every set of the
@@ -550,23 +752,37 @@ Show that there is no set to which every singleton (that is, every set of the
 
 \begin{proof}
 
-  TODO
+  We proceed by contradiction.
+  Suppose there existed a set $A$ consisting of every singleton.
+  Then the \nameref{ref:union-axiom} suggests $\bigcup A$ is a set.
+  But this set is precisely the class of all sets, which is \textit{not} a set.
+  Thus our original assumption was incorrect.
+  That is, there is no set to which every singleton belongs.
 
 \end{proof}
 
-\subsection{\unverified{Exercise 3.9}}%
+\subsection{\verified{Exercise 3.9}}%
 \label{sub:exercise-3.9}
 
 Give an example of sets $a$ and $B$ for which $a \in B$ but
-  $\powerset{A} \not\in \powerset{B}$.
+  $\powerset{a} \not\in \powerset{B}$.
 
-\begin{proof}
+\begin{answer}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_3\_9}
 
-\end{proof}
+  Let $a = \{1\}$ and $B = \{\{1\}\}$.
+  Then
+    \begin{align*}
+      \powerset{a} & = \{\emptyset, \{1\}\} \\
+      \powerset{B} & = \{\emptyset, \{\{1\}\}\}.
+    \end{align*}
+  It immediately follows that $\powerset{a} \not\in \powerset{B}$.
 
-\subsection{\unverified{Exercise 3.10}}%
+\end{answer}
+
+\subsection{\verified{Exercise 3.10}}%
 \label{sub:exercise-3.10}
 
 Show that if $a \in B$, then $\powerset{a} \in \powerset{\powerset{\bigcup B}}$.
@@ -574,7 +790,16 @@ Show that if $a \in B$, then $\powerset{a} \in \powerset{\powerset{\bigcup B}}$.
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_3\_10}
+
+  Suppose $a \in B$.
+  By \nameref{sub:exercise-3.3}, $a \subseteq \bigcup B$.
+  By \nameref{sub:exercise-1.3}, $\powerset{a} \subseteq \powerset{\bigcup B}$.
+  By the definition of the \nameref{ref:power-set},
+    $$\powerset{\powerset{\bigcup B}} =
+      \{ y \mid y \subseteq \powerset{\bigcup B} \}.$$
+  Therefore $\powerset{a} \in \powerset{\powerset{\bigcup B}}$.
 
 \end{proof}
 
diff --git a/Bookshelf/Enderton/Set/Chapter_1.lean b/Bookshelf/Enderton/Set/Chapter_1.lean
index bc79def..996ac5c 100644
--- a/Bookshelf/Enderton/Set/Chapter_1.lean
+++ b/Bookshelf/Enderton/Set/Chapter_1.lean
@@ -1,7 +1,10 @@
-import Mathlib.Init.Set
+import Mathlib.Logic.Basic
 import Mathlib.Data.Set.Basic
+import Mathlib.Data.Set.Lattice
 import Mathlib.Tactic.LibrarySearch
 
+import Common.Set.Basic
+
 /-! # Enderton.Chapter_1
 
 Introduction
@@ -104,8 +107,6 @@ theorem exercise_1_2
 Show that if `B ⊆ C`, then `𝓟 B ⊆ 𝓟 C`.
 -/
 theorem exercise_1_3 (h : B ⊆ C) : Set.powerset B ⊆ Set.powerset C := by
-  unfold Set.powerset
-  simp
   intro x hx
   exact Set.Subset.trans hx h
 
@@ -130,4 +131,273 @@ theorem exercise_1_4 (x y : α) (hx : x ∈ B) (hy : y ∈ B)
       (Set.singleton_subset_iff.mpr hx)
       (Set.singleton_subset_iff.mpr hy)
 
+/-- ### Exercise 3.1
+
+Assume that `A` is the set of integers divisible by `4`. Similarly assume that
+`B` and `C` are the sets of integers divisible by `9` and `10`, respectively.
+What is in `A ∩ B ∩ C`?
+-/
+theorem exercise_3_1 {A B C : Set ℤ}
+  (hA : A = { x | Dvd.dvd 4 x })
+  (hB : B = { x | Dvd.dvd 9 x })
+  (hC : C = { x | Dvd.dvd 10 x })
+  : ∀ x ∈ (A ∩ B ∩ C), (4 ∣ x) ∧ (9 ∣ x) ∧ (10 ∣ x) := by
+  intro x h
+  rw [Set.mem_inter_iff] at h
+  have ⟨⟨ha, hb⟩, hc⟩ := h
+  refine ⟨?_, ⟨?_, ?_⟩⟩
+  · rw [hA] at ha
+    exact Set.mem_setOf.mp ha
+  · rw [hB] at hb
+    exact Set.mem_setOf.mp hb
+  · rw [hC] at hc
+    exact Set.mem_setOf.mp hc
+
+/-- ### Exercise 3.2
+
+Give an example of sets `A` and `B` for which `⋃ A = ⋃ B` but `A ≠ B`.
+-/
+theorem exercise_3_2 {A B : Set (Set ℕ)}
+  (hA : A = {{1}, {2}}) (hB : B = {{1, 2}})
+  : Set.sUnion A = Set.sUnion B ∧ A ≠ B := by
+  apply And.intro
+  · show ⋃₀ A = ⋃₀ B
+    ext x
+    show (∃ t, t ∈ A ∧ x ∈ t) ↔ ∃ t, t ∈ B ∧ x ∈ t
+    apply Iff.intro
+    · intro ⟨t, ⟨ht, hx⟩⟩
+      rw [hA] at ht
+      refine ⟨{1, 2}, ⟨by rw [hB]; simp, ?_⟩⟩
+      apply Or.elim ht <;>
+      · intro ht'
+        rw [ht'] at hx
+        rw [hx]
+        simp
+    · intro ⟨t, ⟨ht, hx⟩⟩
+      rw [hB] at ht
+      rw [ht] at hx
+      apply Or.elim hx
+      · intro hx'
+        exact ⟨{1}, ⟨by rw [hA]; simp, by rw [hx']; simp⟩⟩
+      · intro hx'
+        exact ⟨{2}, ⟨by rw [hA]; simp, by rw [hx']; simp⟩⟩
+  · show A ≠ B
+    -- Find an element that exists in `B` but not in `A`. Extensionality
+    -- concludes the proof.
+    intro h
+    rw [hA, hB, Set.ext_iff] at h
+    have h₁ := h {1, 2}
+    simp at h₁
+    rw [Set.ext_iff] at h₁
+    have h₂ := h₁ 2
+    simp at h₂
+
+/-- ### Exercise 3.3
+
+Show that every member of a set `A` is a subset of `U A`. (This was stated as an
+example in this section.)
+-/
+theorem exercise_3_3 {A : Set (Set α)}
+  : ∀ x ∈ A, x ⊆ Set.sUnion A := by
+  intro x hx
+  show ∀ y ∈ x, y ∈ { a | ∃ t, t ∈ A ∧ a ∈ t }
+  intro y hy
+  rw [Set.mem_setOf_eq]
+  exact ⟨x, ⟨hx, hy⟩⟩
+
+/-- ### Exercise 3.4
+
+Show that if `A ⊆ B`, then `⋃ A ⊆ ⋃ B`.
+-/
+theorem exercise_3_4 (h : A ⊆ B) : ⋃₀ A ⊆ ⋃₀ B := by
+  show ∀ x ∈ { a | ∃ t, t ∈ A ∧ a ∈ t }, x ∈ { a | ∃ t, t ∈ B ∧ a ∈ t }
+  intro x hx
+  rw [Set.mem_setOf_eq] at hx
+  have ⟨t, ⟨ht, hxt⟩⟩ := hx
+  rw [Set.mem_setOf_eq]
+  exact ⟨t, ⟨h ht, hxt⟩⟩
+
+/-- ### Exercise 3.5
+
+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
+  have ⟨t, ⟨ht𝓐, hyt⟩⟩ := hy
+  exact (h t ht𝓐) hyt
+
+/-- ### Exercise 3.6a
+
+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
+  ext x
+  apply Iff.intro
+  · intro hx
+    rw [Set.mem_setOf_eq] at hx
+    have ⟨t, ⟨htl, htr⟩⟩ := hx
+    rw [Set.mem_setOf_eq] at htl
+    exact htl htr
+  · intro hx
+    rw [Set.mem_setOf_eq]
+    exact ⟨A, ⟨by rw [Set.mem_setOf_eq], hx⟩⟩
+
+/-- ### Exercise 3.6b
+
+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
+  apply And.intro
+  · unfold Set.powerset
+    show ∀ x ∈ A, x ∈ { t | t ⊆ ⋃₀ A }
+    intro x hx
+    rw [Set.mem_setOf]
+    exact exercise_3_3 x hx
+  · apply Iff.intro
+    · intro hA
+      exact ⟨⋃₀ A, hA⟩
+    · intro ⟨B, hB⟩
+      conv => rhs; rw [hB, exercise_3_6a]
+      exact hB
+
+/-- ### Exercise 3.7a
+
+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
+    subset_antisymm this.left this.right
+  apply And.intro
+  · unfold Set.powerset
+    intro x hx
+    simp only [Set.mem_inter_iff, Set.mem_setOf_eq] at hx
+    rwa [Set.mem_setOf, Set.subset_inter_iff]
+  · unfold Set.powerset
+    simp
+    intro x hA _
+    exact hA
+
+-- theorem false_of_false_iff_true : (false ↔ true) → false := by simp
+
+/-- ### Exercise 3.7b (i)
+
+Show that `𝓟 A ∪ 𝓟 B ⊆ 𝓟 (A ∪ B)`.
+-/
+theorem exercise_3_7b_i
+  : Set.powerset A ∪ Set.powerset B ⊆ Set.powerset (A ∪ B) := by
+  unfold Set.powerset
+  intro x hx
+  simp at hx
+  apply Or.elim hx
+  · intro hA
+    rw [Set.mem_setOf_eq]
+    exact Set.subset_union_of_subset_left hA B
+  · intro hB
+    rw [Set.mem_setOf_eq]
+    exact Set.subset_union_of_subset_right hB A
+
+/-- ### Exercise 3.7b (ii)
+
+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
+  unfold Set.powerset
+  apply Iff.intro
+  · intro h
+    by_contra nh
+    rw [not_or] at nh
+    have ⟨a, hA⟩ := Set.not_subset.mp nh.left
+    have ⟨b, hB⟩ := Set.not_subset.mp nh.right
+    rw [Set.ext_iff] at h
+    have hz := h {a, b}
+    -- `hz` states that `{a, b} ⊆ A ∨ {a, b} ⊆ B ↔ {a, b} ⊆ A ∪ B`. We show the
+    -- left-hand side is false but the right-hand side is true, yielding our
+    -- contradiction.
+    suffices ¬({a, b} ⊆ A ∨ {a, b} ⊆ B) by
+      have hz₁ : a ∈ A ∪ B := by
+        rw [Set.mem_union]
+        exact Or.inl hA.left
+      have hz₂ : b ∈ A ∪ B := by
+        rw [Set.mem_union]
+        exact Or.inr hB.left
+      exact absurd (hz.mpr $ Set.mem_mem_imp_pair_subset hz₁ hz₂) this
+    intro hAB
+    exact Or.elim hAB
+      (fun y => absurd (y $ show b ∈ {a, b} by simp) hB.right)
+      (fun y => absurd (y $ show a ∈ {a, b} by simp) hA.right)
+  · intro h
+    ext x
+    apply Or.elim h
+    · intro hA
+      apply Iff.intro
+      · intro hx
+        exact Or.elim hx
+          (Set.subset_union_of_subset_left · B)
+          (Set.subset_union_of_subset_right · A)
+      · intro hx
+        refine Or.inr (Set.Subset.trans hx ?_)
+        exact subset_of_eq (Set.left_subset_union_eq_self hA)
+    · intro hB
+      apply Iff.intro
+      · intro hx
+        exact Or.elim hx
+          (Set.subset_union_of_subset_left · B)
+          (Set.subset_union_of_subset_right · A)
+      · intro hx
+        refine Or.inl (Set.Subset.trans hx ?_)
+        exact subset_of_eq (Set.right_subset_union_eq_self hB)
+
+/-- ### Exercise 3.9
+
+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
+  apply And.intro
+  · rw [ha, hB]
+    simp
+  · intro h
+    have h₁ : Set.powerset a = {∅, {1}} := by
+      rw [ha]
+      exact Set.powerset_singleton 1
+    have h₂ : Set.powerset B = {∅, {{1}}} := by
+      rw [hB]
+      exact Set.powerset_singleton {1}
+    rw [h₁, h₂] at h
+    simp at h
+    apply Or.elim h
+    · intro h
+      rw [Set.ext_iff] at h
+      have := h ∅
+      simp at this
+    · intro h
+      rw [Set.ext_iff] at h
+      have := h 1
+      simp at this
+
+/-- ### Exercise 3.10
+
+Show that if `a ∈ B`, then `𝓟 a ∈ 𝓟 𝓟 ⋃ B`.
+-/
+theorem exercise_3_10 (ha : a ∈ B)
+  : Set.powerset a ∈ Set.powerset (Set.powerset (⋃₀ B)) := by
+  have h₁ := exercise_3_3 a ha
+  have h₂ := exercise_1_3 h₁
+  generalize hb : 𝒫 (⋃₀ B) = b
+  conv => rhs; unfold Set.powerset
+  rw [← hb, Set.mem_setOf_eq]
+  exact h₂
+
 end Enderton.Set.Chapter_1
\ No newline at end of file
diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean
index 71d013f..dd37419 100644
--- a/Common/Set/Basic.lean
+++ b/Common/Set/Basic.lean
@@ -7,15 +7,17 @@ Additional theorems and definitions useful in the context of `Set`s.
 
 namespace Set
 
+/-! ## Minkowski Sum -/
+
 /-
-The Minkowski sum of two sets `s` and `t` is the set
+The Minkowski sum of two `Set`s `s` and `t` is the set
 `s + t = { a + b : a ∈ s, b ∈ t }`.
 -/
 def minkowskiSum {α : Type u} [Add α] (s t : Set α) :=
   { x | ∃ a ∈ s, ∃ b ∈ t, x = a + b }
 
 /--
-The sum of two sets is nonempty **iff** the summands are nonempty.
+The sum of two `Set`s is nonempty **iff** the summands are nonempty.
 -/
 theorem nonempty_minkowski_sum_iff_nonempty_add_nonempty {α : Type u} [Add α]
   {s t : Set α}
@@ -30,12 +32,59 @@ theorem nonempty_minkowski_sum_iff_nonempty_add_nonempty {α : Type u} [Add α]
   · intro ⟨⟨a, ha⟩, ⟨b, hb⟩⟩
     exact ⟨a + b, ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩⟩
 
+/-! ## Characteristic Function -/
+
 /--
-The characteristic function of a set `S`.
+The characteristic function of a `Set` `S`.
 
 It returns `1` if the specified input belongs to `S` and `0` otherwise.
 -/
 def characteristic (S : Set α) (x : α) [Decidable (x ∈ S)] : Nat :=
   if x ∈ S then 1 else 0
 
+/-! ## Subsets -/
+
+/--
+Every `Set` is a subset of itself.
+-/
+theorem subset_self (S : Set α) : S ⊆ S := by
+  intro _ hs
+  exact hs
+
+/--
+If `Set` `A` is a subset of `Set` `B`, then `A ∪ B = B`.
+-/
+theorem left_subset_union_eq_self {A B : Set α} (h : A ⊆ B)
+  : A ∪ B = B := by
+  rw [Set.ext_iff]
+  intro x
+  apply Iff.intro
+  · intro hU
+    apply Or.elim hU
+    · intro hA
+      exact h hA
+    · simp
+  · intro hB
+    exact Or.inr hB
+
+/--
+If `Set` `B` is a subset of `Set` `A`, then `A ∪ B = B`.
+-/
+theorem right_subset_union_eq_self {A B : Set α} (h : B ⊆ A)
+  : A ∪ B = A := by
+  rw [Set.union_comm]
+  exact left_subset_union_eq_self h
+
+/--
+If `x` and `y` are members of `Set` `A`, it follows `{x, y}` is a subset of `A`.
+-/
+theorem mem_mem_imp_pair_subset {x y : α}
+  (hx : x ∈ A) (hy : y ∈ A) : ({x, y} : Set α) ⊆ A := by
+  intro a ha
+  apply Or.elim ha
+  · intro hx'
+    rwa [hx']
+  · intro hy'
+    rwa [hy']
+
 end Set
\ No newline at end of file
diff --git a/preamble.tex b/preamble.tex
index 368cd8e..abdfb77 100644
--- a/preamble.tex
+++ b/preamble.tex
@@ -29,7 +29,7 @@
 \newcommand\@linespace{\vspace{10pt}}
 \newcommand\linedivider{\@linespace\hrule\@linespace}
 \WithSuffix\newcommand\linedivider*{\@linespace\hrule}
-\newcommand\suitdivider{$$\spadesuit\spadesuit\spadesuit$$}
+\newcommand\suitdivider{$$\spadesuit\;\spadesuit\;\spadesuit$$}
 
 % ========================================
 % Linking
@@ -89,6 +89,7 @@
 \newcommand\@statement[1]{%
   \linedivider*\paragraph{\normalfont\normalsize\textit{#1.}}}
 
+\newenvironment{answer}{\@statement{Answer}}{\hfill$\square$}
 \newenvironment{axiom}{\@statement{Axiom}}{\hfill$\square$}
 \newenvironment{definition}{\@statement{Definition}}{\hfill$\square$}
 \renewenvironment{proof}{\@statement{Proof}}{\hfill$\square$}
@@ -131,7 +132,7 @@
 \newcommand{\ico}[2]{\left[#1, #2\right)}
 \newcommand{\ioc}[2]{\left(#1, #2\right]}
 \newcommand{\ioo}[2]{\left(#1, #2\right)}
-\newcommand{\powerset}[1]{\mathscr{P}\,#1}
+\newcommand{\powerset}[1]{\mathscr{P}#1}
 \newcommand{\ubar}[1]{\text{\b{$#1$}}}
 
 \let\oldemptyset\emptyset