diff --git a/Bookshelf/Apostol.tex b/Bookshelf/Apostol.tex
index 40b7d49..de22435 100644
--- a/Bookshelf/Apostol.tex
+++ b/Bookshelf/Apostol.tex
@@ -32,7 +32,7 @@ The \textbf{characteristic function} of $S$ is the function $\mathcal{X}_S$ such
 
 \begin{definition}
 
-  \lean*{Common/Set/Basic}{Set.characteristic}
+  \code*{Common/Set/Basic}{Set.characteristic}
 
 \end{definition}
 
@@ -160,7 +160,7 @@ A collection of points satisfying \eqref{sec:partition-eq1} is called a
 
 \begin{definition}
 
-  \lean*{Common/Set/Partition}{Set.Partition}
+  \code*{Common/Set/Partition}{Set.Partition}
 
 \end{definition}
 
@@ -192,7 +192,7 @@ That is to say, for each $k = 1, 2, \ldots, n$, there is a real number $s_k$
 
 \begin{definition}
 
-  \lean*{Common/Geometry/StepFunction}{Geometry.StepFunction}
+  \code*{Common/Geometry/StepFunction}{Geometry.StepFunction}
 
 \end{definition}
 
@@ -239,7 +239,7 @@ It is denoted as $\bar{I}(f)$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_I\_03}
+  \code{Bookshelf/Apostol/Chapter\_I\_03}
     {Apostol.Chapter\_I\_03.is\_lub\_neg\_set\_iff\_is\_glb\_set\_neg}
 
   Suppose $L = \sup{S}$ and fix $x \in S$.
@@ -264,7 +264,7 @@ It is denoted as $\bar{I}(f)$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_I\_03}
+  \code{Bookshelf/Apostol/Chapter\_I\_03}
     {Apostol.Chapter\_I\_03.exists\_isGLB}
 
   Let $S$ be a nonempty set bounded below by $x$.
@@ -288,7 +288,7 @@ It is denoted as $\bar{I}(f)$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_I\_03}
+  \code{Bookshelf/Apostol/Chapter\_I\_03}
     {Apostol.Chapter\_I\_03.exists\_pnat\_geq\_self}
 
   Let $n = \abs{\ceil{x}} + 1$.
@@ -313,7 +313,7 @@ It is denoted as $\bar{I}(f)$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_I\_03}
+  \code{Bookshelf/Apostol/Chapter\_I\_03}
     {Apostol.Chapter\_I\_03.exists\_pnat\_mul\_self\_geq\_of\_pos}
 
   Let $x > 0$ and $y$ be an arbitrary real number.
@@ -336,7 +336,7 @@ It is denoted as $\bar{I}(f)$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_I\_03}
+  \code{Bookshelf/Apostol/Chapter\_I\_03}
     {Apostol.Chapter\_I\_03.forall\_pnat\_leq\_self\_leq\_frac\_imp\_eq}
 
   By the trichotomy of the reals, there are three cases to consider:
@@ -382,7 +382,7 @@ It is denoted as $\bar{I}(f)$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_I\_03}
+  \code{Bookshelf/Apostol/Chapter\_I\_03}
     {Apostol.Chapter\_I\_03.forall\_pnat\_frac\_leq\_self\_leq\_imp\_eq}
 
   By the trichotomy of the reals, there are three cases to consider:
@@ -432,7 +432,7 @@ Let $h$ be a given positive number and let $S$ be a set of real numbers.
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_I\_03}
+  \code{Bookshelf/Apostol/Chapter\_I\_03}
     {Apostol.Chapter\_I\_03.sup\_imp\_exists\_gt\_sup\_sub\_delta}
 
   By definition of a \nameref{ref:supremum}, $\sup{S}$ is the least upper
@@ -458,7 +458,7 @@ Let $h$ be a given positive number and let $S$ be a set of real numbers.
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_I\_03}
+  \code{Bookshelf/Apostol/Chapter\_I\_03}
     {Apostol.Chapter\_I\_03.inf\_imp\_exists\_lt\_inf\_add\_delta}
 
   By definition of an \nameref{ref:infimum}, $\inf{S}$ is the greatest lower
@@ -496,7 +496,7 @@ Given nonempty subsets $A$ and $B$ of $\mathbb{R}$, let $C$ denote the set
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_I\_03}
+  \code{Bookshelf/Apostol/Chapter\_I\_03}
     {Apostol.Chapter\_I\_03.sup\_minkowski\_sum\_eq\_sup\_add\_sup}
 
   We prove (i) $\sup{A} + \sup{B}$ is an upper bound of $C$ and (ii)
@@ -567,7 +567,7 @@ Given nonempty subsets $A$ and $B$ of $\mathbb{R}$, let $C$ denote the set
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_I\_03}
+  \code{Bookshelf/Apostol/Chapter\_I\_03}
     {Apostol.Chapter\_I\_03.inf\_minkowski\_sum\_eq\_inf\_add\_inf}
 
   We prove (i) $\inf{A} + \inf{B}$ is a lower bound of $C$ and (ii)
@@ -639,7 +639,7 @@ Given nonempty subsets $A$ and $B$ of $\mathbb{R}$, let $C$ denote the set
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_I\_03}
+  \code{Bookshelf/Apostol/Chapter\_I\_03}
     {Apostol.Chapter\_I\_03.forall\_mem\_le\_forall\_mem\_imp\_sup\_le\_inf}
 
   By hypothesis, $S$ and $T$ are nonempty sets.
@@ -678,7 +678,7 @@ For each set $S$ in $\mathscr{M}$, we have $a(S) \geq 0$.
 
 \begin{axiom}
 
-  \leanp*{Common/Geometry/Area}{Nonnegative-Property}
+  \codep*{Common/Geometry/Area}{Nonnegative-Property}
     {Nonnegative Property}
 
 \end{axiom}
@@ -691,7 +691,7 @@ If $S$ and $T$ are in $\mathscr{M}$, then $S \cup T$ and $S \cap T$ are in
 
 \begin{axiom}
 
