a small integer linear relation on 2r points

Checked by the kernel — these bytes are the ones its attestation names: attestations/000550.json, merge commit 06ac98c605f5.

import Mathlib
import Nodes.«erdos-1094--h2--h2--h2--h3--h1--h1--h1--h1».Context

open scoped Nat

/-! Hole `hsilr` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

private lemma hadamard_inequality (n : ℕ) (A : Matrix (Fin n) (Fin n) ℝ) :
    A.det ^ 2 ≤ ∏ i : Fin n, ∑ j : Fin n, A i j ^ 2 := by
  set M := A * A.transpose with hM_def
  have hM_pos_semidef : Matrix.PosSemidef M := by
    constructor;
    · simp +decide [ hM_def, Matrix.IsHermitian, Matrix.transpose_mul ];
    · intro x
      have h_sum : ∑ i, ∑ j, x i * M i j * x j = ∑ k, (∑ i, x i * A i k) ^ 2 := by
        simp +zetaDelta at *;
        simp +decide [ Matrix.mul_apply, mul_assoc, mul_comm, mul_left_comm, sq, Finset.mul_sum _ _ _ ];
        exact Finset.sum_comm_cycle;
      simp_all +decide [ Finsupp.sum_fintype ];
      exact Finset.sum_nonneg fun _ _ => sq_nonneg _;
  obtain ⟨U, D, hU, hD⟩ : ∃ U : Matrix (Fin n) (Fin n) ℝ, ∃ D : Fin n → ℝ, U.transpose * U = 1 ∧ (∀ i, D i ≥ 0) ∧ M = U * Matrix.diagonal D * U.transpose := by
    have := Matrix.IsHermitian.spectral_theorem hM_pos_semidef.1;
    refine' ⟨ _, _, _, _, this ⟩;
    · have h := hM_pos_semidef.1.eigenvectorUnitary.2.1;
      simpa [Matrix.star_eq_conjTranspose] using h
    · exact fun i => hM_pos_semidef.eigenvalues_nonneg i;
  have h_det_M : Matrix.det M = ∏ i, D i := by
    apply_fun Matrix.det at hM_def ; simp_all +decide [ Matrix.det_mul, Matrix.det_diagonal ];
    have := congr_arg Matrix.det hU; norm_num at this; cases le_or_gt 0 ( U.det ) <;> nlinarith;
  have h_diag_M : ∀ i, M i i = ∑ j, U i j ^ 2 * D j := by
    simp +decide [ hD, Matrix.mul_apply, sq ];
    simp +decide [Matrix.diagonal, mul_comm, mul_left_comm];
  have h_am_gm : ∀ i, M i i ≥ ∏ j, D j ^ (U i j ^ 2) := by
    intro i;
    have := @Real.geom_mean_le_arith_mean;
    specialize this Finset.univ ( fun j => U i j ^ 2 ) ( fun j => D j ) ; simp_all +decide [ Matrix.mul_apply ];
    have h_sum_one : ∑ j, U i j ^ 2 = 1 := by
      simpa [ sq, Matrix.mul_apply ] using congr_arg ( fun m => m i i ) ( show U * U.transpose = 1 from by rw [ ← mul_eq_one_comm, hU ] );
    simpa [ h_sum_one ] using this ( fun j => sq_nonneg _ ) ( by rw [ h_sum_one ] ; norm_num );
  have h_prod_am_gm : ∏ i, M i i ≥ ∏ j, D j := by
    refine le_trans ?_ ( Finset.prod_le_prod ?_ fun i _ => h_am_gm i );
    · rw [ Finset.prod_comm, ← Finset.prod_congr rfl fun _ _ => Real.rpow_sum_of_nonneg ( hD.1 _ ) _ ];
      · simp_all +decide [← Matrix.ext_iff, sq];
        simp_all +decide [ Matrix.mul_apply, Matrix.one_apply ];
      · exact fun _ _ _ _ => sq_nonneg _;
    · exact fun i _ => Finset.prod_nonneg fun j _ => Real.rpow_nonneg ( hD.1 j ) _;
  simp_all +decide [ sq, Matrix.mul_apply ]

private noncomputable def gramDet (m s : ℕ) (v : Fin m → (Fin s → ℝ)) : ℝ :=
  Matrix.det (Matrix.of (fun i j : Fin m => ∑ k : Fin s, v i k * v j k))

private lemma gramDet_le_prod_sq_norms (m s : ℕ) (v : Fin m → (Fin s → ℝ)) :
    gramDet m s v ≤ ∏ j : Fin m, ∑ k : Fin s, v j k ^ 2 := by
  set B : Matrix (Fin m) (Fin s) ℝ := Matrix.of (fun i j => v i j) with hB_def
  obtain ⟨U, hU⟩ : ∃ U : Matrix (Fin m) (Fin m) ℝ, U * U.transpose = B * B.transpose := by
    have h_pos_semidef : Matrix.PosSemidef (B * B.transpose) := by
      exact Matrix.posSemidef_conjTranspose_mul_self _
    letI : PartialOrder (Matrix (Fin m) (Fin m) ℝ) := Matrix.instPartialOrder
    letI : StarOrderedRing (Matrix (Fin m) (Fin m) ℝ) := Matrix.instStarOrderedRing
    letI : NonnegSpectrumClass ℝ (Matrix (Fin m) (Fin m) ℝ) := Matrix.instNonnegSpectrumClass
    have : 0 ≤ B * B.transpose := h_pos_semidef.nonneg
    obtain ⟨U, hU⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp this
    use U.transpose
    simpa [Matrix.star_eq_conjTranspose, Matrix.conjTranspose_eq_transpose_of_trivial] using hU.symm
  convert hadamard_inequality m U using 1
  · have hG : gramDet m s v = (B * B.transpose).det := by
      unfold gramDet; congr 1
    rw [hG, ← hU, Matrix.det_mul, Matrix.det_transpose, sq]
  · simp_all +decide [← Matrix.ext_iff, Matrix.mul_apply, sq]

private lemma gramDet_unimodular_change (m s : ℕ)
    (z : Fin m → (Fin s → ℤ))
    (U : Matrix (Fin m) (Fin m) ℤ)
    (hU : Int.natAbs U.det = 1) :
    gramDet m s (fun k i => ((∑ j, U k j * z j i : ℤ) : ℝ)) =
    gramDet m s (fun k i => ((z k i : ℤ) : ℝ)) := by
  convert congr_arg ( fun x : ℤ => ( x : ℝ ) ) ( show Matrix.det ( ( U * Matrix.of ( fun k j => ∑ i, z k i * z j i ) ) * U.transpose ) = Matrix.det ( Matrix.of ( fun k j => ∑ i, z k i * z j i ) ) from ?_ ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
  · unfold gramDet;
    norm_num [ Matrix.mul_apply, Matrix.det_apply' ];
    simp +decide only [Finset.mul_sum _ _ _, mul_comm, mul_left_comm, mul_assoc];
    exact Finset.sum_congr rfl fun _ _ => congr_arg _ ( Finset.prod_congr rfl fun _ _ => Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => by ac_rfl ) ) );
  · unfold gramDet;
    norm_num [ Matrix.det_apply' ];
  · cases Int.natAbs_eq_iff.mp hU <;> simp_all +decide [ Matrix.det_mul ]

private lemma finite_integer_vectors_bounded (s : ℕ) (C : ℝ) :
    Set.Finite {a : Fin s → ℤ | ∑ i : Fin s, ((a i : ℤ) : ℝ) ^ 2 ≤ C} := by
  have h_bound : ∀ (a : Fin s → ℤ), (∑ i, (a i : ℝ) ^ 2) ≤ C → ∀ i, abs (a i : ℝ) ≤ Real.sqrt C := by
    exact fun a ha i => Real.abs_le_sqrt ( le_trans ( Finset.single_le_sum ( fun i _ => sq_nonneg ( a i : ℝ ) ) ( Finset.mem_univ i ) ) ha );
  exact Set.Finite.subset ( Set.finite_Icc _ _ ) fun a ha => ⟨ fun i => ( show a i ≥ - ⌈Real.sqrt C⌉₊ by exact_mod_cast neg_le_of_abs_le <| le_trans ( h_bound a ha i ) <| Nat.le_ceil _ ), fun i => ( show a i ≤ ⌈Real.sqrt C⌉₊ by exact_mod_cast le_of_abs_le <| le_trans ( h_bound a ha i ) <| Nat.le_ceil _ ) ⟩

private lemma shortest_lattice_vector_exists
    (m s : ℕ) (hm : 1 ≤ m)
    (z : Fin m → (Fin s → ℤ))
    (hz_indep : LinearIndependent ℤ z) :
    ∃ v : Fin s → ℤ, v ∈ Submodule.span ℤ (Set.range z) ∧ v ≠ 0 ∧
      ∀ w : Fin s → ℤ, w ∈ Submodule.span ℤ (Set.range z) → w ≠ 0 →
        ∑ i, ((v i : ℤ) : ℝ) ^ 2 ≤ ∑ i, ((w i : ℤ) : ℝ) ^ 2 := by
  have h_finite : Set.Finite {w ∈ Submodule.span ℤ (Set.range z) | ∑ i, (w i : ℝ) ^ 2 ≤ ∑ i, (z ⟨0, by linarith⟩ i : ℝ) ^ 2} := by
    refine' Set.Finite.subset ( finite_integer_vectors_bounded s ( ∑ i, ( z ⟨ 0, by linarith ⟩ i : ℝ ) ^ 2 ) ) _;
    grind;
  obtain ⟨v, hv⟩ : ∃ v ∈ {w ∈ Submodule.span ℤ (Set.range z) | w ≠ 0 ∧ ∑ i, (w i : ℝ) ^ 2 ≤ ∑ i, (z ⟨0, by linarith⟩ i : ℝ) ^ 2}, ∀ w ∈ {w ∈ Submodule.span ℤ (Set.range z) | w ≠ 0 ∧ ∑ i, (w i : ℝ) ^ 2 ≤ ∑ i, (z ⟨0, by linarith⟩ i : ℝ) ^ 2}, ∑ i, (v i : ℝ) ^ 2 ≤ ∑ i, (w i : ℝ) ^ 2 := by
    apply_rules [ Set.exists_min_image ];
    · exact h_finite.subset fun x hx => ⟨ hx.1, hx.2.2 ⟩;
    · exact ⟨ z ⟨ 0, hm ⟩, Submodule.subset_span ( Set.mem_range_self _ ), hz_indep.ne_zero _, le_rfl ⟩;
  exact ⟨ v, hv.1.1, hv.1.2.1, fun w hw hw' => if hw'' : ∑ i, ( w i : ℝ ) ^ 2 ≤ ∑ i, ( z ⟨ 0, by linarith ⟩ i : ℝ ) ^ 2 then hv.2 w ⟨ hw, hw', hw'' ⟩ else by linarith [ hv.1.2.2 ] ⟩

private lemma shortest_is_primitive
    (m s : ℕ) (z : Fin m → (Fin s → ℤ))
    (v : Fin s → ℤ)
    (hv_mem : v ∈ Submodule.span ℤ (Set.range z))
    (hv_ne : v ≠ 0)
    (hv_min : ∀ w : Fin s → ℤ, w ∈ Submodule.span ℤ (Set.range z) → w ≠ 0 →
        ∑ i, ((v i : ℤ) : ℝ) ^ 2 ≤ ∑ i, ((w i : ℤ) : ℝ) ^ 2) :
    ∀ n : ℤ, ∀ w : Fin s → ℤ, w ∈ Submodule.span ℤ (Set.range z) →
      v = n • w → n = 1 ∨ n = -1 := by
  intros n w hw hv_eq_nw
  by_contra h_contra
  have h_abs_n : |n| ≥ 2 := by
    exact not_lt.mp fun contra => h_contra <| eq_or_eq_neg_of_abs_eq <| le_antisymm ( Int.le_of_lt_add_one contra ) <| abs_pos.mpr <| show n ≠ 0 from fun h => hv_ne <| by simpa [ h ] using hv_eq_nw;
  specialize hv_min w hw ; simp_all +decide ;
  simp_all +decide [mul_pow, ← Finset.mul_sum _ _ _];
  exact absurd ( hv_min ( by aesop_cat ) ) ( by nlinarith [ show ( n : ℝ ) ^ 2 ≥ 4 by norm_cast; nlinarith [ abs_mul_abs_self n ], show 0 < ∑ i : Fin s, ( w i : ℝ ) ^ 2 from lt_of_le_of_ne ( Finset.sum_nonneg fun _ _ => sq_nonneg _ ) ( Ne.symm <| by intro h; exact hv_ne <| by ext i; simp_all +decide [ Finset.sum_eq_zero_iff_of_nonneg, sq_nonneg ] ) ] )

private lemma bezout_generalized (m : ℕ) (c : Fin m → ℤ)
    (hc : ∀ d : ℤ, (∀ i, d ∣ c i) → (d = 1 ∨ d = -1)) :
    ∃ a : Fin m → ℤ, ∑ i, a i * c i = 1 := by
  have h_one_in_ideal : 1 ∈ Ideal.span (Set.range c) := by
    contrapose! hc with h;
    obtain ⟨ d, hd ⟩ := IsPrincipalIdealRing.principal ( Ideal.span ( Set.range c ) );
    refine' ⟨ d, _, _, _ ⟩ <;> simp_all +decide;
    · exact fun i => by
        have h1 : c i ∈ Ideal.span (Set.range c) := Ideal.subset_span ( Set.mem_range_self i )
        rw [hd] at h1
        exact Ideal.mem_span_singleton.mp (by simpa using h1)
    · aesop;
    · aesop;
  exact (Submodule.mem_span_range_iff_exists_fun ℤ).mp h_one_in_ideal

private lemma int_vector_primitive_extends_unimodular (m : ℕ) (hm : 1 ≤ m) (c : Fin m → ℤ)
    (hc_prim : ∀ d : ℤ, (∀ i, d ∣ c i) → (d = 1 ∨ d = -1)) :
    ∃ U : Matrix (Fin m) (Fin m) ℤ,
      (∀ j, U ⟨0, by omega⟩ j = c j) ∧
      (U.det = 1 ∨ U.det = -1) := by
  obtain ⟨a, ha⟩ := bezout_generalized m c hc_prim;
  rcases m with ( _ | m ) <;> simp_all +decide [ Fin.sum_univ_succ ];
  obtain ⟨B, hB⟩ : ∃ B : Fin m → Fin (m + 1) → ℤ, LinearIndependent ℤ B ∧ ∀ x : Fin (m + 1) → ℤ, (∑ i, a i * x i = 0) ↔ ∃ y : Fin m → ℤ, x = ∑ i, y i • B i := by
    have h_kernel : ∃ B : Fin m → Fin (m + 1) → ℤ, LinearIndependent ℤ B ∧ ∀ x : Fin (m + 1) → ℤ, (∑ i, a i * x i = 0) ↔ ∃ y : Fin m → ℤ, x = ∑ i, y i • B i := by
      have h_submodule : ∃ M : Submodule ℤ (Fin (m + 1) → ℤ), M = {x : Fin (m + 1) → ℤ | ∑ i, a i * x i = 0} ∧ Module.finrank ℤ M = m := by
        have h_submodule : ∃ M : Submodule ℤ (Fin (m + 1) → ℤ), M = {x : Fin (m + 1) → ℤ | ∑ i, a i * x i = 0} ∧ Module.finrank ℤ M = m := by
          have h_map : ∃ f : (Fin (m + 1) → ℤ) →ₗ[ℤ] ℤ, ∀ x : Fin (m + 1) → ℤ, f x = ∑ i, a i * x i := by
            exact ⟨ ∑ i, a i • LinearMap.proj i, fun x => by simp +decide ⟩
          obtain ⟨f, hf⟩ := h_map
          have h_surjective : Function.Surjective f := by
            intro y
            use fun i => y * c i
            simp [hf];
            simp_all +decide [ mul_comm, mul_left_comm, Fin.sum_univ_succ ];
            rw [ ← Finset.mul_sum _ _ _, ← mul_add, ha, mul_one ];
          have h_rank_nullity : Module.finrank ℤ (LinearMap.ker f) + Module.finrank ℤ (LinearMap.range f) = Module.finrank ℤ (Fin (m + 1) → ℤ) := by
            have := Submodule.finrank_quotient_add_finrank ( LinearMap.ker f );
            rw [ add_comm, ← this ];
            rw [ ← ( LinearMap.quotKerEquivRange f ).finrank_eq ];
          rw [ show f.range = ⊤ from LinearMap.range_eq_top.mpr h_surjective ] at h_rank_nullity ; aesop;
        exact h_submodule
      obtain ⟨ M, hM₁, hM₂ ⟩ := h_submodule
      have h_basis : ∃ B : Fin m → M, LinearIndependent ℤ B ∧ Submodule.span ℤ (Set.range B) = ⊤ := by
        have := ( Module.finBasis ℤ M );
        refine' ⟨ _, _, _ ⟩;
        exact fun i => this ⟨ i, by linarith [ Fin.is_lt i ] ⟩
        all_goals generalize_proofs at *;
        · exact this.linearIndependent.comp _ ( fun i j hij => by simpa [ Fin.ext_iff ] using hij );
        · convert this.span_eq
          generalize_proofs at *; (
          linarith);
          linarith
      generalize_proofs at *; (
      obtain ⟨ B, hB₁, hB₂ ⟩ := h_basis; use fun i => B i; simp_all +decide [ SetLike.ext_iff ] ;
      refine' ⟨ _, _ ⟩
      all_goals generalize_proofs at *;
      · exact hB₁.map' ( Submodule.subtype M ) ( by aesop );
      · intro x; specialize hB₂ x; simp_all +decide [ Submodule.mem_span_range_iff_exists_fun ] ;
        exact ⟨ fun hx => by obtain ⟨ y, hy ⟩ := hB₂ ( hM₁.symm.subset hx ) ; exact ⟨ y, by simpa [ Subtype.ext_iff ] using hy.symm ⟩, fun hx => by obtain ⟨ y, hy ⟩ := hx; exact hM₁.subset <| by simpa [ Subtype.ext_iff ] using hy.symm ▸ Submodule.sum_mem _ fun i _ => Submodule.smul_mem _ _ ( B i |>.2 ) ⟩ ;);
    exact h_kernel;
  use Matrix.of (Fin.cons c B);
  have h_unimodular : ∀ x : Fin (m + 1) → ℤ, (∃ y : Fin (m + 1) → ℤ, x = ∑ i, y i • (Fin.cons c B i)) := by
    intro x
    obtain ⟨y, hy⟩ : ∃ y : Fin m → ℤ, x - (∑ i, a i * x i) • c = ∑ i, y i • B i := by
      have h_kernel : ∑ i, a i * (x i - (∑ i, a i * x i) * c i) = 0 := by
        simp +decide [ mul_sub, Finset.sum_sub_distrib ];
        simp +decide [ mul_comm, mul_left_comm, Fin.sum_univ_succ ] at ha ⊢;
        simp +decide [← mul_assoc, ← Finset.sum_mul _ _ _];
        grind +splitImp;
      exact hB.2 _ |>.1 h_kernel;
    use Fin.cons (∑ i, a i * x i) y;
    simp +decide [ Fin.sum_univ_succ, Fin.cons ] at hy ⊢;
    exact eq_add_of_sub_eq' hy;
  have h_unimodular : ∃ U : Matrix (Fin (m + 1)) (Fin (m + 1)) ℤ, U * Matrix.of (Fin.cons c B) = 1 := by
    choose f hf using h_unimodular;
    use Matrix.of (fun i j => f (Pi.single i 1) j);
    ext i j; specialize hf ( Pi.single i 1 ) ; replace hf := congr_fun hf j; simp +decide [Matrix.mul_apply,
      Finset.sum_apply] at hf ⊢;
    simp +decide [ ← hf, Pi.single_apply ];
    simp +decide [ Matrix.one_apply, eq_comm ];
  obtain ⟨ U, hU ⟩ := h_unimodular; have := congr_arg Matrix.det hU; norm_num at this; exact ⟨ fun j => rfl, Int.isUnit_iff.mp <| isUnit_iff_dvd_one.mpr <| by use U.det; linarith ⟩ ;

private lemma primitive_extends_to_basis
    (m s : ℕ) (hm : 2 ≤ m) (hms : m ≤ s)
    (z : Fin m → (Fin s → ℤ))
    (hz_indep : LinearIndependent ℤ z)
    (v : Fin s → ℤ)
    (hv_mem : v ∈ Submodule.span ℤ (Set.range z))
    (hv_prim : ∀ n : ℤ, ∀ w : Fin s → ℤ, w ∈ Submodule.span ℤ (Set.range z) →
      v = n • w → n = 1 ∨ n = -1) :
    ∃ w : Fin (m - 1) → (Fin s → ℤ),
      LinearIndependent ℤ (Fin.cons v w) ∧
      Submodule.span ℤ (Set.range (Fin.cons v w)) = Submodule.span ℤ (Set.range z) := by
  have h_basis : ∃ (u : Fin m → (Fin s → ℤ)), LinearIndependent ℤ u ∧ Submodule.span ℤ (Set.range u) = Submodule.span ℤ (Set.range z) ∧ u ⟨0, by linarith⟩ = v := by
    obtain ⟨c, hc⟩ : ∃ c : Fin m → ℤ, v = ∑ k, c k • z k := by
      rw [ Submodule.mem_span_range_iff_exists_fun ] at hv_mem ; tauto;
    obtain ⟨U, hU⟩ : ∃ U : Matrix (Fin m) (Fin m) ℤ, (∀ j, U ⟨0, by linarith⟩ j = c j) ∧ (U.det = 1 ∨ U.det = -1) := by
      apply int_vector_primitive_extends_unimodular m (by linarith) c;
      intro d hd; specialize hv_prim d ( ∑ k, ( c k / d ) • z k ) ; simp_all +decide [Finset.smul_sum] ;
      refine' hv_prim _ _;
      · exact Submodule.sum_mem _ fun i _ => Submodule.smul_mem _ _ ( Submodule.subset_span ( Set.mem_range_self _ ) );
      · exact Finset.sum_congr rfl fun i _ => by rw [ ← mul_assoc, ← Int.cast_mul, Int.mul_ediv_cancel' ( hd i ) ] ;
    refine' ⟨ fun i => ∑ j, U i j • z j, _, _, _ ⟩;
    · rw [ Fintype.linearIndependent_iff ] at *;
      intro g hg;
      have h_fubini : ∑ j, (∑ i, g i * U i j) • z j = 0 := by
        convert hg using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
        simp +decide only [mul_comm, Finset.sum_smul, Finset.smul_sum, smul_smul];
        exact Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring );
      have h_unimodular : ∀ (g : Fin m → ℤ), (∀ j, ∑ i, g i * U i j = 0) → ∀ i, g i = 0 := by
        intro g hg i
        have h_unimodular : Matrix.mulVec (Matrix.transpose U) g = 0 := by
          exact funext fun j => by simpa [ Matrix.mulVec, dotProduct, mul_comm ] using hg j;
        have h_unimodular : Matrix.det (Matrix.transpose U) ≠ 0 := by
          cases hU.2 <;> simp +decide [ * ];
        exact Matrix.eq_zero_of_mulVec_eq_zero h_unimodular ‹_› ▸ rfl;
      exact h_unimodular g fun j => hz_indep _ h_fubini j;
    · refine' le_antisymm _ _ <;> rw [ Submodule.span_le ] <;> simp +decide [ Set.range_subset_iff ];
      · exact fun i => Submodule.sum_mem _ fun j _ => Submodule.smul_mem _ _ ( Submodule.subset_span ( Set.mem_range_self _ ) );
      · intro i
        have h_inv : ∃ V : Matrix (Fin m) (Fin m) ℤ, V * U = 1 := by
          exact ⟨ U⁻¹, Matrix.nonsing_inv_mul _ <| isUnit_iff_dvd_one.mpr <| by rcases hU.2 with h | h <;> norm_num [ h ] ⟩;
        obtain ⟨ V, hV ⟩ := h_inv;
        have h_inv : z i = ∑ j, V i j • (∑ k, U j k • z k) := by
          have h_inv : ∀ i, ∑ j, V i j • (∑ k, U j k • z k) = ∑ k, (∑ j, V i j * U j k) • z k := by
            simp +decide [ Finset.smul_sum, Finset.sum_smul ];
            exact fun i => Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring );
          simp_all +decide [ ← Matrix.mul_apply, ← Matrix.ext_iff ];
          simp +decide [ Matrix.one_apply ];
        exact h_inv.symm ▸ Submodule.sum_mem _ fun j _ => Submodule.smul_mem _ _ ( Submodule.subset_span ⟨ j, rfl ⟩ );
    · grind;
  obtain ⟨u, hu_indep, hu_span, hu_v⟩ := h_basis;
  use fun i => u ⟨i.val + 1, by
    exact Nat.succ_lt_of_lt_pred i.2⟩;
  generalize_proofs at *;
  rcases m with ( _ | _ | m ) <;> simp_all +decide;
  refine' ⟨ _, _ ⟩;
  · convert hu_indep using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    ext i; induction i using Fin.inductionOn <;> aesop;
  · convert hu_span using 2 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    ext x; simp;
    exact ⟨ fun hx => hx.elim ( fun hx => ⟨ 0, hx.symm ▸ hu_v ⟩ ) fun ⟨ y, hy ⟩ => ⟨ _, hy ⟩, fun hx => by rcases hx with ⟨ y, rfl ⟩ ; exact Fin.cases ( Or.inl <| by aesop ) ( fun y => Or.inr ⟨ y, rfl ⟩ ) y ⟩

private lemma projected_int_vectors_indep
    (n s : ℕ)
    (v : Fin s → ℤ) (hv_ne : v ≠ 0)
    (w : Fin n → (Fin s → ℤ))
    (hw_indep : LinearIndependent ℤ (Fin.cons v w)) :
    LinearIndependent ℤ (fun j : Fin n => fun i : Fin s =>
      (∑ k, v k * v k) * w j i - (∑ k, w j k * v k) * v i) := by
  rw [ Fintype.linearIndependent_iff ] at hw_indep ⊢;
  intro g hg;
  convert hw_indep ( Fin.cons ( -∑ i, g i * ∑ k, w i k * v k ) ( fun i => g i * ∑ k, v k * v k ) ) _ using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
  · simp +decide [ Fin.forall_fin_succ ];
    exact ⟨ fun h => ⟨ by simp +decide [ h ], fun i => Or.inl ( h i ) ⟩, fun h => h.2 |> fun h' => fun i => Or.resolve_right ( h' i ) ( by intro h''; exact hv_ne <| funext fun x => by simp_all +decide [ Finset.sum_eq_zero_iff_of_nonneg, mul_self_nonneg ] ) ⟩;
  · convert hg using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    ext i; simp +decide [ Fin.sum_univ_succ, mul_sub, mul_comm, mul_left_comm ] ; ring_nf;
    simp +decide [mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _] ; ring

