Exists Pz of coeffs of close proximity

lemma exists_Pz_of_coeffs_of_close_proximity    {k : ℕ}  {z : F}  (hS : z ∈ coeffs_of_close_proximity (k := k) ωs δ u₀ u₁)    :  ∃ Pz : F[X], Pz.natDegree ≤ k ∧ δᵣ(u₀ + z • u₁, Pz.eval ∘ ωs) ≤ δ := by    unfold coeffs_of_close_proximity at hS    obtain ⟨w, hS, dist⟩ : ∃ a ∈ ReedSolomon.code ωs (k + 1), ↑δᵣ(u₀ + z • u₁, a) ≤ δ := by      simpa using hS    obtain ⟨p, hS⟩ : ∃ y ∈ degreeLT F (k + 1), (ReedSolomon.evalOnPoints ωs) y = w := by      change ∃ y ∈ degreeLT F (k + 1), (ReedSolomon.evalOnPoints ωs) y = w at hS      exact hS    exact ⟨p, ⟨      by if h : p = 0         then simp [h]         else rw [mem_degreeLT, degree_eq_natDegree h, Nat.cast_lt] at hS; grind,      by convert dist; rw [←hS.2]; rfl    ⟩⟩