From a7bde3532c3b69b3f33bfa03fe5c4ec8cbaab591 Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Tue, 6 Feb 2024 01:35:56 -0600
Subject: [PATCH] chg: Broken some steps for easier understanding

---
 LeanTalkSP24/infinitely_many_primes.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/LeanTalkSP24/infinitely_many_primes.lean b/LeanTalkSP24/infinitely_many_primes.lean
index e6df1df..62fb34f 100644
--- a/LeanTalkSP24/infinitely_many_primes.lean
+++ b/LeanTalkSP24/infinitely_many_primes.lean
@@ -23,13 +23,15 @@ theorem exists_prime_factor {n : Nat} (h : 2 ≤ n) : ∃ p : Nat, p.Prime ∧ p
   have : m ≠ 0 := by
     intro mz
     rw [mz, zero_dvd_iff] at mdvdn
-    linarith
+    -- linarith
+    rw [mz, mdvdn] at mltn
+    contradiction
   have mgt2 : 2 ≤ m := two_le this mne1
   by_cases mp : m.Prime
   · use m, mp
   . rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
     use p, pp
-    apply pdvd.trans mdvdn
+    exact Nat.dvd_trans pdvd mdvdn
 
 theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by
   intro n