Indicator eq 1 on pos

lemma indicator_eq_1_on_pos {pos neg : Finset F} {x : F}  (h_pos : x ∈ pos) :  (indicator pos neg).eval x = 1 := by  unfold indicator  have {x} {y} (hy : y ∈ (pos ∪ neg).erase x) :    (x - y)⁻¹ * (x - y) = 1 :=      inv_mul_cancel₀ (sub_ne_zero_of_ne (by aesop))  rw [Polynomial.eval]  aesop      (add simp        [Polynomial.eval_prod,          Polynomial.eval₂_finsetSum,          Lagrange.basis,          Finset.prod_eq_zero_iff,          Lagrange.basis,          Lagrange.basisDivisor,          Finset.prod_eq_one])      (add safe [(by rw [Finset.sum_eq_single x])])