Enderton (set). Continue refining ordering theorems/exercises.

Bookshelf/Enderton/Set.tex

@@ -6863,6 +6863,8 @@
   \code{Bookshelf/Enderton/Set/Chapter\_4}
     {Enderton.Set.Chapter\_4.zero\_least\_nat}
 
+  \lean{Std/Data/Nat/Init/Lemmas}{Nat.pos\_of\_ne\_zero}
+
   \begin{proof}
 
     Let $$S = \{n \in \omega \mid n = 0 \lor 0 \in n\}.$$
@@ -7255,7 +7257,7 @@
 
   \end{proof}
 
-\subsection{\pending{%
+\subsection{\verified{%
   Well Ordering of \texorpdfstring{$\omega$}{Natural Numbers}}}%
 \hyperlabel{sub:well-ordering-natural-numbers}
 
@@ -7264,6 +7266,9 @@
     Then there is some $m \in A$ such that $m \ineq n$ for all $n \in A$.
   \end{theorem}
 
+  \code{Bookshelf/Enderton/Set/Chapter\_4}
+    {Enderton.Set.Chapter\_4.well\_ordering\_nat}
+
   \lean{Mathlib/SetTheory/Ordinal/Basic}{WellOrder}
 
   \begin{note}
@@ -7295,16 +7300,13 @@
     \hyperlabel{par:well-ordering-natural-numbers-ii}
 
       Suppose $n \in S$.
-      That is, for all $m \in n$, $m \in \omega - A$.
+      We want to prove that $$\forall m, m \in n^+ \Rightarrow m \not\in A.$$
-      Let $p$ be an arbitrary element of $A$.
+      To this end, let $m \in \omega$ such that $m \in n^+$.
-      By the \nameref{sub:trichotomy-law-natural-numbers}, only one of the
+      By definition of the \nameref{ref:successor}, $m \in n$ or $m = n$.
-        following holds:
+      If the former, $n \in S$ implies $m \not\in A$.
-        $$p \in n^+, \quad p = n^+, \quad n^+ \in p.$$
+      If the latter, it isn't possible for $n \in A$ since the
-      It cannot be that $p \in n^+$ since $p \in \omega - A$ by
+        \nameref{sub:trichotomy-law-natural-numbers} would otherwise imply
-        \eqref{sub:well-ordering-natural-numbers-eq1}.
+        $n$ is the least element of $A$, which is assumed to not exist.
-      But then $n^+ = p$ or $n^+ \in p$, implying that $n^+$ is a least element
-        of $A$.
-      Since $A$ does not have a least element, it must be that $n^+ \not\in A$.
       Hence $n^+ \in S$.
 
     \paragraph{Conclusion}%
@@ -7333,7 +7335,7 @@
     Therefore it isn't possible $f(n^+) \in f(n)$ for all $n \in \omega$.
   \end{proof}
 
-\subsection{\pending{%
+\subsection{\verified{%
   Strong Induction Principle for \texorpdfstring{$\omega$}{Natural Numbers}}}%
 \hyperlabel{sub:strong-induction-principle-natural-numbers}
 
@@ -7347,6 +7349,9 @@
     Then $A = \omega$.
   \end{theorem}
 
+  \code{Bookshelf/Enderton/Set/Chapter\_4}
+    {Enderton.Set.Chapter\_4.strong\_induction\_principle\_nat}
+
   \begin{proof}
     For the sake of contradiction, suppose $\omega - A$ is a nonempty set.
     By \nameref{sub:well-ordering-natural-numbers}, there exists a least element
@@ -7861,12 +7866,15 @@
     Refer to \nameref{sub:theorem-4k-5}.
   \end{proof}
 
-\subsection{\pending{Exercise 4.17}}%
+\subsection{\verified{Exercise 4.17}}%
 \hyperlabel{sub:exercise-4.17}
 
   Prove that $m^{n+p} = m^n \cdot m^p$.
 
-  \lean*{Data/Nat/Lemmas}{Nat.pow\_add}
+  \code*{Bookshelf/Enderton/Set/Chapter\_4}
+    {Enderton.Set.Chapter\_4.exercise\_4\_17}
+
+  \lean{Data/Nat/Lemmas}{Nat.pow\_add}
 
   \begin{proof}
 
@@ -7929,15 +7937,97 @@
     Therefore $$\img{\in_\omega^{-1}}{\{7, 8\}} = \{6, 7\}.$$
   \end{proof}
 
-\subsection{\sorry{Exercise 4.19}}%
+\subsection{\verified{Exercise 4.19}}%
 \hyperlabel{sub:exercise-4.19}
 
   Prove that if $m$ is a natural number and $d$ is a nonzero number, then there
-    exist numbers $q$ and $r$ such that $m = (d \cdot q) + r$ and $r$ is less than
+    exist numbers $q$ and $r$ such that $m = (d \cdot q) + r$ and $r$ is less
-    $d$.
+    than $d$.
+
+  \code*{Bookshelf/Enderton/Set/Chapter\_4}
+    {Enderton.Set.Chapter\_4.exercise\_4\_19}
 
   \begin{proof}
-    TODO
+
+    Let $d \in \omega$ such that $d \neq 0$.
+    Define
+      \begin{equation}
+        \hyperlabel{sub:exercise-4.18-eq1}
+        S = \{m \in \omega \mid
+          (\exists q, d \in \omega) m = (d \cdot q) + r \land r < d\}.
+      \end{equation}
+    We prove that $S$ is an \nameref{ref:inductive-set} by showing
+      (i) $0 \in S$ and (ii) if $m \in S$, then $m^+ \in S$.
+    Afterward we prove (iii) the theorem statement.
+
+    \paragraph{(i)}%
+    \hyperlabel{par:exercise-4.19-i}
+
+      Let $q = 0$ and $r = 0$.
+      We note $r < d$ by \textref{sub:zero-least-natural-number}.
+      Furthermore,
+        \begin{align*}
+          (d \cdot 0) + 0
+            & = d \cdot 0 & \textref{sub:theorem-4i} \\
+            & = 0. & \textref{sub:theorem-4j}
+        \end{align*}
+      Thus $0 \in S$.
+
+    \paragraph{(ii)}%
+    \hyperlabel{par:exercise-4.19-ii}
+
+      Suppose $m \in S$.
+      Then there exists $q, d \in \omega$ such that $m = (d \cdot q) + r$ and
+        $r < d$.
+      Then
+        \begin{align*}
+          m^+
+            & = ((d \cdot q) + r)^+ \\
+            & = (d \cdot q) + r^+. & \textref{sub:theorem-4i}
+        \end{align*}
+      By \nameref{sub:trichotomy-law-natural-numbers}, there are three cases to
+        consider:
+
+      \subparagraph{Case 1}%
+
+        Suppose $r^+ \in d$.
+        Then it immediately follows $m^+ \in S$.
+
+      \subparagraph{Case 2}%
+
+        Suppose $r^+ = d$.
+        Then
+          \begin{align*}
+            m^+
+              & = (d \cdot q) + r^+ \\
+              & = (d \cdot q) + d \\
+              & = d \cdot q^+ & \textref{sub:theorem-4j} \\
+              & = (d \cdot q^+) + 0. & \textref{sub:theorem-4i}
+          \end{align*}
+        Hence $m^+ \in S$.
+
+      \subparagraph{Case 3}%
+
+        Suppose $d \in r^+$.
+        Then, by definition of the \nameref{ref:successor}, $d \in r$ or
+          $d = r$.
+        But $r \in d$.
+        Thus, by \nameref{sub:trichotomy-law-natural-numbers}, a contradiction
+          is introduced.
+        Hence this case is not possible.
+
+      \subparagraph{Conclusion}%
+
+        Since the above cases are exhaustive, it follows $m^+ \in S$.
+
+    \paragraph{(iii)}%
+
+      By \nameref{par:exercise-4.19-i} and \nameref{par:exercise-4.19-ii},
+        $S \subseteq \omega$ is indeed an inductive set.
+      By \nameref{sub:theorem-4b}, $S = \omega$.
+      Thus for all $m, d \in \omega$ where $d \neq 0$, there exist numbers $q$
+        and $r$ such that $m = (d \cdot q) + r$ and $r < d$.
+
   \end{proof}
 
 \subsection{\sorry{Exercise 4.20}}%
@@ -7950,44 +8040,148 @@
     TODO
   \end{proof}
 
-\subsection{\sorry{Exercise 4.21}}%
+\subsection{\unverified{Exercise 4.21}}%
 \hyperlabel{sub:exercise-4.21}
 
   Show that no natural number is a subset of any of its elements.
 
   \begin{proof}
-    TODO
+    Let $n$ be a natural number.
+    Suppose $m \in n$.
+    By \nameref{sub:trichotomy-law-natural-numbers}, $n \neq m$ and
+      $n \not\in m$.
+    By \nameref{sub:corollary-4m}, $n \not\subseteq m$.
   \end{proof}
 
-\subsection{\sorry{Exercise 4.22}}%
+\subsection{\verified{Exercise 4.22}}%
 \hyperlabel{sub:exercise-4.22}
 
   Show that for any natural numbers $m$ and $p$ we have $m \in m + p^+$.
 
+  \code*{Bookshelf/Enderton/Set/Chapter\_4}
+    {Enderton.Set.Chapter\_4.exercise\_4\_22}
+
   \begin{proof}
-    TODO
+
+    Let $m$ be a natural number and $$S = \{p \in \omega \mid m \in m + p^+\}.$$
+    We prove that (i) $0 \in S$ and (ii) if $p \in S$, then $p^+ \in S$.
+    Afterward we prove (iii) the theorem statement.
+
+    \paragraph{(i)}%
+    \hyperlabel{par:exercise-4.22-i}
+
+      By definition of the \nameref{ref:successor}, $m^+ = m \cup \{m\}$.
+      Thus $m \in m^+ = m + 1$ (by \nameref{sub:successor-identity}).
+      Hence $0 \in S$.
+
+    \paragraph{(ii)}%
+    \hyperlabel{par:exercise-4.22-ii}
+
+      Suppose $p \in S$.
+      That is, $m \in m + p^+$.
+      By definition of the \nameref{ref:successor},
+        \begin{align*}
+          m + p^+
+            & \in (m + p^+) \cup \{m + p^+\} \\
+            & = (m + p^+)^+ \\
+            & = m + p^{++}. & \textref{sub:theorem-4i}.
+        \end{align*}
+      By \nameref{sub:theorem-4f}, $m + p^{++}$ is a
+        \nameref{ref:transitive-set}.
+      Therefore $m \in m + p^+ \in m + p^{++}$ implies $m \in m + p^{++}$.
+      Hence $p^+ \in S$.
+
+    \paragraph{(iii)}%
+
+      By \nameref{par:exercise-4.22-i} and \nameref{par:exercise-4.22-ii},
+        $S \subseteq \omega$ is an inductive set.
+      Thus \nameref{sub:theorem-4b} implies $S = \omega$.
+      Hence for any natural numbers $m$ and $p$, we have $m \in m + p^+$.
+
   \end{proof}
 
-\subsection{\sorry{Exercise 4.23}}%
+\subsection{\verified{Exercise 4.23}}%
 \hyperlabel{sub:exercise-4.23}
 
   Assume that $m$ and $n$ are natural numbers with $m$ less than $n$.
   Show that there is some $p$ in $\omega$ for which $m + p^+ = n$.
-  (It follows form this and the preceding exercise that $m$ is less than $n$ iff
+  (It follows from this and the preceding exercise that $m$ is less than $n$ iff
     $(\exists p \in \omega)m + p^+ = n$.)
 
+  \code*{Bookshelf/Enderton/Set/Chapter\_4}
+    {Enderton.Set.Chapter\_4.exercise\_4\_23}
+
   \begin{proof}
-    TODO
+
+    Let $$S = \{n \in \omega \mid
+      (\forall m \in n, \exists p \in \omega) m + p^+ = n\}.$$
+    We prove that (i) $0 \in S$ and (ii) if $p \in S$, then $p^+ \in S$.
+    Afterward we prove (iii) the theorem statement.
+
+    \paragraph{(i)}%
+    \hyperlabel{par:exercise-4.23-i}
+
+      It vacuously holds that $0 \in S$.
+
+    \paragraph{(ii)}%
+    \hyperlabel{par:exercise-4.23-ii}
+
+      Suppose $n \in S$.
+      Let $m \in n^+$.
+      By definition of the \nameref{ref:successor}, $m \in n$ or $m = n$.
+      If $m \in n$, then there exists some $p \in \omega$ such that
+        $m + p^+ = n$.
+      But then \nameref{sub:theorem-4i} implies
+        \begin{align*}
+          n^+
+            & = (m + p^+)^+ \\
+            & = m + p^{++}.
+        \end{align*}
+      If instead $m = n$, then \nameref{sub:successor-identity} implies that
+        $$n^+ = m^+ = m + 1 = m + 0^+.$$
+      Hence $n^+ \in S$.
+
+    \paragraph{(iii)}%
+
+      By \nameref{par:exercise-4.23-i} and \nameref{par:exercise-4.23-ii}, $S$
+        is an \nameref{ref:inductive-set}.
+      By \nameref{sub:theorem-4b}, $S = \omega$.
+      Thus for all $m, n \in \omega$ such that $m \in n$, there exists some
+        $p \in \omega$ such that $m + p^+ = n$.
+
   \end{proof}
 
-\subsection{\sorry{Exercise 4.24}}%
+\subsection{\verified{Exercise 4.24}}%
 \hyperlabel{sub:exercise-4.24}
 
   Assume that $m + n = p + q$.
-  Show that $$m \in p \iff n \in q.$$
+  Show that $$m \in p \iff q \in n.$$
+
+  \code*{Bookshelf/Enderton/Set/Chapter\_4}
+    {Enderton.Set.Chapter\_4.exercise\_4\_24}
 
   \begin{proof}
-    TODO
+
+    Let $m, n, p, q \in \omega$ such that $m + n = p + q$.
+
+    \paragraph{($\Rightarrow$)}%
+
+      Suppose $m \in p$.
+      By \nameref{sub:theorem-4n}, $m + n \in p + n$.
+      By hypothesis, $m + n = p + q$ meaning $p + q \in p + n$.
+      By \nameref{sub:theorem-4k-2}, $q + p \in n + p$.
+      Therefore another application of \nameref{sub:theorem-4n} implies
+        $q \in n$.
+
+    \paragraph{($\Leftarrow$)}%
+
+      Suppose $q \in n$.
+      By \nameref{sub:theorem-4n}, $q + p \in n + p$.
+      By \nameref{sub:theorem-4k-2}, $p + q \in p + n$.
+      By hypothesis, $p + q = m + n$ meaning $m + n \in p + n$.
+      Therefore another application of \nameref{sub:theorem-4n} implies
+        $m \in p$.
+
   \end{proof}
 
 \subsection{\sorry{Exercise 4.25}}%

Bookshelf/Enderton/Set/Chapter_4.lean

@@ -1,5 +1,7 @@
 import Common.Logic.Basic
+import Common.Set.Basic
 import Mathlib.Data.Set.Basic
+import Mathlib.SetTheory.Ordinal.Basic
 
 /-! # Enderton.Set.Chapter_4
 
@@ -280,6 +282,8 @@ theorem zero_least_nat (n : ℕ)
     rw [hm]
     exact Nat.succ_pos m
 
+#check Nat.pos_of_ne_zero
+
 /-! #### Theorem 4N
 
 For any natural numbers `n`, `m`, and `p`,
@@ -386,7 +390,52 @@ Let `A` be a nonempty subset of `ω`. Then there is some `m ∈ A` such that
 -/
 theorem well_ordering_nat (A : Set ℕ) (hA : Set.Nonempty A)
   : ∃ m ∈ A, ∀ n, n ∈ A → m ≤ n := by
-  sorry
+  -- Assume `A` does not have a least element.
+  by_contra nh
+  simp only [not_exists, not_and, not_forall, not_le, exists_prop] at nh
+
+  -- If we show the complement of `A` is `ω`, then `A = ∅`, a contradiction.
+  suffices A.compl = Set.univ by
+    have h := Set.univ_diff_compl_eq_self A
+    rw [this] at h
+    simp only [sdiff_self, Set.bot_eq_empty] at h
+    exact absurd h.symm (Set.Nonempty.ne_empty hA)
+  
+  -- Use strong induction to prove every element of `ω` is in the complement.
+  have : ∀ n : ℕ, (∀ m, m < n → m ∈ A.compl) := by
+    intro n
+    induction n with
+    | zero =>
+      intro m hm
+      exact False.elim (Nat.not_lt_zero m hm)
+    | succ n ih =>
+      intro m hm
+      have hm' : m < n ∨ m = n := by
+        rw [Nat.lt_succ] at hm
+        exact Nat.lt_or_eq_of_le hm
+      apply Or.elim hm'
+      · intro h
+        exact ih m h
+      · intro h
+        have : ∀ x : ℕ, x ∈ A → n ≤ x := by
+          intro x hx
+          exact match @trichotomous ℕ LT.lt _ n x with
+          | Or.inl         h₁  => Nat.le_of_lt h₁
+          | Or.inr (Or.inl h₁) => Nat.le_of_eq h₁
+          | Or.inr (Or.inr h₁) => False.elim (ih x h₁ hx)
+        by_cases hn : n ∈ A
+        · have ⟨p, hp⟩ := nh n hn
+          exact absurd hp.left (ih p hp.right)
+        · rw [h]
+          exact hn
+
+  ext x
+  simp only [Set.mem_univ, iff_true]
+  by_contra nh'
+  have ⟨y, hy₁, hy₂⟩ := nh x (show x ∈ A from Set.not_not_mem.mp nh')
+  exact absurd hy₁ (this x y hy₂)
+
+#check WellOrder
 
 /-- #### Strong Induction Principle for ω
 
@@ -394,9 +443,23 @@ Let `A` be a subset of `ω`, and assume that for every `n ∈ ω`, if every numb
 less than `n` is in `A`, then `n ∈ A`. Then `A = ω`.
 -/
 theorem strong_induction_principle_nat (A : Set ℕ)
-  (h : ∀ n : ℕ, (∀ m : ℕ, m < n → m ∈ A) → n ∈ A)
+  (h : ∀ n : ℕ, (∀ x : ℕ, x < n → x ∈ A) → n ∈ A)
   : A = Set.univ := by
-  sorry
+  suffices A.compl = ∅ by
+    have h' := Set.univ_diff_compl_eq_self A
+    rw [this] at h'
+    simp only [Set.diff_empty] at h'
+    exact h'.symm
+
+  by_contra nh
+  have ⟨m, hm⟩ := well_ordering_nat A.compl (Set.nmem_singleton_empty.mp nh)
+  refine absurd (h m ?_) hm.left
+  
+  -- Show that every number less than `m` is in `A`.
+  intro x hx
+  by_contra nx
+  have : x < x := Nat.lt_of_lt_of_le hx (hm.right x nx)
+  simp at this
 
 /-- #### Exercise 4.1
 
@@ -485,4 +548,126 @@ theorem exercise_4_14 (n : ℕ)
       have : even n := ⟨q, hq'⟩
       exact absurd this h
 
+/-- #### Exercise 4.17
+
+Prove that `mⁿ⁺ᵖ = mⁿ ⬝ mᵖ.`
+-/
+theorem exercise_4_17 (m n p : ℕ)
+  : m ^ (n + p) = m ^ n * m ^ p := by
+  induction p with
+  | zero => calc m ^ (n + 0)
+    _ = m ^ n := rfl
+    _ = m ^ n * 1 := by rw [right_mul_id]
+    _ = m ^ n * m ^ 0 := rfl
+  | succ p ih => calc m ^ (n + p.succ)
+    _ = m ^ (n + p).succ := rfl
+    _ = m ^ (n + p) * m := rfl
+    _ = m ^ n * m ^ p * m := by rw [ih]
+    _ = m ^ n * (m ^ p * m) := by rw [theorem_4k_4]
+    _ = m ^ n * m ^ p.succ := rfl
+
+/-- #### Exercise 4.19
+
+Prove that if `m` is a natural number and `d` is a nonzero number, then there
+exist numbers `q` and `r` such that `m = (d ⬝ q) + r` and `r` is less than `d`.
+-/
+theorem exercise_4_19 (m d : ℕ) (hd : d ≠ 0)
+  : ∃ q r : ℕ, m = (d * q) + r ∧ r < d := by
+  induction m with
+  | zero =>
+    refine ⟨0, 0, ?_⟩
+    simp only [Nat.zero_eq, mul_zero, add_zero, true_and]
+    exact Nat.pos_of_ne_zero hd
+  | succ m ih =>
+    have ⟨q, r, hm, hr⟩ := ih
+    have hm' := calc m.succ
+      _ = ((d * q) + r).succ := by rw [hm]
+      _ = (d * q) + r.succ := rfl
+    match @trichotomous ℕ LT.lt _ r.succ d with
+    | Or.inl h₁ =>
+      exact ⟨q, r.succ, hm', h₁⟩
+    | Or.inr (Or.inl h₁) =>
+      refine ⟨q.succ, 0, ?_, Nat.pos_of_ne_zero hd⟩
+      calc Nat.succ m
+      _ = d * q + Nat.succ r := hm'
+      _ = d * q + d := by rw [h₁]
+      _ = d * q.succ := rfl
+      _ = d * q.succ + 0 := rfl
+    | Or.inr (Or.inr h₁) =>
+      have : d < d := calc d
+        _ ≤ r := Nat.lt_succ.mp h₁
+        _ < d := hr
+      simp at this
+
+/-- #### Exercise 4.22
+
+Show that for any natural numbers `m` and `p` we have `m ∈ m + p⁺`.
+-/
+theorem exercise_4_22 (m p : ℕ)
+  : m < m + p.succ := by
+  induction p with
+  | zero => simp
+  | succ p ih => calc m
+    _ < m + p.succ := ih
+    _ < m + p.succ.succ := Nat.lt.base (m + p.succ)
+
+/-- #### Exercise 4.23
+
+Assume that `m` and `n` are natural numbers with `m` less than `n`. Show that
+there is some `p` in `ω` for which `m + p⁺ = n`. (It follows from this and the
+preceding exercise that `m` is less than `n` iff (`∃p ∈ ω) m + p⁺ = n`.)
+-/
+theorem exercise_4_23 (m n : ℕ) (hm : m < n)
+  : ∃ p : ℕ, m + p.succ = n := by
+  induction n with
+  | zero => simp at hm
+  | succ n ih =>
+    have : m < n ∨ m = n := by
+      rw [Nat.lt_succ] at hm
+      exact Nat.lt_or_eq_of_le hm
+    apply Or.elim this
+    · intro hm₁
+      have ⟨p, hp⟩ := ih hm₁
+      refine ⟨p.succ, ?_⟩
+      exact Eq.symm $ calc n.succ
+        _ = (m + p.succ).succ := by rw [← hp]
+        _ = m + p.succ.succ := rfl
+    · intro hm₁
+      refine ⟨0, ?_⟩
+      rw [hm₁]
+
+/-- #### Exercise 4.24
+
+Assume that `m + n = p + q`. Show that
+```
+m ∈ p ↔ q ∈ n.
+```
+-/
+theorem exercise_4_24 (m n p q : ℕ) (h : m + n = p + q)
+  : m < p ↔ q < n := by
+  apply Iff.intro
+  · intro hm
+    have hr : m + n < p + n := (theorem_4n_i m p n).mp hm
+    rw [h] at hr
+    conv at hr => left; rw [add_comm]
+    conv at hr => right; rw [add_comm]
+    exact (theorem_4n_i q n p).mpr hr
+  · intro hq
+    have hr : q + p < n + p := (theorem_4n_i q n p).mp hq
+    conv at hr => left; rw [add_comm]
+    conv at hr => right; rw [add_comm]
+    rw [← h] at hr
+    exact (theorem_4n_i m p n).mpr hr
+
+/-- #### Exercise 4.25
+
+Assume that `n ∈ m` and `q ∈ p`. Show that
+```
+(m ⬝ q) + (n ⬝ p) ∈ (m ⬝ p) + (n ⬝ q).
+```
+-/
+theorem exercise_4_25 (m n p q : ℕ) (h₁ : n < m) (h₂ : q < p)
+  : (m * q) + (n * p) < (m * p) + (n * q) := by
+  sorry
+
 end Enderton.Set.Chapter_4

Common/Set/Basic.lean

@@ -154,6 +154,24 @@ theorem prod_nonempty_nonempty_imp_nonempty_prod {A : Set α} {B : Set β}
     rw [← nonempty_iff_ne_empty, ← nonempty_iff_ne_empty]
     exact ⟨⟨a, ha⟩, ⟨b, hb⟩⟩
 
+/-! ## Difference -/
+
+/--
+For any set `A`, the difference between the sample space and `A` is the
+complement of `A`.
+-/
+theorem univ_diff_self_eq_compl (A : Set α) : Set.univ \ A = A.compl := by
+  unfold Set.compl SDiff.sdiff instSDiffSet Set.diff
+  simp only [mem_univ, true_and]
+
+/--
+For any set `A`, the difference between the sample space and the complement of
+`A` is `A`.
+-/
+theorem univ_diff_compl_eq_self (A : Set α) : Set.univ \ A.compl = A := by
+  unfold Set.compl SDiff.sdiff instSDiffSet Set.diff
+  simp only [mem_univ, mem_setOf_eq, not_not, true_and, setOf_mem_eq]
+
 /-! ## Symmetric Difference -/
 
 /--