Enderton (logic). Begin writing out Lean proofs for Exercises 1.

Bookshelf/Enderton/Logic.lean

@@ -1,3 +1 @@
-import Bookshelf.Enderton.Logic.Chapter_0
+import Bookshelf.Enderton.Logic.Chapter_1
-
-#check Iff

Bookshelf/Enderton/Logic.tex

@@ -62,13 +62,20 @@
         & = (\alpha \Leftrightarrow \beta)
     \end{align*}
 
-  \lean{Init/Prelude}{Not}
+  \code*{Bookshelf/Enderton/Logic/Chapter\_1}
+    {Enderton.Logic.Chapter\_1.WFF}
 
-  \lean{Init/Prelude}{And}
+  \lean{Init/Prelude}
+    {Not}
 
-  \lean{Init/Prelude}{Or}
+  \lean{Init/Prelude}
+    {And}
 
-  \lean{Init/Core}{Iff}
+  \lean{Init/Prelude}
+    {Or}
+
+  \lean{Init/Core}
+    {Iff}
 
 \section{\defined{\texorpdfstring{$n$}{n}-tuple}}%
 \hyperlabel{ref:n-tuple}
@@ -78,7 +85,8 @@
     for $n > 1$.
   We also define $\tuple{x} = x$.
 
-  \lean*{Init/Prelude}{Prod}
+  \lean*{Init/Prelude}
+    {Prod}
 
 \section{\defined{Well-Formed Formula}}%
 \hyperlabel{ref:well-formed-formula}
@@ -87,6 +95,9 @@
     be built up from the sentence symbols by applying some finite number of
     times the \nameref{ref:formula-building-operations}.
 
+  \code*{Bookshelf/Enderton/Logic/Chapter\_1}
+    {Enderton.Logic.Chapter\_1.WFF}
+
 \endgroup
 
 % Reset counter to mirror Enderton's book.
@@ -285,12 +296,18 @@
 
   \end{answer}
 
-\subsection{\unverified{Exercise 1.1.2}}%
+\subsection{\pending{Exercise 1.1.2}}%
 \hyperlabel{sub:exercise-1.1.2}
 
   Show that there are no wffs of length 2, 3, or 6, but that any other positive
     length is possible.
 