-  \leanp*{Common/Geometry/Area}{Additive-Property}
+  \codep*{Common/Geometry/Area}{Additive-Property}
     {Additive Property}
 
 \end{axiom}
@@ -704,7 +704,7 @@ If $S$ and $T$ are in $\mathscr{M}$ with $S \subseteq T$, then $T - S$ is in
 
 \begin{axiom}
 
-  \leanp*{Common/Geometry/Area}{Difference-Property}
+  \codep*{Common/Geometry/Area}{Difference-Property}
     {Difference Property}
 
 \end{axiom}
@@ -717,7 +717,7 @@ If a set $S$ is in $\mathscr{M}$ and if $T$ is congruent to $S$, then $T$ is
 
 \begin{axiom}
 
-  \leanp*{Common/Geometry/Area}{Invariance-Under-Congruence}
+  \codep*{Common/Geometry/Area}{Invariance-Under-Congruence}
     {Invariance Under Congruence}
 
 \end{axiom}
@@ -730,7 +730,7 @@ If the edges of $R$ have lengths $h$ and $k$, then $a(R) = hk$.
 
 \begin{axiom}
 
-  \leanp*{Common/Geometry/Area}{Choice-of-Scale}
+  \codep*{Common/Geometry/Area}{Choice-of-Scale}
     {Choice of Scale}
 
 \end{axiom}
@@ -750,7 +750,7 @@ If there is one and only one number $c$ which satisfies the inequalities
 
 \begin{axiom}
 
-  \leanp*{Common/Geometry/Area}{Exhaustion-Property}
+  \codep*{Common/Geometry/Area}{Exhaustion-Property}
     {Exhaustion Property}
 
 \end{axiom}
@@ -1340,7 +1340,7 @@ $\floor{x + n} = \floor{x} + n$ for every integer $n$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_1\_11}
+  \code{Bookshelf/Apostol/Chapter\_1\_11}
     {Apostol.Chapter\_1\_11.exercise\_4a}
 
   Let $x$ be a real number and $n$ an integer.
@@ -1366,10 +1366,10 @@ $\floor{-x} =
 
   \statementpadding
 
-  \lean*{Bookshelf/Apostol/Chapter\_1\_11}
+  \code*{Bookshelf/Apostol/Chapter\_1\_11}
     {Apostol.Chapter\_1\_11.exercise\_4b\_1}
 
-  \lean{Bookshelf/Apostol/Chapter\_1\_11}
+  \code{Bookshelf/Apostol/Chapter\_1\_11}
     {Apostol.Chapter\_1\_11.exercise\_4b\_2}
 
   There are two cases to consider:
@@ -1409,7 +1409,7 @@ $\floor{x + y} = \floor{x} + \floor{y}$ or $\floor{x} + \floor{y} + 1$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_1\_11}
+  \code{Bookshelf/Apostol/Chapter\_1\_11}
     {Apostol.Chapter\_1\_11.exercise\_4c}
 
   Rewrite $x$ and $y$ as the sum of their floor and fractional components:
@@ -1453,7 +1453,7 @@ $\floor{2x} = \floor{x} + \floor{x + \frac{1}{2}}.$
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_1\_11}
+  \code{Bookshelf/Apostol/Chapter\_1\_11}
     {Apostol.Chapter\_1\_11.exercise\_4d}
 
   This is immediately proven by applying \nameref{sub:hermites-identity}.
@@ -1467,7 +1467,7 @@ $\floor{3x} = \floor{x} + \floor{x + \frac{1}{3}} + \floor{x + \frac{2}{3}}.$
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_1\_11}
+  \code{Bookshelf/Apostol/Chapter\_1\_11}
     {Apostol.Chapter\_1\_11.exercise\_4e}
 
   This is immediately proven by applying \nameref{sub:hermites-identity}.
@@ -1484,7 +1484,7 @@ State and prove such a generalization.
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_1\_11}
+  \code{Bookshelf/Apostol/Chapter\_1\_11}
     {Apostol.Chapter\_1\_11.exercise\_5}
 
   We prove that for all natural numbers $n$ and real numbers $x$, the following
@@ -1710,7 +1710,7 @@ Now apply Exercises 4(a) and (b) to the bracket on the right.
 
 \begin{proof}
 
-  \lean{Bookshelf/Apostol/Chapter\_1\_11}
+  \code{Bookshelf/Apostol/Chapter\_1\_11}
     {Apostol.Chapter\_1\_11.exercise\_7b}
 
   Let $n = 1, \ldots, b - 1$.
diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex
index cd36fcc..dd9f7b9 100644
--- a/Bookshelf/Enderton/Set.tex
+++ b/Bookshelf/Enderton/Set.tex
@@ -111,10 +111,10 @@ The \textbf{composition} of sets $F$ and $G$ is
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.comp}
-
   \lean*{Mathlib/Data/Rel}{Rel.comp}
 
+  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.comp}
+
 \end{definition}
 
 \section{\defined{Connected}}%
@@ -139,10 +139,10 @@ The \textbf{domain} of set $R$, denoted $\dom{R}$, is given by
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.dom}
-
   \lean*{Mathlib/Data/Rel}{Rel.dom}
 
+  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.dom}
+
 \end{definition}
 
 \section{\defined{Empty Set Axiom}}%
@@ -161,13 +161,13 @@ There is a set having no members:
 \hyperlabel{ref:equivalence-class}
 
 The set $[x]_R$ is defined by $$[x]_R = \{t \mid xRt\}.$$
-If $R$ is an \nameref{ref:equivalence-relation} and $x \in fld R$, then $[x]_R$
-  is called the \textbf{equivalence class} of $x$ (\textbf{modulo $R$}).
+If $R$ is an \nameref{ref:equivalence-relation} and $x \in \fld{R}$, then
+  $[x]_R$ is called the \textbf{equivalence class} of $x$ (\textbf{modulo $R$}).
 If the relation $R$ is fixed by the context, we may write just $[x]$.
 
 \begin{definition}
 