private lemma gramDet_projected_identity
    (n s : ℕ) (hn : 1 ≤ n)
    (v : Fin s → ℤ) (hv_ne : v ≠ 0)
    (w : Fin n → (Fin s → ℤ))
    (hw_indep : LinearIndependent ℤ (Fin.cons v w)) :
    let nsq : ℝ := ∑ i, ((v i : ℤ) : ℝ) ^ 2
    let w'_real : Fin n → (Fin s → ℝ) := fun j i =>
      nsq * ((w j i : ℤ) : ℝ) - (∑ k, ((w j k : ℤ) : ℝ) * ((v k : ℤ) : ℝ)) * ((v i : ℤ) : ℝ)
    gramDet n s w'_real =
      nsq ^ (2 * n - 1) *
      gramDet (n + 1) s (Fin.cons (fun i => ((v i : ℤ) : ℝ)) (fun j i => ((w j i : ℤ) : ℝ))) := by
  obtain ⟨nsq, hnsq⟩ : ∃ nsq : ℤ, nsq > 0 ∧ nsq = ∑ i, (v i : ℤ) ^ 2 := by
    exact ⟨ ∑ i, v i ^ 2, lt_of_le_of_ne ( Finset.sum_nonneg fun _ _ => sq_nonneg _ ) ( Ne.symm <| by contrapose! hv_ne; ext i; simp_all +decide [ Finset.sum_eq_zero_iff_of_nonneg, sq_nonneg ] ), rfl ⟩;
  set N := nsq
  set a : Fin n → ℤ := fun j => ∑ k, w j k * v k;
  have h_det : gramDet n s (fun j i => (N : ℝ) * (w j i : ℝ) - (a j : ℝ) * (v i : ℝ)) = N ^ n * Matrix.det (Matrix.of (fun i j : Fin n => N * (∑ k, (w i k : ℝ) * (w j k : ℝ)) - (a i : ℝ) * (a j : ℝ))) := by
    have h_det : ∀ i j : Fin n, ∑ k : Fin s, ((N : ℝ) * (w i k : ℝ) - (a i : ℝ) * (v k : ℝ)) * ((N : ℝ) * (w j k : ℝ) - (a j : ℝ) * (v k : ℝ)) = N ^ 2 * (∑ k : Fin s, (w i k : ℝ) * (w j k : ℝ)) - N * (a i : ℝ) * (a j : ℝ) := by
      intro i j; simp +decide [ sub_mul, mul_sub, Finset.mul_sum _ _ _, mul_assoc, mul_comm, mul_left_comm, sq ] ; ring_nf;
      simp +zetaDelta at *;
      norm_num [ ← Finset.mul_sum _ _ _, ← Finset.sum_mul, mul_assoc, mul_comm, mul_left_comm, sq ] ; ring_nf;
      norm_cast ; simp +decide [ ← Finset.mul_sum _ _ _, ← Finset.sum_mul, hnsq.2 ] ; ring;
    unfold gramDet; simp +decide [ h_det ] ;
    rw [ show ( Matrix.of fun i j : Fin n => ( N : ℝ ) ^ 2 * ∑ k : Fin s, ( w i k : ℝ ) * ( w j k : ℝ ) - ( N : ℝ ) * ( a i : ℝ ) * ( a j : ℝ ) ) = ( N : ℝ ) • ( Matrix.of fun i j : Fin n => ( N : ℝ ) * ∑ k : Fin s, ( w i k : ℝ ) * ( w j k : ℝ ) - ( a i : ℝ ) * ( a j : ℝ ) ) by ext i j; simp +decide [ mul_sub, mul_assoc, pow_two ] ] ; rw [ Matrix.det_smul ] ; norm_num;
  have h_schur : Matrix.det (Matrix.of (fun i j : Fin n => N * (∑ k, (w i k : ℝ) * (w j k : ℝ)) - (a i : ℝ) * (a j : ℝ))) = N ^ (n - 1) * Matrix.det (Matrix.of (fun i j : Fin (n + 1) => ∑ k, (Fin.cases (fun i => (v i : ℝ)) (fun j i => (w j i : ℝ)) i k) * (Fin.cases (fun i => (v i : ℝ)) (fun j i => (w j i : ℝ)) j k))) := by
    have h_factor : Matrix.det (Matrix.of (fun i j : Fin (n + 1) => ∑ k, (Fin.cases (fun i => (v i : ℝ)) (fun j i => (w j i : ℝ)) i k) * (Fin.cases (fun i => (v i : ℝ)) (fun j i => (w j i : ℝ)) j k))) = N * Matrix.det (Matrix.of (fun i j : Fin n => (∑ k, (w i k : ℝ) * (w j k : ℝ)) - (a i : ℝ) * (a j : ℝ) / N)) := by
      have h_schur : ∀ (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ), A 0 0 ≠ 0 → Matrix.det A = A 0 0 * Matrix.det (Matrix.of (fun i j : Fin n => A (Fin.succ i) (Fin.succ j) - A (Fin.succ i) 0 * A 0 (Fin.succ j) / A 0 0)) := by
        intro A hA_nonzero
        have h_schur : Matrix.det A = Matrix.det (Matrix.of (fun i j : Fin (n + 1) => if i = 0 then A i j else if j = 0 then 0 else A i j - A i 0 * A 0 j / A 0 0)) := by
          have h_schur : ∃ P : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ, P.det = 1 ∧ P * A = Matrix.of (fun i j : Fin (n + 1) => if i = 0 then A i j else if j = 0 then 0 else A i j - A i 0 * A 0 j / A 0 0) := by
            refine' ⟨ Matrix.of ( fun i j => if i = 0 then if j = 0 then 1 else 0 else if j = 0 then -A i 0 / A 0 0 else if i = j then 1 else 0 ), _, _ ⟩ <;> norm_num [ Matrix.det_succ_row_zero ];
            · erw [ Matrix.det_of_upperTriangular ] <;> norm_num;
              intro i j hij; aesop;
            · ext i j; simp +decide [ Matrix.mul_apply, Fin.sum_univ_succ ] ; ring_nf;
              rcases i with ⟨ _ | i, hi ⟩ <;> rcases j with ⟨ _ | j, hj ⟩ <;> norm_num [ Fin.ext_iff, Fin.sum_univ_succ ] at *; all_goals rw [ Finset.sum_eq_single ⟨ i, by linarith ⟩ ] <;> aesop;
          obtain ⟨ P, hP₁, hP₂ ⟩ := h_schur; rw [ ← hP₂, Matrix.det_mul, hP₁, one_mul ] ;
        rw [ h_schur, Matrix.det_succ_column_zero ];
        simp +decide [Matrix.submatrix]
      convert h_schur _ _ using 3 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) <;> norm_num [ Fin.sum_univ_succ, hnsq ];
      · exact Finset.sum_congr rfl fun _ _ => by ring;
      · simp +zetaDelta at *;
        simp +decide only [mul_comm];
        norm_num [ ← sq ];
      · norm_cast ; simp_all +decide [ ← sq ];
        linarith;
    have h_factor : Matrix.det (Matrix.of (fun i j : Fin n => N * (∑ k, (w i k : ℝ) * (w j k : ℝ)) - (a i : ℝ) * (a j : ℝ))) = N ^ n * Matrix.det (Matrix.of (fun i j : Fin n => (∑ k, (w i k : ℝ) * (w j k : ℝ)) - (a i : ℝ) * (a j : ℝ) / N)) := by
      have h_factor : Matrix.det (Matrix.of (fun i j : Fin n => N * (∑ k, (w i k : ℝ) * (w j k : ℝ)) - (a i : ℝ) * (a j : ℝ))) = Matrix.det (Matrix.diagonal (fun _ => (N : ℝ)) * Matrix.of (fun i j : Fin n => (∑ k, (w i k : ℝ) * (w j k : ℝ)) - (a i : ℝ) * (a j : ℝ) / N)) := by
        congr with i j ; simp +decide [ mul_sub, mul_div_cancel₀, hnsq.1.ne' ];
      rw [ h_factor, Matrix.det_mul, Matrix.det_diagonal ] ; norm_num;
    cases n <;> simp_all +decide [ pow_succ', mul_assoc, mul_comm, mul_left_comm ];
  convert h_det.trans ( congr_arg _ h_schur ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
  · norm_cast ; aesop;
  · rw [ ← mul_assoc, ← pow_add, show 2 * n - 1 = n + ( n - 1 ) by omega ] ; norm_num [ hnsq.2 ];
    exact Or.inl rfl

private lemma integer_centering_exists
    (s : ℕ) (v l : Fin s → ℤ) (hv_ne : v ≠ 0) :
    ∃ n : ℤ, |(∑ i, (l i + n * v i) * v i : ℤ)| * 2 ≤ ∑ i, v i * v i := by
  norm_num [ add_mul, Finset.sum_add_distrib, mul_assoc ];
  norm_num [ ← Finset.mul_sum _ _ _, ← Finset.sum_mul ];
  set a := ∑ i, l i * v i
  set d := ∑ i, v i * v i
  have hd_pos : 0 < d := by
    exact lt_of_le_of_ne ( Finset.sum_nonneg fun _ _ => mul_self_nonneg _ ) ( Ne.symm <| by intro H; exact hv_ne <| funext fun i => by simpa [ sq ] using Finset.sum_eq_zero_iff_of_nonneg ( fun _ _ => mul_self_nonneg _ ) |>.1 H i );
  obtain ⟨q, r, hr⟩ : ∃ q r : ℤ, a = q * d + r ∧ 0 ≤ r ∧ r < d := by
    exact ⟨ a / d, a % d, by rw [ Int.ediv_mul_add_emod ], Int.emod_nonneg _ hd_pos.ne', Int.emod_lt_of_pos _ hd_pos ⟩;
  by_cases hr_case : 2 * r ≤ d;
  · exact ⟨ -q, by rw [ abs_of_nonneg ] <;> nlinarith ⟩;
  · exact ⟨ -q - 1, by rw [ abs_of_nonpos ] <;> linarith ⟩

private lemma projection_norm_via_scaled
    (s : ℕ) (v l : Fin s → ℤ) (hv_ne : v ≠ 0) :
    let nsq : ℝ := ∑ i, ((v i : ℤ) : ℝ) ^ 2
    let ytilde : Fin s → ℝ := fun i =>
      nsq * ((l i : ℤ) : ℝ) - (∑ k, ((l k : ℤ) : ℝ) * ((v k : ℤ) : ℝ)) * ((v i : ℤ) : ℝ)
    (∑ i, ((l i : ℤ) : ℝ) ^ 2) -
      (∑ i, ((l i : ℤ) : ℝ) * ((v i : ℤ) : ℝ)) ^ 2 / nsq =
    (∑ i, ytilde i ^ 2) / nsq ^ 2 := by
  by_cases h : ∑ i, ( v i : ℝ ) ^ 2 = 0 <;> simp_all +decide [ Finset.sum_div _ _ _ ];
  · exact False.elim <| hv_ne <| funext fun i => by norm_cast at h; simp_all +decide [ Finset.sum_eq_zero_iff_of_nonneg, sq_nonneg ] ;
  · rw [ ← Finset.sum_div, sub_div' ];
    · simp +decide [ ← Finset.sum_mul _, mul_pow, mul_assoc, mul_comm, mul_left_comm, Finset.sum_add_distrib, sub_sq ];
      norm_num [ ← mul_assoc, ← Finset.sum_mul _ _ _ ] ; rw [ div_eq_div_iff ] <;> first | positivity | ring;
    · exact_mod_cast h

private lemma add_monotone
    (m s : ℕ) (z : Fin m → (Fin s → ℤ))
    (y : Fin m → (Fin s → ℤ))
    (hy_mem : ∀ k, y k ∈ Submodule.span ℤ (Set.range z))
    (hy_indep : LinearIndependent ℝ (fun k : Fin m => (fun i : Fin s => ((y k i : ℤ) : ℝ))))
    (hy_bound : ∏ k : Fin m, (∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2) ≤
        (2 : ℝ) ^ (m * (m - 1)) *
        gramDet m s (fun k i => ((z k i : ℤ) : ℝ))) :
    ∃ y' : Fin m → (Fin s → ℤ),
      (∀ k, y' k ∈ Submodule.span ℤ (Set.range z)) ∧
      LinearIndependent ℝ (fun k : Fin m => (fun i : Fin s => ((y' k i : ℤ) : ℝ))) ∧
      Monotone (fun k : Fin m => ∑ i : Fin s, ((y' k i : ℤ) : ℝ) ^ 2) ∧
      ∏ k : Fin m, (∑ i : Fin s, ((y' k i : ℤ) : ℝ) ^ 2) ≤
        (2 : ℝ) ^ (m * (m - 1)) *
        gramDet m s (fun k i => ((z k i : ℤ) : ℝ)) := by
  obtain ⟨σ, hσ⟩ : ∃ σ : Equiv.Perm (Fin m), Monotone (fun k => ∑ i, ((y (σ k) i : ℤ) : ℝ) ^ 2) := by
    have h_exists_perm : ∃ σ : Fin m → Fin m, Function.Injective σ ∧ ∀ i j, i < j → ∑ k, ((y (σ i) k : ℤ) : ℝ) ^ 2 ≤ ∑ k, ((y (σ j) k : ℤ) : ℝ) ^ 2 := by
      have h_exists_perm : ∀ (n : ℕ) (f : Fin n → ℝ), ∃ σ : Fin n → Fin n, Function.Injective σ ∧ ∀ i j, i < j → f (σ i) ≤ f (σ j) := by
        intro n f;
        induction' n with n ih;
        · simp +decide [ Function.Injective ];
        · -- Let $m$ be the index of the minimum element in $f$.
          obtain ⟨m, hm⟩ : ∃ m : Fin (n + 1), ∀ i : Fin (n + 1), f m ≤ f i := by
            simpa using Finset.exists_min_image Finset.univ ( fun i => f i ) ⟨ 0, Finset.mem_univ 0 ⟩;
          obtain ⟨ σ, hσ₁, hσ₂ ⟩ := ih ( fun i => f ( Fin.succAbove m i ) );
          use Fin.cons m ( fun i => Fin.succAbove m ( σ i ) );
          simp +decide [ Fin.forall_fin_succ, Function.Injective, * ];
          exact ⟨ hσ₁, hσ₂ ⟩;
      exact h_exists_perm m fun k => ∑ i, ( y k i : ℝ ) ^ 2;
    obtain ⟨ σ, hσ₁, hσ₂ ⟩ := h_exists_perm; exact ⟨ Equiv.ofBijective σ ⟨ hσ₁, Finite.injective_iff_surjective.mp hσ₁ ⟩, fun i j hij => by cases hij.lt_or_eq <;> aesop ⟩ ;
  refine' ⟨ fun k ↦ y ( σ k ), _, _, hσ, _ ⟩;
  · exact fun k => hy_mem _;
  · exact hy_indep.comp σ σ.injective;
  · convert hy_bound using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    conv_rhs => rw [ ← Equiv.prod_comp σ ] ;

private lemma projection_add_multiple_invariant
    (s : ℕ) (v z : Fin s → ℤ) (t : ℤ) :
    let nsq : ℝ := ∑ i, ((v i : ℤ) : ℝ) ^ 2
    (∑ i, ((z i + t * v i : ℤ) : ℝ) ^ 2) -
      (∑ i, ((z i + t * v i : ℤ) : ℝ) * ((v i : ℤ) : ℝ)) ^ 2 / nsq =
    (∑ i, ((z i : ℤ) : ℝ) ^ 2) -
      (∑ i, ((z i : ℤ) : ℝ) * ((v i : ℤ) : ℝ)) ^ 2 / nsq := by
  norm_num [ Finset.sum_add_distrib, add_sq, mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _, Finset.sum_mul _ _ _ ];
  norm_num [ mul_pow, mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _, Finset.sum_add_distrib, mul_add, add_mul, add_assoc ] ; ring_nf;
  norm_num [ ← Finset.mul_sum _ _ _, ← Finset.sum_mul ];
  by_cases h : ∑ i : Fin s, ( v i : ℝ ) ^ 2 = 0 <;> simp_all +decide [ sq, mul_assoc, mul_comm, mul_left_comm ];
  · simp_all +decide [ Finset.sum_eq_zero_iff_of_nonneg, mul_self_nonneg ];
  · simpa [ ← Finset.mul_sum _ _ _, ← Finset.sum_mul ] using by ring;

private lemma gramDet_eq_of_same_span
    (m s : ℕ)
    (b1 b2 : Fin m → (Fin s → ℤ))
    (h1 : LinearIndependent ℤ b1)
    (h_span : Submodule.span ℤ (Set.range b1) = Submodule.span ℤ (Set.range b2)) :
    gramDet m s (fun k i => ((b1 k i : ℤ) : ℝ)) = gramDet m s (fun k i => ((b2 k i : ℤ) : ℝ)) := by
  obtain ⟨U, hU⟩ : ∃ U : Matrix (Fin m) (Fin m) ℤ, (∀ k, b1 k = ∑ j, U k j • b2 j) ∧ Int.natAbs U.det = 1 := by
    obtain ⟨U, hU⟩ : ∃ U : Matrix (Fin m) (Fin m) ℤ, (∀ k, b1 k = ∑ j, U k j • b2 j) := by
      have h_basis : ∀ k, b1 k ∈ Submodule.span ℤ (Set.range b2) := by
        exact fun k => h_span ▸ Submodule.subset_span ( Set.mem_range_self k );
      choose! U hU using fun k => Submodule.mem_span_range_iff_exists_fun ℤ |>.1 ( h_basis k );
      exact ⟨ U, fun k => hU k ▸ rfl ⟩;
    obtain ⟨V, hV⟩ : ∃ V : Matrix (Fin m) (Fin m) ℤ, (∀ k, b2 k = ∑ j, V k j • b1 j) := by
      have hV : ∀ k, b2 k ∈ Submodule.span ℤ (Set.range b1) := by
        exact fun k => h_span.symm ▸ Submodule.subset_span ( Set.mem_range_self k );
      choose V hV using fun k => ( Finsupp.mem_span_range_iff_exists_finsupp.mp ( hV k ) );
      exact ⟨ fun k j => V k j, fun k => by simpa [ Finsupp.sum_fintype ] using hV k |> Eq.symm ⟩;
    have hUV : U * V = 1 := by
      have hUV : ∀ k, b1 k = ∑ j, (U * V) k j • b1 j := by
        intro k
        rw [hU k]
        simp [Matrix.mul_apply, hV];
        simp +decide only [Finset.mul_sum _ _ _, Finset.sum_mul, mul_assoc];
        rw [ Finset.sum_comm ];
      have hUV : ∀ k j, (U * V) k j = if k = j then 1 else 0 := by
        intro k j;
        have := Fintype.linearIndependent_iff.mp h1 ( fun i => ( U * V ) k i - if k = i then 1 else 0 ) ?_;
        · exact eq_of_sub_eq_zero ( this j );
        · simp +decide [ sub_smul, Finset.sum_sub_distrib, hUV k ];
      exact Matrix.ext fun i j => by simpa [Matrix.one_apply] using hUV i j;
    have := congr_arg Matrix.det hUV; norm_num at this;
    exact ⟨ U, hU, by rw [ Int.mul_eq_one_iff_eq_one_or_neg_one ] at this; omega ⟩;
  convert gramDet_unimodular_change m s b2 U hU.2 using 3 ; aesop

private lemma successive_minima_inductive_step
    (m s : ℕ) (hm : 2 ≤ m) (hms : m ≤ s)
    (z : Fin m → (Fin s → ℤ))
    (hz_indep : LinearIndependent ℤ z)
    (ih : ∀ (m' : ℕ), m' < m → 1 ≤ m' → m' ≤ s →
      ∀ (z' : Fin m' → (Fin s → ℤ)), LinearIndependent ℤ z' →
        ∃ y : Fin m' → (Fin s → ℤ),
          (∀ k, y k ∈ Submodule.span ℤ (Set.range z')) ∧
          LinearIndependent ℝ (fun k : Fin m' => (fun i : Fin s => ((y k i : ℤ) : ℝ))) ∧
          Monotone (fun k : Fin m' => ∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2) ∧
          ∏ k : Fin m', (∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2) ≤
            (2 : ℝ) ^ (m' * (m' - 1)) *
            gramDet m' s (fun k i => ((z' k i : ℤ) : ℝ))) :
    ∃ y : Fin m → (Fin s → ℤ),
      (∀ k, y k ∈ Submodule.span ℤ (Set.range z)) ∧
      LinearIndependent ℝ (fun k : Fin m => (fun i : Fin s => ((y k i : ℤ) : ℝ))) ∧
      Monotone (fun k : Fin m => ∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2) ∧
      ∏ k : Fin m, (∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2) ≤
        (2 : ℝ) ^ (m * (m - 1)) *
        gramDet m s (fun k i => ((z k i : ℤ) : ℝ)) := by
  obtain ⟨v, hv_mem, hv_ne, hv_min⟩ := shortest_lattice_vector_exists m s (by omega) z hz_indep
  have hv_prim := shortest_is_primitive m s z v hv_mem hv_ne hv_min
  obtain ⟨w, hw_indep, hw_span⟩ := primitive_extends_to_basis m s hm hms z hz_indep v hv_mem hv_prim
  set w' : Fin (m - 1) → (Fin s → ℤ) := fun j i =>
    (∑ k, v k * v k) * w j i - (∑ k, w j k * v k) * v i with w'_def
  have hw'_indep : LinearIndependent ℤ w' := projected_int_vectors_indep (m - 1) s v hv_ne w hw_indep
  obtain ⟨ytil, hytil_mem, hytil_indep, _, hytil_bound⟩ :=
    ih (m - 1) (by omega) (by omega) (by omega) w' hw'_indep
  have hytil_coeffs : ∀ j, ∃ a : Fin (m - 1) → ℤ, ytil j = ∑ k, a k • w' k := by
    intro j
    have := hytil_mem j
    rw [Submodule.mem_span_range_iff_exists_fun] at this
    obtain ⟨c, hc⟩ := this; exact ⟨c, hc.symm⟩
  choose a ha using hytil_coeffs
  set l : Fin (m - 1) → (Fin s → ℤ) := fun j i => ∑ k, a j k * w k i with l_def
  have h_center : ∀ j, ∃ n : ℤ, |(∑ i, (l j i + n * v i) * v i : ℤ)| * 2 ≤ ∑ i, v i * v i := by
    intro j; exact integer_centering_exists s v (l j) hv_ne
  choose ctr hctr using h_center
  set zc : Fin (m - 1) → (Fin s → ℤ) := fun j i => l j i + ctr j * v i with zc_def
  set out : Fin m → (Fin s → ℤ) := fun k =>
    if h : k.val = 0 then v
    else zc ⟨k.val - 1, by omega⟩ with out_def
  have hytil_perp_v : ∀ j, ∑ i, (ytil j i : ℝ) * (v i : ℝ) = 0 := by
    intro j; rw [ ha j ] ; simp +decide [ Finset.sum_mul _ _ _, mul_comm ] ;
    rw [ Finset.sum_comm ] ; simp +decide [ w'_def, mul_sub, mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _ ] ;
    exact sub_eq_zero_of_eq ( Finset.sum_congr rfl fun _ _ => Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring ) )
  have hzc_ne : ∀ j, zc j ≠ 0 := by
    intro j hj_zero
    have hytil_zero : ytil j = 0 := by
      convert congr_arg ( fun x : Fin s → ℤ => fun i => ( ∑ k, ( v k * v k ) ) * x i - ( ∑ k, ( x k * v k ) ) * ( v i ) ) hj_zero using 1;
      · convert ha j using 1;
        ext i; simp +decide [ zc_def, l_def, w'_def ] ; ring_nf;
        simp +decide [ Finset.sum_add_distrib, Finset.mul_sum _ _ _, Finset.sum_mul _ _ _, mul_comm, mul_left_comm, sq ] ; ring_nf;
        simp +decide [ mul_comm, mul_left_comm, Finset.mul_sum _ _ _ ] ; ring_nf;
        exact congrArg₂ _ rfl ( Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring ) );
      · norm_num [ funext_iff ];
    exact hytil_indep.ne_zero j <| by ext i; simp +decide [ hytil_zero ] ;
  have hzc_not_mul_v : ∀ j, ¬ ∃ n : ℤ, ∀ i, zc j i = n * v i := by
    intro j hj
    obtain ⟨n, hn⟩ := hj
    have h_l_eq : l j = (n - ctr j) • v := by
      ext i; specialize hn i; norm_num at *; linarith;
    have h_ytil_zero : ytil j = 0 := by
      have h_ytil_zero : ytil j = (∑ k, v k * v k) • l j - (∑ k, l j k * v k) • v := by
        convert ha j using 1;
        ext i; simp +decide [ l_def, w'_def ] ; ring_nf;
        simp +decide [ mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _ ];
        exact Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring );
      simp +decide [ h_ytil_zero, h_l_eq ];
      simp +decide [ mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _ ];
    exact hytil_indep.ne_zero j ( by ext i; simp +decide [ h_ytil_zero ] )
  have h_mem : ∀ k, out k ∈ Submodule.span ℤ (Set.range z) := by
    intro k; by_cases hk : k.val = 0 <;> simp +decide [ hk, out_def, hv_mem ] ;
    refine' hw_span ▸ Submodule.add_mem _ _ _;
    · rw [ Submodule.mem_span ];
      intro p hp;
      convert p.sum_mem fun i _ => p.smul_mem ( a ⟨ k - 1, by omega ⟩ i ) ( hp <| Set.mem_range_self <| Fin.succ i ) using 1;
      any_goals exact Finset.univ;
      exact funext fun i => by simp +decide [ l_def, Fin.cons ] ;
    · exact Submodule.smul_mem _ _ ( Submodule.subset_span ( Set.mem_range_self 0 ) )
  have h_indep : LinearIndependent ℝ (fun k : Fin m => (fun i : Fin s => ((out k i : ℤ) : ℝ))) := by
    have h_linearInd : ∀ (c : Fin m → ℝ), (∑ k : Fin m, c k • (fun i : Fin s => ((out k i : ℤ) : ℝ))) = 0 → c = 0 := by
      intro c hc
      have h_sum : ∑ j : Fin (m - 1), c ⟨j + 1, by omega⟩ • (fun i : Fin s => ((ytil j i : ℤ) : ℝ)) = 0 := by
        have h_sum : ∑ j : Fin (m - 1), c ⟨j + 1, by omega⟩ • (fun i : Fin s => ((ytil j i : ℤ) : ℝ)) = (fun i : Fin s => ((∑ k, v k * v k) : ℝ) * (∑ j : Fin (m - 1), c ⟨j + 1, by omega⟩ * (zc j i : ℝ)) - (∑ j : Fin (m - 1), c ⟨j + 1, by omega⟩ * (∑ i : Fin s, (zc j i : ℝ) * (v i : ℝ))) * (v i : ℝ)) := by
          have hy : ∀ j i, ytil j i = (∑ k, v k * v k) * zc j i - (∑ i', zc j i' * v i') * v i := by
            intro j i
            have h1 : ytil j i = ∑ k, a j k * ((∑ k', v k' * v k') * w k i - (∑ k', w k k' * v k') * v i) := by
              rw [ha j]; simp [w'_def, Finset.sum_apply]
            have h2 : ∑ i', zc j i' * v i' = ∑ k, a j k * (∑ k', w k k' * v k') + ctr j * ∑ k', v k' * v k' := by
              simp only [zc_def, l_def, add_mul, Finset.sum_add_distrib, Finset.sum_mul, Finset.mul_sum]
              rw [Finset.sum_comm]
              congr 1
              · exact Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring
              · exact Finset.sum_congr rfl fun _ _ => by ring
            have h3 : zc j i = ∑ k, a j k * w k i + ctr j * v i := rfl
            have e1 : ∀ k, a j k * ((∑ k', v k' * v k') * w k i - (∑ k', w k k' * v k') * v i)
                = (∑ k', v k' * v k') * (a j k * w k i) - (a j k * ∑ k', w k k' * v k') * v i :=
              fun k => by ring
            rw [h1, h2, h3, Finset.sum_congr rfl (fun k _ => e1 k), Finset.sum_sub_distrib,
              ← Finset.mul_sum, ← Finset.sum_mul]
            ring
          ext i
          simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, hy]
          push_cast
          simp only [Finset.mul_sum, Finset.sum_mul, mul_sub, Finset.sum_sub_distrib]
          congr 1
          · exact Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring
          · exact Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring
        have h_sum_zero : ∑ j : Fin (m - 1), c ⟨j + 1, by omega⟩ • (fun i : Fin s => ((zc j i : ℤ) : ℝ)) = -c ⟨0, by omega⟩ • (fun i : Fin s => ((v i : ℤ) : ℝ)) := by
          rcases m with ( _ | _ | m ) <;> norm_num [ Fin.sum_univ_succ ] at *;
          · contradiction;
          · contradiction;
          · convert eq_neg_of_add_eq_zero_right hc using 1;
            erw [ Fin.sum_univ_succ ] ; norm_num [ Fin.sum_univ_succ ] ; ring!;
            all_goals simp [out_def]
        have h_sum_zero : ∑ j : Fin (m - 1), c ⟨j + 1, by omega⟩ * (∑ i : Fin s, (zc j i : ℝ) * (v i : ℝ)) = -c ⟨0, by omega⟩ * (∑ i : Fin s, (v i : ℝ) * (v i : ℝ)) := by
          convert congr_arg ( fun f : Fin s → ℝ => ∑ i, f i * ( v i : ℝ ) ) h_sum_zero using 1 <;> norm_num [ Finset.sum_mul _ _ _ ];
          · rw [ Finset.sum_comm ] ; exact Finset.sum_congr rfl fun _ _ => by rw [ Finset.mul_sum _ _ _ ] ; exact Finset.sum_congr rfl fun _ _ => by ring;
          · simp +decide only [Finset.mul_sum _ _ _, mul_assoc];
        convert h_sum using 1;
        ext i; simp +decide [ h_sum_zero ] ; ring_nf;
        rename_i h; replace h := congr_fun h i; simp +decide [ mul_comm] at h;
        simp +decide [ add_comm, h ] ; ring;
      have h_c_zero : ∀ j : Fin (m - 1), c ⟨j + 1, by omega⟩ = 0 := by
        exact fun j => Fintype.linearIndependent_iff.mp hytil_indep _ h_sum j;
      ext ⟨ i, hi ⟩ ; induction i <;> simp +decide [ * ] at *;
      · rw [ Finset.sum_eq_single ⟨ 0, hi ⟩ ] at hc <;> simp +decide at hc ⊢;
        · exact hc.resolve_right fun h => hv_ne <| funext fun i => by simpa using congr_fun h i;
        · intro b hb; rcases b with ⟨ _ | b, hb ⟩ <;> simp +decide [ Fin.ext_iff ] at hb ⊢;
          exact Or.inl <| h_c_zero ⟨ b, Nat.lt_pred_iff.mpr ‹_› ⟩;
      · exact h_c_zero ⟨ _, Nat.lt_pred_iff.mpr hi ⟩;
    rw [ Fintype.linearIndependent_iff ] ; tauto
  have product_bound_qed : ∏ k : Fin m, (∑ i : Fin s, ((out k i : ℤ) : ℝ) ^ 2) ≤
      (2 : ℝ) ^ (m * (m - 1)) * gramDet m s (fun k i => ((z k i : ℤ) : ℝ)) := by
    have hzc_bound : ∀ j, (∑ i, (zc j i : ℝ) ^ 2) ≤ 4 * (∑ i, (ytil j i : ℝ) ^ 2) / (∑ i, (v i : ℝ) ^ 2) ^ 2 := by
      intro j
      have h_centering : (∑ i, ((zc j i : ℤ) : ℝ) ^ 2) - (∑ i, ((zc j i : ℤ) : ℝ) * ((v i : ℤ) : ℝ)) ^ 2 / (∑ i, ((v i : ℤ) : ℝ) ^ 2) = (∑ i, ((ytil j i : ℤ) : ℝ) ^ 2) / (∑ i, ((v i : ℤ) : ℝ) ^ 2) ^ 2 := by
        convert projection_norm_via_scaled s v ( l j ) hv_ne using 1;
        · convert projection_add_multiple_invariant s v ( l j ) ( ctr j ) using 1;
        · simp +decide [ ha, l_def, w'_def ];
          simp +decide [ mul_sub, mul_assoc, mul_comm, Finset.mul_sum _ _ _ ];
          simp +decide only [sq, mul_comm, mul_left_comm];
          simp +decide only [← mul_assoc];
          congr! 3; all_goals exact congrArg₂ _ rfl ( Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring ) );
      have h_centering_bound : (∑ i, ((zc j i : ℤ) : ℝ) ^ 2) - (∑ i, ((zc j i : ℤ) : ℝ) * ((v i : ℤ) : ℝ)) ^ 2 / (∑ i, ((v i : ℤ) : ℝ) ^ 2) ≥ (∑ i, ((zc j i : ℤ) : ℝ) ^ 2) / 4 := by
        have h_centering_bound : (∑ i, ((zc j i : ℤ) : ℝ) * ((v i : ℤ) : ℝ)) ^ 2 ≤ (∑ i, ((v i : ℤ) : ℝ) ^ 2) ^ 2 / 4 := by
          have h_centering_bound : |∑ i, ((zc j i : ℤ) : ℝ) * ((v i : ℤ) : ℝ)| ≤ (∑ i, ((v i : ℤ) : ℝ) ^ 2) / 2 := by
            norm_cast;
            rw [ Rat.divInt_eq_div, le_div_iff₀ ] <;> norm_cast;
            simpa only [ sq ] using hctr j;
          nlinarith only [ abs_le.mp h_centering_bound ];
        have h_centering_bound : (∑ i, ((zc j i : ℤ) : ℝ) ^ 2) ≥ (∑ i, ((v i : ℤ) : ℝ) ^ 2) := by
          apply hv_min;
          · convert h_mem ⟨ j + 1, by omega ⟩ using 1; simp [out_def]
          · exact hzc_ne j;
        rw [ sub_div', ge_iff_le, div_le_div_iff₀ ] <;> nlinarith [ show 0 < ∑ i : Fin s, ( v i : ℝ ) ^ 2 from lt_of_le_of_ne ( Finset.sum_nonneg fun _ _ => sq_nonneg _ ) ( Ne.symm <| by intro h; exact hv_ne <| by ext i; simpa [ sq ] using Finset.sum_eq_zero_iff_of_nonneg ( fun _ _ => sq_nonneg _ ) |>.1 h i ) ];
      ring_nf at *; linarith;
    have h_combined : (∏ k : Fin m, (∑ i : Fin s, ((out k i : ℤ) : ℝ) ^ 2)) ≤
      (∑ i : Fin s, ((v i : ℤ) : ℝ) ^ 2) * (4 / (∑ i : Fin s, ((v i : ℤ) : ℝ) ^ 2) ^ 2) ^ (m - 1) *
      (∏ k : Fin (m - 1), (∑ i : Fin s, ((ytil k i : ℤ) : ℝ) ^ 2)) := by
        have h_split : (∏ k : Fin m, (∑ i : Fin s, ((out k i : ℤ) : ℝ) ^ 2)) = (∑ i : Fin s, ((v i : ℤ) : ℝ) ^ 2) * (∏ j : Fin (m - 1), (∑ i : Fin s, ((zc j i : ℤ) : ℝ) ^ 2)) := by
          rcases m with ⟨ ⟩ <;> norm_num [ Fin.prod_univ_succ ] at *;
          · contradiction;
          · simp +decide [ out_def ];
        rw [ h_split, mul_assoc ];
        gcongr;
        convert Finset.prod_le_prod ?_ fun j _ => hzc_bound j using 1;
        · norm_num [ div_eq_mul_inv, mul_pow, mul_assoc, mul_comm, mul_left_comm, Finset.prod_mul_distrib ];
        · exact fun _ _ => Finset.sum_nonneg fun _ _ => sq_nonneg _;
    have hw'_gramDet : gramDet (m - 1) s (fun k i => ((w' k i : ℤ) : ℝ)) =
      (∑ i : Fin s, ((v i : ℤ) : ℝ) ^ 2) ^ (2 * (m - 1) - 1) *
      gramDet m s (fun k i => ((z k i : ℤ) : ℝ)) := by
        convert gramDet_projected_identity ( m - 1 ) s ( by omega ) v hv_ne w hw_indep using 1;
        · norm_num [ w'_def, sq ];
        · rcases m with ( _ | _ | m ) <;> norm_num at *;
          · contradiction;
          · contradiction;
          · left;
            convert gramDet_eq_of_same_span ( m + 1 + 1 ) s z ( Fin.cons v w ) hz_indep _ using 1;
            · congr! 2;
              rename_i k; induction k using Fin.inductionOn <;> simp +decide [ * ] ;
            · convert hw_span.symm using 1;
              congr with x ; simp +decide [ Fin.exists_fin_succ ];
    refine le_trans h_combined ?_;
    convert mul_le_mul_of_nonneg_left hytil_bound _ using 1;
    · rcases m with ( _ | _ | m ) <;> simp +decide [ Nat.mul_succ, pow_succ' ] at *;
      · contradiction;
      · contradiction;
      · rw [ hw'_gramDet ] ; ring_nf;
        field_simp;
        by_cases h : ∑ x : Fin s, ( v x : ℝ ) ^ 2 = 0 <;> simp +decide [h, mul_comm,
          mul_left_comm, pow_mul', div_eq_mul_inv];
        · exact False.elim <| hv_ne <| funext fun i => by norm_cast at h; simpa [ sq ] using Finset.sum_eq_zero_iff_of_nonneg ( fun _ _ => sq_nonneg _ ) |>.1 h i;
        · norm_num [ ← mul_assoc, ← mul_pow ];
    · exact mul_nonneg ( Finset.sum_nonneg fun _ _ => sq_nonneg _ ) ( pow_nonneg ( div_nonneg zero_le_four ( sq_nonneg _ ) ) _ )
  exact add_monotone m s z out h_mem h_indep product_bound_qed

private lemma successive_minima_product_bound_abstract
    (m s : ℕ) (hm : 1 ≤ m) (hms : m ≤ s)
    (z : Fin m → (Fin s → ℤ))
    (hz_indep : LinearIndependent ℤ z) :
    ∃ y : Fin m → (Fin s → ℤ),
      (∀ k, y k ∈ Submodule.span ℤ (Set.range z)) ∧
      LinearIndependent ℝ (fun k : Fin m => (fun i : Fin s => ((y k i : ℤ) : ℝ))) ∧
      Monotone (fun k : Fin m => ∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2) ∧
      ∏ k : Fin m, (∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2) ≤
        (2 : ℝ) ^ (m * (m - 1)) *
        gramDet m s (fun k i => ((z k i : ℤ) : ℝ)) := by
  induction' m using Nat.strongRecOn with m ih generalizing s;
  by_cases hm2 : m ≥ 2;
  · exact successive_minima_inductive_step m s hm2 hms z hz_indep ( fun m' hm' hm1 hm2 z' hz' => ih m' hm' s hm1 hm2 z' hz' );
  · interval_cases m;
    refine' ⟨ fun _ => z 0, _, _, _, _ ⟩ <;> norm_num [ Monotone ];
    · exact Submodule.subset_span ( Set.mem_range_self _ );
    · intro h; have := hz_indep.ne_zero 0; simp_all +decide [ funext_iff ] ;
    · unfold gramDet; norm_num [ Fin.eq_zero ] ;
      norm_num [ sq ]

private lemma gramDet_orthogonal_factorization
    (r s : ℕ) (hs : s = 2 * r)
    (b z : Fin r → (Fin s → ℝ))
    (h_orth : ∀ j k : Fin r, ∑ i : Fin s, b j i * z k i = 0) :
    let C : Fin (2 * r) → (Fin s → ℝ) := fun idx =>
      if h : idx.val < r then b ⟨idx.val, h⟩ else z ⟨idx.val - r, by omega⟩
    Matrix.det (Matrix.of (fun i j : Fin (2 * r) => ∑ k : Fin s, C i k * C j k)) =
    Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin s, b i k * b j k)) *
    Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin s, z i k * z j k)) := by
  intro C
  let ψf : Fin (2 * r) → Fin r ⊕ Fin r := fun i =>
    if h : i.val < r then Sum.inl ⟨i.val, h⟩ else Sum.inr ⟨i.val - r, by omega⟩
  have hinj : Function.Injective ψf := by
    intro i j hij
    by_cases hi : i.val < r <;> by_cases hj : j.val < r <;> simp [ψf, hi, hj] at hij <;> ext <;> omega
  have hsurj : Function.Surjective ψf := by
    rintro (i | i)
    · exact ⟨⟨i.val, by omega⟩, by simp [ψf]⟩
    · refine ⟨⟨i.val + r, by omega⟩, ?_⟩
      simp [ψf]
  let e : Fin (2 * r) ≃ Fin r ⊕ Fin r := Equiv.ofBijective ψf ⟨hinj, hsurj⟩
  have he_l : ∀ i : Fin r, e.symm (Sum.inl i) = ⟨i.val, by omega⟩ := by
    intro i; rw [Equiv.symm_apply_eq]; show _ = ψf _; simp [ψf]
  have he_r : ∀ i : Fin r, e.symm (Sum.inr i) = ⟨i.val + r, by omega⟩ := by
    intro i; rw [Equiv.symm_apply_eq]; show _ = ψf _; simp [ψf]
  have hC_l : ∀ i : Fin r, C (e.symm (Sum.inl i)) = b i := by
    intro i; rw [he_l]; simp [C]
  have hC_r : ∀ i : Fin r, C (e.symm (Sum.inr i)) = z i := by
    intro i; rw [he_r]; simp [C]
  have key : (Matrix.of (fun i j : Fin (2 * r) => ∑ k : Fin s, C i k * C j k)).submatrix e.symm e.symm
      = Matrix.fromBlocks (Matrix.of (fun i j : Fin r => ∑ k : Fin s, b i k * b j k)) 0 0
          (Matrix.of (fun i j : Fin r => ∑ k : Fin s, z i k * z j k)) := by
    ext (i | i) (j | j)
    · simp [hC_l]
    · simp [hC_l, hC_r, h_orth]
    · simp only [Matrix.submatrix_apply, Matrix.of_apply, hC_l, hC_r, Matrix.fromBlocks_apply₂₁, Matrix.zero_apply]
      simpa only [mul_comm] using h_orth j i
    · simp [hC_r]
  rw [← Matrix.det_submatrix_equiv_self e.symm, key, Matrix.det_fromBlocks_zero₂₁]


private lemma gramDet_product_is_square
    (r s : ℕ) (hs : s = 2 * r)
    (b z : Fin r → (Fin s → ℤ))
    (h_orth : ∀ j k : Fin r, ∑ i : Fin s, (b j i : ℝ) * (z k i : ℝ) = 0)
    (h_indep_b : LinearIndependent ℝ (fun j : Fin r => (fun i : Fin s => ((b j i : ℤ) : ℝ))))
    (h_indep_z : LinearIndependent ℝ (fun k : Fin r => (fun i : Fin s => ((z k i : ℤ) : ℝ)))) :
    ∃ d : ℤ, d ≠ 0 ∧
    Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin s, (b i k : ℝ) * (b j k : ℝ))) *
    Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin s, (z i k : ℝ) * (z j k : ℝ))) =
    (d : ℝ) ^ 2 := by
  set C : Matrix (Fin (2 * r)) (Fin s) ℤ := Matrix.of (fun i j =>
    if h : i.val < r then b ⟨i.val, h⟩ j else z ⟨i.val - r, by omega⟩ j);
  have h_det_C_sq : Matrix.det (Matrix.of (fun i j : Fin (2 * r) => ∑ k : Fin s, C i k * C j k)) = (Matrix.det (Matrix.of (fun i j : Fin (2 * r) => C i (Fin.cast hs.symm j)))) ^ 2 := by
    have h_det_C_sq : Matrix.of (fun i j : Fin (2 * r) => ∑ k : Fin s, C i k * C j k) = (Matrix.of (fun i j : Fin (2 * r) => C i (Fin.cast hs.symm j))) * (Matrix.of (fun i j : Fin (2 * r) => C i (Fin.cast hs.symm j))).transpose := by
      ext i j; simp +decide [ Matrix.mul_apply ] ;
      refine' Finset.sum_bij ( fun k _ => ⟨ k, by linarith [ Fin.is_lt k ] ⟩ ) _ _ _ _ <;> simp +decide [ Fin.ext_iff ];
      exact fun i => ⟨ ⟨ i, by linarith [ Fin.is_lt i ] ⟩, rfl ⟩;
    rw [ h_det_C_sq, Matrix.det_mul, Matrix.det_transpose, sq ];
  have h_det_C_prod : Matrix.det (Matrix.of (fun i j : Fin (2 * r) => ∑ k : Fin s, C i k * C j k)) = Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin s, b i k * b j k)) * Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin s, z i k * z j k)) := by
    convert gramDet_orthogonal_factorization r s hs ( fun i j => ( b i j : ℝ ) ) ( fun i j => ( z i j : ℝ ) ) _ using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    · norm_num [ ← @Int.cast_inj ℝ ];
      norm_num [ Matrix.det_apply' ];
      norm_num +zetaDelta at *;
      congr!; all_goals split_ifs <;> rfl;
    · convert h_orth using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
  have h_det_b_nonzero : Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin s, b i k * b j k)) ≠ 0 := by
    have h_det_b_nonzero : Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin s, (b i k : ℝ) * (b j k : ℝ))) ≠ 0 := by
      have h_det_b_nonzero : ∀ (v : Fin r → ℝ), v ≠ 0 → ∑ i, ∑ j, v i * v j * (∑ k, (b i k : ℝ) * (b j k : ℝ)) > 0 := by
        intro v hv_nonzero
        have h_sum_pos : ∑ i, ∑ j, v i * v j * (∑ k, (b i k : ℝ) * (b j k : ℝ)) = ∑ k, (∑ i, v i * (b i k : ℝ)) ^ 2 := by
          simp +decide only [Finset.mul_sum _ _ _, pow_two, mul_comm, mul_left_comm];
          exact Eq.symm ( by rw [ Finset.sum_comm ] ; exact Finset.sum_congr rfl fun _ _ => Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring ) );
        contrapose! hv_nonzero;
        have h_sum_zero : ∀ k, ∑ i, v i * (b i k : ℝ) = 0 := by
          exact fun k => sq_eq_zero_iff.mp ( le_antisymm ( le_trans ( Finset.single_le_sum ( fun a _ => sq_nonneg ( ∑ i : Fin r, v i * ( b i a : ℝ ) ) ) ( Finset.mem_univ k ) ) ( h_sum_pos ▸ hv_nonzero ) ) ( sq_nonneg _ ) );
        rw [ Fintype.linearIndependent_iff ] at h_indep_b;
        exact funext fun i => h_indep_b v ( by ext k; simpa [ mul_comm ] using h_sum_zero k ) i;
      contrapose! h_det_b_nonzero;
      obtain ⟨ v, hv ⟩ := Matrix.exists_mulVec_eq_zero_iff.mpr h_det_b_nonzero;
      use v;
      simp_all +decide [ funext_iff, Matrix.mulVec, dotProduct ];
      simp_all +decide [ ← Finset.mul_sum _ _ _, mul_assoc, mul_comm];
    norm_num [ Matrix.det_apply' ] at *;
    exact_mod_cast h_det_b_nonzero
  have h_det_z_nonzero : Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin s, z i k * z j k)) ≠ 0 := by
    have h_det_z_nonzero : Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin s, (z i k : ℝ) * (z j k : ℝ))) ≠ 0 := by
      have h_det_z_nonzero : ∀ (v : Fin r → ℝ), v ≠ 0 → ∑ i, ∑ j, v i * v j * ∑ k, (z i k : ℝ) * (z j k : ℝ) > 0 := by
        intros v hv_nonzero
        have h_sum_pos : ∑ i, ∑ j, v i * v j * ∑ k, (z i k : ℝ) * (z j k : ℝ) = ∑ k, (∑ i, v i * (z i k : ℝ)) ^ 2 := by
          simp +decide only [Finset.mul_sum _ _ _, pow_two, mul_comm, mul_left_comm];
          exact Eq.symm ( by rw [ Finset.sum_comm ] ; exact Finset.sum_congr rfl fun _ _ => Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring ) );
        contrapose! hv_nonzero;
        have h_sum_zero : ∀ k, ∑ i, v i * (z i k : ℝ) = 0 := by
          exact fun k => sq_eq_zero_iff.mp ( le_antisymm ( le_trans ( Finset.single_le_sum ( fun a _ => sq_nonneg ( ∑ i, v i * ( z i a : ℝ ) ) ) ( Finset.mem_univ k ) ) ( h_sum_pos ▸ hv_nonzero ) ) ( sq_nonneg _ ) );
        rw [ Fintype.linearIndependent_iff ] at h_indep_z;
        exact funext fun i => h_indep_z v ( by ext k; simpa [ mul_comm ] using h_sum_zero k ) i;
      contrapose! h_det_z_nonzero;
      obtain ⟨ v, hv ⟩ := Matrix.exists_mulVec_eq_zero_iff.mpr h_det_z_nonzero;
      use v;
      simp_all +decide [ funext_iff, Matrix.mulVec, dotProduct ];
      simp_all +decide [← Finset.mul_sum _ _ _, mul_assoc, mul_comm];
    norm_num [ Matrix.det_apply' ] at *;
    exact_mod_cast h_det_z_nonzero;
  norm_cast at *;
  refine' ⟨ _, _, _ ⟩;
  exact Matrix.det ( Matrix.of fun i j => C i ( Fin.cast hs.symm j ) );
  · intro h; simp_all +decide [ sq ] ;
  · norm_num [ ← h_det_C_sq, ← h_det_C_prod ];
    convert congr_arg ( ( ↑ ) : ℤ → ℝ ) h_det_C_prod.symm using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    norm_num [ Matrix.det_apply' ]

private lemma int_linearIndependent_implies_real
    (r s : ℕ) (z : Fin r → (Fin s → ℤ))
    (hz : LinearIndependent ℤ z) :
    LinearIndependent ℝ (fun k : Fin r => (fun i : Fin s => ((z k i : ℤ) : ℝ))) := by
  convert Fintype.linearIndependent_iff.mpr _;
  exact inferInstance;
  intro g hg i
  by_contra h_nonzero
  have h_det : Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin s, (z i k : ℝ) * (z j k : ℝ))) = 0 := by
    rw [ ← Matrix.exists_vecMul_eq_zero_iff ];
    refine' ⟨ g, _, _ ⟩ <;> simp_all +decide [ funext_iff, Matrix.vecMul, dotProduct ];
    · use i;
    · intro i; simp +decide only [Finset.mul_sum _ _ _] ;
      rw [ Finset.sum_comm ] ; simp_all +decide [ ← mul_assoc, ← Finset.sum_mul ] ;
  generalize_proofs at *; (
  have h_lin_dep_int : ∃ d : Fin r → ℤ, d ≠ 0 ∧ ∑ i, d i • z i = 0 := by
    have h_lin_dep_rat : ∃ d : Fin r → ℚ, d ≠ 0 ∧ ∑ i, d i • (fun i_1 => (z i i_1 : ℚ)) = 0 := by
      have h_lin_dep_rat : ∃ d : Fin r → ℚ, d ≠ 0 ∧ Matrix.mulVec (Matrix.of (fun i j : Fin r => ∑ k : Fin s, (z i k : ℚ) * (z j k : ℚ))) d = 0 := by
        convert Matrix.exists_mulVec_eq_zero_iff.mpr _;
        all_goals try infer_instance
        generalize_proofs at *; (
        convert h_det using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)))
        generalize_proofs at *; (
        norm_num [ Matrix.det_apply' ];
        norm_cast))
      generalize_proofs at *; (
      obtain ⟨ d, hd_ne_zero, hd_eq_zero ⟩ := h_lin_dep_rat
      use d
      generalize_proofs at *; (
      have h_lin_dep_rat : ∑ i, d i • (fun i_1 => (z i i_1 : ℚ)) = 0 := by
        have h_inner : ∀ i, ∑ j, d j * (∑ k, (z i k : ℚ) * (z j k : ℚ)) = 0 := by
          exact fun i => by simpa [ Matrix.mulVec, dotProduct, mul_comm ] using congr_fun hd_eq_zero i;
        have h_inner : ∑ i, ∑ j, d i * d j * (∑ k, (z i k : ℚ) * (z j k : ℚ)) = 0 := by
          simp_all +decide [ ← Finset.mul_sum _ _ _, mul_assoc ]
        generalize_proofs at *; (
        have h_inner : ∑ k, (∑ i, d i * (z i k : ℚ)) ^ 2 = 0 := by
          convert h_inner using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)))
          generalize_proofs at *; (
          simp +decide only [pow_two, Finset.mul_sum _ _ _, mul_comm, mul_left_comm];
          exact Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring ) ))
        generalize_proofs at *; (
        exact funext fun k => by simpa [ sq ] using Finset.sum_eq_zero_iff_of_nonneg ( fun _ _ => sq_nonneg _ ) |>.1 h_inner k;))
      generalize_proofs at *; (
      exact ⟨ hd_ne_zero, h_lin_dep_rat ⟩)))
    generalize_proofs at *; (
    obtain ⟨ d, hd₁, hd₂ ⟩ := h_lin_dep_rat
    generalize_proofs at *; (
    obtain ⟨q, hq⟩ : ∃ q : ℕ, q > 0 ∧ ∀ i, ∃ k : ℤ, d i = k / q := by
      use ∏ i, (d i).den, Finset.prod_pos fun i _ => Nat.cast_pos.mpr (Rat.pos _), fun i => ⟨(d i).num * (∏ j ∈ Finset.univ.erase i, (d j).den), by
        simp +decide [ ← Finset.mul_prod_erase _ _ ( Finset.mem_univ i ) ];
        rw [ mul_div_mul_right _ _ <| Finset.prod_ne_zero_iff.mpr fun j hj => Nat.cast_ne_zero.mpr <| Rat.den_nz _, Rat.num_div_den ]⟩
    generalize_proofs at *; (
    choose k hk using hq.2; use fun i => k i; simp_all +decide [funext_iff] ;
    simp_all +decide [ div_mul_eq_mul_div, ← Finset.sum_div _ _ _, ne_of_gt hq ];
    exact_mod_cast hd₂;)))
  generalize_proofs at *; (
  exact h_lin_dep_int.elim fun d hd => hd.1 <| by simpa [ funext_iff ] using Fintype.linearIndependent_iff.mp hz d hd.2;))

