{"claim":{"assessments":[],"bundle":{"code":"\n// file: rw.py\nimport re,sys\nE=open('new/E.lean').read()\nFblk=\"namespace Lemma.E\\n\\n\"+E.split(\"\\n\\ntheorem I\")[0].split(\"namespace Lemma.E\\n\\n\")[1]+\"\\n\\nend Lemma.E\\n\"\nspecs={'5_eq_4':('exists4',5,4,'hf',0),'10_eq_9':('exists4',5,4,'hf',0),'8_eq_3':('existsA',8,3,'hf',0),'8_eq_5':('existsA',8,5,'hf',0),\n'8_eq_7':('exists7',8,7,'hf',0),'12_eq_5':('existsA',12,5,'hf',0),'12_eq_7':('existsA',12,7,'hf',0),'12_eq_11':('exists11',12,11,'hf',0),\n'7_eq_6':('exists_factor',7,6,'hall',1),'9_eq_8':('exists_factor',9,8,'hall',1),'11_eq_10':('exists_factor',11,10,'hall',1)}\nfor k,(nm,m,a,hf,sw) in specs.items():\n s=open(f'proofs/Lemma.primes_mod_{k}.lean').read()\n i=s.index(f'theorem {nm} (N')\n j=s.index(':= by',i)\n # end of body: next line starting with 'theorem' or 'end'\n mm=re.compile(r'\\n(theorem|end|lemma|def|noncomputable) ').search(s,j)\n call=f'Lemma.E.F {m} {a} (by norm_num) N hN {hf}'\n body=f':=\\n {call}\\n' if not sw else f':=\\n let ⟨q, h1, h2, h3⟩ := {call}\\n ⟨q, h1, h3, h2⟩\\n'\n s=s[:j]+body+s[mm.start():]\n hdr,rest=s.split('\\n',1)\n s=hdr+'\\n\\n'+Fblk+rest\n open(f'new/Lemma.primes_mod_{k}.lean','w').write(s)\n\n// file: rw2.py\nimport re\nF=open('new/F.lean').read()\nspecs={'5_eq_4':('exists4',5,4,'hf',0),'10_eq_9':('exists4',5,4,'hf',0),'8_eq_3':('existsA',8,3,'hf',0),'8_eq_5':('existsA',8,5,'hf',0),\n'8_eq_7':('exists7',8,7,'hf',0),'12_eq_5':('existsA',12,5,'hf',0),'12_eq_7':('existsA',12,7,'hf',0),'12_eq_11':('exists11',12,11,'hf',0),\n'7_eq_6':('exists_factor',7,6,'hall',1),'9_eq_8':('exists_factor',9,8,'hall',1),'11_eq_10':('exists_factor',11,10,'hall',1)}\nfor k,(nm,m,a,hf,sw) in specs.items():\n s=open(f'src/Lemma.primes_mod_{k}.lean').read()\n i=s.index(f'theorem {nm} (N')\n j=s.index(':= by',i)\n mm=re.compile(r'\\n(theorem|end|lemma|def|noncomputable) ').search(s,j)\n call=f'Lemma.EF {m} {a} (by norm_num) N hN {hf}'\n if sw:\n s=s[:j]+f':=\\n let ⟨q, h1, h2, h3⟩ := {call}\\n ⟨q, h1, h3, h2⟩\\n'+s[mm.start():]\n else:\n s=s[:i]+s[mm.start()+1:]\n s=re.sub(r'(Lemma\\.\\w+\\.)?\\b'+nm+r'\\b',f'Lemma.EF {m} {a} (by norm_num)',s)\n hdr,rest=s.split('\\n',1)\n open(f'new/Lemma.primes_mod_{k}.lean','w').write(hdr+'\\n\\n'+F+rest)\n\n","commit":"05ae10dc3e8c376c905926f8f6e6d433eabdedd4","config":null,"environment":"lemma/0.7.9 agent","logs":"","seeds":[]},"candidate":{"proofs":{"Lemma.primes_mod_10_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Q101\n\ntheorem prime_p : Nat.Prime 5 := by decide\n\ntheorem key (x : ℕ) (hx : 10 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 4 + x ^ 3 + x ^ 2 + x + 1) : q % 10 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 5) := Fact.mk prime_p\n have h1 : ((x ^ 4 + x ^ 3 + x ^ 2 + x + 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at h1\n have hndvd : ¬ q ∣ x := by\n intro hqx\n have : (x : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqx\n rw [this] at h1\n simp at h1\n refine ⟨?_, hndvd⟩\n have hx0 : (x : ZMod q) ≠ 0 := by\n intro h\n exact hndvd ((CharP.cast_eq_zero_iff (ZMod q) q _).1 h)\n have hx1 : (x : ZMod q) ≠ 1 := by\n intro h\n rw [h] at h1\n have h3 : ((5 : ℕ) : ZMod q) = 0 := by push_cast; linear_combination h1\n have hq3 : q ∣ 5 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n have : q = 5 := (Nat.prime_dvd_prime_iff_eq hq prime_p).1 hq3\n exact hndvd (this ▸ (Dvd.dvd.trans (by norm_num) hx))\n have hx3 : (x : ZMod q) ^ 5 = 1 := by\n linear_combination ((x : ZMod q) - 1) * h1\n have hord : orderOf (x : ZMod q) = 5 := orderOf_eq_prime hx3 hx1\n have hdvd : 5 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have h2 := hq.two_le\n have hq2 : q ≠ 2 := by\n rintro rfl\n obtain ⟨k, rfl⟩ := hx\n apply absurd hd\n rw [Nat.dvd_iff_mod_eq_zero]\n have : ∀ y : ℕ, y % 2 = 0 → (y ^ 4 + y ^ 3 + y ^ 2 + y + 1) % 2 = 1 := by\n intro y hy\n obtain ⟨j, rfl⟩ : 2 ∣ y := Nat.dvd_of_mod_eq_zero hy\n rw [Nat.add_mod]\n simp [Nat.pow_mod, Nat.mul_mod, Nat.add_mod]\n rw [this _ (by omega)]\n omega\n rcases Nat.even_or_odd q with he | ho\n · exact absurd ((Nat.prime_dvd_prime_iff_eq Nat.prime_two hq).1 (even_iff_two_dvd.1 he)).symm hq2\n · obtain ⟨k, hk⟩ := ho\n omega\n\nend Lemma.Q101\n\ntheorem Lemma.primes_mod_10_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 10 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 10).factorial with hxdef\n have hx6 : 10 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hN : x ^ 4 + x ^ 3 + x ^ 2 + x + 1 ≠ 1 := by\n have : 0 < x := Nat.factorial_pos _\n omega\n have hq := Nat.minFac_prime hN\n have hqd := Nat.minFac_dvd (x ^ 4 + x ^ 3 + x ^ 2 + x + 1)\n obtain ⟨h6, hnd⟩ := Lemma.Q101.key x hx6 _ hq hqd\n refine ⟨_, ⟨hq, h6⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_10_eq_9":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\nnamespace Lemma.P54\n\ntheorem z5 : (5 : ZMod 5) = 0 := by decide\n\ntheorem nsq2 : ∀ r : ZMod 5, ((2 : ℕ) : ZMod 5) ≠ r * r := by decide\n\ntheorem nsq3 : ∀ r : ZMod 5, ((3 : ℕ) : ZMod 5) ≠ r * r := by decide\n\ntheorem key (y : ℕ) (hy : 2 ∣ y) (hy0 : 0 < y) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ 5 * y ^ 2 - 1) : (q % 5 = 1 ∨ q % 5 = 4) ∧ ¬ q ∣ y := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 5) := Fact.mk Nat.prime_five\n have h1 : ((5 * y ^ 2 - 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n have h5 : 1 ≤ 5 * y ^ 2 := by\n have : 1 ≤ y ^ 2 := Nat.one_le_pow _ _ hy0\n omega\n have h2 : (5 : ZMod q) * (y : ZMod q) ^ 2 = 1 := by\n rw [Nat.cast_sub h5] at h1\n push_cast at h1\n linear_combination h1\n have hndvd : ¬ q ∣ y := by\n intro hqy\n have : (y : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy\n rw [this] at h2\n simp at h2\n refine ⟨?_, hndvd⟩\n have hq2 : q ≠ 2 := by\n rintro rfl\n exact hndvd hy\n have hq5 : q ≠ 5 := by\n rintro rfl\n have : (5 : ZMod 5) = 0 := z5\n rw [this] at h2\n simp at h2\n have hsq : IsSquare ((5 : ℕ) : ZMod q) := ⟨5 * y, by push_cast; linear_combination (-5) * h2⟩\n obtain ⟨r, hr⟩ :=\n (ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one (p := 5) (q := q) (by norm_num) hq2).2 hsq\n rw [← ZMod.natCast_mod q 5] at hr\n have hlt := Nat.mod_lt q (by norm_num : 5 > 0)\n generalize hm : q % 5 = m at hr hlt\n obtain h | h | h | h | h : m = 0 ∨ m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 := by omega\n · subst h\n exact absurd ((Nat.prime_dvd_prime_iff_eq Nat.prime_five hq).1\n (Nat.dvd_of_mod_eq_zero hm)).symm hq5\n · exact Or.inl h\n · subst h\n exact absurd hr (nsq2 r)\n · subst h\n exact absurd hr (nsq3 r)\n · exact Or.inr h\n\nend Lemma.P54\n\ntheorem Lemma.aux54 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 5 = 4} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n have hy2 : 2 ∣ (n + 5).factorial := Nat.dvd_factorial (by norm_num) (by omega)\n have hy0 : 0 < (n + 5).factorial := Nat.factorial_pos _\n have hN : (5 * (n + 5).factorial ^ 2 - 1) % 5 = 4 := by\n have : 1 ≤ (n + 5).factorial ^ 2 := Nat.one_le_pow _ _ hy0\n omega\n obtain ⟨q, hq, hqd, hq4⟩ := Lemma.EF 5 4 (by norm_num) _ hN\n (fun q hq hd => (Lemma.P54.key _ hy2 hy0 q hq hd).1)\n refine ⟨q, ⟨hq, hq4⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P54.key _ hy2 hy0 q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n\ntheorem Lemma.primes_mod_10_eq_9 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 10 = 9} := by\n refine Lemma.aux54.mono ?_\n rintro p ⟨hp, h4⟩\n refine ⟨hp, ?_⟩\n rcases hp.eq_two_or_odd with h2 | h2\n · subst h2; simp at h4\n · omega\n-- U180 cold\n","Lemma.primes_mod_11_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Q111\n\ntheorem prime_p : Nat.Prime 11 := by decide\n\ntheorem key (x : ℕ) (hx : 11 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 10 + x ^ 9 + x ^ 8 + x ^ 7 + x ^ 6 + x ^ 5 + x ^ 4 + x ^ 3 + x ^ 2 + x + 1) : q % 11 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 11) := Fact.mk prime_p\n have h1 : ((x ^ 10 + x ^ 9 + x ^ 8 + x ^ 7 + x ^ 6 + x ^ 5 + x ^ 4 + x ^ 3 + x ^ 2 + x + 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at h1\n have hndvd : ¬ q ∣ x := by\n intro hqx\n have : (x : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqx\n rw [this] at h1\n simp at h1\n refine ⟨?_, hndvd⟩\n have hx0 : (x : ZMod q) ≠ 0 := by\n intro h\n exact hndvd ((CharP.cast_eq_zero_iff (ZMod q) q _).1 h)\n have hx1 : (x : ZMod q) ≠ 1 := by\n intro h\n rw [h] at h1\n have h3 : ((11 : ℕ) : ZMod q) = 0 := by push_cast; linear_combination h1\n have hq3 : q ∣ 11 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n have : q = 11 := (Nat.prime_dvd_prime_iff_eq hq prime_p).1 hq3\n exact hndvd (this ▸ hx)\n have hx3 : (x : ZMod q) ^ 11 = 1 := by\n linear_combination ((x : ZMod q) - 1) * h1\n have hord : orderOf (x : ZMod q) = 11 := orderOf_eq_prime hx3 hx1\n have hdvd : 11 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have h2 := hq.two_le\n omega\n\nend Lemma.Q111\n\ntheorem Lemma.primes_mod_11_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 11 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 22).factorial with hxdef\n have hx6 : 11 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hN : x ^ 10 + x ^ 9 + x ^ 8 + x ^ 7 + x ^ 6 + x ^ 5 + x ^ 4 + x ^ 3 + x ^ 2 + x + 1 ≠ 1 := by\n have : 0 < x := Nat.factorial_pos _\n omega\n have hq := Nat.minFac_prime hN\n have hqd := Nat.minFac_dvd (x ^ 10 + x ^ 9 + x ^ 8 + x ^ 7 + x ^ 6 + x ^ 5 + x ^ 4 + x ^ 3 + x ^ 2 + x + 1)\n obtain ⟨h6, hnd⟩ := Lemma.Q111.key x hx6 _ hq hqd\n refine ⟨_, ⟨hq, h6⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_11_eq_10":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\nnamespace Lemma.P1110\n\nopen Polynomial\n\ntheorem prime11 : Nat.Prime 11 := by decide\n\ntheorem key (q : ℕ) (hq : q.Prime) (hq11 : q ≠ 11) (t : ZMod q)\n (ht : t ^ 5 + t ^ 4 - 4 * t ^ 3 - 3 * t ^ 2 + 3 * t + 1 = 0) :\n q % 11 = 1 ∨ q % 11 = 10 := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 11) := Fact.mk prime11\n set p : (ZMod q)[X] := X ^ 2 - C t * X + 1 with hpdef\n have hp : p.natDegree = 2 := by rw [hpdef]; compute_degree!\n have hpu : ¬ IsUnit p := by\n intro h\n have := Polynomial.natDegree_eq_zero_of_isUnit h\n omega\n have hp0 : p ≠ 0 := by\n intro h\n rw [h] at hp\n simp at hp\n obtain ⟨g, hg, hgp⟩ := WfDvdMonoid.exists_irreducible_factor hpu hp0\n haveI := Fact.mk hg\n let K := AdjoinRoot g\n let r : K := AdjoinRoot.root g\n have hr0 : aeval r p = 0 := by\n obtain ⟨c, hc⟩ := hgp\n rw [hc, map_mul, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self, zero_mul]\n set T : K := algebraMap (ZMod q) K t with hTdef\n have hr : r ^ 2 - T * r + 1 = 0 := by\n rw [hpdef] at hr0\n simpa [hTdef] using hr0\n haveI : CharP K q := charP_of_injective_algebraMap (algebraMap (ZMod q) K).injective q\n have hT : T ^ 5 + T ^ 4 - 4 * T ^ 3 - 3 * T ^ 2 + 3 * T + 1 = 0 := by\n have := congrArg (algebraMap (ZMod q) K) ht\n simpa [hTdef, map_ofNat] using this\n have hTq : T ^ q = T := by rw [hTdef, ← map_pow, ZMod.pow_card]\n have hphi : r ^ 10 + r ^ 9 + r ^ 8 + r ^ 7 + r ^ 6 + r ^ 5 + r ^ 4 + r ^ 3 + r ^ 2 + r + 1\n = 0 := by\n linear_combination r ^ 5 * hT\n + (1 + r + r * T + r ^ 2 * T + r ^ 2 * T ^ 2 - r ^ 3 * T + r ^ 3 * T ^ 2 + r ^ 3 * T ^ 3\n + r ^ 4 - r ^ 4 * T - 2 * r ^ 4 * T ^ 2 + r ^ 4 * T ^ 3 + r ^ 4 * T ^ 4\n - r ^ 5 * T + r ^ 5 * T ^ 2 + r ^ 5 * T ^ 3 + r ^ 6 * T + r ^ 6 * T ^ 2\n + r ^ 7 + r ^ 7 * T + r ^ 8) * hr\n have hr11 : r ^ 11 = 1 := by\n linear_combination (r - 1) * hphi\n have hr1 : r ≠ 1 := by\n intro h1\n rw [h1] at hr\n have hT2 : T = 2 := by linear_combination -hr\n rw [hT2] at hT\n have h11 : ((11 : ℕ) : K) = 0 := by push_cast; linear_combination hT\n have hq11' : q ∣ 11 := (CharP.cast_eq_zero_iff K q 11).1 h11\n exact hq11 ((Nat.prime_dvd_prime_iff_eq hq prime11).1 hq11')\n have hrne : r ≠ 0 := by\n intro h0\n rw [h0] at hr\n simp at hr\n have hrq : (r ^ q) ^ 2 - T * r ^ q + 1 = 0 := by\n have : (r ^ 2 - T * r + 1) ^ q = 0 := by rw [hr, zero_pow hq.ne_zero]\n rw [add_pow_char, sub_pow_char, mul_pow, hTq, one_pow] at this\n rw [← this]\n ring\n have hprod : (r ^ q - r) * (r ^ q - (T - r)) = 0 := by linear_combination hrq - hr\n have hord : orderOf r = 11 := orderOf_eq_prime hr11 hr1\n have hq2 := hq.two_le\n rcases mul_eq_zero.1 hprod with h | h\n · have h' : r ^ (q - 1) = 1 := by\n have e : r ^ q = r ^ (q - 1) * r := by\n rw [← pow_succ]; congr 1; omega\n have : (r ^ (q - 1) - 1) * r = 0 := by linear_combination e.symm.trans (sub_eq_zero.1 h)\n rcases mul_eq_zero.1 this with h2 | h2\n · exact sub_eq_zero.1 h2\n · exact absurd h2 hrne\n have := orderOf_dvd_of_pow_eq_one h'\n rw [hord] at this\n omega\n · have h' : r ^ (q + 1) = 1 := by\n rw [pow_succ, sub_eq_zero.1 h]\n linear_combination -hr\n have := orderOf_dvd_of_pow_eq_one h'\n rw [hord] at this\n omega\n\ntheorem exists_factor (N : ℕ) (hN : N % 11 = 10)\n (hall : ∀ q, q.Prime → q ∣ N → q % 11 = 1 ∨ q % 11 = 10) :\n ∃ q, q.Prime ∧ q % 11 = 10 ∧ q ∣ N :=\n let ⟨q, h1, h2, h3⟩ := Lemma.EF 11 10 (by norm_num) N hN hall\n ⟨q, h1, h3, h2⟩\n\nend Lemma.P1110\n\ntheorem Lemma.primes_mod_11_eq_10 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 11 = 10} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set y := (n + 11).factorial with hydef\n have hy0 : 0 < y := Nat.factorial_pos _\n set x := 11 * y with hxdef\n have hx : 11 ≤ x := by omega\n have hle : x ^ 4 + 4 * x ^ 3 + 1 ≤ x ^ 5 + 3 * x ^ 2 + 3 * x := by\n have e5 : x ^ 5 = x ^ 4 * x := by ring\n have e4 : x ^ 4 = x ^ 3 * x := by ring\n have h3 : 1 ≤ x ^ 3 := Nat.one_le_pow _ _ (by omega)\n have h4 : x ^ 3 * 11 ≤ x ^ 3 * x := Nat.mul_le_mul_left _ hx\n have h5 : x ^ 4 * 11 ≤ x ^ 4 * x := Nat.mul_le_mul_left _ hx\n nlinarith\n set N := x ^ 5 + 3 * x ^ 2 + 3 * x - (x ^ 4 + 4 * x ^ 3 + 1) with hNdef\n have hN : N + (x ^ 4 + 4 * x ^ 3 + 1) = x ^ 5 + 3 * x ^ 2 + 3 * x := Nat.sub_add_cancel hle\n have hN' : N + (14641 * y ^ 4 + 5324 * y ^ 3 + 1) = 161051 * y ^ 5 + 363 * y ^ 2 + 33 * y := by\n rw [hxdef] at hN; linarith [hN]\n have hN11 : N % 11 = 10 := by\n generalize y ^ 5 = a at hN'\n generalize y ^ 4 = b at hN'\n generalize y ^ 3 = c at hN'\n generalize y ^ 2 = d at hN'\n omega\n have hfac : ∀ q, q.Prime → q ∣ N → (q % 11 = 1 ∨ q % 11 = 10) ∧ ¬ q ∣ y := by\n intro q hq hqN\n haveI := Fact.mk hq\n have hc : ((N : ℕ) : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqN\n have hc2 : ((N + (x ^ 4 + 4 * x ^ 3 + 1) : ℕ) : ZMod q)\n = ((x ^ 5 + 3 * x ^ 2 + 3 * x : ℕ) : ZMod q) := by rw [hN]\n push_cast at hc2\n rw [hc] at hc2\n have hf : (-(x : ZMod q)) ^ 5 + (-(x : ZMod q)) ^ 4 - 4 * (-(x : ZMod q)) ^ 3\n - 3 * (-(x : ZMod q)) ^ 2 + 3 * (-(x : ZMod q)) + 1 = 0 := by\n linear_combination hc2\n have hny : ¬ q ∣ y := by\n intro hqy\n have : (x : ZMod q) = 0 := by\n rw [hxdef]; push_cast\n rw [(CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy, mul_zero]\n rw [this] at hf\n norm_num at hf\n refine ⟨Lemma.P1110.key q hq ?_ _ hf, hny⟩\n rintro rfl\n have := Nat.mod_eq_zero_of_dvd hqN\n omega\n obtain ⟨q, hq, h10, hqd⟩ :=\n Lemma.P1110.exists_factor N hN11 (fun q hq hd => (hfac q hq hd).1)\n refine ⟨q, ⟨hq, h10⟩, ?_⟩\n by_contra hle'\n push_neg at hle'\n exact (hfac q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_12_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P121\n\ntheorem prime3 : Nat.Prime 3 := by decide\n\ntheorem key (x : ℕ) (hx3 : 3 ∣ x) (hx2 : 2 ∣ x) (N : ℕ) (hN : N + x ^ 2 = x ^ 4 + 1)\n (q : ℕ) (hq : q.Prime) (hd : q ∣ N) : q % 12 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 3) := Fact.mk prime3\n have hc : ((N : ℕ) : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n have hc2 : ((N + x ^ 2 : ℕ) : ZMod q) = ((x ^ 4 + 1 : ℕ) : ZMod q) := by rw [hN]\n push_cast at hc2\n rw [hc] at hc2\n have h1 : (x : ZMod q) ^ 4 - (x : ZMod q) ^ 2 + 1 = 0 := by linear_combination -hc2\n have hndvd : ¬ q ∣ x := by\n intro hqx\n have : (x : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqx\n rw [this] at h1\n simp at h1\n refine ⟨?_, hndvd⟩\n have hx0 : (x : ZMod q) ≠ 0 := fun h => hndvd ((CharP.cast_eq_zero_iff (ZMod q) q _).1 h)\n have hq3 : q ≠ 3 := by\n rintro rfl\n exact hndvd hx3\n have hq2 : q ≠ 2 := by\n rintro rfl\n exact hndvd hx2\n set u : ZMod q := -(x : ZMod q) ^ 2 with hu\n have hu3 : u ^ 3 = 1 := by\n rw [hu]\n linear_combination (-(x : ZMod q) ^ 2 - 1) * h1\n have hu1 : u ≠ 1 := by\n intro h\n rw [hu] at h\n have h3 : ((3 : ℕ) : ZMod q) = 0 := by\n push_cast\n linear_combination h1 + ((x : ZMod q) ^ 2 - 2) * h\n have hq3' : q ∣ 3 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n exact hq3 ((Nat.prime_dvd_prime_iff_eq hq prime3).1 hq3')\n have hu0 : u ≠ 0 := by\n rw [hu]\n exact neg_ne_zero.2 (pow_ne_zero _ hx0)\n have hord : orderOf u = 3 := orderOf_eq_prime hu3 hu1\n have hdvd : 3 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hu0\n have hsq : IsSquare (-1 : ZMod q) := by\n refine ⟨((x : ZMod q) ^ 2 - 1) * (x : ZMod q)⁻¹, ?_⟩\n have hinv : (x : ZMod q) * (x : ZMod q)⁻¹ = 1 := mul_inv_cancel₀ hx0\n linear_combination (-(x : ZMod q)⁻¹ ^ 2) * h1 + ((x : ZMod q) * (x : ZMod q)⁻¹ + 1) * hinv\n have h4 := (ZMod.exists_sq_eq_neg_one_iff (p := q)).1 hsq\n have hodd := hq.eq_two_or_odd\n have h2 := hq.two_le\n omega\n\nend Lemma.P121\n\ntheorem Lemma.primes_mod_12_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 12 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 3).factorial with hxdef\n have hx3 : 3 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hx2 : 2 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hx6 : 6 ≤ x := by\n have : (3 : ℕ).factorial ≤ (n + 3).factorial := Nat.factorial_le (by omega)\n have : (3 : ℕ).factorial = 6 := rfl\n omega\n have e : x ^ 4 = x ^ 2 * x ^ 2 := by ring\n have h36 : 36 ≤ x ^ 2 := by nlinarith\n have hbig : x ^ 2 * 36 ≤ x ^ 2 * x ^ 2 := Nat.mul_le_mul_left _ h36\n have hle : x ^ 2 ≤ x ^ 4 + 1 := by rw [e]; nlinarith\n set N := x ^ 4 + 1 - x ^ 2 with hNdef\n have hN : N + x ^ 2 = x ^ 4 + 1 := Nat.sub_add_cancel hle\n have hN1 : N ≠ 1 := by\n rw [e] at hN\n nlinarith\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n obtain ⟨h12, hnd⟩ := Lemma.P121.key x hx3 hx2 N hN _ hq hqd\n refine ⟨_, ⟨hq, h12⟩, ?_⟩\n by_contra hle'\n push_neg at hle'\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_12_eq_11":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\nnamespace Lemma.P1211\n\ntheorem z3 : (3 : ZMod 3) = 0 := by decide\n\ntheorem nsq2 : ∀ r : ZMod 3, ((2 : ℕ) : ZMod 3) ≠ r * r := by decide\n\ntheorem sq1 : IsSquare ((1 : ℕ) : ZMod 3) := ⟨1, by decide⟩\n\ntheorem prime_three' : Nat.Prime 3 := by decide\n\ntheorem key (y : ℕ) (hy : 2 ∣ y) (hy0 : 0 < y) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ 3 * y ^ 2 - 1) : (q % 12 = 1 ∨ q % 12 = 11) ∧ ¬ q ∣ y := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 3) := Fact.mk prime_three'\n have h1 : ((3 * y ^ 2 - 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n have h5 : 1 ≤ 3 * y ^ 2 := by\n have : 1 ≤ y ^ 2 := Nat.one_le_pow _ _ hy0\n omega\n have h2 : (3 : ZMod q) * (y : ZMod q) ^ 2 = 1 := by\n rw [Nat.cast_sub h5] at h1\n push_cast at h1\n linear_combination h1\n have hndvd : ¬ q ∣ y := by\n intro hqy\n have : (y : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy\n rw [this] at h2\n simp at h2\n refine ⟨?_, hndvd⟩\n have hq2 : q ≠ 2 := by\n rintro rfl\n exact hndvd hy\n have hq3 : q ≠ 3 := by\n rintro rfl\n have : (3 : ZMod 3) = 0 := z3\n rw [this] at h2\n simp at h2\n have hsq : IsSquare ((3 : ℕ) : ZMod q) := ⟨3 * y, by push_cast; linear_combination (-3) * h2⟩\n have hodd := hq.eq_two_or_odd\n have hq30 : q % 3 ≠ 0 := by\n intro h0\n exact hq3 ((Nat.prime_dvd_prime_iff_eq prime_three' hq).1\n (Nat.dvd_of_mod_eq_zero h0)).symm\n have hlt3 := Nat.mod_lt q (by norm_num : 3 > 0)\n rcases hodd with h | hodd\n · exact absurd h hq2\n have h4 : q % 4 = 1 ∨ q % 4 = 3 := by omega\n rcases h4 with h4 | h4\n · obtain ⟨r, hr⟩ :=\n (ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one (p := q) (q := 3) h4 (by norm_num)).1 hsq\n rw [← ZMod.natCast_mod q 3] at hr\n have : q % 3 ≠ 2 := by\n intro h32\n rw [h32] at hr\n exact nsq2 r hr\n left; omega\n · have hns : ¬ IsSquare ((q : ℕ) : ZMod 3) := fun hh =>\n (ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_three (p := 3) (q := q) (by norm_num) h4\n (Ne.symm hq3)).1 hh hsq\n rw [← ZMod.natCast_mod q 3] at hns\n have : q % 3 ≠ 1 := by\n intro h31\n rw [h31] at hns\n exact hns sq1\n right; omega\n\nend Lemma.P1211\n\ntheorem Lemma.primes_mod_12_eq_11 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 12 = 11} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n have hy2 : 2 ∣ (n + 3).factorial := Nat.dvd_factorial (by norm_num) (by omega)\n have hy0 : 0 < (n + 3).factorial := Nat.factorial_pos _\n have hN : (3 * (n + 3).factorial ^ 2 - 1) % 12 = 11 := by\n obtain ⟨k, hk⟩ := hy2\n have hz : (n + 3).factorial ^ 2 = 4 * k ^ 2 := by rw [hk]; ring\n have : 1 ≤ (n + 3).factorial ^ 2 := Nat.one_le_pow _ _ hy0\n rw [hz] at this ⊢\n omega\n obtain ⟨q, hq, hqd, hq4⟩ := Lemma.EF 12 11 (by norm_num) _ hN\n (fun q hq hd => (Lemma.P1211.key _ hy2 hy0 q hq hd).1)\n refine ⟨q, ⟨hq, hq4⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P1211.key _ hy2 hy0 q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_12_eq_5":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\nnamespace Lemma.P125\n\ndef P (n : ℕ) : ℕ := ∏ i ∈ Finset.range n, (6 * i + 5)\n\ntheorem P_mod (n : ℕ) : P n % 6 = 1 ∨ P n % 6 = 5 := by\n unfold P\n apply Finset.prod_induction _ (fun x => x % 6 = 1 ∨ x % 6 = 5)\n · intro a b ha hb\n rcases ha with ha | ha <;> rcases hb with hb | hb <;> rw [Nat.mul_mod, ha, hb] <;> decide\n · left; rfl\n · intro i _; right; omega\n\ntheorem P_sq (n : ℕ) : P n ^ 2 % 12 = 1 := by\n have h := P_mod n\n have h12 : P n % 12 = 1 ∨ P n % 12 = 5 ∨ P n % 12 = 7 ∨ P n % 12 = 11 := by omega\n rw [Nat.pow_mod]\n rcases h12 with h12 | h12 | h12 | h12 <;> rw [h12]\n\ntheorem dvd_P (n q : ℕ) (hq : q % 6 = 5) (hle : q ≤ n) : q ∣ P n := by\n unfold P\n have hmem : q / 6 ∈ Finset.range n := Finset.mem_range.2 (by omega)\n have := Finset.dvd_prod_of_mem (fun i => 6 * i + 5) hmem\n have he : 6 * (q / 6) + 5 = q := by omega\n simpa [he] using this\n\ntheorem prime_three' : Nat.Prime 3 := by decide\n\ntheorem key (n q : ℕ) (hq : q.Prime) (hd : q ∣ 4 * P n ^ 2 + 1) :\n (q % 12 = 1 ∨ q % 12 = 5) ∧ ¬ q ∣ P n := by\n haveI := Fact.mk hq\n have h2 : 4 * ((P n : ℕ) : ZMod q) ^ 2 + 1 = 0 := by\n have := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at this\n exact this\n have hq2 : q ≠ 2 := by\n rintro rfl\n have : (4 * P n ^ 2 + 1) % 2 = 0 := Nat.mod_eq_zero_of_dvd hd\n omega\n have hq3 : q ≠ 3 := by\n rintro rfl\n have : (4 * P n ^ 2 + 1) % 3 = 0 := Nat.mod_eq_zero_of_dvd hd\n have := P_sq n\n omega\n have hndvd : ¬ q ∣ P n := by\n intro hqy\n have : ((P n : ℕ) : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy\n rw [this] at h2\n simp at h2\n refine ⟨?_, hndvd⟩\n have hsq : IsSquare (-1 : ZMod q) := ⟨2 * (P n : ZMod q), by linear_combination (-1) * h2⟩\n have h4 := (ZMod.exists_sq_eq_neg_one_iff (p := q)).1 hsq\n have hodd := hq.eq_two_or_odd\n have hq30 : q % 3 ≠ 0 := by\n intro h0\n exact hq3 ((Nat.prime_dvd_prime_iff_eq prime_three' hq).1\n (Nat.dvd_of_mod_eq_zero h0)).symm\n omega\n\nend Lemma.P125\n\ntheorem Lemma.primes_mod_12_eq_5 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 12 = 5} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n have hN : (4 * Lemma.P125.P n ^ 2 + 1) % 12 = 5 := by\n have := Lemma.P125.P_sq n\n omega\n obtain ⟨q, hq, hqd, hq4⟩ := Lemma.EF 12 5 (by norm_num) _ hN\n (fun q hq hd => (Lemma.P125.key n q hq hd).1)\n refine ⟨q, ⟨hq, hq4⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P125.key n q hq hqd).2 (Lemma.P125.dvd_P n q (by omega) hle)\n-- U180 cold\n","Lemma.primes_mod_12_eq_7":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\nnamespace Lemma.P127\n\ndef Q (n : ℕ) : ℕ := ∏ i ∈ Finset.range n, (2 * i + 1)\n\ntheorem Q_odd (n : ℕ) : Q n % 2 = 1 := by\n unfold Q\n apply Finset.prod_induction _ (fun x => x % 2 = 1)\n · intro a b ha hb; rw [Nat.mul_mod, ha, hb]\n · rfl\n · intro i _; omega\n\ntheorem dvd_Q (n q : ℕ) (hq : q % 2 = 1) (hle : q ≤ n) : q ∣ Q n := by\n unfold Q\n have hmem : q / 2 ∈ Finset.range n := Finset.mem_range.2 (by omega)\n have := Finset.dvd_prod_of_mem (fun i => 2 * i + 1) hmem\n have he : 2 * (q / 2) + 1 = q := by omega\n simpa [he] using this\n\ntheorem prime3 : Nat.Prime 3 := by decide\n\ntheorem key (x : ℕ) (hx : 3 ∣ x) (hx2 : 2 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 2 + x + 1) : (q % 12 = 1 ∨ q % 12 = 7) ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 3) := Fact.mk prime3\n have h1 : ((x ^ 2 + x + 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at h1\n have hndvd : ¬ q ∣ x := by\n intro hqx\n have : (x : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqx\n rw [this] at h1\n simp at h1\n refine ⟨?_, hndvd⟩\n have hx0 : (x : ZMod q) ≠ 0 := by\n intro h\n exact hndvd ((CharP.cast_eq_zero_iff (ZMod q) q _).1 h)\n have hq3 : q ≠ 3 := by\n rintro rfl\n exact hndvd hx\n have hq2 : q ≠ 2 := by\n rintro rfl\n exact hndvd hx2\n have hn : (x : ZMod q) ≠ 1 := by\n intro h\n have h3 : ((3 : ℕ) : ZMod q) = 0 := by\n push_cast\n linear_combination h1 - ((x : ZMod q) + 2) * h\n have hq3' : q ∣ 3 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n exact hq3 ((Nat.prime_dvd_prime_iff_eq hq prime3).1 hq3')\n have h3 : (x : ZMod q) ^ 3 = 1 := by\n linear_combination ((x : ZMod q) - 1) * h1\n have hord : orderOf (x : ZMod q) = 3 := orderOf_eq_prime h3 hn\n have hdvd : 3 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have h2 := hq.two_le\n have hodd := hq.eq_two_or_odd\n omega\n\nend Lemma.P127\n\ntheorem Lemma.primes_mod_12_eq_7 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 12 = 7} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := 6 * Lemma.P127.Q n with hxdef\n have hx3 : 3 ∣ x := ⟨2 * Lemma.P127.Q n, by rw [hxdef]; ring⟩\n have hx2 : 2 ∣ x := ⟨3 * Lemma.P127.Q n, by rw [hxdef]; ring⟩\n have hN : (x ^ 2 + x + 1) % 12 = 7 := by\n have hQ := Lemma.P127.Q_odd n\n have : x ^ 2 + x + 1 = 12 * (3 * Lemma.P127.Q n ^ 2) + 6 * Lemma.P127.Q n + 1 := by\n rw [hxdef]; ring\n rw [this]\n omega\n obtain ⟨q, hq, hqd, hq7⟩ := Lemma.EF 12 7 (by norm_num) _ hN\n (fun q hq hd => (Lemma.P127.key x hx3 hx2 q hq hd).1)\n refine ⟨q, ⟨hq, hq7⟩, ?_⟩\n by_contra hle\n push_neg at hle\n have hqQ : q ∣ Lemma.P127.Q n := Lemma.P127.dvd_Q n q (by omega) hle\n exact (Lemma.P127.key x hx3 hx2 q hq hqd).2 (hqQ.trans ⟨6, by rw [hxdef]; ring⟩)\n-- U180 cold\n","Lemma.primes_mod_3_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P31\n\ntheorem key (x : ℕ) (hx : 6 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 2 + x + 1) : q % 6 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 3) := Fact.mk Nat.prime_three\n have h1 : ((x ^ 2 + x + 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at h1\n have hndvd : ¬ q ∣ x := by\n intro hqx\n have : (x : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqx\n rw [this] at h1\n simp at h1\n refine ⟨?_, hndvd⟩\n have hx0 : (x : ZMod q) ≠ 0 := by\n intro h\n exact hndvd ((CharP.cast_eq_zero_iff (ZMod q) q _).1 h)\n have hx1 : (x : ZMod q) ≠ 1 := by\n intro h\n rw [h] at h1\n have h3 : ((3 : ℕ) : ZMod q) = 0 := by push_cast; linear_combination h1\n have hq3 : q ∣ 3 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n have : q = 3 := (Nat.prime_dvd_prime_iff_eq hq Nat.prime_three).1 hq3\n exact hndvd (this ▸ (Dvd.dvd.trans (by norm_num : 3 ∣ 6) hx))\n have hx3 : (x : ZMod q) ^ 3 = 1 := by\n linear_combination ((x : ZMod q) - 1) * h1\n have hord : orderOf (x : ZMod q) = 3 := orderOf_eq_prime hx3 hx1\n have hdvd : 3 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have hq2 : q ≠ 2 := by\n rintro rfl\n obtain ⟨k, rfl⟩ := hx\n apply absurd hd\n rw [Nat.dvd_iff_mod_eq_zero]\n have : (6 * k) ^ 2 + 6 * k + 1 = 2 * (18 * k ^ 2 + 3 * k) + 1 := by ring\n rw [this]\n omega\n have h2 := hq.two_le\n rcases Nat.even_or_odd q with he | ho\n · exact absurd ((Nat.prime_dvd_prime_iff_eq Nat.prime_two hq).1 (even_iff_two_dvd.1 he)).symm hq2\n · obtain ⟨k, hk⟩ := ho\n omega\n\nend Lemma.P31\n\ntheorem Lemma.primes_mod_3_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 3 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 3).factorial with hxdef\n have hx6 : 6 ∣ x := by\n have : (3 : ℕ).factorial ∣ x := Nat.factorial_dvd_factorial (by omega)\n simpa [Nat.factorial] using this\n have hN : x ^ 2 + x + 1 ≠ 1 := by\n have : 0 < x := Nat.factorial_pos _\n omega\n have hq := Nat.minFac_prime hN\n have hqd := Nat.minFac_dvd (x ^ 2 + x + 1)\n obtain ⟨h6, hnd⟩ := Lemma.P31.key x hx6 _ hq hqd\n refine ⟨_, ⟨hq, by omega⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_3_eq_2":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\ntheorem Lemma.primes_mod_3_eq_2 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 3 = 2} :=\n Set.infinite_of_forall_exists_gt fun n => by\n have hx := (n + 3).factorial_pos\n have H : ∀ q, q.Prime → q ∣ 3 * (n + 3).factorial - 1 → n + 3 < q := fun q hq hd => by\n by_contra h\n refine hq.one_lt.ne' (Nat.dvd_one.1 ((Nat.dvd_add_right hd).1 ?_))\n rw [Nat.sub_add_cancel (by omega)]\n exact (Nat.dvd_factorial hq.pos (by omega)).mul_left 3\n obtain ⟨q, hq, hd, h⟩ := Lemma.EF 3 2 (by norm_num) _\n (by omega : (3 * (n + 3).factorial - 1) % 3 = 2) fun q hq hd => by\n have := H q hq hd\n have : ¬ 3 ∣ q := fun h => by have := hq.eq_one_or_self_of_dvd 3 h; omega\n omega\n exact ⟨q, ⟨hq, h⟩, by have := H q hq hd; omega⟩\n-- U180 cold\n","Lemma.primes_mod_4_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P41\n\ntheorem key (x : ℕ) (hx : 2 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 2 + 1) : q % 4 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two\n have h1 : ((x ^ 2 + 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at h1\n have hndvd : ¬ q ∣ x := by\n intro hqx\n have : (x : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqx\n rw [this] at h1\n simp at h1\n refine ⟨?_, hndvd⟩\n have hx0 : (x : ZMod q) ≠ 0 := by\n intro h\n exact hndvd ((CharP.cast_eq_zero_iff (ZMod q) q _).1 h)\n have hq2 : q ≠ 2 := by\n rintro rfl\n obtain ⟨k, rfl⟩ := hx\n apply absurd hd\n rw [Nat.dvd_iff_mod_eq_zero]\n have : (2 * k) ^ 2 + 1 = 2 * (2 * k ^ 2) + 1 := by ring\n rw [this]\n omega\n have hn : ¬ (x : ZMod q) ^ (2 ^ 1) = 1 := by\n intro h\n have h2 : ((2 : ℕ) : ZMod q) = 0 := by\n push_cast\n have : (x : ZMod q) ^ 2 = 1 := by simpa using h\n linear_combination h1 - this\n have hq2' : q ∣ 2 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h2\n exact hq2 ((Nat.prime_dvd_prime_iff_eq hq Nat.prime_two).1 hq2')\n have h8 : (x : ZMod q) ^ (2 ^ (1 + 1)) = 1 := by\n norm_num\n linear_combination ((x : ZMod q) ^ 2 - 1) * h1\n have hord : orderOf (x : ZMod q) = 2 ^ (1 + 1) := orderOf_eq_prime_pow hn h8\n have hdvd : 2 ^ (1 + 1) ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have h2 := hq.two_le\n norm_num at hdvd\n omega\n\nend Lemma.P41\n\ntheorem Lemma.primes_mod_4_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 4 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 2).factorial with hxdef\n have hx2 : 2 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hN : x ^ 2 + 1 ≠ 1 := by\n have : 0 < x := Nat.factorial_pos _\n have : 0 < x ^ 2 := by positivity\n omega\n have hq := Nat.minFac_prime hN\n have hqd := Nat.minFac_dvd (x ^ 2 + 1)\n obtain ⟨h8, hnd⟩ := Lemma.P41.key x hx2 _ hq hqd\n refine ⟨_, ⟨hq, h8⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_4_eq_3":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\ntheorem Lemma.primes_mod_4_eq_3 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 4 = 3} :=\n Set.infinite_of_forall_exists_gt fun n => by\n have hx := (n + 3).factorial_pos\n have H : ∀ q, q.Prime → q ∣ 4 * (n + 3).factorial - 1 → n + 3 < q := fun q hq hd => by\n by_contra h\n refine hq.one_lt.ne' (Nat.dvd_one.1 ((Nat.dvd_add_right hd).1 ?_))\n rw [Nat.sub_add_cancel (by omega)]\n exact (Nat.dvd_factorial hq.pos (by omega)).mul_left 4\n obtain ⟨q, hq, hd, h⟩ := Lemma.EF 4 3 (by norm_num) _\n (by omega : (4 * (n + 3).factorial - 1) % 4 = 3) fun q hq hd => by\n have := H q hq hd\n have : ¬ 2 ∣ q := fun h => by have := hq.eq_one_or_self_of_dvd 2 h; omega\n omega\n exact ⟨q, ⟨hq, h⟩, by have := H q hq hd; omega⟩\n-- U180 cold\n","Lemma.primes_mod_5_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Q51\n\ntheorem prime_p : Nat.Prime 5 := by decide\n\ntheorem key (x : ℕ) (hx : 5 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 4 + x ^ 3 + x ^ 2 + x + 1) : q % 5 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 5) := Fact.mk prime_p\n have h1 : ((x ^ 4 + x ^ 3 + x ^ 2 + x + 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at h1\n have hndvd : ¬ q ∣ x := by\n intro hqx\n have : (x : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqx\n rw [this] at h1\n simp at h1\n refine ⟨?_, hndvd⟩\n have hx0 : (x : ZMod q) ≠ 0 := by\n intro h\n exact hndvd ((CharP.cast_eq_zero_iff (ZMod q) q _).1 h)\n have hx1 : (x : ZMod q) ≠ 1 := by\n intro h\n rw [h] at h1\n have h3 : ((5 : ℕ) : ZMod q) = 0 := by push_cast; linear_combination h1\n have hq3 : q ∣ 5 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n have : q = 5 := (Nat.prime_dvd_prime_iff_eq hq prime_p).1 hq3\n exact hndvd (this ▸ hx)\n have hx3 : (x : ZMod q) ^ 5 = 1 := by\n linear_combination ((x : ZMod q) - 1) * h1\n have hord : orderOf (x : ZMod q) = 5 := orderOf_eq_prime hx3 hx1\n have hdvd : 5 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have h2 := hq.two_le\n omega\n\nend Lemma.Q51\n\ntheorem Lemma.primes_mod_5_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 5 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 10).factorial with hxdef\n have hx6 : 5 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hN : x ^ 4 + x ^ 3 + x ^ 2 + x + 1 ≠ 1 := by\n have : 0 < x := Nat.factorial_pos _\n omega\n have hq := Nat.minFac_prime hN\n have hqd := Nat.minFac_dvd (x ^ 4 + x ^ 3 + x ^ 2 + x + 1)\n obtain ⟨h6, hnd⟩ := Lemma.Q51.key x hx6 _ hq hqd\n refine ⟨_, ⟨hq, h6⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_5_eq_4":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\nnamespace Lemma.P54\n\ntheorem z5 : (5 : ZMod 5) = 0 := by decide\n\ntheorem nsq2 : ∀ r : ZMod 5, ((2 : ℕ) : ZMod 5) ≠ r * r := by decide\n\ntheorem nsq3 : ∀ r : ZMod 5, ((3 : ℕ) : ZMod 5) ≠ r * r := by decide\n\ntheorem key (y : ℕ) (hy : 2 ∣ y) (hy0 : 0 < y) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ 5 * y ^ 2 - 1) : (q % 5 = 1 ∨ q % 5 = 4) ∧ ¬ q ∣ y := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 5) := Fact.mk Nat.prime_five\n have h1 : ((5 * y ^ 2 - 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n have h5 : 1 ≤ 5 * y ^ 2 := by\n have : 1 ≤ y ^ 2 := Nat.one_le_pow _ _ hy0\n omega\n have h2 : (5 : ZMod q) * (y : ZMod q) ^ 2 = 1 := by\n rw [Nat.cast_sub h5] at h1\n push_cast at h1\n linear_combination h1\n have hndvd : ¬ q ∣ y := by\n intro hqy\n have : (y : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy\n rw [this] at h2\n simp at h2\n refine ⟨?_, hndvd⟩\n have hq2 : q ≠ 2 := by\n rintro rfl\n exact hndvd hy\n have hq5 : q ≠ 5 := by\n rintro rfl\n have : (5 : ZMod 5) = 0 := z5\n rw [this] at h2\n simp at h2\n have hsq : IsSquare ((5 : ℕ) : ZMod q) := ⟨5 * y, by push_cast; linear_combination (-5) * h2⟩\n obtain ⟨r, hr⟩ :=\n (ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one (p := 5) (q := q) (by norm_num) hq2).2 hsq\n rw [← ZMod.natCast_mod q 5] at hr\n have hlt := Nat.mod_lt q (by norm_num : 5 > 0)\n generalize hm : q % 5 = m at hr hlt\n obtain h | h | h | h | h : m = 0 ∨ m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 := by omega\n · subst h\n exact absurd ((Nat.prime_dvd_prime_iff_eq Nat.prime_five hq).1\n (Nat.dvd_of_mod_eq_zero hm)).symm hq5\n · exact Or.inl h\n · subst h\n exact absurd hr (nsq2 r)\n · subst h\n exact absurd hr (nsq3 r)\n · exact Or.inr h\n\nend Lemma.P54\n\ntheorem Lemma.primes_mod_5_eq_4 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 5 = 4} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n have hy2 : 2 ∣ (n + 5).factorial := Nat.dvd_factorial (by norm_num) (by omega)\n have hy0 : 0 < (n + 5).factorial := Nat.factorial_pos _\n have hN : (5 * (n + 5).factorial ^ 2 - 1) % 5 = 4 := by\n have : 1 ≤ (n + 5).factorial ^ 2 := Nat.one_le_pow _ _ hy0\n omega\n obtain ⟨q, hq, hqd, hq4⟩ := Lemma.EF 5 4 (by norm_num) _ hN\n (fun q hq hd => (Lemma.P54.key _ hy2 hy0 q hq hd).1)\n refine ⟨q, ⟨hq, hq4⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P54.key _ hy2 hy0 q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_6_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P61\n\ntheorem key (x : ℕ) (hx : 6 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 2 + x + 1) : q % 6 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 3) := Fact.mk Nat.prime_three\n have h1 : ((x ^ 2 + x + 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at h1\n have hndvd : ¬ q ∣ x := by\n intro hqx\n have : (x : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqx\n rw [this] at h1\n simp at h1\n refine ⟨?_, hndvd⟩\n have hx0 : (x : ZMod q) ≠ 0 := by\n intro h\n exact hndvd ((CharP.cast_eq_zero_iff (ZMod q) q _).1 h)\n have hx1 : (x : ZMod q) ≠ 1 := by\n intro h\n rw [h] at h1\n have h3 : ((3 : ℕ) : ZMod q) = 0 := by push_cast; linear_combination h1\n have hq3 : q ∣ 3 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n have : q = 3 := (Nat.prime_dvd_prime_iff_eq hq Nat.prime_three).1 hq3\n exact hndvd (this ▸ (Dvd.dvd.trans (by norm_num : 3 ∣ 6) hx))\n have hx3 : (x : ZMod q) ^ 3 = 1 := by\n linear_combination ((x : ZMod q) - 1) * h1\n have hord : orderOf (x : ZMod q) = 3 := orderOf_eq_prime hx3 hx1\n have hdvd : 3 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have hq2 : q ≠ 2 := by\n rintro rfl\n obtain ⟨k, rfl⟩ := hx\n apply absurd hd\n rw [Nat.dvd_iff_mod_eq_zero]\n have : (6 * k) ^ 2 + 6 * k + 1 = 2 * (18 * k ^ 2 + 3 * k) + 1 := by ring\n rw [this]\n omega\n have h2 := hq.two_le\n rcases Nat.even_or_odd q with he | ho\n · exact absurd ((Nat.prime_dvd_prime_iff_eq Nat.prime_two hq).1 (even_iff_two_dvd.1 he)).symm hq2\n · obtain ⟨k, hk⟩ := ho\n omega\n\nend Lemma.P61\n\ntheorem Lemma.primes_mod_6_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 6 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 3).factorial with hxdef\n have hx6 : 6 ∣ x := by\n have : (3 : ℕ).factorial ∣ x := Nat.factorial_dvd_factorial (by omega)\n simpa [Nat.factorial] using this\n have hN : x ^ 2 + x + 1 ≠ 1 := by\n have : 0 < x := Nat.factorial_pos _\n omega\n have hq := Nat.minFac_prime hN\n have hqd := Nat.minFac_dvd (x ^ 2 + x + 1)\n obtain ⟨h6, hnd⟩ := Lemma.P61.key x hx6 _ hq hqd\n refine ⟨_, ⟨hq, h6⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_6_eq_5":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\ntheorem Lemma.primes_mod_6_eq_5 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 6 = 5} :=\n Set.infinite_of_forall_exists_gt fun n => by\n have hx := (n + 3).factorial_pos\n have H : ∀ q, q.Prime → q ∣ 6 * (n + 3).factorial - 1 → n + 3 < q := fun q hq hd => by\n by_contra h\n refine hq.one_lt.ne' (Nat.dvd_one.1 ((Nat.dvd_add_right hd).1 ?_))\n rw [Nat.sub_add_cancel (by omega)]\n exact (Nat.dvd_factorial hq.pos (by omega)).mul_left 6\n obtain ⟨q, hq, hd, h⟩ := Lemma.EF 6 5 (by norm_num) _\n (by omega : (6 * (n + 3).factorial - 1) % 6 = 5) fun q hq hd => by\n have := H q hq hd\n have : ¬ 2 ∣ q := fun h => by have := hq.eq_one_or_self_of_dvd 2 h; omega\n have : ¬ 3 ∣ q := fun h => by have := hq.eq_one_or_self_of_dvd 3 h; omega\n omega\n exact ⟨q, ⟨hq, h⟩, by have := H q hq hd; omega⟩\n-- U180 cold\n","Lemma.primes_mod_7_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Q71\n\ntheorem prime_p : Nat.Prime 7 := by decide\n\ntheorem key (x : ℕ) (hx : 7 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 6 + x ^ 5 + x ^ 4 + x ^ 3 + x ^ 2 + x + 1) : q % 7 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 7) := Fact.mk prime_p\n have h1 : ((x ^ 6 + x ^ 5 + x ^ 4 + x ^ 3 + x ^ 2 + x + 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at h1\n have hndvd : ¬ q ∣ x := by\n intro hqx\n have : (x : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqx\n rw [this] at h1\n simp at h1\n refine ⟨?_, hndvd⟩\n have hx0 : (x : ZMod q) ≠ 0 := by\n intro h\n exact hndvd ((CharP.cast_eq_zero_iff (ZMod q) q _).1 h)\n have hx1 : (x : ZMod q) ≠ 1 := by\n intro h\n rw [h] at h1\n have h3 : ((7 : ℕ) : ZMod q) = 0 := by push_cast; linear_combination h1\n have hq3 : q ∣ 7 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n have : q = 7 := (Nat.prime_dvd_prime_iff_eq hq prime_p).1 hq3\n exact hndvd (this ▸ hx)\n have hx3 : (x : ZMod q) ^ 7 = 1 := by\n linear_combination ((x : ZMod q) - 1) * h1\n have hord : orderOf (x : ZMod q) = 7 := orderOf_eq_prime hx3 hx1\n have hdvd : 7 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have h2 := hq.two_le\n omega\n\nend Lemma.Q71\n\ntheorem Lemma.primes_mod_7_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 7 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 14).factorial with hxdef\n have hx6 : 7 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hN : x ^ 6 + x ^ 5 + x ^ 4 + x ^ 3 + x ^ 2 + x + 1 ≠ 1 := by\n have : 0 < x := Nat.factorial_pos _\n omega\n have hq := Nat.minFac_prime hN\n have hqd := Nat.minFac_dvd (x ^ 6 + x ^ 5 + x ^ 4 + x ^ 3 + x ^ 2 + x + 1)\n obtain ⟨h6, hnd⟩ := Lemma.Q71.key x hx6 _ hq hqd\n refine ⟨_, ⟨hq, h6⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_7_eq_6":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\nnamespace Lemma.P76\n\nopen Polynomial\n\ntheorem prime7 : Nat.Prime 7 := by decide\n\ntheorem key (q : ℕ) (hq : q.Prime) (hq7 : q ≠ 7) (t : ZMod q)\n (ht : t ^ 3 + t ^ 2 - 2 * t - 1 = 0) : q % 7 = 1 ∨ q % 7 = 6 := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 7) := Fact.mk prime7\n set p : (ZMod q)[X] := X ^ 2 - C t * X + 1 with hpdef\n have hp : p.natDegree = 2 := by rw [hpdef]; compute_degree!\n have hpu : ¬ IsUnit p := by\n intro h\n have := Polynomial.natDegree_eq_zero_of_isUnit h\n omega\n have hp0 : p ≠ 0 := by\n intro h\n rw [h] at hp\n simp at hp\n obtain ⟨g, hg, hgp⟩ := WfDvdMonoid.exists_irreducible_factor hpu hp0\n haveI := Fact.mk hg\n let K := AdjoinRoot g\n let r : K := AdjoinRoot.root g\n have hr0 : aeval r p = 0 := by\n obtain ⟨c, hc⟩ := hgp\n rw [hc, map_mul, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self, zero_mul]\n set T : K := algebraMap (ZMod q) K t with hTdef\n have hr : r ^ 2 - T * r + 1 = 0 := by\n rw [hpdef] at hr0\n simpa [hTdef] using hr0\n haveI : CharP K q := charP_of_injective_algebraMap (algebraMap (ZMod q) K).injective q\n have hT : T ^ 3 + T ^ 2 - 2 * T - 1 = 0 := by\n have := congrArg (algebraMap (ZMod q) K) ht\n simpa [hTdef, map_ofNat] using this\n have hTq : T ^ q = T := by rw [hTdef, ← map_pow, ZMod.pow_card]\n have hr7 : r ^ 7 = 1 := by\n linear_combination (r - 1) * (r ^ 3 * hT + (1 + r + r * T + r ^ 2 * T + r ^ 2 * T ^ 2\n + r ^ 3 + r ^ 3 * T + r ^ 4) * hr)\n have hr1 : r ≠ 1 := by\n intro h1\n rw [h1] at hr\n have hT2 : T = 2 := by linear_combination -hr\n rw [hT2] at hT\n have h7 : ((7 : ℕ) : K) = 0 := by push_cast; linear_combination hT\n have hq7' : q ∣ 7 := (CharP.cast_eq_zero_iff K q 7).1 h7\n exact hq7 ((Nat.prime_dvd_prime_iff_eq hq prime7).1 hq7')\n have hrne : r ≠ 0 := by\n intro h0\n rw [h0] at hr\n simp at hr\n have hrq : (r ^ q) ^ 2 - T * r ^ q + 1 = 0 := by\n have : (r ^ 2 - T * r + 1) ^ q = 0 := by rw [hr, zero_pow hq.ne_zero]\n rw [add_pow_char, sub_pow_char, mul_pow, hTq, one_pow] at this\n rw [← this]\n ring\n have hprod : (r ^ q - r) * (r ^ q - (T - r)) = 0 := by linear_combination hrq - hr\n have hord : orderOf r = 7 := orderOf_eq_prime hr7 hr1\n have hq2 := hq.two_le\n rcases mul_eq_zero.1 hprod with h | h\n · have h' : r ^ (q - 1) = 1 := by\n have e : r ^ q = r ^ (q - 1) * r := by\n rw [← pow_succ]; congr 1; omega\n have : (r ^ (q - 1) - 1) * r = 0 := by linear_combination e.symm.trans (sub_eq_zero.1 h)\n rcases mul_eq_zero.1 this with h2 | h2\n · exact sub_eq_zero.1 h2\n · exact absurd h2 hrne\n have := orderOf_dvd_of_pow_eq_one h'\n rw [hord] at this\n omega\n · have h' : r ^ (q + 1) = 1 := by\n rw [pow_succ, sub_eq_zero.1 h]\n linear_combination -hr\n have := orderOf_dvd_of_pow_eq_one h'\n rw [hord] at this\n omega\n\ntheorem exists_factor (N : ℕ) (hN : N % 7 = 6)\n (hall : ∀ q, q.Prime → q ∣ N → q % 7 = 1 ∨ q % 7 = 6) :\n ∃ q, q.Prime ∧ q % 7 = 6 ∧ q ∣ N :=\n let ⟨q, h1, h2, h3⟩ := Lemma.EF 7 6 (by norm_num) N hN hall\n ⟨q, h1, h3, h2⟩\n\nend Lemma.P76\n\ntheorem Lemma.primes_mod_7_eq_6 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 7 = 6} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set y := (n + 7).factorial with hydef\n have hy0 : 0 < y := Nat.factorial_pos _\n set x := 7 * y with hxdef\n have hle : 2 * x + 1 ≤ x ^ 3 + x ^ 2 := by\n have : 7 ≤ x := by omega\n nlinarith\n set N := x ^ 3 + x ^ 2 - (2 * x + 1) with hNdef\n have hN : N + (2 * x + 1) = x ^ 3 + x ^ 2 := Nat.sub_add_cancel hle\n have hN' : N + (14 * y + 1) = 343 * y ^ 3 + 49 * y ^ 2 := by\n rw [hxdef] at hN; linarith [hN]\n have hN7 : N % 7 = 6 := by\n generalize y ^ 3 = a at hN'\n generalize y ^ 2 = b at hN'\n omega\n have hfac : ∀ q, q.Prime → q ∣ N → (q % 7 = 1 ∨ q % 7 = 6) ∧ ¬ q ∣ y := by\n intro q hq hqN\n haveI := Fact.mk hq\n have hc : ((N : ℕ) : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqN\n have hc2 : ((N + (2 * x + 1) : ℕ) : ZMod q) = ((x ^ 3 + x ^ 2 : ℕ) : ZMod q) := by rw [hN]\n push_cast at hc2\n rw [hc] at hc2\n have hf : (x : ZMod q) ^ 3 + (x : ZMod q) ^ 2 - 2 * (x : ZMod q) - 1 = 0 := by\n linear_combination -hc2\n have hny : ¬ q ∣ y := by\n intro hqy\n have : (x : ZMod q) = 0 := by\n rw [hxdef]; push_cast\n rw [(CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy, mul_zero]\n rw [this] at hf\n norm_num at hf\n refine ⟨Lemma.P76.key q hq ?_ _ hf, hny⟩\n rintro rfl\n omega\n obtain ⟨q, hq, h6, hqd⟩ := Lemma.P76.exists_factor N hN7 (fun q hq hd => (hfac q hq hd).1)\n refine ⟨q, ⟨hq, h6⟩, ?_⟩\n by_contra hle'\n push_neg at hle'\n exact (hfac q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_8_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P81\n\ntheorem key (x : ℕ) (hx : 2 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 4 + 1) : q % 8 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two\n have h1 : ((x ^ 4 + 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at h1\n have hndvd : ¬ q ∣ x := by\n intro hqx\n have : (x : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqx\n rw [this] at h1\n simp at h1\n refine ⟨?_, hndvd⟩\n have hx0 : (x : ZMod q) ≠ 0 := by\n intro h\n exact hndvd ((CharP.cast_eq_zero_iff (ZMod q) q _).1 h)\n have hq2 : q ≠ 2 := by\n rintro rfl\n obtain ⟨k, rfl⟩ := hx\n apply absurd hd\n rw [Nat.dvd_iff_mod_eq_zero]\n have : (2 * k) ^ 4 + 1 = 2 * (8 * k ^ 4) + 1 := by ring\n rw [this]\n omega\n have hn : ¬ (x : ZMod q) ^ (2 ^ 2) = 1 := by\n intro h\n have h2 : ((2 : ℕ) : ZMod q) = 0 := by\n push_cast\n have : (x : ZMod q) ^ 4 = 1 := by simpa using h\n linear_combination h1 - this\n have hq2' : q ∣ 2 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h2\n exact hq2 ((Nat.prime_dvd_prime_iff_eq hq Nat.prime_two).1 hq2')\n have h8 : (x : ZMod q) ^ (2 ^ (2 + 1)) = 1 := by\n norm_num\n linear_combination ((x : ZMod q) ^ 4 - 1) * h1\n have hord : orderOf (x : ZMod q) = 2 ^ (2 + 1) := orderOf_eq_prime_pow hn h8\n have hdvd : 2 ^ (2 + 1) ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have h2 := hq.two_le\n norm_num at hdvd\n omega\n\nend Lemma.P81\n\ntheorem Lemma.primes_mod_8_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 8 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 2).factorial with hxdef\n have hx2 : 2 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hN : x ^ 4 + 1 ≠ 1 := by\n have : 0 < x := Nat.factorial_pos _\n have : 0 < x ^ 4 := by positivity\n omega\n have hq := Nat.minFac_prime hN\n have hqd := Nat.minFac_dvd (x ^ 4 + 1)\n obtain ⟨h8, hnd⟩ := Lemma.P81.key x hx2 _ hq hqd\n refine ⟨_, ⟨hq, h8⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_8_eq_3":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\nnamespace Lemma.P83\n\ndef Q (n : ℕ) : ℕ := ∏ i ∈ Finset.range n, (2 * i + 1)\n\ntheorem Q_odd (n : ℕ) : Q n % 2 = 1 := by\n unfold Q\n apply Finset.prod_induction _ (fun x => x % 2 = 1)\n · intro a b ha hb; rw [Nat.mul_mod, ha, hb]\n · rfl\n · intro i _; omega\n\ntheorem Q_pos (n : ℕ) : 0 < Q n := by have := Q_odd n; omega\n\ntheorem Q_sq (n : ℕ) : Q n ^ 2 % 8 = 1 := by\n have h := Q_odd n\n have h8 : Q n % 8 = 1 ∨ Q n % 8 = 3 ∨ Q n % 8 = 5 ∨ Q n % 8 = 7 := by omega\n rw [Nat.pow_mod]\n rcases h8 with h8 | h8 | h8 | h8 <;> rw [h8]\n\ntheorem dvd_Q (n q : ℕ) (hq : q % 2 = 1) (hle : q ≤ n) : q ∣ Q n := by\n unfold Q\n have hmem : q / 2 ∈ Finset.range n := Finset.mem_range.2 (by omega)\n have := Finset.dvd_prod_of_mem (fun i => 2 * i + 1) hmem\n have he : 2 * (q / 2) + 1 = q := by omega\n simpa [he] using this\n\ntheorem key (n q : ℕ) (hq : q.Prime) (hd : q ∣ Q n ^ 2 + 2) :\n (q % 8 = 1 ∨ q % 8 = 3) ∧ ¬ q ∣ Q n := by\n haveI := Fact.mk hq\n have h2 : ((Q n : ℕ) : ZMod q) ^ 2 + 2 = 0 := by\n have := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at this\n exact this\n have hq2 : q ≠ 2 := by\n rintro rfl\n have h := Q_sq n\n have : (Q n ^ 2 + 2) % 2 = 0 := Nat.mod_eq_zero_of_dvd hd\n omega\n have hndvd : ¬ q ∣ Q n := by\n intro hqy\n have hq2' : q ∣ 2 := (Nat.dvd_add_right (dvd_pow hqy two_ne_zero)).1 hd\n exact hq2 ((Nat.prime_dvd_prime_iff_eq hq Nat.prime_two).1 hq2')\n refine ⟨?_, hndvd⟩\n have hsq : IsSquare (-2 : ZMod q) := ⟨(Q n : ZMod q), by linear_combination (-1) * h2⟩\n exact (ZMod.exists_sq_eq_neg_two_iff hq2).1 hsq\n\nend Lemma.P83\n\ntheorem Lemma.primes_mod_8_eq_3 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 8 = 3} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n have hN : (Lemma.P83.Q n ^ 2 + 2) % 8 = 3 := by\n have := Lemma.P83.Q_sq n\n omega\n obtain ⟨q, hq, hqd, hq4⟩ := Lemma.EF 8 3 (by norm_num) _ hN\n (fun q hq hd => (Lemma.P83.key n q hq hd).1)\n refine ⟨q, ⟨hq, hq4⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P83.key n q hq hqd).2 (Lemma.P83.dvd_Q n q (by omega) hle)\n-- U180 cold\n","Lemma.primes_mod_8_eq_5":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\nnamespace Lemma.P85\n\ndef Q (n : ℕ) : ℕ := ∏ i ∈ Finset.range n, (2 * i + 1)\n\ntheorem Q_odd (n : ℕ) : Q n % 2 = 1 := by\n unfold Q\n apply Finset.prod_induction _ (fun x => x % 2 = 1)\n · intro a b ha hb; rw [Nat.mul_mod, ha, hb]\n · rfl\n · intro i _; omega\n\ntheorem Q_pos (n : ℕ) : 0 < Q n := by have := Q_odd n; omega\n\ntheorem Q_sq (n : ℕ) : Q n ^ 2 % 8 = 1 := by\n have h := Q_odd n\n have h8 : Q n % 8 = 1 ∨ Q n % 8 = 3 ∨ Q n % 8 = 5 ∨ Q n % 8 = 7 := by omega\n rw [Nat.pow_mod]\n rcases h8 with h8 | h8 | h8 | h8 <;> rw [h8]\n\ntheorem dvd_Q (n q : ℕ) (hq : q % 2 = 1) (hle : q ≤ n) : q ∣ Q n := by\n unfold Q\n have hmem : q / 2 ∈ Finset.range n := Finset.mem_range.2 (by omega)\n have := Finset.dvd_prod_of_mem (fun i => 2 * i + 1) hmem\n have he : 2 * (q / 2) + 1 = q := by omega\n simpa [he] using this\n\ntheorem key (n q : ℕ) (hq : q.Prime) (hd : q ∣ 4 * Q n ^ 2 + 1) :\n (q % 8 = 1 ∨ q % 8 = 5) ∧ ¬ q ∣ Q n := by\n haveI := Fact.mk hq\n have h2 : 4 * ((Q n : ℕ) : ZMod q) ^ 2 + 1 = 0 := by\n have := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at this\n exact this\n have hq2 : q ≠ 2 := by\n rintro rfl\n have : (4 * Q n ^ 2 + 1) % 2 = 0 := Nat.mod_eq_zero_of_dvd hd\n omega\n have hndvd : ¬ q ∣ Q n := by\n intro hqy\n have : ((Q n : ℕ) : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy\n rw [this] at h2\n simp at h2\n refine ⟨?_, hndvd⟩\n have hsq : IsSquare (-1 : ZMod q) := ⟨2 * (Q n : ZMod q), by linear_combination (-1) * h2⟩\n have h4 := (ZMod.exists_sq_eq_neg_one_iff (p := q)).1 hsq\n have hodd := hq.eq_two_or_odd\n omega\n\nend Lemma.P85\n\ntheorem Lemma.primes_mod_8_eq_5 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 8 = 5} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n have hN : (4 * Lemma.P85.Q n ^ 2 + 1) % 8 = 5 := by\n have := Lemma.P85.Q_sq n\n omega\n obtain ⟨q, hq, hqd, hq4⟩ := Lemma.EF 8 5 (by norm_num) _ hN\n (fun q hq hd => (Lemma.P85.key n q hq hd).1)\n refine ⟨q, ⟨hq, hq4⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P85.key n q hq hqd).2 (Lemma.P85.dvd_Q n q (by omega) hle)\n-- U180 cold\n","Lemma.primes_mod_8_eq_7":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\nnamespace Lemma.P87\n\ntheorem key (y : ℕ) (hy : 2 ∣ y) (hy0 : 0 < y) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ 2 * y ^ 2 - 1) : (q % 8 = 1 ∨ q % 8 = 7) ∧ ¬ q ∣ y := by\n haveI := Fact.mk hq\n have h1 : ((2 * y ^ 2 - 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n have h5 : 1 ≤ 2 * y ^ 2 := by\n have : 1 ≤ y ^ 2 := Nat.one_le_pow _ _ hy0\n omega\n have h2 : (2 : ZMod q) * (y : ZMod q) ^ 2 = 1 := by\n rw [Nat.cast_sub h5] at h1\n push_cast at h1\n linear_combination h1\n have hndvd : ¬ q ∣ y := by\n intro hqy\n have : (y : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy\n rw [this] at h2\n simp at h2\n refine ⟨?_, hndvd⟩\n have hq2 : q ≠ 2 := by\n rintro rfl\n exact hndvd hy\n have hsq : IsSquare (2 : ZMod q) := ⟨2 * y, by linear_combination (-2) * h2⟩\n exact (ZMod.exists_sq_eq_two_iff hq2).1 hsq\n\nend Lemma.P87\n\ntheorem Lemma.primes_mod_8_eq_7 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 8 = 7} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n have hy2 : 2 ∣ (n + 3).factorial := Nat.dvd_factorial (by norm_num) (by omega)\n have hy0 : 0 < (n + 3).factorial := Nat.factorial_pos _\n have hN : (2 * (n + 3).factorial ^ 2 - 1) % 8 = 7 := by\n obtain ⟨k, hk⟩ := hy2\n have hz : (n + 3).factorial ^ 2 = 4 * k ^ 2 := by rw [hk]; ring\n have : 1 ≤ (n + 3).factorial ^ 2 := Nat.one_le_pow _ _ hy0\n rw [hz] at this ⊢\n omega\n obtain ⟨q, hq, hqd, hq4⟩ := Lemma.EF 8 7 (by norm_num) _ hN\n (fun q hq hd => (Lemma.P87.key _ hy2 hy0 q hq hd).1)\n refine ⟨q, ⟨hq, hq4⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P87.key _ hy2 hy0 q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_9_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P91\n\ntheorem prime3 : Nat.Prime 3 := by decide\n\ntheorem key (x : ℕ) (hx : 3 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 6 + x ^ 3 + 1) : q % 9 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 3) := Fact.mk prime3\n have h1 : ((x ^ 6 + x ^ 3 + 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at h1\n have hndvd : ¬ q ∣ x := by\n intro hqx\n have : (x : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqx\n rw [this] at h1\n simp at h1\n refine ⟨?_, hndvd⟩\n have hx0 : (x : ZMod q) ≠ 0 := by\n intro h\n exact hndvd ((CharP.cast_eq_zero_iff (ZMod q) q _).1 h)\n have hq3 : q ≠ 3 := by\n rintro rfl\n exact hndvd hx\n have hn : ¬ (x : ZMod q) ^ (3 ^ 1) = 1 := by\n intro h\n have h3 : ((3 : ℕ) : ZMod q) = 0 := by\n push_cast\n have : (x : ZMod q) ^ 3 = 1 := by simpa using h\n linear_combination h1 - ((x : ZMod q) ^ 3 + 2) * this\n have hq3' : q ∣ 3 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n exact hq3 ((Nat.prime_dvd_prime_iff_eq hq prime3).1 hq3')\n have h9 : (x : ZMod q) ^ (3 ^ (1 + 1)) = 1 := by\n norm_num\n linear_combination ((x : ZMod q) ^ 3 - 1) * h1\n have hord : orderOf (x : ZMod q) = 3 ^ (1 + 1) := orderOf_eq_prime_pow hn h9\n have hdvd : 3 ^ (1 + 1) ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have h2 := hq.two_le\n norm_num at hdvd\n omega\n\nend Lemma.P91\n\ntheorem Lemma.primes_mod_9_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 9 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 3).factorial with hxdef\n have hx3 : 3 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hN : x ^ 6 + x ^ 3 + 1 ≠ 1 := by\n have : 0 < x := Nat.factorial_pos _\n have : 0 < x ^ 3 := by positivity\n omega\n have hq := Nat.minFac_prime hN\n have hqd := Nat.minFac_dvd (x ^ 6 + x ^ 3 + 1)\n obtain ⟨h9, hnd⟩ := Lemma.P91.key x hx3 _ hq hqd\n refine ⟨_, ⟨hq, h9⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_9_eq_8":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n induction N using Nat.strong_induction_on with | _ N ih =>\n obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n rcases h q hq (dvd_mul_right q k) with h1 | h1\n · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n exact ⟨p, hp, d.mul_left q, e⟩\n · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\nnamespace Lemma.P98\n\nopen Polynomial\n\ntheorem prime3 : Nat.Prime 3 := by decide\n\ntheorem key (q : ℕ) (hq : q.Prime) (hq3 : q ≠ 3) (t : ZMod q)\n (ht : t ^ 3 - 3 * t + 1 = 0) : q % 9 = 1 ∨ q % 9 = 8 := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 3) := Fact.mk prime3\n set p : (ZMod q)[X] := X ^ 2 - C t * X + 1 with hpdef\n have hp : p.natDegree = 2 := by rw [hpdef]; compute_degree!\n have hpu : ¬ IsUnit p := by\n intro h\n have := Polynomial.natDegree_eq_zero_of_isUnit h\n omega\n have hp0 : p ≠ 0 := by\n intro h\n rw [h] at hp\n simp at hp\n obtain ⟨g, hg, hgp⟩ := WfDvdMonoid.exists_irreducible_factor hpu hp0\n haveI := Fact.mk hg\n let K := AdjoinRoot g\n let r : K := AdjoinRoot.root g\n have hr0 : aeval r p = 0 := by\n obtain ⟨c, hc⟩ := hgp\n rw [hc, map_mul, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self, zero_mul]\n set T : K := algebraMap (ZMod q) K t with hTdef\n have hr : r ^ 2 - T * r + 1 = 0 := by\n rw [hpdef] at hr0\n simpa [hTdef] using hr0\n haveI : CharP K q := charP_of_injective_algebraMap (algebraMap (ZMod q) K).injective q\n have hT : T ^ 3 - 3 * T + 1 = 0 := by\n have := congrArg (algebraMap (ZMod q) K) ht\n simpa [hTdef, map_ofNat] using this\n have hTq : T ^ q = T := by rw [hTdef, ← map_pow, ZMod.pow_card]\n have hphi : r ^ 6 + r ^ 3 + 1 = 0 := by\n linear_combination r ^ 3 * hT\n + (1 + r * T - r ^ 2 + r ^ 2 * T ^ 2 + r ^ 3 * T + r ^ 4) * hr\n have hr9 : r ^ 9 = 1 := by\n linear_combination (r ^ 3 - 1) * hphi\n have hr3 : ¬ r ^ (3 ^ 1) = 1 := by\n intro h3\n have h3' : r ^ 3 = 1 := by simpa using h3\n have h3K : ((3 : ℕ) : K) = 0 := by\n push_cast\n linear_combination hphi - (r ^ 3 + 2) * h3'\n have hq3' : q ∣ 3 := (CharP.cast_eq_zero_iff K q 3).1 h3K\n exact hq3 ((Nat.prime_dvd_prime_iff_eq hq prime3).1 hq3')\n have hr9' : r ^ (3 ^ (1 + 1)) = 1 := by norm_num; exact hr9\n have hord0 : orderOf r = 3 ^ (1 + 1) := orderOf_eq_prime_pow hr3 hr9'\n have hord : orderOf r = 9 := by rw [hord0]; norm_num\n have hrne : r ≠ 0 := by\n intro h0\n rw [h0] at hr\n simp at hr\n have hrq : (r ^ q) ^ 2 - T * r ^ q + 1 = 0 := by\n have : (r ^ 2 - T * r + 1) ^ q = 0 := by rw [hr, zero_pow hq.ne_zero]\n rw [add_pow_char, sub_pow_char, mul_pow, hTq, one_pow] at this\n rw [← this]\n ring\n have hprod : (r ^ q - r) * (r ^ q - (T - r)) = 0 := by linear_combination hrq - hr\n have hq2 := hq.two_le\n rcases mul_eq_zero.1 hprod with h | h\n · have h' : r ^ (q - 1) = 1 := by\n have e : r ^ q = r ^ (q - 1) * r := by\n rw [← pow_succ]; congr 1; omega\n have : (r ^ (q - 1) - 1) * r = 0 := by linear_combination e.symm.trans (sub_eq_zero.1 h)\n rcases mul_eq_zero.1 this with h2 | h2\n · exact sub_eq_zero.1 h2\n · exact absurd h2 hrne\n have := orderOf_dvd_of_pow_eq_one h'\n rw [hord] at this\n omega\n · have h' : r ^ (q + 1) = 1 := by\n rw [pow_succ, sub_eq_zero.1 h]\n linear_combination -hr\n have := orderOf_dvd_of_pow_eq_one h'\n rw [hord] at this\n omega\n\ntheorem exists_factor (N : ℕ) (hN : N % 9 = 8)\n (hall : ∀ q, q.Prime → q ∣ N → q % 9 = 1 ∨ q % 9 = 8) :\n ∃ q, q.Prime ∧ q % 9 = 8 ∧ q ∣ N :=\n let ⟨q, h1, h2, h3⟩ := Lemma.EF 9 8 (by norm_num) N hN hall\n ⟨q, h1, h3, h2⟩\n\nend Lemma.P98\n\ntheorem Lemma.primes_mod_9_eq_8 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 9 = 8} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set y := (n + 9).factorial with hydef\n have hy0 : 0 < y := Nat.factorial_pos _\n set x := 9 * y with hxdef\n have hle : 3 * x + 1 ≤ x ^ 3 := by\n have hx : 9 ≤ x := by omega\n have e3 : x ^ 3 = x ^ 2 * x := by ring\n have e2 : x ^ 2 = x * x := by ring\n have h2 : x * 9 ≤ x * x := Nat.mul_le_mul_left _ hx\n have h3 : x ^ 2 * 9 ≤ x ^ 2 * x := Nat.mul_le_mul_left _ hx\n nlinarith\n set N := x ^ 3 - (3 * x + 1) with hNdef\n have hN : N + (3 * x + 1) = x ^ 3 := Nat.sub_add_cancel hle\n have hN' : N + (27 * y + 1) = 729 * y ^ 3 := by\n rw [hxdef] at hN; linarith [hN]\n have hN9 : N % 9 = 8 := by\n generalize y ^ 3 = a at hN'\n omega\n have hfac : ∀ q, q.Prime → q ∣ N → (q % 9 = 1 ∨ q % 9 = 8) ∧ ¬ q ∣ y := by\n intro q hq hqN\n haveI := Fact.mk hq\n have hc : ((N : ℕ) : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqN\n have hc2 : ((N + (3 * x + 1) : ℕ) : ZMod q) = ((x ^ 3 : ℕ) : ZMod q) := by rw [hN]\n push_cast at hc2\n rw [hc] at hc2\n have hf : (-(x : ZMod q)) ^ 3 - 3 * (-(x : ZMod q)) + 1 = 0 := by\n linear_combination hc2\n have hny : ¬ q ∣ y := by\n intro hqy\n have : (x : ZMod q) = 0 := by\n rw [hxdef]; push_cast\n rw [(CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy, mul_zero]\n rw [this] at hf\n norm_num at hf\n refine ⟨Lemma.P98.key q hq ?_ _ hf, hny⟩\n rintro rfl\n have := Nat.mod_eq_zero_of_dvd hqN\n omega\n obtain ⟨q, hq, h8, hqd⟩ := Lemma.P98.exists_factor N hN9 (fun q hq hd => (hfac q hq hd).1)\n refine ⟨q, ⟨hq, h8⟩, ?_⟩\n by_contra hle'\n push_neg at hle'\n exact (hfac q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n"}},"flags":[],"id":132,"lab_check":false,"label":"no-improvement","measured":24.0,"reason":null,"score":24.0,"significance":[],"status":"verified","verdicts":[{"audit":true,"lab":true,"measured":24.0,"node":3,"seed":0}]},"entry":{"body":"All 12 \"−1 Euclid / quadratic-character\" files (3_2, 4_3, 5_4, 6_5, 8_3, 8_5, 8_7, 10_9, 12_5, 12_7, 12_11, and the induction step of 7_6/9_8/11_10) share one strong-induction step, and it can be stated once. The generic lemma would be: for N ≥ 2 with N % m = a, where every prime factor q of N has q % m ∈ {1, a} and a ≠ 1, some prime factor of N has q % m = a. Combined with the Cyc port (chat 145) and RC.frob (chat 143), all 24 files then become thin instances, and the total proof text shrinks by ≥40% compared with the best.json set while all 24 still check valid.\nMethod: (1) Minutes 0–5: load the 24 verified texts from best.json and record the total character count (the baseline). (2) Minutes 5–20: prove `Lemma.Euc.exists_factor (m a N : ℕ) (hm : 2 ≤ m) (ha : a ≠ 1) (hN : N % m = a) (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a`. Use strong induction on N through minFac and N/minFac, with Nat.mul_mod and omega, which avoids interval_cases. (3) Minutes 20–45: rewrite each −1/quadratic file so it gives only the specific N, the factor-class fact and q>n, then calls exists_factor. Paste the Cyc port (chat 145) into the ≡1 files and RC.frob (chat 143) into 7_6/9_8/11_10. (4) Run one check_candidate on all 24. Record the new total character count and one cold wall time (cache-busted by a trailing comment). Submit once if 24 are valid. Post the size ratio and the cold time to chat. Pre-declared: success means 24 valid and total size ≤60% of the baseline. If the generic lemma does not compile by minute 20, stop and post the blocker.\nThreshold: 24 (must reach). Result 24; verified by node #3.\nSubmitter notes (data): U180: 24/24 valid. Generic Lemma.EF (m a) (1