Interpolate degree ge of no data

lemma interpolate_degree_ge_of_no_data {n L : ℕ} (S : Finset (Fin L))    {queryOf responseOf : Fin L → ZMod p}    (hquery : Set.InjOn queryOf ↑S)    (hNoData : ¬ ∃ d : Fin (n + 1) → ZMod p,      ∀ i ∈ S, (CPolynomial.ofFn d).eval (queryOf i) = responseOf i) :    (↑(n + 1) : WithBot ℕ) ≤      (CLagrange.interpolate S queryOf responseOf).degree := by  by_contra hlt  push Not at hlt  set Q : Polynomial (ZMod p) :=    Lagrange.interpolate S queryOf responseOf with hQ_def  have hQdeg_lt : Q.degree < (↑(n + 1) : WithBot ℕ) := by    have h := hlt    rw [show        (CLagrange.interpolate S          queryOf responseOf).degree          = Q.degree from by          rw [hQ_def, ← CLagrange.cinterpolate_eq_interpolate, ← degree_toPoly]] at h    exact h  have hQ_mem : Q ∈ Polynomial.degreeLT (ZMod p) (n + 1) :=    Polynomial.mem_degreeLT.mpr hQdeg_lt  apply hNoData  refine ⟨Polynomial.degreeLTEquiv (ZMod p) (n + 1) ⟨Q, hQ_mem⟩, ?_⟩  intro i hi  have hQ_eval : Q.eval (queryOf i) = responseOf i := by    rw [hQ_def]    exact Lagrange.eval_interpolate_at_node responseOf      hquery hi  have hQ_sum :      Q.eval (queryOf i) =        ∑ k : Fin (n + 1),          Polynomial.degreeLTEquiv (ZMod p) (n + 1) ⟨Q, hQ_mem⟩ k *            (queryOf i) ^ (k : ℕ) :=    Polynomial.eval_eq_sum_degreeLTEquiv hQ_mem (queryOf i)  set d : Fin (n + 1) → ZMod p :=    Polynomial.degreeLTEquiv (ZMod p) (n + 1) ⟨Q, hQ_mem⟩ with hd_def  let P_C : CPolynomial (ZMod p) :=    ⟨(CompPoly.CPolynomial.Raw.mk (Array.ofFn d)).trim,      CompPoly.CPolynomial.Raw.Trim.isCanonical_trim _⟩  change CPolynomial.eval (queryOf i) P_C = responseOf i  rw [eval_toPoly]  have hPC_eq : P_C.toPoly = Q := by    apply Polynomial.ext    intro k    rw [← coeff_toPoly]    change ((CompPoly.CPolynomial.Raw.mk (Array.ofFn d)).trim).coeff k = Q.coeff k    rw [CompPoly.CPolynomial.Raw.Trim.coeff_eq_coeff]    change (Array.ofFn d).getD k 0 = Q.coeff k    rw [Array.getD_eq_getD_getElem?, Array.getElem?_ofFn]    by_cases hk : k < n + 1    · simp [hk, hd_def, Polynomial.degreeLTEquiv]    · push Not at hk      simp only [hk.not_gt, dite_false, Option.getD_none]      symm      exact Polynomial.coeff_eq_zero_of_degree_lt        (lt_of_lt_of_le hQdeg_lt (by exact_mod_cast hk))  rw [hPC_eq]  exact hQ_eval