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

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

diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
index 97091c5..7e00e32 100644
--- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
+++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
@@ -183,7 +183,31 @@ theorem infinitude_of_primes_tfae : [
 
   tfae_have 5 → 6 := by sorry -- Theo
 
-  tfae_have 2 → 3 := by sorry -- Arthur
+  tfae_have 2 → 3 := by -- Arthur
+   intro h S
+   let s := Set.infinite_univ_iff.2 h
+   let P := @Set.univ { p // Nat.Prime p }
+   by_contra a
+   push_neg at a
+   let PN := P.image Subtype.val
+   have PS : PN ⊆ S := by rw [Set.subset_def]
+                          intro k b
+                          by_contra l
+                          have x : k ∉ S := by exact Finset.notMem_mono (fun ⦃a⦄ a_1 ↦ a_1) l
+                          have knp := a k x
+                          have kp : Nat.Prime k := by unfold PN at b
+                                                      unfold P at b
+                                                      simp at b
+                                                      exact b
+                          contradiction
+   have PNI : PN.Infinite := by unfold PN
+                                unfold P
+                                simp
+                                exact Set.infinite_coe_iff.mp h
+   have SF : (S : Set ℕ).Finite := by exact Finset.finite_toSet S
+   obtain ⟨a , inn, nis⟩ := Set.Infinite.exists_notMem_finite PNI SF
+   let is := PS inn
+   contradiction
 
   tfae_have 1 → 2 := by sorry -- Onat