-  \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.modEquiv}
+  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.modEquiv}
 
 \end{definition}
 
@@ -180,7 +180,7 @@ Relation $R$ is an \textbf{equivalence relation} on set $A$ if and only if
 
 \begin{definition}
 
-  \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isEquivalence}
+  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isEquivalence}
 
 \end{definition}
 
@@ -271,10 +271,10 @@ The \textbf{image of $A$ under $F$} is the set
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.image}
-
   \lean*{Mathlib/Data/Rel}{Rel.image}
 
+  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.image}
+
 \end{definition}
 
 \section{\defined{Inductive Set}}%
@@ -333,9 +333,9 @@ The \textbf{inverse} of a set $F$ is the set
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.inv}
+  \lean*{Mathlib/Data/Rel}{Rel.inv}
 
-  \lean{Mathlib/Data/Rel}{Rel.inv}
+  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.inv}
 
 \end{definition}
 
@@ -430,10 +430,10 @@ For any sets $u$ and $v$, the \textbf{ordered pair} $\pair{u, v}$ is
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/OrderedPair}{OrderedPair}
-
   \lean*{Prelude}{Prod}
 
+  \code*{Bookshelf/Enderton/Set/OrderedPair}{OrderedPair}
+
 \end{definition}
 
 \section{\defined{Ordering on \texorpdfstring{$\omega$}{Natural Numbers}}}%
@@ -521,7 +521,7 @@ A \textbf{Peano system} is a triple $\langle N, S, e \rangle$ consisting of a
 
 \begin{definition}
 
-  \lean*{Common/Set/Peano}{Peano.System}
+  \code*{Common/Set/Peano}{Peano.System}
 
 \end{definition}
 
@@ -586,10 +586,10 @@ The \textbf{range} of set $R$, denoted $\ran{R}$, is given by
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.ran}
-
   \lean*{Mathlib/Data/Rel}{Rel.codom}
 
+  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.ran}
+
 \end{definition}
 
 \section{\defined{Reflexive}}%
@@ -602,10 +602,10 @@ A binary relation $R$ is \textbf{reflexive} on $A$ if and only if $xRx$ for all
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isReflexive}
-
   \lean*{Mathlib/Init/Algebra/Classes}{IsRefl}
 
+  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isReflexive}
+
 \end{definition}
 
 \section{\defined{Relation}}%
@@ -617,10 +617,10 @@ A \textbf{relation} is a set of \nameref{ref:ordered-pair}s.
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation}
-
   \lean*{Mathlib/Data/Rel}{Rel}
 
+  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation}
+
 \end{definition}
 
 \section{\defined{Restriction}}%
@@ -631,7 +631,7 @@ The \textbf{restriction} of a set $F$ to set $A$ is the set
 
 \begin{definition}
 
-  \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.restriction}
+  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.restriction}
 
 \end{definition}
 
@@ -673,7 +673,7 @@ A binary relation $R$ is \textbf{symmetric} if and only if whenever $xRy$ then
 
 \begin{definition}
 
-  \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isSymmetric}
+  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isSymmetric}
 
 \end{definition}
 
@@ -699,10 +699,10 @@ A binary relation $R$ is \textbf{transitive} if and only if whenever $xRy$ and
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isTransitive}
-
   \lean*{Mathlib/Init/Algebra/Classes}{IsTrans}
 
+  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isTransitive}
+
 \end{definition}
 
 \section{\defined{Transitive Set}}%
@@ -776,7 +776,7 @@ $\{\emptyset\} \_\_\_\_ \{\emptyset, \{\emptyset\}\}$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+  \code{Bookshelf/Enderton/Set/Chapter\_1}
     {Enderton.Set.Chapter\_1.exercise\_1\_1a}
 
   Because the \textit{object} $\{\emptyset\}$ is a member of the right-hand set,
@@ -795,7 +795,7 @@ $\{\emptyset\} \_\_\_\_ \{\emptyset, \{\{\emptyset\}\}\}$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+  \code{Bookshelf/Enderton/Set/Chapter\_1}
     {Enderton.Set.Chapter\_1.exercise\_1\_1b}
 
   Because the \textit{object} $\{\emptyset\}$ is not a member of the right-hand
@@ -813,7 +813,7 @@ $\{\{\emptyset\}\} \_\_\_\_ \{\emptyset, \{\emptyset\}\}$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+  \code{Bookshelf/Enderton/Set/Chapter\_1}
     {Enderton.Set.Chapter\_1.exercise\_1\_1c}
 
   Because the \textit{object} $\{\{\emptyset\}\}$ is not a member of the
@@ -831,7 +831,7 @@ $\{\{\emptyset\}\} \_\_\_\_ \{\emptyset, \{\{\emptyset\}\}\}$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+  \code{Bookshelf/Enderton/Set/Chapter\_1}
     {Enderton.Set.Chapter\_1.exercise\_1\_1d}
 
   Because the \textit{object} $\{\{\emptyset\}\}$ is a member of the right-hand
@@ -850,7 +850,7 @@ $\{\{\emptyset\}\} \_\_ \{\emptyset, \{\emptyset, \{\emptyset\}\}\}$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+  \code{Bookshelf/Enderton/Set/Chapter\_1}
     {Enderton.Set.Chapter\_1.exercise\_1\_1e}
 
   Because the \textit{object} $\{\{\emptyset\}\}$ is not a member of the
@@ -870,7 +870,7 @@ Show that no two of the three sets $\emptyset$, $\{\emptyset\}$, and
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+  \code{Bookshelf/Enderton/Set/Chapter\_1}
     {Enderton.Set.Chapter\_1.exercise\_1\_2}
 
   By the \nameref{ref:extensionality-axiom}, $\emptyset$ is only equal to