+  \code*{Enderton.Logic.Chapter\_1}
+    {Enderton.Logic.Chapter\_1.exercise\_1\_1\_2\_i}
+
+  \code{Enderton.Logic.Chapter\_1}
+    {Enderton.Logic.Chapter\_1.exercise\_1\_1\_2\_ii}
+
   \begin{proof}
 
     Define $$S = \{ \phi \mid
@@ -351,7 +368,7 @@
 
   \end{proof}
 
-\subsection{\sorry{Exercise 1.1.3}}%
+\subsection{\pending{Exercise 1.1.3}}%
 \hyperlabel{sub:exercise-1.1.3}
 
   Let $\alpha$ be a wff; let $c$ be the number of places at which binary
@@ -363,10 +380,64 @@
   Show by using the induction principle that $s = c + 1$.
 
   \begin{proof}
-    TODO
+
+    Define
+      \begin{equation}
+        \hyperlabel{sub:exercise-1.1.3-eq1}
+        S = \{\phi \mid \phi \text{ is a wff such that } s = c + 1\}.
+      \end{equation}
+    We prove that (i) all the sentence symbols are members of $S$ and (ii)
+      $S$ is closed under the five \nameref{ref:formula-building-operations}.
+    We then conclude with (iii) the proof of the theorem statement.
+
+    \paragraph{(i)}%
+    \hyperlabel{par:exercise-1.1.3-i}
+
+      Let $\phi = A_n$ be an arbitrary sentence symbol.
+      The number of places at which sentence symbols occur in $\phi$ is 1.
+      The number of places at which binary connective symbols occur in $\phi$ is
+        0.
+      Hence $\phi \in S$.
+
+    \paragraph{(ii)}%
+    \hyperlabel{par:exercise-1.1.3-ii}
+
+      Let $\alpha, \beta \in S$.
+      Denote the number of places at which sentence symbols occur in each as
+        $s_\alpha$ and $s_\beta$ respectively.
+      Likewise, denote the number of places at which binary connective symbols
+        occur as $c_\alpha$ and $c_\beta$.
+
+      By definition, $\mathcal{E}_{\neg}(\alpha) = (\neg\alpha)$.
+      The number of sentence and binary connective symbols in
+        $\mathcal{E}_{\neg}(\alpha)$ does not change.
+      Thus $\mathcal{E}_{\neg}(\alpha) \in S$.
+      Likewise,
+        $\mathcal{E}_{\square}(\phi, \psi) = (\phi \mathop{\square} \psi)$
+        where $\square$ is one of the binary connectives $\land$, $\lor$,
+          $\Rightarrow$, $\Leftrightarrow$.
+      Therefore $\mathcal{E}_{\square}(\phi, \psi)$ has $s_\alpha + s_\beta$
+        sentence symbols and $c_\alpha + c_\beta + 1$ binary connective symbols.
+      But \eqref{sub:exercise-1.1.3-eq1} implies
+        \begin{align*}
+          s_\alpha + s_\beta
+            & = (c_\alpha + 1) + (c_\beta + 1) \\
+            & = (c_\alpha + c_\beta + 1) + 1,
+        \end{align*}
+      meaning $\mathcal{E}_{\square}(\phi, \psi) \in S$.
+
+      Hence $S$ is closed under the five formula-building operations.
+
+    \paragraph{(iii)}%
+    \hyperlabel{par:exercise-1.1.3-iii}
+
+      By \nameref{par:exercise-1.1.3-i} and \nameref{par:exercise-1.1.3-ii}, the
+        \nameref{sub:induction-principle-1} indicates $S$ is the set of all
+        wffs.
+
   \end{proof}
 
-\subsection{\sorry{Exercise 1.1.4}}%
+\subsection{\unverified{Exercise 1.1.4}}%
 \hyperlabel{sub:exercise-1.1.4}
 
   Assume we have a construction sequence ending in $\phi$, where $\phi$ does not
@@ -376,20 +447,75 @@
   Show that the result is still a legal construction sequence.
 
   \begin{proof}
-    TODO
+
+
+    Let $S$ denote a \nameref{ref:construction-sequence}
+      $\ltuple{\epsilon_1}{\epsilon_n}$ such that $\epsilon_n = \phi$.
+    Let $S' = \ltuple{\epsilon_{i_1}}{\epsilon_{i_m}}$ denote the construction
+      sequence resulting from deleting all expressions in $S$ containing $A_4$.
+    Fix $1 \leq j \leq m$.
+    Then there exists some $1 \leq k \leq n$ such that
+      $\epsilon_{i_j} = \epsilon_k$.
+    By definition of a construction sequence, there are three cases to consider:
+
+    \paragraph{Case 1}%
+
+      Suppose $\epsilon_k$ is a sentence symbol.
+      Then $\epsilon_{i_j}$ is also sentence symbol.
+
+    \paragraph{Case 2}%
+
+      Suppose $\epsilon_k = \mathcal{E}_{\neg}(\epsilon_a)$ for some $a < k$.
+      It must be that $A_4$ is not found in $\epsilon_a$, else an immediate
+        contradiction is raised.
+      Therefore $\epsilon_a$ is a member of $S'$ that precedes $\epsilon_{i_j}$.
+      Hence $\epsilon_{i_j} = \mathcal{E}_{\neg}(\epsilon_{i_a})$ for some
+        $a < j$.
+
+    \paragraph{Case 3}%
+
+      Suppose $\epsilon_k = \mathcal{E}_{\square}(\epsilon_a, \epsilon_b)$ for
+        some $a, b < k$ where $\square$ is one of the binary connectives
+        $\land$, $\lor$, $\Rightarrow$, $\Leftrightarrow$.
+      It must be that $A_4$ is found in neither $\epsilon_a$ nor $\epsilon_b$,
+        else an immediate contradiction is raised.
+      Therefore $\epsilon_a$ and $\epsilon_b$ is a member of $S'$, both of which
+        precede $\epsilon_{i_j}$.
+      Hence
+        $\epsilon_{i_j} = \mathcal{E}_{\square}(\epsilon_{i_a}, \epsilon_{i_b})$
+        for some $a, b < j$.
+
+    \paragraph{Conclusion}%
+
+      Since the above cases are exhaustive and apply to an arbitrary member of
+        $S'$, it must be that every member of $S'$ is valid.
+      Hence $S'$ is still a legal construction sequence.
+
   \end{proof}
 
 \subsection{\sorry{Exercise 1.1.5}}%
 \hyperlabel{sub:exercise-1.1.5}
 
   Suppose that $\alpha$ is a wff not containing the negation symbol $\neg$.
-  \begin{enumerate}[(a)]
+
-    \item Show that the length of $\alpha$ (i.e., the number of symbols in the
+\subsubsection{\sorry{Exercise 1.1.5a}}%
-      string) is odd.
+\hyperlabel{ssub:exercise-1.1.5-a}
-    \item Show that more than a quarter of the symbols are sentence symbols.
+
-  \end{enumerate}
+  Show that the length of $\alpha$ (i.e., the number of symbols in the string)
+    is odd.
   \textit{Suggestion}: Apply induction to show that the length is of the form
-    $4k + 1$ and the number of sentence symbols is $k + 1$.
+    $4k + 1$.
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsubsection{\sorry{Exercise 1.1.6a}}%
+\hyperlabel{ssub:exercise-1.1.6-a}
+
+  Show that more than a quarter of the symbols are sentence symbols.
+  \textit{Suggestion}: Apply induction to show that the number of sentence
+    symbols is $k + 1$.
 
   \begin{proof}
     TODO

Bookshelf/Enderton/Logic/Chapter_0.lean

@@ -1,10 +0,0 @@
-/-! # Enderton.Logic.Chapter_0
-
-Useful Facts About Sets
--/
-
-namespace Enderton.Logic.Chapter_0
-
--- TODO
-
-end Enderton.Logic.Chapter_0

Bookshelf/Enderton/Logic/Chapter_1.lean

@@ -0,0 +1,184 @@
+import Common.Nat.Basic
+import Mathlib.Data.Nat.Basic
+import Mathlib.Tactic.NormNum
+
+/-! # Enderton.Logic.Chapter_1
+
+Sentential Logic
+-/
+
+namespace Enderton.Logic.Chapter_1
+
+/--
+An abstract representation of a well-formed formula as defined by Enderton.
+-/
+inductive Wff where
+  |   SS : Nat → Wff        -- e.g. **S**entence **S**ymbol `Aₙ`
+  |  Not : Wff → Wff        -- e.g. `(¬ α)`
+  |  And : Wff → Wff → Wff  -- e.g. `(α ∧ β)`
+  |   Or : Wff → Wff → Wff  -- e.g. `(α ∨ β)`
+  | Cond : Wff → Wff → Wff  -- e.g. `(α → β)`
+  |  Iff : Wff → Wff → Wff  -- e.g. `(α ↔ β)`
+
+namespace Wff
+
+/--
+Returns the length of the expression, including symbols.
+-/
+def length : Wff → ℕ
+  | Wff.SS   _     => 1
+  | Wff.Not  e     => length e + 3
+  | Wff.And  e₁ e₂
+  | Wff.Or   e₁ e₂
+  | Wff.Cond e₁ e₂
+  | Wff.Iff  e₁ e₂ => length e₁ + length e₂ + 3
+
+/--
+Every well-formed formula has a positive length.
+-/
+theorem length_gt_zero (φ : Wff)
+  : length φ > 0 := by
+  unfold length
+  match φ with
+  |   SS _
+  |  Not _
+  |  And _ _
+  |   Or _ _
+  | Cond _ _
+  |  Iff _ _ => simp
+
+end Wff
+
+/-! #### Exercise 1.1.2
+
+Show that there are no wffs of length `2`, `3`, or `6`, but that any other
+positive length is possible.
+-/
+
+section Exercise_1_1_2
+
+private lemma eq_3_by_cases (m n : ℕ) (h : m + n = 3)
+  : m = 0 ∧ n = 3 ∨
+    m = 1 ∧ n = 2 ∨
+    m = 2 ∧ n = 1 ∨
+    m = 3 ∧ n = 0 := by
+  have m_le_3 : m ≤ 3 := by
+    have : m = 3 - n := Eq.symm $ Nat.sub_eq_of_eq_add (Eq.symm h)
+    rw [this]
+    norm_num
+  apply Or.elim (Nat.lt_or_eq_of_le m_le_3)
+  · intro hm₁
+    apply Or.elim (Nat.lt_or_eq_of_lt hm₁)
+    · intro hm₂
+      apply Or.elim (Nat.lt_or_eq_of_lt hm₂)
+      · intro hm₃
+        refine Or.elim (Nat.lt_or_eq_of_lt hm₃) (by simp) ?_
+        intro m_eq_0
+        rw [m_eq_0, zero_add] at h
+        left
+        exact ⟨m_eq_0, h⟩
+      · intro m_eq_1
+        rw [m_eq_1, add_comm] at h
+        norm_num at h
+        right; left
+        exact ⟨m_eq_1, h⟩
+    · intro m_eq_2
+      rw [m_eq_2, add_comm] at h
+      norm_num at h
+      right; right; left
+      exact ⟨m_eq_2, h⟩
+  · intro m_eq_3
+    rw [m_eq_3, add_comm] at h
+    norm_num at h
+    right; right; right
+    exact ⟨m_eq_3, h⟩
+
+theorem exercise_1_1_2_i (φ : Wff)
+  : φ.length ≠ 2 ∧ φ.length ≠ 3 ∧ φ.length ≠ 6 := by
+  induction φ with
+  | SS c =>
+    unfold Wff.length
+    simp
+  | Not e ih =>
+    unfold Wff.length
+    refine ⟨by norm_num, ?_, ?_⟩
+    · intro h
+      norm_num at h
+      have := e.length_gt_zero
+      rw [h] at this
+      simp at this
+    · intro h
+      norm_num at h
+      rw [h] at ih
+      simp at ih
+  | And  e₁ e₂ ih₁ ih₂
+  | Or   e₁ e₂ ih₁ ih₂
+  | Cond e₁ e₂ ih₁ ih₂
+  | Iff  e₁ e₂ ih₁ ih₂ =>
+    unfold Wff.length
+    refine ⟨by norm_num, ?_, ?_⟩
+    · intro h
+      norm_num at h
+      have := e₁.length_gt_zero
+      rw [h.left] at this
+      simp at this
+    · intro h
+      norm_num at h
+      apply Or.elim (eq_3_by_cases e₁.length e₂.length h)
+      · intro h₁
+        have := e₁.length_gt_zero
+        rw [h₁.left] at this
+        simp at this
+      · intro h₁
+        apply Or.elim h₁
+        · intro h₂
+          exact absurd h₂.right ih₂.left
+        intro h₂
+        apply Or.elim h₂
+        · intro h₃
+          exact absurd h₃.left ih₁.left
+        intro h₃
+        exact absurd h₃.left ih₁.right.left
+
+theorem exercise_1_1_2_ii (n : ℕ) (h : n ≠ 2 ∧ n ≠ 3 ∧ n ≠ 6)
+  : ∃ φ : Wff, φ.length = n := by
+  let φ₁ := Wff.SS 1
+  let φ₂ := Wff.And φ₁ (Wff.SS 2)
+  let φ₃ := Wff.And φ₂ (Wff.SS 3)
+  sorry
+
+end Exercise_1_1_2
+
+/-! #### Exercise 1.1.3
+
+Let `α` be a wff; let `c` be the number of places at which binary connective
+symbols (`∧`, `∨`, `→`, `↔`) occur in `α`; let `s` be the number of places at
+which sentence symbols occur in `α`. (For example, if `α` is `(A → (¬ A))` then
+`c = 1` and `s = 2`.) Show by using the induction principle that `s = c + 1`.
+-/
+
+section Exercise_1_1_3
+
+private def binary_symbol_count : Wff → ℕ
+  | Wff.SS   _     => 0
+  | Wff.Not  e     => binary_symbol_count e
+  | Wff.And  e₁ e₂
+  | Wff.Or   e₁ e₂
+  | Wff.Cond e₁ e₂
+  | Wff.Iff  e₁ e₂ => binary_symbol_count e₁ + binary_symbol_count e₂ + 1
+
+private def sentence_symbol_count : Wff → ℕ
+  | Wff.SS   _     => 1
+  | Wff.Not  e     => sentence_symbol_count e
+  | Wff.And  e₁ e₂
+  | Wff.Or   e₁ e₂
+  | Wff.Cond e₁ e₂
+  | Wff.Iff  e₁ e₂ => sentence_symbol_count e₁ + sentence_symbol_count e₂
+
+theorem exercise_1_1_3 (φ : Wff)
+  : sentence_symbol_count φ = binary_symbol_count φ + 1 := by
+  sorry
+
+end Exercise_1_1_3
+
+end Enderton.Logic.Chapter_1

Bookshelf/Enderton/Set.tex

@@ -35,7 +35,8 @@
   \textbf{Addition} ($+$) is the \nameref{ref:binary-operation} on $\omega$ such
     that for any $m$ and $n$ in $\omega$, $$m + n = A_m(n).$$
 
-  \lean{Init/Prelude}{Add.add}
+  \lean{Init/Prelude}
+    {Add.add}
 
 \section{\defined{Axiom of Choice, First Form}}%
 \hyperlabel{ref:axiom-of-choice-1}
@@ -43,7 +44,8 @@
   For any relation $R$ there is a function $H \subseteq R$ with
     $\dom{H} = \dom{R}$.
 
-  \lean*{Init/Prelude}{Classical.choice}
+  \lean*{Init/Prelude}
+    {Classical.choice}
 
 \section{\defined{Axiom of Choice, Second Form}}%
 \hyperlabel{ref:axiom-of-choice-2}
@@ -51,7 +53,8 @@
   For any set $I$ and any function $H$ with domain $I$, if $H(i) \neq \emptyset$
     for all $i \in I$, then $$\bigtimes_{i \in I} H(i) \neq \emptyset.$$
 
-  \lean{Init/Prelude}{Classical.choice}
+  \lean{Init/Prelude}
+    {Classical.choice}
 
 \section{\defined{Binary Operation}}%
 \hyperlabel{ref:binary-operation}
@@ -79,7 +82,8 @@
     only if for all $x$ and $y$ in $A$,
     $$xRy \Rightarrow F(x)RF(y).$$
 
-  \lean{Init/Core}{Quotient.lift}
+  \lean{Init/Core}
+    {Quotient.lift}
 
 \section{\defined{Composition}}%
 \hyperlabel{ref:composition}
@@ -87,9 +91,11 @@
   The \textbf{composition} of sets $F$ and $G$ is
     $$F \circ G = \{\tuple{u, v} \mid \exists t(uGt \land tFv)\}.$$
 
-  \code{Bookshelf/Enderton/Set/Relation}{Set.Relation.comp}
+  \code{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.comp}
 
-  \lean{Mathlib/Data/Rel}{Rel.comp}
+  \lean{Mathlib/Data/Rel}
+    {Rel.comp}
 
 \section{\defined{Connected}}%
 \hyperlabel{ref:connected}
@@ -105,9 +111,11 @@
   The \textbf{domain} of set $R$, denoted $\dom{R}$, is given by
     $$x \in \dom{R} \iff \exists y \tuple{x, y} \in R.$$
 
-  \code{Bookshelf/Enderton/Set/Relation}{Set.Relation.dom}
+  \code{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.dom}
 
-  \lean{Mathlib/Data/Rel}{Rel.dom}
+  \lean{Mathlib/Data/Rel}
+    {Rel.dom}
 
 \section{\defined{Empty Set Axiom}}%
 \hyperlabel{ref:empty-set-axiom}
@@ -122,7 +130,8 @@
 A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   only if there is a one-to-one \nameref{ref:function} from $A$ onto $B$.
 
-  \lean*{Mathlib/Init/Function}{Function.Bijective}
+  \lean*{Mathlib/Init/Function}
+    {Function.Bijective}
 
 \section{\defined{Equivalence Class}}%
 \hyperlabel{ref:equivalence-class}
@@ -133,7 +142,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     (\textbf{modulo $R$}).
   If the relation $R$ is fixed by the context, we may write just $[x]$.
 
-  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.modEquiv}
+  \code*{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.modEquiv}
 
 \section{\defined{Equivalence Relation}}%
 \hyperlabel{ref:equivalence-relation}
