Find a successful

lemma find_a_successful {L : ℕ} (U : Finset (Fin L)) (n : ℕ)    (query : Fin L → ZMod p) (response : Fin L → ZMod p)    (hUcard : n < U.card) (hqueryU : Set.InjOn query ↑U)    (hinterp : (CLagrange.interpolate U query response).degree ≥ n) :    (findA U n query response).isSome := by  by_contra h_not  have h_none : findA U n query response = none := by    match hc : findA U n query response with    | none => rfl    | some _ => simp [hc] at h_not  unfold findA at h_none  rw [List.find?_eq_none] at h_none  simp only [decide_eq_true_eq] at h_none  have h_deg_lt : ∀ (s : Finset (Fin L)), s ⊆ U → s.card = n + 1 →      (CLagrange.interpolate s query response).degree < ↑n := by    intro s hsU hs    exact lt_of_le_of_ne      (interp_degree_le_of_card s query response (hqueryU.mono hsU) hs)      (h_none s (finset_subset_mem_sublists_len_map s U hsU hs))  -- Core argument: construct a polynomial of degree < n agreeing with all L values  -- Pick a subset T of size n  obtain ⟨T, hTU, hTcard⟩ :=    Finset.exists_subset_card_eq (n := n) (s := U) (by omega)  -- Let Q_T be the Mathlib interpolation over T  set Q_T := Lagrange.interpolate T query response with hQ_T_def  have hQ_T_deg : Q_T.degree < ↑n := by    rw [← hTcard]    exact Lagrange.degree_interpolate_lt response (hqueryU.mono hTU)  -- Show Q_T agrees with response on all of Fin L  have hQ_T_eval : ∀ i ∈ U, Q_T.eval (query i) = response i := by    intro i hiU    by_cases hiT : i ∈ T    · exact Lagrange.eval_interpolate_at_node response (hqueryU.mono hTU) hiT    · -- Use the `(n + 1)`-subset `T ∪ {i}`.      set Si := insert i T with hSi_def      have hSiU : Si ⊆ U := by        intro x hx        simp only [hSi_def, Finset.mem_insert] at hx        rcases hx with rfl | hxT        · exact hiU        · exact hTU hxT      have hSicard : Si.card = n + 1 := by        rw [Finset.card_insert_of_notMem hiT, hTcard]      -- The interpolation over Si also has degree < n (via CPolynomial bridge)      have hSi_deg_lt : (CLagrange.interpolate Si query response).degree < ↑n :=        h_deg_lt Si hSiU hSicard      -- Transfer to Polynomial world      set Q_Si := Lagrange.interpolate Si query response with hQ_Si_def      have hQ_Si_deg : Q_Si.degree < ↑n := by        have h := hSi_deg_lt        rw [degree_toPoly, CLagrange.cinterpolate_eq_interpolate] at h        exact h      -- Q_T and Q_Si agree on T      have hagree : ∀ j ∈ T, Q_T.eval (query j) = Q_Si.eval (query j) := by        intro j hjT        rw [Lagrange.eval_interpolate_at_node response (hqueryU.mono hTU) hjT,            Lagrange.eval_interpolate_at_node response              (hqueryU.mono hSiU)              (Finset.mem_insert_of_mem hjT)]      -- By uniqueness (both degree < |T| = n, agree on T), Q_T = Q_Si      have hTn : (↑n : WithBot ℕ) = ↑(T.card) := by        rw [hTcard]      have heq : Q_T = Q_Si := by        rw [hTn] at hQ_T_deg hQ_Si_deg        exact Polynomial.eq_of_degrees_lt_of_eval_index_eq T          (hqueryU.mono hTU) hQ_T_deg hQ_Si_deg hagree      -- Hence Q_T.eval(query i) = Q_Si.eval(query i) = response i      rw [heq]      exact Lagrange.eval_interpolate_at_node response        (hqueryU.mono hSiU) (Finset.mem_insert_self i T)  -- Derive n < U.card from hinterp and degree_interpolate_lt  have hinterp_poly : (Lagrange.interpolate U query response).degree ≥ ↑n := by    have h := hinterp    rw [degree_toPoly, CLagrange.cinterpolate_eq_interpolate] at h    exact h  have hScard_gt : n < U.card := by    have h2 : (Lagrange.interpolate U query response).degree < ↑U.card :=      Lagrange.degree_interpolate_lt response hqueryU    exact_mod_cast lt_of_le_of_lt hinterp_poly h2  -- Q_T = interpolation over U, since Q_T has degree < U.card and agrees on U  have hQ_T_deg_S : Q_T.degree < ↑U.card :=    lt_trans hQ_T_deg (by exact_mod_cast hScard_gt)  have hP_eq : Q_T = Lagrange.interpolate U query response :=    Lagrange.eq_interpolate_of_eval_eq (s := U) response      hqueryU hQ_T_deg_S hQ_T_eval  -- Contradiction: interp over S has degree ≥ n but Q_T has degree < n  exact absurd (hP_eq ▸ hQ_T_deg) (not_lt.mpr hinterp_poly)