@@ -891,7 +891,7 @@ Show that if $B \subseteq C$, then $\powerset{B} \subseteq \powerset{C}$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+  \code{Bookshelf/Enderton/Set/Chapter\_1}
     {Enderton.Set.Chapter\_1.exercise\_1\_3}
 
   Let $x \in \powerset{B}$.
@@ -911,7 +911,7 @@ Show that $\{\{x\}, \{x, y\}\} \in \powerset{\powerset{B}}.$
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+  \code{Bookshelf/Enderton/Set/Chapter\_1}
     {Enderton.Set.Chapter\_1.exercise\_1\_4}
 
   Let $x$ and $y$ be members of set $B$.
@@ -1114,7 +1114,7 @@ List all the members of $V_4$.
 \section{Algebra of Sets}%
 \hyperlabel{sec:algebra-sets}
 
-\subsection{\pending{Commutative Laws}}%
+\subsection{\verified{Commutative Laws}}%
 \hyperlabel{sub:commutative-laws}
 
 For any sets $A$ and $B$,
@@ -1129,7 +1129,13 @@ For any sets $A$ and $B$,
 
   \lean*{Mathlib/Data/Set/Basic}{Set.union\_comm}
 
-  \lean{Mathlib/Data/Set/Basic}{Set.inter\_comm}
+  \lean*{Mathlib/Data/Set/Basic}{Set.inter\_comm}
+
+  \code*{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.commutative\_law\_i}
+
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
+    {Enderton.Set.Chapter\_2.commutative\_law\_ii}
 
   \noindent Let $A$ and $B$ be sets.
   We prove that
@@ -1676,7 +1682,7 @@ Let $A$ and $B$ be sets. $x \not\in A + B$ if and only if either
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Basic}
+  \code{Bookshelf/Enderton/Set/Basic}
     {Set.not\_mem\_symm\_diff\_inter\_or\_not\_union}
 
   By definition of the \nameref{ref:symmetric-difference},
@@ -1712,7 +1718,7 @@ What is in $A \cap B \cap C$?
 
 \begin{answer}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_1}
 
   The set of integers divisible by $4$, $9$, and $10$.
@@ -1727,7 +1733,7 @@ Give an example of sets $A$ and $B$ for which $\bigcup A = \bigcup B$ but
 
 \begin{answer}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_2}
 
   Let $A = \{\{1\}, \{2\}\}$ and $B = \{\{1, 2\}\}$.
@@ -1742,7 +1748,7 @@ Show that every member of a set $A$ is a subset of $\bigcup A$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_3}
 
   Let $x \in A$.
@@ -1760,7 +1766,7 @@ Show that if $A \subseteq B$, then $\bigcup A \subseteq \bigcup B$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_4}
 
   Let $A$ and $B$ be sets such that $A \subseteq B$.
@@ -1781,7 +1787,7 @@ Show that $\bigcup \mathscr{A} \subseteq B$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_5}
 
   Let $x \in \bigcup \mathscr{A}$.
@@ -1802,7 +1808,7 @@ Show that for any set $A$, $\bigcup \powerset{A} = A$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_6a}
 
   We prove that (i) $\bigcup \powerset{A} \subseteq A$ and (ii)
@@ -1843,7 +1849,7 @@ Under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_6b}
 
   Let $x \in A$.
@@ -1892,7 +1898,7 @@ Show that for any sets $A$ and $B$,
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_7a}
 
   Let $A$ and $B$ be arbitrary sets. We show that
@@ -1943,10 +1949,10 @@ Under what conditions does equality hold?
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_2}
+  \code*{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_7b\_i}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_7b\_ii}
 
   Let $x \in \powerset{A} \cup \powerset{B}$.
@@ -2039,7 +2045,7 @@ Give an example of sets $a$ and $B$ for which $a \in B$ but
 
 \begin{answer}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_9}
 
   Let $a = \{1\}$ and $B = \{\{1\}\}$.
@@ -2060,7 +2066,7 @@ Show that if $a \in B$, then $\powerset{a} \in \powerset{\powerset{\bigcup B}}$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_10}
 
   Suppose $a \in B$.
@@ -2084,10 +2090,10 @@ Show that for any sets $A$ and $B$,
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_2}
+  \code*{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_11\_i}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_11\_ii}
 
   \noindent Let $A$ and $B$ be sets.
@@ -2166,7 +2172,7 @@ Show by example that for some sets $A$, $B$, and $C$, the set $A - (B - C)$ is
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_14}
 
   Let $A = \{1, 2, 3\}$, $B = \{2, 3, 4\}$, and $C = \{3, 4, 5\}$.
@@ -2328,7 +2334,7 @@ Simplify:
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_16}
 
   Let $A$, $B$, and $C$ be arbitrary sets.
@@ -2363,16 +2369,16 @@ Show that the following four conditions are equivalent.
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_2}
+  \code*{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_17\_i}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_2}
+  \code*{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_17\_ii}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_2}
+  \code*{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_17\_iii}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_17\_iv}
 
   Let $A$ and $B$ be arbitrary sets.
@@ -2452,7 +2458,7 @@ Is it ever equal to $\powerset{A} - \powerset{B}$?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_19}
 
   Let $A$ and $B$ be arbitrary sets.
@@ -2489,7 +2495,7 @@ Show that $B = C$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_20}
 
   Let $A$, $B$, and $C$ be arbitrary sets.
@@ -2546,7 +2552,7 @@ Show that $\bigcup (A \cup B) = \bigcup A \cup \bigcup B$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_21}
 
   Let $A$ and $B$ be arbitrary sets.
@@ -2585,7 +2591,7 @@ Show that if $A$ and $B$ are nonempty sets, then
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_22}
 
   Let $A$ and $B$ be arbitrary, nonempty sets.
@@ -2638,7 +2644,7 @@ Show that if $\mathscr{A}$ is nonempty, then
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_24a}
 
   Suppose $\mathscr{A}$ is a nonempty set.