@@ -142,7 +152,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     $R$ is a binary \nameref{ref:relation} on $A$ that is \nameref{ref:reflexive}
     on $A$, \nameref{ref:symmetric}, and \nameref{ref:transitive}.
 
-  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isEquivalence}
+  \code*{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.isEquivalence}
 
 \section{\defined{Exponentiation}}%
 \hyperlabel{ref:exponentiation}
@@ -157,7 +168,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   \textbf{Exponentiation} is the \nameref{ref:binary-operation} on $\omega$
     such that for any $m$ and $n$ in $\omega$, $$m^n = E_m(n).$$
 
-  \lean{Init/Prelude}{Pow.pow}
+  \lean{Init/Prelude}
+    {Pow.pow}
 
 \section{\defined{Extensionality Axiom}}%
 \hyperlabel{ref:extensionality-axiom}
@@ -166,7 +178,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     $$\forall A, \forall B,
         \left[\forall x, (x \in A \iff x \in B) \Rightarrow A = B\right].$$
 
-  \lean{Mathlib/Init/Set}{Set.ext}
+  \lean{Mathlib/Init/Set}
+    {Set.ext}
 
 \section{\defined{Field}}%
 \hyperlabel{ref:field}
@@ -174,7 +187,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   Given \nameref{ref:relation} $R$, the \textbf{field} of $R$, denoted $\fld{R}$,
     is given by $$\fld{R} = \dom{R} \cup \ran{R}.$$
 
