Enderton (Set). Additions to exercise set 6. (#8)

Bookshelf/Enderton/Set.tex

@@ -421,6 +421,17 @@
   \lean{Init/Prelude}
     {Mul.mul}
 
+\section{\defined{Natural Map}}%
+\hyperlabel{ref:natural-map}
+
+  Let $R$ be an \nameref{ref:equivalence-relation} on $A$.
+  Then the \textbf{natural map} (or \textbf{canonical map})
+    $\phi \colon A \rightarrow A / R$ is defined as $$\phi(x) = [x]_R$$ for
+    $x \in A$.
+
+  \lean*{Init/Core}
+    {Quotient.lift}
+
 \section{\defined{Natural Number}}%
 \hyperlabel{ref:natural-number}
 
@@ -3072,6 +3083,9 @@
   \code{Bookshelf/Enderton/Set/Relation}
     {Set.Relation.one\_to\_one\_comp\_is\_one\_to\_one}
 
+  \lean{Mathlib/Data/Set/Function}
+    {Set.InjOn.comp}
+
   \begin{proof}
     Let $F \colon B \rightarrow C$ and $G \colon A \rightarrow B$ be
       one-to-one \nameref{ref:function}s from sets $A$, $B$, and $C$.
@@ -3116,35 +3130,23 @@
       \end{align*}
   \end{proof}
 
-\subsection{\verified{Theorem 3J}}%
+\subsection{\verified{Theorem 3J (a)}}%
-\hyperlabel{sub:theorem-3j}
+\hyperlabel{sub:theorem-3j-a}
 
-  \begin{theorem}[3J]
+  \begin{theorem}[3J(a)]
     Assume that $F \colon A \rightarrow B$, and that $A$ is nonempty.
-    \begin{enumerate}[(a)]
+    There exists a function $G \colon B \rightarrow A$ (a "left inverse") such
-      \item There exists a function $G \colon B \rightarrow A$
+      that $G \circ F$ is the identity function $I_A$ on $A$ iff $F$ is
-        (a "left inverse") such that $G \circ F$ is the identity function $I_A$
+      one-to-one.
-        on $A$ iff $F$ is one-to-one.
-      \item There exists a function $H \colon B \rightarrow A$
-        (a "right inverse") such that $F \circ H$ is the identity function $I_B$
-        on $B$ iff $F$ maps $A$ \textit{onto} $B$.
-    \end{enumerate}
   \end{theorem}
 
   \code{Bookshelf/Enderton/Set/Chapter\_3}
     {Enderton.Set.Chapter\_3.theorem\_3j\_a}
 
-  \code{Bookshelf/Enderton/Set/Chapter\_3}
-    {Enderton.Set.Chapter\_3.theorem\_3j\_b}
-
   \begin{proof}
+
     Let $F$ be a \nameref{ref:function} from nonempty set $A$ to set $B$.
 
-    \paragraph{(a)}%
-
-      We prove there exists a function $G \colon B \rightarrow A$ such that
-        $G \circ F = I_A$ if and only if $F$ is one-to-one.
-
     \subparagraph{($\Rightarrow$)}%
 
       Let $G \colon B \rightarrow A$ such that $G \circ F = I_A$.
@@ -3172,10 +3174,24 @@
       Thus $(G \circ F)(x) = G(F(x)) = F^{-1}(F(x)) = x$ by
         \nameref{sub:theorem-3g}.
 
-    \paragraph{(b)}%
+  \end{proof}
 
-      We prove there exists a function $H \colon B \rightarrow A$ such that
+\subsection{\unverified{Theorem 3J (b)}}%
-        $F \circ H = I_A$ if and only if $F$ maps $A$ onto $B$.
+\hyperlabel{sub:theorem-3j-b}
+
+  \begin{theorem}[3J(b)]
+    Assume that $F \colon A \rightarrow B$, and that $A$ is nonempty.
+    There exists a function $H \colon B \rightarrow A$ (a "right inverse") such
+      that $F \circ H$ is the identity function $I_B$ on $B$ iff $F$ maps $A$
+      \textit{onto} $B$.
+  \end{theorem}
+
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3j\_b}
+
+  \begin{proof}
+
+    Let $F$ be a \nameref{ref:function} from nonempty set $A$ to set $B$.
 
     \subparagraph{($\Rightarrow$)}%
 
@@ -3215,9 +3231,9 @@
   \begin{proof}
     By definition, a one-to-one correspondence $f$ between sets $A$ and $B$ must
       be both one-to-one and onto.
-    By \nameref{sub:theorem-3j}, $f$ is one-to-one if and only if it has a left
+    By \nameref{sub:theorem-3j-a}, $f$ is one-to-one if and only if it has a
-      inverse.
+      left inverse.
-    The same theorem states that $f$ is onto $B$ if and only if it has a right
+    By \nameref{sub:theorem-3j-b}, $f$ is onto $B$ if and only if it has a right
       inverse.
   \end{proof}
 
@@ -9099,7 +9115,7 @@
 \hyperlabel{sub:lemma-6f}
 
   \begin{lemma}[6F]
-    If $C$ is a proper subset of a natural number $n$, then $C \approx m$ for
+    If $C$ is a proper subset of a natural number $n$, then $C \equin m$ for
       some $m$ less than $n$.
   \end{lemma}
 
@@ -9199,6 +9215,214 @@
     Hence $S'$ is a finite set.
   \end{proof}
 