@@ -2681,7 +2687,7 @@ Under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_24b}
 
   We first prove \eqref{sub:exercise-2.24b-eq1}.
@@ -2740,7 +2746,7 @@ If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_2}
+  \code{Bookshelf/Enderton/Set/Chapter\_2}
     {Enderton.Set.Chapter\_2.exercise\_2\_25}
 
   We prove that
@@ -2829,7 +2835,7 @@ If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.OrderedPair.ext\_iff}
 
   Let $x$, $y$, $u$, and $v$ be arbitrary sets.
@@ -2901,7 +2907,7 @@ If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.theorem\_3b}
 
   Let $C$ be an arbitrary set and $x, y \in C$.
@@ -2963,7 +2969,7 @@ If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.theorem\_3d}
 
   Let $A$ be a set and $\pair{x, y} \in A$.
@@ -2994,13 +3000,13 @@ If not, then under what conditions does equality hold?
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Relation}
+  \code*{Bookshelf/Enderton/Set/Relation}
     {Set.Relation.dom\_inv\_eq\_ran\_self}
 
-  \lean*{Bookshelf/Enderton/Set/Relation}
+  \code*{Bookshelf/Enderton/Set/Relation}
     {Set.Relation.ran\_inv\_eq\_dom\_self}
 
-  \lean{Bookshelf/Enderton/Set/Relation}
+  \code{Bookshelf/Enderton/Set/Relation}
     {Set.Relation.inv\_inv\_eq\_self}
 
   We prove that (i) $\dom{(F^{-1})} = \ran{F}$, (ii) $\ran{(F^{-1})} = \dom{F}$,
@@ -3052,10 +3058,10 @@ If not, then under what conditions does equality hold?
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Relation}
+  \code*{Bookshelf/Enderton/Set/Relation}
     {Set.Relation.single\_valued\_inv\_iff\_single\_rooted\_self}
 
-  \lean{Bookshelf/Enderton/Set/Relation}
+  \code{Bookshelf/Enderton/Set/Relation}
     {Set.Relation.single\_valued\_self\_iff\_single\_rooted\_inv}
 
   We prove that (i) any set $F$, $F^{-1}$ is a function iff $F$ is
@@ -3121,7 +3127,7 @@ If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Relation}
+  \code{Bookshelf/Enderton/Set/Relation}
     {Set.Relation.one\_to\_one\_self\_iff\_one\_to\_one\_inv}
 
   We prove that (i) $F^{-1}$ is a function and (ii) $F^{-1}$ is single-rooted.
@@ -3172,10 +3178,10 @@ If not, then under what conditions does equality hold?
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.theorem\_3g\_i}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.theorem\_3g\_ii}
 
   Suppose $F$ is a one-to-one \nameref{ref:function}.
@@ -3211,10 +3217,10 @@ If not, then under what conditions does equality hold?
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Relation}
+  \code*{Bookshelf/Enderton/Set/Relation}
     {Set.Relation.single\_valued\_comp\_is\_single\_valued}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.theorem\_3h\_dom}
 
   Let $F$ and $G$ be \nameref{ref:function}s.
@@ -3265,7 +3271,7 @@ If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Relation}
+  \code{Bookshelf/Enderton/Set/Relation}
     {Set.Relation.comp\_inv\_eq\_inv\_comp\_inv}
 
   By definition of the \nameref{ref:composition} of $F$ and $G$,
@@ -3389,7 +3395,7 @@ If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.theorem\_3k\_a}
 
   Let $F$, $A$, $B$, and $\mathscr{A}$ be arbitrary sets.
@@ -3464,10 +3470,10 @@ If not, then under what conditions does equality hold?
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.theorem\_3k\_b\_i}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.theorem\_3k\_b\_ii}
 
   Let $F$, $A$, $B$ be arbitrary sets.
@@ -3550,10 +3556,10 @@ If not, then under what conditions does equality hold?
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.theorem\_3k\_c\_i}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.theorem\_3k\_c\_ii}
 
   We prove that (i) \eqref{sub:theorem-3k-c-eq1} holds and (ii) equality holds
@@ -3613,13 +3619,13 @@ If not, then under what conditions does equality hold?
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.corollary\_3l\_i}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.corollary\_3l\_ii}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.corollary\_3l\_iii}
 
   \nameref{sub:theorem-3k-a} implies \eqref{sub:corollary-3l-eq1}.
@@ -3644,7 +3650,7 @@ If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.theorem\_3m}
 
   Suppose $R$ is a \nameref{ref:symmetric} and \nameref{ref:transitive}
@@ -3681,7 +3687,7 @@ If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Relation}
+  \code{Bookshelf/Enderton/Set/Relation}
     {Set.Relation.neighborhood\_iff\_mem}
 
   Suppose $R$ is an \nameref{ref:equivalence-relation} on set $A$.
@@ -3730,7 +3736,7 @@ If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Relation}
+  \code{Bookshelf/Enderton/Set/Relation}
     {Set.Relation.modEquiv\_partition}
 
   Let $\Pi = \{[x]_R \mid x \in A\}$.
@@ -3838,7 +3844,7 @@ If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.theorem\_3r}
 
   Suppose $R$ is a \nameref{ref:linear-ordering} on $A$.
@@ -3875,7 +3881,7 @@ Show that this definition is unsuccessful by giving examples of objects
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_1}
 
   Let $x = 1$, $y = 1$, and $z = 2$.
@@ -3905,7 +3911,7 @@ Show that $A \times (B \cup C) = (A \times B) \cup (A \times C)$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_2a}
 
   Let $A$, $B$, and $C$ be arbitrary sets.
@@ -3931,7 +3937,7 @@ Show that if $A \times B = A \times C$ and $A \neq \emptyset$, then $B = C$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_2b}
 
   Let $A$, $B$, and $C$ be arbitrary sets such that $A \neq \emptyset$.
@@ -3977,7 +3983,7 @@ Show that $A \times \bigcup \mathscr{B} =
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_3}
 
   Let $A$ and $\mathscr{B}$ be arbitrary sets.
