From 7760086ea95a3d6c4eff9cf6c167e51bbae257da Mon Sep 17 00:00:00 2001
From: Christoph Spiegel <christophspiegel.berlin@gmail.com>
Date: Thu, 12 Mar 2026 11:24:54 +0100
Subject: [PATCH] =?UTF-8?q?prove=205=20=E2=86=92=204?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../P06_Mathlib/S01_PrimeTheorem.lean              | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
index 97091c5..bb14acb 100644
--- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
+++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
@@ -198,7 +198,19 @@ theorem infinitude_of_primes_tfae : [
 
   tfae_have 3 → 4 := by sorry -- Alexandra
 
-  tfae_have 5 → 4 := by sorry -- Sammy
+  tfae_have 5 → 4 := by -- Sammy
+    intro h S _
+    rcases Finset.eq_empty_or_nonempty S with SE|SNE
+    · use 2
+      constructor
+      · simp[SE]
+      · exact Nat.prime_two
+    · obtain ⟨maxS,h₂⟩ := Finset.max_of_nonempty SNE
+      obtain⟨p,h₃,h₄⟩ := h maxS
+      use p
+      constructor
+      · have h₅ := GT.gt.lt h₃; exact Finset.notMem_of_max_lt h₅ h₂
+      · exact h₄
 
   tfae_have 6 → 3 := by
    intro h