private lemma kernel_has_complement
    (n m : ℕ) (phi : (Fin n → ℤ) →ₗ[ℤ] (Fin m → ℤ)) :
    ∃ W : Submodule ℤ (Fin n → ℤ), IsCompl (LinearMap.ker phi) W := by
  obtain ⟨sec, hsec⟩ : ∃ sec : (Fin n → ℤ) ⧸ phi.ker →ₗ[ℤ] (Fin n → ℤ), Submodule.mkQ phi.ker ∘ₗ sec = LinearMap.id := by
    convert Module.projective_lifting_property ( Submodule.mkQ phi.ker ) LinearMap.id ( Submodule.Quotient.mk_surjective _ );
    convert Module.Projective.of_equiv ( phi.quotKerEquivRange ).symm;
  refine' ⟨ LinearMap.range sec, _, _ ⟩;
  · simp_all +decide [ Submodule.disjoint_def, LinearMap.ext_iff ];
    intro x hx y hy; specialize hsec y; simp_all +decide ;
    rw [ ← hy, show y = 0 from by rw [ ← hsec, show Submodule.Quotient.mk x = 0 from by rw [ Submodule.Quotient.mk_eq_zero ] ; aesop ] ] ; aesop;
  · rw [ codisjoint_iff ];
    ext x; simp ;
    rw [ Submodule.mem_sup ];
    refine' ⟨ x - sec ( Submodule.mkQ phi.ker x ), _, sec ( Submodule.mkQ phi.ker x ), _, _ ⟩ <;> norm_num;
    replace hsec := LinearMap.congr_fun hsec ( Submodule.Quotient.mk x ) ; simp_all +decide ;
    rw [ ← eq_comm, ← sub_eq_zero ] ; erw [ Submodule.Quotient.eq ] at hsec ; aesop;