@@ -4027,7 +4033,7 @@ In other words, show that $\{\{x\} \times B \mid x \in A\}$ is a set.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_5a}
 
   Let $a \in A$.
@@ -4076,7 +4082,7 @@ With $A$, $B$, and $C$ as above, show that $A \times B = \bigcup C$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_5b}
 
   Let $A$ and $B$ be arbitrary sets.
@@ -4126,7 +4132,7 @@ Show that a set $A$ is a relation iff $A \subseteq \dom{A} \times \ran{A}$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_6}
 
   Let $A$ be a set.
@@ -4160,7 +4166,7 @@ Show that if $R$ is a relation, then $\fld{R} = \bigcup\bigcup R$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_7}
 
   Let $R$ be a \nameref{ref:relation}.
@@ -4217,10 +4223,10 @@ Show that for any set $\mathscr{A}$:
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_8\_i}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_8\_ii}
 
   We prove (i) \eqref{sub:exercise-3.8-eq1} and then (ii)
@@ -4270,10 +4276,10 @@ Discuss the result of replacing the union operation by the intersection
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_9\_i}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_9\_ii}
 
   Replacing the union operation with the intersection problem produces the
@@ -4381,7 +4387,7 @@ Assume that $f$ and $g$ are functions and show that
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_12}
 
   Let $f$ and $g$ be \nameref{ref:function}s.
@@ -4417,7 +4423,7 @@ Show that $f = g$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_13}
 
   Let $f$ and $g$ be functions such that $f \subseteq g$ and
@@ -4445,10 +4451,10 @@ Assume that $f$ and $g$ are functions.
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_14\_a}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_14\_b}
 
   Assume $f$ and $g$ are \nameref{ref:function}s.
@@ -4506,7 +4512,7 @@ Show that $\bigcup{\mathscr{A}}$ is a function.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_15}
 
   Let $\mathscr{A}$ be a set of \nameref{ref:function}s such that for any $f$
@@ -4569,10 +4575,10 @@ Conclude that the composition of two one-to-one functions is again one-to-one.
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_17\_i}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_17\_ii}
 
   Let $F$ and $G$ be two single-rooted sets.
@@ -4617,19 +4623,19 @@ Evaluate the following: $R \circ R$, $R \restriction \{1\}$,
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_18\_i}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_18\_ii}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_18\_iii}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_18\_iv}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_18\_v}
 
   \begin{enumerate}[(i)]
@@ -4659,34 +4665,34 @@ Evaluate each of the following: $A(\emptyset)$, $\img{A}{\emptyset}$,
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_19\_i}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_19\_ii}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_19\_iii}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_19\_iv}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_19\_v}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_19\_vi}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_19\_vii}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_19\_viii}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_19\_ix}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_19\_x}
 
   \begin{enumerate}[(i)]
@@ -4718,7 +4724,7 @@ Show that $F \restriction A = F \cap (A \times \ran{F})$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_20}
 
   Let $F$ and $A$ be arbitrary sets.
@@ -4744,7 +4750,7 @@ Show that $(R \circ S) \circ T = R \circ (S \circ T)$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Relation}
+  \code{Bookshelf/Enderton/Set/Relation}
     {Set.Relation.comp\_assoc}
 
   Let $R$, $S$, and $T$ be arbitrary sets.
@@ -4784,13 +4790,13 @@ Show that the following are correct for any sets.
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_22\_a}
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_22\_b}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_22\_c}
 
   Let $A$, $B$, $F$, $G$, and $Q$ be arbitrary sets.
@@ -4853,10 +4859,10 @@ Show that for any sets $B$ and $C$,
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_23\_i}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_23\_ii}
 
   Let $I_A$ be the identity function on the set $A$.
@@ -4911,7 +4917,7 @@ Show that for a function $F$,
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_24}
 
   Let $F$ be a function.
@@ -4942,10 +4948,10 @@ Show that for a function $F$,
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_25\_b}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_25\_a}
 
   \paragraph{(b)}%
@@ -5006,7 +5012,7 @@ Show that $\dom{(F \circ G)} = \img{G^{-1}}{\dom{F}}$ for any sets $F$ and $G$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_27}
 
   Let $F$ and $G$ be arbitrary sets.
@@ -5052,7 +5058,7 @@ Show that $G$ maps $\powerset{A}$ one-to-one into $\powerset{B}$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_28}
 
   By construction, $\dom{G} = \powerset{A}$.
@@ -5089,7 +5095,7 @@ Does the converse hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_39}
 
   Let $f \colon A \rightarrow B$ such that $f$ maps $A$ onto $B$.
@@ -5228,7 +5234,7 @@ Show that $R$ is symmetric iff $R^{-1} \subseteq R$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_32\_a}
 
   \paragraph{($\Rightarrow$)}%
@@ -5259,7 +5265,7 @@ Show that $R$ is transitive iff $R \circ R \subseteq R$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_32\_b}
 
   \paragraph{($\Rightarrow$)}%
@@ -5290,7 +5296,7 @@ Show that $R$ is a symmetric and transitive relation iff $R = R^{-1} \circ R$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_33}
 
   By definition of the \nameref{ref:inverse} and \nameref{ref:composition}
@@ -5378,10 +5384,10 @@ Assume that $\mathscr{A}$ is a nonempty set, every member of which is a
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_34\_a}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_34\_b}
 
   \paragraph{(a)}%
@@ -5420,7 +5426,7 @@ Show that for any $R$ and $x$, we have $[x]_R = \img{R}{\{x\}}$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_35}
 
   Let $R$ and $x$ be arbitrary sets.
@@ -5448,7 +5454,7 @@ Show that $Q$ is an equivalence relation on $A$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_36}
 
   We prove that (i) $Q$ is \nameref{ref:reflexive} on $A$, (ii) $Q$ is