+\subsection{\verified{Subset Size}}%
+\hyperlabel{sub:subset-size}
+
+  \begin{lemma}
+    Let $A$ be a finite set and $B \subseteq A$.
+    Then there exist natural numbers $m, n \in \omega$ such that
+      $B \equin m$, $A \equin n$, and $m \leq n$.
+  \end{lemma}
+
+  \code{Bookshelf/Enderton/Set/Chapter\_6}
+    {Enderton.Set.Chapter\_6.subset\_size}
+
+  \begin{proof}
+
+    Let $A$ be a \nameref{ref:finite-set} and $B$ be a subset of $A$.
+    By \nameref{sub:corollary-6g}, $B$ must be finite.
+    By definition of a finite set, there exists natural numbers
+      $m, n \in \omega$ such that $B \equin m$ and $A \equin n$.
+    By \nameref{sub:trichotomy-law-natural-numbers}, it suffices to prove that
+      $m > n$ is not possible for then either $m < n$ or $m = n$.
+
+    For the sake of contradiction, assume $m > n$.
+    By definition of \nameref{ref:equinumerous}, there exists a one-to-one
+      correspondence between $B$ and $m$.
+    \nameref{sub:theorem-6a} indicates there then exists a one-to-one
+      correspondence $f$ between $m$ and $B$.
+    Likewise, there exists a one-to-one correspondence $g$ between $A$ and
+      $n$.
+
+    Define $h \colon A \rightarrow B$ as $h(x) = f(g(x))$ for all $x \in A$.
+    Since $n \subset m$ by \nameref{sub:corollary-4m}, $h$ is well-defined.
+    By \nameref{sub:one-to-one-composition}, $h$ must be one-to-one.
+    Thus $h$ is a one-to-one correspondence between $A$ and $\ran{h}$, i.e.
+      $A \equin \ran{h}$.
+    But $n < m$ meaning $\ran{h} \subset B$ which in turn is a proper subset
+      of $A$ by hypothesis.
+    \nameref{sub:corollary-6c} states no finite set is equinumerous to a
+      proper subset of itself, a contradiction.
+
+  \end{proof}
+
+\subsection{\pending{Finite Domain and Range Size}}%
+\hyperlabel{sub:finite-domain-range-size}
+
+  \begin{lemma}
+    Let $A$ and $B$ be finite sets and $f \colon A \rightarrow B$ be a function.
+    Then there exist natural numbers $m, n \in \omega$ such that
+      $\dom{f} \equin m$, $\ran{f} \equin n$, and $m \geq n$.
+  \end{lemma}
+
+  \begin{note}
+    This proof avoids the \nameref{ref:axiom-of-choice-1} because $A$ and $B$
+      are finite.
+    In particular, we are able to choose a "smallest" element of each preimage
+      set.
+    Contrast this to \nameref{sub:theorem-3j-b}.
+  \end{note}
+
+  \begin{proof}
+    Let $A$ and $B$ be \nameref{ref:finite-set}s and $f \colon A \rightarrow B$
+      be a function.
+    By definition of finite sets, there exists \nameref{ref:natural-number}s
+      $m, p \in \omega$ such that $A \equin m$ and $B \equin p$.
+    By definition of the \nameref{ref:domain} of a function, $\dom{f} = A$.
+    Thus $\dom{f} \equin m$.
+
+    By \nameref{sub:theorem-6a}, there exists a one-to-one correspondence $g$
+      between $m$ and $\dom{f} = A$.
+    For all $y \in \ran{f}$, consider $\img{f^{-1}}{\{y\}}$.
+    Let $$A_y = \{ x \in m \mid f(g(x)) = y \}.$$
+    Since $g$ is a one-to-one correspondence, it follows that
+      $A_y \equin \img{f^{-1}}{\{y\}}$.
+    Since $A_y$ is a nonempty subset of natural numbers, the
+      \nameref{sub:well-ordering-natural-numbers} implies there exists a least
+      element, say $q_y$.
+    Define $C = \{q_y \mid y \in \ran{f}\}$.
+    Thus $h \colon C \rightarrow \ran{f}$ given by $h(x) = f(g(x))$ is a
+      one-to-one correspondence between $C$ and $\ran{f}$ by construction.
+    That is, $C \equin \ran{f}$.
+    By \nameref{sub:lemma-6f}, there exists some $n \leq m$ such that
+      $C \equin n$.
+    By \nameref{sub:theorem-6a}, $n \equin \ran{f}$.
+  \end{proof}
+
+\subsection{\pending{Set Difference Size}}%
+\hyperlabel{sub:set-difference-size}
+
+  \begin{lemma}
+    Let $A \equin m$ for some natural number $m$ and $B \subseteq A$.
+    Then there exists some $n \in \omega$ such that $B \equin n$ and
+      $A - B \equin m - n$.
+  \end{lemma}
+
+  \code{Bookshelf/Enderton/Set/Chapter\_6}
+    {Enderton.Set.Chapter\_6.sdiff\_size}
+
+  TODO: Update IH and add additional lemmas to fully prove this out.
+
+  \begin{proof}
+
+    Let
+      \begin{equation}
+        \hyperlabel{sub:set-difference-size-ih}
+        S = \{m \in \omega \mid
+          \forall A \equin m, \forall B \subseteq A, \exists n
+            \in \omega (B \equin n \land A - B \equin m - n)\}.
+      \end{equation}
+    We prove that (i) $0 \in S$ and (ii) if $n \in S$ then $n^+ \in S$.
+    Afterward we prove (iii) the lemma statement.
+
+    \paragraph{(i)}%
+    \hyperlabel{par:set-difference-size-i}
+
+      Let $A \equin 0$ and $B \subseteq A$.
+      Then it follows $A = B = \emptyset$.
+      Therefore $B \equin 0$ and $$A - B = \emptyset \equin 0 = 0 - 0$$ as
+        expected.
+
+    \paragraph{(ii)}%
+    \hyperlabel{par:set-difference-size-ii}
+
+      Suppose $m \in S$ and consider $m^+$.
+      Let $A \equin m^+$ and let $B \subseteq A$.
+      By definition of \nameref{ref:equinumerous}, there exists a one-to-one
+        correspondence $f$ between $A$ and $m^+$.
+      Since $f$ is one-to-one and onto, there exists a unique value $a \in A$
+        such that $f(a) = m$.
+      Then $B - \{a\} \subseteq A - \{a\}$ and $f$ is a one-to-one
+        correspondence between $A - \{a\}$ and $m$.
+      By \ihref{sub:set-difference-size-ih}, there exists some $n \in \omega$
+        such that $B - \{a\} \equin n$ and
+        \begin{equation}
+          \hyperlabel{par:set-difference-size-ii-eq1}
+          (A - \{a\}) - (B - \{a\}) \equin m - n.
+        \end{equation}
+      There are two cases to consider:
+
+      \subparagraph{Case 1}%
+
+        Assume $a \in B$.
+        Then $B \equin n^+$.
+        Furthermore, by definition of the set difference,
+          \begin{align}
+            (A - \{a\}) & - (B - \{a\}) \nonumber \\
+              & = \{x \mid
+                x \in A - \{a\} \land x \not\in B - \{a\}\} \nonumber \\
+              & = \{x \mid
+                (x \in A \land x \neq a) \land
+                \neg(x \in B \land x \neq a)\} \nonumber \\
+              & = \{x \mid
+                (x \in A \land x \neq a) \land
+                (x \not\in B \lor x = a)\} \nonumber \\
+              & = \{x \mid
+                (x \in A \land x \neq a \land x \not\in B) \lor
+                (x \in A \land x \neq a \land x = a)\} \nonumber \\
+              & = \{x \mid
+                (x \in A \land x \neq a \land x \not\in B) \lor F\} \nonumber \\
+              & = \{x \mid
+                (x \in A \land x \neq a \land x \not\in B)\} \nonumber \\
+              & = \{x \mid x \in A - B \land x \neq a\} \nonumber \\
+              & = \{x \mid x \in A - B \land x \not\in \{a\}\} \nonumber \\
+              & = (A - B) - \{a\}.
+                \label{par:set-difference-size-ii-eq2}
+          \end{align}
+        Since $a \in A$ and $a \in B$, $(A - B) - \{a\} = A - B$.
+        Thus
+          \begin{align*}
+            (A - \{a\} - (B - \{a\})
+              & = (A - B) - \{a\} & \eqref{par:set-difference-size-ii-eq2} \\
+              & = A - B \\
+              & \equin m - n & \eqref{par:set-difference-size-ii-eq1} \\
+              & \equin m^+ - n^+ & \textref{sub:theorem-6a}.
+          \end{align*}
+
+      \subparagraph{Case 2}%
+
+        Assume $a \not\in B$.
+        Then $B - \{a\} = B$ (i.e. $B \approx n$) and
+          \begin{align*}
+            (A - \{a\}) - (B - \{a\})
+              & = (A - \{a\}) - B \\
+              & \equin m - n & \eqref{par:set-difference-size-ii-eq1}.
+          \end{align*}
+        The above implies that there exists a one-to-one correspondence $g$
+          between $(A - \{a\}) - B$ and $m - n$.
+        Therefore $g \cup \{\tuple{a, m}\}$ is a one-to-one correspondence
+          between $A - B$ and $(m - n) \cup \{m\}$.
+        By \nameref{sub:theorem-6a},
+          $$A - B \equin (m - n) \cup \{m\} \equin m^+ - n.$$
+
+      \subparagraph{Subconclusion}%
+
+        The above two cases are exhaustive and both conclude the existence of
+          some $n \in \omega$ such that $B \equin n$ and $A - B \equin m^+ - n$.
+        Hence $m^+ \in S$.
+
+    \paragraph{(iii)}%
+
+      By \nameref{par:set-difference-size-i} and
+        \nameref{par:set-difference-size-ii}, $S \subseteq \omega$ is an
+        \nameref{ref:inductive-set}.
+      Thus \nameref{sub:theorem-4b} implies $S = \omega$.
+      Hence, for all $A \equin m$ for some $m \in \omega$, if $B \subseteq A$,
+        then there exists some $n \in \omega$ such that $B \equin n$ and
+        $A - B \equin m - n$.
+
+  \end{proof}
+
 \subsection{\sorry{Theorem 6H}}%
 \hyperlabel{sub:theorem-6h}
 
@@ -9601,8 +9825,33 @@
 
     \paragraph{($\Leftarrow$)}%
 
-      Suppose $\ran{f} = A$.
+      If $A = \emptyset$, then $f$ is trivially one-to-one.
-      TODO: by induction?
+      Assume now $A \neq \emptyset$ and $\ran{f} = A$.
+      Let $x_1, x_2 \in A$ such that $f(x_1) = f(x_2) = y$ for some $y \in A$.
+      We must prove that $x_1 = x_2$.
+
+      Let $B = \img{f^{-1}}{\{y\}}$.
+      Then $x_1, x_2 \in B$.
+      Since $B \subseteq A$, \nameref{sub:subset-size} indicates that there
+        exist natural numbers $m_1, n_1 \in \omega$ such that $B \equin m_1$,
+        $A \equin n_1$, and $m_1 \leq n_1$.
+      Define $f' \colon (A - B) \rightarrow (A - \{y\})$ as the
+        \nameref{ref:restriction} of $f$ to $A - B$.
+      Since $\ran{f} = A$, it follows $\ran{f'} = A - \{y\}$.
+      Since \nameref{sub:corollary-6g} implies $A - B$ and $A - \{y\}$ are
+        finite sets, \nameref{sub:finite-domain-range-size} implies the
+        existence of natural numbers $m_2, n_2 \in \omega$ such that
+        $\dom{f'} \equin m_2$, $\ran{f'} \equin n_2$, and $m_2 \geq n_2$.
+      Thus, by \nameref{sub:set-difference-size},
+        \begin{align*}
+          m_2 & \equin \dom{f'} \equin A - B \equin n_1 - m_1 \\
+          n_2 & \equin \ran{f'} \equin A - \{y\} \equin n_1 - 1.
+        \end{align*}
+      By \nameref{sub:corollary-6e}, $m_2 = n_1 - m_1$ and $n_2 = n_1 - 1$.
+      Since $m_2 \geq n_2$, $n_1 - m_1 \geq n_1 - 1$.
+      But $1 \leq m_1 \leq n_1$ meaning $m_1 = 1$.
+      Hence $B$ is a singleton.
+      Therefore $x_1 = x_2$, i.e. $f$ is one-to-one.
 
   \end{proof}
 

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -264,7 +264,7 @@ theorem theorem_3j_a {F : Set.HRelation α β}
 
 Assume that `F : A → B`, and that `A` is nonempty. There exists a function
 `H : B → A` (a "right inverse") such that `F ∘ H` is the identity function on
-`B` **iff** `F` maps `A` onto `B`.
+`B` only if `F` maps `A` onto `B`.
 -/
 theorem theorem_3j_b {F : Set.HRelation α β} (hF : mapsInto F A B)
   : (∃ H, mapsInto H B A ∧ comp F H = { p | p.1 ∈ B ∧ p.1 = p.2 }) →

Bookshelf/Enderton/Set/Chapter_6.lean

@@ -3,10 +3,10 @@ import Common.Logic.Basic
 import Common.Nat.Basic
 import Common.Set.Basic
 import Common.Set.Equinumerous
+import Common.Set.Function
 import Common.Set.Intervals
 import Mathlib.Data.Finset.Card
 import Mathlib.Data.Set.Finite
-import Mathlib.Tactic.LibrarySearch
 
 /-! # Enderton.Set.Chapter_6
 
@@ -83,11 +83,8 @@ lemma pigeonhole_principle_aux (n : ℕ)
     intro M hM f ⟨hf_maps, hf_inj⟩ hf_surj
 
     by_cases hM' : M = ∅
-    · unfold Set.SurjOn at hf_surj
+    · rw [hM', Set.SurjOn_emptyset_Iio_iff_eq_zero] at hf_surj
-      rw [hM'] at hf_surj
+      simp at hf_surj
-      simp only [Set.image_empty] at hf_surj
-      rw [Set.subset_def] at hf_surj
-      exact hf_surj n (show n < n + 1 by simp)
 
     by_cases h : ¬ ∃ t, t ∈ M ∧ f t = n
     -- Trivial case. `f` must not be onto if this is the case.
@@ -95,17 +92,18 @@ lemma pigeonhole_principle_aux (n : ℕ)
       exact absurd ⟨t, ht⟩ h
 
     -- Continue under the assumption `n ∈ ran f`.
-    simp only [not_not] at h
+    have ⟨t, ht₁, ht₂⟩ := not_not.mp h
-    have ⟨t, ht₁, ht₂⟩ := h
 
-    -- `M ≠ ∅` so `∃ p, ∀ x ∈ M, p ≥ x`.
+    -- `M ≠ ∅` so `∃ p, ∀ x ∈ M, p ≥ x`, i.e. a maximum member.
     have ⟨p, hp₁, hp₂⟩ : ∃ p ∈ M, ∀ x, x ∈ M → p ≥ x := by
       refine subset_finite_max_nat (show Set.Finite M from ?_) ?_ ?_
-      · have := Set.finite_lt_nat (n + 1)
+      · show Set.Finite M
+        have := Set.finite_lt_nat (n + 1)
         exact Set.Finite.subset this (subset_of_ssubset hM)
-      · exact Set.nmem_singleton_empty.mp hM'
+      · show Set.Nonempty M
-      · show ∀ t, t ∈ M → t ∈ M
+        exact Set.nmem_singleton_empty.mp hM'
-        simp only [imp_self, forall_const]
+      · show M ⊆ M
+        exact Eq.subset rfl
 
     -- `g` is a variant of `f` in which the largest element of its domain
     -- (i.e. `p`) corresponds to value `n`.
@@ -675,6 +673,349 @@ theorem corollary_6g {S S' : Set α} (hS : Set.Finite S) (hS' : S' ⊆ S)
   · intro h
     rwa [h]
 
+/-- #### Subset Size
+
+Let `A` be a finite set and `B ⊂ A`. Then there exist natural numbers `m, n ∈ ω`
+such that `B ≈ m`, `A ≈ n`, and `m ≤ n`.
+-/
+lemma subset_size [DecidableEq α] [Nonempty α] {A B : Set α}
+  (hBA : B ⊆ A) (hA : Set.Finite A)
+  : ∃ m n : ℕ, B ≈ Set.Iio m ∧ A ≈ Set.Iio n ∧ m ≤ n := by
+  have ⟨n, hn⟩ := Set.finite_iff_equinumerous_nat.mp hA
+  have ⟨m, hm⟩ := Set.finite_iff_equinumerous_nat.mp (corollary_6g hA hBA)
+  refine ⟨m, n, hm, hn, ?_⟩
+
+  suffices ¬ m > n by
+    match @trichotomous ℕ LT.lt _ m n with
+    | Or.inr (Or.inl hr) =>  -- m = n
+      rw [hr]
+    | Or.inr (Or.inr hr) =>  -- m > n
+      exact absurd hr this
+    | Or.inl hr          =>  -- m < n
+      exact Nat.le_of_lt hr
+
+  by_contra nr
+  have ⟨f, hf⟩ := Set.equinumerous_symm hm
+  have ⟨g, hg⟩ := hn
+
+  let h x := f (g x)
+  have hh : Set.BijOn h A (h '' A) := by
+    refine ⟨?_, ?_, Eq.subset rfl⟩
+    · -- `Set.MapsTo h A (ran h)`
+      intro x hx
+      simp only [Set.mem_image]
+      exact ⟨x, hx, rfl⟩
+    · -- `Set.InjOn h A`
+      refine Set.InjOn.comp hf.right.left hg.right.left ?_
+      intro x hx
+      exact Nat.lt_trans (hg.left hx) nr
+
+  have : h '' A ⊂ A := by
+    rw [Set.ssubset_def]
+    apply And.intro
+    · show ∀ x, x ∈ h '' A → x ∈ A
+      intro x hx
+      have ⟨y, hy₁, hy₂⟩ := hx
+      have h₁ : g y ∈ Set.Iio n := hg.left hy₁
+      have h₂ : f (g y) ∈ B := hf.left (Nat.lt_trans h₁ nr)
+      have h₃ : x ∈ B := by rwa [← hy₂]
+      exact hBA h₃
+    · rw [Set.subset_def]
+      simp only [Set.mem_image, not_forall, not_exists, not_and, exists_prop]
+      refine ⟨f n, hBA (hf.left nr), ?_⟩
+      intro x hx
+      by_contra nh
+      have h₁ : g x < n := hg.left hx
+      have h₂ : g x ∈ Set.Iio m := Nat.lt_trans h₁ nr
+      rw [hf.right.left h₂ nr nh] at h₁
+      simp at h₁
+  exact absurd ⟨h, hh⟩ (corollary_6c hA this)
+
+/-- #### Finite Domain and Range Size
+
+Let `A` and `B` be finite sets and `f : A → B` be a function. Then there exist
+natural numbers `m, n ∈ ω` such that `dom f ≈ m`, `ran f ≈ n`, and `m ≥ n`.
+-/
+theorem finite_dom_ran_size [Nonempty α] {A B : Set α}
+  (hA : Set.Finite A) (hB : Set.Finite B) (hf : Set.MapsTo f A B)
+  : ∃ m n : ℕ, A ≈ Set.Iio m ∧ f '' A ≈ Set.Iio n ∧ m ≥ n := by
+  have ⟨m, hm⟩ := Set.finite_iff_equinumerous_nat.mp hA
+  have ⟨p, hp⟩ := Set.finite_iff_equinumerous_nat.mp hB
+  have ⟨g, hg⟩ := Set.equinumerous_symm hm
+
+  let A_y y := { x ∈ Set.Iio m | f (g x) = y }
+  have hA₁ : ∀ y ∈ B, A_y y ≈ f ⁻¹' {y} := by
+    sorry
+  have hA₂ : ∀ y ∈ B, Set.Nonempty (A_y y) := by
+    sorry
+  have hA₃ : ∀ y ∈ B, ∃ q : ℕ, ∀ p ∈ A_y y, q ≤ p := by
+    sorry
+
+  let C := { q | ∃ y ∈ B, ∀ p ∈ A_y y, q ≤ p }
+  let h x := f (g x)
+  have hh : C ≈ f '' A := by
+    sorry
+
+  sorry
+
+/-- #### Set Difference Size
+
+Let `A ≈ m` for some natural number `m` and `B ⊆ A`. Then there exists some
+`n ∈ ω` such that `B ≈ n` and `A - B ≈ m - n`.
+-/
+lemma sdiff_size_aux [DecidableEq α] [Nonempty α]
+  : ∀ A : Set α, A ≈ Set.Iio m →
+      ∀ B, B ⊆ A →
+        ∃ n : ℕ, n ≤ m ∧ B ≈ Set.Iio n ∧ A \ B ≈ (Set.Iio m) \ (Set.Iio n) := by
+  induction m with
+  | zero =>
+    intro A hA B hB
+    refine ⟨0, ?_⟩
+    simp only [
+      Nat.zero_eq,
+      sdiff_self,
+      Set.bot_eq_empty,
+      Set.equinumerous_zero_iff_emptyset
+    ] at hA ⊢
+    have hB' : B = ∅ := Set.subset_eq_empty hB hA
+    have : A \ B = ∅ := by
+      rw [hB']
+      simp only [Set.diff_empty]
+      exact hA
+    rw [this]
+    refine ⟨trivial, hB', Set.equinumerous_emptyset_emptyset⟩
+
+  | succ m ih =>
+    intro A ⟨f, hf⟩ B hB
+
+    -- Since `f` is one-to-one and onto, there exists a unique value `a ∈ A`
+    -- such that `f(a) = m`.
+    have hfa := hf.right.right
+    unfold Set.SurjOn at hfa
+    have ⟨a, ha₁, ha₂⟩ := (Set.subset_def ▸ hfa) m (by simp)
+
+    -- `f` is a one-to-one correspondence between `A - {a}` and `m`.
+    have hBA : B \ {a} ⊆ A \ {a} := Set.diff_subset_diff_left hB
+    have hfBA : Set.BijOn f (A \ {a}) (Set.Iio m) := by
+      refine ⟨?_, ?_, ?_⟩
+      · intro x hx
+        have := hf.left hx.left
+        simp only [Set.mem_Iio, gt_iff_lt] at this ⊢
+        apply Or.elim (Nat.lt_or_eq_of_lt this)
+        · simp
+        · intro h
+          rw [← ha₂] at h
+          exact absurd (hf.right.left hx.left ha₁ h) hx.right
+      · intro x₁ hx₁ x₂ hx₂ h
+        exact hf.right.left hx₁.left hx₂.left h
+      · have := hf.right.right
+        unfold Set.SurjOn Set.image at this ⊢
+        rw [Set.subset_def] at this ⊢
+        simp only [
+          Set.mem_Iio,
+          Set.mem_diff,
+          Set.mem_singleton_iff,
+          Set.mem_setOf_eq
+        ] at this ⊢
+        intro x hx
+        have ⟨b, hb⟩ := this x (Nat.lt.step hx)
+        refine ⟨b, ⟨hb.left, ?_⟩, hb.right⟩
+        by_contra nb
+        rw [← nb, hb.right] at ha₂
+        exact absurd ha₂ (Nat.ne_of_lt hx)
+
+    -- `(A - {a}) - (B - {a}) ≈ m - n`
+    have ⟨n, hn₁, hn₂, hn₃⟩ := ih (A \ {a}) ⟨f, hfBA⟩ (B \ {a}) hBA
+    by_cases hc : a ∈ B
+
+    · refine ⟨n.succ, ?_, ?_, ?_⟩
+      · exact Nat.succ_le_succ hn₁
+      · -- `B ≈ Set.Iio n.succ`
+        have ⟨g, hg⟩ := hn₂
+        let g' x := if x = a then n else g x
+        refine ⟨g', ⟨?_, ?_, ?_⟩⟩
+        · -- `Set.MapsTo g' B (Set.Iio n.succ)`
+          intro x hx
+          dsimp only
+          by_cases hx' : x = a
+          · rw [if_pos hx']
+            simp
+          · rw [if_neg hx']
+            calc g x
+              _ < n := hg.left ⟨hx, hx'⟩
+              _ < n + 1 := by simp
+        · -- `Set.InjOn g' B`
+          intro x₁ hx₁ x₂ hx₂ h
+          dsimp only at h
+          by_cases hc₁ : x₁ = a <;> by_cases hc₂ : x₂ = a
+          · rw [hc₁, hc₂]
+          · rw [if_pos hc₁, if_neg hc₂] at h
+            exact absurd h.symm (Nat.ne_of_lt $ hg.left ⟨hx₂, hc₂⟩)
+          · rw [if_neg hc₁, if_pos hc₂] at h
+            exact absurd h (Nat.ne_of_lt $ hg.left ⟨hx₁, hc₁⟩)
+          · rw [if_neg hc₁, if_neg hc₂] at h
+            exact hg.right.left ⟨hx₁, hc₁⟩ ⟨hx₂, hc₂⟩ h
+        · -- `Set.SurjOn g' B (Set.Iio n.succ)`
+          have := hg.right.right
+          unfold Set.SurjOn Set.image at this ⊢
+          rw [Set.subset_def] at this ⊢
+          simp only [Set.mem_Iio, Set.mem_setOf_eq] at this ⊢
+          intro x hx
+          by_cases hc₁ : x = n
+          · refine ⟨a, hc, ?_⟩
+            simp only [ite_true]
+            exact hc₁.symm
+          · apply Or.elim (Nat.lt_or_eq_of_lt hx)
+            · intro hx₁
+              have ⟨b, ⟨hb₁, hb₂⟩, hb₃⟩ := this x hx₁
+              refine ⟨b, hb₁, ?_⟩
+              simp only [Set.mem_singleton_iff] at hb₂
+              rwa [if_neg hb₂]
+            · intro hx₁
+              exact absurd hx₁ hc₁
+      · have hA₁ : (A \ {a}) \ (B \ {a}) = (A \ B) \ {a} :=
+          Set.diff_mem_diff_mem_eq_diff_diff_mem
+        have hA₂ : (A \ B) \ {a} = A \ B := by
+          refine Set.not_mem_diff_eq_self ?_
+          by_contra na
+          exact absurd hc na.right
+        rw [hA₁, hA₂] at hn₃
+        suffices (Set.Iio m) \ (Set.Iio n) ≈ (Set.Iio m.succ) \ (Set.Iio n.succ)
+          from Set.equinumerous_trans hn₃ this
+        -- `m - n ≈ m⁺ - n⁺`
+        refine ⟨fun x => x + 1, ?_, ?_, ?_⟩
+        · intro x ⟨hx₁, hx₂⟩
+          simp at hx₁ hx₂ ⊢
+          exact ⟨Nat.le_add_of_sub_le hx₂, Nat.add_lt_of_lt_sub hx₁⟩
+        · intro _ _ _ _ h
+          simp only [add_left_inj] at h
+          exact h
+        · unfold Set.SurjOn Set.image
+          rw [Set.subset_def]
+          intro x ⟨hx₁, hx₂⟩
+          simp only [
+            Set.Iio_diff_Iio,
+            gt_iff_lt,
+            not_lt,
+            ge_iff_le,
+            Set.mem_setOf_eq,
+            Set.mem_Iio
+          ] at hx₁ hx₂ ⊢
+          have ⟨p, hp⟩ : ∃ p : ℕ, x = p.succ := by
+            refine Nat.exists_eq_succ_of_ne_zero ?_
+            have := calc 0
+              _ < n.succ := by simp
+              _ ≤ x := hx₂
+            exact Nat.pos_iff_ne_zero.mp this
+          refine ⟨p, ⟨?_, ?_⟩, hp.symm⟩
+          · rw [hp] at hx₂
+            exact Nat.lt_succ.mp hx₂
+          · rw [hp] at hx₁
+            exact Nat.succ_lt_succ_iff.mp hx₁
+
+    · have hB : B \ {a} = B := Set.not_mem_diff_eq_self hc
+      refine ⟨n, ?_, ?_, ?_⟩
+      · calc n
+          _ ≤ m := hn₁
+          _ ≤ m + 1 := by simp
+      · rwa [← hB]
+      · rw [hB] at hn₃
+        have ⟨g, hg⟩ := hn₃
+        have hAB : A \ B ≈ (Set.Iio m) \ (Set.Iio n) ∪ {m} := by
+          refine ⟨fun x => if x = a then m else g x, ?_, ?_, ?_⟩
+          · intro x hx
+            dsimp only
+            by_cases hc₁ : x = a
+            · rw [if_pos hc₁]
+              simp
+            · rw [if_neg hc₁]
+              have := hg.left ⟨⟨hx.left, hc₁⟩, hx.right⟩
+              simp only [
+                Set.Iio_diff_Iio,
+                gt_iff_lt,
+                not_lt,
+                ge_iff_le,
+                Set.union_singleton,
+                Set.mem_Ico,
+                lt_self_iff_false,
+                and_false,
+                Set.mem_insert_iff
+              ] at this ⊢
+              right
+              exact this
+          · intro x₁ hx₁ x₂ hx₂ h
+            dsimp only at h
+            by_cases hc₁ : x₁ = a <;> by_cases hc₂ : x₂ = a
+            · rw [hc₁, hc₂]
+            · rw [if_pos hc₁, if_neg hc₂] at h
+              have := hg.left ⟨⟨hx₂.left, hc₂⟩, hx₂.right⟩
+              simp at this
+              exact absurd h.symm (Nat.ne_of_lt this.right)
+            · rw [if_neg hc₁, if_pos hc₂] at h
+              have := hg.left ⟨⟨hx₁.left, hc₁⟩, hx₁.right⟩
+              simp at this
+              exact absurd h (Nat.ne_of_lt this.right)
+            · rw [if_neg hc₁, if_neg hc₂] at h
+              exact hg.right.left ⟨⟨hx₁.left, hc₁⟩, hx₁.right⟩ ⟨⟨hx₂.left, hc₂⟩, hx₂.right⟩ h
+          · have := hg.right.right
+            unfold Set.SurjOn Set.image at this ⊢
+            rw [Set.subset_def] at this ⊢
+            simp at this ⊢
+            refine ⟨⟨a, ⟨ha₁, hc⟩, ?_⟩, ?_⟩
+            · intro ha
+              simp at ha
+            · intro x hx₁ hx₂
+              have ⟨y, hy₁, hy₂⟩ := this x hx₁ hx₂
+              refine ⟨y, ?_, ?_⟩
+              · exact ⟨hy₁.left.left, hy₁.right⟩
+              · rwa [if_neg hy₁.left.right]
+
+        suffices (Set.Iio m) \ (Set.Iio n) ∪ {m} ≈ (Set.Iio m.succ) \ (Set.Iio n)
+          from Set.equinumerous_trans hAB this
+
+        refine ⟨fun x => x, ?_, ?_, ?_⟩
+        · intro x hx
+          simp at hx ⊢
+          apply Or.elim hx
+          · intro hx₁
+            rw [hx₁]
+            exact ⟨hn₁, by simp⟩
+          · intro ⟨hx₁, hx₂⟩
+            exact ⟨hx₁, calc x
+              _ < m := hx₂
+              _ < m + 1 := by simp⟩
+        · intro _ _ _ _ h
+          exact h
+        · unfold Set.SurjOn Set.image
+          rw [Set.subset_def]
+          simp only [
+            Set.Iio_diff_Iio,
+            gt_iff_lt,
+            not_lt,
+            ge_iff_le,
+            Set.mem_Ico,
+            Set.union_singleton,
+            lt_self_iff_false,
+            and_false,
+            Set.mem_insert_iff,
+            exists_eq_right,
+            Set.mem_setOf_eq,
+            and_imp
+          ]
+          intro x hn hm
+          apply Or.elim (Nat.lt_or_eq_of_lt hm)
+          · intro hx
+            right
+            exact ⟨hn, hx⟩
+          · intro hx
+            left
+            exact hx
+
+lemma sdiff_size [DecidableEq α] [Nonempty α] {A B : Set α}
+  (hB : B ⊆ A) (hA : A ≈ Set.Iio m)
+  : ∃ n : ℕ, n ≤ m ∧ B ≈ Set.Iio n ∧ A \ B ≈ (Set.Iio m) \ (Set.Iio n) :=
+  sdiff_size_aux A hA B hB
+
 /-- #### Exercise 6.7
 
 Assume that `A` is finite and `f : A → A`. Show that `f` is one-to-one **iff**
@@ -702,6 +1043,26 @@ theorem exercise_6_7 [DecidableEq α] [Nonempty α] {A : Set α} {f : α → α}
     rw [subset_iff_ssubset_or_eq] at hf₃
     exact Or.elim hf₃ (fun h => absurd hf₂ (corollary_6c hA₁ h)) id
   · intro hf₁
+    by_cases hA₃ : A = ∅
+    · rw [hA₃]
+      simp
+    · intro x₁ hx₁ x₂ hx₂ hf₂
+      let y := f x₁
+      let B := f ⁻¹' {y}
+      have hB₁ : x₁ ∈ B := sorry
+      have hB₂ : x₂ ∈ B := sorry
+      have hB₃ : B ⊆ A := sorry
+      have ⟨m₁, n₁, hm₁, hn₁, hmn₁⟩ := subset_size hB₃ hA₁
+      
+      have hf'₁ : Set.MapsTo f (A \ B) (A \ {y}) := sorry
+      have hf'₂ : f '' (A \ B) = A \ {y} := sorry
+      have hf'₃ : Set.Finite (A \ B) := sorry
+      have hf'₄ : Set.Finite (A \ {y}) := sorry
+
+      have ⟨m₂, n₂, hm₂, hn₂, hmn₂⟩ := finite_dom_ran_size hf'₃ hf'₄ hf'₁
+      
+      have h₁ : A \ B ≈ Set.Iio (n₁ - m₁) := sorry
+      have h₂ : A \ {y} ≈ Set.Iio (n₁ - 1) := sorry
       sorry
 
 /-- #### Exercise 6.8

Common/Set.lean

@@ -1,4 +1,5 @@
 import Common.Set.Basic
 import Common.Set.Equinumerous
+import Common.Set.Function
 import Common.Set.Intervals
 import Common.Set.Peano

Common/Set/Basic.lean

@@ -193,6 +193,62 @@ theorem diff_ssubset_nonempty {A B : Set α} (h : A ⊂ B)
   · intro hx
     exact ⟨x, hx⟩
 
+/--
+If an element `x` is not a member of a set `A`, then `A - {x} = A`. 
+-/
+theorem not_mem_diff_eq_self {A : Set α} (h : a ∉ A)
+  : A \ {a} = A := by
+  ext x
+  apply Iff.intro
+  · exact And.left
+  · intro hx
+    refine ⟨hx, ?_⟩
+    simp only [mem_singleton_iff]
+    by_contra nx
+    rw [nx] at hx
+    exact absurd hx h
+
+/--
+Given two sets `A` and `B`, `(A - {a}) - (B - {b}) = (A - B) - {a}`.
+-/
+theorem diff_mem_diff_mem_eq_diff_diff_mem {A B : Set α} {a : α}
+  : (A \ {a}) \ (B \ {a}) = (A \ B) \ {a} := by
+  calc (A \ {a}) \ (B \ {a})
+    _ = { x | x ∈ A \ {a} ∧ x ∉ B \ {a} } := rfl
+    _ = { x | x ∈ A \ {a} ∧ ¬(x ∈ B \ {a}) } := rfl
+    _ = { x | (x ∈ A ∧ x ≠ a) ∧ ¬(x ∈ B ∧ x ≠ a) } := rfl
+    _ = { x | (x ∈ A ∧ x ≠ a) ∧ (x ∉ B ∨ x = a) } := by
+      ext x
+      rw [mem_setOf_eq, not_and_de_morgan]
+      simp
+    _ = { x | (x ∈ A ∧ x ≠ a ∧ x ∉ B) ∨ (x ∈ A ∧ x ≠ a ∧ x = a) } := by
+      ext x
+      simp only [mem_setOf_eq]
+      rw [and_or_left, and_assoc, and_assoc]
+    _ = { x | x ∈ A ∧ x ≠ a ∧ x ∉ B } := by simp
+    _ = { x | x ∈ A ∧ x ∉ B ∧ x ≠ a } := by
+      ext x
+      simp only [ne_eq, sep_and, mem_inter_iff, mem_setOf_eq]
+      apply Iff.intro <;>
+      · intro ⟨⟨_, hx₂⟩, hx₃, hx₄⟩
+        exact ⟨⟨hx₃, hx₄⟩, ⟨hx₃, hx₂⟩⟩
+    _ = { x | x ∈ A ∧ x ∉ B ∧ x ∉ ({a} : Set α) } := rfl
+    _ = { x | x ∈ A \ B ∧ x ∉ ({a} : Set α) } := by
+      ext x
+      simp only [
+        mem_singleton_iff,
+        sep_and,
+        mem_inter_iff,
+        mem_setOf_eq,
+        mem_diff,
+        and_congr_right_iff,
+        and_iff_right_iff_imp,
+        and_imp
+      ]
+      intro hx _ _
+      exact hx
+    _ = (A \ B) \ {a} := rfl
+
 /--
 For any set `A`, the difference between the sample space and `A` is the
 complement of `A`.

Common/Set/Equinumerous.lean

@@ -8,6 +8,8 @@ Additional theorems around finite sets.
 
 namespace Set
 
+/-! ### Definitions -/
+
 /--
 A set `A` is equinumerous to a set `B` (written `A ≈ B`) if and only if there is
 a one-to-one function from `A` onto `B`.
@@ -19,6 +21,26 @@ infix:50 " ≈ " => Equinumerous
 theorem equinumerous_def (A : Set α) (B : Set β)
   : A ≈ B ↔ ∃ F, Set.BijOn F A B := Iff.rfl
 
+/--
+A set `A` is not equinumerous to a set `B` (written `A ≉ B`) if and only if
+there is no one-to-one function from `A` onto `B`.
+-/
+def NotEquinumerous (A : Set α) (B : Set β) : Prop := ¬ Equinumerous A B
+
+infix:50 " ≉ " => NotEquinumerous
+
+@[simp]
+theorem not_equinumerous_def : A ≉ B ↔ ∀ F, ¬ Set.BijOn F A B := by
+  apply Iff.intro
+  · intro h
+    unfold NotEquinumerous Equinumerous at h
+    simp only [not_exists] at h
+    exact h
+  · intro h
+    unfold NotEquinumerous Equinumerous
+    simp only [not_exists]
+    exact h
+
 /--
 For any set `A`, `A ≈ A`.
 -/
@@ -57,30 +79,53 @@ theorem eq_imp_equinumerous {A B : Set α} (h : A = B)
   conv at this => right; rw [h]
   exact this
 
+/-! ### Finite Sets -/
+
 /--
 A set is finite if and only if it is equinumerous to a natural number.
 -/
 axiom finite_iff_equinumerous_nat {α : Type _} {S : Set α}
   : Set.Finite S ↔ ∃ n : ℕ, S ≈ Set.Iio n
 
+/-! ### Emptyset -/
+
 /--
-A set `A` is not equinumerous to a set `B` (written `A ≉ B`) if and only if
+Any set equinumerous to the emptyset is the emptyset.
-there is no one-to-one function from `A` onto `B`.
 -/
-def NotEquinumerous (A : Set α) (B : Set β) : Prop := ¬ Equinumerous A B
-
-infix:50 " ≉ " => NotEquinumerous
-
 @[simp]
-theorem not_equinumerous_def : A ≉ B ↔ ∀ F, ¬ Set.BijOn F A B := by
+theorem equinumerous_zero_iff_emptyset {S : Set α}
+  : S ≈ Set.Iio 0 ↔ S = ∅ := by
   apply Iff.intro
+  · intro ⟨f, hf⟩
+    by_contra nh
+    rw [← Ne.def, ← Set.nonempty_iff_ne_empty] at nh
+    have ⟨x, hx⟩ := nh
+    have := hf.left hx
+    simp at this
   · intro h
-    unfold NotEquinumerous Equinumerous at h
+    rw [h]
-    simp only [not_exists] at h
+    refine ⟨fun _ => ⊥, ?_, ?_, ?_⟩
-    exact h
+    · intro _ hx
-  · intro h
+      simp at hx
-    unfold NotEquinumerous Equinumerous
+    · intro _ hx
-    simp only [not_exists]
+      simp at hx
-    exact h
+    · unfold SurjOn
+      simp only [bot_eq_zero', image_empty]
+      show ∀ x, x ∈ Set.Iio 0 → x ∈ ∅
+      intro _ hx
+      simp at hx
+
+/--
+Empty sets are always equinumerous, regardless of their underlying type.
+-/
+theorem equinumerous_emptyset_emptyset [Bot β]
+  : (∅ : Set α) ≈ (∅ : Set β) := by
+  refine ⟨fun _ => ⊥, ?_, ?_, ?_⟩
+  · intro _ hx
+    simp at hx
+  · intro _ hx
+    simp at hx
+  · unfold SurjOn
+    simp
 
 end Set

Common/Set/Function.lean

@@ -0,0 +1,235 @@
+import Mathlib.Data.Set.Function
+
+/-! # Common.Set.Function
+
+Additional theorems around functions defined on sets.
+-/
+
+namespace Set
+
+/--
+Produce a new function that swaps the outputs of the two specified inputs.
+-/
+def swap [DecidableEq α] (f : α → β) (x₁ x₂ : α) (x : α) : β :=
+  if x = x₁ then f x₂ else
+  if x = x₂ then f x₁ else
+                 f x
+
+/--
+Swapping the same input yields the original function.
+-/
+@[simp]
+theorem swap_eq_eq_self [DecidableEq α] {f : α → β} {x : α}
+  : swap f x x = f := by
+  refine funext ?_
+  intro y
+  unfold swap
+  by_cases hy : y = x
+  · rw [if_pos hy, hy]
+  · rw [if_neg hy, if_neg hy]
+
+/--
+Swapping a function twice yields the original function.
+-/
+@[simp]
+theorem swap_swap_eq_self [DecidableEq α] {f : α → β} {x₁ x₂ : α}
+  : swap (swap f x₁ x₂) x₁ x₂ = f := by
+  refine funext ?_
+  intro y
+  by_cases hc₁ : x₂ = x₁
+  · rw [hc₁]
+    simp
+  rw [← Ne.def] at hc₁
+  unfold swap
+  by_cases hc₂ : y = x₁ <;>
+  by_cases hc₃ : y = x₂
+  · rw [if_pos hc₂, if_neg hc₁, if_pos rfl, ← hc₂]
+  · rw [if_pos hc₂, if_neg hc₁, if_pos rfl, ← hc₂]
+  · rw [if_neg hc₂, if_pos hc₃, if_pos rfl, ← hc₃]
+  · rw [if_neg hc₂, if_neg hc₃, if_neg hc₂, if_neg hc₃]
+
+/--
+If `f : A → B`, then a swapped variant of `f` also maps `A` into `B`.
+-/
+theorem swap_MapsTo_self [DecidableEq α]
+  {A : Set α} {B : Set β} {f : α → β}
+  (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : MapsTo f A B)
+  : MapsTo (swap f a₁ a₂) A B := by
+  intro x hx
+  unfold swap
+  by_cases hc₁ : x = a₁ <;> by_cases hc₂ : x = a₂
+  · rw [if_pos hc₁]
+    exact hf ha₂
+  · rw [if_pos hc₁]
+    exact hf ha₂
+  · rw [if_neg hc₁, if_pos hc₂]
+    exact hf ha₁
+  · rw [if_neg hc₁, if_neg hc₂]
+    exact hf hx
+
+/--
+The converse of `swap_MapsTo_self`.
+-/
+theorem self_MapsTo_swap [DecidableEq α]
+  {A : Set α} {B : Set β} {f : α → β}
+  (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : MapsTo (swap f a₁ a₂) A B)
+  : MapsTo f A B := by
+  rw [← @swap_swap_eq_self _ _ _ f a₁ a₂]
+  exact swap_MapsTo_self ha₁ ha₂ hf
+
+/--
+If `f : A → B`, then `f` maps `A` into `B` **iff** a swap of `f` maps `A` into
+`B`.
+-/
+theorem self_iff_swap_MapsTo [DecidableEq α]
+  {A : Set α} {B : Set β} {f : α → β}
+  (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A)
+  : MapsTo (swap f a₁ a₂) A B ↔ MapsTo f A B :=
+  ⟨self_MapsTo_swap ha₁ ha₂, swap_MapsTo_self ha₁ ha₂⟩
+
+/--
+If `f : A → B` is one-to-one, then a swapped variant of `f` is also one-to-one.
+-/
+theorem swap_InjOn_self [DecidableEq α]
+  {A : Set α} {f : α → β}
+  (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : InjOn f A)
+  : InjOn (swap f a₁ a₂) A := by
+  intro x₁ hx₁ x₂ hx₂ h
+  unfold swap at h
+  by_cases hc₁ : x₁ = a₁ <;>
+  by_cases hc₂ : x₁ = a₂ <;>
+  by_cases hc₃ : x₂ = a₁ <;>
+  by_cases hc₄ : x₂ = a₂
+  · rw [hc₁, hc₃]
+  · rw [hc₁, hc₃]
+  · rw [hc₂, hc₄]
+  · rw [if_pos hc₁, if_neg hc₃, if_neg hc₄, ← hc₂] at h
+    exact hf hx₁ hx₂ h
+  · rw [hc₁, hc₃]
+  · rw [hc₁, hc₃]
+  · rw [if_pos hc₁, if_neg hc₃, if_pos hc₄, ← hc₁, ← hc₄] at h
+    exact hf hx₁ hx₂ h.symm
+  · rw [if_pos hc₁, if_neg hc₃, if_neg hc₄] at h
+    exact absurd (hf hx₂ ha₂ h.symm) hc₄
+  · rw [hc₂, hc₄]
+  · rw [if_neg hc₁, if_pos hc₂, if_pos hc₃, ← hc₂, ← hc₃] at h
+    exact hf hx₁ hx₂ h.symm
+  · rw [hc₂, hc₄]
+  · rw [if_neg hc₁, if_pos hc₂, if_neg hc₃, if_neg hc₄] at h
+    exact absurd (hf hx₂ ha₁ h.symm) hc₃
+  · rw [if_neg hc₁, if_neg hc₂, if_pos hc₃, ← hc₄] at h
+    exact hf hx₁ hx₂ h
+  · rw [if_neg hc₁, if_neg hc₂, if_pos hc₃] at h
+    exact absurd (hf hx₁ ha₂ h) hc₂
+  · rw [if_neg hc₁, if_neg hc₂, if_neg hc₃, if_pos hc₄] at h
+    exact absurd (hf hx₁ ha₁ h) hc₁
+  · rw [if_neg hc₁, if_neg hc₂, if_neg hc₃, if_neg hc₄] at h
+    exact hf hx₁ hx₂ h
+
+/--
+The converse of `swap_InjOn_self`.
+-/
+theorem self_InjOn_swap [DecidableEq α]
+  {A : Set α} {f : α → β}
+  (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : InjOn (swap f a₁ a₂) A)
+  : InjOn f A := by
+  rw [← @swap_swap_eq_self _ _ _ f a₁ a₂]
+  exact swap_InjOn_self ha₁ ha₂ hf
+
+/--
+If `f : A → B`, then `f` is one-to-one **iff** a swap of `f` is one-to-one.
+-/
+theorem self_iff_swap_InjOn [DecidableEq α]
+  {A : Set α} {f : α → β}
+  (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A)
+  : InjOn (swap f a₁ a₂) A ↔ InjOn f A :=
+  ⟨self_InjOn_swap ha₁ ha₂, swap_InjOn_self ha₁ ha₂⟩
+
+/--
+If `f : A → B` is onto, then a swapped variant of `f` is also onto.
+-/
+theorem swap_SurjOn_self [DecidableEq α]
+  {A : Set α} {B : Set β} {f : α → β}
+  (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : SurjOn f A B)
+  : SurjOn (swap f a₁ a₂) A B := by
+  show ∀ x, x ∈ B → ∃ a ∈ A, swap f a₁ a₂ a = x
+  intro x hx
+  have ⟨a, ha⟩ := hf hx
+  by_cases hc₁ : a = a₁
+  · refine ⟨a₂, ha₂, ?_⟩
+    unfold swap
+    by_cases hc₂ : a₁ = a₂
+    · rw [if_pos hc₂.symm, ← hc₂, ← hc₁]
+      exact ha.right
+    · rw [← Ne.def] at hc₂
+      rw [if_neg hc₂.symm, if_pos rfl, ← hc₁]
+      exact ha.right
+  · by_cases hc₂ : a = a₂
+    · unfold swap
+      refine ⟨a₁, ha₁, ?_⟩
+      rw [if_pos rfl, ← hc₂]
+      exact ha.right
+    · refine ⟨a, ha.left, ?_⟩
+      unfold swap
+      rw [if_neg hc₁, if_neg hc₂]
+      exact ha.right
+
+/--
+The converse of `swap_SurjOn_self`.
+-/
+theorem self_SurjOn_swap [DecidableEq α]
+  {A : Set α} {B : Set β} {f : α → β}
+  (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : SurjOn (swap f a₁ a₂) A B)
+  : SurjOn f A B := by
+  rw [← @swap_swap_eq_self _ _ _ f a₁ a₂]
+  exact swap_SurjOn_self ha₁ ha₂ hf
+
+/--
+If `f : A → B`, then `f` is onto **iff** a swap of `f` is onto.
+-/
+theorem self_iff_swap_SurjOn [DecidableEq α]
+  {A : Set α} {B : Set β} {f : α → β}
+  (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A)
+  : SurjOn (swap f a₁ a₂) A B ↔ SurjOn f A B :=
+  ⟨self_SurjOn_swap ha₁ ha₂, swap_SurjOn_self ha₁ ha₂⟩
+
+/--
+If `f : A → B` is a one-to-one correspondence, then a swapped variant of `f` is
+also a one-to-one correspondence.
+-/
+theorem swap_BijOn_self [DecidableEq α]
+  {A : Set α} {B : Set β} {f : α → β}
+  (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : BijOn f A B)
+  : BijOn (swap f a₁ a₂) A B := by
+  have ⟨hf₁, hf₂, hf₃⟩ := hf
+  exact ⟨
+    swap_MapsTo_self ha₁ ha₂ hf₁,
+    swap_InjOn_self ha₁ ha₂ hf₂,
+    swap_SurjOn_self ha₁ ha₂ hf₃
+  ⟩
+
+/--
+The converse of `swap_BijOn_self`.
+-/
+theorem self_BijOn_swap [DecidableEq α]
+  {A : Set α} {B : Set β} {f : α → β}
+  (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : BijOn (swap f a₁ a₂) A B)
+  : BijOn f A B := by
+  have ⟨hf₁, hf₂, hf₃⟩ := hf
+  exact ⟨
+    self_MapsTo_swap ha₁ ha₂ hf₁,
+    self_InjOn_swap ha₁ ha₂ hf₂,
+    self_SurjOn_swap ha₁ ha₂ hf₃
+  ⟩
+
+/--
+If `f : A → B`, `f` is a one-to-one correspondence **iff** a swap of `f` is a
+one-to-one correspondence.
+-/
+theorem self_iff_swap_BijOn [DecidableEq α]
+  {A : Set α} {B : Set β} {f : α → β}
+  (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A)
+  : BijOn (swap f a₁ a₂) A B ↔ BijOn f A B :=
+  ⟨self_BijOn_swap ha₁ ha₂, swap_BijOn_self ha₁ ha₂⟩
+
+end Set

Common/Set/Intervals.lean

@@ -1,4 +1,5 @@
 import Common.Logic.Basic
+import Mathlib.Data.Set.Function
 import Mathlib.Data.Set.Intervals.Basic
 
 namespace Set
@@ -8,6 +9,9 @@ namespace Set
 Additional theorems around intervals.
 -/
 
+/--
+If `m < n` then `{0, …, m - 1} ⊂ {0, …, n - 1}`.
+-/
 theorem Iio_nat_lt_ssubset {m n : ℕ} (h : m < n)
   : Iio m ⊂ Iio n := by
   rw [ssubset_def]
@@ -22,4 +26,22 @@ theorem Iio_nat_lt_ssubset {m n : ℕ} (h : m < n)
     simp only [not_forall, not_lt, exists_prop]
     exact ⟨m, h, by simp⟩
 
+/--
+It is never the case that the emptyset is surjective
+-/
+theorem SurjOn_emptyset_Iio_iff_eq_zero {n : ℕ} {f : α → ℕ}
+  : SurjOn f ∅ (Set.Iio n) ↔ n = 0 := by
+  apply Iff.intro
+  · intro h
+    unfold SurjOn at h
+    rw [subset_def] at h
+    simp only [mem_Iio, image_empty, mem_empty_iff_false] at h
+    by_contra nh
+    exact h 0 (Nat.pos_of_ne_zero nh)
+  · intro hn
+    unfold SurjOn
+    rw [hn, subset_def]
+    intro x hx
+    exact absurd hx (Nat.not_lt_zero x)
+
 end Set