Div by monic zs to poly eq nodal erase

lemma div_by_monic_zs_to_poly_eq_nodal_erase {L : ℕ}    (S : Finset (Fin L)) (query : Fin L → ZMod p)    (hquery : Set.InjOn query ↑S) (i : Fin L) (hi : i ∈ S) :    let Zₛ := ∏ s ∈ S.image query, (X - C s)    (Zₛ.divByMonic (X - C (query i))).toPoly      = Lagrange.nodal (S.erase i) query := by  intro Zₛ  have hq_toPoly : (X - C (query i) : CPolynomial (ZMod p)).toPoly      = Polynomial.X - Polynomial.C (query i) := by    rw [CPolynomial.toPoly_sub, X_toPoly, C_toPoly]  have hmonic : (X - C (query i) : CPolynomial (ZMod p)).toPoly.Monic := by    rw [hq_toPoly]; exact Polynomial.monic_X_sub_C _  rw [CPolynomial.toPoly_divByMonic _ _ hmonic, zs_to_poly_eq_nodal S query hquery, hq_toPoly,    Lagrange.nodal_eq_mul_nodal_erase hi]  exact Polynomial.mul_divByMonic_cancel_left _ (Polynomial.monic_X_sub_C _)