Cleared U173 threshold: theorems proved 7

Claim 128

Status

verified

Claimed

7

Measured

7

Label

no improvement

Signed commit

5f095fe570c697a865752f8ecad49d96190c8cef

Verification runs

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 Finse
… (truncated; the full value is in this page's JSON)

Code

// file: four_squares.orig.lean
import Mathlib.Data.ZMod.Basic

lemma fs_euler (a b c d x y z w : ℤ) :
    (a^2+b^2+c^2+d^2)*(x^2+y^2+z^2+w^2) =
      (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
        + (a*w+b*z-c*y-d*x)^2 := by
  grind

lemma fs_mul (m n : ℕ) (hm : ∃ a b c d : ℤ, a^2+b^2+c^2+d^2 = (m:ℤ))
    (hn : ∃ a b c d : ℤ, a^2+b^2+c^2+d^2 = (n:ℤ)) :
    ∃ a b c d : ℤ, a^2+b^2+c^2+d^2 = ((m*n : ℕ):ℤ) := by
  obtain ⟨a, b, c, d, h1⟩ := hm
  obtain ⟨x, y, z, w, h2⟩ := hn
  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, ?_⟩
  rw [Nat.cast_mul, ← h1, ← h2, fs_euler]

lemma fs_sq_mod_two (a : ℤ) : a^2 % 2 = a % 2 := by
  rcases Int.even_or_odd a with ⟨q, hq⟩ | ⟨q, hq⟩
  · subst hq
    have : (q+q)^2 = 2*(2*q^2) := by grind
    rw [this]; omega
  · subst hq
    have : (2*q+1)^2 = 2*(2*q^2+2*q) + 1 := by grind
    rw [this]; omega

lemma fs_resid (x k : ℤ) (hk : 0 ≤ k) :
    ∃ y t : ℤ, x = y + (2*k+1)*t ∧ -k ≤ y ∧ y ≤ k := by
  refine ⟨(x+k)%(2*k+1) - k, (x+k)/(2*k+1), ?_, ?_, ?_⟩ <;>
  · have h1 := Int.emod_def (x+k) (2*k+1)
    have h2 := Int.emod_nonneg (x+k) (show (2*k+1) ≠ 0 by omega)
    have h3 := Int.emod_lt_of_pos (x+k) (show (0:ℤ) < 2*k+1 by omega)
    generalize (x+k)%(2*k+1) = a at *
    generalize (2*k+1)*((x+k)/(2*k+1)) = b at *
    omega

lemma fs_sq_inj (p : ℕ) (hp : p.Prime) (hodd : p % 2 = 1) (i j : ℕ) (hi : i ≤ p/2) (hj : j ≤ p/2)
    (h : ((i:ZMod p))^2 = ((j:ZMod p))^2) : i = j := by
  have h' : (((i:ℤ)^2 : ℤ) : ZMod p) = (((j:ℤ)^2 : ℤ) : ZMod p) := by
    push_cast; exact h
  rw [ZMod.intCast_eq_intCast_iff_dvd_sub] at h'
  have e : (j:ℤ)^2 - (i:ℤ)^2 = ((j:ℤ) - i) * ((j:ℤ) + i) := by grind
  rw [e, Int.natCast_dvd, Int.natAbs_mul] at h'
  have hp2 := hp.two_le
  rcases hp.dvd_mul.mp h' with h1 | h1
  · have hlt : ((j:ℤ) - i).natAbs < p := by omega
    have := Nat.eq_zero_of_dvd_of_lt h1 hlt
    omega
  · have hlt : ((j:ℤ) + i).natAbs < p := by omega
    have := Nat.eq_zero_of_dvd_of_lt h1 hlt
    omega

lemma fs_pigeon (p : ℕ) (hp : p.Prime) (hodd : p % 2 = 1) :
    ∃ x y : ℕ, x ≤ p/2 ∧ y ≤ p/2 ∧ p ∣ x^2+y^2+1 := by
  haveI : NeZero p := ⟨hp.ne_zero⟩
  by_contra hne
  let f : Fin (p/2+1) ⊕ Fin (p/2+1) → ZMod p :=
    Sum.elim (fun i => ((i.val : ℕ) : ZMod p)^2) (fun j => -1 - ((j.val : ℕ) : ZMod p)^2)
  have key : ∀ i j : Fin (p/2+1), ((i.val:ℕ):ZMod p)^2 = -1 - ((j.val:ℕ):ZMod p)^2 → False := by
    intro i j hij
    apply hne
    refine ⟨i.val, j.val, by omega, by omega, ?_⟩
    rw [← CharP.cast_eq_zero_iff (ZMod p) p]
    push_cast
    rw [hij]
    grind
  have hinj : Function.Injective f := by
    intro a b hab
    rcases a with i | i <;> rcases b with j | j
    · simp only [f, Sum.elim_inl] at hab
      have := fs_sq_inj p hp hodd i.val j.val (by omega) (by omega) hab
      rw [Fin.ext this]
    · simp only [f, Sum.elim_inl, Sum.elim_inr] at hab
      exact (key i j hab).elim
    · simp only [f, Sum.elim_inl, Sum.elim_inr] at hab
      exact (key j i hab.symm).elim
    · simp only [f, Sum.elim_inr] at hab
      have hab' : ((i.val:ℕ):ZMod p)^2 = ((j.val:ℕ):ZMod p)^2 := by grind
      have := fs_sq_inj p hp hodd i.val j.val (by omega) (by omega) hab'
      rw [Fin.ext this]
  have := Fintype.card_le_of_injective f hinj
  simp only [Fintype.card_sum, Fintype.card_fin, ZMod.card] at this
  omega

lemma fs_par (s1 s2 s3 s4 a1 a2 a3 a4 : ℤ) (e1 : s1 % 2 = a1 % 2) (e2 : s2 % 2 = a2 % 2)
    (e3 : s3 % 2 = a3 % 2) (e4 : s4 % 2 = a4 % 2) (hev : (s1+s2+s3+s4) % 2 = 0) :
    (a1 % 2 = a2 % 2 ∧ a3 % 2 = a4 % 2) ∨ (a1 % 2 = a3 % 2 ∧ a2 % 2 = a4 % 2)
        ∨ (a1 % 2 = a4 % 2 ∧ a2 % 2 = a3 % 2) := by
  omega

lemma fs_halve (a b c d k p : ℤ) (hab : a % 2 = b % 2) (hcd : c % 2 = d % 2)
    (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
  obtain ⟨u, hu⟩ : ∃ u, a + b = 2*u := ⟨(a+b)/2, by omega⟩
  obtain ⟨v, hv⟩ : ∃ v, a - b = 2*v := ⟨(a-b)/2, by omega⟩
  obtain ⟨w, hw⟩ : ∃ w, c + d = 2*w := ⟨(c+d)/2, by omega⟩
  obtain ⟨z, hz⟩ : ∃ z, c - d = 2*z := ⟨(c-d)/2, by omega⟩
  have ha : a = u + v := by omega
  have hb : b = u - v := by omega
  have hc : c = w + z := by omega
  have hd : d = w - z := by omega
  subst ha hb hc hd
  refine ⟨u, v, w, z, ?_⟩
  have : 2*(u^2+v^2+w^2+z^2) = 2*(k*p) := by grind
  omega

lemma fs_prime (p : ℕ) (hp : p.Prime) : ∃ a b c d : ℤ, a^2+b^2+c^2+d^2 = (p:ℤ) := by
  classical
  rcases hp.eq_two_or_odd with h2 | hodd
  · exact ⟨1, 1, 0, 0, by subst h2; simp⟩
  obtain ⟨x, y, hx, hy, hdvd⟩ := fs_pigeon p hp hodd
  obtain ⟨m, hm⟩ := hdvd
  have hp2 := hp.two_le
  have hmp : m < p := by
    have h1 : x^2 ≤ (p/2)^2 := Nat.pow_le_pow_left hx 2
    have h2 : y^2 ≤ (p/2)^2 := Nat.pow_le_pow_left hy 2
    have h3 : p * p = 4*(p/2)^2 + 4*(p/2) + 1 := by
      have : p = 2*(p/2)+1 := by omega
      conv_lhs => rw [this]
      grind
    have h4 : p * m < p * p := by
      generalize (p/2)^2 = s at *
      generalize p * m = t at *
      generalize p * p = r at *
      omega
    exact Nat.lt_of_mul_lt_mul_left h4
  let P : ℕ → Prop := fun m => 0 < m ∧ ∃ a b c d : ℤ, a^2+b^2+c^2+d^2 = (m:ℤ)*p
  have hPm : P m := by
    refine ⟨?_, (x:ℤ), (y:ℤ), 1, 0, ?_⟩
    · rcases Nat.eq_zero_or_pos m with h0 | h0
      · subst h0; simp at hm
      · exact h0
    · have : ((x^2+y^2+1 : ℕ) : ℤ) = ((p*m : ℕ) : ℤ) := by rw [hm]
      push_cast at this
      grind
  have hex : ∃ m, P m := ⟨m, hPm⟩
  have hspec := Nat.find_spec hex
  have hmin : ∀ r, r < Nat.find hex → ¬ P r := fun r hr => Nat.find_min hex hr
  have hle : Nat.find hex ≤ m := Nat.find_min' hex hPm
  generalize Nat.find hex = M at hspec hmin hle
  obtain ⟨hM0, a1, a2, a3, a4, hA⟩ := hspec
  by_cases hM1 : M = 1
  · subst hM1; exact ⟨a1, a2, a3, a4, by rw [hA]; simp⟩
  exfalso
  obtain ⟨k, hk | hk⟩ := Nat.even_or_odd' M
  · -- even case
    apply hmin k (by omega)
    refine ⟨by omega, ?_⟩
    have e1 := fs_sq_mod_two a1
    have e2 := fs_sq_mod_two a2
    have e3 := fs_sq_mod_two a3
    have e4 := fs_sq_mod_two a4
    have hA' : a1^2+a2^2+a3^2+a4^2 = (2*(k:ℤ))*p := by rw [hA, hk]; push_cast; rfl
    have hev : (a1^2+a2^2+a3^2+a4^2) % 2 = 0 := by
      rw [hA', mul_assoc]; omega
    have hcases : (a1 % 2 = a2 % 2 ∧ a3 % 2 = a4 % 2) ∨ (a1 % 2 = a3 % 2 ∧ a2 % 2 = a4 % 2)
        ∨ (a1 % 2 = a4 % 2 ∧ a2 % 2 = a3 % 2) := by
      exact fs_par _ _ _ _ _ _ _ _ e1 e2 e3 e4 hev
    rcases hcases with ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩
    · exact fs_halve a1 a2 a3 a4 k p h1 h2 hA'
    · exact fs_halve a1 a3 a2 a4 k p h1 h2 (by rw [← hA']; grind)
    · exact fs_halve a1 a4 a2 a3 k p h1 h2 (by rw [← hA']; grind)
  · -- odd case
    have hk1 : 1 ≤ k := by omega
    have hkz : (0:ℤ) ≤ k := by omega
    obtain ⟨y1, t1, hx1, hl1, hu1⟩ := fs_resid a1 k hkz
    obtain ⟨y2, t2, hx2, hl2, hu2⟩ := fs_resid a2 k hkz
    obtain ⟨y3, t3, hx3, hl3, hu3⟩ := fs_resid a3 k hkz
    obtain ⟨y4, t4, hx4, hl4, hu4⟩ := fs_resid a4 k hkz
    have hMz : (M:ℤ) = 2*k+1 := by rw [hk]; push_cast; rfl
    rw [← hMz] at hx1 hx2 hx3 hx4
    subst hx1 hx2 hx3 hx4
    -- divisibility of sum of y^2
    have hdiv : (M:ℤ) ∣ y1^2+y2^2+y3^2+y4^2 := by
      refine ⟨p - (2*(y1*t1+y2*t2+y3*t3+y4*t4) + (M:ℤ)*(t1^2+t2^2+t3^2+t4^2)), ?_⟩
      grind
    obtain ⟨r, hr⟩ := hdiv
    have s1 := sq_nonneg y1
    have s2 := sq_nonneg y2
    have s3 := sq_nonneg y3
    have s4 := sq_nonneg y4
    have b1 : y1^2 ≤ (k:ℤ)^2 := sq_le_sq' hl1 hu1
    have b2 : y2^2 ≤ (k:ℤ)^2 := sq_le_sq' hl2 hu2
    have b3 : y3^2 ≤ (k:ℤ)^2 := sq_le_sq' hl3 hu3
    have b4 : y4^2 ≤ (k:ℤ)^2 := sq_le_sq' hl4 hu4
    have hMM : (M:ℤ)*M = 4*(k:ℤ)^2 + 4*k + 1 := by rw [hMz]; grind
    have hMpos : (0:ℤ) < M := by omega
    have hr0 : 0 ≤ r := by
      by_contra hneg
      have : (M:ℤ) * r < 0 := Int.mul_neg_of_pos_of_neg hMpos (by omega)
      omega
    have hrM : r < M := by
      by_contra hge
      have : (M:ℤ) * M ≤ M * r := Int.mul_le_mul_of_nonneg_left (by omega) (by omega)
      generalize (k:ℤ)^2 = K at *
      generalize (M:ℤ) * M = Q at *
      generalize (M:ℤ) * r = R at *
      omega
    rcases (show r = 0 ∨ 0 < r by omega) with hr00 | hrpos
    · -- all y = 0, so M ∣ p
      subst hr00
      have z1 : y1 = 0 := by
        have : y1^2 = 0 := by rw [mul_zero] at hr; omega
        exact pow_eq_zero_iff two_ne_zero |>.mp this
      have z2 : y2 = 0 := by
        have : y2^2 = 0 := by rw [mul_zero] at hr; omega
        exact pow_eq_zero_iff two_ne_zero |>.mp this
      have z3 : y3 = 0 := by
        have : y3^2 = 0 := by rw [mul_zero] at hr; omega
        exact pow_eq_zero_iff two_ne_zero |>.mp this
      have z4 : y4 = 0 := by
        have : y4^2 = 0 := by rw [mul_zero] at hr; omega
        exact pow_eq_zero_iff two_ne_zero |>.mp this
      subst z1 z2 z3 z4
      have hMd : (M:ℤ) * ((M:ℤ)*(t1^2+t2^2+t3^2+t4^2)) = (M:ℤ) * p := by
        rw [← hA]; grind
      have hMd' := mul_left_cancel₀ (show (M:ℤ) ≠ 0 by omega) hMd
      have hdvd : (M:ℤ) ∣ (p:ℤ) := ⟨_, hMd'.symm⟩
      have hdvdN : M ∣ p := Int.natCast_dvd_natCast.mp hdvd
      rcases hp.eq_one_or_self_of_dvd M hdvdN with h | h <;> omega
    · -- descent
      apply hmin r.toNat (by omega)
      refine ⟨by omega, ?_⟩
      refine ⟨r + (y1*t1+y2*t2+y3*t3+y4*t4), t1*y2-t2*y1+t3*y4-t4*y3,
        t1*y3-t2*y4-t3*y1+t4*y2, t1*y4+t2*y3-t3*y2-t4*y1, ?_⟩
      rw [Int.toNat_of_nonneg hr0]
      have E := fs_euler (y1 + M*t1) (y2 + M*t2) (y3 + M*t3) (y4 + M*t4) y1 y2 y3 y4
      rw [hA, hr] at E
      have f1 : (y1 + M*t1)*y1 + (y2 + M*t2)*y2 + (y3 + M*t3)*y3 + (y4 + M*t4)*y4
          = (M:ℤ) * (r + (y1*t1+y2*t2+y3*t3+y4*t4)) := by grind
      have f2 : (y1 + M*t1)*y2 - (y2 + M*t2)*y1 + (y3 + M*t3)*y4 - (y4 + M*t4)*y3
          = (M:ℤ) * (t1*y2-t2*y1+t3*y4-t4*y3) := by grind
      have f3 : (y1 + M*t1)*y3 - (y2 + M*t2)*y4 - (y3 + M*t3)*y1 + (y4 + M*t4)*y2
          = (M:ℤ) * (t1*y3-t2*y4-t3*y1+t4*y2) := by grind
      have f4 : (y1 + M*t1)*y4 + (y2 + M*t2)*y3 - (y3 + M*t3)*y2 - (y4 + M*t4)*y1
          = (M:ℤ) * (t1*y4+t2*y3-t3*y2-t4*y1) := by grind
      rw [f1, f2, f3, f4] at E
      have E2 : ((M:ℤ)*M) * ((r + (y1*t1+y2*t2+y3*t3+y4*t4))^2 + (t1*y2-t2*y1+t3*y4-t4*y3)^2
          + (t1*y3-t2*y4-t3*y1+t4*y2)^2 + (t1*y4+t2*y3-t3*y2-t4*y1)^2)
          = ((M:ℤ)*M) * (r * p) := by
        have E3 : ((M:ℤ)*M) * ((r + (y1*t1+y2*t2+y3*t3+y4*t4))^2 + (t1*y2-t2*y1+t3*y4-t4*y3)^2
            + (t1*y3-t2*y4-t3*y1+t4*y2)^2 + (t1*y4+t2*y3-t3*y2-t4*y1)^2)
            = ((M:ℤ) * (r + (y1*t1+y2*t2+y3*t3+y4*t4)))^2 + ((M:ℤ) * (t1*y2-t2*y1+t3*y4-t4*y3))^2
            + ((M:ℤ) * (t1*y3-t2*y4-t3*y1+t4*y2))^2 + ((M:ℤ) * (t1*y4+t2*y3-t3*y2-t4*y1))^2 := by
          grind
        rw [E3, ← E]
        grind
      exact mul_left_cancel₀ (show (M:ℤ)*M ≠ 0 from (mul_ne_zero (by omega) (by omega))) E2

lemma fs_int : ∀ n : ℕ, ∃ a b c d : ℤ, a^2+b^2+c^2+d^2 = (n:ℤ) := by
  intro n
  induction n using Nat.strong_induction_on with
  | _ n ih =>
    rcases n with _ | _ | n
    · exact ⟨0, 0, 0, 0, by simp⟩
    · exact ⟨1, 0, 0, 0, by simp⟩
    · have hp := Nat.minFac_prime (show n + 2 ≠ 1 by omega)
      obtain ⟨q, hq⟩ := Nat.minFac_dvd (n+2)
      have hq0 : 0 < q := by
        rcases Nat.eq_zero_or_pos q with h | h
        · rw [h, Nat.mul_zero] at hq; omega
        · exact h
      have h2 : 2 * q ≤ (n+2).minFac * q := Nat.mul_le_mul_right q hp.two_le
      have hlt : q < n + 2 := by
        generalize (n+2).minFac * q = t at *
        omega
      rw [hq]
      exact fs_mul _ _ (fs_prime _ hp) (ih q hlt)

theorem Lemma.four_squares :
    ∀ n : ℕ, ∃ a b c d : ℕ, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n := by
  intro n
  obtain ⟨a, b, c, d, h⟩ := fs_int n
  refine ⟨a.natAbs, b.natAbs, c.natAbs, d.natAbs, ?_⟩
  have h1 : ((a.natAbs^2 + b.natAbs^2 + c.natAbs^2 + d.natAbs^2 : ℕ) : ℤ) = n := by
    simp only [Nat.cast_add, Nat.cast_pow, Int.natCast_natAbs, sq_abs]
    exact h
  exact_mod_cast h1