@@ -5499,7 +5505,7 @@ Show that $R_\Pi$ is an equivalence relation on $A$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_37}
 
   We prove that (i) $R_\Pi$ is \nameref{ref:reflexive} on $B$, (ii) $R_\Pi$ is
@@ -5547,7 +5553,7 @@ Show that if we start with the equivalence relation $R_\Pi$ of the preceding
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_38}
 
   By definition,
@@ -5639,7 +5645,7 @@ Show that $R_\Pi$, as defined in Exercise 37, is just $R$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_39}
 
   By definition,
@@ -5714,7 +5720,7 @@ Show that $Q$ is an equivalence relation on $\mathbb{R} \times \mathbb{R}$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_41\_a}
 
   We show (i) $Q$ is \nameref{ref:reflexive} on $\mathbb{R} \times \mathbb{R}$,
@@ -5823,7 +5829,7 @@ Show that $R^{-1}$ is also a linear ordering on $A$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_43}
 
   Assume that $R$ is a \nameref{ref:linear-ordering} on a set $A$.
@@ -5871,10 +5877,10 @@ Show that $f$ is one-to-one and that whenever $f(x) < f(y)$, then $x < y$.
 
   \statementpadding
 
-  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_44\_i}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_44\_ii}
 
   We show that (i) $f$ is one-to-one and (ii) whenever $f(x) < f(y)$, then
@@ -5964,7 +5970,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.exercise\_3\_45}
 
   We show that $<_L$ is (i) \nameref{ref:transitive} and (ii)
@@ -6133,7 +6139,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_4}
+  \code{Bookshelf/Enderton/Set/Chapter\_4}
     {Enderton.Set.Chapter\_4.theorem\_4c}
 
   Let $T = \{n \mid n = 0 \lor (\exists m) n = m^+\}$.
@@ -6254,7 +6260,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \begin{proof}
 
-  \lean{Common/Set/Peano}{Peano.instSystemNatUnivSuccOfNatInstOfNatNat}
+  \code{Common/Set/Peano}{Peano.instSystemNatUnivSuccOfNatInstOfNatNat}
 
   Note $\sigma$ is defined as $\sigma = \{\pair{n, n^+} \mid n \in \omega\}$.
   To prove $\langle \omega, \sigma, 0 \rangle$ is a \nameref{ref:peano-system},
@@ -7352,7 +7358,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_4}
+  \code{Bookshelf/Enderton/Set/Chapter\_4}
     {Enderton.Set.Chapter\_4.zero\_least\_nat}
 
   Let $$S = \{n \in \omega \mid n = 0 \lor 0 \in n\}.$$
@@ -7397,7 +7403,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_4}
+  \code{Bookshelf/Enderton/Set/Chapter\_4}
     {Enderton.Set.Chapter\_4.trichotomy\_law\_for\_nat}
 
   Let $n \in \omega$ and define
@@ -7482,7 +7488,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_4}
+  \code{Bookshelf/Enderton/Set/Chapter\_4}
     {Enderton.Set.Chapter\_4.linear\_ordering\_on\_nat}
 
   By definition, \eqref{sub:linear-ordering-natural-numbers-eq1} is a
@@ -7717,7 +7723,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
   \lean*{Init/Data/Nat/Basic}{Nat.add\_right\_cancel}
 
-  \lean{Common/Nat/Basic}{Nat.mul\_right\_cancel}
+  \code{Common/Nat/Basic}{Nat.mul\_right\_cancel}
 
   \paragraph{\eqref{sub:corollary-4p-eq1}}%
 
@@ -7807,7 +7813,7 @@ Show that $1 \neq 3$ i.e., that $\emptyset^+ \neq \emptyset^{+++}$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_4}
+  \code{Bookshelf/Enderton/Set/Chapter\_4}
     {Enderton.Set.Chapter\_4.exercise\_4\_1}
 
   By definition,
@@ -8172,7 +8178,7 @@ Show that either $m = 0$ or $n = 0$.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_4}
+  \code{Bookshelf/Enderton/Set/Chapter\_4}
     {Enderton.Set.Chapter\_4.exercise\_4\_13}
 
   Suppose $m \cdot n = 0$.
@@ -8203,7 +8209,7 @@ Show that each natural number is either even or odd, but never both.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_4}
+  \code{Bookshelf/Enderton/Set/Chapter\_4}
     {Enderton.Set.Chapter\_4.exercise\_4\_14}
 
   Let $$S = \{n \in \omega \mid n \text{ is even or odd but not both}\}.$$
diff --git a/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean
index eba3a73..2386f27 100644
--- a/Bookshelf/Enderton/Set/Chapter_2.lean
+++ b/Bookshelf/Enderton/Set/Chapter_2.lean
@@ -9,6 +9,34 @@ Axioms and Operations
 
 namespace Enderton.Set.Chapter_2
 
+/-! #### Commutative Laws
+
+For any sets `A` and `B`,
+```
+A ∪ B = B ∪ A
+A ∩ B = B ∩ A
+```
+-/
+
+#check Set.union_comm
+
+theorem commutative_law_i (A B : Set α)
+  : A ∪ B = B ∪ A := calc A ∪ B
+  _ = { x | x ∈ A ∨ x ∈ B } := rfl
+  _ = { x | x ∈ B ∨ x ∈ A } := by
+    ext
+    exact or_comm
+  _ = B ∪ A := rfl
+
+#check Set.inter_comm
+
+theorem commutative_law_ii (A B : Set α)
+  : A ∩ B = B ∩ A := calc A ∩ B
+  _ = { x | x ∈ A ∧ x ∈ B } := rfl
+  _ = { x | x ∈ B ∧ x ∈ A } := by
+    ext
+    exact and_comm
+  _ = B ∩ A := rfl
 
 /-- #### Exercise 2.1
 
diff --git a/Common/Real/Sequence.tex b/Common/Real/Sequence.tex
index e8edd00..965b9d6 100644
--- a/Common/Real/Sequence.tex
+++ b/Common/Real/Sequence.tex
@@ -24,7 +24,7 @@ Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$.
 
 \begin{proof}
 