-  \lean{Bookshelf/Enderton/Set/Relation}{Set.Relation.fld}
+  \lean{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.fld}
 
 \section{\defined{Finite Set}}%
 \hyperlabel{ref:finite-set}
@@ -182,7 +196,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   A set is \textbf{finite} if and only if it is \nameref{ref:equinumerous} to a
     \nameref{ref:natural-number}.
 
-  \lean{Mathlib/Data/Finset/Basic}{Finset}
+  \lean{Mathlib/Data/Finset/Basic}
+    {Finset}
 
 \section{\defined{Function}}%
 \hyperlabel{ref:function}
@@ -200,11 +215,14 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     only one $x$ such that $xFy$.
   One-to-one functions are sometimes called \textbf{injections}.
 
-  \lean*{Mathlib/Init/Function}{Function.Injective}
+  \lean*{Mathlib/Init/Function}
+    {Function.Injective}
 
-  \lean{Mathlib/Init/Function}{Function.Surjective}
+  \lean{Mathlib/Init/Function}
+    {Function.Surjective}
 
-  \lean{Mathlib/Init/Function}{Function.Bijective}
+  \lean{Mathlib/Init/Function}
+    {Function.Bijective}
 
 \section{\defined{Image}}%
 \hyperlabel{ref:image}
@@ -217,9 +235,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
         & = \{v \mid (\exists u \in A) uFv\}.
     \end{align*}
 