private lemma gramDet_int_ge_one
    (r s : ℕ) (z : Fin r → (Fin s → ℤ))
    (hz : LinearIndependent ℤ z) :
    1 ≤ gramDet r s (fun k i => ((z k i : ℤ) : ℝ)) := by
  have h_real_indep : LinearIndependent ℝ (fun k => fun i => ((z k i : ℤ) : ℝ)) := by
    convert int_linearIndependent_implies_real r s z hz using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
  have h_pos_def : Matrix.PosDef (Matrix.of (fun i j => ∑ k, (z i k : ℝ) * (z j k : ℝ))) := by
    have h_pos_def : ∀ (v : Fin r → ℝ), v ≠ 0 → 0 < ∑ i, ∑ j, v i * v j * ∑ k, (z i k : ℝ) * (z j k : ℝ) := by
      intro v hv_ne_zero
      have h_pos_def : 0 < ∑ k, (∑ i, v i * (z i k : ℝ)) ^ 2 := by
        contrapose! hv_ne_zero
        generalize_proofs at *; (
        have h_zero : ∀ k, ∑ i, v i * (z i k : ℝ) = 0 := by
          exact fun k => sq_eq_zero_iff.mp ( le_antisymm ( le_trans ( Finset.single_le_sum ( fun a _ => sq_nonneg ( ∑ i, v i * ( z i a : ℝ ) ) ) ( Finset.mem_univ k ) ) hv_ne_zero ) ( sq_nonneg _ ) )
        generalize_proofs at *; (
        rw [ Fintype.linearIndependent_iff ] at h_real_indep
        generalize_proofs at *; (
        exact funext fun i => h_real_indep v ( by ext k; simpa [ mul_comm ] using h_zero k ) i)))
      generalize_proofs at *; (
      convert h_pos_def using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) ; simp +decide [ pow_two, mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _] ; ring_nf!;
      exact Finset.sum_comm_cycle)
    generalize_proofs at *; (
    constructor <;> norm_num [ Matrix.PosDef ];
    · ext i j; simp +decide [ mul_comm ] ;
    · intro x hx; specialize h_pos_def ( fun i => x i ) ; simp_all +decide [ Finsupp.sum_fintype, mul_assoc, mul_comm, mul_left_comm ] ;);
  have h_det_int : ∃ d : ℤ, Matrix.det (Matrix.of (fun i j => ∑ k, (z i k : ℝ) * (z j k : ℝ))) = d := by
    norm_num [ Matrix.det_apply' ];
    exact ⟨ ∑ x : Equiv.Perm ( Fin r ), Equiv.Perm.sign x * ∏ x_1 : Fin r, ∑ k : Fin s, z ( x x_1 ) k * z x_1 k, by push_cast; rfl ⟩;
  obtain ⟨ d, hd ⟩ := h_det_int; have := h_pos_def.det_pos; simp_all +decide [ gramDet ] ;
  exact_mod_cast this

private lemma ker_rank_ge_r
    (r : ℕ) (phi : (Fin (2 * r) → ℤ) →ₗ[ℤ] (Fin r → ℤ)) :
    r ≤ Module.finrank ℤ (LinearMap.ker phi) := by
  have h_rank_nullity : Module.finrank ℤ (Fin (2 * r) → ℤ) = Module.finrank ℤ (↥phi.ker) + Module.finrank ℤ (↥(LinearMap.range phi)) := by
    have := Submodule.finrank_quotient_add_finrank phi.ker;
    rw [ ← this, add_comm, ← LinearEquiv.finrank_eq ( phi.quotKerEquivRange ) ];
  norm_num +zetaDelta at *;
  linarith [ show Module.finrank ℤ ( LinearMap.range phi ) ≤ r from le_trans ( Submodule.finrank_le _ ) ( by norm_num ) ]

private lemma kernel_and_complement_exist
    (r : ℕ) (hr : 0 < r)
    (phi : (Fin (2 * r) → ℤ) →ₗ[ℤ] (Fin r → ℤ)) :
    ∃ (z w : Fin r → (Fin (2 * r) → ℤ)),
      (∀ k : Fin r, phi (z k) = 0) ∧
      LinearIndependent ℤ z ∧
      let Q : Matrix (Fin (2 * r)) (Fin (2 * r)) ℤ :=
        Matrix.of (fun i j =>
          if h : j.val < r then z ⟨j.val, h⟩ i
          else w ⟨j.val - r, by omega⟩ i)
      Q.det = 1 ∨ Q.det = -1 := by
  have h_basis : ∃ (b : Module.Basis (Fin (2 * r)) ℤ (Fin (2 * r) → ℤ)), (∀ k : Fin r, phi (b (Fin.castLE (by omega) k)) = 0) := by
    obtain ⟨K, W, hK, hW, h_compl⟩ : ∃ K W : Submodule ℤ (Fin (2 * r) → ℤ), K = LinearMap.ker phi ∧ IsCompl K W := by
      exact ⟨ _, _, rfl, kernel_has_complement _ _ _ |> Classical.choose_spec ⟩;
    obtain ⟨bK, hbK⟩ : ∃ bK : Module.Basis (Fin (Module.finrank ℤ K)) ℤ K, True := by
      exact ⟨ Module.finBasis ℤ K, trivial ⟩
    obtain ⟨bW, hbW⟩ : ∃ bW : Module.Basis (Fin (Module.finrank ℤ W)) ℤ W, True := by
      exact ⟨ Module.finBasis ℤ W, trivial ⟩;
    obtain ⟨b, hb⟩ : ∃ b : Module.Basis (Fin (Module.finrank ℤ K + Module.finrank ℤ W)) ℤ (Fin (2 * r) → ℤ), (∀ k : Fin (Module.finrank ℤ K), b (Fin.castLE (by omega) k) ∈ K) ∧ (∀ k : Fin (Module.finrank ℤ W), b (Fin.castLE (by omega) (Fin.addNat k (Module.finrank ℤ K))) ∈ W) := by
      have h_combined_basis : ∃ b : Module.Basis (Fin (Module.finrank ℤ K) ⊕ Fin (Module.finrank ℤ W)) ℤ (Fin (2 * r) → ℤ), (∀ k : Fin (Module.finrank ℤ K), b (Sum.inl k) ∈ K) ∧ (∀ k : Fin (Module.finrank ℤ W), b (Sum.inr k) ∈ W) := by
        refine' ⟨ _, _, _ ⟩;
        refine' ( bK.prod bW ).map _;
        refine' ( Submodule.prodEquivOfIsCompl K W _ );
        exact ⟨ hW, h_compl ⟩;
        · intro k; simp [Module.Basis.map_apply, Module.Basis.prod_apply, Submodule.coe_prodEquivOfIsCompl']
        · simp +decide [ Module.Basis.map ];
      obtain ⟨ b, hb₁, hb₂ ⟩ := h_combined_basis;
      refine' ⟨ b.reindex ( Equiv.ofBijective _ ⟨ _, _ ⟩ ), _, _ ⟩;
      use fun x => x.elim ( fun k => Fin.castLE ( by omega ) k ) ( fun k => Fin.castLE ( by omega ) ( k.addNat ( Module.finrank ℤ K ) ) );
      all_goals norm_num [ Function.Injective, Function.Surjective ];
      all_goals norm_num [ Fin.ext_iff, Fin.val_add ];
      exact ⟨ fun a b h => False.elim <| by linarith [ Fin.is_lt a, Fin.is_lt b ], fun b a h => False.elim <| by linarith [ Fin.is_lt a, Fin.is_lt b ] ⟩;
      exact fun x => if hx : x.val < Module.finrank ℤ K then Or.inl ⟨ ⟨ x.val, hx ⟩, rfl ⟩ else Or.inr ⟨ ⟨ x.val - Module.finrank ℤ K, by omega ⟩, by simp +decide [ Nat.sub_add_cancel ( show Module.finrank ℤ K ≤ x.val from le_of_not_gt hx ) ] ⟩;
      · intro k; convert hb₁ k using 1;
        congr! 1;
        (simp +decide [ Equiv.symm_apply_eq ]) <;> rfl
      · intro k; convert hb₂ k using 1;
        congr! 1;
        (simp +decide [ Equiv.symm_apply_eq ]) <;> rfl
    have h_rank : Module.finrank ℤ K + Module.finrank ℤ W = 2 * r := by
      convert Module.finrank_eq_card_basis b |> Eq.symm; all_goals norm_num;
    use b.reindex (finCongr h_rank);
    intro k; specialize hb; have := hb.1 ⟨ k, by linarith [ Fin.is_lt k, show Module.finrank ℤ K ≥ r from by
                                                                          have := ker_rank_ge_r r phi; aesop; ] ⟩ ; aesop;
  obtain ⟨ b, hb ⟩ := h_basis;
  refine' ⟨ fun k => b ( Fin.castLE ( by omega ) k ), fun k => b ( Fin.castLE ( by omega ) ( Fin.addNat k r ) ), _, _, _ ⟩ <;> simp_all +decide [ Fintype.linearIndependent_iff ];
  · intro g hg i; have := b.linearIndependent; simp_all +decide [ Fintype.linearIndependent_iff ] ;
    convert this ( fun x => if hx : x.val < r then g ⟨ x.val, hx ⟩ else 0 ) _ ⟨ i, by linarith [ Fin.is_lt i ] ⟩ using 1 ; simp +decide ;
    rw [ ← Finset.sum_subset ( Finset.subset_univ ( Finset.image ( fun x : Fin r => Fin.castLE ( by omega ) x ) Finset.univ ) ) ] <;> norm_num [ Finset.sum_image ];
    · rw [ Finset.sum_image ] ; aesop;
      exact fun x _ y _ h => by simpa [ Fin.ext_iff ] using h;
    · intro x hx; split_ifs <;> simp_all +decide [ Fin.ext_iff ] ;
      exact False.elim <| hx ⟨ x, by linarith ⟩ rfl;
  · have h_det : Matrix.det (Matrix.of (fun i j => b j i)) = 1 ∨ Matrix.det (Matrix.of (fun i j => b j i)) = -1 := by
      have h_det : IsUnit (Matrix.det (Matrix.of (fun i j => b j i))) := by
        have h_det : IsUnit (Matrix.det (Matrix.of (fun i j => b j i))) := by
          have h_basis : ∀ (v : Fin (2 * r) → ℤ), ∃ (c : Fin (2 * r) → ℤ), v = ∑ i, c i • b i := by
            exact fun v => ⟨ _, Eq.symm ( b.sum_repr v ) ⟩
          have h_det : ∀ (v : Fin (2 * r) → ℤ), ∃ (c : Fin (2 * r) → ℤ), v = Matrix.mulVec (Matrix.of (fun i j => b j i)) c := by
            intro v; obtain ⟨ c, hc ⟩ := h_basis v; use c; ext i; simp +decide [ hc, Matrix.mulVec, dotProduct ] ;
            grind +revert
          generalize_proofs at *;
          have h_det : Function.Surjective (Matrix.mulVec (Matrix.of (fun i j => b j i))) := by
            exact fun v => by obtain ⟨ c, rfl ⟩ := h_det v; exact ⟨ c, rfl ⟩ ;
          generalize_proofs at *;
          have h_det : ∃ (A : Matrix (Fin (2 * r)) (Fin (2 * r)) ℤ), Matrix.of (fun i j => b j i) * A = 1 := by
            exact Matrix.mulVec_surjective_iff_exists_right_inverse.mp h_det
          generalize_proofs at *;
          exact isUnit_iff_exists_inv.mpr ⟨ h_det.choose.det, by simpa using congr_arg Matrix.det h_det.choose_spec ⟩
        generalize_proofs at *;
        exact h_det;
      exact Int.isUnit_iff.mp h_det;
    convert h_det using 1;
    · congr! 2;
      ext i j; aesop;
    · congr! 2;
      ext i j; aesop

private lemma det_block_zero_upper_left (r : ℕ)
    (B C D : Matrix (Fin r) (Fin r) ℤ) :
    Matrix.det (Matrix.fromBlocks 0 B C D) =
    (-1) ^ (r * r) * Matrix.det B * Matrix.det C := by
  have h_swap_sign : Matrix.det (Matrix.fromBlocks 0 (1 : Matrix (Fin r) (Fin r) ℤ) 1 0) = (-1 : ℤ) ^ r := by
    convert Matrix.det_permutation ( Equiv.sumComm ( Fin r ) ( Fin r ) ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    all_goals try infer_instance;
    · congr ; ext i j ; aesop;
    · -- The permutation sumComm (Fin r) (Fin r) can be decomposed into r transpositions.
      have h_decomp : ∃ σ : Equiv.Perm (Fin r ⊕ Fin r), σ = Equiv.sumComm (Fin r) (Fin r) ∧ σ.support.card = 2 * r := by
        simp +decide [ two_mul, Equiv.Perm.support ];
        rw [ Finset.filter_true_of_mem ] <;> simp +decide [ Finset.card_univ ];
      obtain ⟨ σ, hσ₁, hσ₂ ⟩ := h_decomp; rw [ ← hσ₁ ] ; rw [ Equiv.Perm.sign_of_cycleType ] ; simp +decide ;
      have := Equiv.Perm.sum_cycleType σ; simp_all +decide [ two_mul ] ;
      have h_cycle_type : ∀ c ∈ Equiv.Perm.cycleType (Equiv.sumComm (Fin r) (Fin r)), c = 2 := by
        intro c hc; have := Equiv.Perm.two_le_of_mem_cycleType hc; (
        have h_cycle_type : ∀ c ∈ Equiv.Perm.cycleType (Equiv.sumComm (Fin r) (Fin r)), c ≤ 2 := by
          intros c hc; exact (by
          have h_cycle_type : ∀ c ∈ Equiv.Perm.cycleType (Equiv.sumComm (Fin r) (Fin r)), c ∣ 2 := by
            intros c hc; exact (by
            have h_cycle_type : ∀ c ∈ Equiv.Perm.cycleType (Equiv.sumComm (Fin r) (Fin r)), c ∣ orderOf (Equiv.sumComm (Fin r) (Fin r)) := by
              exact fun c a => Equiv.Perm.dvd_of_mem_cycleType a;
            exact dvd_trans ( h_cycle_type c hc ) ( orderOf_dvd_of_pow_eq_one ( by aesop ) ));
          exact Nat.le_of_dvd ( by decide ) ( h_cycle_type c hc ));
        exact le_antisymm ( h_cycle_type c hc ) this);
      rw [ Multiset.eq_replicate_of_mem fun x hx => h_cycle_type x hx ] at this ⊢ ; norm_num at this ⊢ ; ring_nf at this ⊢ ; aesop;
  convert congr_arg ( fun x : ℤ => x * Matrix.det ( Matrix.fromBlocks C D 0 B ) ) h_swap_sign using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
  · convert Matrix.det_mul _ _ using 2 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) ; norm_num [ Matrix.fromBlocks_multiply ];
  · rw [ Matrix.det_fromBlocks_zero₂₁ ] ; ring_nf;
    rcases Nat.even_or_odd' r with ⟨ k, rfl | rfl ⟩ <;> ring_nf <;> norm_num

private lemma gramDet_divides_combined_det
    (r : ℕ) (hr : 0 < r)
    (b z w : Fin r → (Fin (2 * r) → ℤ))
    (h_orth : ∀ j k : Fin r, ∑ i, b j i * z k i = 0)
    (h_unimod : let Q : Matrix (Fin (2 * r)) (Fin (2 * r)) ℤ :=
        Matrix.of (fun i j =>
          if h : j.val < r then z ⟨j.val, h⟩ i
          else w ⟨j.val - r, by omega⟩ i)
      Q.det = 1 ∨ Q.det = -1) :
    (Matrix.det (Matrix.of (fun i j : Fin r => ∑ k, z i k * z j k))) ∣
    (Matrix.det (Matrix.of (fun i j : Fin (2 * r) =>
      if h : i.val < r then b ⟨i.val, h⟩ j
      else z ⟨i.val - r, by omega⟩ j))) := by
  obtain ⟨Q, hQ⟩ : ∃ Q : Matrix (Fin (2 * r)) (Fin (2 * r)) ℤ, (∀ i j : Fin (2 * r), Q i j = if h : j.val < r then (z (Fin.mk j.val h)) i else (w (Fin.mk (j.val - r) (by omega))) i) ∧ (Q.det = 1 ∨ Q.det = -1) := by
    exact ⟨ _, fun i j => rfl, h_unimod ⟩;
  set C : Matrix (Fin (2 * r)) (Fin (2 * r)) ℤ := Matrix.of (fun i j => if h : i.val < r then b (Fin.mk i.val h) j else z (Fin.mk (i.val - r) (by omega)) j);
  set BW : Matrix (Fin r) (Fin r) ℤ := Matrix.of (fun i j => ∑ k : Fin (2 * r), b i k * w j k) with hBW
  set ZZ : Matrix (Fin r) (Fin r) ℤ := Matrix.of (fun i j => ∑ k : Fin (2 * r), z i k * z j k) with hZZ
  set ZW : Matrix (Fin r) (Fin r) ℤ := Matrix.of (fun i j => ∑ k : Fin (2 * r), z i k * w j k) with hZW
  let ψf : Fin (2 * r) → Fin r ⊕ Fin r := fun i =>
    if h : i.val < r then Sum.inl ⟨i.val, h⟩ else Sum.inr ⟨i.val - r, by omega⟩
  have hinj : Function.Injective ψf := by
    intro i j hij
    by_cases hi : i.val < r <;> by_cases hj : j.val < r <;> simp [ψf, hi, hj] at hij <;> ext <;> omega
  have hsurj : Function.Surjective ψf := by
    rintro (i | i)
    · exact ⟨⟨i.val, by omega⟩, by simp [ψf]⟩
    · refine ⟨⟨i.val + r, by omega⟩, ?_⟩
      simp [ψf]
  let e : Fin (2 * r) ≃ Fin r ⊕ Fin r := Equiv.ofBijective ψf ⟨hinj, hsurj⟩
  have he_l : ∀ i : Fin r, e.symm (Sum.inl i) = ⟨i.val, by omega⟩ := by
    intro i; rw [Equiv.symm_apply_eq]; show _ = ψf _; simp [ψf]
  have he_r : ∀ i : Fin r, e.symm (Sum.inr i) = ⟨i.val + r, by omega⟩ := by
    intro i; rw [Equiv.symm_apply_eq]; show _ = ψf _; simp [ψf]
  have hC_l : ∀ i k, C (e.symm (Sum.inl i)) k = b i k := by intro i k; rw [he_l]; simp [C]
  have hC_r : ∀ i k, C (e.symm (Sum.inr i)) k = z i k := by intro i k; rw [he_r]; simp [C]
  have hQ_l : ∀ j k, Q k (e.symm (Sum.inl j)) = z j k := by intro j k; rw [he_l, hQ.1]; simp
  have hQ_r : ∀ j k, Q k (e.symm (Sum.inr j)) = w j k := by intro j k; rw [he_r, hQ.1]; simp
  have key : (C * Q).submatrix e.symm e.symm = Matrix.fromBlocks 0 BW ZZ ZW := by
    ext (i | i) (j | j) <;>
      simp [Matrix.mul_apply, hC_l, hC_r, hQ_l, hQ_r, h_orth, hBW, hZZ, hZW]
  have h_det_CQ : (C * Q).det = (-1) ^ (r * r) * BW.det * ZZ.det := by
    rw [← Matrix.det_submatrix_equiv_self e.symm, key, det_block_zero_upper_left]
  have hdet : C.det * Q.det = (-1) ^ (r * r) * BW.det * ZZ.det := by
    rw [← Matrix.det_mul]; exact h_det_CQ
  show ZZ.det ∣ C.det
  rcases hQ.2 with h | h
  · rw [h] at hdet
    exact ⟨(-1) ^ (r * r) * BW.det, by linear_combination hdet⟩
  · rw [h] at hdet
    exact ⟨-((-1) ^ (r * r) * BW.det), by linear_combination -hdet⟩


private lemma annihilator_det_bound
    (r : ℕ) (hr : 1 ≤ r) (s : ℕ) (hs : s = 2 * r)
    (b : Fin r → (Fin s → ℤ))
    (hb_indep : LinearIndependent ℝ (fun j : Fin r => (fun i : Fin s => ((b j i : ℤ) : ℝ)))) :
    ∃ z : Fin r → (Fin s → ℤ),
      (∀ k j : Fin r, ∑ i : Fin s, (z k i : ℝ) * (b j i : ℝ) = 0) ∧
      LinearIndependent ℤ z ∧
      gramDet r s (fun k i => ((z k i : ℤ) : ℝ)) ≤
        gramDet r s (fun j i => ((b j i : ℤ) : ℝ)) := by
  subst hs
  set phi : (Fin (2 * r) → ℤ) →ₗ[ℤ] (Fin r → ℤ) :=
    { toFun := fun x j => ∑ i, b j i * x i,
      map_add' := fun x y => funext fun j => by simp [mul_add, Finset.sum_add_distrib],
      map_smul' := fun c x => funext fun j => by simp [mul_left_comm, Finset.mul_sum] }
  obtain ⟨z, w, hz_ker, hz_indep, h_unimod⟩ := kernel_and_complement_exist r (by omega) phi
  have h_orth_int : ∀ k j : Fin r, ∑ i, b j i * z k i = 0 := by
    intro k j; have := congr_fun (hz_ker k) j; simp [phi] at this; exact this
  have h_orth_bz : ∀ j k : Fin r, ∑ i, (b j i : ℝ) * (z k i : ℝ) = 0 := by
    intro j k; exact_mod_cast h_orth_int k j
  have h_orth_zb : ∀ k j : Fin r, ∑ i, (z k i : ℝ) * (b j i : ℝ) = 0 := by
    intro k j; rw [← h_orth_bz j k]; congr 1; ext; ring
  refine ⟨z, h_orth_zb, hz_indep, ?_⟩
  have h_z_real_indep := int_linearIndependent_implies_real r (2 * r) z hz_indep
  have hgz_ge_one := gramDet_int_ge_one r (2 * r) z hz_indep
  obtain ⟨D, hD_ne, hD_sq⟩ := gramDet_product_is_square r (2 * r) rfl b z h_orth_bz hb_indep h_z_real_indep
  have h_div := gramDet_divides_combined_det r (by omega) b z w (fun j k => h_orth_int k j) h_unimod
  have hD_eq_detC : (Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin (2 * r), (b i k : ℝ) * (b j k : ℝ)))) * (Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin (2 * r), (z i k : ℝ) * (z j k : ℝ)))) = (Matrix.det (Matrix.of (fun i j : Fin (2 * r) => if h : i.val < r then (b ⟨i.val, h⟩ j : ℝ) else (z ⟨i.val - r, by omega⟩ j : ℝ)))) ^ 2 := by
    have h_detC_sq : Matrix.det (Matrix.of (fun i j : Fin (2 * r) => if h : i.val < r then (b ⟨i.val, h⟩ j : ℝ) else (z ⟨i.val - r, by omega⟩ j : ℝ))) ^ 2 = Matrix.det (Matrix.of (fun i j : Fin (2 * r) => ∑ k : Fin (2 * r), (if h : i.val < r then (b ⟨i.val, h⟩ k : ℝ) else (z ⟨i.val - r, by omega⟩ k : ℝ)) * (if h : j.val < r then (b ⟨j.val, h⟩ k : ℝ) else (z ⟨j.val - r, by omega⟩ k : ℝ)))) := by
      have h_detC_sq : Matrix.det (Matrix.of (fun i j : Fin (2 * r) => if h : i.val < r then (b ⟨i.val, h⟩ j : ℝ) else (z ⟨i.val - r, by omega⟩ j : ℝ))) ^ 2 = Matrix.det (Matrix.of (fun i j : Fin (2 * r) => ∑ k : Fin (2 * r), (if h : i.val < r then (b ⟨i.val, h⟩ k : ℝ) else (z ⟨i.val - r, by omega⟩ k : ℝ)) * (if h : j.val < r then (b ⟨j.val, h⟩ k : ℝ) else (z ⟨j.val - r, by omega⟩ k : ℝ)))) := by
        have h_detC_sq : Matrix.of (fun i j : Fin (2 * r) => ∑ k : Fin (2 * r), (if h : i.val < r then (b ⟨i.val, h⟩ k : ℝ) else (z ⟨i.val - r, by omega⟩ k : ℝ)) * (if h : j.val < r then (b ⟨j.val, h⟩ k : ℝ) else (z ⟨j.val - r, by omega⟩ k : ℝ))) = Matrix.of (fun i j : Fin (2 * r) => if h : i.val < r then (b ⟨i.val, h⟩ j : ℝ) else (z ⟨i.val - r, by omega⟩ j : ℝ)) * Matrix.transpose (Matrix.of (fun i j : Fin (2 * r) => if h : i.val < r then (b ⟨i.val, h⟩ j : ℝ) else (z ⟨i.val - r, by omega⟩ j : ℝ))) := by
          ext i j; simp +decide [ Matrix.mul_apply ] ;
        rw [ h_detC_sq, Matrix.det_mul, Matrix.det_transpose, sq ];
      convert h_detC_sq using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    rw [ h_detC_sq ];
    convert gramDet_orthogonal_factorization r ( 2 * r ) rfl ( fun i k => ( b i k : ℝ ) ) ( fun i k => ( z i k : ℝ ) ) h_orth_bz |> Eq.symm using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    congr! 3;
    ext j; split_ifs <;> simp +decide [ * ] ;
  obtain ⟨ k, hk ⟩ := h_div;
  have hD_eq_k_detz : (D : ℝ) ^ 2 = (k : ℝ) ^ 2 * (Matrix.det (Matrix.of (fun i j : Fin r => ∑ k : Fin (2 * r), (z i k : ℝ) * (z j k : ℝ)))) ^ 2 := by
    rw [ ← hD_sq, hD_eq_detC ];
    convert congr_arg ( · ^ 2 ) ( congr_arg ( ( ↑ ) : ℤ → ℝ ) hk ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) ; norm_num [ Matrix.det_apply' ] ; ring_nf;
    · exact congr_arg ( · ^ 2 ) ( Finset.sum_congr rfl fun _ _ => by congr; ext; split_ifs <;> norm_cast );
    · norm_num [ Matrix.det_apply' ] ; ring;
  unfold gramDet at *;
  norm_num [ Matrix.det_apply' ] at *;
  norm_cast at *;
  nlinarith [ show k ^ 2 > 0 by exact sq_pos_of_ne_zero ( show k ≠ 0 by rintro rfl; exact hD_ne <| by nlinarith ) ]

private lemma orthogonal_lattice_short_vectors
    (r : ℕ) (hr : 1 ≤ r) (s : ℕ) (hs : s = 2 * r)
    (b : Fin r → (Fin s → ℤ))
    (hb_indep : LinearIndependent ℝ (fun j : Fin r => (fun i : Fin s => ((b j i : ℤ) : ℝ)))) :
    ∃ y : Fin r → (Fin s → ℤ),
      (∀ k j : Fin r, ∑ i : Fin s, (y k i : ℝ) * (b j i : ℝ) = 0) ∧
      LinearIndependent ℝ (fun k : Fin r => (fun i : Fin s => ((y k i : ℤ) : ℝ))) ∧
      Monotone (fun k : Fin r => ∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2) ∧
      ∏ k : Fin r, (∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2) ≤
        (2 : ℝ) ^ (r * (r - 1)) *
        ∏ j : Fin r, (∑ i : Fin s, ((b j i : ℤ) : ℝ) ^ 2) := by
  have := @annihilator_det_bound r hr s hs b hb_indep;
  obtain ⟨ z, hz₁, hz₂, hz₃ ⟩ := this; have := successive_minima_product_bound_abstract r s hr ( by omega ) z hz₂; simp_all +decide [ Monotone ] ;
  refine' ⟨ this.choose, _, this.choose_spec.2.1, this.choose_spec.2.2.1, this.choose_spec.2.2.2.trans _ ⟩;
  · intro k j
    have h_span : this.choose k ∈ Submodule.span ℤ (Set.range z) := by
      exact this.choose_spec.1 k
    have h_kernel : ∀ v ∈ Submodule.span ℤ (Set.range z), ∀ j, ∑ i, (v i : ℝ) * (b j i : ℝ) = 0 := by
      intro v hv j; induction hv using Submodule.span_induction <;> simp_all +decide [ Finset.sum_add_distrib, add_mul ] ;
      · aesop;
      · simp_all +decide [ mul_assoc, ← Finset.mul_sum _ _ _ ]
    exact h_kernel (this.choose k) h_span j;
  · exact mul_le_mul_of_nonneg_left ( hz₃.trans ( gramDet_le_prod_sq_norms r s _ ) ) ( by positivity )

private lemma weighted_vandermonde_trivial_kernel
    (s : ℕ)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_strict : StrictMono u)
    (hw_pos : ∀ i, 0 < w i)
    (a : Fin s → ℤ)
    (ha : ∀ j : ℕ, j < s → ∑ i, (a i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) :
    a = 0 := by
  have h_vandermonde : Matrix.det (Matrix.of (fun i j : Fin s => (w j : ℝ) * (u j : ℝ) ^ (i : ℕ))) ≠ 0 := by
    have h_vandermonde_det : Matrix.det (Matrix.of (fun i j : Fin s => (u j : ℝ) ^ (i : ℕ))) ≠ 0 := by
      erw [ Matrix.det_transpose, Matrix.det_vandermonde ]
      exact Finset.prod_ne_zero_iff.mpr fun i hi => Finset.prod_ne_zero_iff.mpr fun j hj => sub_ne_zero_of_ne <| mod_cast hu_strict.injective.ne <| ne_of_gt <| Finset.mem_Ioi.mp hj
    convert mul_ne_zero h_vandermonde_det ( show ( ∏ i : Fin s, ( w i : ℝ ) ) ≠ 0 from Finset.prod_ne_zero_iff.mpr fun i _ => Nat.cast_ne_zero.mpr <| ne_of_gt <| hw_pos i ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)))
    simp +decide [ Matrix.det_apply', mul_comm, Finset.prod_mul_distrib ]
    simp +decide only [mul_assoc, Finset.mul_sum _ _ _]
  have h_mulvec : Matrix.mulVec (Matrix.of (fun i j : Fin s => (w j : ℝ) * (u j : ℝ) ^ (i : ℕ))) (fun i => (a i : ℝ)) = 0 := by
    ext i; simp_all +decide [ Matrix.mulVec, dotProduct, mul_comm, mul_left_comm ]
  exact funext fun i => by simpa [ funext_iff ] using Matrix.eq_zero_of_mulVec_eq_zero ‹_› h_mulvec |> fun h => by simpa [ funext_iff ] using congr_fun h i

private lemma excess_zero_among_independent
    (r : ℕ) (hr : 2 ≤ r)
    (s : ℕ) (hs : s = 2 * r)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_strict : StrictMono u)
    (hw_pos : ∀ i, 0 < w i)
    (v : Fin r → (Fin s → ℤ))
    (hv_kernel : ∀ (k : Fin r) (j : ℕ), j < r →
      ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0)
    (hv_indep : LinearIndependent ℝ (fun k : Fin r => (fun i : Fin s => ((v k i : ℤ) : ℝ)))) :
    ∃ m : Fin r, ∑ i, (v m i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0 := by
  by_contra h_contra
  push_neg at h_contra
  have h_all_zero : ∀ k : Fin r, ∑ i, ((v k i) : ℝ) * (w i : ℝ) * ((u i) : ℝ) ^ r = 0 := by
    exact h_contra
  have h_contra : r ≤ r - 1 := by
    have h_contra : Module.finrank ℝ (Submodule.span ℝ (Set.range (fun k : Fin r => fun i : Fin s => (v k i : ℝ)))) ≤ Module.finrank ℝ (LinearMap.ker (Matrix.mulVecLin (Matrix.of (fun (j : Fin (r + 1)) (i : Fin s) => (w i : ℝ) * ((u i) : ℝ) ^ (j : ℕ))))) := by
      refine' Submodule.finrank_mono _;
      rw [ Submodule.span_le ];
      rintro _ ⟨ k, rfl ⟩ ; ext j; simp +decide [ Matrix.mulVec, dotProduct, mul_comm, mul_left_comm] ;
      by_cases hj : j.val < r <;> simp_all +decide [ mul_comm];
      rw [ show ( j : ℕ ) = r by linarith [ Fin.is_lt j ] ] ; exact h_contra k;
    have h_contra : Matrix.rank (Matrix.of (fun (j : Fin (r + 1)) (i : Fin s) => (w i : ℝ) * ((u i) : ℝ) ^ (j : ℕ))) = r + 1 := by
      have h_contra : LinearIndependent ℝ (fun j : Fin (r + 1) => fun i : Fin s => (w i : ℝ) * ((u i) : ℝ) ^ (j : ℕ)) := by
        refine' Fintype.linearIndependent_iff.2 _;
        intro g hg i
        have h_poly : ∀ x : ℝ, ∑ j : Fin (r + 1), g j * x ^ (j : ℕ) = 0 := by
          have h_poly : ∀ x : ℝ, ∑ j : Fin (r + 1), g j * x ^ (j : ℕ) = 0 := by
            intro x
            have h_poly_eq : ∀ i : Fin s, ∑ j : Fin (r + 1), g j * (u i : ℝ) ^ (j : ℕ) = 0 := by
              intro i; replace hg := congr_fun hg i; simp_all +decide [ mul_comm ] ;
              simp_all +decide [ ← mul_assoc, ← Finset.sum_mul _ _ _ ];
              exact hg.resolve_right ( ne_of_gt ( hw_pos i ) )
            have h_poly_eq : ∀ p : Polynomial ℝ, p.degree ≤ r → (∀ i : Fin s, p.eval (u i : ℝ) = 0) → p = 0 := by
              intros p hp h_eval_zero
              have h_card_roots : p.roots.toFinset.card ≤ r := by
                exact le_trans ( Multiset.toFinset_card_le _ ) ( le_trans ( Polynomial.card_roots' _ ) ( Polynomial.natDegree_le_of_degree_le hp ) );
              exact Classical.not_not.1 fun h => by have := Finset.card_le_card ( show Finset.image ( fun i : Fin s => ( u i : ℝ ) ) Finset.univ ⊆ p.roots.toFinset from Finset.image_subset_iff.2 fun i _ => by aesop ) ; rw [ Finset.card_image_of_injective _ fun i j hij => by simpa [ hu_strict.injective.eq_iff ] using hij ] at this ; norm_num at this ; linarith;
            specialize h_poly_eq ( ∑ j : Fin ( r + 1 ), g j • Polynomial.X ^ ( j : ℕ ) ) ; simp_all +decide [ Polynomial.eval_finset_sum ];
            replace h_poly_eq := congr_arg ( Polynomial.eval x ) ( h_poly_eq <| le_trans ( Polynomial.degree_sum_le _ _ ) <| Finset.sup_le fun i _ => Polynomial.degree_smul_le _ _ |> le_trans <| Polynomial.degree_X_pow_le _ |> le_trans <| WithBot.coe_le_coe.mpr <| Nat.le_of_lt_succ <| Fin.is_lt i ) ; simp_all +decide [ Polynomial.eval_finset_sum ] ;
          exact h_poly;
        have h_poly_zero : ∑ j : Fin (r + 1), Polynomial.C (g j) * Polynomial.X ^ (j : ℕ) = 0 := by
          exact Polynomial.funext fun x => by simpa [ Polynomial.eval_finset_sum ] using h_poly x;
        replace h_poly_zero := congr_arg ( fun p => p.coeff ( i : ℕ ) ) h_poly_zero ; simp_all +decide [ Polynomial.coeff_X_pow ] ;
        simp_all +decide [ Fin.val_inj ];
      rw [ ← Matrix.rank_transpose, Matrix.rank ];
      rw [ @LinearMap.finrank_range_of_inj ] <;> norm_num [ Function.Injective ];
      intro a₁ a₂ h; simp_all +decide [ funext_iff, Matrix.vecMul, dotProduct ] ;
      rw [ Fintype.linearIndependent_iff ] at h_contra;
      exact fun i => sub_eq_zero.mp ( h_contra ( fun j => a₁ j - a₂ j ) ( by ext x; simpa [ sub_mul ] using sub_eq_zero.mpr ( h x ) ) i );
    have := LinearMap.finrank_range_add_finrank_ker ( Matrix.mulVecLin ( Matrix.of ( fun ( j : Fin ( r + 1 ) ) ( i : Fin s ) => ( w i : ℝ ) * ( u i : ℝ ) ^ ( j : ℕ ) ) ) ) ; simp_all +decide [ Matrix.rank ] ;
    linarith [ show Module.finrank ℝ ( Submodule.span ℝ ( Set.range fun k i => ( v k i : ℝ ) ) ) = r from by rw [ finrank_span_eq_card ] <;> aesop ]
  linarith [Nat.sub_add_cancel (by linarith : 1 ≤ r)]

private lemma choose_le_pow_div_factorial (n j : ℕ) :
    (Nat.choose n j : ℝ) ≤ (n : ℝ) ^ j / (Nat.factorial j : ℝ) := by
  rw [ le_div_iff₀ ( by positivity ) ];
  rw_mod_cast [ mul_comm, ← Nat.descFactorial_eq_factorial_mul_choose ] ; exact Nat.descFactorial_le_pow n j;

private lemma norm_sq_defining_vector_bound
    (s : ℕ) (M : ℝ) (W : ℝ) (hW : 1 ≤ W)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_range : ∀ i, 0 ≤ u i ∧ (u i : ℝ) ≤ M)
    (hw_bound : ∀ i, (w i : ℝ) ≤ W)
    (j : ℕ) :
    ∑ i : Fin s, ((w i : ℝ) * (Nat.choose (u i).toNat j : ℝ)) ^ 2 ≤
      (s : ℝ) * W ^ 2 * ((M : ℝ) ^ j / (Nat.factorial j : ℝ)) ^ 2 := by
  have h_term_bound : ∀ i : Fin s, ((w i : ℝ) * Nat.choose (u i).toNat j) ^ 2 ≤ (W * (M ^ j / (Nat.factorial j))) ^ 2 := by
    have h_binom_bound : ∀ i : Fin s, (Nat.choose (u i).toNat j : ℝ) ≤ (M ^ j / (Nat.factorial j)) := by
      intro i
      have h_choose_bound : (Nat.choose (u i).toNat j : ℝ) ≤ (u i).toNat ^ j / (Nat.factorial j : ℝ) := by
        convert choose_le_pow_div_factorial ( Int.toNat ( u i ) ) j using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)))
      generalize_proofs at *; (
      exact h_choose_bound.trans ( by gcongr ; linarith [ hu_range i, show ( u i |> Int.toNat : ℝ ) ≤ M from by linarith [ hu_range i, show ( u i |> Int.toNat : ℝ ) = u i from mod_cast Int.toNat_of_nonneg ( hu_range i |>.1 ) ] ] ));
    exact fun i => pow_le_pow_left₀ ( by positivity ) ( mul_le_mul ( hw_bound i ) ( h_binom_bound i ) ( by positivity ) ( by positivity ) ) _;
  convert Finset.sum_le_sum fun i _ => h_term_bound i using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) ; norm_num ; ring

