{"claim":{"assessments":[],"bundle":{"code":"","commit":"63189c7c0f31aa19dde11bdf6c2417b72357283e","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.Cyc\n\nopen Polynomial Nat\n\ntheorem exists_prime_gt_modEq_one' (k n : ℕ) (hk1 : 1 < k) :\n ∃ p : ℕ, p.Prime ∧ n < p ∧ p % k = 1 := by\n have hk0 : k ≠ 0 := by omega\n let b := k * n.factorial\n have hgt : 1 < (eval (b : ℤ) (cyclotomic k ℤ)).natAbs := by\n rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩\n have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos\n calc\n 1 ≤ b - 1 := Nat.le_sub_one_of_lt hb\n _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=\n sub_one_lt_natAbs_cyclotomic_eval hk1 (Nat.succ_le_iff.1 hb).ne'\n let p := minFac (eval (b : ℤ) (cyclotomic k ℤ)).natAbs\n haveI hprime : Fact p.Prime := ⟨minFac_prime (Nat.ne_of_lt hgt).symm⟩\n have h0 : ((eval (b : ℤ) (cyclotomic k ℤ) : ℤ) : ZMod p) = 0 := by\n rw [ZMod.intCast_zmod_eq_zero_iff_dvd]\n exact Int.ofNat_dvd_left.2 (minFac_dvd _)\n have hroot : IsRoot (cyclotomic k (ZMod p)) (b : ZMod p) := by\n have : ((b : ℤ) : ZMod p) = (b : ZMod p) := by push_cast; rfl\n rw [IsRoot.def, ← this, ← map_cyclotomic_int k (ZMod p), eval_intCast_map]\n exact h0\n have hpb : ¬p ∣ b := by\n intro hd\n have hb0 : (b : ZMod p) = 0 := (CharP.cast_eq_zero_iff (ZMod p) p b).2 hd\n have := hroot\n rw [IsRoot.def, hb0, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hk1] at this\n exact one_ne_zero this\n refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩\n · exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)\n · have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=\n ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)\n haveI : NeZero (k : ZMod p) :=\n NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)\n have : k = orderOf (b : ZMod p) := by\n have := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf\n simpa using this\n rw [← this] at hdiv\n have h2 := hprime.1.two_le\n have : (p - 1) % k = 0 := Nat.mod_eq_zero_of_dvd hdiv\n have hpk : p % k = ((p - 1) % k + 1 % k) % k := by\n rw [← Nat.add_mod]; congr 1; omega\n rw [hpk, this, Nat.mod_eq_of_lt hk1]\n simp [Nat.mod_eq_of_lt hk1]\n\ntheorem infinite (k : ℕ) (hk : 1 < k) : Set.Infinite {p : ℕ | p.Prime ∧ p % k = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n obtain ⟨p, hp, hnp, hpk⟩ := exists_prime_gt_modEq_one' k n hk\n exact ⟨p, ⟨hp, hpk⟩, hnp⟩\n\nend Lemma.Cyc\n\ntheorem Lemma.primes_mod_10_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 10 = 1} :=\n Lemma.Cyc.infinite 10 (by norm_num)\n","Lemma.primes_mod_10_eq_9":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\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\ntheorem exists4 (N : ℕ) (hN : N % 5 = 4)\n (hf : ∀ q, q.Prime → q ∣ N → q % 5 = 1 ∨ q % 5 = 4) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 5 = 4 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 5 = 4 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, 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.P54.exists4 _ 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","Lemma.primes_mod_11_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Cyc\n\nopen Polynomial Nat\n\ntheorem exists_prime_gt_modEq_one' (k n : ℕ) (hk1 : 1 < k) :\n ∃ p : ℕ, p.Prime ∧ n < p ∧ p % k = 1 := by\n have hk0 : k ≠ 0 := by omega\n let b := k * n.factorial\n have hgt : 1 < (eval (b : ℤ) (cyclotomic k ℤ)).natAbs := by\n rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩\n have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos\n calc\n 1 ≤ b - 1 := Nat.le_sub_one_of_lt hb\n _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=\n sub_one_lt_natAbs_cyclotomic_eval hk1 (Nat.succ_le_iff.1 hb).ne'\n let p := minFac (eval (b : ℤ) (cyclotomic k ℤ)).natAbs\n haveI hprime : Fact p.Prime := ⟨minFac_prime (Nat.ne_of_lt hgt).symm⟩\n have h0 : ((eval (b : ℤ) (cyclotomic k ℤ) : ℤ) : ZMod p) = 0 := by\n rw [ZMod.intCast_zmod_eq_zero_iff_dvd]\n exact Int.ofNat_dvd_left.2 (minFac_dvd _)\n have hroot : IsRoot (cyclotomic k (ZMod p)) (b : ZMod p) := by\n have : ((b : ℤ) : ZMod p) = (b : ZMod p) := by push_cast; rfl\n rw [IsRoot.def, ← this, ← map_cyclotomic_int k (ZMod p), eval_intCast_map]\n exact h0\n have hpb : ¬p ∣ b := by\n intro hd\n have hb0 : (b : ZMod p) = 0 := (CharP.cast_eq_zero_iff (ZMod p) p b).2 hd\n have := hroot\n rw [IsRoot.def, hb0, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hk1] at this\n exact one_ne_zero this\n refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩\n · exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)\n · have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=\n ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)\n haveI : NeZero (k : ZMod p) :=\n NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)\n have : k = orderOf (b : ZMod p) := by\n have := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf\n simpa using this\n rw [← this] at hdiv\n have h2 := hprime.1.two_le\n have : (p - 1) % k = 0 := Nat.mod_eq_zero_of_dvd hdiv\n have hpk : p % k = ((p - 1) % k + 1 % k) % k := by\n rw [← Nat.add_mod]; congr 1; omega\n rw [hpk, this, Nat.mod_eq_of_lt hk1]\n simp [Nat.mod_eq_of_lt hk1]\n\ntheorem infinite (k : ℕ) (hk : 1 < k) : Set.Infinite {p : ℕ | p.Prime ∧ p % k = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n obtain ⟨p, hp, hnp, hpk⟩ := exists_prime_gt_modEq_one' k n hk\n exact ⟨p, ⟨hp, hpk⟩, hnp⟩\n\nend Lemma.Cyc\n\ntheorem Lemma.primes_mod_11_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 11 = 1} :=\n Lemma.Cyc.infinite 11 (by norm_num)\n","Lemma.primes_mod_11_eq_10":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\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) : 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 = 0 := by\n linear_combination r ^ 5 * hT + (r ^ 8 + r ^ 7 * T + r ^ 7 + r ^ 6 * T ^ 2 + r ^ 6 * T + r ^ 5 * T ^ 3 + r ^ 5 * T ^ 2 - r ^ 5 * T + r ^ 4 * T ^ 4 + r ^ 4 * T ^ 3 - 2 * r ^ 4 * T ^ 2 - r ^ 4 * T + r ^ 4 + r ^ 3 * T ^ 3 + r ^ 3 * T ^ 2 - r ^ 3 * T + r ^ 2 * T ^ 2 + r ^ 2 * T + r * T + r + 1) * 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 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n set q := N.minFac with hqdef\n rcases hall q hq hqd with h1 | h6\n · obtain ⟨m, hm⟩ := hqd\n have hmod := Nat.mul_mod q m 11\n rw [h1, ← hm, hN] at hmod\n have hm6 : m % 11 = 10 := by omega\n have hmlt : m < N := by\n have hm0 : 0 < m := by\n apply Nat.pos_of_ne_zero\n rintro rfl\n rw [mul_zero] at hm\n omega\n rw [hm]\n calc m = 1 * m := (one_mul m).symm\n _ < q * m := Nat.mul_lt_mul_of_pos_right hq.one_lt hm0\n have hall' : ∀ r, r.Prime → r ∣ m → r % 11 = 1 ∨ r % 11 = 10 := fun r hr hrm =>\n hall r hr (hrm.trans ⟨q, by rw [hm, mul_comm]⟩)\n obtain ⟨r, hr, hr6, hrd⟩ := ih m hmlt hm6 hall'\n exact ⟨r, hr, hr6, hrd.trans ⟨q, by rw [hm, mul_comm]⟩⟩\n · exact ⟨q, hq, h6, hqd⟩\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 hle : x ^ 4 + 4 * x ^ 3 + 1 ≤ x ^ 5 + 3 * x ^ 2 + 3 * x := by\n have h11 : 11 ≤ x := by omega\n have h4 : x ^ 4 * 11 ≤ x ^ 5 := by\n calc x ^ 4 * 11 ≤ x ^ 4 * x := Nat.mul_le_mul_left _ h11\n _ = x ^ 5 := by ring\n have h3 : x ^ 3 * 11 ≤ x ^ 4 := by\n calc x ^ 3 * 11 ≤ x ^ 3 * x := Nat.mul_le_mul_left _ h11\n _ = x ^ 4 := by ring\n have h2 : x ^ 2 * 11 ≤ x ^ 3 := by\n calc x ^ 2 * 11 ≤ x ^ 2 * x := Nat.mul_le_mul_left _ h11\n _ = x ^ 3 := by ring\n have h1 : x * 11 ≤ x ^ 2 := by\n calc x * 11 ≤ x * x := Nat.mul_le_mul_left _ h11\n _ = x ^ 2 := by ring\n omega\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\n have e1 : (11 * y) ^ 4 + 4 * (11 * y) ^ 3 + 1 = 14641 * y ^ 4 + 5324 * y ^ 3 + 1 := by ring\n have e2 : (11 * y) ^ 5 + 3 * (11 * y) ^ 2 + 3 * (11 * y) = 161051 * y ^ 5 + 363 * y ^ 2 + 33 * y := by ring\n rw [← e1, ← e2]; exact 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) = ((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 - 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 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 obtain ⟨q, hq, h8, hqd⟩ := Lemma.P1110.exists_factor N hN11 (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","Lemma.primes_mod_12_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Cyc\n\nopen Polynomial Nat\n\ntheorem exists_prime_gt_modEq_one' (k n : ℕ) (hk1 : 1 < k) :\n ∃ p : ℕ, p.Prime ∧ n < p ∧ p % k = 1 := by\n have hk0 : k ≠ 0 := by omega\n let b := k * n.factorial\n have hgt : 1 < (eval (b : ℤ) (cyclotomic k ℤ)).natAbs := by\n rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩\n have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos\n calc\n 1 ≤ b - 1 := Nat.le_sub_one_of_lt hb\n _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=\n sub_one_lt_natAbs_cyclotomic_eval hk1 (Nat.succ_le_iff.1 hb).ne'\n let p := minFac (eval (b : ℤ) (cyclotomic k ℤ)).natAbs\n haveI hprime : Fact p.Prime := ⟨minFac_prime (Nat.ne_of_lt hgt).symm⟩\n have h0 : ((eval (b : ℤ) (cyclotomic k ℤ) : ℤ) : ZMod p) = 0 := by\n rw [ZMod.intCast_zmod_eq_zero_iff_dvd]\n exact Int.ofNat_dvd_left.2 (minFac_dvd _)\n have hroot : IsRoot (cyclotomic k (ZMod p)) (b : ZMod p) := by\n have : ((b : ℤ) : ZMod p) = (b : ZMod p) := by push_cast; rfl\n rw [IsRoot.def, ← this, ← map_cyclotomic_int k (ZMod p), eval_intCast_map]\n exact h0\n have hpb : ¬p ∣ b := by\n intro hd\n have hb0 : (b : ZMod p) = 0 := (CharP.cast_eq_zero_iff (ZMod p) p b).2 hd\n have := hroot\n rw [IsRoot.def, hb0, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hk1] at this\n exact one_ne_zero this\n refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩\n · exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)\n · have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=\n ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)\n haveI : NeZero (k : ZMod p) :=\n NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)\n have : k = orderOf (b : ZMod p) := by\n have := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf\n simpa using this\n rw [← this] at hdiv\n have h2 := hprime.1.two_le\n have : (p - 1) % k = 0 := Nat.mod_eq_zero_of_dvd hdiv\n have hpk : p % k = ((p - 1) % k + 1 % k) % k := by\n rw [← Nat.add_mod]; congr 1; omega\n rw [hpk, this, Nat.mod_eq_of_lt hk1]\n simp [Nat.mod_eq_of_lt hk1]\n\ntheorem infinite (k : ℕ) (hk : 1 < k) : Set.Infinite {p : ℕ | p.Prime ∧ p % k = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n obtain ⟨p, hp, hnp, hpk⟩ := exists_prime_gt_modEq_one' k n hk\n exact ⟨p, ⟨hp, hpk⟩, hnp⟩\n\nend Lemma.Cyc\n\ntheorem Lemma.primes_mod_12_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 12 = 1} :=\n Lemma.Cyc.infinite 12 (by norm_num)\n","Lemma.primes_mod_12_eq_11":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\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\ntheorem exists11 (N : ℕ) (hN : N % 12 = 11)\n (hf : ∀ q, q.Prime → q ∣ N → q % 12 = 1 ∨ q % 12 = 11) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 12 = 11 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 12 = 11 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, h⟩\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.P1211.exists11 _ 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","Lemma.primes_mod_12_eq_5":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\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]; omega)\n · left; rfl\n · intro i _; 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 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\ntheorem existsA (N : ℕ) (hN : N % 12 = 5)\n (hf : ∀ q, q.Prime → q ∣ N → q % 12 = 1 ∨ q % 12 = 5) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 12 = 5 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 12 = 5 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, h⟩\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 set x := 2 * Lemma.P125.P n with hxdef\n have hx2 : 2 ∣ x := Dvd.intro _ rfl\n have hsq := Lemma.P125.P_sq n\n have hN : (x ^ 2 + 1) % 12 = 5 := by\n have : x ^ 2 + 1 = 4 * Lemma.P125.P n ^ 2 + 1 := by rw [hxdef]; ring\n rw [this]; omega\n obtain ⟨q, hq, hqd, hq5⟩ := Lemma.P125.existsA _ hN (fun q hq hd => by\n have h4 := (Lemma.P125.key x hx2 q hq hd).1\n have h3 : q % 3 ≠ 0 := by\n intro h0\n have h3q : 3 ∣ q := Nat.dvd_of_mod_eq_zero h0\n have : q = 3 := ((Nat.prime_dvd_prime_iff_eq Nat.prime_three hq).1 h3q).symm\n subst this\n have := Nat.mod_eq_zero_of_dvd hd\n omega\n omega)\n refine ⟨q, ⟨hq, hq5⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P125.key x hx2 q hq hqd).2\n (Dvd.dvd.mul_left (Lemma.P125.dvd_P n q (by omega) hle) 2)\n","Lemma.primes_mod_12_eq_7":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\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 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\ntheorem existsA (N : ℕ) (hN : N % 12 = 7)\n (hf : ∀ q, q.Prime → q ∣ N → q % 12 = 1 ∨ q % 12 = 7) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 12 = 7 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 12 = 7 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, h⟩\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 hx6 : 6 ∣ x := Dvd.intro _ rfl\n have hodd := Lemma.P127.Q_odd n\n obtain ⟨k, hk⟩ : ∃ k, x = 12 * k + 6 := ⟨Lemma.P127.Q n / 2, by omega⟩\n have hN : (x ^ 2 + x + 1) % 12 = 7 := by\n have : x ^ 2 + x + 1 = 12 * (12 * k ^ 2 + 13 * k + 3) + 7 := by rw [hk]; ring\n rw [this]; omega\n obtain ⟨q, hq, hqd, hq7⟩ := Lemma.P127.existsA _ hN (fun q hq hd => by\n have := (Lemma.P127.key x hx6 q hq hd).1\n have h2 : q % 2 = 1 := by\n rcases hq.eq_two_or_odd with h | h\n · omega\n · exact h\n omega)\n refine ⟨q, ⟨hq, hq7⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P127.key x hx6 q hq hqd).2\n (Dvd.dvd.mul_left (Lemma.P127.dvd_Q n q (by omega) hle) 6)\n","Lemma.primes_mod_3_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Cyc\n\nopen Polynomial Nat\n\ntheorem exists_prime_gt_modEq_one' (k n : ℕ) (hk1 : 1 < k) :\n ∃ p : ℕ, p.Prime ∧ n < p ∧ p % k = 1 := by\n have hk0 : k ≠ 0 := by omega\n let b := k * n.factorial\n have hgt : 1 < (eval (b : ℤ) (cyclotomic k ℤ)).natAbs := by\n rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩\n have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos\n calc\n 1 ≤ b - 1 := Nat.le_sub_one_of_lt hb\n _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=\n sub_one_lt_natAbs_cyclotomic_eval hk1 (Nat.succ_le_iff.1 hb).ne'\n let p := minFac (eval (b : ℤ) (cyclotomic k ℤ)).natAbs\n haveI hprime : Fact p.Prime := ⟨minFac_prime (Nat.ne_of_lt hgt).symm⟩\n have h0 : ((eval (b : ℤ) (cyclotomic k ℤ) : ℤ) : ZMod p) = 0 := by\n rw [ZMod.intCast_zmod_eq_zero_iff_dvd]\n exact Int.ofNat_dvd_left.2 (minFac_dvd _)\n have hroot : IsRoot (cyclotomic k (ZMod p)) (b : ZMod p) := by\n have : ((b : ℤ) : ZMod p) = (b : ZMod p) := by push_cast; rfl\n rw [IsRoot.def, ← this, ← map_cyclotomic_int k (ZMod p), eval_intCast_map]\n exact h0\n have hpb : ¬p ∣ b := by\n intro hd\n have hb0 : (b : ZMod p) = 0 := (CharP.cast_eq_zero_iff (ZMod p) p b).2 hd\n have := hroot\n rw [IsRoot.def, hb0, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hk1] at this\n exact one_ne_zero this\n refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩\n · exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)\n · have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=\n ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)\n haveI : NeZero (k : ZMod p) :=\n NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)\n have : k = orderOf (b : ZMod p) := by\n have := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf\n simpa using this\n rw [← this] at hdiv\n have h2 := hprime.1.two_le\n have : (p - 1) % k = 0 := Nat.mod_eq_zero_of_dvd hdiv\n have hpk : p % k = ((p - 1) % k + 1 % k) % k := by\n rw [← Nat.add_mod]; congr 1; omega\n rw [hpk, this, Nat.mod_eq_of_lt hk1]\n simp [Nat.mod_eq_of_lt hk1]\n\ntheorem infinite (k : ℕ) (hk : 1 < k) : Set.Infinite {p : ℕ | p.Prime ∧ p % k = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n obtain ⟨p, hp, hnp, hpk⟩ := exists_prime_gt_modEq_one' k n hk\n exact ⟨p, ⟨hp, hpk⟩, hnp⟩\n\nend Lemma.Cyc\n\ntheorem Lemma.primes_mod_3_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 3 = 1} :=\n Lemma.Cyc.infinite 3 (by norm_num)\n","Lemma.primes_mod_3_eq_2":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P32\n\ntheorem exists_factor (N : ℕ) (hN : N % 6 = 5) :\n ∃ q, q.Prime ∧ q % 6 = 5 ∧ q ∣ N := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n set q := N.minFac with hqdef\n have hq2 : q % 2 = 1 := by\n by_contra h\n have h2 : 2 ∣ q := by omega\n have : q = 2 := ((Nat.prime_dvd_prime_iff_eq Nat.prime_two hq).1 h2).symm\n rw [this] at hqd\n omega\n have hq3 : q % 3 ≠ 0 := by\n intro h\n have h3 : 3 ∣ q := by omega\n have : q = 3 := ((Nat.prime_dvd_prime_iff_eq Nat.prime_three hq).1 h3).symm\n rw [this] at hqd\n omega\n by_cases h5 : q % 6 = 5\n · exact ⟨q, hq, h5, hqd⟩\n · have h1 : q % 6 = 1 := by omega\n obtain ⟨m, hm⟩ := hqd\n have hmod := Nat.mul_mod q m 6\n rw [h1, ← hm, hN] at hmod\n have hm5 : m % 6 = 5 := by omega\n have hq2' := hq.two_le\n have hmlt : m < N := by\n have hm0 : 0 < m := by\n apply Nat.pos_of_ne_zero\n rintro rfl\n rw [mul_zero] at hm\n omega\n rw [hm]\n calc m = 1 * m := (one_mul m).symm\n _ < q * m := Nat.mul_lt_mul_of_pos_right hq.one_lt hm0\n obtain ⟨r, hr, hr5, hrd⟩ := ih m hmlt hm5\n exact ⟨r, hr, hr5, hrd.trans ⟨q, by rw [hm, mul_comm]⟩⟩\n\nend Lemma.P32\n\ntheorem Lemma.primes_mod_3_eq_2 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 3 = 2} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 3).factorial with hxdef\n have hx0 : 0 < x := Nat.factorial_pos _\n obtain ⟨q, hq, h5, hd⟩ := Lemma.P32.exists_factor (6 * x - 1) (by omega)\n refine ⟨q, ⟨hq, by omega⟩, ?_⟩\n by_contra hle\n push_neg at hle\n have hqx : q ∣ 6 * x := Dvd.dvd.mul_left (Nat.dvd_factorial hq.pos (by omega)) 6\n have h1 : q ∣ 6 * x - (6 * x - 1) := Nat.dvd_sub hqx hd\n have : 6 * x - (6 * x - 1) = 1 := by omega\n rw [this] at h1\n exact hq.one_lt.ne' (Nat.dvd_one.1 h1)\n","Lemma.primes_mod_4_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Cyc\n\nopen Polynomial Nat\n\ntheorem exists_prime_gt_modEq_one' (k n : ℕ) (hk1 : 1 < k) :\n ∃ p : ℕ, p.Prime ∧ n < p ∧ p % k = 1 := by\n have hk0 : k ≠ 0 := by omega\n let b := k * n.factorial\n have hgt : 1 < (eval (b : ℤ) (cyclotomic k ℤ)).natAbs := by\n rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩\n have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos\n calc\n 1 ≤ b - 1 := Nat.le_sub_one_of_lt hb\n _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=\n sub_one_lt_natAbs_cyclotomic_eval hk1 (Nat.succ_le_iff.1 hb).ne'\n let p := minFac (eval (b : ℤ) (cyclotomic k ℤ)).natAbs\n haveI hprime : Fact p.Prime := ⟨minFac_prime (Nat.ne_of_lt hgt).symm⟩\n have h0 : ((eval (b : ℤ) (cyclotomic k ℤ) : ℤ) : ZMod p) = 0 := by\n rw [ZMod.intCast_zmod_eq_zero_iff_dvd]\n exact Int.ofNat_dvd_left.2 (minFac_dvd _)\n have hroot : IsRoot (cyclotomic k (ZMod p)) (b : ZMod p) := by\n have : ((b : ℤ) : ZMod p) = (b : ZMod p) := by push_cast; rfl\n rw [IsRoot.def, ← this, ← map_cyclotomic_int k (ZMod p), eval_intCast_map]\n exact h0\n have hpb : ¬p ∣ b := by\n intro hd\n have hb0 : (b : ZMod p) = 0 := (CharP.cast_eq_zero_iff (ZMod p) p b).2 hd\n have := hroot\n rw [IsRoot.def, hb0, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hk1] at this\n exact one_ne_zero this\n refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩\n · exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)\n · have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=\n ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)\n haveI : NeZero (k : ZMod p) :=\n NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)\n have : k = orderOf (b : ZMod p) := by\n have := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf\n simpa using this\n rw [← this] at hdiv\n have h2 := hprime.1.two_le\n have : (p - 1) % k = 0 := Nat.mod_eq_zero_of_dvd hdiv\n have hpk : p % k = ((p - 1) % k + 1 % k) % k := by\n rw [← Nat.add_mod]; congr 1; omega\n rw [hpk, this, Nat.mod_eq_of_lt hk1]\n simp [Nat.mod_eq_of_lt hk1]\n\ntheorem infinite (k : ℕ) (hk : 1 < k) : Set.Infinite {p : ℕ | p.Prime ∧ p % k = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n obtain ⟨p, hp, hnp, hpk⟩ := exists_prime_gt_modEq_one' k n hk\n exact ⟨p, ⟨hp, hpk⟩, hnp⟩\n\nend Lemma.Cyc\n\ntheorem Lemma.primes_mod_4_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 4 = 1} :=\n Lemma.Cyc.infinite 4 (by norm_num)\n","Lemma.primes_mod_4_eq_3":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P43\n\ntheorem exists_factor (N : ℕ) (hN : N % 4 = 3) :\n ∃ q, q.Prime ∧ q % 4 = 3 ∧ q ∣ N := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n set q := N.minFac with hqdef\n have hq2 : q % 2 = 1 := by\n by_contra h\n have h2 : 2 ∣ q := by omega\n have : q = 2 := ((Nat.prime_dvd_prime_iff_eq Nat.prime_two hq).1 h2).symm\n rw [this] at hqd\n omega\n by_cases h5 : q % 4 = 3\n · exact ⟨q, hq, h5, hqd⟩\n · have h1 : q % 4 = 1 := by omega\n obtain ⟨m, hm⟩ := hqd\n have hmod := Nat.mul_mod q m 4\n rw [h1, ← hm, hN] at hmod\n have hm5 : m % 4 = 3 := by omega\n have hq2' := hq.two_le\n have hmlt : m < N := by\n have hm0 : 0 < m := by\n apply Nat.pos_of_ne_zero\n rintro rfl\n rw [mul_zero] at hm\n omega\n rw [hm]\n calc m = 1 * m := (one_mul m).symm\n _ < q * m := Nat.mul_lt_mul_of_pos_right hq.one_lt hm0\n obtain ⟨r, hr, hr5, hrd⟩ := ih m hmlt hm5\n exact ⟨r, hr, hr5, hrd.trans ⟨q, by rw [hm, mul_comm]⟩⟩\n\nend Lemma.P43\n\ntheorem Lemma.primes_mod_4_eq_3 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 4 = 3} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 3).factorial with hxdef\n have hx0 : 0 < x := Nat.factorial_pos _\n obtain ⟨q, hq, h5, hd⟩ := Lemma.P43.exists_factor (4 * x - 1) (by omega)\n refine ⟨q, ⟨hq, h5⟩, ?_⟩\n by_contra hle\n push_neg at hle\n have hqx : q ∣ 4 * x := Dvd.dvd.mul_left (Nat.dvd_factorial hq.pos (by omega)) 4\n have h1 : q ∣ 4 * x - (4 * x - 1) := Nat.dvd_sub hqx hd\n have : 4 * x - (4 * x - 1) = 1 := by omega\n rw [this] at h1\n exact hq.one_lt.ne' (Nat.dvd_one.1 h1)\n","Lemma.primes_mod_5_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Cyc\n\nopen Polynomial Nat\n\ntheorem exists_prime_gt_modEq_one' (k n : ℕ) (hk1 : 1 < k) :\n ∃ p : ℕ, p.Prime ∧ n < p ∧ p % k = 1 := by\n have hk0 : k ≠ 0 := by omega\n let b := k * n.factorial\n have hgt : 1 < (eval (b : ℤ) (cyclotomic k ℤ)).natAbs := by\n rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩\n have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos\n calc\n 1 ≤ b - 1 := Nat.le_sub_one_of_lt hb\n _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=\n sub_one_lt_natAbs_cyclotomic_eval hk1 (Nat.succ_le_iff.1 hb).ne'\n let p := minFac (eval (b : ℤ) (cyclotomic k ℤ)).natAbs\n haveI hprime : Fact p.Prime := ⟨minFac_prime (Nat.ne_of_lt hgt).symm⟩\n have h0 : ((eval (b : ℤ) (cyclotomic k ℤ) : ℤ) : ZMod p) = 0 := by\n rw [ZMod.intCast_zmod_eq_zero_iff_dvd]\n exact Int.ofNat_dvd_left.2 (minFac_dvd _)\n have hroot : IsRoot (cyclotomic k (ZMod p)) (b : ZMod p) := by\n have : ((b : ℤ) : ZMod p) = (b : ZMod p) := by push_cast; rfl\n rw [IsRoot.def, ← this, ← map_cyclotomic_int k (ZMod p), eval_intCast_map]\n exact h0\n have hpb : ¬p ∣ b := by\n intro hd\n have hb0 : (b : ZMod p) = 0 := (CharP.cast_eq_zero_iff (ZMod p) p b).2 hd\n have := hroot\n rw [IsRoot.def, hb0, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hk1] at this\n exact one_ne_zero this\n refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩\n · exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)\n · have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=\n ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)\n haveI : NeZero (k : ZMod p) :=\n NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)\n have : k = orderOf (b : ZMod p) := by\n have := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf\n simpa using this\n rw [← this] at hdiv\n have h2 := hprime.1.two_le\n have : (p - 1) % k = 0 := Nat.mod_eq_zero_of_dvd hdiv\n have hpk : p % k = ((p - 1) % k + 1 % k) % k := by\n rw [← Nat.add_mod]; congr 1; omega\n rw [hpk, this, Nat.mod_eq_of_lt hk1]\n simp [Nat.mod_eq_of_lt hk1]\n\ntheorem infinite (k : ℕ) (hk : 1 < k) : Set.Infinite {p : ℕ | p.Prime ∧ p % k = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n obtain ⟨p, hp, hnp, hpk⟩ := exists_prime_gt_modEq_one' k n hk\n exact ⟨p, ⟨hp, hpk⟩, hnp⟩\n\nend Lemma.Cyc\n\ntheorem Lemma.primes_mod_5_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 5 = 1} :=\n Lemma.Cyc.infinite 5 (by norm_num)\n","Lemma.primes_mod_5_eq_4":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\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\ntheorem exists4 (N : ℕ) (hN : N % 5 = 4)\n (hf : ∀ q, q.Prime → q ∣ N → q % 5 = 1 ∨ q % 5 = 4) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 5 = 4 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 5 = 4 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, 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.P54.exists4 _ 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","Lemma.primes_mod_6_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Cyc\n\nopen Polynomial Nat\n\ntheorem exists_prime_gt_modEq_one' (k n : ℕ) (hk1 : 1 < k) :\n ∃ p : ℕ, p.Prime ∧ n < p ∧ p % k = 1 := by\n have hk0 : k ≠ 0 := by omega\n let b := k * n.factorial\n have hgt : 1 < (eval (b : ℤ) (cyclotomic k ℤ)).natAbs := by\n rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩\n have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos\n calc\n 1 ≤ b - 1 := Nat.le_sub_one_of_lt hb\n _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=\n sub_one_lt_natAbs_cyclotomic_eval hk1 (Nat.succ_le_iff.1 hb).ne'\n let p := minFac (eval (b : ℤ) (cyclotomic k ℤ)).natAbs\n haveI hprime : Fact p.Prime := ⟨minFac_prime (Nat.ne_of_lt hgt).symm⟩\n have h0 : ((eval (b : ℤ) (cyclotomic k ℤ) : ℤ) : ZMod p) = 0 := by\n rw [ZMod.intCast_zmod_eq_zero_iff_dvd]\n exact Int.ofNat_dvd_left.2 (minFac_dvd _)\n have hroot : IsRoot (cyclotomic k (ZMod p)) (b : ZMod p) := by\n have : ((b : ℤ) : ZMod p) = (b : ZMod p) := by push_cast; rfl\n rw [IsRoot.def, ← this, ← map_cyclotomic_int k (ZMod p), eval_intCast_map]\n exact h0\n have hpb : ¬p ∣ b := by\n intro hd\n have hb0 : (b : ZMod p) = 0 := (CharP.cast_eq_zero_iff (ZMod p) p b).2 hd\n have := hroot\n rw [IsRoot.def, hb0, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hk1] at this\n exact one_ne_zero this\n refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩\n · exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)\n · have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=\n ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)\n haveI : NeZero (k : ZMod p) :=\n NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)\n have : k = orderOf (b : ZMod p) := by\n have := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf\n simpa using this\n rw [← this] at hdiv\n have h2 := hprime.1.two_le\n have : (p - 1) % k = 0 := Nat.mod_eq_zero_of_dvd hdiv\n have hpk : p % k = ((p - 1) % k + 1 % k) % k := by\n rw [← Nat.add_mod]; congr 1; omega\n rw [hpk, this, Nat.mod_eq_of_lt hk1]\n simp [Nat.mod_eq_of_lt hk1]\n\ntheorem infinite (k : ℕ) (hk : 1 < k) : Set.Infinite {p : ℕ | p.Prime ∧ p % k = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n obtain ⟨p, hp, hnp, hpk⟩ := exists_prime_gt_modEq_one' k n hk\n exact ⟨p, ⟨hp, hpk⟩, hnp⟩\n\nend Lemma.Cyc\n\ntheorem Lemma.primes_mod_6_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 6 = 1} :=\n Lemma.Cyc.infinite 6 (by norm_num)\n","Lemma.primes_mod_6_eq_5":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P65\n\ntheorem exists_factor (N : ℕ) (hN : N % 6 = 5) :\n ∃ q, q.Prime ∧ q % 6 = 5 ∧ q ∣ N := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n set q := N.minFac with hqdef\n have hq2 : q % 2 = 1 := by\n by_contra h\n have h2 : 2 ∣ q := by omega\n have : q = 2 := ((Nat.prime_dvd_prime_iff_eq Nat.prime_two hq).1 h2).symm\n rw [this] at hqd\n omega\n have hq3 : q % 3 ≠ 0 := by\n intro h\n have h3 : 3 ∣ q := by omega\n have : q = 3 := ((Nat.prime_dvd_prime_iff_eq Nat.prime_three hq).1 h3).symm\n rw [this] at hqd\n omega\n by_cases h5 : q % 6 = 5\n · exact ⟨q, hq, h5, hqd⟩\n · have h1 : q % 6 = 1 := by omega\n obtain ⟨m, hm⟩ := hqd\n have hmod := Nat.mul_mod q m 6\n rw [h1, ← hm, hN] at hmod\n have hm5 : m % 6 = 5 := by omega\n have hq2' := hq.two_le\n have hmlt : m < N := by\n have hm0 : 0 < m := by\n apply Nat.pos_of_ne_zero\n rintro rfl\n rw [mul_zero] at hm\n omega\n rw [hm]\n calc m = 1 * m := (one_mul m).symm\n _ < q * m := Nat.mul_lt_mul_of_pos_right hq.one_lt hm0\n obtain ⟨r, hr, hr5, hrd⟩ := ih m hmlt hm5\n exact ⟨r, hr, hr5, hrd.trans ⟨q, by rw [hm, mul_comm]⟩⟩\n\nend Lemma.P65\n\ntheorem Lemma.primes_mod_6_eq_5 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 6 = 5} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 3).factorial with hxdef\n have hx0 : 0 < x := Nat.factorial_pos _\n obtain ⟨q, hq, h5, hd⟩ := Lemma.P65.exists_factor (6 * x - 1) (by omega)\n refine ⟨q, ⟨hq, h5⟩, ?_⟩\n by_contra hle\n push_neg at hle\n have hqx : q ∣ 6 * x := Dvd.dvd.mul_left (Nat.dvd_factorial hq.pos (by omega)) 6\n have h1 : q ∣ 6 * x - (6 * x - 1) := Nat.dvd_sub hqx hd\n have : 6 * x - (6 * x - 1) = 1 := by omega\n rw [this] at h1\n exact hq.one_lt.ne' (Nat.dvd_one.1 h1)\n","Lemma.primes_mod_7_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Cyc\n\nopen Polynomial Nat\n\ntheorem exists_prime_gt_modEq_one' (k n : ℕ) (hk1 : 1 < k) :\n ∃ p : ℕ, p.Prime ∧ n < p ∧ p % k = 1 := by\n have hk0 : k ≠ 0 := by omega\n let b := k * n.factorial\n have hgt : 1 < (eval (b : ℤ) (cyclotomic k ℤ)).natAbs := by\n rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩\n have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos\n calc\n 1 ≤ b - 1 := Nat.le_sub_one_of_lt hb\n _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=\n sub_one_lt_natAbs_cyclotomic_eval hk1 (Nat.succ_le_iff.1 hb).ne'\n let p := minFac (eval (b : ℤ) (cyclotomic k ℤ)).natAbs\n haveI hprime : Fact p.Prime := ⟨minFac_prime (Nat.ne_of_lt hgt).symm⟩\n have h0 : ((eval (b : ℤ) (cyclotomic k ℤ) : ℤ) : ZMod p) = 0 := by\n rw [ZMod.intCast_zmod_eq_zero_iff_dvd]\n exact Int.ofNat_dvd_left.2 (minFac_dvd _)\n have hroot : IsRoot (cyclotomic k (ZMod p)) (b : ZMod p) := by\n have : ((b : ℤ) : ZMod p) = (b : ZMod p) := by push_cast; rfl\n rw [IsRoot.def, ← this, ← map_cyclotomic_int k (ZMod p), eval_intCast_map]\n exact h0\n have hpb : ¬p ∣ b := by\n intro hd\n have hb0 : (b : ZMod p) = 0 := (CharP.cast_eq_zero_iff (ZMod p) p b).2 hd\n have := hroot\n rw [IsRoot.def, hb0, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hk1] at this\n exact one_ne_zero this\n refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩\n · exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)\n · have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=\n ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)\n haveI : NeZero (k : ZMod p) :=\n NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)\n have : k = orderOf (b : ZMod p) := by\n have := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf\n simpa using this\n rw [← this] at hdiv\n have h2 := hprime.1.two_le\n have : (p - 1) % k = 0 := Nat.mod_eq_zero_of_dvd hdiv\n have hpk : p % k = ((p - 1) % k + 1 % k) % k := by\n rw [← Nat.add_mod]; congr 1; omega\n rw [hpk, this, Nat.mod_eq_of_lt hk1]\n simp [Nat.mod_eq_of_lt hk1]\n\ntheorem infinite (k : ℕ) (hk : 1 < k) : Set.Infinite {p : ℕ | p.Prime ∧ p % k = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n obtain ⟨p, hp, hnp, hpk⟩ := exists_prime_gt_modEq_one' k n hk\n exact ⟨p, ⟨hp, hpk⟩, hnp⟩\n\nend Lemma.Cyc\n\ntheorem Lemma.primes_mod_7_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 7 = 1} :=\n Lemma.Cyc.infinite 7 (by norm_num)\n","Lemma.primes_mod_7_eq_6":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\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 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n set q := N.minFac with hqdef\n rcases hall q hq hqd with h1 | h6\n · obtain ⟨m, hm⟩ := hqd\n have hmod := Nat.mul_mod q m 7\n rw [h1, ← hm, hN] at hmod\n have hm6 : m % 7 = 6 := by omega\n have hmlt : m < N := by\n have hm0 : 0 < m := by\n apply Nat.pos_of_ne_zero\n rintro rfl\n rw [mul_zero] at hm\n omega\n rw [hm]\n calc m = 1 * m := (one_mul m).symm\n _ < q * m := Nat.mul_lt_mul_of_pos_right hq.one_lt hm0\n have hall' : ∀ r, r.Prime → r ∣ m → r % 7 = 1 ∨ r % 7 = 6 := fun r hr hrm =>\n hall r hr (hrm.trans ⟨q, by rw [hm, mul_comm]⟩)\n obtain ⟨r, hr, hr6, hrd⟩ := ih m hmlt hm6 hall'\n exact ⟨r, hr, hr6, hrd.trans ⟨q, by rw [hm, mul_comm]⟩⟩\n · exact ⟨q, hq, h6, hqd⟩\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","Lemma.primes_mod_8_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Cyc\n\nopen Polynomial Nat\n\ntheorem exists_prime_gt_modEq_one' (k n : ℕ) (hk1 : 1 < k) :\n ∃ p : ℕ, p.Prime ∧ n < p ∧ p % k = 1 := by\n have hk0 : k ≠ 0 := by omega\n let b := k * n.factorial\n have hgt : 1 < (eval (b : ℤ) (cyclotomic k ℤ)).natAbs := by\n rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩\n have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos\n calc\n 1 ≤ b - 1 := Nat.le_sub_one_of_lt hb\n _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=\n sub_one_lt_natAbs_cyclotomic_eval hk1 (Nat.succ_le_iff.1 hb).ne'\n let p := minFac (eval (b : ℤ) (cyclotomic k ℤ)).natAbs\n haveI hprime : Fact p.Prime := ⟨minFac_prime (Nat.ne_of_lt hgt).symm⟩\n have h0 : ((eval (b : ℤ) (cyclotomic k ℤ) : ℤ) : ZMod p) = 0 := by\n rw [ZMod.intCast_zmod_eq_zero_iff_dvd]\n exact Int.ofNat_dvd_left.2 (minFac_dvd _)\n have hroot : IsRoot (cyclotomic k (ZMod p)) (b : ZMod p) := by\n have : ((b : ℤ) : ZMod p) = (b : ZMod p) := by push_cast; rfl\n rw [IsRoot.def, ← this, ← map_cyclotomic_int k (ZMod p), eval_intCast_map]\n exact h0\n have hpb : ¬p ∣ b := by\n intro hd\n have hb0 : (b : ZMod p) = 0 := (CharP.cast_eq_zero_iff (ZMod p) p b).2 hd\n have := hroot\n rw [IsRoot.def, hb0, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hk1] at this\n exact one_ne_zero this\n refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩\n · exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)\n · have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=\n ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)\n haveI : NeZero (k : ZMod p) :=\n NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)\n have : k = orderOf (b : ZMod p) := by\n have := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf\n simpa using this\n rw [← this] at hdiv\n have h2 := hprime.1.two_le\n have : (p - 1) % k = 0 := Nat.mod_eq_zero_of_dvd hdiv\n have hpk : p % k = ((p - 1) % k + 1 % k) % k := by\n rw [← Nat.add_mod]; congr 1; omega\n rw [hpk, this, Nat.mod_eq_of_lt hk1]\n simp [Nat.mod_eq_of_lt hk1]\n\ntheorem infinite (k : ℕ) (hk : 1 < k) : Set.Infinite {p : ℕ | p.Prime ∧ p % k = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n obtain ⟨p, hp, hnp, hpk⟩ := exists_prime_gt_modEq_one' k n hk\n exact ⟨p, ⟨hp, hpk⟩, hnp⟩\n\nend Lemma.Cyc\n\ntheorem Lemma.primes_mod_8_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 8 = 1} :=\n Lemma.Cyc.infinite 8 (by norm_num)\n","Lemma.primes_mod_8_eq_3":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\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\ntheorem existsA (N : ℕ) (hN : N % 8 = 3)\n (hf : ∀ q, q.Prime → q ∣ N → q % 8 = 1 ∨ q % 8 = 3) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 8 = 3 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 8 = 3 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, h⟩\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.P83.existsA _ 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","Lemma.primes_mod_8_eq_5":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\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\ntheorem existsA (N : ℕ) (hN : N % 8 = 5)\n (hf : ∀ q, q.Prime → q ∣ N → q % 8 = 1 ∨ q % 8 = 5) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 8 = 5 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 8 = 5 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, h⟩\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.P85.existsA _ 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","Lemma.primes_mod_8_eq_7":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\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\ntheorem exists7 (N : ℕ) (hN : N % 8 = 7)\n (hf : ∀ q, q.Prime → q ∣ N → q % 8 = 1 ∨ q % 8 = 7) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 8 = 7 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 8 = 7 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, h⟩\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.P87.exists7 _ 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","Lemma.primes_mod_9_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Cyc\n\nopen Polynomial Nat\n\ntheorem exists_prime_gt_modEq_one' (k n : ℕ) (hk1 : 1 < k) :\n ∃ p : ℕ, p.Prime ∧ n < p ∧ p % k = 1 := by\n have hk0 : k ≠ 0 := by omega\n let b := k * n.factorial\n have hgt : 1 < (eval (b : ℤ) (cyclotomic k ℤ)).natAbs := by\n rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩\n have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos\n calc\n 1 ≤ b - 1 := Nat.le_sub_one_of_lt hb\n _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=\n sub_one_lt_natAbs_cyclotomic_eval hk1 (Nat.succ_le_iff.1 hb).ne'\n let p := minFac (eval (b : ℤ) (cyclotomic k ℤ)).natAbs\n haveI hprime : Fact p.Prime := ⟨minFac_prime (Nat.ne_of_lt hgt).symm⟩\n have h0 : ((eval (b : ℤ) (cyclotomic k ℤ) : ℤ) : ZMod p) = 0 := by\n rw [ZMod.intCast_zmod_eq_zero_iff_dvd]\n exact Int.ofNat_dvd_left.2 (minFac_dvd _)\n have hroot : IsRoot (cyclotomic k (ZMod p)) (b : ZMod p) := by\n have : ((b : ℤ) : ZMod p) = (b : ZMod p) := by push_cast; rfl\n rw [IsRoot.def, ← this, ← map_cyclotomic_int k (ZMod p), eval_intCast_map]\n exact h0\n have hpb : ¬p ∣ b := by\n intro hd\n have hb0 : (b : ZMod p) = 0 := (CharP.cast_eq_zero_iff (ZMod p) p b).2 hd\n have := hroot\n rw [IsRoot.def, hb0, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hk1] at this\n exact one_ne_zero this\n refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩\n · exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)\n · have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=\n ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)\n haveI : NeZero (k : ZMod p) :=\n NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)\n have : k = orderOf (b : ZMod p) := by\n have := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf\n simpa using this\n rw [← this] at hdiv\n have h2 := hprime.1.two_le\n have : (p - 1) % k = 0 := Nat.mod_eq_zero_of_dvd hdiv\n have hpk : p % k = ((p - 1) % k + 1 % k) % k := by\n rw [← Nat.add_mod]; congr 1; omega\n rw [hpk, this, Nat.mod_eq_of_lt hk1]\n simp [Nat.mod_eq_of_lt hk1]\n\ntheorem infinite (k : ℕ) (hk : 1 < k) : Set.Infinite {p : ℕ | p.Prime ∧ p % k = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n obtain ⟨p, hp, hnp, hpk⟩ := exists_prime_gt_modEq_one' k n hk\n exact ⟨p, ⟨hp, hpk⟩, hnp⟩\n\nend Lemma.Cyc\n\ntheorem Lemma.primes_mod_9_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 9 = 1} :=\n Lemma.Cyc.infinite 9 (by norm_num)\n","Lemma.primes_mod_9_eq_8":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P98\n\nopen Polynomial\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 Nat.prime_three\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 + (r ^ 4 + r ^ 3 * T + r ^ 2 * T ^ 2 - r ^ 2 + r * T + 1) * hr\n have hr9 : r ^ (3 ^ (1 + 1)) = 1 := by\n norm_num\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 h33 : ((3 : ℕ) : K) = 0 := by\n push_cast\n linear_combination (-(r ^ 3 + 2)) * h3' + hphi\n have hq3' : q ∣ 3 := (CharP.cast_eq_zero_iff K q 3).1 h33\n exact hq3 ((Nat.prime_dvd_prime_iff_eq hq Nat.prime_three).1 hq3')\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 = 3 ^ (1 + 1) := orderOf_eq_prime_pow hr3 hr9\n norm_num at hord\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 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n set q := N.minFac with hqdef\n rcases hall q hq hqd with h1 | h6\n · obtain ⟨m, hm⟩ := hqd\n have hmod := Nat.mul_mod q m 9\n rw [h1, ← hm, hN] at hmod\n have hm6 : m % 9 = 8 := by omega\n have hmlt : m < N := by\n have hm0 : 0 < m := by\n apply Nat.pos_of_ne_zero\n rintro rfl\n rw [mul_zero] at hm\n omega\n rw [hm]\n calc m = 1 * m := (one_mul m).symm\n _ < q * m := Nat.mul_lt_mul_of_pos_right hq.one_lt hm0\n have hall' : ∀ r, r.Prime → r ∣ m → r % 9 = 1 ∨ r % 9 = 8 := fun r hr hrm =>\n hall r hr (hrm.trans ⟨q, by rw [hm, mul_comm]⟩)\n obtain ⟨r, hr, hr6, hrd⟩ := ih m hmlt hm6 hall'\n exact ⟨r, hr, hr6, hrd.trans ⟨q, by rw [hm, mul_comm]⟩⟩\n · exact ⟨q, hq, h6, hqd⟩\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 h9 : 9 ≤ x := by omega\n have h3 : x ^ 3 = x * (x * x) := by ring\n have h1 : 9 * x ≤ x * x := Nat.mul_le_mul_right x h9\n have h2 : 9 * (x * x) ≤ x * (x * x) := Nat.mul_le_mul_right (x * x) h9\n rw [h3]\n omega\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 generalize y ^ 3 = a at hN'\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"}},"flags":[],"id":118,"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":"C118 completes the set: theorems proved 24. 0 open unit(s) closed; the lab's maintainers can retire the program or add challenges.","claim":118,"created":1792131620,"credit":[2],"id":298,"kind":"summary","label":null,"parent":null,"program":"euclid-primes","score":24.0,"title":"Primes in progressions, Euclid's way: every challenge is settled","unit":161},"followups":[]}