Find s existence

lemma find_s_existence {L : ℕ} (n : ℕ) (τ c : ZMod p) (A : Finset (Fin L))    (query : Fin L → ZMod p) (response : Fin L → ZMod p)    (hA : (CLagrange.interpolate A query response).degree = n + 1)    (hquery : Set.InjOn query ↑A) (hn : 1 ≤ n) :    ∃ S ⊆ A, S.card = n + 1      ∧ (CLagrange.interpolate S query response).eval τ ≠ c := by  by_contra h_all  push Not at h_all  -- Bridge h_all to Polynomial world  have h_poly : ∀ S ⊆ A, S.card = n + 1 →      (Lagrange.interpolate S query response).eval τ = c := by    intro S hS hcard    have h := h_all S hS hcard    rwa [eval_toPoly, CLagrange.cinterpolate_eq_interpolate] at h  -- Bridge hA to Polynomial world  have hA_poly : (Lagrange.interpolate A query response).degree = ↑(n + 1) := by    rw [← CLagrange.cinterpolate_eq_interpolate, ← degree_toPoly]; exact_mod_cast hA  -- Step A: n + 1 < A.card  have hn_lt : n + 1 < A.card := by    have h := Lagrange.degree_interpolate_lt response hquery    rw [hA_poly] at h; exact_mod_cast h  -- Step B: Pick A' ⊆ A with |A'| = n + 2  obtain ⟨A', hA'_sub, hA'_card⟩ :=    Finset.exists_subset_card_eq (show n + 2 ≤ A.card by omega)  -- Step C: interpolate A = interpolate A' (by uniqueness, since deg < |A'| and agrees on A')  have hA'_eq : Lagrange.interpolate A query response =      Lagrange.interpolate A' query response :=    Lagrange.eq_interpolate_of_eval_eq response      (hquery.mono hA'_sub)      (by rw [hA_poly, hA'_card]; exact_mod_cast (show n + 1 < n + 2 by omega))      (fun i hi => Lagrange.eval_interpolate_at_node response        hquery (hA'_sub hi))  -- Degree of interpolate A' equals n + 1  have hA'_deg : (Lagrange.interpolate A' query response).degree = ↑(n + 1) := by    rw [← hA'_eq]; exact hA_poly  -- Step D: Pick two distinct elements `i`, `j ∈ A'` (possible since `|A'| = n + 2 ≥ 2`).  obtain ⟨i, j, hi, hj, hij⟩ := Finset.one_lt_card_iff.mp (show 1 < A'.card by omega)  -- Erase subset/cardinality facts  have hej_sub : A'.erase j ⊆ A := (Finset.erase_subset j A').trans hA'_sub  have hei_sub : A'.erase i ⊆ A := (Finset.erase_subset i A').trans hA'_sub  have hej_card : (A'.erase j).card = n + 1 := by    rw [Finset.card_erase_of_mem hj, hA'_card]; omega  have hei_card : (A'.erase i).card = n + 1 := by    rw [Finset.card_erase_of_mem hi, hA'_card]; omega  -- Step E: Show (interpolate A').eval τ = c via decomposition  --   PA' = P_{A'\j} · basisDivisor(qi,qj) + P_{A'\i} · basisDivisor(qj,qi)  --   Evaluating at τ and using h_poly gives c · (bd + bd') = c · 1 = c  have hA'_eval_tau : (Lagrange.interpolate A' query response).eval τ = c := by    have hdecomp := Lagrange.interpolate_eq_add_interpolate_erase response      (hquery.mono hA'_sub) hi hj hij    have h1 := congr_arg (Polynomial.eval τ) hdecomp    simp only [Polynomial.eval_add, Polynomial.eval_mul] at h1    rw [h_poly (A'.erase j) hej_sub hej_card,        h_poly (A'.erase i) hei_sub hei_card] at h1    rw [h1, ← _root_.mul_add, ← Polynomial.eval_add,        Lagrange.basisDivisor_add_symm          (show query i ≠ query j from fun h => hij (hquery (hA'_sub hi) (hA'_sub hj) h))]    simp  -- Step F: Choose k ∈ A' such that τ ∉ (A'.erase k).image query  obtain ⟨k, hk, hk_fresh⟩ : ∃ k ∈ A', τ ∉ (A'.erase k).image query := by    by_cases hτ : ∃ k ∈ A', query k = τ    · obtain ⟨k, hk, hkq⟩ := hτ      exact ⟨k, hk, by        simp only [Finset.mem_image]        rintro ⟨x, hxe, hxq⟩        exact Finset.ne_of_mem_erase hxe          (hquery (hA'_sub (Finset.mem_of_mem_erase hxe)) (hA'_sub hk)            (hxq.trans hkq.symm))⟩    · push Not at hτ      obtain ⟨k, hk⟩ := Finset.card_pos.mp (show 0 < A'.card by omega)      exact ⟨k, hk, by        simp only [Finset.mem_image]        rintro ⟨x, hxe, hxq⟩        exact hτ x (Finset.mem_of_mem_erase hxe) hxq⟩  -- Erase-k facts  have hek_card : (A'.erase k).card = n + 1 := by    rw [Finset.card_erase_of_mem hk, hA'_card]; omega  have hek_sub : A'.erase k ⊆ A := (Finset.erase_subset k A').trans hA'_sub  -- Degree of interpolate (A'.erase k) < n + 1  have h_deg_ek : (Lagrange.interpolate (A'.erase k) query response).degree < ↑(n + 1) := by    rw [← hek_card]    exact Lagrange.degree_interpolate_lt response      (hquery.mono ((Finset.erase_subset k A').trans hA'_sub))  -- Step G: The difference polynomial vanishes at `n + 2` distinct field values, so it is zero.  have hQ_zero : Lagrange.interpolate A' query response -      Lagrange.interpolate (A'.erase k) query response = 0 := by    apply Polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zero      ((A'.erase k).image query ∪ {τ})    · -- degree < |T|      have hT_card : ((A'.erase k).image query ∪ {τ}).card = n + 2 := by        rw [Finset.card_union_of_disjoint (Finset.disjoint_singleton_right.mpr hk_fresh),            Finset.card_image_of_injOn              (hquery.mono ((Finset.erase_subset k A').trans hA'_sub)),            hek_card, Finset.card_singleton]      rw [hT_card]      calc (Lagrange.interpolate A' query response -              Lagrange.interpolate (A'.erase k) query response).degree          ≤ max (Lagrange.interpolate A' query response).degree                (Lagrange.interpolate (A'.erase k) query response).degree :=            Polynomial.degree_sub_le _ _        _ ≤ ↑(n + 1) := max_le (le_of_eq hA'_deg) (le_of_lt h_deg_ek)        _ < ↑(n + 2) := by exact_mod_cast (show n + 1 < n + 2 by omega)    · -- vanishes on T      intro x hx      simp only [Finset.mem_union, Finset.mem_image, Finset.mem_singleton] at hx      rw [Polynomial.eval_sub, sub_eq_zero]      rcases hx with ⟨m, hm, rfl⟩ | rfl      · rw [Lagrange.eval_interpolate_at_node response              (hquery.mono hA'_sub) (Finset.mem_of_mem_erase hm),            Lagrange.eval_interpolate_at_node response              (hquery.mono ((Finset.erase_subset k A').trans hA'_sub)) hm]      · rw [hA'_eval_tau, h_poly (A'.erase k) hek_sub hek_card]  -- But they can't be equal (degrees n vs < n)  have hne : Lagrange.interpolate A' query response ≠      Lagrange.interpolate (A'.erase k) query response := by    intro h    rw [h] at hA'_deg    exact absurd hA'_deg (ne_of_lt h_deg_ek)  exact hne (sub_eq_zero.mp hQ_zero)