-  \code{Bookshelf/Enderton/Set/Relation}{Set.Relation.image}
+  \code{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.image}
 
-  \lean{Mathlib/Data/Rel}{Rel.image}
+  \lean{Mathlib/Data/Rel}
+    {Rel.image}
 
 \section{\defined{Inductive Set}}%
 \hyperlabel{ref:inductive-set}
@@ -228,9 +248,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     and it is "closed under \nameref{ref:successor}", i.e.
     $$(\forall a \in A) a^+ \in A.$$
 
-  \lean{Prelude}{Nat}
+  \lean{Prelude}
+    {Nat}
 
-  \lean{Mathlib/Init/Set}{Set.univ}
+  \lean{Mathlib/Init/Set}
+    {Set.univ}
 
   \begin{note}
     Induction is baked into Lean's type system.
@@ -252,9 +274,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     $$(\exists A)\left[
       \emptyset \in A \land (\forall a \in A) a^+ \in A\right].$$
 
-  \lean{Prelude}{Nat}
+  \lean{Prelude}
+    {Nat}
 
-  \lean{Mathlib/Init/Set}{Set.univ}
+  \lean{Mathlib/Init/Set}
+    {Set.univ}
 
 \section{\defined{Inverse}}%
 \hyperlabel{ref:inverse}