private lemma integer_kernel_has_r_independent_vectors
    (r : ℕ) (hr : 2 ≤ r)
    (s : ℕ) (hs : s = 2 * r)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_strict : StrictMono u)
    (hw_pos : ∀ i, 0 < w i) :
    ∃ v : Fin r → (Fin s → ℤ),
      (∀ (k : Fin r) (j : ℕ), j < r →
        ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧
      LinearIndependent ℝ (fun k : Fin r => (fun i : Fin s => ((v k i : ℤ) : ℝ))) := by
  set B₀ : Matrix (Fin r) (Fin r) ℤ := fun j k => w ⟨r + k.val, by omega⟩ * (u ⟨r + k.val, by omega⟩ : ℤ) ^ j.val;
  obtain ⟨v, hv⟩ : ∃ v : Fin r → Fin s → ℤ, (∀ j₀ : Fin r, ∀ j : ℕ, j < r → ∑ i, (v j₀ i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧ (∀ j₀ j₁ : Fin r, j₀ ≠ j₁ → v j₀ ⟨j₁.val, by omega⟩ = 0) ∧ (∀ j₀ : Fin r, v j₀ ⟨j₀.val, by omega⟩ = B₀.det) := by
    refine' ⟨ fun j₀ i => if h : i.val < r then if h' : i.val = j₀.val then B₀.det else 0 else -Matrix.det ( Matrix.updateCol B₀ ( ⟨ i.val - r, by omega ⟩ : Fin r ) ( fun j => w ⟨ j₀.val, by omega ⟩ * ( u ⟨ j₀.val, by omega ⟩ : ℤ ) ^ j.val ) ), _, _, _ ⟩ <;> simp +decide ;
    · intro j₀ j hj;
      have h_split_sum : ∑ x : Fin s, (if h : x.val < r then if h' : x.val = j₀.val then B₀.det else 0 else -Matrix.det (Matrix.updateCol B₀ (⟨x.val - r, by omega⟩ : Fin r) (fun j => w ⟨j₀.val, by omega⟩ * (u ⟨j₀.val, by omega⟩ : ℤ) ^ j.val))) * (w x : ℝ) * ((u x : ℝ)) ^ j = ∑ x : Fin r, (B₀.det : ℝ) * (w ⟨x.val, by omega⟩ : ℝ) * ((u ⟨x.val, by omega⟩ : ℝ)) ^ j * (if x.val = j₀.val then 1 else 0) + ∑ x : Fin r, (-Matrix.det (Matrix.updateCol B₀ x (fun j => w ⟨j₀.val, by omega⟩ * (u ⟨j₀.val, by omega⟩ : ℤ) ^ j.val))) * (w ⟨r + x.val, by omega⟩ : ℝ) * ((u ⟨r + x.val, by omega⟩ : ℝ)) ^ j := by
        rw [ show ( Finset.univ : Finset ( Fin s ) ) = Finset.image ( fun x : Fin r => ⟨ x.val, by omega ⟩ ) Finset.univ ∪ Finset.image ( fun x : Fin r => ⟨ r + x.val, by omega ⟩ ) Finset.univ from ?_, Finset.sum_union ];
        · rw [ Finset.sum_image, Finset.sum_image ] <;> simp +decide ;
          · exact fun x y h => by simpa [ Fin.ext_iff ] using h;
          · exact fun x y h => Fin.ext <| by simpa using congr_arg Fin.val h;
        · norm_num [ Finset.disjoint_left ];
          exact fun a x => by linarith [ Fin.is_lt a, Fin.is_lt x ] ;
        · ext ⟨ x, hx ⟩ ; simp +decide [ Fin.ext_iff ];
          exact if h : x < r then Or.inl ⟨ ⟨ x, by linarith ⟩, rfl ⟩ else Or.inr ⟨ ⟨ x - r, by omega ⟩, by rw [ add_tsub_cancel_of_le ( by linarith ) ] ⟩;
      have h_det_sum : ∑ x : Fin r, Matrix.det (Matrix.updateCol B₀ x (fun j => w ⟨j₀.val, by omega⟩ * (u ⟨j₀.val, by omega⟩ : ℤ) ^ j.val)) * (w ⟨r + x.val, by omega⟩ : ℝ) * ((u ⟨r + x.val, by omega⟩ : ℝ)) ^ j = Matrix.det B₀ * (w ⟨j₀.val, by omega⟩ : ℝ) * ((u ⟨j₀.val, by omega⟩ : ℝ)) ^ j := by
        have h_det_sum : Matrix.mulVec B₀ (fun x : Fin r => Matrix.det (Matrix.updateCol B₀ x (fun j => w ⟨j₀.val, by omega⟩ * (u ⟨j₀.val, by omega⟩ : ℤ) ^ j.val))) = Matrix.det B₀ • (fun j => w ⟨j₀.val, by omega⟩ * (u ⟨j₀.val, by omega⟩ : ℤ) ^ j.val) := by
          rw [← Matrix.mulVec_cramer]
          first | rfl | (congr 1; funext x; rw [Matrix.cramer_apply]) | (congr 1; funext x) | congr 1
        convert congr_arg ( fun x : Fin r → ℤ => ( x ⟨ j, by linarith ⟩ : ℝ ) ) h_det_sum using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) <;> norm_num [ Matrix.mulVec, dotProduct ] ; ring_nf;
        · exact Finset.sum_congr rfl fun _ _ => by push_cast [ B₀ ] ; ring;
        · ring;
      simp_all +decide [ Fin.val_inj ];
    · exact fun j₀ j₁ hij h => False.elim <| hij <| Fin.ext h.symm;
  have h_det_B₀ : B₀.det ≠ 0 := by
    have h_det_B₀ : Matrix.det B₀ = Matrix.det (Matrix.of (fun j k : Fin r => (u ⟨r + k.val, by omega⟩ : ℤ) ^ j.val)) * ∏ k : Fin r, (w ⟨r + k.val, by omega⟩ : ℤ) := by
      erw [ Matrix.det_mul_row ];
      ring!;
    rw [ h_det_B₀ ];
    erw [ Matrix.det_transpose, Matrix.det_vandermonde ];
    exact mul_ne_zero ( Finset.prod_ne_zero_iff.mpr fun i hi => Finset.prod_ne_zero_iff.mpr fun j hj => sub_ne_zero_of_ne <| hu_strict.injective.ne <| by simpa [ Fin.ext_iff ] using ne_of_gt <| Finset.mem_Ioi.mp hj ) <| Finset.prod_ne_zero_iff.mpr fun i hi => Nat.cast_ne_zero.mpr <| ne_of_gt <| hw_pos _;
  refine' ⟨ v, hv.1, Fintype.linearIndependent_iff.2 _ ⟩;
  intro g hg i; replace hg := congr_fun hg ⟨ i, by linarith [ Fin.is_lt i ] ⟩ ; simp_all +decide [ Finset.sum_eq_single i ] ;

private lemma finite_integer_vectors_bounded_norm (s : ℕ) (C : ℝ) :
    Set.Finite {a : Fin s → ℤ | ∑ i : Fin s, ((a i : ℤ) : ℝ) ^ 2 ≤ C} := by
  have h_finite_components : ∀ (i : Fin s), Set.Finite {a : ℤ | (a : ℝ) ^ 2 ≤ C} := by
    exact fun i => Set.Finite.subset ( Set.finite_Icc ( -⌈C⌉₊ : ℤ ) ⌈C⌉₊ ) fun x hx => ⟨ by exact Int.le_of_lt_add_one ( by rw [ ← @Int.cast_lt ℝ ] ; push_cast; nlinarith [ hx.out, Nat.le_ceil C ] ), by exact Int.le_of_lt_add_one ( by rw [ ← @Int.cast_lt ℝ ] ; push_cast; nlinarith [ hx.out, Nat.le_ceil C ] ) ⟩ ;
  exact Set.Finite.subset ( Set.Finite.pi fun i => h_finite_components i ) fun x hx => by simpa using fun i => hx.trans' ( Finset.single_le_sum ( fun a _ => sq_nonneg ( x a : ℝ ) ) ( Finset.mem_univ i ) ) ;

private noncomputable def int_sq_norm (s : ℕ) (x : Fin s → ℤ) : ℕ := ∑ i : Fin s, (x i).natAbs ^ 2

private lemma int_sq_norm_eq_real_sq_norm (s : ℕ) (x : Fin s → ℤ) :
    (int_sq_norm s x : ℝ) = ∑ i : Fin s, ((x i : ℤ) : ℝ) ^ 2 := by
  unfold int_sq_norm;
  norm_num [ ← @Int.cast_inj ℝ ]

private lemma min_norm_kernel_vector_exists
    (r s : ℕ) (hr : 2 ≤ r) (hs : s = 2 * r)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_strict : StrictMono u) (hw_pos : ∀ i, 0 < w i)
    (V : Submodule ℝ (Fin s → ℝ)) (hV_dim : Module.finrank ℝ V < r) :
    ∃ x : Fin s → ℤ,
      (∀ j : ℕ, j < r → ∑ i, (x i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧
      (fun i : Fin s => (x i : ℝ)) ∉ V ∧
      (∀ y : Fin s → ℤ,
        (∀ j : ℕ, j < r → ∑ i, (y i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) →
        (fun i : Fin s => (y i : ℝ)) ∉ V →
        int_sq_norm s x ≤ int_sq_norm s y) := by
  obtain ⟨x, hx_kernel, hx_not_in_V⟩ : ∃ x : Fin s → ℤ, (∀ j < r, ∑ i, (x i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧ (fun i => (x i : ℝ)) ∉ V := by
    obtain ⟨ v, hv ⟩ := integer_kernel_has_r_independent_vectors r hr s hs u w hu_strict hw_pos;
    contrapose! hV_dim;
    have hV_dim : Module.finrank ℝ (Submodule.span ℝ (Set.range (fun k : Fin r => (fun i => ((v k i : ℤ) : ℝ))))) ≤ Module.finrank ℝ V := by
      exact Submodule.finrank_mono <| Submodule.span_le.mpr <| Set.range_subset_iff.mpr fun k => hV_dim _ <| hv.1 k;
    rw [ finrank_span_eq_card ] at hV_dim <;> aesop;
  have h_finite : Set.Finite {y : Fin s → ℤ | (∀ j < r, ∑ i, (y i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧ (fun i => (y i : ℝ)) ∉ V ∧ int_sq_norm s y ≤ int_sq_norm s x} := by
    have h_finite : Set.Finite {y : Fin s → ℤ | int_sq_norm s y ≤ int_sq_norm s x} := by
      convert finite_integer_vectors_bounded_norm s ( int_sq_norm s x ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
      norm_num [ ← int_sq_norm_eq_real_sq_norm ];
    exact h_finite.subset fun y hy => hy.2.2;
  obtain ⟨y, hy⟩ : ∃ y ∈ {y : Fin s → ℤ | (∀ j < r, ∑ i, (y i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧ (fun i => (y i : ℝ)) ∉ V ∧ int_sq_norm s y ≤ int_sq_norm s x}, ∀ z ∈ {y : Fin s → ℤ | (∀ j < r, ∑ i, (y i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧ (fun i => (y i : ℝ)) ∉ V ∧ int_sq_norm s y ≤ int_sq_norm s x}, int_sq_norm s y ≤ int_sq_norm s z := by
    apply_rules [ Set.exists_min_image ];
    exact ⟨ x, hx_kernel, hx_not_in_V, le_rfl ⟩;
  exact ⟨ y, hy.1.1, hy.1.2.1, fun z hz₁ hz₂ => if hz₃ : int_sq_norm s z ≤ int_sq_norm s x then hy.2 z ⟨ hz₁, hz₂, hz₃ ⟩ else by linarith [ hy.1.2.2 ] ⟩

private lemma finrank_span_image_lt (s r : ℕ) (k : Fin r)
    (f : Fin r → (Fin s → ℝ)) :
    Module.finrank ℝ (Submodule.span ℝ (f '' {j | j.val < k.val})) ≤ k.val := by
  refine' le_trans ( finrank_span_le_card _ ) _ ; norm_num;
  refine' le_trans ( Finset.card_le_card _ ) _;
  exact Finset.image f ( Finset.Iio k );
  · grind;
  · exact Finset.card_image_le.trans ( by simp )

private lemma successive_minima_in_kernel
    (r : ℕ) (hr : 2 ≤ r)
    (s : ℕ) (hs : s = 2 * r)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_strict : StrictMono u) (hw_pos : ∀ i, 0 < w i) :
    ∃ v : Fin r → (Fin s → ℤ),
      (∀ (k : Fin r) (j : ℕ), j < r →
        ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧
      (LinearIndependent ℝ (fun k : Fin r => (fun i : Fin s => ((v k i : ℤ) : ℝ)))) ∧
      (Monotone (fun k : Fin r => ∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2)) ∧
      (∀ k : Fin r, ∀ x : Fin s → ℤ,
        (∀ j : ℕ, j < r → ∑ i, (x i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) →
        (fun i : Fin s => (x i : ℝ)) ∉
          Submodule.span ℝ ((fun j : Fin r => fun i : Fin s => (v j i : ℝ)) ''
            { j | j.val < k.val }) →
        ∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2 ≤ ∑ i : Fin s, ((x i : ℤ) : ℝ) ^ 2) := by
  have := @integer_kernel_has_r_independent_vectors r hr s hs u w hu_strict hw_pos;
  have h_ind : ∀ k : Fin (r + 1), ∃ v : Fin k → (Fin s → ℤ), (∀ j : Fin k, ∀ l < r, ∑ i, (v j i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ l = 0) ∧ LinearIndependent ℝ (fun j : Fin k => (fun i : Fin s => ((v j i : ℤ) : ℝ))) ∧ Monotone (fun j : Fin k => ∑ i, ((v j i : ℤ) : ℝ) ^ 2) ∧ ∀ j : Fin k, ∀ x : Fin s → ℤ, (∀ l < r, ∑ i, (x i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ l = 0) → (fun i : Fin s => (x i : ℝ)) ∉ Submodule.span ℝ (Set.image (fun l : Fin k => (fun i : Fin s => ((v l i : ℤ) : ℝ))) {l | l.val < j.val}) → ∑ i, ((v j i : ℤ) : ℝ) ^ 2 ≤ ∑ i, ((x i : ℤ) : ℝ) ^ 2 := by
    intro k;
    induction' k using Fin.induction with k ih;
    · simp +decide [ Monotone ];
    · obtain ⟨ v, hv₁, hv₂, hv₃, hv₄ ⟩ := ih;
      obtain ⟨ x, hx₁, hx₂, hx₃ ⟩ := min_norm_kernel_vector_exists r s hr hs u w hu_strict hw_pos ( Submodule.span ℝ ( Set.range ( fun j : Fin k.castSucc => fun i : Fin s => ( v j i : ℝ ) ) ) ) ( by
        rw [ finrank_span_eq_card ] <;> norm_num [ hv₂ ] );
      refine' ⟨ Fin.snoc v x, _, _, _, _ ⟩;
      · intro j l hl; refine' Fin.lastCases _ _ j <;> simp +decide [ * ] ;
      · rw [ Fintype.linearIndependent_iff ] at *;
        intro g hg;
        simp +decide [ Fin.sum_univ_castSucc, funext_iff ] at hg ⊢;
        have hg_last : g (Fin.last k) = 0 := by
          contrapose! hx₂;
          rw [ Submodule.mem_span ];
          intro p hp;
          convert p.smul_mem ( - ( g ( Fin.last k ) ) ⁻¹ ) ( p.add_mem ( p.sum_mem fun i _ => p.smul_mem ( g ( Fin.castSucc i ) ) ( hp <| Set.mem_range_self i ) ) ( p.zero_mem ) ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) ; ext i ; simp +decide ;
          rw [ inv_mul_eq_div, neg_div', eq_div_iff hx₂ ] ; linarith [ hg i ];
        intro i; induction i using Fin.lastCases <;> simp +decide [ * ] at *;
        exact hv₂ _ ( by ext; simpa [ Finset.sum_apply, mul_comm ] using hg _ ) _;
      · intro i j hij;
        by_cases hi : i.val < k.val <;> by_cases hj : j.val < k.val <;> simp +decide [ *, Fin.snoc ] at hij ⊢;
        · exact hv₃ (by first | (simp only [Fin.le_def, Fin.coe_castLT] at hij ⊢; omega) | simpa [Fin.le_def] using hij | exact hij)
        · convert hv₄ ( Fin.castLT i hi ) x hx₁ _ using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
          refine' fun h => hx₂ _;
          exact Submodule.span_mono ( Set.image_subset_range _ _ ) h;
        · grind;
      · intro j y hy₁ hy₂;
        by_cases hj : j.val < k.val;
        · convert hv₄ ⟨ j, hj ⟩ y hy₁ _ using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
          · simp +decide [ Fin.snoc, hj ];
            congr!;
          · contrapose! hy₂;
            refine' Submodule.span_le.mpr _ hy₂;
            rintro _ ⟨ l, hl, rfl ⟩;
            exact Submodule.subset_span ⟨ ⟨ l, by
              exact lt_of_lt_of_le l.2 ( Nat.le_succ _ ) ⟩, by
              exact hl, by
              simp +decide [ Fin.snoc ] ⟩;
        · convert hx₃ y hy₁ _ using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
          · simp +decide [ Fin.eq_last_of_not_lt hj, int_sq_norm ];
            norm_cast;
            norm_num [ ← Int.ofNat_le, Int.natAbs_pow ];
          · contrapose! hy₂;
            refine' Submodule.span_le.mpr _ hy₂;
            rintro _ ⟨ j, rfl ⟩;
            refine' Submodule.subset_span ⟨ Fin.castSucc j, _, _ ⟩ <;> simp +decide [ Fin.snoc ];
            exact lt_of_lt_of_le ( Fin.castSucc_lt_last j ) ( Nat.le_of_not_lt hj );
  exact h_ind ⟨ r, Nat.lt_succ_self r ⟩

private lemma succ_min_product_le_basis_product
    (r s : ℕ)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (v : Fin r → (Fin s → ℤ))
    (hv_succ : ∀ k : Fin r, ∀ x : Fin s → ℤ,
      (∀ j : ℕ, j < r → ∑ i, (x i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) →
      (fun i : Fin s => (x i : ℝ)) ∉
        Submodule.span ℝ ((fun j : Fin r => fun i : Fin s => (v j i : ℝ)) ''
          { j | j.val < k.val }) →
      ∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2 ≤ ∑ i : Fin s, ((x i : ℤ) : ℝ) ^ 2)
    (y : Fin r → (Fin s → ℤ))
    (hy_kernel : ∀ (k : Fin r) (j : ℕ), j < r →
      ∑ i, (y k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0)
    (hy_indep : LinearIndependent ℝ (fun k : Fin r => (fun i : Fin s => ((y k i : ℤ) : ℝ))))
    (hy_sorted : Monotone (fun k : Fin r => ∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2)) :
    ∏ k : Fin r, (∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2) ≤
      ∏ k : Fin r, (∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2) := by
  apply Finset.prod_le_prod;
  · exact fun _ _ => Finset.sum_nonneg fun _ _ => sq_nonneg _;
  · intro k hk
    obtain ⟨j, hj⟩ : ∃ j ≤ k, (fun i => (y j i : ℝ)) ∉ Submodule.span ℝ (Set.image (fun l : Fin r => (fun i => ((v l i : ℝ))) ) {l | l.val < k.val}) := by
      by_contra h_contra;
      have h_subspace : Module.finrank ℝ (Submodule.span ℝ (Set.image (fun l : Fin r => (fun i => ((y l i : ℝ))) ) (Finset.Iic k))) ≤ k.val := by
        have h_subspace : Submodule.span ℝ (Set.image (fun l : Fin r => (fun i => ((y l i : ℝ))) ) (Finset.Iic k)) ≤ Submodule.span ℝ (Set.image (fun l : Fin r => (fun i => ((v l i : ℝ))) ) {l | l.val < k.val}) := by
          exact Submodule.span_le.mpr ( Set.image_subset_iff.mpr fun l hl => by aesop );
        refine' le_trans ( Submodule.finrank_mono h_subspace ) _;
        convert finrank_span_image_lt s r k ( fun l i => ( v l i : ℝ ) ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
      rw [ Set.image_eq_range ] at h_subspace;
      rw [ finrank_span_eq_card ] at h_subspace <;> norm_num at *;
      first
        | exact hy_indep.comp _ Subtype.coe_injective
        | (convert hy_indep.comp _ Subtype.coe_injective using 1)
        | (convert hy_indep.comp _ Subtype.coe_injective)
    exact le_trans ( hv_succ k ( y j ) ( hy_kernel j ) hj.2 ) ( hy_sorted hj.1 )

private lemma annihilator_short_vectors
    (r : ℕ) (hr : 2 ≤ r)
    (s : ℕ) (hs : s = 2 * r)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_nonneg : ∀ i, 0 ≤ u i)
    (hu_strict : StrictMono u)
    (hw_pos : ∀ i, 0 < w i) :
    ∃ y : Fin r → (Fin s → ℤ),
      (∀ (k : Fin r) (j : ℕ), j < r →
        ∑ i, (y k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧
      (LinearIndependent ℝ (fun k : Fin r => (fun i : Fin s => ((y k i : ℤ) : ℝ)))) ∧
      (Monotone (fun k : Fin r => ∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2)) ∧
      ∏ k : Fin r, (∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2) ≤
        (2 : ℝ) ^ (r * (r - 1)) *
        ∏ j ∈ Finset.range r,
          (∑ i : Fin s, ((w i : ℝ) * (Nat.choose (u i).toNat j : ℝ)) ^ 2) := by
  obtain ⟨y, hy⟩ := orthogonal_lattice_short_vectors r (by linarith) s (by
  omega) (fun j => fun i => ((w i : ℤ) * (Nat.choose (u i).toNat j : ℤ))) (by
  refine' Fintype.linearIndependent_iff.2 _;
  intro g hg i
  have h_poly : ∀ i_1 : Fin s, ∑ j : Fin r, g j * (Nat.choose (u i_1).toNat j : ℝ) = 0 := by
    intro i_1; replace hg := congr_fun hg i_1; simp_all +decide [ mul_comm] ;
    convert congr_arg ( fun x : ℝ => x / ( w i_1 : ℝ ) ) hg using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) <;> norm_num [ Finset.sum_div _ _ _, mul_div_assoc, ne_of_gt ( hw_pos i_1 ) ];
  have h_poly_roots : ∀ x : ℕ, x ∈ Finset.image (fun i => (u i).toNat) Finset.univ → ∑ j : Fin r, g j * (Nat.choose x j : ℝ) = 0 := by
    aesop;
  have h_poly_zero : ∀ x : ℕ, ∑ j : Fin r, g j * (Nat.choose x j : ℝ) = 0 := by
    intro x
    by_contra h_nonzero_poly
    have h_poly_roots_card : Finset.card (Finset.image (fun i => (u i).toNat) Finset.univ) ≥ r := by
      rw [ Finset.card_image_of_injective _ fun i j hij => _ ] <;> norm_num [ Fin.ext_iff, hu_strict.injective.eq_iff ] at * ; linarith;
      exact fun i j hij => by simpa [ Fin.ext_iff ] using hu_strict.injective ( by linarith [ Int.toNat_of_nonneg ( hu_nonneg i ), Int.toNat_of_nonneg ( hu_nonneg j ) ] : u i = u j ) ;
    have h_poly_roots_card : Finset.card (Finset.filter (fun x => ∑ j : Fin r, g j * (Nat.choose x j : ℝ) = 0) (Finset.range (Finset.sup (Finset.image (fun i => (u i).toNat) Finset.univ) id + 1))) ≥ r := by
      refine' le_trans h_poly_roots_card ( Finset.card_le_card _ );
      exact fun x hx => Finset.mem_filter.mpr ⟨ Finset.mem_range.mpr ( Nat.lt_succ_of_le ( Finset.le_sup ( f := id ) hx ) ), h_poly_roots x hx ⟩
    have h_poly_roots_card : Finset.card (Finset.filter (fun x => ∑ j : Fin r, g j * (Nat.choose x j : ℝ) = 0) (Finset.range (Finset.sup (Finset.image (fun i => (u i).toNat) Finset.univ) id + 1))) < r := by
      have h_poly_roots_card : ∃ p : Polynomial ℝ, p.degree < r ∧ ∀ x : ℕ, ∑ j : Fin r, g j * (Nat.choose x j : ℝ) = p.eval (x : ℝ) := by
        use ∑ j : Fin r, Polynomial.C (g j) * (Polynomial.C (1 / (Nat.factorial j : ℝ)) * ∏ k ∈ Finset.range j, (Polynomial.X - Polynomial.C (k : ℝ)));
        refine' ⟨ lt_of_le_of_lt ( Polynomial.degree_sum_le _ _ ) _, _ ⟩;
        · erw [ Finset.sup_lt_iff ] ; norm_num [ Polynomial.degree_prod ];
          · intro j; by_cases hj : g j = 0 <;> simp +decide [ hj, Polynomial.degree_C ] ;
            exact lt_of_le_of_lt ( add_le_add ( Polynomial.degree_C_le ) ( Finset.sum_le_sum fun _ _ => Polynomial.degree_X_sub_C_le _ ) ) ( by norm_cast; simp );
          · exact WithBot.bot_lt_coe r;
        · intro x; simp +decide [ Polynomial.eval_finset_sum, Polynomial.eval_mul, Polynomial.eval_prod, Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_C ] ;
          refine' Finset.sum_congr rfl fun j hj => _;
          by_cases hx : x < j.val <;> simp_all +decide [ Nat.choose_eq_zero_of_lt ];
          · exact Or.inr <| Or.inr <| Finset.prod_eq_zero ( Finset.mem_range.mpr hx ) <| sub_self _;
          · field_simp;
            rw_mod_cast [ mul_comm, ← Nat.descFactorial_eq_factorial_mul_choose ];
            rw [ Nat.descFactorial_eq_prod_range ] ; norm_num [ Int.subNatNat_eq_coe ];
            exact Or.inl ( Finset.prod_congr rfl fun i hi => by rw [ Nat.cast_sub ( by linarith [ Finset.mem_range.mp hi ] ) ] );
      obtain ⟨ p, hp_deg, hp_eval ⟩ := h_poly_roots_card; simp_all +decide [ Polynomial.eval_eq_sum_range ] ;
      have h_poly_roots_card : Finset.card (Finset.filter (fun x : ℕ => p.eval (x : ℝ) = 0) (Finset.range (Finset.sup (Finset.image (fun i => (u i).toNat) Finset.univ) id + 1))) ≤ p.natDegree := by
        have h_poly_roots_card : Finset.card (Finset.image (fun x : ℕ => (x : ℝ)) (Finset.filter (fun x : ℕ => p.eval (x : ℝ) = 0) (Finset.range (Finset.sup (Finset.image (fun i => (u i).toNat) Finset.univ) id + 1)))) ≤ p.natDegree := by
          exact le_trans ( Finset.card_le_card <| show _ ⊆ p.roots.toFinset from by aesop_cat ) <| by exact le_trans ( Multiset.toFinset_card_le _ ) <| Polynomial.card_roots' _;
        rwa [ Finset.card_image_of_injective _ fun x y hxy => by simpa using hxy ] at h_poly_roots_card;
      simp_all +decide [ Polynomial.eval_eq_sum_range ];
      exact lt_of_le_of_lt h_poly_roots_card ( Nat.lt_of_not_ge fun h => hp_deg.not_ge <| by rw [ Polynomial.degree_eq_natDegree <| by aesop_cat ] ; exact_mod_cast h )
    exact absurd h_poly_roots_card (by linarith);
  induction' i with i ih;
  induction' i using Nat.strong_induction_on with i ih;
  have := h_poly_zero i;
  rw [ Finset.sum_eq_single ⟨ i, ih ⟩ ] at this <;> simp_all +decide ;
  intro j hj; cases lt_or_gt_of_ne ( show j.val ≠ i from by simpa [ Fin.ext_iff ] using hj ) <;> [ exact Or.inl ( ih _ ‹_› <| by linarith [ Fin.is_lt j ] ) ; exact Or.inr <| Nat.choose_eq_zero_of_lt ‹_› ] ;);
  refine' ⟨ y, _, hy.2.1, hy.2.2.1, _ ⟩ <;> simp_all +decide [ Finset.prod_range ];
  have h_poly : ∀ j : ℕ, j < r → ∃ c : Fin (j + 1) → ℤ, ∀ i : Fin s, (u i : ℝ) ^ j = ∑ l : Fin (j + 1), (c l : ℝ) * (Nat.choose (u i).toNat l : ℝ) := by
    intro j hj;
    have h_poly : ∀ j : ℕ, ∃ c : Fin (j + 1) → ℤ, ∀ x : ℕ, x ^ j = ∑ l : Fin (j + 1), (c l : ℤ) * Nat.choose x l := by
      intro j;
      induction' j with j ih;
      · exact ⟨ fun l => if l = 0 then 1 else 0, fun x => by simp +decide ⟩;
      · obtain ⟨ c, hc ⟩ := ih;
        have h_expand : ∀ x : ℕ, (x : ℤ) ^ (j + 1) = ∑ l : Fin (j + 1), (c l : ℤ) * (x * Nat.choose x l : ℤ) := by
          simp +decide [ pow_succ', mul_left_comm, Finset.mul_sum _ _ _, hc ];
        have h_identity : ∀ x : ℕ, ∀ l : Fin (j + 1), (x * Nat.choose x l : ℤ) = (l.val + 1) * Nat.choose x (l.val + 1) + l.val * Nat.choose x l := by
          intro x l; norm_cast;
          nlinarith [ Nat.add_one_mul_choose_eq x l, Nat.choose_succ_succ x l ];
        use fun l => ∑ k : Fin (j + 1), c k * (if l.val = k.val + 1 then (k.val + 1 : ℤ) else if l.val = k.val then (k.val : ℤ) else 0);
        intro x; rw [ h_expand x ] ; simp +decide [ h_identity, Finset.sum_mul _ _ _ ] ;
        rw [ Finset.sum_comm ];
        refine' Finset.sum_congr rfl fun i hi => _;
        rw [ Finset.sum_eq_add ( ⟨ i + 1, by linarith [ Fin.is_lt i ] ⟩ : Fin ( j + 2 ) ) ( ⟨ i, by linarith [ Fin.is_lt i ] ⟩ : Fin ( j + 2 ) ) ] <;> norm_num ; ring;
        simp +contextual [ Fin.ext_iff ];
    obtain ⟨ c, hc ⟩ := h_poly j; use c; intro i; specialize hc ( Int.toNat ( u i ) ) ; simp_all +decide [ Int.toNat_of_nonneg ( hu_nonneg i ) ] ;
    exact_mod_cast hc;
  intro k j hj; obtain ⟨ c, hc ⟩ := h_poly j hj; simp +decide [ hc, mul_assoc, mul_left_comm, Finset.mul_sum _ _ _ ] ;
  rw [ Finset.sum_comm ];
  refine' Finset.sum_eq_zero fun l hl => _;
  convert congr_arg ( fun x : ℝ => x * c l ) ( hy.1 k ⟨ l, by linarith [ Fin.is_lt l ] ⟩ ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) <;> ring_nf;
  simp +decide only [mul_assoc, Finset.mul_sum _ _ _, mul_left_comm]

private lemma kernel_basis_product_bound
    (r : ℕ) (hr : 2 ≤ r)
    (s : ℕ) (hs : s = 2 * r)
    (M : ℝ)
    (W : ℝ) (hW : 1 ≤ W)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_range : ∀ i, 0 ≤ u i ∧ (u i : ℝ) ≤ M)
    (hu_strict : StrictMono u)
    (hw_pos : ∀ i, 0 < w i)
    (hw_bound : ∀ i, (w i : ℝ) ≤ W) :
    ∃ y : Fin r → (Fin s → ℤ),
      (∀ (k : Fin r) (j : ℕ), j < r →
        ∑ i, (y k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧
      (LinearIndependent ℝ (fun k : Fin r => (fun i : Fin s => ((y k i : ℤ) : ℝ)))) ∧
      (Monotone (fun k : Fin r => ∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2)) ∧
      ∏ k : Fin r, (∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2) ≤
        (2 : ℝ) ^ (r * (r - 1)) * (2 * (r : ℝ)) ^ r * W ^ (2 * r) *
        (∏ j ∈ Finset.range r, ((M : ℝ) ^ j / (Nat.factorial j : ℝ))) ^ 2 := by
  obtain ⟨y, hy_kernel, hy_indep, hy_mono, hy_prod⟩ :=
    annihilator_short_vectors r hr s hs u w (fun i => (hu_range i).1) hu_strict hw_pos
  refine ⟨y, hy_kernel, hy_indep, hy_mono, ?_⟩
  calc ∏ k : Fin r, (∑ i : Fin s, ((y k i : ℤ) : ℝ) ^ 2)
      ≤ (2 : ℝ) ^ (r * (r - 1)) *
        ∏ j ∈ Finset.range r,
          (∑ i : Fin s, ((w i : ℝ) * (Nat.choose (u i).toNat j : ℝ)) ^ 2) := hy_prod
    _ ≤ (2 : ℝ) ^ (r * (r - 1)) *
        ∏ j ∈ Finset.range r,
          ((s : ℝ) * W ^ 2 * ((M : ℝ) ^ j / (Nat.factorial j : ℝ)) ^ 2) := by
        gcongr with j hj
        exact norm_sq_defining_vector_bound s M W hW u w hu_range hw_bound j
    _ = (2 : ℝ) ^ (r * (r - 1)) * (2 * (r : ℝ)) ^ r * W ^ (2 * r) *
        (∏ j ∈ Finset.range r, ((M : ℝ) ^ j / (Nat.factorial j : ℝ))) ^ 2 := by
        rw [Finset.prod_mul_distrib, Finset.prod_mul_distrib]
        simp only [Finset.prod_const, Finset.card_range, Finset.prod_pow]
        rw [hs]; push_cast; ring

private lemma successive_minima_product_bound
    (r : ℕ) (hr : 2 ≤ r)
    (s : ℕ) (hs : s = 2 * r)
    (M : ℝ)
    (W : ℝ) (hW : 1 ≤ W)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_range : ∀ i, 0 ≤ u i ∧ (u i : ℝ) ≤ M)
    (hu_strict : StrictMono u)
    (hw_pos : ∀ i, 0 < w i)
    (hw_bound : ∀ i, (w i : ℝ) ≤ W)
    (v : Fin r → (Fin s → ℤ))
    (hv_succ : ∀ k : Fin r, ∀ x : Fin s → ℤ,
      (∀ j : ℕ, j < r → ∑ i, (x i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) →
      (fun i : Fin s => (x i : ℝ)) ∉
        Submodule.span ℝ ((fun j : Fin r => fun i : Fin s => (v j i : ℝ)) ''
          { j | j.val < k.val }) →
      ∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2 ≤ ∑ i : Fin s, ((x i : ℤ) : ℝ) ^ 2) :
    ∏ k : Fin r, (∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2) ≤
      (2 : ℝ) ^ (r * (r - 1)) * (2 * (r : ℝ)) ^ r * W ^ (2 * r) *
      (∏ j ∈ Finset.range r, ((M : ℝ) ^ j / (Nat.factorial j : ℝ))) ^ 2 := by
  obtain ⟨y, hy_kernel, hy_indep, hy_sorted, hy_prod⟩ := kernel_basis_product_bound r hr s hs M W hW u w hu_range hu_strict hw_pos hw_bound;
  refine le_trans ?_ hy_prod;
  convert succ_min_product_le_basis_product r s u w v hv_succ y hy_kernel hy_indep hy_sorted using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)))

private lemma successive_kernel_vectors_exist
    (r : ℕ) (hr : 2 ≤ r)
    (s : ℕ) (hs : s = 2 * r)
    (M : ℝ)
    (W : ℝ) (hW : 1 ≤ W)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_range : ∀ i, 0 ≤ u i ∧ (u i : ℝ) ≤ M)
    (hu_strict : StrictMono u)
    (hw_pos : ∀ i, 0 < w i)
    (hw_bound : ∀ i, (w i : ℝ) ≤ W) :
    ∃ v : Fin r → (Fin s → ℤ),
      (∀ (k : Fin r) (j : ℕ), j < r →
        ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧
      (LinearIndependent ℝ (fun k : Fin r => (fun i : Fin s => ((v k i : ℤ) : ℝ)))) ∧
      (Monotone (fun k : Fin r => ∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2)) ∧
      (∏ k : Fin r, (∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2) ≤
        (2 : ℝ) ^ (r * (r - 1)) * (2 * (r : ℝ)) ^ r * W ^ (2 * r) *
        (∏ j ∈ Finset.range r, ((M : ℝ) ^ j / (Nat.factorial j : ℝ))) ^ 2) ∧
      (∀ k : Fin r, ∀ x : Fin s → ℤ,
        (∀ j : ℕ, j < r → ∑ i, (x i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) →
        (fun i : Fin s => (x i : ℝ)) ∉
          Submodule.span ℝ ((fun j : Fin r => fun i : Fin s => (v j i : ℝ)) ''
            { j | j.val < k.val }) →
        ∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2 ≤ ∑ i : Fin s, ((x i : ℤ) : ℝ) ^ 2) := by
  obtain ⟨ v, hv₁, hv₂, hv₃, hv₄ ⟩ := successive_minima_in_kernel r hr s hs u w hu_strict hw_pos;
  refine' ⟨ v, hv₁, hv₂, hv₃, _, hv₄ ⟩;
  convert successive_minima_product_bound r hr s hs M W hW u w hu_range hu_strict hw_pos hw_bound v hv₄ using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)))

private lemma kernel_binomial_multiply
    (s : ℕ) (u : Fin s → ℤ) (w : Fin s → ℕ) (v : Fin s → ℤ)
    (hu_nonneg : ∀ i, 0 ≤ u i) (ℓ : ℕ) :
    ∀ n : ℕ, (∀ t : ℕ, t < n + ℓ → ∑ i, (v i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ t = 0) →
    ∀ j : ℕ, j < n →
      ∑ i, ((Nat.choose (u i).toNat ℓ : ℤ) * v i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0 := by
  intro n hn j hj
  induction' ℓ with ℓ ih generalizing n j;
  · aesop;
  · -- Use the identity: (ℓ+1) * choose(n, ℓ+1) = choose(n, ℓ) * (n - ℓ) for natural numbers.
    have h_identity : ∀ i, ((u i).toNat.choose (ℓ + 1) : ℝ) * (ℓ + 1) = ((u i).toNat.choose ℓ : ℝ) * ((u i : ℝ) - ℓ) := by
      intro i; norm_cast; have := Nat.choose_succ_right_eq ( Int.toNat ( u i ) ) ℓ; simp_all +decide [add_comm] ;
      by_cases h : ℓ ≤ Int.toNat ( u i ) <;> simp_all +decide [ Nat.choose_eq_zero_of_lt ];
    have h_sum_rewrite : ∑ i, ((u i).toNat.choose (ℓ + 1) : ℝ) * (v i : ℝ) * (w i : ℝ) * (u i : ℝ) ^ j * (ℓ + 1) = ∑ i, ((u i).toNat.choose ℓ : ℝ) * (v i : ℝ) * (w i : ℝ) * (u i : ℝ) ^ (j + 1) - ℓ * ∑ i, ((u i).toNat.choose ℓ : ℝ) * (v i : ℝ) * (w i : ℝ) * (u i : ℝ) ^ j := by
      rw [ Finset.mul_sum _ _ _ ] ; rw [ ← Finset.sum_sub_distrib ] ; congr ; ext i ; linear_combination' h_identity i * v i * w i * u i ^ j;
    simp_all +decide [ ← Finset.sum_mul _ _ _ ];
    exact eq_zero_of_ne_zero_of_mul_right_eq_zero ( by positivity ) ( h_sum_rewrite.trans ( by rw [ ih ( n + 1 ) ( fun t ht => hn t ( by linarith ) ) ( j + 1 ) ( by linarith ), ih n ( fun t ht => hn t ( by linarith ) ) j hj ] ; ring ) )

private lemma binomial_multiply_norm_bound
    (s : ℕ) (M : ℝ) (u : Fin s → ℤ) (v : Fin s → ℤ) (ℓ : ℕ)
    (hu_range : ∀ i, 0 ≤ u i ∧ (u i : ℝ) ≤ M) :
    ∑ i : Fin s, ((Nat.choose (u i).toNat ℓ : ℤ) * v i : ℝ) ^ 2 ≤
      (M ^ ℓ / (Nat.factorial ℓ : ℝ)) ^ 2 * ∑ i : Fin s, ((v i : ℤ) : ℝ) ^ 2 := by
  have h_binom_bound : ∀ i, ((Nat.choose (u i).toNat ℓ) : ℝ) ≤ (M ^ ℓ / (Nat.factorial ℓ)) := by
    intro i
    have h_choose_bound : (Nat.choose (u i).toNat ℓ : ℝ) ≤ (↑(u i).toNat) ^ ℓ / (Nat.factorial ℓ) := by
      convert choose_le_pow_div_factorial ( Int.toNat ( u i ) ) ℓ using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    refine le_trans h_choose_bound ?_;
    gcongr;
    exact le_trans ( mod_cast Int.toNat_of_nonneg ( hu_range i |>.1 ) |> le_of_eq ) ( hu_range i |>.2 );
  rw [ Finset.mul_sum _ _ _ ] ; exact Finset.sum_le_sum fun i _ => by simpa [ mul_pow ] using mul_le_mul_of_nonneg_right ( pow_le_pow_left₀ ( Nat.cast_nonneg _ ) ( h_binom_bound i ) 2 ) ( sq_nonneg _ ) ;

private lemma pow_div_factorial_mono {M : ℝ} (hM : 0 ≤ M) {j k : ℕ}
    (hjk : j ≤ k) (hkM : (k : ℝ) ≤ M) :
    M ^ j / (Nat.factorial j : ℝ) ≤ M ^ k / (Nat.factorial k : ℝ) := by
  induction hjk <;> simp_all +decide [ Nat.factorial_succ, pow_succ ];
  rename_i k hk ih;
  exact le_trans ( ih ( by linarith ) ) ( by rw [ div_le_div_iff₀ ] <;> first | positivity | nlinarith [ pow_nonneg hM k, show ( k.factorial : ℝ ) > 0 by positivity, mul_le_mul_of_nonneg_right hkM ( show ( 0 : ℝ ) ≤ M ^ k by positivity ) ] )

private lemma kernel_high_excess_count
    (r s e : ℕ) (hs : s = 2 * r) (he : e ≤ r)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_strict : StrictMono u) (hw_pos : ∀ i, 0 < w i)
    (t : ℕ) (v : Fin t → (Fin s → ℤ))
    (hv : ∀ (k : Fin t) (j : ℕ), j < r + e →
      ∑ i, (v k i : ℝ) * (w i : ℝ) * (u i : ℝ) ^ j = 0)
    (hv_indep : LinearIndependent ℝ (fun k : Fin t => fun i : Fin s => (v k i : ℝ))) :
    t ≤ r - e := by
  have h_rank : Matrix.rank (Matrix.of (fun (j : Fin (r + e)) (i : Fin s) => (w i : ℝ) * ((u i : ℝ)) ^ j.val)) = r + e := by
    have h_vandermonde_indep : LinearIndependent ℝ (fun j : Fin (r + e) => fun i : Fin s => (w i : ℝ) * ((u i : ℝ)) ^ j.val) := by
      refine' Fintype.linearIndependent_iff.2 _;
      intro g hg i
      have h_poly : ∀ i_1 : Fin s, ∑ j : Fin (r + e), g j * ((u i_1 : ℝ)) ^ (j : ℕ) = 0 := by
        intro i_1; replace hg := congr_fun hg i_1; simp_all +decide ;
        convert congr_arg ( fun x : ℝ => x / ( w i_1 : ℝ ) ) hg using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) <;> norm_num [ Finset.sum_div _ _ _, mul_assoc, mul_comm, mul_left_comm, ne_of_gt ( hw_pos i_1 ) ];
        exact Finset.sum_congr rfl fun _ _ => by rw [ mul_div_assoc, mul_div_cancel_right₀ _ ( Nat.cast_ne_zero.mpr <| ne_of_gt <| hw_pos i_1 ) ] ;
      have h_poly_zero : ∑ j : Fin (r + e), g j • (Polynomial.monomial j.val (1 : ℝ)) = 0 := by
        refine' Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq _ _ _;
        exact Finset.image ( fun i : Fin s => ( u i : ℝ ) ) Finset.univ;
        · rw [ Finset.card_image_of_injective _ fun i j hij => hu_strict.injective <| by simpa using hij ] ; norm_num [ Polynomial.degree_lt_iff_coeff_zero ];
          simp +decide [ Polynomial.coeff_monomial ];
          exact fun m hm => Finset.sum_eq_zero fun i hi => if_neg <| by linarith [ Fin.is_lt i ] ;
        · simp_all +decide [ Polynomial.eval_finset_sum ];
      replace h_poly_zero := congr_arg ( fun p => p.coeff i ) h_poly_zero ; simp_all +decide [ Polynomial.coeff_monomial ];
      simp_all +decide [ Fin.val_inj ];
    rw [Matrix.rank_eq_finrank_span_row]
    exact (finrank_span_eq_card h_vandermonde_indep).trans (Fintype.card_fin _)
  have h_ker_dim : Module.finrank ℝ (LinearMap.ker (Matrix.mulVecLin (Matrix.of (fun (j : Fin (r + e)) (i : Fin s) => (w i : ℝ) * ((u i : ℝ)) ^ j.val)))) = s - (r + e) := by
    have := LinearMap.finrank_range_add_finrank_ker ( Matrix.mulVecLin ( Matrix.of ( fun ( j : Fin ( r + e ) ) ( i : Fin s ) => ( w i : ℝ ) * ( u i : ℝ ) ^ j.val ) ) );
    have hr' : Module.finrank ℝ (LinearMap.range (Matrix.mulVecLin (Matrix.of (fun (j : Fin (r + e)) (i : Fin s) => (w i : ℝ) * ((u i : ℝ)) ^ j.val)))) = r + e := h_rank
    rw [hr', Module.finrank_fin_fun] at this
    omega
  have h_span_ker : Submodule.span ℝ (Set.range (fun k : Fin t => (fun i : Fin s => ((v k i : ℤ) : ℝ)))) ≤ LinearMap.ker (Matrix.mulVecLin (Matrix.of (fun (j : Fin (r + e)) (i : Fin s) => (w i : ℝ) * ((u i : ℝ)) ^ j.val))) := by
    rw [ Submodule.span_le ];
    rintro _ ⟨ k, rfl ⟩ ; ext j; simp +decide [ Matrix.mulVec, dotProduct, mul_comm, mul_left_comm ] ;
    simpa only [ mul_assoc, mul_comm, mul_left_comm ] using hv k j ( Fin.is_lt j );
  have := Submodule.finrank_mono h_span_ker;
  rw [ finrank_span_eq_card ] at this <;> norm_num [ hv_indep ] at * ; omega

private lemma binomial_multiply_moment
    (s : ℕ) (u : Fin s → ℤ) (w : Fin s → ℕ) (v : Fin s → ℤ)
    (hu_nonneg : ∀ i, 0 ≤ u i) (e : ℕ) :
    ∀ r : ℕ,
    (∀ t : ℕ, t < r + e → ∑ i, (v i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ t = 0) →
    (∑ i, (v i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ (r + e) ≠ 0) →
    ∑ i, ((Nat.choose (u i).toNat e : ℤ) * v i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0 := by
  induction' e with e ih;
  · aesop;
  · intro r hr₁ hr₂;
    have h_identity : ∑ i, (Nat.choose (u i).toNat (e + 1) * v i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r = (1 / (e + 1 : ℝ)) * (∑ i, (Nat.choose (u i).toNat e * v i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ (r + 1)) - (e / (e + 1 : ℝ)) * (∑ i, (Nat.choose (u i).toNat e * v i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r) := by
      have h_identity : ∀ i, (Nat.choose (u i).toNat (e + 1) : ℝ) = (Nat.choose (u i).toNat e : ℝ) * ((u i : ℝ) - e) / (e + 1) := by
        intro i; rw [ eq_div_iff ] <;> norm_cast ;
        cases h : u i <;> simp_all +decide [ Nat.choose_succ_right_eq ];
        · exact Classical.or_iff_not_imp_right.2 fun h' => by rw [ Nat.cast_sub ( le_of_not_gt fun h'' => h' <| Nat.choose_eq_zero_of_lt h'' ) ] ;
        · linarith [ hu_nonneg i, Int.negSucc_lt_zero ‹_› ];
      rw [ Finset.mul_sum _ _ _, Finset.mul_sum _ _ _ ] ; rw [ ← Finset.sum_sub_distrib ] ; congr ; ext i ; rw [ h_identity i ] ; ring;
    have h_ind : ∑ i, (Nat.choose (u i).toNat e * v i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ (r + 1) ≠ 0 := by
      apply ih (r + 1);
      · exact fun t ht => hr₁ t ( by linarith );
      · convert hr₂ using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) ; ring_nf;
    have h_ind : ∑ i, (Nat.choose (u i).toNat e * v i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r = 0 := by
      convert kernel_binomial_multiply s u w v hu_nonneg e ( r + 1 ) ( fun t ht => hr₁ t ( by linarith ) ) r ( by linarith ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    simp_all +decide [ Nat.cast_add_one_ne_zero ]

private lemma excess_product_bound
    (r : ℕ) (hr : 2 ≤ r)
    (m : ℕ) (hm : m ≤ r)
    (M : ℝ) (hM : 0 ≤ M) (hrM : (r : ℝ) - 1 ≤ M)
    (e : Fin m → ℕ)
    (he_pos : ∀ k, 1 ≤ e k)
    (he_bound : ∀ k, e k ≤ r - 1)
    (he_dim : ∀ e₀ : ℕ, 1 ≤ e₀ →
      (Finset.univ.filter (fun k : Fin m => e₀ ≤ e k)).card ≤ r - e₀) :
    ∏ k : Fin m, (M ^ (e k) / (Nat.factorial (e k) : ℝ)) ≤
      ∏ j ∈ Finset.range r, (M ^ j / (Nat.factorial j : ℝ)) := by
  have h_sorted : ∃ σ : Fin m ≃ Fin m, ∀ k l : Fin m, k < l → e (σ k) ≤ e (σ l) := by
    have h_sort : ∃ σ : Fin m → Fin m, Function.Injective σ ∧ ∀ k l : Fin m, k < l → e (σ k) ≤ e (σ l) := by
      have h_exists_min : ∀ (S : Finset (Fin m)), S.Nonempty → ∃ k ∈ S, ∀ j ∈ S, e k ≤ e j := by
        exact fun S hS => Finset.exists_min_image _ _ hS
      have h_sort : ∀ (n : ℕ) (hn : n ≤ m), ∀ (S : Finset (Fin m)), S.card = n → ∃ σ : Fin n → Fin m, Function.Injective σ ∧ (∀ k : Fin n, σ k ∈ S) ∧ (∀ k l : Fin n, k < l → e (σ k) ≤ e (σ l)) := by
        intro n hn S hS_card
        induction' n with n ih generalizing S;
        · simp +decide [ Function.Injective ];
        · obtain ⟨ k, hk₁, hk₂ ⟩ := h_exists_min S ( Finset.card_pos.mp ( by linarith ) ) ; obtain ⟨ σ, hσ₁, hσ₂, hσ₃ ⟩ := ih ( by linarith ) ( S.erase k ) ( by rw [ Finset.card_erase_of_mem hk₁, hS_card ] ; simp +decide ) ; use Fin.cons k σ; simp_all +decide [ Fin.forall_fin_succ, Function.Injective ] ;
          exact ⟨ fun i hi => False.elim <| hσ₂ i |>.1 <| hi.symm, fun i j hij => hσ₁ hij ⟩;
      exact Exists.elim ( h_sort m le_rfl Finset.univ ( by simp ) ) fun σ hσ => ⟨ σ, hσ.1, hσ.2.2 ⟩;
    exact ⟨ Equiv.ofBijective h_sort.choose ( ⟨ h_sort.choose_spec.1, Finite.injective_iff_surjective.mp h_sort.choose_spec.1 ⟩ ), h_sort.choose_spec.2 ⟩;
  obtain ⟨σ, hσ⟩ := h_sorted
  have h_prod_sorted : ∏ k, M ^ (e (σ k)) / (Nat.factorial (e (σ k)) : ℝ) ≤ ∏ j ∈ Finset.range m, M ^ (r - m + j) / (Nat.factorial (r - m + j) : ℝ) := by
    have h_prod_sorted : ∀ k : Fin m, e (σ k) ≤ r - m + k := by
      intro k
      have h_card : Finset.card (Finset.filter (fun l => e (σ k) ≤ e (σ l)) Finset.univ) ≥ m - k := by
        refine' le_trans _ ( Finset.card_mono <| show Finset.image ( fun l : Fin m => l ) ( Finset.Ici k ) ⊆ Finset.filter ( fun l => e ( σ k ) ≤ e ( σ l ) ) Finset.univ from _ );
        · simp +decide ;
        · grind;
      have h_card : Finset.card (Finset.filter (fun l => e (σ k) ≤ e l) Finset.univ) ≥ m - k := by
        convert h_card using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
        rw [ Finset.card_filter, Finset.card_filter ];
        conv_lhs => rw [ ← Equiv.sum_comp σ ] ;
      grind +suggestions;
    have h_prod_sorted : ∀ k : Fin m, M ^ (e (σ k)) / (Nat.factorial (e (σ k)) : ℝ) ≤ M ^ (r - m + k) / (Nat.factorial (r - m + k) : ℝ) := by
      intros k
      apply pow_div_factorial_mono hM (h_prod_sorted k);
      rw [ Nat.cast_add, Nat.cast_sub hm ] ; linarith [ show ( k : ℝ ) + 1 ≤ m by norm_cast; linarith [ Fin.is_lt k ] ];
    simpa only [ Finset.prod_range ] using Finset.prod_le_prod ( fun _ _ => div_nonneg ( pow_nonneg hM _ ) ( Nat.cast_nonneg _ ) ) fun _ _ => h_prod_sorted _;
  have h_prod_split : ∏ j ∈ Finset.range r, M ^ j / (Nat.factorial j : ℝ) = (∏ j ∈ Finset.range (r - m), M ^ j / (Nat.factorial j : ℝ)) * (∏ j ∈ Finset.range m, M ^ (r - m + j) / (Nat.factorial (r - m + j) : ℝ)) := by
    convert Finset.prod_range_add _ _ _ using 3 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) ; omega;
  have h_prod_ge_one : ∀ j ∈ Finset.range (r - m), 1 ≤ M ^ j / (Nat.factorial j : ℝ) := by
    intros j hj; rw [ one_le_div ( by positivity ) ] ; induction' j with j ih <;> norm_num [ pow_succ, Nat.factorial_succ ] at *;
    nlinarith [ ih ( Nat.lt_of_succ_lt hj ), show ( j : ℝ ) + 1 ≤ r - 1 by exact le_tsub_of_add_le_right ( by norm_cast; omega ), pow_nonneg hM j ];
  rw [ ← Equiv.prod_comp σ ];
  exact h_prod_sorted.trans ( h_prod_split.symm ▸ le_mul_of_one_le_left ( Finset.prod_nonneg fun _ _ => div_nonneg ( pow_nonneg hM _ ) ( Nat.cast_nonneg _ ) ) ( le_trans ( by norm_num ) ( Finset.prod_le_prod ( fun _ _ => by positivity ) h_prod_ge_one ) ) )

private lemma comparison_with_vanishing
    (r : ℕ) (hr : 2 ≤ r)
    (s : ℕ) (hs : s = 2 * r)
    (M : ℝ) (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_range : ∀ i, 0 ≤ u i ∧ (u i : ℝ) ≤ M)
    (hu_strict : StrictMono u) (hw_pos : ∀ i, 0 < w i)
    (v : Fin r → (Fin s → ℤ))
    (hv_kernel : ∀ (k : Fin r) (j : ℕ), j < r →
      ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0)
    (hv_indep : LinearIndependent ℝ (fun k : Fin r => (fun i : Fin s => ((v k i : ℤ) : ℝ))))
    (hv_succ : ∀ k : Fin r, ∀ x : Fin s → ℤ,
      (∀ j : ℕ, j < r → ∑ i, (x i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) →
      (fun i : Fin s => (x i : ℝ)) ∉
        Submodule.span ℝ ((fun j : Fin r => fun i : Fin s => (v j i : ℝ)) ''
          { j | j.val < k.val }) →
      ∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2 ≤ ∑ i : Fin s, ((x i : ℤ) : ℝ) ^ 2)
    (m : Fin r)
    (hm_nonzero : ∑ i, (v m i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0)
    (hm_min : ∀ k : Fin r, k.val < m.val →
      ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r = 0)
    (k : Fin r) (hk : k.val < m.val) :
    ∃ e : ℕ, 1 ≤ e ∧ e ≤ r - 1 ∧
      (∀ j : ℕ, j < r + e → ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧
      ∑ i : Fin s, ((v m i : ℤ) : ℝ) ^ 2 ≤
        (M ^ e / (Nat.factorial e : ℝ)) ^ 2 *
        ∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2 := by
  obtain ⟨e, he_pos, he_bound, he_vanish⟩ : ∃ e : ℕ, 1 ≤ e ∧ e ≤ r - 1 ∧ (∀ j : ℕ, j < r + e → ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧ (∑ i, ((Nat.choose (u i).toNat e : ℤ) * v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0) := by
    obtain ⟨t, ht⟩ : ∃ t : ℕ, r < t ∧ t < s ∧ (∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ t ≠ 0) ∧ (∀ j : ℕ, r < j → j < t → (∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0)) := by
      have ht_exists : ∃ t, r < t ∧ t < s ∧ (∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ t ≠ 0) := by
        have ht_exists : ∃ t, t < s ∧ (∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ t ≠ 0) := by
          contrapose! hv_indep;
          have := weighted_vandermonde_trivial_kernel s u w hu_strict hw_pos ( v k ) hv_indep; simp_all +decide [ funext_iff ] ;
          exact fun h => by have := h.ne_zero k; simp_all +decide [ funext_iff ] ;
        obtain ⟨ t, ht₁, ht₂ ⟩ := ht_exists;
        by_cases ht₃ : t < r;
        · exact False.elim <| ht₂ <| hv_kernel k t ht₃;
        · exact ⟨ t, lt_of_le_of_ne ( le_of_not_gt ht₃ ) ( Ne.symm <| by rintro rfl; exact ht₂ <| hm_min k hk ), ht₁, ht₂ ⟩;
      exact ⟨ Nat.find ht_exists, Nat.find_spec ht_exists |>.1, Nat.find_spec ht_exists |>.2.1, Nat.find_spec ht_exists |>.2.2, fun j hj₁ hj₂ => Classical.not_not.1 fun hj₃ => Nat.find_min ht_exists hj₂ ⟨ hj₁, by linarith [ Nat.find_spec ht_exists |>.2.1 ], hj₃ ⟩ ⟩;
    refine' ⟨ t - r, _, _, _, _ ⟩ <;> norm_num at *;
    · exact Nat.sub_pos_of_lt ht.1;
    · omega;
    · intro j hj; by_cases hj' : j < r <;> simp_all +decide [ Nat.add_sub_of_le ht.1.le ] ;
      cases hj'.eq_or_lt <;> [ aesop; exact ht.2.2.2 _ ‹_› ‹_› ];
    · convert binomial_multiply_moment s u w ( v k ) ( fun i => hu_range i |>.1 ) ( t - r ) r _ _ using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
      · intro j hj; by_cases hj' : j < r <;> simp_all +decide [ Nat.add_sub_of_le ht.1.le ] ;
        cases hj'.eq_or_lt <;> [ aesop; exact ht.2.2.2 _ ‹_› ‹_› ];
      · simpa only [ add_tsub_cancel_of_le ht.1.le ] using ht.2.2.1;
  refine' ⟨ e, he_pos, he_bound, he_vanish.1, le_trans ( hv_succ m _ _ _ ) _ ⟩;
  use fun i => Nat.choose ( u i |> Int.toNat ) e * v k i;
  · convert kernel_binomial_multiply s u w ( v k ) ( fun i => hu_range i |>.1 ) e r ( fun j hj => he_vanish.1 j ( by linarith ) ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    norm_cast;
  · intro h;
    refine' he_vanish.2 _;
    rw [ Submodule.mem_span ] at h;
    specialize h ( LinearMap.ker ( show ( Fin s → ℝ ) →ₗ[ℝ] ℝ from { toFun := fun x => ∑ i, x i * ( w i : ℝ ) * ( u i : ℝ ) ^ r, map_add' := fun x y => by simp +decide [ Finset.sum_add_distrib, mul_add, add_mul, mul_comm, mul_left_comm ], map_smul' := fun c x => by simp +decide [ Finset.mul_sum _ _ _, mul_assoc, mul_comm, mul_left_comm ] } ) ) ; simp_all +decide [ Set.subset_def ];
  · convert binomial_multiply_norm_bound s M u ( v k ) e hu_range using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    norm_cast

private lemma dim_constraint_from_vanishing
    (r s : ℕ) (_hr : 2 ≤ r) (hs : s = 2 * r)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_strict : StrictMono u) (hw_pos : ∀ i, 0 < w i)
    (m : ℕ) (_hm : m ≤ r)
    (v : Fin m → (Fin s → ℤ))
    (hv_indep : LinearIndependent ℝ (fun k : Fin m => fun i : Fin s => (v k i : ℝ)))
    (e : Fin m → ℕ)
    (he_vanish : ∀ k : Fin m, ∀ j : ℕ, j < r + e k →
      ∑ i, (v k i : ℝ) * (w i : ℝ) * (u i : ℝ) ^ j = 0) :
    ∀ e₀ : ℕ, 1 ≤ e₀ →
      (Finset.univ.filter (fun k : Fin m => e₀ ≤ e k)).card ≤ r - e₀ := by
  intro e₀ he₀_pos;
  by_cases he₀_le_r : e₀ ≤ r;
  · convert kernel_high_excess_count r s e₀ hs he₀_le_r u w hu_strict hw_pos _ _ _ _;
    use fun k i => v ( Finset.orderEmbOfFin ( Finset.univ.filter fun k => e₀ ≤ e k ) ( by simp +decide ) k ) i;
    · exact fun k j hj => he_vanish _ _ <| by linarith [ Finset.mem_filter.mp ( Finset.orderEmbOfFin_mem ( Finset.univ.filter fun k => e₀ ≤ e k ) ( by simp +decide ) k ) ] ;
    · exact hv_indep.comp _ ( fun k l hkl => by simpa [ Fin.ext_iff ] using hkl );
  · have h_empty : ∀ k : Fin m, e k < r := by
      intro k;
      contrapose! hv_indep;
      have h_zero : ∀ i : Fin s, v k i = 0 := by
        have h_zero : ∀ j : ℕ, j < s → ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0 := by
          exact fun j hj => he_vanish k j ( by linarith );
        have := weighted_vandermonde_trivial_kernel s u w hu_strict hw_pos ( v k ) h_zero; aesop;
      rw [ Fintype.not_linearIndependent_iff ];
      exact ⟨ fun i => if i = k then 1 else 0, by aesop ⟩;
    exact Finset.card_eq_zero.mpr ( Finset.eq_empty_of_forall_notMem fun k hk => by linarith [ Finset.mem_filter.mp hk, h_empty k ] ) |> fun h => h.symm ▸ Nat.zero_le _

private lemma multiply_comparison_bounds
    (r : ℕ)
    (N : Fin r → ℝ) (hN_nonneg : ∀ k, 0 ≤ N k)
    (N_mono : Monotone N)
    (m : Fin r)
    (f : Fin m.val → ℝ) (hf_nonneg : ∀ k, 0 ≤ f k)
    (h_comp : ∀ k : Fin m.val, N m ≤ f k * N ⟨k.val, by omega⟩)
    : N m ^ r ≤ (∏ k : Fin m.val, f k) * ∏ k : Fin r, N k := by
  have h_prod_mono : N m ^ (r - m.val) ≤ ∏ k : Fin (r - m.val), N (⟨m.val + k.val, by
    linarith [ Fin.is_lt m, Fin.is_lt k, Nat.sub_add_cancel ( show ( m : ℕ ) ≤ r from m.2.le ) ]⟩) := by
    exact le_trans ( by norm_num ) ( Finset.prod_le_prod ( fun _ _ => hN_nonneg _ ) fun _ _ => N_mono <| Fin.le_iff_val_le_val.mpr <| Nat.le_add_right _ _ )
  generalize_proofs at *;
  convert mul_le_mul ( show N m ^ m.val ≤ ∏ k : Fin m, f k * N ⟨ k.val, by linarith [ Fin.is_lt k, m.2 ] ⟩ from ?_ ) h_prod_mono ( ?_ ) ( Finset.prod_nonneg fun _ _ => mul_nonneg ( hf_nonneg _ ) ( hN_nonneg _ ) ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
  · rw [ ← pow_add, Nat.add_sub_of_le ( Nat.le_of_lt m.2 ) ];
  · rw [ Finset.prod_mul_distrib ];
    rw [ mul_assoc, ← Finset.prod_image ];
    · rw [ ← Finset.prod_mul_prod_compl ];
      congr! 2;
      any_goals exact Finset.univ.filter fun i => i.val < m.val;
      · refine' Finset.prod_bij ( fun x hx => ⟨ x, by linarith [ Fin.is_lt x, Fin.is_lt m, Finset.mem_filter.mp hx ] ⟩ ) _ _ _ _ <;> simp +decide [ Fin.ext_iff ];
        exact fun k => ⟨ ⟨ k, by linarith [ Fin.is_lt k, Fin.is_lt m ] ⟩, k.2, rfl ⟩;
      · refine' Finset.prod_bij ( fun i hi => ⟨ i - m, by
          grind ⟩ ) _ _ _ _ <;> simp +decide [Fin.ext_iff]
        all_goals generalize_proofs at *;
        · grind;
        · exact fun k => ⟨ ⟨ m + k, by linarith [ Fin.is_lt k, Nat.sub_add_cancel ( show ( m : ℕ ) ≤ r from m.2.le ) ] ⟩, Nat.le_add_right _ _, by simp +decide ⟩;
        · exact fun a ha => congr_arg N ( Fin.ext <| by simp +decide [ Nat.add_sub_of_le <| show ( m : ℕ ) ≤ a from ha ] );
    · exact fun x _ y _ h => by simpa [ Fin.ext_iff ] using h;
  · exact le_trans ( by norm_num ) ( Finset.prod_le_prod ( fun _ _ => hN_nonneg _ ) fun _ _ => h_comp _ );
  · exact pow_nonneg ( hN_nonneg _ ) _

private lemma excess_zero_with_comparison_bound
    (r : ℕ) (hr : 2 ≤ r)
    (s : ℕ) (hs : s = 2 * r)
    (M : ℝ) (hM : (s : ℝ) - 1 ≤ M)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_range : ∀ i, 0 ≤ u i ∧ (u i : ℝ) ≤ M)
    (hu_strict : StrictMono u)
    (hw_pos : ∀ i, 0 < w i)
    (v : Fin r → (Fin s → ℤ))
    (hv_kernel : ∀ (k : Fin r) (j : ℕ), j < r →
      ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0)
    (hv_indep : LinearIndependent ℝ (fun k : Fin r => (fun i : Fin s => ((v k i : ℤ) : ℝ))))
    (hv_mono : Monotone (fun k : Fin r => ∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2))
    (hv_succ : ∀ k : Fin r, ∀ x : Fin s → ℤ,
      (∀ j : ℕ, j < r → ∑ i, (x i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) →
      (fun i : Fin s => (x i : ℝ)) ∉
        Submodule.span ℝ ((fun j : Fin r => fun i : Fin s => (v j i : ℝ)) ''
          { j | j.val < k.val }) →
      ∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2 ≤ ∑ i : Fin s, ((x i : ℤ) : ℝ) ^ 2) :
    ∃ m : Fin r,
      (∑ i, (v m i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0) ∧
      (∑ i : Fin s, ((v m i : ℤ) : ℝ) ^ 2) ^ r ≤
        (∏ j ∈ Finset.range r, ((M : ℝ) ^ j / (Nat.factorial j : ℝ))) ^ 2 *
        ∏ k : Fin r, (∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2) := by
  obtain ⟨m, hm⟩ : ∃ m : Fin r, ∑ i, (v m i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0 ∧ ∀ k : Fin r, k.val < m.val → ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r = 0 := by
    obtain ⟨m, hm⟩ : ∃ m : Fin r, ∑ i, (v m i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0 := by
      apply excess_zero_among_independent r hr s hs u w hu_strict hw_pos v hv_kernel hv_indep;
    obtain ⟨m, hm⟩ : ∃ m : Fin r, ∑ i, (v m i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0 ∧ ∀ k : Fin r, k.val < m.val → ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r = 0 := by
      have h_exists_min : ∃ m : Fin r, ∑ i, (v m i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0 ∧ ∀ k : Fin r, k.val < m.val → ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r = 0 := by
        have h_nonempty : ∃ k : Fin r, ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0 := by
          use m
        obtain ⟨m, hm⟩ : ∃ m : Fin r, ∑ i, (v m i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0 ∧ ∀ k : Fin r, k.val < m.val → ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r = 0 := by
          have h_nonempty : ∃ k : Fin r, ∑ i, (v k i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0 := h_nonempty
          have h_well_founded : WellFounded (fun k l : Fin r => k.val < l.val) := by
            exact wellFounded_lt
          have := h_well_founded.has_min { k : Fin r | ∑ i, ( v k i : ℝ ) * w i * u i ^ r ≠ 0 } ⟨ m, hm ⟩;
          exact ⟨ this.choose, this.choose_spec.1, fun k hk => Classical.not_not.1 fun hk' => this.choose_spec.2 k hk' hk ⟩;
        use m
      exact h_exists_min;
    use m;
  obtain ⟨e, he_pos, he_bound, he_vanish, he_comp⟩ : ∃ e : Fin m.val → ℕ, (∀ k, 1 ≤ e k) ∧ (∀ k, e k ≤ r - 1) ∧ (∀ k, ∀ j, j < r + e k → ∑ i, (v ⟨k.val, by omega⟩ i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧ (∀ k, ∑ i, ((v m i : ℤ) : ℝ) ^ 2 ≤ (M ^ (e k) / (Nat.factorial (e k) : ℝ)) ^ 2 * ∑ i, ((v ⟨k.val, by omega⟩ i : ℤ) : ℝ) ^ 2) := by
    choose! e he₁ he₂ he₃ he₄ using comparison_with_vanishing r hr s hs M u w hu_range hu_strict hw_pos v hv_kernel hv_indep hv_succ m hm.1 hm.2;
    exact ⟨ _, fun k => he₁ _ <| k.2, fun k => he₂ _ <| k.2, fun k => he₃ _ <| k.2, fun k => he₄ _ <| k.2 ⟩;
  have h_prod_bound : (∏ k : Fin m.val, (M ^ (e k) / (Nat.factorial (e k) : ℝ))) ≤ (∏ j ∈ Finset.range r, (M ^ j / (Nat.factorial j : ℝ))) := by
    apply_rules [ excess_product_bound ];
    · exact Nat.le_of_lt m.2;
    · linarith [ show ( s : ℝ ) ≥ 2 by norm_cast; linarith ];
    · exact le_trans ( by norm_num [ hs ] ; linarith ) hM;
    · apply_rules [ dim_constraint_from_vanishing ];
      · exact Nat.le_of_lt m.2;
      · exact hv_indep.comp _ ( fun a b h => by simpa [ Fin.ext_iff ] using h );
  refine' ⟨ m, hm.1, _ ⟩;
  refine le_trans ?_ ( mul_le_mul_of_nonneg_right ( pow_le_pow_left₀ ( Finset.prod_nonneg fun _ _ => div_nonneg ( pow_nonneg ( by linarith [ show ( s : ℝ ) ≥ 2 by norm_cast; linarith ] ) _ ) ( Nat.cast_nonneg _ ) ) h_prod_bound 2 ) ?_ );
  · convert multiply_comparison_bounds r ( fun k => ∑ i, ( v k i : ℝ ) ^ 2 ) ( fun k => Finset.sum_nonneg fun _ _ => sq_nonneg _ ) hv_mono m ( fun k => ( M ^ e k / ( e k |> Nat.factorial : ℝ ) ) ^ 2 ) ( fun k => sq_nonneg _ ) ( fun k => he_comp k ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    rw [ Finset.prod_pow ];
  · exact Finset.prod_nonneg fun _ _ => Finset.sum_nonneg fun _ _ => sq_nonneg _

private lemma lattice_core
    (r : ℕ) (hr : 2 ≤ r)
    (s : ℕ) (hs : s = 2 * r)
    (M : ℝ) (hM : (s : ℝ) - 1 ≤ M)
    (W : ℝ) (hW : 1 ≤ W)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_range : ∀ i, 0 ≤ u i ∧ (u i : ℝ) ≤ M)
    (hu_strict : StrictMono u)
    (hw_pos : ∀ i, 0 < w i)
    (hw_bound : ∀ i, (w i : ℝ) ≤ W) :
    ∃ a : Fin s → ℤ,
      (∀ (j : ℕ), j < r → ∑ i, (a i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧
      (∑ i, (a i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0) ∧
      ((∑ i : Fin s, ((a i : ℤ) : ℝ) ^ 2) ^ r ≤
        (∏ j ∈ Finset.range r, ((M : ℝ) ^ j / (Nat.factorial j : ℝ))) ^ 4 *
        (2 : ℝ) ^ (r * (r - 1)) * (2 * (r : ℝ)) ^ r * W ^ (2 * r)) := by
  obtain ⟨v, hv_kernel, hv_indep, hv_mono, hv_prod, hv_succ⟩ :=
    successive_kernel_vectors_exist r hr s hs M W hW u w hu_range hu_strict hw_pos hw_bound
  obtain ⟨m, hm_nonzero, hm_bound⟩ :=
    excess_zero_with_comparison_bound r hr s hs M hM u w hu_range hu_strict hw_pos
      v hv_kernel hv_indep hv_mono hv_succ
  refine ⟨v m, fun j hj => hv_kernel m j hj, hm_nonzero, ?_⟩
  set P := ∏ j ∈ Finset.range r, ((M : ℝ) ^ j / (Nat.factorial j : ℝ))
  set Q := (2 : ℝ) ^ (r * (r - 1)) * (2 * (r : ℝ)) ^ r * W ^ (2 * r)
  calc (∑ i : Fin s, ((v m i : ℤ) : ℝ) ^ 2) ^ r
      ≤ P ^ 2 * ∏ k : Fin r, (∑ i : Fin s, ((v k i : ℤ) : ℝ) ^ 2) := hm_bound
    _ ≤ P ^ 2 * (Q * P ^ 2) := by
        gcongr
    _ = P ^ 4 * Q := by ring
    _ = P ^ 4 * (2 : ℝ) ^ (r * (r - 1)) * (2 * (r : ℝ)) ^ r * W ^ (2 * r) := by ring

private lemma factorial_product_lower_bound (r : ℕ) (hr : 2 ≤ r) :
    ((r : ℝ) / 64) ^ (r * (r - 1) / 2) ≤
    ∏ j ∈ Finset.range r, (Nat.factorial j : ℝ) := by
  induction' r with r ih <;> norm_num [ Finset.prod_range_succ ] at *;
  by_cases hr : r ≤ 64;
  · interval_cases r <;> norm_num [ Nat.factorial_succ, Finset.prod_range_succ ]
    all_goals first
      | (rw [show (2080 : ℕ) = 32 * 65 by norm_num, pow_mul]
         exact le_trans (pow_le_pow_left₀ (by norm_num) (show ((65 : ℝ) / 64) ^ 32 ≤ 3 by norm_num) 65) (by norm_num))
      | exact le_trans (pow_le_one₀ (by norm_num) (by norm_num)) (by norm_num)
  · -- For the inductive step, we can use the fact that $r! \geq \left(\frac{r}{e}\right)^r$.
    have h_factorial_bound : (r.factorial : ℝ) ≥ (r / Real.exp 1) ^ r := by
      rw [ div_pow, ge_iff_le, div_le_iff₀ ] <;> norm_cast <;> norm_num [ Nat.factorial_pos ];
      · rw [ ← div_le_iff₀' ( by positivity ) ] ; rw [ Real.exp_eq_exp_ℝ ] ; norm_num [ NormedSpace.exp_eq_tsum_div ] ; exact Summable.le_tsum ( show Summable _ from Real.summable_pow_div_factorial _ ) r ( fun _ _ => by positivity ) ;
      · positivity;
    suffices h_div : ((r + 1) / r : ℝ) ^ (r * (r - 1) / 2) * ((r + 1) / 64 : ℝ) ^ r ≤ (r / Real.exp 1) ^ r by
      refine le_trans ?_ ( mul_le_mul ( ih <| by linarith ) h_factorial_bound ?_ ?_ ) <;> try positivity;
      convert mul_le_mul_of_nonneg_left h_div ( show ( 0 :ℝ ) ≤ ( r / 64 ) ^ ( r * ( r - 1 ) / 2 ) by positivity ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
      rw [ ← mul_assoc, ← mul_pow ];
      rw [ show ( r + 1 ) * r / 2 = r * ( r - 1 ) / 2 + r by exact Nat.div_eq_of_eq_mul_left zero_lt_two <| by nlinarith [ Nat.sub_add_cancel ( by linarith : 1 ≤ r ), Nat.div_mul_cancel ( show 2 ∣ r * ( r - 1 ) from even_iff_two_dvd.mp <| Nat.even_mul_pred_self _ ) ] ] ; rw [ pow_add ] ; ring_nf;
      norm_num [ sq, mul_assoc, ne_of_gt ( by linarith : 0 < r ) ];
    suffices h_root : ((r + 1) / r : ℝ) ^ ((r - 1) / 2 : ℝ) * ((r + 1) / 64 : ℝ) ≤ (r / Real.exp 1) by
      convert pow_le_pow_left₀ ( by positivity ) h_root r using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) ; norm_num [ mul_pow, ← Real.rpow_natCast, ← Real.rpow_mul ( by positivity : 0 ≤ ( r + 1 : ℝ ) / r ) ] ; ring_nf ; norm_num [ Nat.cast_sub ( show 1 ≤ r by linarith ) ] ; ring_nf;
      exact Or.inl ( by rw [ ← Real.rpow_natCast ] ; rw [ Nat.cast_div ( show 2 ∣ r * ( r - 1 ) from even_iff_two_dvd.mp ( Nat.even_mul_pred_self _ ) ) ( by positivity ) ] ; cases r <;> norm_num ; ring_nf ) ;
    have h_exp_bound : ((r + 1) / r : ℝ) ^ ((r - 1) / 2 : ℝ) ≤ Real.exp (1 / 2) := by
      rw [ Real.rpow_def_of_pos ( by exact div_pos ( by positivity ) ( by norm_cast; linarith ) ) ];
      norm_num +zetaDelta at *;
      exact le_trans ( mul_le_mul_of_nonneg_right ( Real.log_le_sub_one_of_pos ( by positivity ) ) ( by linarith [ show ( r : ℝ ) ≥ 65 by norm_cast ] ) ) ( by nlinarith [ show ( r : ℝ ) ≥ 65 by norm_cast, div_mul_cancel₀ ( ( r : ℝ ) + 1 ) ( by positivity : ( r : ℝ ) ≠ 0 ) ] );
    refine le_trans ( mul_le_mul_of_nonneg_right h_exp_bound <| by positivity ) ?_;
    rw [ le_div_iff₀ ( Real.exp_pos _ ) ];
    have := Real.exp_one_lt_d9.le ; norm_num1 at * ; rw [ show ( 1 : ℝ ) = 1 / 2 + 1 / 2 by norm_num, Real.exp_add ] at * ; norm_num at *;
    nlinarith [ Real.add_one_le_exp ( 1 / 2 ), show ( r : ℝ ) ≥ 65 by norm_cast, mul_le_mul_of_nonneg_left ( show ( r : ℝ ) ≥ 65 by norm_cast ) ( Real.exp_nonneg ( 1 / 2 ) ) ]

private lemma two_mul_r_le_eight_pow (r : ℕ) (hr : 2 ≤ r) :
    2 * (r : ℝ) ≤ (8 : ℝ) ^ (r - 1) := by
  rcases r with ( _ | _ | r ) <;> norm_num at *;
  exact mod_cast Nat.recOn r ( by norm_num ) fun n ihn => by norm_num [ Nat.pow_succ ] at ihn ⊢ ; linarith;

private lemma moment_product_upper_bound (r : ℕ) (hr : 2 ≤ r) (M : ℝ) (hM : 0 ≤ M) :
    ∏ j ∈ Finset.range r, (M ^ j / (Nat.factorial j : ℝ)) ≤
    (64 * M / (r : ℝ)) ^ (r * (r - 1) / 2) := by
  have hr0 : (0 : ℝ) < (r : ℝ) := by exact_mod_cast (show 0 < r by omega)
  have hP : 0 < ((r : ℝ) / 64) ^ (r * (r - 1) / 2) := pow_pos (div_pos hr0 (by norm_num)) _
  rw [Finset.prod_div_distrib, Finset.prod_pow_eq_pow_sum, Finset.sum_range_id]
  rw [show (64 * M / (r : ℝ)) ^ (r * (r - 1) / 2) = M ^ (r * (r - 1) / 2) / ((r : ℝ) / 64) ^ (r * (r - 1) / 2) by
    rw [div_pow, div_pow, mul_pow]; first | (field_simp; done) | (field_simp; ring)]
  exact div_le_div_of_nonneg_left (pow_nonneg hM _) hP (factorial_product_lower_bound r hr)

private lemma lattice_bound_implies_coord_bound (r : ℕ) (hr : 2 ≤ r) (M W : ℝ)
    (hM : 0 ≤ M) (hW : 0 ≤ W) :
    (∏ j ∈ Finset.range r, (M ^ j / (Nat.factorial j : ℝ))) ^ 4 *
    (2 : ℝ) ^ (r * (r - 1)) * (2 * (r : ℝ)) ^ r * W ^ (2 * r) ≤
    ((256 * M / (r : ℝ)) ^ (r - 1 : ℕ) * W) ^ (2 * r) := by
  have h1 : (∏ j ∈ Finset.range r, (M ^ j / (Nat.factorial j : ℝ))) ^ 4 ≤ (64 * M / r) ^ (2 * r * (r - 1)) := by
    convert pow_le_pow_left₀ ( Finset.prod_nonneg fun _ _ => by positivity ) ( moment_product_upper_bound r hr M hM ) 4 using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) ; ring_nf;
    rw [ show r * ( r - 1 ) * 2 = r * ( r - 1 ) / 2 * 4 by linarith [ Nat.div_mul_cancel ( show 2 ∣ r * ( r - 1 ) from even_iff_two_dvd.mp ( Nat.even_mul_pred_self _ ) ) ] ];
  have h2 : (2 * r : ℝ) ^ r ≤ 8 ^ (r * (r - 1)) := by
    convert pow_le_pow_left₀ ( by positivity ) ( two_mul_r_le_eight_pow r hr ) r using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) ; ring
  have h3 : (2 : ℝ) ^ (r * (r - 1)) * (2 * r) ^ r ≤ 4 ^ (2 * r * (r - 1)) := by
    convert mul_le_mul_of_nonneg_left h2 ( pow_nonneg zero_le_two ( r * ( r - 1 ) ) ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) ; ring_nf;
    norm_num [ pow_mul', ← mul_pow ];
  convert mul_le_mul_of_nonneg_right ( mul_le_mul h1 h3 ( by positivity ) ( by positivity ) ) ( by positivity : 0 ≤ W ^ ( 2 * r ) ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) ; ring;
  rw [ show ( 256 * M / r : ℝ ) = ( 64 * M / r ) * 4 by ring ] ; rw [ mul_pow ] ; ring_nf;
  norm_num [ mul_assoc, ← mul_pow ]

private lemma silr_lattice_case
    (r : ℕ) (hr : 2 ≤ r)
    (s : ℕ) (hs : s = 2 * r)
    (M : ℝ) (hM : (s : ℝ) - 1 ≤ M)
    (W : ℝ) (hW : 1 ≤ W)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_range : ∀ i, 0 ≤ u i ∧ (u i : ℝ) ≤ M)
    (hu_strict : StrictMono u)
    (hw_pos : ∀ i, 0 < w i)
    (hw_bound : ∀ i, (w i : ℝ) ≤ W) :
    ∃ a : Fin s → ℤ,
      (∀ (j : ℕ), j < r → ∑ i, (a i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧
      (∑ i, (a i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0) ∧
      (∀ i, |(a i : ℝ)| ≤ (256 * M / (r : ℝ)) ^ (r - 1 : ℕ) * W) := by
  obtain ⟨a, ha⟩ := lattice_core r hr s hs M hM W hW u w hu_range hu_strict hw_pos hw_bound;
  refine' ⟨ a, ha.1, ha.2.1, _ ⟩;
  intro i
  have h_sq : (a i : ℝ) ^ 2 ≤ (∑ j : Fin s, (a j : ℝ) ^ 2) := by
    exact_mod_cast Finset.single_le_sum ( fun i _ => sq_nonneg ( a i ) ) ( Finset.mem_univ i );
  have h_abs : (a i : ℝ) ^ (2 * r) ≤ ((256 * M / r) ^ (r - 1) * W) ^ (2 * r) := by
    convert le_trans _ ( ha.2.2.trans _ ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
    · simpa only [ pow_mul ] using pow_le_pow_left₀ ( sq_nonneg _ ) h_sq _;
    · convert lattice_bound_implies_coord_bound r hr M W ( by linarith [ show ( s : ℝ ) ≥ 2 * 2 by norm_cast; linarith ] ) ( by linarith ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
  contrapose! h_abs;
  convert pow_lt_pow_left₀ h_abs ( mul_nonneg ( pow_nonneg ( div_nonneg ( mul_nonneg ( by norm_num ) ( show 0 ≤ M by linarith [ show ( s : ℝ ) ≥ 2 by norm_cast; linarith ] ) ) ( Nat.cast_nonneg _ ) ) _ ) ( by positivity ) ) ( by positivity : ( 2 * r ) ≠ 0 ) using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl))) ; norm_num [ pow_mul ]

private theorem small_integer_linear_relation_proof
    (r : ℕ) (hr : 1 ≤ r)
    (s : ℕ) (hs : s = 2 * r)
    (M : ℝ) (hM : (s : ℝ) - 1 ≤ M)
    (W : ℝ) (hW : 1 ≤ W)
    (u : Fin s → ℤ) (w : Fin s → ℕ)
    (hu_range : ∀ i, 0 ≤ u i ∧ (u i : ℝ) ≤ M)
    (hu_strict : StrictMono u)
    (hw_pos : ∀ i, 0 < w i)
    (hw_bound : ∀ i, (w i : ℝ) ≤ W) :
    ∃ a : Fin s → ℤ,
      (∀ (j : ℕ), j < r → ∑ i, (a i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ j = 0) ∧
      (∑ i, (a i : ℝ) * (w i : ℝ) * ((u i : ℝ)) ^ r ≠ 0) ∧
      (∀ i, |(a i : ℝ)| ≤ (256 * M / (r : ℝ)) ^ (r - 1 : ℕ) * W) := by
  by_cases hr2 : r ≥ 2;
  · convert silr_lattice_case r hr2 s hs M hM W hW u w hu_range hu_strict hw_pos hw_bound using 1 <;> (try (first | with_reducible_and_instances rfl | (show (_ : LE ℝ) = _; rfl) | (show (_ : LT ℝ) = _; rfl) | (show (_ : LE ℝ) = _; with_unfolding_all rfl) | (show (_ : LT ℝ) = _; with_unfolding_all rfl)));
  · interval_cases r ; subst hs;
    refine' ⟨ fun i => if i = 0 then w 1 else -w 0, _, _, _ ⟩ <;> simp_all +decide [ Fin.sum_univ_succ ];
    · ring;
    · nlinarith [ show ( w 0 : ℝ ) * w 1 > 0 by exact mul_pos ( Nat.cast_pos.mpr hw_pos.1 ) ( Nat.cast_pos.mpr hw_pos.2 ), show ( u 0 : ℝ ) < u 1 by exact_mod_cast hu_strict ( by decide ) ]


theorem erdos_1094__h2__h2__h2__h3__h1__h1__h1__h1 : ∀ (r : ℕ),
  (1 : ℕ) ≤ r →
    ∀ (s : ℕ),
      s = (2 : ℕ) * r →
        ∀ (M : ℝ),
          (↑s : ℝ) - (1 : ℝ) ≤ M →
            ∀ (W : ℝ),
              (1 : ℝ) ≤ W →
                ∀ (u : Fin s → ℤ) (w : Fin s → ℕ),
                  (∀ (i : Fin s), (0 : ℤ) ≤ u i ∧ (↑(u i) : ℝ) ≤ M) →
                    StrictMono u →
                      (∀ (i : Fin s), (0 : ℕ) < w i) →
                        (∀ (i : Fin s), (↑(w i) : ℝ) ≤ W) →
                          ∃ (a : Fin s → ℤ),
                            (∀ j < r, ∑ i : Fin s, (↑(a i) : ℝ) * (↑(w i) : ℝ) * (↑(u i) : ℝ) ^ j = (0 : ℝ)) ∧
                              ∑ i : Fin s, (↑(a i) : ℝ) * (↑(w i) : ℝ) * (↑(u i) : ℝ) ^ r ≠ (0 : ℝ) ∧
                                ∀ (i : Fin s), |(↑(a i) : ℝ)| ≤ ((256 : ℝ) * M / (↑r : ℝ)) ^ (r - (1 : ℕ)) * W := by
  intro r hr s hs M hM W hW u w h1 h2 h3 h4
  exact small_integer_linear_relation_proof r hr s hs M hM W hW u w h1 h2 h3 h4