Mem decoder of dist

theorem mem_decoder_of_dist    {k r D e : ℕ}    (he : (e : ℝ) < ↑n - Real.sqrt ((↑k + 1) * ↑n))    {ωs : Fin n ↪ F}    {f : Fin n → F}    {p : F[X]}    (hdeg : p.natDegree < k)    (hdist : Δ₀(f, p.eval ∘ ωs) ≤ e) :    p ∈ decoder k r D e ωs f := by  -- Extract basic bounds from he  have heNonneg : (0 : ℝ) ≤ e := Nat.cast_nonneg e  have hsqrtNonneg := Real.sqrt_nonneg ((↑k + 1) * (↑n : ℝ))  have hnPos : (0 : ℝ) < n := by linarith  have hkLtN : k + 1 ≤ n := by    by_contra hc    push Not at hc    have : (↑k + 1 : ℝ) * ↑n ≥ ↑n * ↑n := by      have h1 : n ≤ k + 1 := le_of_lt hc      exact_mod_cast Nat.mul_le_mul_right n h1    have : Real.sqrt ((↑k + 1) * ↑n) ≥ ↑n := by      calc Real.sqrt ((↑k + 1) * ↑n)            ≥ Real.sqrt (↑n * ↑n) :=            Real.sqrt_le_sqrt (by exact_mod_cast this)        _ = ↑n := Real.sqrt_mul_self (le_of_lt hnPos)    linarith  -- Show there exists a suitable multiplicity parameter m such that  -- `proximity_gap_johnson k n m > e / n`.  -- `proximity_gap_johnson k n m = 1 - √ρ - √ρ/(2m)` where  -- $\rho = (k+1)/n$.  -- From `he` we get $e/n < 1 - \sqrt{\rho}$; for $m$ large enough,  -- $\sqrt{\rho}/(2m) < \text{gap}$.  have hExists :      ∃ m : ℕ, 0 < m ∧        (e : ℝ) / ↑n < proximity_gap_johnson k n m := by    -- Relate the ℚ-based √ρ in `proximity_gap_johnson` to the    -- ℝ-based $\sqrt{(k+1) \cdot n}$ in `he`.    -- $\rho = (k+1)/n$ casts to $(k+1)/n$ in ℝ, and    -- $\sqrt{\rho} \cdot n = \sqrt{(k+1) \cdot n}$.    set sqrtRho : ℝ :=      Real.sqrt (↑((k + 1 : ℚ) / (↑n : ℚ)))    have hρCast :        (↑((k + 1 : ℚ) / (↑n : ℚ)) : ℝ) = (↑k + 1) / ↑n := by      push_cast      ring    have hρNonneg :        (0 : ℝ) ≤ ↑((k + 1 : ℚ) / (↑n : ℚ)) := by      rw [hρCast]      positivity    have hsqrtRhoNonneg : 0 ≤ sqrtRho :=      Real.sqrt_nonneg _    -- Key identity: sqrtRho * n = √((k+1)*n)    have hsqrtRel :        sqrtRho * ↑n = Real.sqrt ((↑k + 1) * ↑n) := by      conv_rhs =>        rw [show (↑k + 1 : ℝ) * ↑n =          ↑((k + 1 : ℚ) / ↑n) * (↑n * ↑n) from by          rw [hρCast]; field_simp]      rw [Real.sqrt_mul hρNonneg,        Real.sqrt_mul_self (le_of_lt hnPos)]    -- From he, derive e/n < 1 - sqrtRho    have hGap : (e : ℝ) / ↑n < 1 - sqrtRho := by      rw [div_lt_iff₀ hnPos]      nlinarith [hsqrtRel]    -- The gap is positive    set gap := 1 - sqrtRho - (e : ℝ) / ↑n with gapDef    have hgapPos : 0 < gap := by linarith    -- Find m₀ > sqrtRho / (2 * gap) by the Archimedean    -- property    obtain ⟨m₀, hm₀⟩ := exists_nat_gt (sqrtRho / (2 * gap))    have hm₀Pos : 0 < m₀ := by      rcases Nat.eq_zero_or_pos m₀ with rfl | h      · exfalso        simp at hm₀        linarith [div_nonneg hsqrtRhoNonneg          (by linarith : (0:ℝ) ≤ 2 * gap)]      · exact h    -- sqrtRho / (2 * m₀) < gap    have hm₀PosReal : (0 : ℝ) < ↑m₀ :=      Nat.cast_pos.mpr hm₀Pos    have hm₀Bound : sqrtRho / (2 * ↑m₀) < gap := by      have h2m : (0 : ℝ) < 2 * ↑m₀ := by linarith      have h2g : (0 : ℝ) < 2 * gap := by linarith      rw [div_lt_iff₀ h2m]      have hm₀' : sqrtRho / (2 * gap) < ↑m₀ := hm₀      rw [div_lt_iff₀ h2g] at hm₀'      nlinarith    exact ⟨m₀, hm₀Pos, by      simp only [proximity_gap_johnson]      linarith⟩  -- Unfold the decoder and enter the if-branch  simp only [decoder]  rw [dif_pos hExists]  simp only [List.mem_filter, decide_eq_true_eq]  refine ⟨?_, hdist⟩  -- Show p is a root of Q = polySol k n m ωs f via  -- `dvd_property`.  -- `dvd_property` gives (Y - p(X)) | Q when p is a close  -- codeword, which by the factor theorem makes p a root of Q.  obtain ⟨hmPos, hmJohnson⟩ := hExists.choose_spec  set mDec := hExists.choose  -- Form p's evaluation as a codeword in code ωs k  have hpDeg : p.degree < (k : WithBot ℕ) :=    lt_of_le_of_lt degree_le_natDegree      (by exact_mod_cast hdeg)  have hkLeN : k ≤ n := by omega  have hpCode :      p.eval ∘ (ωs : Fin n → F) ∈ code ωs k :=    Submodule.mem_map.mpr      ⟨p, mem_degreeLT.mpr hpDeg, rfl⟩  set p' : code ωs k :=    ⟨p.eval ∘ (ωs : Fin n → F), hpCode⟩  -- `toPolynomial` recovers p from its evaluations  -- (since deg p < k ≤ n)  have hctp : toPolynomial p' = p := by    simp only [toPolynomial, p']    exact interpolate_eq_of_degree_lt p      (lt_of_lt_of_le hdeg hkLeN)  -- `dvd_property` gives divisibility  have hdvd : X - C p ∣ polySol k n mDec ωs f := by    rw [← hctp]    exact dvd_property (f := f) hkLtN      (by omega : 1 ≤ mDec) p'      polySol_weightedDegree_le      polySol_multiplicity (by        have hfEq :            (fun i ↦ (toPolynomial p').eval (ωs i)) =            p.eval ∘ ωs := by          ext i          simp [hctp]        rw [hfEq]        exact lt_of_le_of_lt          (div_le_div_of_nonneg_right            (Nat.cast_le.mpr hdist) (le_of_lt hnPos))          hmJohnson)  -- From divisibility, p is a root of Q, hence in Q.roots  have hroot : (polySol k n mDec ωs f).IsRoot p :=    dvd_iff_isRoot.mp hdvd  exact Multiset.mem_toList.mpr    ((mem_roots polySol_ne_zero).mpr hroot)