@@ -262,9 +286,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   The \textbf{inverse} of a set $F$ is the set
     $$F^{-1} = \{\tuple{u, v} \mid vFu\}.$$
 
-  \code{Bookshelf/Enderton/Set/Relation}{Set.Relation.inv}
+  \code{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.inv}
 
-  \lean{Mathlib/Data/Rel}{Rel.inv}
+  \lean{Mathlib/Data/Rel}
+    {Rel.inv}
 
 \section{\defined{Irreflexive}}%
 \hyperlabel{ref:irreflexive}
@@ -272,7 +298,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   A binary relation $R$ on set $A$ is \textbf{irreflexive} if there is no
     $x \in A$ for which $xRx$.
 
-  \lean*{Mathlib/Init/Algebra/Classes}{IsIrrefl}
+  \lean*{Mathlib/Init/Algebra/Classes}
+    {IsIrrefl}
 
 \section{\defined{Linear Ordering}}
 \hyperlabel{ref:linear-ordering}
@@ -287,7 +314,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     \item $R$ is \nameref{ref:trichotomous}.
   \end{enumerate}
 
-  \lean{Mathlib/Init/Algebra/Classes}{IsStrictTotalOrder}
+  \lean{Mathlib/Init/Algebra/Classes}
+    {IsStrictTotalOrder}
 
   \begin{note}
     This definition does not agree with how Lean defines a linear order.
@@ -320,7 +348,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   \textbf{Multiplication} ($\cdot$) is the \nameref{ref:binary-operation} on
     $\omega$ such that for any $m$ and $n$ in $\omega$, $$m \cdot n = M_m(n).$$
 
-  \lean{Init/Prelude}{Mul.mul}
+  \lean{Init/Prelude}
+    {Mul.mul}
 
 \section{\defined{Natural Number}}%
 \hyperlabel{ref:natural-number}
@@ -329,7 +358,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   The set of all natural numbers exists by virtue of \nameref{sub:theorem-4a}.
   This set is denoted as $\omega$.
 
-  \lean*{Prelude}{Nat}
+  \lean*{Prelude}
+    {Nat}
 
 \section{\defined{Ordered Pair}}%
 \hyperlabel{ref:ordered-pair}
@@ -337,9 +367,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   For any sets $u$ and $v$, the \textbf{ordered pair} $\tuple{u, v}$ is
     the set $\{\{u\}, \{u, v\}\}$.
 
-  \code*{Bookshelf/Enderton/Set/OrderedPair}{OrderedPair}
+  \code*{Bookshelf/Enderton/Set/OrderedPair}
+    {OrderedPair}
 
-  \lean{Prelude}{Prod}
+  \lean{Prelude}
+    {Prod}
 
 \section{\defined{Ordering on \texorpdfstring{$\omega$}{Natural Numbers}}}%
 \hyperlabel{ref:ordering-natural-numbers}
@@ -356,7 +388,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
         & \iff m < n \lor m = n.
     \end{align*}
 
-  \lean{Init/Prelude}{Nat.lt}
+  \lean{Init/Prelude}
+    {Nat.lt}
 
 \section{\defined{Pair Set}}%
 \hyperlabel{ref:pair-set}
@@ -364,9 +397,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   For any sets $u$ and $v$, the \textbf{pair set $\{u, v\}$} is the set whose
     only members are $u$ and $v$.
 
-  \lean*{Mathlib/Init/Set}{Set.insert}
+  \lean*{Mathlib/Init/Set}
+    {Set.insert}
 
-  \lean{Mathlib/Init/Set}{Set.singleton}
+  \lean{Mathlib/Init/Set}
+    {Set.singleton}
 
 \section{\defined{Pairing Axiom}}%
 \hyperlabel{ref:pairing-axiom}
@@ -375,9 +410,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     $$\forall u, \forall v, \exists B, \forall x,
         (x \in B \iff x = u \text{ or } x = v).$$
 
-  \lean{Mathlib/Init/Set}{Set.insert}
+  \lean{Mathlib/Init/Set}
+    {Set.insert}
 
-  \lean{Mathlib/Init/Set}{Set.singleton}
+  \lean{Mathlib/Init/Set}
+    {Set.singleton}
 
 \section{\defined{Partition}}%
 \hyperlabel{ref:partition}
@@ -389,7 +426,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
       \item each element of $A$ is in some set in $\Pi$.
     \end{enumerate}
 
-  \lean{Mathlib/Data/Setoid/Partition}{Setoid.IsPartition}
+  \code{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.Partition}
+
+  \lean{Mathlib/Data/Setoid/Partition}
+    {Setoid.IsPartition}
 
 \section{\defined{Peano System}}%
 \hyperlabel{ref:peano-system}
@@ -404,7 +445,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
       itself.
   \end{enumerate}
 
-  \code{Common/Set/Peano}{Peano.System}
+  \code{Common/Set/Peano}
+    {Peano.System}
 
 \section{\defined{Power Set}}%
 \hyperlabel{ref:power-set}
