{"claim":{"assessments":[],"bundle":{"code":"","commit":"25abb822d7319ebd2381f3c4c9e9aa2cff537916","config":null,"environment":"lemma/0.7.9 agent","logs":"","seeds":[]},"candidate":{"proofs":{"Lemma.am_gm":"import Mathlib.Data.Real.Basic\nimport Mathlib.Algebra.BigOperators.Fin\n\nlemma amgm_bern (c d : ℝ) (hc : 0 ≤ c) (hcd : 0 ≤ c + d) :\n    ∀ m : ℕ, c ^ m * (c + m * d) ≤ c * (c + d) ^ m := by\n  intro m\n  induction m with\n  | zero => simp\n  | succ m ih =>\n    have h1 : c ^ m * (c + m * d) * (c + d) ≤ c * (c + d) ^ m * (c + d) :=\n      mul_le_mul_of_nonneg_right ih hcd\n    have h2 : 0 ≤ c ^ m * ((m : ℝ) * (d * d)) :=\n      mul_nonneg (pow_nonneg hc m) (mul_nonneg (Nat.cast_nonneg m) (mul_self_nonneg d))\n    have e1 : c ^ m * (c + m * d) * (c + d)\n        = c ^ (m + 1) * (c + ((m + 1 : ℕ) : ℝ) * d) + c ^ m * ((m : ℝ) * (d * d)) := by\n      push_cast; grind\n    have e2 : c * (c + d) ^ m * (c + d) = c * (c + d) ^ (m + 1) := by grind\n    grind\n\nlemma amgm_step (A x : ℝ) (hA : 0 ≤ A) (hx : 0 ≤ x) (n : ℕ) :\n    A ^ n * x ≤ ((n * A + x) / (n + 1)) ^ (n + 1) := by\n  have hn : (0 : ℝ) < n + 1 := by\n    have := Nat.cast_nonneg (α := ℝ) n\n    grind\n  have hB : 0 ≤ (n * A + x) / (n + 1) :=\n    div_nonneg (add_nonneg (mul_nonneg (Nat.cast_nonneg n) hA) hx) hn.le\n  have hmul : ((n : ℝ) + 1) * ((n * A + x) / (n + 1)) = n * A + x := by\n    rw [mul_div_assoc']\n    exact mul_div_cancel_left₀ _ hn.ne'\n  rcases hA.lt_or_eq with hA' | hA'\n  · have h := amgm_bern A ((n * A + x) / (n + 1) - A) hA (by grind) (n + 1)\n    have e : A + ((n + 1 : ℕ) : ℝ) * ((n * A + x) / (n + 1) - A) = x := by\n      push_cast; grind\n    rw [e, show A + ((n * A + x) / (n + 1) - A) = (n * A + x) / (n + 1) by grind] at h\n    have : A * (A ^ n * x) ≤ A * ((n * A + x) / (n + 1)) ^ (n + 1) := by\n      calc A * (A ^ n * x) = A ^ (n + 1) * x := by grind\n        _ ≤ _ := h\n    exact le_of_mul_le_mul_left this hA'\n  · subst hA'\n    rcases n with _ | n\n    · simp\n    · simp only [ne_eq, Nat.add_one_ne_zero, not_false_eq_true, zero_pow, zero_mul]\n      exact pow_nonneg hB _\n\nlemma amgm_sum_nonneg : ∀ (n : ℕ) (x : Fin n → ℝ), (∀ i, 0 ≤ x i) → 0 ≤ ∑ i, x i := by\n  intro n\n  induction n with\n  | zero => intro x _; simp\n  | succ n ih =>\n    intro x hx\n    rw [Fin.sum_univ_castSucc]\n    exact add_nonneg (ih _ (fun i => hx _)) (hx _)\n\ntheorem Lemma.am_gm : ∀ (n : ℕ) (x : Fin n → ℝ), (∀ i, 0 ≤ x i) → ∏ i, x i ≤ ((∑ i, x i) / n) ^ n := by\n  intro n\n  induction n with\n  | zero => intro x _; simp\n  | succ n ih =>\n    intro x hx\n    rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]\n    have hS0 : 0 ≤ ∑ i : Fin n, x i.castSucc := amgm_sum_nonneg n _ (fun i => hx _)\n    have hih := ih (fun i => x i.castSucc) (fun i => hx _)\n    have hS00 : n = 0 → ∑ i : Fin n, x i.castSucc = 0 := by rintro rfl; simp\n    generalize ∑ i : Fin n, x i.castSucc = S at hS0 hih hS00 ⊢\n    have hSA : S = n * (S / n) := by\n      rcases Nat.eq_zero_or_pos n with h | h\n      · simp [hS00 h, h]\n      · have : (n : ℝ) ≠ 0 := by exact_mod_cast h.ne'\n        rw [mul_div_assoc']\n        exact (mul_div_cancel_left₀ _ this).symm\n    have hA : 0 ≤ S / n := div_nonneg hS0 (Nat.cast_nonneg n)\n    have key := amgm_step (S / n) (x (Fin.last n)) hA (hx _) n\n    rw [← hSA] at key\n    push_cast\n    calc (∏ i : Fin n, x i.castSucc) * x (Fin.last n)\n        ≤ (S / n) ^ n * x (Fin.last n) := mul_le_mul_of_nonneg_right hih (hx _)\n      _ ≤ _ := key\n","Lemma.bertrand":"import Mathlib.NumberTheory.Primorial\nimport Mathlib.Data.Nat.Choose.Central\nimport Mathlib.Data.Nat.Choose.Factorization\n\nopen Nat\n\ntheorem bert_mid_le (k : ℕ) :\n    (∏ i ∈ Finset.Ico (k+1+1) (2*k+1+1), if i.Prime then i else 1) ≤ 4 ^ k := by\n  rw [← Finset.prod_filter]\n  have hd : (∏ p ∈ Finset.filter Nat.Prime (Finset.Ico (k+1+1) (2*k+1+1)), p) ∣\n      choose (k+1+k) (k+1) := by\n    apply Finset.prod_primes_dvd\n    · intro a ha; exact (Finset.mem_filter.1 ha).2.prime\n    · intro a ha\n      obtain ⟨h1, h2⟩ := Finset.mem_filter.1 ha\n      rw [Finset.mem_Ico] at h1\n      exact h2.dvd_choose_add (by omega) (by omega) (by omega)\n  have hc : choose (k+1+k) (k+1) = choose (2*k+1) k := by\n    rw [show k+1+k = 2*k+1 by omega]\n    exact Nat.choose_symm_of_eq_add (by omega)\n  rw [hc] at hd\n  exact (Nat.le_of_dvd (Nat.choose_pos (by omega)) hd).trans (Nat.choose_middle_le_pow k)\n\ntheorem bert_Q_le (n : ℕ) :\n    (∏ i ∈ Finset.range (n+1), if i.Prime then i else 1) ≤ 4 ^ n := by\n  induction n using Nat.strong_induction_on with\n  | _ n ih =>\n  rcases Nat.even_or_odd' n with ⟨k, rfl | rfl⟩\n  · rcases Nat.lt_or_ge k 2 with hk | hk\n    · interval_cases k <;> decide\n    · obtain ⟨j, hj⟩ : ∃ j, 2 * k = j + 1 := ⟨2 * k - 1, by omega⟩\n      rw [hj, Finset.prod_range_succ, if_neg, Nat.mul_one]\n      · exact (ih j (by omega)).trans (Nat.pow_le_pow_right (by omega) (by omega))\n      · rw [← hj]; intro hp\n        rcases hp.eq_one_or_self_of_dvd 2 (Nat.dvd_mul_right 2 k) with h | h <;> omega\n  · rcases Nat.lt_or_ge k 1 with hk | hk\n    · interval_cases k; decide\n    · rw [← Finset.prod_range_mul_prod_Ico _ (show k+1+1 ≤ 2*k+1+1 by omega)]\n      calc _ ≤ 4 ^ (k+1) * 4 ^ k := Nat.mul_le_mul (ih (k+1) (by omega)) (bert_mid_le k)\n        _ = 4 ^ (2*k+1) := by rw [← Nat.pow_add]; congr 1; omega\n\ntheorem bert_primorial_le (n : ℕ) :\n    ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n+1)), p ≤ 4 ^ n := by\n  rw [Finset.prod_filter]; exact bert_Q_le n\n\ntheorem bert_factorization_small (n : ℕ) (n_large : 2 < n)\n    (no_prime : ¬∃ p : ℕ, p.Prime ∧ n < p ∧ p ≤ 2 * n) :\n    centralBinom n = ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ (centralBinom n).factorization p := by\n  refine (Eq.trans ?_ n.prod_pow_factorization_centralBinom).symm\n  apply Finset.prod_subset\n  · exact Finset.range_subset_range.2 (Nat.add_le_add_right (Nat.div_le_self _ _) _)\n  intro x hx h2x\n  rw [Finset.mem_range, Nat.lt_succ_iff] at hx h2x\n  have h3 : 2 * n < 3 * x := by omega\n  by_cases hp : x.Prime\n  · have : x ≤ n := by\n      by_contra h\n      exact no_prime ⟨x, hp, by omega, hx⟩\n    rw [factorization_centralBinom_of_two_mul_self_lt_three_mul n_large this h3, Nat.pow_zero]\n  · rw [Nat.factorization_eq_zero_of_not_prime _ hp, Nat.pow_zero]\n\ntheorem bert_centralBinom_le (n : ℕ) (n_large : 2 < n)\n    (no_prime : ¬∃ p : ℕ, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n) :\n    centralBinom n ≤ (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) := by\n  have n_pos : 0 < n := (Nat.zero_le _).trans_lt n_large\n  have n2_pos : 1 ≤ 2 * n := by omega\n  let S := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}\n  let f x := x ^ n.centralBinom.factorization x\n  have : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x := by\n    refine Finset.prod_filter_of_ne fun p _ h => ?_\n    contrapose! h; dsimp only [f]\n    rw [Nat.factorization_eq_zero_of_not_prime n.centralBinom h, _root_.pow_zero]\n  rw [bert_factorization_small n n_large no_prime, ← this, ←\n    Finset.prod_filter_mul_prod_filter_not S fun p => p ^ 2 ≤ 2 * n]\n  apply Nat.mul_le_mul\n  · refine (Finset.prod_le_prod' fun p _ => (?_ : f p ≤ 2 * n)).trans ?_\n    · exact pow_factorization_choose_le (by omega)\n    have : (Finset.Icc 1 (sqrt (2 * n))).card = sqrt (2 * n) := by\n      rw [Nat.card_Icc, Nat.add_sub_cancel]\n    rw [Finset.prod_const]\n    refine pow_right_mono₀ n2_pos ((Finset.card_le_card fun x hx => ?_).trans this.le)\n    obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hx\n    exact Finset.mem_Icc.mpr ⟨(Finset.mem_filter.1 h1).2.one_lt.le, Nat.le_sqrt'.mpr h2⟩\n  · refine le_trans ?_ (bert_primorial_le (2 * n / 3))\n    refine (Finset.prod_le_prod' fun p hp => (?_ : f p ≤ p)).trans ?_\n    · obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hp\n      refine (pow_right_mono₀ (Finset.mem_filter.1 h1).2.one_lt.le ?_).trans (pow_one p).le\n      exact Nat.factorization_choose_le_one (not_le.1 h2)\n    refine Finset.prod_le_prod_of_subset_of_one_le' (Finset.filter_subset _ _) ?_\n    exact fun p hp _ => (Finset.mem_filter.1 hp).2.one_lt.le\n\ntheorem bert_step (t : ℕ) (h : 9 ≤ t) : (t+1)^6 ≤ 2*t^6 := by\n  have h1 : 9*(t+1) ≤ 10*t := by omega\n  have h2 := Nat.pow_le_pow_left h1 6\n  rw [Nat.mul_pow, Nat.mul_pow] at h2\n  have h3 : 9^6*(t+1)^6 ≤ 9^6*(2*t^6) := by\n    calc 9^6*(t+1)^6 ≤ 10^6*t^6 := h2\n      _ ≤ 9^6*(2*t^6) := by rw [← Nat.mul_assoc]; exact Nat.mul_le_mul_right _ (by norm_num)\n  exact Nat.le_of_mul_le_mul_left h3 (by norm_num)\n\ntheorem bert_pow6 (s : ℕ) (h : 31 ≤ s) : (s+1)^6 ≤ 2^(s-1) := by\n  induction s, h using Nat.le_induction with\n  | base => norm_num\n  | succ k hk ih =>\n    have := bert_step (k+1) (by omega)\n    have e : k + 1 - 1 = (k - 1) + 1 := by omega\n    rw [e, show 2^((k-1)+1) = 2^(k-1)*2 from Nat.pow_succ ..]\n    omega\n\ntheorem bert_A3 (n : ℕ) (hs : 31 ≤ sqrt (2 * n)) :\n    (n * (2 * n) ^ sqrt (2 * n)) ^ 3 ≤ 4 ^ n := by\n  set s := sqrt (2 * n) with hsdef\n  have hlt : 2 * n < (s+1)^2 := by\n    have := Nat.lt_succ_sqrt' (2 * n); rw [← hsdef] at this; exact this\n  have hle : s * s ≤ 2 * n := by\n    have := Nat.sqrt_le (2 * n); rw [← hsdef] at this; exact this\n  have hA : n * (2 * n) ^ s ≤ (s+1)^(2*s+2) := by\n    have h1 : n ≤ (s+1)^2 := by omega\n    have h2 : (2*n)^s ≤ ((s+1)^2)^s := Nat.pow_le_pow_left (by omega) s\n    calc n * (2 * n) ^ s ≤ (s+1)^2 * ((s+1)^2)^s := Nat.mul_le_mul h1 h2\n      _ = (s+1)^(2*s+2) := by rw [← Nat.pow_mul, ← Nat.pow_add]; congr 1; omega\n  calc (n * (2 * n) ^ s) ^ 3 ≤ ((s+1)^(2*s+2))^3 := Nat.pow_le_pow_left hA 3\n    _ = ((s+1)^6)^(s+1) := by rw [← Nat.pow_mul, ← Nat.pow_mul]; congr 1; ring\n    _ ≤ (2^(s-1))^(s+1) := Nat.pow_le_pow_left (bert_pow6 s hs) _\n    _ = 2^((s-1)*(s+1)) := by rw [Nat.pow_mul]\n    _ ≤ 2^(2*n) := by\n        apply Nat.pow_le_pow_right (by norm_num)\n        have : (s-1)*(s+1) ≤ s * s := by\n          obtain ⟨k, hk⟩ : ∃ k, s = k + 1 := ⟨s-1, by omega⟩\n          rw [hk, Nat.add_sub_cancel]\n          ring_nf; omega\n        omega\n    _ = 4^n := by rw [Nat.pow_mul]\n\ntheorem bert_four_pow (n : ℕ) (hn : 4 ≤ n) : 4 ^ n < n * centralBinom n := by\n  induction n, hn using Nat.le_induction with\n  | base => decide\n  | succ k hk ih =>\n    rw [Nat.succ_mul_centralBinom_succ, Nat.pow_succ]\n    have h1 : 4 ^ k * 4 < k * centralBinom k * 4 := by omega\n    have h2 : k * centralBinom k * 4 ≤ 2 * (2 * k + 1) * centralBinom k := by\n      rw [Nat.mul_right_comm]; exact Nat.mul_le_mul_right _ (by omega)\n    exact Nat.lt_of_lt_of_le h1 h2\n\ntheorem bert_large (n : ℕ) (hn : 481 ≤ n) : ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n := by\n  by_contra no_prime\n  have hs : 31 ≤ sqrt (2 * n) := Nat.le_sqrt'.mpr (by omega)\n  have h1 := bert_four_pow n (by omega)\n  have h2 := bert_centralBinom_le n (by omega) no_prime\n  have h3 := bert_A3 n hs\n  set A := n * (2 * n) ^ sqrt (2 * n) with hA\n  set m := n - 2 * n / 3 with hm\n  have hm3 : n ≤ 3 * m := by\n    have := Nat.div_mul_le_self (2 * n) 3\n    omega\n  have h4 : A ≤ 4 ^ m := by\n    have : A ^ 3 ≤ (4 ^ m) ^ 3 := by\n      rw [← Nat.pow_mul]\n      exact h3.trans (Nat.pow_le_pow_right (by norm_num) (by omega))\n    exact (Nat.pow_le_pow_iff_left (by norm_num)).mp this\n  have h5 : n * centralBinom n ≤ A * 4 ^ (2 * n / 3) := by\n    rw [hA, Nat.mul_assoc]; exact Nat.mul_le_mul_left _ h2\n  have h6 : A * 4 ^ (2 * n / 3) ≤ 4 ^ n := by\n    calc A * 4 ^ (2 * n / 3) ≤ 4 ^ m * 4 ^ (2 * n / 3) := Nat.mul_le_mul_right _ h4\n      _ = 4 ^ n := by\n        rw [← Nat.pow_add]; congr 1\n        have := Nat.div_le_self (2 * n) 3\n        have := Nat.div_mul_le_self (2 * n) 3\n        omega\n  omega\n\ntheorem Lemma.bertrand :\n    ∀ n : ℕ, n ≠ 0 → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n := by\n  intro n hn\n  by_cases h : 481 ≤ n\n  · exact bert_large n h\n  by_cases h1 : n ≤ 1\n  · exact ⟨2, by decide +kernel, by omega, by omega⟩\n  by_cases h2 : n ≤ 2\n  · exact ⟨3, by decide +kernel, by omega, by omega⟩\n  by_cases h3 : n ≤ 4\n  · exact ⟨5, by decide +kernel, by omega, by omega⟩\n  by_cases h4 : n ≤ 6\n  · exact ⟨7, by decide +kernel, by omega, by omega⟩\n  by_cases h5 : n ≤ 12\n  · exact ⟨13, by decide +kernel, by omega, by omega⟩\n  by_cases h6 : n ≤ 22\n  · exact ⟨23, by decide +kernel, by omega, by omega⟩\n  by_cases h7 : n ≤ 42\n  · exact ⟨43, by decide +kernel, by omega, by omega⟩\n  by_cases h8 : n ≤ 82\n  · exact ⟨83, by decide +kernel, by omega, by omega⟩\n  by_cases h9 : n ≤ 162\n  · exact ⟨163, by decide +kernel, by omega, by omega⟩\n  by_cases h10 : n ≤ 316\n  · exact ⟨317, by decide +kernel, by omega, by omega⟩\n  · exact ⟨631, by decide +kernel, by omega, by omega⟩\n","Lemma.fermat_little":"import Mathlib.Data.Nat.Choose.Sum\nimport Mathlib.Data.Nat.Choose.Dvd\n\ntheorem Lemma.fermat_little_key (p a : ℕ) (hp : p.Prime) :\n    ∃ t, (a + 1) ^ p = a ^ p + 1 + p * t := by\n  obtain ⟨m, rfl⟩ : ∃ m, p = m + 1 := ⟨p - 1, by have := hp.two_le; omega⟩\n  rw [add_pow, Finset.sum_range_succ, Finset.sum_range_succ']\n  simp only [Nat.cast_id]\n  have hd : (m + 1) ∣ ∑ k ∈ Finset.range m,\n      a ^ (k + 1) * 1 ^ (m + 1 - (k + 1)) * (m + 1).choose (k + 1) := by\n    apply Finset.dvd_sum\n    intro k hk\n    rw [Finset.mem_range] at hk\n    exact Dvd.dvd.mul_left (hp.dvd_choose_self (by omega) (by omega)) _\n  obtain ⟨t, ht⟩ := hd\n  refine ⟨t, ?_⟩\n  rw [ht]\n  simp only [pow_zero, one_pow, mul_one, one_mul, Nat.choose_zero_right, Nat.choose_self,\n    Nat.sub_self]\n  generalize a ^ (m + 1) = x\n  generalize (m + 1) * t = y\n  omega\n\ntheorem Lemma.fermat_little :\n    ∀ p a : ℕ, p.Prime → a ^ p % p = a % p := by\n  intro p a hp\n  induction a with\n  | zero =>\n    rw [zero_pow hp.ne_zero]\n  | succ n ih =>\n    obtain ⟨t, ht⟩ := Lemma.fermat_little_key p n hp\n    rw [ht, Nat.add_mul_mod_self_left, Nat.add_mod, ih, ← Nat.add_mod]\n","Lemma.four_squares":"import Mathlib.Data.ZMod.Basic\n\nlemma fs_four_int : (4:ℤ) = 2 + 2 := by omega\nlemma fs_four_nat : (4:ℕ) = 2 + 2 := by omega\n\nmacro \"ac_ring\" : tactic => `(tactic| (simp only [sq, two_mul, mul_two, fs_four_int, fs_four_nat, mul_one, one_mul, add_mul, mul_add, sub_mul, mul_sub, mul_assoc, mul_comm, mul_left_comm] <;> omega))\n\nlemma fs_euler (a b c d x y z w : ℤ) :\n    (a^2+b^2+c^2+d^2)*(x^2+y^2+z^2+w^2) =\n      (a*x+b*y+c*z+d*w)^2 + (a*y-b*x+c*w-d*z)^2 + (a*z-b*w-c*x+d*y)^2\n        + (a*w+b*z-c*y-d*x)^2 := by\n  simp only [sq, add_mul, mul_add, sub_mul, mul_sub, mul_assoc, mul_comm, mul_left_comm]\n  omega\n\nlemma fs_mul (m n : ℕ) (hm : ∃ a b c d : ℤ, a^2+b^2+c^2+d^2 = (m:ℤ))\n    (hn : ∃ a b c d : ℤ, a^2+b^2+c^2+d^2 = (n:ℤ)) :\n    ∃ a b c d : ℤ, a^2+b^2+c^2+d^2 = ((m*n : ℕ):ℤ) := by\n  obtain ⟨a, b, c, d, h1⟩ := hm\n  obtain ⟨x, y, z, w, h2⟩ := hn\n  refine ⟨a*x+b*y+c*z+d*w, a*y-b*x+c*w-d*z, a*z-b*w-c*x+d*y, a*w+b*z-c*y-d*x, ?_⟩\n  rw [Nat.cast_mul, ← h1, ← h2, fs_euler]\n\nlemma fs_sq_mod_two (a : ℤ) : a^2 % 2 = a % 2 := by\n  rcases Int.even_or_odd a with ⟨q, hq⟩ | ⟨q, hq⟩\n  · subst hq\n    have : (q+q)^2 = 2*(2*q^2) := by ac_ring\n    rw [this]; omega\n  · subst hq\n    have : (2*q+1)^2 = 2*(2*q^2+2*q) + 1 := by ac_ring\n    rw [this]; omega\n\nlemma fs_resid (x k : ℤ) (hk : 0 ≤ k) :\n    ∃ y t : ℤ, x = y + (2*k+1)*t ∧ -k ≤ y ∧ y ≤ k := by\n  refine ⟨(x+k)%(2*k+1) - k, (x+k)/(2*k+1), ?_, ?_, ?_⟩ <;>\n  · have h1 := Int.emod_def (x+k) (2*k+1)\n    have h2 := Int.emod_nonneg (x+k) (show (2*k+1) ≠ 0 by omega)\n    have h3 := Int.emod_lt_of_pos (x+k) (show (0:ℤ) < 2*k+1 by omega)\n    generalize (x+k)%(2*k+1) = a at *\n    generalize (2*k+1)*((x+k)/(2*k+1)) = b at *\n    omega\n\nlemma fs_sq_inj (p : ℕ) (hp : p.Prime) (hodd : p % 2 = 1) (i j : ℕ) (hi : i ≤ p/2) (hj : j ≤ p/2)\n    (h : ((i:ZMod p))^2 = ((j:ZMod p))^2) : i = j := by\n  have h' : (((i:ℤ)^2 : ℤ) : ZMod p) = (((j:ℤ)^2 : ℤ) : ZMod p) := by\n    push_cast; exact h\n  rw [ZMod.intCast_eq_intCast_iff_dvd_sub] at h'\n  have e : (j:ℤ)^2 - (i:ℤ)^2 = ((j:ℤ) - i) * ((j:ℤ) + i) := by ac_ring\n  rw [e, Int.natCast_dvd, Int.natAbs_mul] at h'\n  have hp2 := hp.two_le\n  rcases hp.dvd_mul.mp h' with h1 | h1\n  · have hlt : ((j:ℤ) - i).natAbs < p := by omega\n    have := Nat.eq_zero_of_dvd_of_lt h1 hlt\n    omega\n  · have hlt : ((j:ℤ) + i).natAbs < p := by omega\n    have := Nat.eq_zero_of_dvd_of_lt h1 hlt\n    omega\n\nlemma fs_pigeon (p : ℕ) (hp : p.Prime) (hodd : p % 2 = 1) :\n    ∃ x y : ℕ, x ≤ p/2 ∧ y ≤ p/2 ∧ p ∣ x^2+y^2+1 := by\n  haveI : NeZero p := ⟨hp.ne_zero⟩\n  by_contra hne\n  let f : Fin (p/2+1) ⊕ Fin (p/2+1) → ZMod p :=\n    Sum.elim (fun i => ((i.val : ℕ) : ZMod p)^2) (fun j => -1 - ((j.val : ℕ) : ZMod p)^2)\n  have key : ∀ i j : Fin (p/2+1), ((i.val:ℕ):ZMod p)^2 = -1 - ((j.val:ℕ):ZMod p)^2 → False := by\n    intro i j hij\n    apply hne\n    refine ⟨i.val, j.val, by omega, by omega, ?_⟩\n    rw [← CharP.cast_eq_zero_iff (ZMod p) p]\n    push_cast\n    rw [hij, sub_add_cancel, neg_add_cancel]\n  have hinj : Function.Injective f := by\n    intro a b hab\n    rcases a with i | i <;> rcases b with j | j\n    · simp only [f, Sum.elim_inl] at hab\n      have := fs_sq_inj p hp hodd i.val j.val (by omega) (by omega) hab\n      rw [Fin.ext this]\n    · simp only [f, Sum.elim_inl, Sum.elim_inr] at hab\n      exact (key i j hab).elim\n    · simp only [f, Sum.elim_inl, Sum.elim_inr] at hab\n      exact (key j i hab.symm).elim\n    · simp only [f, Sum.elim_inr] at hab\n      have hab' : ((i.val:ℕ):ZMod p)^2 = ((j.val:ℕ):ZMod p)^2 := sub_right_inj.mp hab\n      have := fs_sq_inj p hp hodd i.val j.val (by omega) (by omega) hab'\n      rw [Fin.ext this]\n  have := Fintype.card_le_of_injective f hinj\n  simp only [Fintype.card_sum, Fintype.card_fin, ZMod.card] at this\n  omega\n\nlemma fs_par (s1 s2 s3 s4 a1 a2 a3 a4 : ℤ) (e1 : s1 % 2 = a1 % 2) (e2 : s2 % 2 = a2 % 2)\n    (e3 : s3 % 2 = a3 % 2) (e4 : s4 % 2 = a4 % 2) (hev : (s1+s2+s3+s4) % 2 = 0) :\n    (a1 % 2 = a2 % 2 ∧ a3 % 2 = a4 % 2) ∨ (a1 % 2 = a3 % 2 ∧ a2 % 2 = a4 % 2)\n        ∨ (a1 % 2 = a4 % 2 ∧ a2 % 2 = a3 % 2) := by\n  omega\n\nlemma fs_halve (a b c d k p : ℤ) (hab : a % 2 = b % 2) (hcd : c % 2 = d % 2)\n    (h : a^2+b^2+c^2+d^2 = (2*k)*p) : ∃ a b c d : ℤ, a^2+b^2+c^2+d^2 = k*p := by\n  obtain ⟨u, hu⟩ : ∃ u, a + b = 2*u := ⟨(a+b)/2, by omega⟩\n  obtain ⟨v, hv⟩ : ∃ v, a - b = 2*v := ⟨(a-b)/2, by omega⟩\n  obtain ⟨w, hw⟩ : ∃ w, c + d = 2*w := ⟨(c+d)/2, by omega⟩\n  obtain ⟨z, hz⟩ : ∃ z, c - d = 2*z := ⟨(c-d)/2, by omega⟩\n  have ha : a = u + v := by omega\n  have hb : b = u - v := by omega\n  have hc : c = w + z := by omega\n  have hd : d = w - z := by omega\n  subst ha hb hc hd\n  refine ⟨u, v, w, z, ?_⟩\n  have : 2*(u^2+v^2+w^2+z^2) = 2*(k*p) := by\n    simp only [sq, two_mul, mul_two, fs_four_int, fs_four_nat, mul_one, one_mul, add_mul, mul_add, sub_mul, mul_sub, mul_assoc, mul_comm, mul_left_comm] at h ⊢\n    omega\n  omega\n\nlemma fs_prime (p : ℕ) (hp : p.Prime) : ∃ a b c d : ℤ, a^2+b^2+c^2+d^2 = (p:ℤ) := by\n  classical\n  rcases hp.eq_two_or_odd with h2 | hodd\n  · exact ⟨1, 1, 0, 0, by subst h2; simp⟩\n  obtain ⟨x, y, hx, hy, hdvd⟩ := fs_pigeon p hp hodd\n  obtain ⟨m, hm⟩ := hdvd\n  have hp2 := hp.two_le\n  have hmp : m < p := by\n    have h1 : x^2 ≤ (p/2)^2 := Nat.pow_le_pow_left hx 2\n    have h2 : y^2 ≤ (p/2)^2 := Nat.pow_le_pow_left hy 2\n    have h3 : p * p = 4*(p/2)^2 + 4*(p/2) + 1 := by\n      have : p = 2*(p/2)+1 := by omega\n      conv_lhs => rw [this]\n      ac_ring\n    have h4 : p * m < p * p := by\n      generalize (p/2)^2 = s at *\n      generalize p * m = t at *\n      generalize p * p = r at *\n      omega\n    exact Nat.lt_of_mul_lt_mul_left h4\n  let P : ℕ → Prop := fun m => 0 < m ∧ ∃ a b c d : ℤ, a^2+b^2+c^2+d^2 = (m:ℤ)*p\n  have hPm : P m := by\n    refine ⟨?_, (x:ℤ), (y:ℤ), 1, 0, ?_⟩\n    · rcases Nat.eq_zero_or_pos m with h0 | h0\n      · subst h0; simp at hm\n      · exact h0\n    · have : ((x^2+y^2+1 : ℕ) : ℤ) = ((p*m : ℕ) : ℤ) := by rw [hm]\n      push_cast at this\n      simp only [sq, two_mul, mul_two, fs_four_int, fs_four_nat, mul_one, one_mul, add_mul, mul_add, sub_mul, mul_sub, mul_assoc, mul_comm, mul_left_comm] at this ⊢\n      omega\n  have hex : ∃ m, P m := ⟨m, hPm⟩\n  have hspec := Nat.find_spec hex\n  have hmin : ∀ r, r < Nat.find hex → ¬ P r := fun r hr => Nat.find_min hex hr\n  have hle : Nat.find hex ≤ m := Nat.find_min' hex hPm\n  generalize Nat.find hex = M at hspec hmin hle\n  obtain ⟨hM0, a1, a2, a3, a4, hA⟩ := hspec\n  by_cases hM1 : M = 1\n  · subst hM1; exact ⟨a1, a2, a3, a4, by rw [hA]; simp⟩\n  exfalso\n  obtain ⟨k, hk | hk⟩ := Nat.even_or_odd' M\n  · -- even case\n    apply hmin k (by omega)\n    refine ⟨by omega, ?_⟩\n    have e1 := fs_sq_mod_two a1\n    have e2 := fs_sq_mod_two a2\n    have e3 := fs_sq_mod_two a3\n    have e4 := fs_sq_mod_two a4\n    have hA' : a1^2+a2^2+a3^2+a4^2 = (2*(k:ℤ))*p := by rw [hA, hk]; push_cast; rfl\n    have hev : (a1^2+a2^2+a3^2+a4^2) % 2 = 0 := by\n      rw [hA', mul_assoc]; omega\n    have hcases : (a1 % 2 = a2 % 2 ∧ a3 % 2 = a4 % 2) ∨ (a1 % 2 = a3 % 2 ∧ a2 % 2 = a4 % 2)\n        ∨ (a1 % 2 = a4 % 2 ∧ a2 % 2 = a3 % 2) := by\n      exact fs_par _ _ _ _ _ _ _ _ e1 e2 e3 e4 hev\n    rcases hcases with ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩\n    · exact fs_halve a1 a2 a3 a4 k p h1 h2 hA'\n    · exact fs_halve a1 a3 a2 a4 k p h1 h2 (by rw [← hA']; omega)\n    · exact fs_halve a1 a4 a2 a3 k p h1 h2 (by rw [← hA']; omega)\n  · -- odd case\n    have hk1 : 1 ≤ k := by omega\n    have hkz : (0:ℤ) ≤ k := by omega\n    obtain ⟨y1, t1, hx1, hl1, hu1⟩ := fs_resid a1 k hkz\n    obtain ⟨y2, t2, hx2, hl2, hu2⟩ := fs_resid a2 k hkz\n    obtain ⟨y3, t3, hx3, hl3, hu3⟩ := fs_resid a3 k hkz\n    obtain ⟨y4, t4, hx4, hl4, hu4⟩ := fs_resid a4 k hkz\n    have hMz : (M:ℤ) = 2*k+1 := by rw [hk]; push_cast; rfl\n    rw [← hMz] at hx1 hx2 hx3 hx4\n    subst hx1 hx2 hx3 hx4\n    -- divisibility of sum of y^2\n    have hdiv : (M:ℤ) ∣ y1^2+y2^2+y3^2+y4^2 := by\n      refine ⟨p - (2*(y1*t1+y2*t2+y3*t3+y4*t4) + (M:ℤ)*(t1^2+t2^2+t3^2+t4^2)), ?_⟩\n      simp only [sq, two_mul, mul_two, fs_four_int, fs_four_nat, mul_one, one_mul, add_mul, mul_add, sub_mul, mul_sub, mul_assoc, mul_comm, mul_left_comm] at hA ⊢\n      omega\n    obtain ⟨r, hr⟩ := hdiv\n    have s1 := sq_nonneg y1\n    have s2 := sq_nonneg y2\n    have s3 := sq_nonneg y3\n    have s4 := sq_nonneg y4\n    have b1 : y1^2 ≤ (k:ℤ)^2 := sq_le_sq' hl1 hu1\n    have b2 : y2^2 ≤ (k:ℤ)^2 := sq_le_sq' hl2 hu2\n    have b3 : y3^2 ≤ (k:ℤ)^2 := sq_le_sq' hl3 hu3\n    have b4 : y4^2 ≤ (k:ℤ)^2 := sq_le_sq' hl4 hu4\n    have hMM : (M:ℤ)*M = 4*(k:ℤ)^2 + 4*k + 1 := by rw [hMz]; ac_ring\n    have hMpos : (0:ℤ) < M := by omega\n    have hr0 : 0 ≤ r := by\n      by_contra hneg\n      have : (M:ℤ) * r < 0 := Int.mul_neg_of_pos_of_neg hMpos (by omega)\n      omega\n    have hrM : r < M := by\n      by_contra hge\n      have : (M:ℤ) * M ≤ M * r := Int.mul_le_mul_of_nonneg_left (by omega) (by omega)\n      generalize (k:ℤ)^2 = K at *\n      generalize (M:ℤ) * M = Q at *\n      generalize (M:ℤ) * r = R at *\n      omega\n    rcases (show r = 0 ∨ 0 < r by omega) with hr00 | hrpos\n    · -- all y = 0, so M ∣ p\n      subst hr00\n      have z1 : y1 = 0 := by\n        have : y1^2 = 0 := by rw [mul_zero] at hr; omega\n        exact pow_eq_zero_iff two_ne_zero |>.mp this\n      have z2 : y2 = 0 := by\n        have : y2^2 = 0 := by rw [mul_zero] at hr; omega\n        exact pow_eq_zero_iff two_ne_zero |>.mp this\n      have z3 : y3 = 0 := by\n        have : y3^2 = 0 := by rw [mul_zero] at hr; omega\n        exact pow_eq_zero_iff two_ne_zero |>.mp this\n      have z4 : y4 = 0 := by\n        have : y4^2 = 0 := by rw [mul_zero] at hr; omega\n        exact pow_eq_zero_iff two_ne_zero |>.mp this\n      subst z1 z2 z3 z4\n      have hMd : (M:ℤ) * ((M:ℤ)*(t1^2+t2^2+t3^2+t4^2)) = (M:ℤ) * p := by\n        rw [← hA]; ac_ring\n      have hMd' := mul_left_cancel₀ (show (M:ℤ) ≠ 0 by omega) hMd\n      have hdvd : (M:ℤ) ∣ (p:ℤ) := ⟨_, hMd'.symm⟩\n      have hdvdN : M ∣ p := Int.natCast_dvd_natCast.mp hdvd\n      rcases hp.eq_one_or_self_of_dvd M hdvdN with h | h <;> omega\n    · -- descent\n      apply hmin r.toNat (by omega)\n      refine ⟨by omega, ?_⟩\n      refine ⟨r + (y1*t1+y2*t2+y3*t3+y4*t4), t1*y2-t2*y1+t3*y4-t4*y3,\n        t1*y3-t2*y4-t3*y1+t4*y2, t1*y4+t2*y3-t3*y2-t4*y1, ?_⟩\n      rw [Int.toNat_of_nonneg hr0]\n      have E := fs_euler (y1 + M*t1) (y2 + M*t2) (y3 + M*t3) (y4 + M*t4) y1 y2 y3 y4\n      rw [hA, hr] at E\n      have f1 : (y1 + M*t1)*y1 + (y2 + M*t2)*y2 + (y3 + M*t3)*y3 + (y4 + M*t4)*y4\n          = (M:ℤ) * (r + (y1*t1+y2*t2+y3*t3+y4*t4)) := by\n        have hr' := hr\n        simp only [sq, two_mul, mul_two, fs_four_int, fs_four_nat, mul_one, one_mul, add_mul, mul_add, sub_mul, mul_sub, mul_assoc, mul_comm, mul_left_comm] at hr' ⊢\n        omega\n      have f2 : (y1 + M*t1)*y2 - (y2 + M*t2)*y1 + (y3 + M*t3)*y4 - (y4 + M*t4)*y3\n          = (M:ℤ) * (t1*y2-t2*y1+t3*y4-t4*y3) := by ac_ring\n      have f3 : (y1 + M*t1)*y3 - (y2 + M*t2)*y4 - (y3 + M*t3)*y1 + (y4 + M*t4)*y2\n          = (M:ℤ) * (t1*y3-t2*y4-t3*y1+t4*y2) := by ac_ring\n      have f4 : (y1 + M*t1)*y4 + (y2 + M*t2)*y3 - (y3 + M*t3)*y2 - (y4 + M*t4)*y1\n          = (M:ℤ) * (t1*y4+t2*y3-t3*y2-t4*y1) := by ac_ring\n      rw [f1, f2, f3, f4] at E\n      have E2 : ((M:ℤ)*M) * ((r + (y1*t1+y2*t2+y3*t3+y4*t4))^2 + (t1*y2-t2*y1+t3*y4-t4*y3)^2\n          + (t1*y3-t2*y4-t3*y1+t4*y2)^2 + (t1*y4+t2*y3-t3*y2-t4*y1)^2)\n          = ((M:ℤ)*M) * (r * p) := by\n        have E3 : ((M:ℤ)*M) * ((r + (y1*t1+y2*t2+y3*t3+y4*t4))^2 + (t1*y2-t2*y1+t3*y4-t4*y3)^2\n            + (t1*y3-t2*y4-t3*y1+t4*y2)^2 + (t1*y4+t2*y3-t3*y2-t4*y1)^2)\n            = ((M:ℤ) * (r + (y1*t1+y2*t2+y3*t3+y4*t4)))^2 + ((M:ℤ) * (t1*y2-t2*y1+t3*y4-t4*y3))^2\n            + ((M:ℤ) * (t1*y3-t2*y4-t3*y1+t4*y2))^2 + ((M:ℤ) * (t1*y4+t2*y3-t3*y2-t4*y1))^2 := by\n          ac_ring\n        rw [E3, ← E]\n        ac_ring\n      exact mul_left_cancel₀ (show (M:ℤ)*M ≠ 0 from (mul_ne_zero (by omega) (by omega))) E2\n\nlemma fs_int : ∀ n : ℕ, ∃ a b c d : ℤ, a^2+b^2+c^2+d^2 = (n:ℤ) := by\n  intro n\n  induction n using Nat.strong_induction_on with\n  | _ n ih =>\n    rcases n with _ | _ | n\n    · exact ⟨0, 0, 0, 0, by simp⟩\n    · exact ⟨1, 0, 0, 0, by simp⟩\n    · have hp := Nat.minFac_prime (show n + 2 ≠ 1 by omega)\n      obtain ⟨q, hq⟩ := Nat.minFac_dvd (n+2)\n      have hq0 : 0 < q := by\n        rcases Nat.eq_zero_or_pos q with h | h\n        · rw [h, Nat.mul_zero] at hq; omega\n        · exact h\n      have h2 : 2 * q ≤ (n+2).minFac * q := Nat.mul_le_mul_right q hp.two_le\n      have hlt : q < n + 2 := by\n        generalize (n+2).minFac * q = t at *\n        omega\n      rw [hq]\n      exact fs_mul _ _ (fs_prime _ hp) (ih q hlt)\n\ntheorem Lemma.four_squares :\n    ∀ n : ℕ, ∃ a b c d : ℕ, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n := by\n  intro n\n  obtain ⟨a, b, c, d, h⟩ := fs_int n\n  refine ⟨a.natAbs, b.natAbs, c.natAbs, d.natAbs, ?_⟩\n  have h1 : ((a.natAbs^2 + b.natAbs^2 + c.natAbs^2 + d.natAbs^2 : ℕ) : ℤ) = n := by\n    simp only [Nat.cast_add, Nat.cast_pow, Int.natCast_natAbs, sq_abs]\n    exact h\n  exact_mod_cast h1\n","Lemma.quadratic_reciprocity":"import Mathlib.FieldTheory.Finite.Basic\n\nopen Finset\n\nnamespace QR\n\n/-- the \"absolute least residue\" of a*i mod p -/\ndef m (p a i : ℕ) : ℕ := min ((a * i) % p) (p - (a * i) % p)\n\nlemma r_pos (p a i : ℕ) (hp : p.Prime) (ha : ¬ p ∣ a) (h1 : 1 ≤ i) (h2 : i < p) :\n    0 < (a * i) % p := by\n  rcases Nat.eq_zero_or_pos ((a * i) % p) with h | h\n  · exfalso\n    have hd : p ∣ a * i := Nat.dvd_of_mod_eq_zero h\n    rcases (Nat.Prime.dvd_mul hp).mp hd with h' | h'\n    · exact ha h'\n    · have := Nat.le_of_dvd (by omega) h'\n      omega\n  · exact h\n\nlemma odd_p (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) : p % 2 = 1 := by\n  rcases hp.eq_two_or_odd with h | h\n  · exact absurd h hp2\n  · exact h\n\n-- L0 : bijection\ntheorem m_mem (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :\n    ∀ i ∈ Ico 1 (p / 2 + 1), m p a i ∈ Ico 1 (p / 2 + 1) := by\n  intro i hi\n  rw [Finset.mem_Ico] at hi\n  have hodd := odd_p p hp hp2\n  have hr := r_pos p a i hp ha hi.1 (by omega)\n  have hlt := Nat.mod_lt (a * i) hp.pos\n  rw [Finset.mem_Ico]\n  unfold m\n  constructor\n  · apply le_min <;> omega\n  · have := min_le_left ((a * i) % p) (p - (a * i) % p)\n    have := min_le_right ((a * i) % p) (p - (a * i) % p)\n    rcases le_total ((a * i) % p) (p - (a * i) % p) with h | h\n    · rw [min_eq_left h]; omega\n    · rw [min_eq_right h]; omega\n\ntheorem m_inj (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :\n    Set.InjOn (m p a) (Ico 1 (p / 2 + 1) : Set ℕ) := by\n  intro i hi j hj h\n  simp only [Finset.coe_Ico, Set.mem_Ico, Finset.mem_coe, Finset.mem_Ico] at hi hj\n  have hodd := odd_p p hp hp2\n  have hri := r_pos p a i hp ha hi.1 (by omega)\n  have hrj := r_pos p a j hp ha hj.1 (by omega)\n  have hlti := Nat.mod_lt (a * i) hp.pos\n  have hltj := Nat.mod_lt (a * j) hp.pos\n  unfold m at h\n  have key : (a * i) % p = (a * j) % p ∨ (a * i) % p + (a * j) % p = p := by\n    rcases le_total ((a * i) % p) (p - (a * i) % p) with h1 | h1 <;>\n    rcases le_total ((a * j) % p) (p - (a * j) % p) with h2 | h2 <;>\n    simp only [min_eq_left h1, min_eq_right h1, min_eq_left h2, min_eq_right h2] at h <;>\n    omega\n  haveI := Fact.mk hp\n  rcases key with k | k\n  · have e := (ZMod.natCast_eq_natCast_iff' (a * i) (a * j) p).mpr k\n    push_cast at e\n    have ha' : (a : ZMod p) ≠ 0 := by\n      rwa [Ne, CharP.cast_eq_zero_iff (ZMod p) p]\n    have e2 := mul_left_cancel₀ ha' e\n    have e3 := (ZMod.natCast_eq_natCast_iff' i j p).mp e2\n    rwa [Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega)] at e3\n  · exfalso\n    have hz : (a * (i + j)) % p = 0 := by\n      rw [Nat.mul_add, Nat.add_mod, k, Nat.mod_self]\n    have hd : p ∣ a * (i + j) := Nat.dvd_of_mod_eq_zero hz\n    rcases (Nat.Prime.dvd_mul hp).mp hd with h' | h'\n    · exact ha h'\n    · have := Nat.le_of_dvd (by omega) h'\n      omega\n\ntheorem m_image (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :\n    (Ico 1 (p / 2 + 1)).image (m p a) = Ico 1 (p / 2 + 1) := by\n  apply Finset.eq_of_subset_of_card_le\n  · intro x hx\n    rw [Finset.mem_image] at hx\n    obtain ⟨i, hi, rfl⟩ := hx\n    exact m_mem p a hp hp2 ha i hi\n  · rw [Finset.card_image_of_injOn (m_inj p a hp hp2 ha)]\n\nlemma term (p a i : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) (hi : i ∈ Ico 1 (p / 2 + 1)) :\n    ((a : ZMod p) * (i : ZMod p)) =\n      (if p / 2 < (a * i) % p then (-1 : ZMod p) else 1) * ((m p a i : ℕ) : ZMod p) := by\n  rw [Finset.mem_Ico] at hi\n  have hodd := odd_p p hp hp2\n  have hr := r_pos p a i hp ha hi.1 (by omega)\n  have hlt := Nat.mod_lt (a * i) hp.pos\n  have e : ((a : ZMod p) * (i : ZMod p)) = (((a * i) % p : ℕ) : ZMod p) := by\n    rw [ZMod.natCast_mod]; push_cast; ring\n  rw [e]\n  unfold m\n  split_ifs with h\n  · rw [min_eq_right (by omega), Nat.cast_sub (by omega), ZMod.natCast_self]\n    ring\n  · rw [min_eq_left (by omega)]\n    ring\n\n-- L2a : Gauss lemma\ntheorem gauss (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :\n    (a : ZMod p) ^ (p / 2) =\n      (-1) ^ ((Ico 1 (p / 2 + 1)).filter (fun i => p / 2 < (a * i) % p)).card := by\n  haveI := Fact.mk hp\n  set S := Ico 1 (p / 2 + 1) with hS\n  have hcard : S.card = p / 2 := by simp [hS]\n  have h1 : ∏ i ∈ S, ((a : ZMod p) * (i : ZMod p)) = (a : ZMod p) ^ (p / 2) * ∏ i ∈ S, (i : ZMod p) := by\n    rw [Finset.prod_mul_distrib, Finset.prod_const, hcard]\n  have h2 : ∏ i ∈ S, ((a : ZMod p) * (i : ZMod p)) =\n      (-1) ^ (S.filter (fun i => p / 2 < (a * i) % p)).card * ∏ i ∈ S, (i : ZMod p) := by\n    rw [Finset.prod_congr rfl (fun i hi => term p a i hp hp2 ha hi), Finset.prod_mul_distrib,\n      Finset.prod_ite, Finset.prod_const, Finset.prod_const_one, mul_one]\n    congr 1\n    have := Finset.prod_image (s := S) (g := m p a) (f := fun j : ℕ => ((j : ℕ) : ZMod p))\n      (m_inj p a hp hp2 ha)\n    rw [← this, hS, m_image p a hp hp2 ha]\n  have hne : ∏ i ∈ S, (i : ZMod p) ≠ 0 := by\n    rw [Finset.prod_ne_zero_iff]\n    intro i hi\n    rw [hS, Finset.mem_Ico] at hi\n    rw [Ne, CharP.cast_eq_zero_iff (ZMod p) p]\n    intro hd\n    have := Nat.le_of_dvd (by omega) hd\n    have := odd_p p hp hp2\n    omega\n  exact mul_right_cancel₀ hne (h1.symm.trans h2)\n\n-- L2b : Eisenstein parity\ntheorem eisenstein_parity (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a)\n    (hodd : a % 2 = 1) :\n    ((Ico 1 (p / 2 + 1)).filter (fun i => p / 2 < (a * i) % p)).card % 2 =\n      (∑ i ∈ Ico 1 (p / 2 + 1), (a * i) / p) % 2 := by\n  have hp1 : p % 2 = 1 := by\n    rcases Nat.mod_two_eq_zero_or_one p with h | h\n    · rcases hp.eq_one_or_self_of_dvd 2 (Nat.dvd_of_mod_eq_zero h) with h' | h' <;> omega\n    · exact h\n  have hp0 : 0 < p := hp.pos\n  set s := Ico 1 (p / 2 + 1) with hs\n  set L := s.filter (fun i => p / 2 < (a * i) % p) with hL\n  -- sum of m equals sum of i\n  have hM : ∑ i ∈ s, m p a i = ∑ i ∈ s, i := by\n    have h1 := m_image p a hp hp2 ha\n    have h2 := m_inj p a hp hp2 ha\n    rw [hs]\n    conv_rhs => rw [← h1]\n    rw [Finset.sum_image (fun x hx y hy hxy => h2 (by simpa using hx) (by simpa using hy) hxy)]\n  have hmL : ∀ i ∈ L, m p a i + (a * i) % p = p := by\n    intro i hi\n    have hi' := (Finset.mem_filter.mp hi).2\n    have hr : (a * i) % p < p := Nat.mod_lt _ hp0\n    unfold m\n    rw [Nat.min_def]; split_ifs <;> omega\n  have hmN : ∀ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), m p a i = (a * i) % p := by\n    intro i hi\n    have hi' := (Finset.mem_filter.mp hi).2\n    have hr : (a * i) % p < p := Nat.mod_lt _ hp0\n    unfold m\n    rw [Nat.min_def]; split_ifs <;> omega\n  have hsplitM := Finset.sum_filter_add_sum_filter_not s (fun i => p / 2 < (a * i) % p) (m p a)\n  have hsplitR := Finset.sum_filter_add_sum_filter_not s (fun i => p / 2 < (a * i) % p)\n    (fun i => (a * i) % p)\n  have hNsum : ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), m p a i\n      = ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), (a * i) % p :=\n    Finset.sum_congr rfl hmN\n  have hLsum : ∑ i ∈ L, m p a i + ∑ i ∈ L, (a * i) % p = L.card * p := by\n    rw [← Finset.sum_add_distrib, Finset.sum_congr rfl hmL, Finset.sum_const, smul_eq_mul]\n  have hdiv : a * ∑ i ∈ s, i = p * ∑ i ∈ s, (a * i) / p + ∑ i ∈ s, (a * i) % p := by\n    rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib]\n    exact Finset.sum_congr rfl (fun i _ => (Nat.div_add_mod (a * i) p).symm)\n  rw [← hL] at hsplitM hsplitR\n  generalize ∑ i ∈ s, i = S at *\n  generalize ∑ i ∈ s, (a * i) / p = F at *\n  generalize ∑ i ∈ s, (a * i) % p = R at *\n  generalize ∑ i ∈ s, m p a i = M at *\n  generalize ∑ i ∈ L, m p a i = ML at *\n  generalize ∑ i ∈ L, (a * i) % p = RL at *\n  generalize ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), m p a i = MN at *\n  generalize ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), (a * i) % p = RN at *\n  generalize L.card = c at *\n  obtain ⟨a', rfl⟩ : ∃ a', a = 2 * a' + 1 := ⟨a / 2, by omega⟩\n  obtain ⟨p', rfl⟩ : ∃ p', p = 2 * p' + 1 := ⟨p / 2, by omega⟩\n  have e1 : (2 * a' + 1) * S = 2 * (a' * S) + S := by ring\n  have e2 : c * (2 * p' + 1) = 2 * (c * p') + c := by ring\n  have e3 : (2 * p' + 1) * F = 2 * (p' * F) + F := by ring\n  rw [e1, e3] at hdiv\n  rw [e2] at hLsum\n  generalize a' * S = X at *\n  generalize c * p' = Y at *\n  generalize p' * F = Z at *\n  omega\n\n-- L1 : lattice count\ntheorem lattice_count (a b n : ℕ) (hb : 0 < b) (hn : a / b ≤ n) (hnd : ¬ b ∣ a) :\n    ((Ico 1 (n + 1)).filter (fun j => b * j < a)).card = a / b := by\n  have : (Ico 1 (n + 1)).filter (fun j => b * j < a) = Ico 1 (a / b + 1) := by\n    ext j\n    simp only [mem_filter, mem_Ico]\n    have h1 : j ≤ a / b ↔ j * b ≤ a := Nat.le_div_iff_mul_le hb\n    have h2 : b * j ≠ a := fun h => hnd ⟨j, h.symm⟩\n    have h3 : j * b = b * j := Nat.mul_comm j b\n    constructor\n    · rintro ⟨⟨h4, h5⟩, h6⟩\n      refine ⟨h4, ?_⟩\n      have : j ≤ a / b := h1.mpr (by omega)\n      omega\n    · rintro ⟨h4, h5⟩\n      have : j * b ≤ a := h1.mp (by omega)\n      refine ⟨⟨h4, by omega⟩, by omega⟩\n  rw [this]\n  simp\n\ntheorem lattice_bound (p q i : ℕ) (hp : p % 2 = 1) (hq : q % 2 = 1) (hi : i ≤ p / 2) :\n    q * i / p ≤ q / 2 := by\n  have hp0 : 0 < p := by omega\n  have := (Nat.div_lt_iff_lt_mul hp0 (x := q * i) (y := q / 2 + 1)).mpr\n  suffices h : q * i < (q / 2 + 1) * p by have := this h; omega\n  obtain ⟨a, rfl⟩ : ∃ a, p = 2 * a + 1 := ⟨p / 2, by omega⟩\n  obtain ⟨b, rfl⟩ : ∃ b, q = 2 * b + 1 := ⟨q / 2, by omega⟩\n  have ha : (2 * a + 1) / 2 = a := by omega\n  have hb : (2 * b + 1) / 2 = b := by omega\n  rw [ha] at hi\n  rw [hb]\n  have : (2 * b + 1) * i ≤ (2 * b + 1) * a := Nat.mul_le_mul_left _ hi\n  nlinarith\n\ntheorem lattice_nd (p q i : ℕ) (hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q) (hi1 : 1 ≤ i)\n    (hi : i ≤ p / 2) : ¬ p ∣ q * i := by\n  intro h\n  rcases (Nat.Prime.dvd_mul hp).mp h with h | h\n  · exact hpq ((Nat.prime_dvd_prime_iff_eq hp hq).mp h)\n  · have := Nat.le_of_dvd (by omega) h\n    omega\n\ntheorem lattice (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q) (hp2 : p ≠ 2) (hq2 : q ≠ 2) :\n    (∑ i ∈ Ico 1 (p / 2 + 1), (q * i) / p) + (∑ j ∈ Ico 1 (q / 2 + 1), (p * j) / q)\n      = (p / 2) * (q / 2) := by\n  have hpo : p % 2 = 1 := Nat.odd_iff.mp (hp.odd_of_ne_two hp2)\n  have hqo : q % 2 = 1 := Nat.odd_iff.mp (hq.odd_of_ne_two hq2)\n  have key : ∀ i ∈ Ico 1 (p / 2 + 1), ∀ j ∈ Ico 1 (q / 2 + 1), q * i ≠ p * j := by\n    intro i hi j _ h\n    rw [mem_Ico] at hi\n    exact lattice_nd p q i hp hq hpq (by omega) (by omega) ⟨j, h⟩\n  symm\n  calc (p / 2) * (q / 2) = ∑ i ∈ Ico 1 (p / 2 + 1), ∑ j ∈ Ico 1 (q / 2 + 1), (1 : ℕ) := by simp\n    _ = ∑ i ∈ Ico 1 (p / 2 + 1), ∑ j ∈ Ico 1 (q / 2 + 1),\n          ((if p * j < q * i then 1 else 0) + (if q * i < p * j then 1 else 0)) := by\n        refine sum_congr rfl fun i hi => sum_congr rfl fun j hj => ?_\n        have := key i hi j hj\n        split_ifs <;> omega\n    _ = ∑ i ∈ Ico 1 (p / 2 + 1), ∑ j ∈ Ico 1 (q / 2 + 1), (if p * j < q * i then 1 else 0)\n        + ∑ j ∈ Ico 1 (q / 2 + 1), ∑ i ∈ Ico 1 (p / 2 + 1), (if q * i < p * j then 1 else 0) := by\n        rw [sum_comm (s := Ico 1 (q / 2 + 1))]\n        simp only [sum_add_distrib]\n    _ = _ := by\n        congr 1\n        · refine sum_congr rfl fun i hi => ?_\n          rw [mem_Ico] at hi\n          rw [← card_filter]\n          exact lattice_count (q * i) p (q / 2) hp.pos (lattice_bound p q i hpo hqo (by omega))\n            (lattice_nd p q i hp hq hpq (by omega) (by omega))\n        · refine sum_congr rfl fun j hj => ?_\n          rw [mem_Ico] at hj\n          rw [← card_filter]\n          exact lattice_count (p * j) q (p / 2) hq.pos (lattice_bound q p j hqo hpo (by omega))\n            (lattice_nd q p j hq hp (Ne.symm hpq) (by omega) (by omega))\n\ntheorem euler (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :\n    (∃ x : ℕ, x ^ 2 % p = a % p) ↔ (a : ZMod p) ^ (p / 2) = 1 := by\n  haveI := Fact.mk hp\n  have hne : (a : ZMod p) ≠ 0 := by\n    rwa [Ne, CharP.cast_eq_zero_iff (ZMod p) p a]\n  have hc : ringChar (ZMod p) ≠ 2 := by\n    rw [ZMod.ringChar_zmod_n]; exact hp2\n  have hsq := FiniteField.isSquare_iff hc hne\n  rw [ZMod.card] at hsq\n  rw [← hsq]\n  constructor\n  · rintro ⟨x, hx⟩\n    refine ⟨(x : ZMod p), ?_⟩\n    have : ((x ^ 2 : ℕ) : ZMod p) = (a : ZMod p) := (ZMod.natCast_eq_natCast_iff' _ _ _).mpr hx\n    rw [← this]; push_cast; ring\n  · rintro ⟨r, hr⟩\n    refine ⟨r.val, ?_⟩\n    rw [← ZMod.natCast_eq_natCast_iff']\n    push_cast\n    rw [ZMod.natCast_zmod_val, hr]; ring\n\ntheorem neg_one_pow_iff (p n : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) :\n    ((-1 : ZMod p) ^ n = 1) ↔ n % 2 = 0 := by\n  haveI : Fact (2 < p) := ⟨by have := hp.two_le; omega⟩\n  rcases Nat.even_or_odd n with h | h\n  · rw [h.neg_one_pow]; simp only [true_iff]; exact Nat.even_iff.mp h\n  · rw [h.neg_one_pow]\n    constructor\n    · intro h1; exact absurd h1 (ZMod.neg_one_ne_one)\n    · intro h2; have := Nat.odd_iff.mp h; omega\n\nend QR\n\ntheorem Lemma.quadratic_reciprocity :\n    ∀ p q : ℕ, p.Prime → q.Prime → p ≠ q → p ≠ 2 → q ≠ 2 → (((∃ x : ℕ, x ^ 2 % q = p % q) ↔ (∃ y : ℕ, y ^ 2 % p = q % p)) ↔ (p % 4 = 1 ∨ q % 4 = 1)) := by\n  intro p q hp hq hpq hp2 hq2\n  have hqp : ¬ q ∣ p := fun h => hpq ((Nat.prime_dvd_prime_iff_eq hq hp).mp h).symm\n  have hpq' : ¬ p ∣ q := fun h => hpq ((Nat.prime_dvd_prime_iff_eq hp hq).mp h)\n  have hp1 : p % 2 = 1 := by\n    rcases hp.eq_two_or_odd with h | h\n    · exact absurd h hp2\n    · exact h\n  have hq1 : q % 2 = 1 := by\n    rcases hq.eq_two_or_odd with h | h\n    · exact absurd h hq2\n    · exact h\n  rw [QR.euler q p hq hq2 hqp, QR.euler p q hp hp2 hpq', QR.gauss q p hq hq2 hqp,\n    QR.gauss p q hp hp2 hpq', QR.neg_one_pow_iff q _ hq hq2, QR.neg_one_pow_iff p _ hp hp2,\n    QR.eisenstein_parity q p hq hq2 hqp hp1, QR.eisenstein_parity p q hp hp2 hpq' hq1]\n  have hl := QR.lattice p q hp hq hpq hp2 hq2\n  have hm := Nat.mul_mod (p / 2) (q / 2) 2\n  have hs := Nat.add_mod (∑ i ∈ Finset.Ico 1 (p / 2 + 1), q * i / p)\n    (∑ j ∈ Finset.Ico 1 (q / 2 + 1), p * j / q) 2\n  rw [hl] at hs\n  rcases Nat.mod_two_eq_zero_or_one (p / 2) with h1 | h1 <;>\n  rcases Nat.mod_two_eq_zero_or_one (q / 2) with h2 | h2 <;>\n  simp only [h1, h2] at hm <;> omega\n\n","Lemma.two_squares":"import Mathlib.FieldTheory.Finite.Basic\n\ntheorem Lemma.two_squares :\n    ∀ p : ℕ, p.Prime → p % 4 = 1 → ∃ a b : ℕ, a ^ 2 + b ^ 2 = p := by\n  intro p hp h4\n  haveI := Fact.mk hp\n  obtain ⟨x, hx⟩ : IsSquare (-1 : ZMod p) := by\n    have hne : (-1 : ZMod p) ≠ 0 := neg_ne_zero.mpr one_ne_zero\n    have hc : ringChar (ZMod p) ≠ 2 := by\n      rw [ZMod.ringChar_zmod_n]; omega\n    rw [FiniteField.isSquare_iff hc hne, ZMod.card]\n    obtain ⟨t, ht⟩ : ∃ t, p / 2 = 2 * t := ⟨p / 4, by omega⟩\n    rw [ht, pow_mul]; simp\n  obtain ⟨m, hm⟩ : ∃ m, m = Nat.sqrt p := ⟨_, rfl⟩\n  have hm1 : m * m ≤ p := hm ▸ Nat.sqrt_le p\n  have hm2 : p < (m + 1) * (m + 1) := hm ▸ Nat.lt_succ_sqrt p\n  have hmp : m * m ≠ p := by\n    intro h\n    rcases hp.eq_one_or_self_of_dvd m (Dvd.intro m h) with h1 | h1\n    · subst h1; exact hp.one_lt.ne (by omega)\n    · subst h1\n      have := Nat.eq_of_mul_eq_mul_left hp.pos (h.trans (mul_one m).symm)\n      exact hp.one_lt.ne this.symm\n  have hcard : Fintype.card (ZMod p) < Fintype.card (Fin (m + 1) × Fin (m + 1)) := by\n    simp only [ZMod.card, Fintype.card_prod, Fintype.card_fin]; exact hm2\n  obtain ⟨⟨u1, v1⟩, ⟨u2, v2⟩, hne, heq⟩ := Fintype.exists_ne_map_eq_of_card_lt\n    (fun uv : Fin (m + 1) × Fin (m + 1) =>\n      ((uv.1 : ℕ) : ZMod p) + x * ((uv.2 : ℕ) : ZMod p)) hcard\n  simp only at heq\n  have hu1 := u1.isLt\n  have hu2 := u2.isLt\n  have hv1 := v1.isLt\n  have hv2 := v2.isLt\n  obtain ⟨a, ha⟩ : ∃ a : ℤ, a = ((u1 : ℕ) : ℤ) - ((u2 : ℕ) : ℤ) := ⟨_, rfl⟩\n  obtain ⟨b, hb⟩ : ∃ b : ℤ, b = ((v1 : ℕ) : ℤ) - ((v2 : ℕ) : ℤ) := ⟨_, rfl⟩\n  have hdiv : (p : ℤ) ∣ a ^ 2 + b ^ 2 := by\n    rw [← ZMod.intCast_zmod_eq_zero_iff_dvd, ha, hb]\n    push_cast\n    have h' : ((u1 : ℕ) : ZMod p) - ((u2 : ℕ) : ZMod p)\n        = -(x * (((v1 : ℕ) : ZMod p) - ((v2 : ℕ) : ZMod p))) := by\n      grind\n    rw [h']\n    grind\n  have hpos : 0 < a ^ 2 + b ^ 2 := by\n    by_contra hc\n    have hsa := sq_nonneg a\n    have hsb := sq_nonneg b\n    have ha0 : a = 0 := pow_eq_zero_iff (n := 2) (by decide) |>.mp (by omega)\n    have hb0 : b = 0 := pow_eq_zero_iff (n := 2) (by decide) |>.mp (by omega)\n    apply hne\n    have e1 : u1 = u2 := Fin.ext (by omega)\n    have e2 : v1 = v2 := Fin.ext (by omega)\n    rw [e1, e2]\n  have hmZ : (m : ℤ) * m < p := by\n    have := lt_of_le_of_ne hm1 hmp\n    exact_mod_cast this\n  have hsa : a ^ 2 ≤ (m : ℤ) * m := by\n    have h1 : a ≤ m := by omega\n    have h2 : -(m : ℤ) ≤ a := by omega\n    calc a ^ 2 ≤ (m : ℤ) ^ 2 := sq_le_sq' h2 h1\n      _ = m * m := sq _\n  have hsb : b ^ 2 ≤ (m : ℤ) * m := by\n    have h1 : b ≤ m := by omega\n    have h2 : -(m : ℤ) ≤ b := by omega\n    calc b ^ 2 ≤ (m : ℤ) ^ 2 := sq_le_sq' h2 h1\n      _ = m * m := sq _\n  obtain ⟨k, hk⟩ := hdiv\n  have hpZ : (0 : ℤ) < p := by exact_mod_cast hp.pos\n  have hk1 : k = 1 := by\n    have : 0 < k := by\n      by_contra hc\n      have := mul_nonpos_of_nonneg_of_nonpos hpZ.le (show k ≤ 0 by omega)\n      omega\n    have : k < 2 := by\n      by_contra hc\n      have := mul_le_mul_of_nonneg_left (show (2 : ℤ) ≤ k by omega) hpZ.le\n      omega\n    omega\n  subst hk1\n  refine ⟨a.natAbs, b.natAbs, ?_⟩\n  have : ((a.natAbs ^ 2 + b.natAbs ^ 2 : ℕ) : ℤ) = p := by\n    push_cast\n    rw [sq_abs, sq_abs]\n    omega\n  exact_mod_cast this\n","Lemma.wilson":"import Mathlib.Data.ZMod.Basic\nimport Mathlib.Data.Nat.Factorial.Basic\n\nlemma wil_mic (p : ℕ) [hp : Fact p.Prime] (a : ZMod p) (h : a ≠ 0) : a * a⁻¹ = 1 := by\n  rw [ZMod.mul_inv_eq_gcd, ← Nat.cast_one]\n  congr 1\n  have hnd : ¬ p ∣ a.val := by\n    intro hd\n    have hlt : a.val < p := ZMod.val_lt a\n    have h0 : a.val = 0 := Nat.eq_zero_of_dvd_of_lt hd hlt\n    exact h ((ZMod.val_eq_zero a).mp h0)\n  exact ((Nat.Prime.coprime_iff_not_dvd hp.out).mpr hnd).symm\n\nlemma wil_inv_eq (p : ℕ) [Fact p.Prime] (a b : ZMod p) (h : a * b = 1) : a⁻¹ = b := by\n  have ha : a ≠ 0 := by\n    intro h0\n    rw [h0, zero_mul] at h\n    haveI : Fact (1 < p) := ⟨(Fact.out : p.Prime).one_lt⟩\n    exact zero_ne_one h\n  calc a⁻¹ = a⁻¹ * (a * b) := by rw [h, mul_one]\n    _ = (a * a⁻¹) * b := by rw [← mul_assoc, mul_comm a⁻¹ a]\n    _ = b := by rw [wil_mic p a ha, one_mul]\n\nlemma wil_inv_ne (p : ℕ) [Fact p.Prime] (a : ZMod p) (h : a ≠ 0) : a⁻¹ ≠ 0 := by\n  intro h0\n  have h1 := wil_mic p a h\n  rw [h0, mul_zero] at h1\n  haveI : Fact (1 < p) := ⟨(Fact.out : p.Prime).one_lt⟩\n  exact zero_ne_one h1\n\nlemma wil_inv_inv (p : ℕ) [Fact p.Prime] (a : ZMod p) (h : a ≠ 0) : a⁻¹⁻¹ = a := by\n  apply wil_inv_eq\n  rw [mul_comm]\n  exact wil_mic p a h\n\nlemma wil_nzd (p : ℕ) [Fact p.Prime] (x y : ZMod p) (hx : x ≠ 0) (h : x * y = 0) : y = 0 := by\n  calc y = (x⁻¹ * x) * y := by rw [mul_comm x⁻¹ x, wil_mic p x hx, one_mul]\n    _ = 0 := by rw [mul_assoc, h, mul_zero]\n\nlemma fact_cast (p : ℕ) : ∀ n : ℕ,\n    ((n.factorial : ℕ) : ZMod p) = ∏ i ∈ Finset.range n, ((i + 1 : ℕ) : ZMod p)\n  | 0 => by rw [Nat.factorial_zero, Finset.prod_range_zero, Nat.cast_one]\n  | n + 1 => by\n    rw [Finset.prod_range_succ, ← fact_cast p n, Nat.factorial_succ, Nat.cast_mul, mul_comm]\n\nlemma wilson_cast (p : ℕ) [hp : Fact p.Prime] :\n    ((p - 1).factorial : ZMod p) = ∏ x ∈ (Finset.univ.erase 0 : Finset (ZMod p)), x := by\n  have hp1 : 1 < p := hp.out.one_lt\n  rw [fact_cast]\n  refine Finset.prod_bij (fun i _ => ((i + 1 : ℕ) : ZMod p)) ?_ ?_ ?_ ?_\n  · intro a ha\n    rw [Finset.mem_range] at ha\n    rw [Finset.mem_erase]\n    refine ⟨?_, Finset.mem_univ _⟩\n    intro h\n    have := congrArg ZMod.val h\n    rw [ZMod.val_natCast_of_lt (by omega), ZMod.val_zero] at this\n    omega\n  · intro a ha b hb h\n    rw [Finset.mem_range] at ha hb\n    have := congrArg ZMod.val h\n    rw [ZMod.val_natCast_of_lt (by omega), ZMod.val_natCast_of_lt (by omega)] at this\n    omega\n  · intro b hb\n    rw [Finset.mem_erase] at hb\n    have h1 : b.val ≠ 0 := by\n      intro h; exact hb.1 ((ZMod.val_eq_zero b).mp h)\n    have h2 : b.val < p := ZMod.val_lt b\n    refine ⟨b.val - 1, Finset.mem_range.mpr (by omega), ?_⟩\n    rw [show b.val - 1 + 1 = b.val by omega, ZMod.natCast_zmod_val]\n  · intro a ha\n    rfl\n\nlemma wilson_prod (p : ℕ) [hp : Fact p.Prime] (h2 : p ≠ 2) :\n    ∏ x ∈ (Finset.univ.erase 0 : Finset (ZMod p)), x = -1 := by\n  have hne : (1 : ZMod p) ≠ -1 := by\n    intro h\n    have h' : ((2 : ℕ) : ZMod p) = 0 := by\n      rw [Nat.cast_ofNat]\n      calc (2 : ZMod p) = 1 + 1 := one_add_one_eq_two.symm\n        _ = -1 + 1 := by rw [← h]\n        _ = 0 := neg_add_cancel 1\n    rw [ZMod.natCast_eq_zero_iff] at h'\n    have := (Nat.prime_dvd_prime_iff_eq hp.out Nat.prime_two).mp h'\n    exact h2 this\n  have hsub : ({1, -1} : Finset (ZMod p)) ⊆ Finset.univ.erase 0 := by\n    intro x hx\n    simp only [Finset.mem_insert, Finset.mem_singleton] at hx\n    rw [Finset.mem_erase]\n    refine ⟨?_, Finset.mem_univ _⟩\n    rcases hx with rfl | rfl\n    · exact one_ne_zero\n    · exact neg_ne_zero.mpr one_ne_zero\n  rw [← Finset.prod_sdiff hsub]\n  have hrest : ∏ x ∈ (Finset.univ.erase 0 : Finset (ZMod p)) \\ {1, -1}, x = 1 := by\n    refine Finset.prod_involution (fun x _ => x⁻¹) ?_ ?_ ?_ ?_\n    · intro a ha\n      simp only [Finset.mem_sdiff, Finset.mem_erase] at ha\n      exact wil_mic p a ha.1.1\n    · intro a ha _ h\n      simp only [Finset.mem_sdiff, Finset.mem_erase, Finset.mem_insert,\n        Finset.mem_singleton, not_or] at ha\n      have h1 : a * a = 1 := by\n        calc a * a = a * a⁻¹ := by rw [h]\n          _ = 1 := wil_mic p a ha.1.1\n      have h3 : (a - 1) * (a + 1) = 0 := by\n        calc (a - 1) * (a + 1) = a * a - 1 := by grind\n          _ = 0 := by rw [h1]; exact sub_self 1\n      have hs : a - 1 ≠ 0 := fun h0 => ha.2.1 (sub_eq_zero.mp h0)\n      have h4 := wil_nzd p _ _ hs h3\n      exact ha.2.2 (eq_neg_of_add_eq_zero_left h4)\n    · intro a ha\n      simp only [Finset.mem_sdiff, Finset.mem_erase, Finset.mem_insert,\n        Finset.mem_singleton, not_or, Finset.mem_univ, and_true] at ha ⊢\n      refine ⟨wil_inv_ne p a ha.1, ?_, ?_⟩\n      · intro h; apply ha.2.1\n        rw [← wil_inv_inv p a ha.1, h]\n        exact wil_inv_eq p 1 1 (one_mul 1)\n      · intro h; apply ha.2.2\n        rw [← wil_inv_inv p a ha.1, h]\n        exact wil_inv_eq p (-1) (-1) (by rw [neg_mul_neg, one_mul])\n    · intro a ha\n      simp only [Finset.mem_sdiff, Finset.mem_erase] at ha\n      exact wil_inv_inv p a ha.1.1\n  rw [hrest, Finset.prod_pair hne]\n  simp\n\ntheorem Lemma.wilson :\n    ∀ p : ℕ, p.Prime → (p - 1).factorial % p = p - 1 := by\n  intro p hp\n  haveI := Fact.mk hp\n  have hp1 : 1 < p := hp.one_lt\n  by_cases h2 : p = 2\n  · subst h2; decide\n  have key : (((p - 1).factorial : ℕ) : ZMod p) = ((p - 1 : ℕ) : ZMod p) := by\n    rw [wilson_cast, wilson_prod p h2, Nat.cast_sub (by omega), ZMod.natCast_self]\n    simp\n  rw [ZMod.natCast_eq_natCast_iff'] at key\n  rw [key, Nat.mod_eq_of_lt (by omega)]\n"}},"flags":[],"id":115,"lab_check":false,"label":"no-improvement","measured":7.0,"reason":null,"score":7.0,"significance":[],"status":"verified","verdicts":[{"audit":true,"lab":true,"measured":7.0,"node":3,"seed":0}]},"entry":{"body":"C115 completes the set: theorems proved 7. 0 open unit(s) closed; the lab's maintainers can retire the program or add challenges.","claim":115,"created":1792131621,"credit":[2],"id":308,"kind":"summary","label":null,"parent":null,"program":"lean-ablations","score":7.0,"title":"Classic theorems without their usual tools: every challenge is settled","unit":167},"followups":[]}