-  \lean{Common/Real/Sequence/Arithmetic}
+  \code{Common/Real/Sequence/Arithmetic}
     {Real.Arithmetic.sum\_recursive\_closed}
 
   Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$.
@@ -84,7 +84,7 @@ Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$.
 
 \begin{proof}
 
-  \lean{Common/Real/Sequence/Geometric}
+  \code{Common/Real/Sequence/Geometric}
     {Real.Geometric.sum\_recursive\_closed}
 
   Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$.
diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean
index 7033767..da4be39 100644
--- a/DocGen4/Output/Index.lean
+++ b/DocGen4/Output/Index.lean
@@ -40,28 +40,26 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
           <li>
             <span style="color:darkgray">Dark gray statements </span> are
             reserved for definitions and axioms that have been encoded in LaTeX.
-            A corresponding reference to a definition/axiom in Lean may also be
-            provided.
+            A reference to a definition in Lean may also be provided.
           </li>
           <li>
             <span style="color:teal">Teal statements </span> are reserved for
-            statements, theorems, lemmas, etc. that have been proven in both
-            LaTeX and Lean.
+            statements, theorems, lemmas, etc. that have been proven in LaTeX
+            and have a corresponding proof in Lean.
           </li>
           <li>
             <span style="color:olive">Olive statements </span> are reserved for
-            statements, theorems, lemmas, etc. that have been proven in LaTeX
-            and will <i>not </i> be proven in Lean.
+            statements, theorems, lemmas, etc. that have been proven in LaTeX.
+            A reference to a statement in Lean may also be provided.
           </li>
           <li>
             <span style="color:fuchsia">Fuchsia statements </span> are reserved
-            for definitions, axioms, statements, theorems, lemmas, etc. that
-            have been proven or encoded in LaTeX and <i>will </i> be encoded in
-            Lean.
+            for statements, theorems, lemmas, etc. that have been proven in
+            LaTeX and <i>will </i> have a corresponding proof in Lean.
           </li>
           <li>
             <span style="color:maroon">Maroon </span> serves as a catch-all for
-            all statements that don't fit the above categorizations. Incomplete
+            statements that don't fit the above categorizations. Incomplete
             definitions, statements without proof, etc. belong here.
           </li>
         </ul>
diff --git a/preamble.tex b/preamble.tex
index cb04f75..f5db378 100644
--- a/preamble.tex
+++ b/preamble.tex
@@ -9,7 +9,9 @@
 \usepackage{mathabx, mathrsfs}
 \usepackage{soul}
 \usepackage{stmaryrd}
-\usepackage[usenames,dvipsnames]{xcolor}
+% Must load `xcolor` before `tikz`.
+\usepackage[dvipsnames]{xcolor}
+\usepackage{tikz}
 % `hyperref` comes after `xr-hyper`.
 \usepackage{xr-hyper}
 \usepackage{hyperref}
@@ -42,8 +44,17 @@
   \label{#1}%
   \hypertarget{#1}{}}
 
+% Denote whether we are working with a standard/Mathlib statement (lean) or a
+% custom one (code).
 \newcommand\@leanlink[4]{%
-  \textcolor{blue}{$\pmb{\exists}\;{-}\;$}\href{#1/#2.html\##3}{#4}}
+  \textcolor{blue}{\raisebox{-4.5pt}{%
+    \tikz{\draw (0, 0) node[yscale=-1,xscale=1] {\faFont};}}}%
+  {-\;}\href{#1/#2.html\##3}{#4}}
+
+\newcommand\@codelink[4]{%
+  \textcolor{blue}{\raisebox{-4.5pt}{%
+    \tikz{\draw (0, 0) node[] {\faCodeBranch};}}}%
+  {-\;}\href{#1/#2.html\##3}{#4}}
 
 % Reference to an anchor of Lean documentation.
 \newcommand\leanref[3]{%
@@ -51,22 +62,43 @@
 \WithSuffix\newcommand\leanref*[3]{%
   \@leanlink{#1}{#2}{#3}{#3}}
 
-% Variant that allows customizing display text.
+\newcommand\coderef[3]{%
+  \@codelink{#1}{#2}{#3}{#3}\vspace{10pt}}
+\WithSuffix\newcommand\coderef*[3]{%
+  \@codelink{#1}{#2}{#3}{#3}}
+
+% Variants that allows customizing display text.
 \newcommand\leanpref[4]{%
   \@leanlink{#1}{#2}{#3}{#4}\vspace{10pt}}
 \WithSuffix\newcommand\leanpref*[4]{%
   \@leanlink{#1}{#2}{#3}{#4}}
 
+\newcommand\codepref[4]{%
+  \@codelink{#1}{#2}{#3}{#4}\vspace{10pt}}
+\WithSuffix\newcommand\codepref*[4]{%
+  \@codelink{#1}{#2}{#3}{#4}}
+
 % Macro to build all Lean related commands relative to a specified directory.
 \newcommand\makeleancommands[1]{%
   \newcommand\lean[2]{%
     \leanref{#1}{##1}{##2}}
   \WithSuffix\newcommand\lean*[2]{%
     \leanref*{#1}{##1}{##2}}
+
+  \newcommand\code[2]{%
+    \coderef{#1}{##1}{##2}}
+  \WithSuffix\newcommand\code*[2]{%
+    \coderef*{#1}{##1}{##2}}
+
   \newcommand\leanp[3]{%
     \leanpref{#1}{##1}{##2}{##3}}
   \WithSuffix\newcommand\leanp*[3]{%
     \leanpref*{#1}{##1}{##2}{##3}}
+
+  \newcommand\codep[3]{%
+    \codepref{#1}{##1}{##2}{##3}}
+  \WithSuffix\newcommand\codep*[3]{%
+    \codepref*{#1}{##1}{##2}{##3}}
 }
 
 % ========================================