From 3bf6f13055b07f6bd415311b7875c3838eea85a5 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Thu, 24 Aug 2023 07:50:47 -0600
Subject: [PATCH] Enderton (set). Add Lean scaffolding for finite set
 theorems/bijections.

---
 Bookshelf/Enderton/Set.tex            | 28 +++++++++++++++++++++++++--
 Bookshelf/Enderton/Set/Chapter_6.lean | 17 ++++++++++++----
 2 files changed, 39 insertions(+), 6 deletions(-)

diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex
index 29e6e2d..f458214 100644
--- a/Bookshelf/Enderton/Set.tex
+++ b/Bookshelf/Enderton/Set.tex
@@ -3171,8 +3171,8 @@
 
   \end{proof}
 
-\subsection{\unverified{Bijections are Two-Sided Inverses}}%
-\hyperlabel{sub:bijections-two-sided-inverses}
+\subsection{\unverified{Bijections and Inverses}}%
+\hyperlabel{sub:bijections-inverses}
 
   \begin{corollary}
     A function $f$ is a one-to-one correspondence if and only if it has a left
@@ -3188,6 +3188,30 @@
       inverse.
   \end{proof}
 
+\subsection{\unverified{Left and Right Inverses and Two-Sided Inverses}}%
+\hyperlabel{sub:left-right-inverse-two-sided-inverse}
+
+  \begin{lemma}
+    Let $f$ be a function with left inverse $g_1$ and right inverse $g_2$.
+    Then $g_1 = g_2 = f^{-1}$.
+  \end{lemma}
+
+  \begin{proof}
+    Let $I$ denote the identity map with appropriate domain and codomain
+      depending on placement in the following:
+      \begin{align*}
+        g_1
+          & = g_1 \circ I \\
+          & = g_1 \circ (f \circ g_2) \\
+          & = (g_1 \circ f) \circ g_2 \\
+          & = I \circ g_2 \\
+          & = g_2.
+      \end{align*}
+    By \nameref{sub:bijections-inverses}, $f$ is a bijection meaning $f^{-1}$
+      is both a left and right inverse.
+    Hence $g_1 = g_2 = f^{-1}$.
+  \end{proof}
+
 \subsection{\verified{Theorem 3K(a)}}%
 \hyperlabel{sub:theorem-3k-a}
 
diff --git a/Bookshelf/Enderton/Set/Chapter_6.lean b/Bookshelf/Enderton/Set/Chapter_6.lean
index 9e39277..da0e40e 100644
--- a/Bookshelf/Enderton/Set/Chapter_6.lean
+++ b/Bookshelf/Enderton/Set/Chapter_6.lean
@@ -67,7 +67,12 @@ No natural number is equinumerous to a proper subset of itself.
 -/
 theorem pigeonhole_principle (m n : ℕ) (hm : m < n)
   : ∀ f : Fin m → Fin n, ¬ Function.Bijective f := by
-  sorry
+  induction n with
+  | zero =>
+    intro f hf
+    simp at hm
+  | succ n ih =>
+    sorry
 
 /-- #### Corollary 6C
 
@@ -97,8 +102,8 @@ theorem corollary_6d_b
 
 Any finite set is equinumerous to a unique natural number.
 -/
-theorem corollary_6e (S : Set α) (f : S → Fin n) (hf : Function.Bijective f)
-  : S ≃ Fin m → m = n := by
+theorem corollary_6e (S : Set α) (hn : S ≃ Fin n) (hm : S ≃ Fin m)
+  : m = n := by
   sorry
 
 /-- #### Lemma 6F
@@ -106,10 +111,14 @@ theorem corollary_6e (S : Set α) (f : S → Fin n) (hf : Function.Bijective f)
 If `C` is a proper subset of a natural number `n`, then `C ≈ m` for some `m`
 less than `n`.
 -/
-lemma lemma_6f {n : ℕ} (C S : Finset ℕ) (hC : C ⊂ S) (hS : S ≃ Fin n)
+lemma lemma_6f {n : ℕ} (hC : C ⊂ Finset.range n)
   : ∃ m : ℕ, m < n ∧ ∃ f : C → Fin m, Function.Bijective f := by
   sorry
 
+theorem corollary_6g (S S' : Set α) (hS : Finite S) (hS' : S' ⊆ S)
+  : Finite S' := by
+  sorry
+
 /-- #### Exercise 6.1
 
 Show that the equation