@@ -412,7 +454,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   For any set $a$, the \textbf{power set $\powerset{a}$} is the set whose
     members are exactly the subsets of $a$.
 
-  \lean*{Mathlib/Init/Set}{Set.powerset}
+  \lean*{Mathlib/Init/Set}
+    {Set.powerset}
 
 \section{\defined{Power Set Axiom}}%
 \hyperlabel{ref:power-set-axiom}
@@ -420,7 +463,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   For any set $a$, there is a set whose members are exactly the subsets of $a$:
     $$\forall a, \exists B, \forall x, (x \in B \iff x \subseteq a).$$
 
-  \lean{Mathlib/Init/Set}{Set.powerset}
+  \lean{Mathlib/Init/Set}
+    {Set.powerset}
 
 \section{\defined{Proper Subset}}%
 \hyperlabel{ref:proper-subset}
@@ -429,7 +473,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     only if it is a subset of $B$ that is unequal to $B$.
   $$A \subset B \iff A \subseteq B \land A \neq B.$$
 
-  \lean{Std/Classes/SetNotation}{HasSSubset}
+  \lean{Std/Classes/SetNotation}
+    {HasSSubset}
 
 \section{\defined{Quotient Set}}%
 \hyperlabel{ref:quotient-set}
@@ -439,7 +484,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     are the equivalence classes.
   The expression $A / R$ is read "$A$ modulo $R$.
 
-  \lean*{Init/Core}{Quotient}
+  \lean*{Init/Core}
+    {Quotient}
 
 \section{\defined{Range}}%
 \hyperlabel{ref:range}
@@ -447,9 +493,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   The \textbf{range} of set $R$, denoted $\ran{R}$, is given by
     $$x \in \ran{R} \iff \exists t \tuple{t, x} \in R.$$
 
-  \code{Bookshelf/Enderton/Set/Relation}{Set.Relation.ran}
+  \code{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.ran}
 
-  \lean{Mathlib/Data/Rel}{Rel.codom}
+  \lean{Mathlib/Data/Rel}
+    {Rel.codom}
 
 \section{\defined{Reflexive}}%
 \hyperlabel{ref:reflexive}
@@ -457,16 +505,19 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   A binary relation $R$ is \textbf{reflexive} on $A$ if and only if $xRx$ for
     all $x \in A$.
 
-  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isReflexive}
+  \code*{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.isReflexive}
 
-  \lean{Mathlib/Init/Algebra/Classes}{IsRefl}
+  \lean{Mathlib/Init/Algebra/Classes}
+    {IsRefl}
 
 \section{\defined{Relation}}%
 \hyperlabel{ref:relation}
 
   A \textbf{relation} is a set of \nameref{ref:ordered-pair}s.
 
-  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation}
+  \code*{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation}
 
   \lean{Mathlib/Data/Rel}{Rel}
 
@@ -476,14 +527,16 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   The \textbf{restriction} of a set $F$ to set $A$ is the set
     $$F \restriction A = \{\tuple{u, v} \mid uFv \land u \in A\}.$$
 
-  \code{Bookshelf/Enderton/Set/Relation}{Set.Relation.restriction}
+  \code{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.restriction}
 
 \section{\defined{Successor}}%
 \hyperlabel{ref:successor}
 
   For any set $a$, its \textbf{successor} is defined by $$a^+ = a \cup \{a\}.$$
 
-  \lean{Prelude}{Nat.succ}
+  \lean{Prelude}
+    {Nat.succ}
 
   \begin{note}
     The corresponding Lean definition refers to the `Nat.succ` constructor.
@@ -498,7 +551,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     $$\forall t_1, \cdots \forall t_k, \forall c,
         \exists B, \forall x, (x \in B \iff x \in c \land \phi).$$
 
-  \lean{Mathlib/Init/Set}{Set.Subset}
+  \lean{Mathlib/Init/Set}
+    {Set.Subset}
 
 \section{\defined{Symmetric}}%
 \hyperlabel{ref:symmetric}
@@ -506,7 +560,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   A binary relation $R$ is \textbf{symmetric} if and only if whenever $xRy$ then
     $yRx$.
 
-  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isSymmetric}
+  \code*{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.isSymmetric}
 
 \section{\defined{Symmetric Difference}}%
 \hyperlabel{ref:symmetric-difference}
@@ -514,7 +569,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   The \textbf{symmetric difference} $A + B$ of sets $A$ and $B$ is the set
     $(A - B) \cup (B - A)$.
 
-  \lean*{Mathlib/Data/Set/Basic}{symmDiff\_def}
+  \lean*{Mathlib/Data/Set/Basic}
+    {symmDiff\_def}
 
 \section{\defined{Transitive}}%
 \hyperlabel{ref:transitive}
@@ -522,9 +578,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
   A binary relation $R$ is \textbf{transitive} if and only if whenever $xRy$ and
     $yRz$, then $xRz$.
 
-  \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isTransitive}
+  \code*{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.isTransitive}
 
