Lagrange zs conversion

lemma lagrange_zs_conversion {L : ℕ} (τ : ZMod p) (S : Finset (Fin L))    (query : Fin L → ZMod p) (response : Fin L → ZMod p)    (hτ : ∀ i ∈ S, (query i) ≠ τ) (hquery : Set.InjOn query ↑S) :    let Zₛ := ∏ s ∈ S.image query, (X - C s)    ((CLagrange.interpolate S query response).eval τ) / (Zₛ.eval τ)      = ∑ x ∈ S, response x /        (eval (query x) (Zₛ.divByMonic (X - C (query x))) * (τ - query x)) := by  intro Zₛ  -- Derive τ ≠ query i (Mathlib direction)  have hτ' : ∀ i ∈ S, τ ≠ query i := fun i hi => Ne.symm (hτ i hi)  -- Convert CPolynomial evals to Polynomial evals  have hZₛ_toPoly : Zₛ.toPoly = Lagrange.nodal S query := zs_to_poly_eq_nodal S query hquery  have hZₛ_eval : Zₛ.eval τ = Polynomial.eval τ (Lagrange.nodal S query) := by    rw [eval_toPoly, hZₛ_toPoly]  have hinterp_eval : (CLagrange.interpolate S query response).eval τ      = Polynomial.eval τ (Lagrange.interpolate S query response) := by    rw [eval_toPoly, CLagrange.cinterpolate_eq_interpolate]  rw [hinterp_eval, hZₛ_eval]  -- Apply first barycentric form  rw [Lagrange.eval_interpolate_not_at_node response hτ']  -- Cancel nodal(τ)  have hne : Polynomial.eval τ (Lagrange.nodal S query) ≠ 0 :=    Lagrange.eval_nodal_not_at_node hτ'  rw [mul_div_cancel_left₀ _ hne]  -- Match summands  apply Finset.sum_congr rfl  intro i hi  -- Rewrite nodalWeight using eval of nodal (S.erase i)  rw [Lagrange.nodalWeight_eq_eval_nodal_erase_inv]  -- Connect divByMonic eval to nodal (S.erase i) eval  have hdiv_eval : eval (query i) (Zₛ.divByMonic (X - C (query i)))      = Polynomial.eval (query i) (Lagrange.nodal (S.erase i) query) := by    rw [eval_toPoly, div_by_monic_zs_to_poly_eq_nodal_erase S query hquery i hi]  rw [hdiv_eval]  -- Field algebra: a⁻¹ * b⁻¹ * c = c / (a * b)  have heval_ne : Polynomial.eval (query i) (Lagrange.nodal (S.erase i) query) ≠ 0 :=    Lagrange.eval_nodal_not_at_node (fun j hj =>      fun h => (Finset.ne_of_mem_erase hj) (hquery hi (Finset.mem_of_mem_erase hj) h).symm)  have hτqi_ne : τ - query i ≠ 0 := sub_ne_zero.mpr (hτ' i hi)  field_simp