From 7275ff9294627670d38f538fce36719447d823ec Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Tyburn?= <theo.tyburn@posteo.net>
Date: Thu, 12 Mar 2026 11:10:38 +0100
Subject: [PATCH 1/2] Proof

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

diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
index 9437e8e..8505341 100644
--- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
+++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
@@ -181,7 +181,35 @@ theorem infinitude_of_primes_tfae : [
    Cardinal.mk { p : ℕ // p.Prime } = ℵ₀,
   ].TFAE := by
 
-  tfae_have 5 → 6 := by sorry -- Theo
+    tfae_have 5 → 6 := by -- Theo
+      intro h
+      choose P hP using h
+      have ⟨pn, hp⟩ := And.intro (fun n ↦ (hP n).left) fun n ↦ (hP n).right
+
+      let f : ℕ → ℕ := fun n ↦ P^[n+1] 0
+      use f
+
+      have iterate_nfixed (f : ℕ → ℕ) (h : ∀ x, f x > x) (x n : ℕ) : f^[n+1] x > f^[n] x := by
+        rw [Function.iterate_succ']
+        exact h (f^[n] x)
+
+      have hfinc: ∀ (n : ℕ), f (n + 1) > f n := by
+        unfold f
+        intro n
+        exact iterate_nfixed P pn 0 (n+1)
+
+      have hfmon : StrictMono f := by exact strictMono_nat_of_lt_succ hfinc
+
+      have hfinj : Function.Injective f := StrictMono.injective hfmon
+
+      have hfprime (n : ℕ) : Nat.Prime (f n) := by
+        unfold f
+        cases n with
+        | zero => exact hp 0
+        | succ k => rw [Function.iterate_succ']
+                    exact hp (P^[k+1] 0)
+
+      use hfinj
 
   tfae_have 2 → 3 := by sorry -- Arthur
 

From ec8dcfbc37bccbdfeea56c283c84d0c97d8b8b48 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Tyburn?= <theo.tyburn@posteo.net>
Date: Thu, 12 Mar 2026 11:15:38 +0100
Subject: [PATCH 2/2] Add missing import

---
 LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
index 8505341..aa1ba88 100644
--- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
+++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
@@ -5,6 +5,9 @@ import Mathlib.NumberTheory.PrimeCounting
 import Mathlib.SetTheory.Cardinal.Basic
 import Mathlib.Tactic.TFAE
 
+import Mathlib.Logic.Function.Iterate
+import Mathlib.Order.Monotone.Basic
+
 /-
 ## Euclid's theorem: there are infinitely many primes