From 5f783040b479f430e87c7b12489575db3d3050e6 Mon Sep 17 00:00:00 2001
From: Anna <97442536+anliki@users.noreply.github.com>
Date: Thu, 12 Mar 2026 10:28:24 +0100
Subject: [PATCH] 6 -> 3

---
 .../P06_Mathlib/S01_PrimeTheorem.lean           | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
index a423dff..4ad863a 100644
--- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
+++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
@@ -82,8 +82,21 @@ theorem infinitude_of_primes_tfae : [
   tfae_have 3 → 4 := by sorry -- Alexandra
 
   tfae_have 5 → 4 := by sorry -- Sammy
-  
-  tfae_have 6 → 3 := by sorry -- Anna
+
+  tfae_have 6 → 3 := by
+   intro h
+   rcases h with ⟨P, hP_inj, hP_prime⟩
+   intro S
+   -- die Menge des Bilds von der inj. Fkt P ist unendlich
+   have hR : (Set.range P).Infinite := Set.infinite_range_of_injective hP_inj
+   -- ∃ p ∈ ℕ , p ∈ hR ∧ p ∉ S , weil S endl. hR unendlich
+   obtain ⟨p, hpR, hpS⟩ := Set.Infinite.exists_notMem_finset hR S
+   -- p ∈ hR -> ∃ k ∈ ℕ , p = P k
+   rcases hpR with ⟨k, rfl⟩
+   -- p = P k ist eine Primzahl
+   have g : Nat.Prime (P k) := hP_prime k
+   use (P k)
+
 
   tfae_have 6 → 1 := by sorry -- Alexander