-  \lean{Mathlib/Init/Algebra/Classes}{IsTrans}
+  \lean{Mathlib/Init/Algebra/Classes}
+    {IsTrans}
 
 \section{\defined{Transitive Set}}%
 \hyperlabel{ref:transitive-set}
@@ -541,7 +599,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     $$xRy, \quad x = y, \quad yRx$$
     holds.
 
-  \lean*{Mathlib/Init/Algebra/Classes}{IsTrichotomous}
+  \lean*{Mathlib/Init/Algebra/Classes}
+    {IsTrichotomous}
 
 \section{\defined{Union Axiom}}%
 \hyperlabel{ref:union-axiom}
@@ -551,7 +610,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     $$\forall A, \exists B, \forall x
       \left[ x \in B \iff (\exists b \in A) x \in b \right]$$
 
-  \lean{Mathlib/Data/Set/Lattice}{Set.sUnion}
+  \lean{Mathlib/Data/Set/Lattice}
+    {Set.sUnion}
 
 \section{\defined{Union Axiom, Preliminary Form}}%
 \hyperlabel{ref:union-axiom-preliminary-form}
@@ -561,7 +621,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and
     $$\forall a, \forall b, \exists B, \forall x,
         (x \in B \iff x \in a \text{ or } x \in b).$$
 
-  \lean{Mathlib/Init/Set}{Set.union}
+  \lean{Mathlib/Init/Set}
+    {Set.union}
 
 \endgroup
 

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -1941,7 +1941,7 @@ Show that `Rₚ` is an equivalence relation on `A`. (This is a formalized versio
 of the discussion at the beginning of this section.)
 -/
 theorem exercise_3_37 {P : Set (Set α)} {A : Set α}
-  (hP : isPartition P A) (Rₚ : Set.Relation α)
+  (hP : Partition P A) (Rₚ : Set.Relation α)
   (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B)
   : isEquivalence Rₚ A := by
   have hRₚ_eq : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by
@@ -2014,7 +2014,7 @@ equivalence relation on `A`. Show that if we start with the equivalence relation
 `Rₚ` of the preceding exercise, then the partition `A / Rₚ` is just `P`.
 -/
 theorem exercise_3_38 {P : Set (Set α)} {A : Set α}
-  (hP : isPartition P A) (Rₚ : Set.Relation α)
+  (hP : Partition P A) (Rₚ : Set.Relation α)
   (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B)
   : modEquiv (exercise_3_37 hP Rₚ hRₚ) = P := by
   have hRₚ_eq : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by

Bookshelf/Enderton/Set/Relation.lean

@@ -575,7 +575,7 @@ theorem neighborhood_mem_imp_relate {R : Set.Relation α} {A : Set α}
 A **partition** `Π` of a set `A` is a set of nonempty subsets of `A` that is
 disjoint and exhaustive.
 -/
-structure isPartition (P : Set (Set α)) (A : Set α) : Prop where
+structure Partition (P : Set (Set α)) (A : Set α) : Prop where
   p_subset : ∀ p ∈ P, p ⊆ A 
   nonempty : ∀ p ∈ P, Set.Nonempty p
   disjoint : ∀ a ∈ P, ∀ b, b ∈ P → a ≠ b → a ∩ b = ∅
@@ -585,7 +585,7 @@ structure isPartition (P : Set (Set α)) (A : Set α) : Prop where
 Membership of sets within `P` is unique.
 -/
 theorem partition_mem_mem_eq {P : Set (Set α)} {A : Set α}
-  (hP : isPartition P A) (hx : x ∈ A)
+  (hP : Partition P A) (hx : x ∈ A)
   : ∃! B, B ∈ P ∧ x ∈ B := by
   have ⟨B, hB⟩ := hP.exhaustive x hx
   refine ⟨B, hB, ?_⟩
@@ -606,7 +606,7 @@ def modEquiv {A : Set α} {R : Relation α} (_ : isEquivalence R A) :=
 Show the sets formed by `modEquiv` do indeed form a `partition`.
 -/
 theorem modEquiv_partition {A : Set α} {R : Relation α} (hR : isEquivalence R A)
-  : isPartition (modEquiv hR) A := by
+  : Partition (modEquiv hR) A := by
   refine ⟨?_, ?_, ?_, ?_⟩
   · intro p hp
     have ⟨x, hx⟩ := hp

Common/Nat/Basic.lean

@@ -1,7 +1,14 @@
 import Mathlib.Data.Set.Basic
+import Mathlib.Tactic.NormNum
 
 namespace Nat
 
+/--
+If `n < m⁺`, then `n < m` or `n = m`.
+-/
+theorem lt_or_eq_of_lt {n m : Nat} (h : n < m.succ) : n < m ∨ n = m :=
+  lt_or_eq_of_le (lt_succ.mp h)
+
 /--
 The following cancellation law holds for `m`, `n`, and `p` in `ω`:
 ```

DocGen4/Output/Index.lean

@@ -44,6 +44,7 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
         <li>Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford university press, 2000.</li>
       </ul>
 
+      <h2>Legend</h2>
       <p>
         A color/symbol code is used on generated PDF headers to indicate their
         status: