From 8f714dbe4291994571bd98474b8f8455e8c75571 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 25 Jul 2025 09:34:41 +0100
Subject: [PATCH 1/5] refactor: following #2746

---
 src/Data/Fin/Properties.agda | 20 ++++++++------------
 1 file changed, 8 insertions(+), 12 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 0f87eef534..a1365729a7 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -1035,20 +1035,16 @@ pigeonhole : m ℕ.< n → (f : Fin n → Fin m) → ∃₂ λ i j → i < j ×
 pigeonhole z<s               f = contradiction (f zero) λ()
 pigeonhole (s<s m<n@(s≤s _)) f with any? (λ k → f zero ≟ f (suc k))
 ... | yes (j , f₀≡fⱼ) = zero , suc j , z<s , f₀≡fⱼ
-... | no  f₀≢fₖ
-  with i , j , i<j , fᵢ≡fⱼ ← pigeonhole m<n (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
-  = suc i , suc j , s<s i<j , punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
-
-injective⇒≤ : ∀ {f : Fin m → Fin n} → Injective _≡_ _≡_ f → m ℕ.≤ n
-injective⇒≤ {zero}  {_}     {f} _   = z≤n
-injective⇒≤ {suc _} {zero}  {f} _   = contradiction (f zero) ¬Fin0
-injective⇒≤ {suc _} {suc _} {f} inj = s≤s (injective⇒≤ (λ eq →
-  suc-injective (inj (punchOut-injective
-    (contraInjective inj 0≢1+n)
-    (contraInjective inj 0≢1+n) eq))))
+... | no  f₀≢fₖ =
+  let i , j , i<j , fᵢ≡fⱼ = pigeonhole m<n (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
+  in suc i , suc j , s<s i<j , punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
 
 <⇒notInjective : ∀ {f : Fin m → Fin n} → n ℕ.< m → ¬ (Injective _≡_ _≡_ f)
-<⇒notInjective n<m inj = ℕ.≤⇒≯ (injective⇒≤ inj) n<m
+<⇒notInjective {f = f} n<m inj =
+  let i , j , i<j , fᵢ≡fⱼ = pigeonhole n<m f in <-irrefl (inj fᵢ≡fⱼ) i<j
+
+injective⇒≤ : ∀ {f : Fin m → Fin n} → Injective _≡_ _≡_ f → m ℕ.≤ n
+injective⇒≤ = ℕ.≮⇒≥ ∘ flip <⇒notInjective
 
 ℕ→Fin-notInjective : ∀ (f : ℕ → Fin n) → ¬ (Injective _≡_ _≡_ f)
 ℕ→Fin-notInjective f inj = ℕ.<-irrefl refl

From f9e3203bd3e2d37f8dd90fb46fdb44efa6bd3396 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 26 Jul 2025 11:19:37 +0100
Subject: [PATCH 2/5] refactor: deploy the `flip contradiction` workaround

---
 src/Data/Fin/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index a1365729a7..0f596ea58e 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -1063,7 +1063,7 @@ injective⇒existsPivot : ∀ {f : Fin n → Fin m} → Injective _≡_ _≡_ f
 injective⇒existsPivot {f = f} f-injective i
   with any? (λ j → j ≤? i ×-dec i ≤? f j)
 ... | yes result = result
-... | no ¬result = contradiction (injective⇒≤ f∘inject!-injective) ℕ.1+n≰n
+... | no ¬result = flip contradiction (<⇒notInjective (ℕ.n<1+n _)) f∘inject!-injective
   where
   fj<i : (j : Fin′ (suc i)) → f (inject! j) < i
   fj<i j with f (inject! j) <? i

From e8580144cfe7b3af934b8662bb1a9dd66b70e47b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 26 Jul 2025 12:47:01 +0100
Subject: [PATCH 3/5] =?UTF-8?q?refactor:=20prefer=20`<=E2=87=92notInjectiv?=
 =?UTF-8?q?e`=20over=20`injective=E2=87=92=E2=89=A4`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Fin/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 0f596ea58e..639d85bebc 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -1047,8 +1047,8 @@ injective⇒≤ : ∀ {f : Fin m → Fin n} → Injective _≡_ _≡_ f → m 
 injective⇒≤ = ℕ.≮⇒≥ ∘ flip <⇒notInjective
 
 ℕ→Fin-notInjective : ∀ (f : ℕ → Fin n) → ¬ (Injective _≡_ _≡_ f)
-ℕ→Fin-notInjective f inj = ℕ.<-irrefl refl
-  (injective⇒≤ (Comp.injective _≡_ _≡_ _≡_ toℕ-injective inj))
+ℕ→Fin-notInjective f inj = 
+  <⇒notInjective (ℕ.n<1+n _) (Comp.injective _≡_ _≡_ _≡_ toℕ-injective inj)
 
 -- Cantor-Schröder-Bernstein for finite sets
 

From cffce87595d830839371241dd4660bc8e3d7a308 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 26 Jul 2025 12:50:16 +0100
Subject: [PATCH 4/5] fix: whitespace

---
 src/Data/Fin/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 639d85bebc..fec02528a9 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -1047,7 +1047,7 @@ injective⇒≤ : ∀ {f : Fin m → Fin n} → Injective _≡_ _≡_ f → m 
 injective⇒≤ = ℕ.≮⇒≥ ∘ flip <⇒notInjective
 
 ℕ→Fin-notInjective : ∀ (f : ℕ → Fin n) → ¬ (Injective _≡_ _≡_ f)
-ℕ→Fin-notInjective f inj = 
+ℕ→Fin-notInjective f inj =
   <⇒notInjective (ℕ.n<1+n _) (Comp.injective _≡_ _≡_ _≡_ toℕ-injective inj)
 
 -- Cantor-Schröder-Bernstein for finite sets

From 92477cf9a6dfb4e912ef97c9bfc4b13b249b39ab Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 2 Aug 2025 12:06:26 +0100
Subject: [PATCH 5/5] fix: DRY with `private` specialisation

---
 src/Data/Fin/Properties.agda | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index fec02528a9..46f0ae80d2 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -1043,12 +1043,18 @@ pigeonhole (s<s m<n@(s≤s _)) f with any? (λ k → f zero ≟ f (suc k))
 <⇒notInjective {f = f} n<m inj =
   let i , j , i<j , fᵢ≡fⱼ = pigeonhole n<m f in <-irrefl (inj fᵢ≡fⱼ) i<j
 
+-- specialised to m = suc n
+
+private
+  notInjective-Fin[1+n]→Fin[n] : ∀ {f : Fin (suc n) → Fin n} → ¬ (Injective _≡_ _≡_ f)
+  notInjective-Fin[1+n]→Fin[n] {n = n} = <⇒notInjective (ℕ.n<1+n n)
+
 injective⇒≤ : ∀ {f : Fin m → Fin n} → Injective _≡_ _≡_ f → m ℕ.≤ n
 injective⇒≤ = ℕ.≮⇒≥ ∘ flip <⇒notInjective
 
 ℕ→Fin-notInjective : ∀ (f : ℕ → Fin n) → ¬ (Injective _≡_ _≡_ f)
-ℕ→Fin-notInjective f inj =
-  <⇒notInjective (ℕ.n<1+n _) (Comp.injective _≡_ _≡_ _≡_ toℕ-injective inj)
+ℕ→Fin-notInjective f =
+  notInjective-Fin[1+n]→Fin[n] ∘ Comp.injective _≡_ _≡_ _≡_ toℕ-injective
 
 -- Cantor-Schröder-Bernstein for finite sets
 
@@ -1063,7 +1069,7 @@ injective⇒existsPivot : ∀ {f : Fin n → Fin m} → Injective _≡_ _≡_ f
 injective⇒existsPivot {f = f} f-injective i
   with any? (λ j → j ≤? i ×-dec i ≤? f j)
 ... | yes result = result
-... | no ¬result = flip contradiction (<⇒notInjective (ℕ.n<1+n _)) f∘inject!-injective
+... | no ¬result = flip contradiction notInjective-Fin[1+n]→Fin[n] f∘inject!-injective
   where
   fj<i : (j : Fin′ (suc i)) → f (inject! j) < i
   fj<i j with f (inject! j) <? i