diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
index 97091c5..9555c8a 100644
--- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
+++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
@@ -196,7 +196,9 @@ theorem infinitude_of_primes_tfae : [
 
   tfae_have 3 → 2 := by sorry -- Leonie
 
-  tfae_have 3 → 4 := by sorry -- Alexandra
+  tfae_have 3 → 4 := by -- Alexandra
+   intro a b c
+   exact a b
 
   tfae_have 5 → 4 := by sorry -- Sammy