From f1a10c68770d835d8b86a8ef5d3f9bd724d5697b Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Thu, 14 Sep 2023 10:00:39 -0600
Subject: [PATCH] Enderton (set). Wrap original pigeonhole expression into aux.

---
 Bookshelf/Enderton/Set/Chapter_6.lean | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/Bookshelf/Enderton/Set/Chapter_6.lean b/Bookshelf/Enderton/Set/Chapter_6.lean
index 2f4271d..dcf16ff 100644
--- a/Bookshelf/Enderton/Set/Chapter_6.lean
+++ b/Bookshelf/Enderton/Set/Chapter_6.lean
@@ -65,11 +65,12 @@ theorem theorem_6b (A : Set α)
     have := hfa.right ⟨ha, h⟩
     exact absurd this h
 
-/-- #### Pigeonhole Principle
+/-! #### Pigeonhole Principle
 
 No natural number is equinumerous to a proper subset of itself.
 -/
-theorem pigeonhole_principle (n : ℕ)
+
+lemma pigeonhole_principle_aux (n : ℕ)
   : ∀ m : ℕ, m < n →
       ∀ f : Fin m → Fin n, Function.Injective f →
         ¬ Function.Surjective f := by
@@ -318,6 +319,12 @@ theorem pigeonhole_principle (n : ℕ)
     simp only [Fin.coe_eq_castSucc, Set.mem_setOf_eq] at hfa
     exact absurd (hf_surj $ Fin.castSucc a) hfa
 
+theorem pigeonhole_principle (m n : ℕ) (h : m < n)
+  : ∀ f : Fin m → Fin n, ¬ Function.Bijective f := by
+  intro f nf
+  have := pigeonhole_principle_aux n m h f nf.left
+  exact absurd nf.right this
+
 /-- #### Corollary 6C
 
 No finite set is equinumerous to a proper subset of itself.