import Mathlib.Data.Nat.Prime import Mathlib.Algebra.BigOperators.Order import Mathlib.Tactic import Mathlib.Tactic.IntervalCases open BigOperators theorem two_le {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := by have : m > 0 := Nat.pos_of_ne_zero h0 have : m >= 1 := this have h1 : 1 ≠ m := Ne.symm h1 change ¬_ = _ at h1 have : m > 1 := Nat.lt_of_le_of_ne this h1 exact this theorem exists_prime_factor {n : Nat} (h : 2 ≤ n) : ∃ p : Nat, p.Prime ∧ p ∣ n := by by_cases np : n.Prime · use n, np induction' n using Nat.strong_induction_on with n ih rw [Nat.prime_def_lt] at np push_neg at np rcases np h with ⟨m, mltn, mdvdn, mne1⟩ have : m ≠ 0 := by intro mz rw [mz, zero_dvd_iff] at mdvdn -- 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 exact Nat.dvd_trans pdvd mdvdn theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by intro n have : 2 ≤ Nat.factorial (n + 1) + 1 := by apply Nat.succ_le_succ apply Nat.succ_le_of_lt apply Nat.factorial_pos rcases exists_prime_factor this with ⟨p, pp, pdvd⟩ refine' ⟨p, _, pp⟩ show p > n by_contra ple push_neg at ple have : p ∣ Nat.factorial (n + 1) := by apply Nat.dvd_factorial apply pp.pos linarith have : p ∣ 1 := by convert Nat.dvd_sub' pdvd this simp show False have ple1 : p ≤ 1 := Nat.le_of_dvd (Nat.lt_succ_self 0) this have plt1 : p > 1 := pp.one_lt linarith open Finset section variable {α : Type _} [DecidableEq α] (r s t : Finset α) example : r ∩ (s ∪ t) ⊆ r ∩ s ∪ r ∩ t := by rw [subset_iff] intro x rw [mem_inter, mem_union, mem_union, mem_inter, mem_inter] tauto example : r ∩ (s ∪ t) ⊆ r ∩ s ∪ r ∩ t := by simp [subset_iff] intro x tauto example : r ∩ s ∪ r ∩ t ⊆ r ∩ (s ∪ t) := by simp [subset_iff] intro x tauto example : r ∩ s ∪ r ∩ t = r ∩ (s ∪ t) := by ext x simp tauto end theorem _root_.Nat.Prime.eq_of_dvd_of_prime {p q : ℕ} (prime_p : Nat.Prime p) (prime_q : Nat.Prime q) (h : p ∣ q) : p = q := by cases prime_q.eq_one_or_self_of_dvd _ h · linarith [prime_p.two_le] assumption theorem mem_of_dvd_prod_primes {s : Finset ℕ} {p : ℕ} (prime_p : p.Prime) : (∀ n ∈ s, Nat.Prime n) → (p ∣ ∏ n in s, n) → p ∈ s := by intro h₀ h₁ induction' s using Finset.induction_on with a s ans ih · simp at h₁ linarith [prime_p.two_le] simp [Finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁ rw [mem_insert] cases' h₁ with h₁ h₁ · left exact prime_p.eq_of_dvd_of_prime h₀.1 h₁ right exact ih h₀.2 h₁ theorem primes_infinite' : ∀ s : Finset Nat, ∃ p, Nat.Prime p ∧ p ∉ s := by intro s by_contra h push_neg at h set s' := s.filter Nat.Prime with s'_def have mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime := by intro n simp [s'_def] apply h have : 2 ≤ (∏ i in s', i) + 1 := by apply Nat.succ_le_succ apply Nat.succ_le_of_lt apply Finset.prod_pos intro n ns' apply (mem_s'.mp ns').pos rcases exists_prime_factor this with ⟨p, pp, pdvd⟩ have : p ∣ ∏ i in s', i := by apply dvd_prod_of_mem rw [mem_s'] apply pp have : p ∣ 1 := by convert Nat.dvd_sub' pdvd this simp show False have := Nat.le_of_dvd zero_lt_one this linarith [pp.two_le] theorem bounded_of_ex_finset (Q : ℕ → Prop) : (∃ s : Finset ℕ, ∀ k, Q k → k ∈ s) → ∃ n, ∀ k, Q k → k < n := by rintro ⟨s, hs⟩ use s.sup id + 1 intro k Qk apply Nat.lt_succ_of_le show id k ≤ s.sup id apply le_sup (hs k Qk) theorem ex_finset_of_bounded (Q : ℕ → Prop) [DecidablePred Q] : (∃ n, ∀ k, Q k → k ≤ n) → ∃ s : Finset ℕ, ∀ k, Q k ↔ k ∈ s := by rintro ⟨n, hn⟩ use (range (n + 1)).filter Q intro k simp [Nat.lt_succ_iff] exact hn k theorem mod_4_eq_3_or_mod_4_eq_3 {m n : ℕ} (h : m * n % 4 = 3) : m % 4 = 3 ∨ n % 4 = 3 := by revert h rw [Nat.mul_mod] have : m % 4 < 4 := Nat.mod_lt m (by norm_num) interval_cases hm : m % 4 <;> simp [hm] have : n % 4 < 4 := Nat.mod_lt n (by norm_num) interval_cases hn : n % 4 <;> simp [hn] theorem two_le_of_mod_4_eq_3 {n : ℕ} (h : n % 4 = 3) : 2 ≤ n := by apply two_le <;> · intro neq rw [neq] at h norm_num at h theorem aux {m n : ℕ} (h₀ : m ∣ n) (h₁ : 2 ≤ m) (h₂ : m < n) : n / m ∣ n ∧ n / m < n := by constructor · exact Nat.div_dvd_of_dvd h₀ exact Nat.div_lt_self (lt_of_le_of_lt (zero_le _) h₂) h₁ theorem exists_prime_factor_mod_4_eq_3 {n : Nat} (h : n % 4 = 3) : ∃ p : Nat, p.Prime ∧ p ∣ n ∧ p % 4 = 3 := by by_cases np : n.Prime · use n induction' n using Nat.strong_induction_on with n ih rw [Nat.prime_def_lt] at np push_neg at np rcases np (two_le_of_mod_4_eq_3 h) with ⟨m, mltn, mdvdn, mne1⟩ have mge2 : 2 ≤ m := by apply two_le _ mne1 intro mz rw [mz, zero_dvd_iff] at mdvdn linarith have neq : m * (n / m) = n := Nat.mul_div_cancel' mdvdn have : m % 4 = 3 ∨ n / m % 4 = 3 := by apply mod_4_eq_3_or_mod_4_eq_3 rw [neq, h] cases' this with h1 h1 · by_cases mp : m.Prime · use m rcases ih m mltn h1 mp with ⟨p, pp, pdvd, p4eq⟩ use p exact ⟨pp, pdvd.trans mdvdn, p4eq⟩ obtain ⟨nmdvdn, nmltn⟩ := aux mdvdn mge2 mltn by_cases nmp : (n / m).Prime · use n / m rcases ih (n / m) nmltn h1 nmp with ⟨p, pp, pdvd, p4eq⟩ use p exact ⟨pp, pdvd.trans nmdvdn, p4eq⟩ theorem primes_mod_4_eq_3_infinite : ∀ n, ∃ p > n, Nat.Prime p ∧ p % 4 = 3 := by by_contra h push_neg at h cases' h with n hn have : ∃ s : Finset Nat, ∀ p : ℕ, p.Prime ∧ p % 4 = 3 ↔ p ∈ s := by apply ex_finset_of_bounded use n contrapose! hn rcases hn with ⟨p, ⟨pp, p4⟩, pltn⟩ exact ⟨p, pltn, pp, p4⟩ cases' this with s hs have h₁ : ((4 * ∏ i in erase s 3, i) + 3) % 4 = 3 := by rw [add_comm, Nat.add_mul_mod_self_left] norm_num rcases exists_prime_factor_mod_4_eq_3 h₁ with ⟨p, pp, pdvd, p4eq⟩ have ps : p ∈ s := by rw [← hs p] exact ⟨pp, p4eq⟩ have pne3 : p ≠ 3 := by intro peq rw [peq, ← Nat.dvd_add_iff_left (dvd_refl 3)] at pdvd rw [Nat.prime_three.dvd_mul] at pdvd norm_num at pdvd have : 3 ∈ s.erase 3 := by apply mem_of_dvd_prod_primes Nat.prime_three _ pdvd intro n simp [← hs n] tauto simp at this have : p ∣ 4 * ∏ i in erase s 3, i := by apply dvd_trans _ (dvd_mul_left _ _) apply dvd_prod_of_mem simp constructor <;> assumption have : p ∣ 3 := by convert Nat.dvd_sub' pdvd this simp have : p = 3 := by apply pp.eq_of_dvd_of_prime Nat.prime_three this contradiction